Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * A technique for synthesizing candidate rewrites of the form t1 = t2,
11 : : * where t1 and t2 are subterms of the input.
12 : : */
13 : :
14 : : #include "preprocessing/passes/synth_rew_rules.h"
15 : :
16 : : #include <sstream>
17 : :
18 : : #include "expr/sygus_datatype.h"
19 : : #include "expr/term_canonize.h"
20 : : #include "options/base_options.h"
21 : : #include "options/datatypes_options.h"
22 : : #include "options/quantifiers_options.h"
23 : : #include "preprocessing/assertion_pipeline.h"
24 : : #include "printer/printer.h"
25 : : #include "printer/smt2/smt2_printer.h"
26 : : #include "smt/set_defaults.h"
27 : : #include "theory/quantifiers/candidate_rewrite_database.h"
28 : : #include "theory/quantifiers/quantifiers_attributes.h"
29 : : #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
30 : : #include "theory/quantifiers/sygus/sygus_utils.h"
31 : : #include "theory/quantifiers/term_util.h"
32 : : #include "theory/smt_engine_subsolver.h"
33 : :
34 : : using namespace std;
35 : : using namespace cvc5::internal::kind;
36 : :
37 : : namespace cvc5::internal {
38 : : namespace preprocessing {
39 : : namespace passes {
40 : :
41 : 50669 : SynthRewRulesPass::SynthRewRulesPass(PreprocessingPassContext* preprocContext)
42 : 50669 : : PreprocessingPass(preprocContext, "synth-rr"){};
43 : :
44 : 0 : PreprocessingPassResult SynthRewRulesPass::applyInternal(
45 : : AssertionPipeline* assertionsToPreprocess)
46 : : {
47 : 0 : return PreprocessingPassResult::NO_CONFLICT;
48 : : }
49 : :
50 : 11 : std::vector<TypeNode> SynthRewRulesPass::getGrammarsFrom(
51 : : Env& env, const std::vector<Node>& assertions, uint64_t nvars)
52 : : {
53 : 11 : std::vector<TypeNode> ret;
54 : : std::map<TypeNode, TypeNode> tlGrammarTypes =
55 : 11 : constructTopLevelGrammar(env, assertions, nvars);
56 [ + + ]: 38 : for (std::pair<const TypeNode, TypeNode> ttp : tlGrammarTypes)
57 : : {
58 : 27 : ret.push_back(ttp.second);
59 : 27 : }
60 : 22 : return ret;
61 : 11 : }
62 : :
63 : 11 : std::map<TypeNode, TypeNode> SynthRewRulesPass::constructTopLevelGrammar(
64 : : Env& env, const std::vector<Node>& assertions, uint64_t nvars)
65 : : {
66 : 11 : std::map<TypeNode, TypeNode> tlGrammarTypes;
67 [ - + ]: 11 : if (assertions.empty())
68 : : {
69 : 0 : return tlGrammarTypes;
70 : : }
71 : 11 : NodeManager* nm = env.getNodeManager();
72 : : // initialize the candidate rewrite
73 : 11 : std::unordered_map<TNode, bool> visited;
74 : 11 : std::unordered_map<TNode, bool>::iterator it;
75 : 11 : std::vector<TNode> visit;
76 : : // Get all usable terms from the input. A term is usable if it does not
77 : : // contain a quantified subterm
78 : 11 : std::vector<Node> terms;
79 : : // all variables (free constants) appearing in the input
80 : 11 : std::vector<Node> vars;
81 : : // does the input contain a Boolean variable?
82 : 11 : bool hasBoolVar = false;
83 : : // the types of subterms of our input
84 : 11 : std::map<TypeNode, bool> typesFound;
85 : : // standard constants for each type (e.g. true, false for Bool)
86 : 11 : std::map<TypeNode, std::vector<Node> > consts;
87 : :
88 : 11 : TNode cur;
89 [ + - ]: 11 : Trace("srs-input") << "Collect terms in assertions..." << std::endl;
90 [ + + ]: 23 : for (const Node& a : assertions)
91 : : {
92 [ + - ]: 12 : Trace("srs-input-debug") << "Assertion : " << a << std::endl;
93 : 12 : visit.push_back(a);
94 : : do
95 : : {
96 : 150 : cur = visit.back();
97 : 150 : visit.pop_back();
98 : : // we recurse on this node if it is not a quantified formula
99 [ + + ]: 150 : if (cur.isClosure())
100 : : {
101 : 3 : visited[cur] = false;
102 : 3 : continue;
103 : : }
104 : 147 : it = visited.find(cur);
105 [ + + ]: 147 : if (it == visited.end())
106 : : {
107 [ + - ]: 63 : Trace("srs-input-debug") << "...preprocess " << cur << std::endl;
108 : 63 : visited[cur] = false;
109 : 63 : visit.push_back(cur);
110 [ + + ]: 138 : for (const Node& cc : cur)
111 : : {
112 : 75 : visit.push_back(cc);
113 : 75 : }
114 : : }
115 [ + + ]: 84 : else if (!it->second)
116 : : {
117 [ + - ]: 63 : Trace("srs-input-debug") << "...postprocess " << cur << std::endl;
118 : : // check if all of the children are valid
119 : : // this ensures we do not register terms that have e.g. quantified
120 : : // formulas as subterms
121 : 63 : bool childrenValid = true;
122 [ + + ]: 138 : for (const Node& cc : cur)
123 : : {
124 [ - + ][ - + ]: 75 : Assert(visited.find(cc) != visited.end());
[ - - ]
125 [ + + ]: 75 : if (!visited[cc])
126 : : {
127 : 3 : childrenValid = false;
128 : : }
129 : 75 : }
130 [ + + ]: 63 : if (childrenValid)
131 : : {
132 [ + - ]: 61 : Trace("srs-input-debug") << "...children are valid" << std::endl;
133 [ + - ]: 61 : Trace("srs-input-debug") << "Add term " << cur << std::endl;
134 : 61 : TypeNode tn = cur.getType();
135 [ + + ]: 61 : if (cur.isVar())
136 : : {
137 : 14 : vars.push_back(cur);
138 [ + + ]: 14 : if (tn.isBoolean())
139 : : {
140 : 3 : hasBoolVar = true;
141 : : }
142 : : }
143 : : // register type information
144 [ + + ]: 61 : if (typesFound.find(tn) == typesFound.end())
145 : : {
146 : 27 : typesFound[tn] = true;
147 : : // add the standard constants for this type
148 : 27 : theory::quantifiers::SygusGrammarCons::mkSygusConstantsForType(
149 : 27 : env, tn, consts[tn]);
150 : : // We prepend them so that they come first in the grammar
151 : : // construction. The motivation is we'd prefer seeing e.g. "true"
152 : : // instead of (= x x) as a canonical term.
153 : 27 : terms.insert(terms.begin(), consts[tn].begin(), consts[tn].end());
154 : : }
155 : 61 : terms.push_back(cur);
156 : 61 : }
157 : 63 : visited[cur] = childrenValid;
158 : : }
159 [ + + ]: 150 : } while (!visit.empty());
160 : : }
161 [ + - ]: 11 : Trace("srs-input") << "...finished." << std::endl;
162 : :
163 [ + - ]: 11 : Trace("srs-input") << "Make synth variables for types..." << std::endl;
164 : : // We will generate a fixed number of variables per type. These are the
165 : : // variables that appear as free variables in the rewrites we generate.
166 : : // must have at least one variable per type
167 [ + - ]: 11 : nvars = nvars < 1 ? 1 : nvars;
168 : 11 : std::map<TypeNode, std::vector<Node> > tvars;
169 : 11 : std::vector<Node> allVars;
170 : 11 : uint64_t varCounter = 0;
171 [ + + ]: 38 : for (std::pair<const TypeNode, bool> tfp : typesFound)
172 : : {
173 : 27 : TypeNode tn = tfp.first;
174 : : // we do not allocate variables for non-first class types, e.g. regular
175 : : // expressions
176 [ + + ]: 27 : if (!env.isFirstClassType(tn))
177 : : {
178 : 3 : continue;
179 : : }
180 : : // If we are not interested in purely propositional rewrites, we only
181 : : // need to make one Boolean variable if the input has a Boolean variable.
182 : : // This ensures that no type in our grammar has zero constructors. If
183 : : // our input does not contain a Boolean variable, we need not allocate any
184 : : // Boolean variables here.
185 [ + + ][ + + ]: 24 : uint64_t useNVars = !tn.isBoolean() ? nvars : (hasBoolVar ? 1 : 0);
186 [ + + ]: 72 : for (uint64_t i = 0; i < useNVars; i++)
187 : : {
188 : : // We must have a good name for these variables, these are
189 : : // the ones output in rewrite rules. We choose
190 : : // a,b,c,...,y,z,x1,x2,...
191 : 48 : std::stringstream ssv;
192 [ + - ]: 48 : if (varCounter < 26)
193 : : {
194 : 48 : ssv << static_cast<char>(varCounter + static_cast<uint64_t>('A'));
195 : : }
196 : : else
197 : : {
198 : 0 : ssv << "x" << (varCounter - 26);
199 : : }
200 : 48 : varCounter++;
201 : 48 : Node v = NodeManager::mkBoundVar(ssv.str(), tn);
202 [ + - ]: 96 : Trace("srs-input") << "Make variable " << v << " of type " << tn
203 : 48 : << std::endl;
204 : 48 : tvars[tn].push_back(v);
205 : 48 : allVars.push_back(v);
206 : 48 : }
207 [ + + ][ + + ]: 30 : }
208 [ + - ]: 11 : Trace("srs-input") << "...finished." << std::endl;
209 : :
210 : : // if the problem is trivial, e.g. contains no non-constant terms, then we
211 : : // exit with an exception.
212 [ + + ]: 11 : if (allVars.empty())
213 : : {
214 : 1 : return tlGrammarTypes;
215 : : }
216 : :
217 [ + - ]: 20 : Trace("srs-input") << "Convert subterms to free variable form..."
218 : 10 : << std::endl;
219 : : // Replace all free variables with bound variables. This ensures that
220 : : // we can perform term canonization on subterms.
221 : 10 : std::vector<Node> vsubs;
222 [ + + ]: 24 : for (const Node& v : vars)
223 : : {
224 : 14 : TypeNode tnv = v.getType();
225 : 14 : Node vs = NodeManager::mkBoundVar(tnv);
226 : 14 : vsubs.push_back(vs);
227 : 14 : }
228 [ + + ]: 10 : if (!vars.empty())
229 : : {
230 [ + + ]: 98 : for (unsigned i = 0, nterms = terms.size(); i < nterms; i++)
231 : : {
232 : 178 : terms[i] = terms[i].substitute(
233 : 89 : vars.begin(), vars.end(), vsubs.begin(), vsubs.end());
234 : : }
235 : : }
236 [ + - ]: 10 : Trace("srs-input") << "...finished." << std::endl;
237 : :
238 [ + - ]: 20 : Trace("srs-input") << "Process " << terms.size() << " subterms..."
239 : 10 : << std::endl;
240 : : // We've collected all terms in the input. We construct a sygus grammar in
241 : : // following which generates terms that correspond to abstractions of the
242 : : // terms in the input.
243 : :
244 : : // We map terms to a canonical (ordered variable) form. This ensures that
245 : : // we don't generate distinct grammar types for distinct alpha-equivalent
246 : : // terms, which would produce grammars of identical shape.
247 : 10 : std::map<Node, Node> term_to_cterm;
248 : 10 : std::map<Node, Node> cterm_to_term;
249 : 10 : std::vector<Node> cterms;
250 : : // canonical terms for each type
251 : 10 : std::map<TypeNode, std::vector<Node> > t_cterms;
252 : 10 : expr::TermCanonize tcanon;
253 [ + + ]: 109 : for (unsigned i = 0, nterms = terms.size(); i < nterms; i++)
254 : : {
255 : 99 : Node n = terms[i];
256 : 99 : Node cn = tcanon.getCanonicalTerm(n);
257 : 99 : term_to_cterm[n] = cn;
258 [ + - ]: 99 : Trace("srs-input-debug") << "Canon : " << n << " -> " << cn << std::endl;
259 : 99 : std::map<Node, Node>::iterator itc = cterm_to_term.find(cn);
260 [ + + ]: 99 : if (itc == cterm_to_term.end())
261 : : {
262 : 92 : cterm_to_term[cn] = n;
263 : 92 : cterms.push_back(cn);
264 : 92 : t_cterms[cn.getType()].push_back(cn);
265 : : }
266 : 99 : }
267 [ + - ]: 10 : Trace("srs-input") << "...finished." << std::endl;
268 : : // the sygus variable list
269 : 10 : Node sygusVarList = nm->mkNode(Kind::BOUND_VAR_LIST, allVars);
270 [ + - ]: 20 : Trace("srs-input") << "Have " << cterms.size() << " canonical subterms."
271 : 10 : << std::endl;
272 : :
273 [ + - ]: 10 : Trace("srs-input") << "Construct unresolved types..." << std::endl;
274 : : // each canonical subterm corresponds to a grammar type
275 : 10 : std::vector<SygusDatatype> sdts;
276 : : // make unresolved types for each canonical term
277 : 10 : std::map<Node, TypeNode> cterm_to_utype;
278 [ + + ]: 102 : for (unsigned i = 0, ncterms = cterms.size(); i < ncterms; i++)
279 : : {
280 : 92 : Node ct = cterms[i];
281 : 92 : std::stringstream ss;
282 : 92 : ss << "T" << i;
283 : 92 : std::string tname = ss.str();
284 : 92 : TypeNode tnu = nm->mkUnresolvedDatatypeSort(tname);
285 : 92 : cterm_to_utype[ct] = tnu;
286 : 92 : sdts.push_back(SygusDatatype(tname));
287 : 92 : }
288 [ + - ]: 10 : Trace("srs-input") << "...finished." << std::endl;
289 : :
290 [ + - ]: 10 : Trace("srs-input") << "Construct sygus datatypes..." << std::endl;
291 [ + + ]: 102 : for (unsigned i = 0, ncterms = cterms.size(); i < ncterms; i++)
292 : : {
293 : 92 : Node ct = cterms[i];
294 : 92 : Node t = cterm_to_term[ct];
295 : :
296 : : // add the variables for the type
297 : 92 : TypeNode ctt = ct.getType();
298 : 92 : std::vector<TypeNode> argList;
299 : : // we add variable constructors if we are not Boolean, we are interested
300 : : // in purely propositional rewrites (via the option), or this term is
301 : : // a Boolean variable.
302 [ + + ][ + + ]: 92 : if (!ctt.isBoolean() || ct.getKind() == Kind::BOUND_VARIABLE)
[ + + ]
303 : : {
304 : : // may or may not have variables for this type
305 [ + + ]: 59 : if (tvars.find(ctt) != tvars.end())
306 : : {
307 [ + + ]: 198 : for (const Node& v : tvars[ctt])
308 : : {
309 : 147 : std::stringstream ssc;
310 : 147 : ssc << "C_" << i << "_" << v;
311 : 147 : sdts[i].addConstructor(v, ssc.str(), argList);
312 : 147 : }
313 : : }
314 : : }
315 : : // add the constructor for the operator if it is not a variable
316 [ + + ]: 92 : if (!ct.isVar())
317 : : {
318 : : // note that some terms like re.allchar have operators despite having
319 : : // no children, we should take ct itself in these cases
320 : : Node op =
321 [ + + ][ + - ]: 80 : (ct.getNumChildren() > 0 && ct.hasOperator()) ? ct.getOperator() : ct;
322 : : // iterate over the original term
323 [ + + ]: 149 : for (const Node& tc : t)
324 : : {
325 : : // map its arguments back to canonical
326 [ - + ][ - + ]: 69 : Assert(term_to_cterm.find(tc) != term_to_cterm.end());
[ - - ]
327 : 69 : Node ctc = term_to_cterm[tc];
328 [ - + ][ - + ]: 69 : Assert(cterm_to_utype.find(ctc) != cterm_to_utype.end());
[ - - ]
329 : : // get the type
330 : 69 : argList.push_back(cterm_to_utype[ctc]);
331 : 69 : }
332 : : // check if we should chain
333 : 80 : Kind k = NodeManager::operatorToKind(op);
334 : 80 : bool do_chain = argList.size() > 2
335 [ - + ]: 3 : && theory::quantifiers::TermUtil::isAssoc(k)
336 [ + + ][ - - ]: 83 : && theory::quantifiers::TermUtil::isComm(k);
337 [ - + ]: 80 : if (do_chain)
338 : : {
339 : : // eliminate duplicate child types
340 : 0 : std::set<TypeNode> argSet(argList.begin(), argList.end());
341 : :
342 : : // we make one type per child
343 : : // the operator of each constructor is a no-op
344 : 0 : Node tbv = NodeManager::mkBoundVar(ctt);
345 : : Node lambdaOp = nm->mkNode(
346 : 0 : Kind::LAMBDA, nm->mkNode(Kind::BOUND_VAR_LIST, tbv), tbv);
347 : 0 : std::vector<TypeNode> argListc;
348 : : // the following construction admits any number of repeated factors,
349 : : // so for instance, t1+t2+t3, we generate the grammar:
350 : : // T_{t1+t2+t3} ->
351 : : // +( T_{t1+t2+t3}, T_{t1+t2+t3} ) | T_{t1} | T_{t2} | T_{t3}
352 : : // where we write T_t to denote "the type that abstracts term t".
353 : : // Notice this construction allows to abstract subsets of the factors
354 : : // of t1+t2+t3. This is particularly helpful for terms t1+...+tn for
355 : : // large n, where we would like to consider binary applications of +.
356 : 0 : size_t j = 0;
357 [ - - ]: 0 : for (const TypeNode& arg : argSet)
358 : : {
359 : 0 : argListc.clear();
360 : 0 : argListc.push_back(arg);
361 : 0 : std::stringstream sscs;
362 : 0 : sscs << "C_factor_" << i << "_" << j;
363 [ - - ]: 0 : Trace("srs-input-cons") << "Add (nested chain) " << lambdaOp << " "
364 : 0 : << lambdaOp.getType() << std::endl;
365 : : // ID function is not printed and does not count towards weight
366 : 0 : sdts[i].addConstructor(lambdaOp,
367 : 0 : sscs.str(),
368 : : argListc,
369 : : 0);
370 : 0 : j++;
371 : 0 : }
372 : : // recursive apply
373 : 0 : TypeNode recType = cterm_to_utype[ct];
374 : 0 : argListc.clear();
375 : 0 : argListc.push_back(recType);
376 : 0 : argListc.push_back(recType);
377 : 0 : std::stringstream ssc;
378 : 0 : ssc << "C_" << i << "_rec_" << op;
379 [ - - ]: 0 : Trace("srs-input-cons")
380 : 0 : << "Add (chain) " << op << " " << op.getType() << std::endl;
381 : 0 : sdts[i].addConstructor(op, ssc.str(), argListc);
382 : 0 : }
383 : : else
384 : : {
385 : 80 : std::stringstream ssc;
386 : 80 : ssc << "C_" << i << "_" << op;
387 [ + - ]: 160 : Trace("srs-input-cons")
388 [ - + ][ - - ]: 80 : << "Add " << op << " " << op.getType() << std::endl;
389 : 80 : sdts[i].addConstructor(op, ssc.str(), argList);
390 : 80 : }
391 : 80 : }
392 [ - + ][ - + ]: 92 : Assert(sdts[i].getNumConstructors() > 0);
[ - - ]
393 : 92 : sdts[i].initializeDatatype(ctt, sygusVarList, false, false);
394 : 92 : }
395 [ + - ]: 10 : Trace("srs-input") << "...finished." << std::endl;
396 : :
397 [ + - ]: 20 : Trace("srs-input") << "Make mutual datatype types for subterms..."
398 : 10 : << std::endl;
399 : : // extract the datatypes
400 : 10 : std::vector<DType> datatypes;
401 [ + + ]: 102 : for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++)
402 : : {
403 : 92 : datatypes.push_back(sdts[i].getDatatype());
404 : : }
405 : 10 : std::vector<TypeNode> types = nm->mkMutualDatatypeTypes(datatypes);
406 [ + - ]: 10 : Trace("srs-input") << "...finished." << std::endl;
407 [ - + ][ - + ]: 10 : Assert(types.size() == datatypes.size());
[ - - ]
408 : 10 : std::map<Node, TypeNode> subtermTypes;
409 [ + + ]: 102 : for (unsigned i = 0, ncterms = cterms.size(); i < ncterms; i++)
410 : : {
411 : 92 : subtermTypes[cterms[i]] = types[i];
412 : : }
413 : :
414 [ + - ]: 10 : Trace("srs-input") << "Construct the top-level types..." << std::endl;
415 : : // we now are ready to create the "top-level" types
416 [ + + ]: 37 : for (std::pair<const TypeNode, std::vector<Node> >& tcp : t_cterms)
417 : : {
418 : 27 : TypeNode t = tcp.first;
419 : 27 : std::stringstream ss;
420 : 27 : ss << "T_" << t;
421 : 27 : SygusDatatype sdttl(ss.str());
422 : 27 : Node tbv = NodeManager::mkBoundVar(t);
423 : : // the operator of each constructor is a no-op
424 : : Node lambdaOp =
425 : 54 : nm->mkNode(Kind::LAMBDA, nm->mkNode(Kind::BOUND_VAR_LIST, tbv), tbv);
426 [ + - ]: 54 : Trace("srs-input") << " We have " << tcp.second.size()
427 : 27 : << " subterms of type " << t << std::endl;
428 [ + + ]: 119 : for (unsigned i = 0, size = tcp.second.size(); i < size; i++)
429 : : {
430 : 92 : Node n = tcp.second[i];
431 : : // add constructor that encodes abstractions of this subterm
432 : 92 : std::vector<TypeNode> argList;
433 [ - + ][ - + ]: 92 : Assert(subtermTypes.find(n) != subtermTypes.end());
[ - - ]
434 : 92 : argList.push_back(subtermTypes[n]);
435 : 92 : std::stringstream ssc;
436 : 92 : ssc << "Ctl_" << i;
437 : : // the no-op should not be printed, hence we pass an empty callback
438 : 92 : sdttl.addConstructor(lambdaOp,
439 : 184 : ssc.str(),
440 : : argList,
441 : : 0);
442 [ + - ]: 184 : Trace("srs-input-debug")
443 : 92 : << "Grammar for subterm " << n << " is: " << std::endl;
444 [ + - ]: 92 : Trace("srs-input-debug") << subtermTypes[n].getDType() << std::endl;
445 : 92 : }
446 : : // set that this is a sygus datatype
447 : 27 : sdttl.initializeDatatype(t, sygusVarList, false, false);
448 : 27 : DType dttl = sdttl.getDatatype();
449 : 27 : TypeNode tlt = nm->mkDatatypeType(dttl);
450 : 27 : tlGrammarTypes[t] = tlt;
451 [ + - ]: 27 : Trace("srs-input") << "Grammar is: " << std::endl;
452 [ + - ][ - + ]: 54 : Trace("srs-input") << printer::smt2::Smt2Printer::sygusGrammarString(tlt)
[ - - ]
453 : 27 : << std::endl;
454 : 27 : }
455 [ + - ]: 10 : Trace("srs-input") << "...finished." << std::endl;
456 : 10 : return tlGrammarTypes;
457 : 11 : }
458 : :
459 : : } // namespace passes
460 : : } // namespace preprocessing
461 : : } // namespace cvc5::internal
|
