Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Daniel Larraz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of utility for inferring whether a synthesis conjecture
14 : : * encodes a transition system.
15 : : */
16 : : #include "theory/quantifiers/sygus/transition_inference.h"
17 : :
18 : : #include "expr/node_algorithm.h"
19 : : #include "expr/skolem_manager.h"
20 : : #include "theory/arith/arith_msum.h"
21 : : #include "theory/quantifiers/term_util.h"
22 : : #include "theory/rewriter.h"
23 : :
24 : : using namespace cvc5::internal::kind;
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : : namespace quantifiers {
29 : :
30 : 630 : bool DetTrace::DetTraceTrie::add(Node loc, const std::vector<Node>& val)
31 : : {
32 : 630 : DetTraceTrie* curr = this;
33 [ + + ]: 1876 : for (const Node& v : val)
34 : : {
35 : 1246 : curr = &(curr->d_children[v]);
36 : : }
37 [ + - ]: 630 : if (curr->d_children.empty())
38 : : {
39 : 630 : curr->d_children[loc].clear();
40 : 630 : return true;
41 : : }
42 : 0 : return false;
43 : : }
44 : :
45 : 14 : Node DetTrace::DetTraceTrie::constructFormula(NodeManager* nm,
46 : : const std::vector<Node>& vars,
47 : : unsigned index)
48 : : {
49 [ - + ]: 14 : if (index == vars.size())
50 : : {
51 : 0 : return nm->mkConst(true);
52 : : }
53 : 28 : std::vector<Node> disj;
54 [ + + ]: 48 : for (std::pair<const Node, DetTraceTrie>& p : d_children)
55 : : {
56 : 68 : Node eq = vars[index].eqNode(p.first);
57 [ + + ]: 34 : if (index < vars.size() - 1)
58 : : {
59 : 10 : Node conc = p.second.constructFormula(nm, vars, index + 1);
60 : 10 : disj.push_back(nm->mkNode(Kind::AND, eq, conc));
61 : : }
62 : : else
63 : : {
64 : 24 : disj.push_back(eq);
65 : : }
66 : : }
67 [ - + ][ - + ]: 14 : Assert(!disj.empty());
[ - - ]
68 [ + + ]: 14 : return disj.size() == 1 ? disj[0] : nm->mkNode(Kind::OR, disj);
69 : : }
70 : :
71 : 630 : bool DetTrace::increment(Node loc, std::vector<Node>& vals)
72 : : {
73 [ + - ]: 630 : if (d_trie.add(loc, vals))
74 : : {
75 [ + + ]: 1876 : for (unsigned i = 0, vsize = vals.size(); i < vsize; i++)
76 : : {
77 : 1246 : d_curr[i] = vals[i];
78 : : }
79 : 630 : return true;
80 : : }
81 : 0 : return false;
82 : : }
83 : :
84 : 4 : Node DetTrace::constructFormula(NodeManager* nm, const std::vector<Node>& vars)
85 : : {
86 : 4 : return d_trie.constructFormula(nm, vars);
87 : : }
88 : :
89 : 634 : void DetTrace::print(const char* c) const
90 : : {
91 [ + + ]: 1886 : for (const Node& n : d_curr)
92 : : {
93 [ + - ]: 1252 : Trace(c) << n << " ";
94 : : }
95 : 634 : }
96 : :
97 : 495 : Node TransitionInference::getFunction() const { return d_func; }
98 : :
99 : 602 : void TransitionInference::getVariables(std::vector<Node>& vars) const
100 : : {
101 : 602 : vars.insert(vars.end(), d_vars.begin(), d_vars.end());
102 : 602 : }
103 : :
104 : 602 : Node TransitionInference::getPreCondition() const { return d_pre.d_this; }
105 : 1226 : Node TransitionInference::getPostCondition() const { return d_post.d_this; }
106 : 1210 : Node TransitionInference::getTransitionRelation() const
107 : : {
108 : 1210 : return d_trans.d_this;
109 : : }
110 : :
111 : 1421 : void TransitionInference::getConstantSubstitution(
112 : : const std::vector<Node>& vars,
113 : : const std::vector<Node>& disjuncts,
114 : : std::vector<Node>& const_var,
115 : : std::vector<Node>& const_subs,
116 : : bool reqPol)
117 : : {
118 [ + + ]: 4547 : for (const Node& d : disjuncts)
119 : : {
120 : 6252 : Node sn;
121 [ + + ]: 3126 : if (!const_var.empty())
122 : : {
123 : 944 : sn = d.substitute(const_var.begin(),
124 : : const_var.end(),
125 : : const_subs.begin(),
126 : 472 : const_subs.end());
127 : 472 : sn = rewrite(sn);
128 : : }
129 : : else
130 : : {
131 : 2654 : sn = d;
132 : : }
133 : 3126 : bool slit_pol = sn.getKind() != Kind::NOT;
134 [ + + ]: 6252 : Node slit = sn.getKind() == Kind::NOT ? sn[0] : sn;
135 [ + + ][ + + ]: 3126 : if (slit.getKind() == Kind::EQUAL && slit_pol == reqPol)
[ + + ]
136 : : {
137 : : // check if it is a variable equality
138 : 844 : TNode v;
139 : 844 : Node s;
140 [ + + ]: 847 : for (unsigned r = 0; r < 2; r++)
141 : : {
142 [ + + ]: 663 : if (std::find(vars.begin(), vars.end(), slit[r]) != vars.end())
143 : : {
144 [ + + ]: 239 : if (!expr::hasSubterm(slit[1 - r], slit[r]))
145 : : {
146 : 238 : v = slit[r];
147 : 238 : s = slit[1 - r];
148 : 238 : break;
149 : : }
150 : : }
151 : : }
152 [ + + ]: 422 : if (v.isNull())
153 : : {
154 : : // solve for var
155 : 368 : std::map<Node, Node> msum;
156 [ + + ]: 184 : if (ArithMSum::getMonomialSumLit(slit, msum))
157 : : {
158 [ + + ]: 233 : for (std::pair<const Node, Node>& m : msum)
159 : : {
160 [ + + ]: 172 : if (std::find(vars.begin(), vars.end(), m.first) != vars.end())
161 : : {
162 : 108 : Node veq_c;
163 : 108 : Node val;
164 : : int ires =
165 : 54 : ArithMSum::isolate(m.first, msum, veq_c, val, Kind::EQUAL);
166 [ + - ]: 54 : if (ires != 0 && veq_c.isNull()
167 : 108 : && !expr::hasSubterm(val, m.first))
168 : : {
169 : 54 : v = m.first;
170 : 54 : s = val;
171 : : }
172 : : }
173 : : }
174 : : }
175 : : }
176 [ + + ]: 422 : if (!v.isNull())
177 : : {
178 : 584 : TNode ts = s;
179 [ + + ]: 486 : for (unsigned k = 0, csize = const_subs.size(); k < csize; k++)
180 : : {
181 : 194 : const_subs[k] = rewrite(const_subs[k].substitute(v, ts));
182 : : }
183 [ + - ]: 584 : Trace("cegqi-inv-debug2")
184 : 292 : << "...substitution : " << v << " -> " << s << std::endl;
185 : 292 : const_var.push_back(v);
186 : 292 : const_subs.push_back(s);
187 : : }
188 : : }
189 : : }
190 : 1421 : }
191 : :
192 : 1456 : void TransitionInference::process(Node n, Node f)
193 : : {
194 : : // set the function
195 : 1456 : d_func = f;
196 : 1456 : process(n);
197 : 1456 : }
198 : :
199 : 1456 : void TransitionInference::process(Node n)
200 : : {
201 : 1456 : NodeManager* nm = nodeManager();
202 : 1456 : d_complete = true;
203 : 1456 : d_trivial = true;
204 : 2912 : std::vector<Node> n_check;
205 [ + + ]: 1456 : if (n.getKind() == Kind::AND)
206 : : {
207 [ + + ]: 1559 : for (const Node& nc : n)
208 : : {
209 : 1090 : n_check.push_back(nc);
210 : : }
211 : : }
212 : : else
213 : : {
214 : 987 : n_check.push_back(n);
215 : : }
216 [ + + ]: 3533 : for (const Node& nn : n_check)
217 : : {
218 : 2077 : std::map<bool, std::map<Node, bool> > visited;
219 : 2077 : std::map<bool, Node> terms;
220 : 2077 : std::vector<Node> disjuncts;
221 [ + - ]: 4154 : Trace("cegqi-inv") << "TransitionInference : Process disjunct : " << nn
222 : 2077 : << std::endl;
223 [ + + ]: 2077 : if (!processDisjunct(nn, terms, disjuncts, visited, true))
224 : : {
225 : 283 : d_complete = false;
226 : 283 : continue;
227 : : }
228 [ + + ]: 1794 : if (terms.empty())
229 : : {
230 : 373 : continue;
231 : : }
232 : 1421 : Node curr;
233 : : // The component that this disjunct contributes to, where
234 : : // 1 : pre-condition, -1 : post-condition, 0 : transition relation
235 : : int comp_num;
236 : 1421 : std::map<bool, Node>::iterator itt = terms.find(false);
237 [ + + ]: 1421 : if (itt != terms.end())
238 : : {
239 : 909 : curr = itt->second;
240 [ + + ]: 909 : if (terms.find(true) != terms.end())
241 : : {
242 : 66 : comp_num = 0;
243 : : }
244 : : else
245 : : {
246 : 843 : comp_num = -1;
247 : : }
248 : : }
249 : : else
250 : : {
251 : 512 : curr = terms[true];
252 : 512 : comp_num = 1;
253 : : }
254 [ + - ]: 1421 : Trace("cegqi-inv-debug2") << " normalize based on " << curr << std::endl;
255 : 1421 : std::vector<Node> vars;
256 : 1421 : std::vector<Node> svars;
257 : 1421 : getNormalizedSubstitution(curr, d_vars, vars, svars, disjuncts);
258 [ + + ]: 4531 : for (unsigned j = 0, dsize = disjuncts.size(); j < dsize; j++)
259 : : {
260 [ + - ]: 3110 : Trace("cegqi-inv-debug2") << " apply " << disjuncts[j] << std::endl;
261 : 6220 : disjuncts[j] = rewrite(disjuncts[j].substitute(
262 : 3110 : vars.begin(), vars.end(), svars.begin(), svars.end()));
263 [ + - ]: 3110 : Trace("cegqi-inv-debug2") << " ..." << disjuncts[j] << std::endl;
264 : : }
265 : 1421 : std::vector<Node> const_var;
266 : 1421 : std::vector<Node> const_subs;
267 [ + + ]: 1421 : if (comp_num == 0)
268 : : {
269 : : // transition
270 [ - + ][ - + ]: 66 : Assert(terms.find(true) != terms.end());
[ - - ]
271 : 132 : Node next = terms[true];
272 : 132 : next = rewrite(next.substitute(
273 : 66 : vars.begin(), vars.end(), svars.begin(), svars.end()));
274 [ + - ]: 132 : Trace("cegqi-inv-debug")
275 : 66 : << "transition next predicate : " << next << std::endl;
276 : : // make the primed variables if we have not already
277 [ + - ]: 66 : if (d_prime_vars.empty())
278 : : {
279 [ + + ]: 374 : for (unsigned j = 0, nchild = next.getNumChildren(); j < nchild; j++)
280 : : {
281 : : Node v = NodeManager::mkDummySkolem(
282 : 924 : "ir", next[j].getType(), "template inference rev argument");
283 : 308 : d_prime_vars.push_back(v);
284 : : }
285 : : }
286 : : // normalize the other direction
287 [ + - ]: 66 : Trace("cegqi-inv-debug2") << " normalize based on " << next << std::endl;
288 : 132 : std::vector<Node> rvars;
289 : 132 : std::vector<Node> rsvars;
290 : 66 : getNormalizedSubstitution(next, d_prime_vars, rvars, rsvars, disjuncts);
291 [ - + ][ - + ]: 66 : Assert(rvars.size() == rsvars.size());
[ - - ]
292 [ + + ]: 368 : for (unsigned j = 0, dsize = disjuncts.size(); j < dsize; j++)
293 : : {
294 [ + - ]: 302 : Trace("cegqi-inv-debug2") << " apply " << disjuncts[j] << std::endl;
295 : 604 : disjuncts[j] = rewrite(disjuncts[j].substitute(
296 : 302 : rvars.begin(), rvars.end(), rsvars.begin(), rsvars.end()));
297 [ + - ]: 302 : Trace("cegqi-inv-debug2") << " ..." << disjuncts[j] << std::endl;
298 : : }
299 : 66 : getConstantSubstitution(
300 : 66 : d_prime_vars, disjuncts, const_var, const_subs, false);
301 : : }
302 : : else
303 : : {
304 : 1355 : getConstantSubstitution(d_vars, disjuncts, const_var, const_subs, false);
305 : : }
306 : 1421 : Node res;
307 [ + + ]: 1421 : if (disjuncts.empty())
308 : : {
309 : 12 : res = nm->mkConst(false);
310 : : }
311 [ + + ]: 1409 : else if (disjuncts.size() == 1)
312 : : {
313 : 309 : res = disjuncts[0];
314 : : }
315 : : else
316 : : {
317 : 1100 : res = nm->mkNode(Kind::OR, disjuncts);
318 : : }
319 [ + + ]: 1421 : if (expr::hasBoundVar(res))
320 : : {
321 [ + - ]: 626 : Trace("cegqi-inv-debug2") << "...failed, free variable." << std::endl;
322 : 626 : d_complete = false;
323 : 626 : continue;
324 : : }
325 [ + - ]: 1590 : Trace("cegqi-inv") << "*** inferred "
326 [ - - ]: 795 : << (comp_num == 1 ? "pre"
327 [ - - ]: 0 : : (comp_num == -1 ? "post" : "trans"))
328 : 795 : << "-condition : " << res << std::endl;
329 [ + + ][ + + ]: 795 : Component& c =
330 : : (comp_num == 1 ? d_pre : (comp_num == -1 ? d_post : d_trans));
331 : 795 : c.d_conjuncts.push_back(res);
332 [ + + ]: 795 : if (!const_var.empty())
333 : : {
334 : 133 : bool has_const_eq = const_var.size() == d_vars.size();
335 [ + - ]: 266 : Trace("cegqi-inv") << " with constant substitution, complete = "
336 : 133 : << has_const_eq << " : " << std::endl;
337 [ + + ]: 390 : for (unsigned i = 0, csize = const_var.size(); i < csize; i++)
338 : : {
339 [ + - ]: 514 : Trace("cegqi-inv") << " " << const_var[i] << " -> "
340 : 257 : << const_subs[i] << std::endl;
341 [ + + ]: 257 : if (has_const_eq)
342 : : {
343 : 144 : c.d_const_eq[res][const_var[i]] = const_subs[i];
344 : : }
345 : : }
346 [ + - ]: 266 : Trace("cegqi-inv") << "...size = " << const_var.size()
347 : 133 : << ", #vars = " << d_vars.size() << std::endl;
348 : : }
349 : : }
350 : :
351 : : // finalize the components
352 [ + + ]: 5824 : for (int i = -1; i <= 1; i++)
353 : : {
354 [ + + ][ + + ]: 4368 : Component& c = (i == 1 ? d_pre : (i == -1 ? d_post : d_trans));
355 : 8736 : Node ret;
356 [ + + ]: 4368 : if (c.d_conjuncts.empty())
357 : : {
358 : 3581 : ret = nm->mkConst(true);
359 : : }
360 [ + + ]: 787 : else if (c.d_conjuncts.size() == 1)
361 : : {
362 : 781 : ret = c.d_conjuncts[0];
363 : : }
364 : : else
365 : : {
366 : 6 : ret = nm->mkNode(Kind::AND, c.d_conjuncts);
367 : : }
368 [ + + ][ + + ]: 4368 : if (i == 0 || i == 1)
369 : : {
370 : : // pre-condition and transition are negated
371 : 2912 : ret = TermUtil::simpleNegate(ret);
372 : : }
373 : 4368 : c.d_this = ret;
374 : : }
375 : 1456 : }
376 : 1487 : void TransitionInference::getNormalizedSubstitution(
377 : : Node curr,
378 : : const std::vector<Node>& pvars,
379 : : std::vector<Node>& vars,
380 : : std::vector<Node>& subs,
381 : : std::vector<Node>& disjuncts)
382 : : {
383 [ + + ]: 4597 : for (unsigned j = 0, nchild = curr.getNumChildren(); j < nchild; j++)
384 : : {
385 [ + + ]: 3110 : if (curr[j].getKind() == Kind::BOUND_VARIABLE)
386 : : {
387 : : // if the argument is a bound variable, add to the renaming
388 : 3009 : vars.push_back(curr[j]);
389 : 3009 : subs.push_back(pvars[j]);
390 : : }
391 : : else
392 : : {
393 : : // otherwise, treat as a constraint on the variable
394 : : // For example, this transforms e.g. a precondition clause
395 : : // I( 0, 1 ) to x1 != 0 OR x2 != 1 OR I( x1, x2 ).
396 : 101 : Node eq = curr[j].eqNode(pvars[j]);
397 : 101 : disjuncts.push_back(eq.negate());
398 : : }
399 : : }
400 : 1487 : }
401 : :
402 : 22837 : bool TransitionInference::processDisjunct(
403 : : Node n,
404 : : std::map<bool, Node>& terms,
405 : : std::vector<Node>& disjuncts,
406 : : std::map<bool, std::map<Node, bool> >& visited,
407 : : bool topLevel)
408 : : {
409 [ + + ]: 22837 : if (visited[topLevel].find(n) != visited[topLevel].end())
410 : : {
411 : 4958 : return true;
412 : : }
413 : 17879 : visited[topLevel][n] = true;
414 [ + + ][ + + ]: 17879 : bool childTopLevel = n.getKind() == Kind::OR && topLevel;
415 : : // if another part mentions UF or a free variable, then fail
416 : 17879 : bool lit_pol = n.getKind() != Kind::NOT;
417 [ + + ]: 35758 : Node lit = n.getKind() == Kind::NOT ? n[0] : n;
418 : : // is it an application of the function-to-synthesize? Yes if we haven't
419 : : // encountered a function or if it matches the existing d_func.
420 : 53637 : if (lit.getKind() == Kind::APPLY_UF
421 [ + + ][ + - ]: 17879 : && (d_func.isNull() || lit.getOperator() == d_func))
[ + + ][ + + ]
[ + + ][ - - ]
422 : : {
423 : 3540 : Node op = lit.getOperator();
424 : : // initialize the variables
425 [ + + ]: 1770 : if (d_trivial)
426 : : {
427 : 1093 : d_trivial = false;
428 : 1093 : d_func = op;
429 [ + - ]: 1093 : Trace("cegqi-inv-debug") << "Use " << op << " with args ";
430 [ + + ]: 3235 : for (const Node& l : lit)
431 : : {
432 : : Node v = NodeManager::mkDummySkolem(
433 : 4284 : "i", l.getType(), "template inference argument");
434 : 2142 : d_vars.push_back(v);
435 [ + - ]: 2142 : Trace("cegqi-inv-debug") << v << " ";
436 : : }
437 [ + - ]: 1093 : Trace("cegqi-inv-debug") << std::endl;
438 : : }
439 [ - + ][ - + ]: 1770 : Assert(!d_func.isNull());
[ - - ]
440 [ + + ]: 1770 : if (topLevel)
441 : : {
442 [ + - ]: 1487 : if (terms.find(lit_pol) == terms.end())
443 : : {
444 : 1487 : terms[lit_pol] = lit;
445 : 1487 : return true;
446 : : }
447 : : else
448 : : {
449 [ - - ]: 0 : Trace("cegqi-inv-debug")
450 : 0 : << "...failed, repeated inv-app : " << lit << std::endl;
451 : 0 : return false;
452 : : }
453 : : }
454 [ + - ]: 566 : Trace("cegqi-inv-debug")
455 : 283 : << "...failed, non-entailed inv-app : " << lit << std::endl;
456 : 283 : return false;
457 : : }
458 [ + + ][ + + ]: 16109 : else if (topLevel && !childTopLevel)
459 : : {
460 : 3717 : disjuncts.push_back(n);
461 : : }
462 [ + + ]: 36404 : for (const Node& nc : n)
463 : : {
464 [ + + ]: 20760 : if (!processDisjunct(nc, terms, disjuncts, visited, childTopLevel))
465 : : {
466 : 465 : return false;
467 : : }
468 : : }
469 : 15644 : return true;
470 : : }
471 : :
472 : 43 : TraceIncStatus TransitionInference::initializeTrace(DetTrace& dt,
473 : : Node loc,
474 : : bool fwd)
475 : : {
476 [ + - ]: 43 : Component& c = fwd ? d_pre : d_post;
477 [ - + ][ - + ]: 43 : Assert(c.has(loc));
[ - - ]
478 : 43 : std::map<Node, std::map<Node, Node> >::iterator it = c.d_const_eq.find(loc);
479 [ + + ]: 43 : if (it != c.d_const_eq.end())
480 : : {
481 : 10 : std::vector<Node> next;
482 [ + + ]: 28 : for (const Node& v : d_vars)
483 : : {
484 [ - + ][ - + ]: 18 : Assert(it->second.find(v) != it->second.end());
[ - - ]
485 : 18 : next.push_back(it->second[v]);
486 : 18 : dt.d_curr.push_back(it->second[v]);
487 : : }
488 [ + - ]: 10 : Trace("cegqi-inv-debug2") << "dtrace : initial increment" << std::endl;
489 : 10 : bool ret = dt.increment(loc, next);
490 [ - + ][ - + ]: 10 : AlwaysAssert(ret);
[ - - ]
491 : 10 : return TRACE_INC_SUCCESS;
492 : : }
493 : 33 : return TRACE_INC_INVALID;
494 : : }
495 : :
496 : 624 : TraceIncStatus TransitionInference::incrementTrace(DetTrace& dt,
497 : : Node loc,
498 : : bool fwd)
499 : : {
500 [ - + ][ - + ]: 624 : Assert(d_trans.has(loc));
[ - - ]
501 : : // check if it satisfies the pre/post condition
502 [ + - ]: 1248 : Node cc = fwd ? getPostCondition() : getPreCondition();
503 [ - + ][ - + ]: 624 : Assert(!cc.isNull());
[ - - ]
504 : 624 : Node ccr = rewrite(cc.substitute(
505 : 2496 : d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
506 [ + - ]: 624 : if (ccr.isConst())
507 : : {
508 [ + - ][ - + ]: 624 : if (ccr.getConst<bool>() == (fwd ? false : true))
509 : : {
510 [ - - ]: 0 : Trace("cegqi-inv-debug2") << "dtrace : counterexample" << std::endl;
511 : 0 : return TRACE_INC_CEX;
512 : : }
513 : : }
514 : :
515 : : // terminates?
516 : 1248 : Node c = getTransitionRelation();
517 [ - + ][ - + ]: 624 : Assert(!c.isNull());
[ - - ]
518 : :
519 [ - + ][ - + ]: 624 : Assert(d_vars.size() == dt.d_curr.size());
[ - - ]
520 : 624 : Node cr = rewrite(c.substitute(
521 : 2496 : d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
522 [ + + ]: 624 : if (cr.isConst())
523 : : {
524 [ + - ]: 4 : if (!cr.getConst<bool>())
525 : : {
526 [ + - ]: 4 : Trace("cegqi-inv-debug2") << "dtrace : terminated" << std::endl;
527 : 4 : return TRACE_INC_TERMINATE;
528 : : }
529 : 0 : return TRACE_INC_INVALID;
530 : : }
531 [ - + ]: 620 : if (!fwd)
532 : : {
533 : : // only implemented in forward direction
534 : 0 : Assert(false);
535 : : return TRACE_INC_INVALID;
536 : : }
537 : 620 : Component& cm = d_trans;
538 : 620 : std::map<Node, std::map<Node, Node> >::iterator it = cm.d_const_eq.find(loc);
539 [ - + ]: 620 : if (it == cm.d_const_eq.end())
540 : : {
541 : 0 : return TRACE_INC_INVALID;
542 : : }
543 : 1240 : std::vector<Node> next;
544 [ + + ]: 1848 : for (const Node& pv : d_prime_vars)
545 : : {
546 [ - + ][ - + ]: 1228 : Assert(it->second.find(pv) != it->second.end());
[ - - ]
547 : 2456 : Node pvs = it->second[pv];
548 [ - + ][ - + ]: 1228 : Assert(d_vars.size() == dt.d_curr.size());
[ - - ]
549 : 1228 : Node pvsr = rewrite(pvs.substitute(
550 : 4912 : d_vars.begin(), d_vars.end(), dt.d_curr.begin(), dt.d_curr.end()));
551 : 1228 : next.push_back(pvsr);
552 : : }
553 [ + - ]: 620 : if (dt.increment(loc, next))
554 : : {
555 [ + - ]: 620 : Trace("cegqi-inv-debug2") << "dtrace : success increment" << std::endl;
556 : 620 : return TRACE_INC_SUCCESS;
557 : : }
558 : : // looped
559 [ - - ]: 0 : Trace("cegqi-inv-debug2") << "dtrace : looped" << std::endl;
560 : 0 : return TRACE_INC_TERMINATE;
561 : : }
562 : :
563 : 45 : TraceIncStatus TransitionInference::initializeTrace(DetTrace& dt, bool fwd)
564 : : {
565 [ + - ]: 45 : Trace("cegqi-inv-debug2") << "Initialize trace" << std::endl;
566 [ + - ]: 45 : Component& c = fwd ? d_pre : d_post;
567 [ + + ]: 45 : if (c.d_conjuncts.size() == 1)
568 : : {
569 : 43 : return initializeTrace(dt, c.d_conjuncts[0], fwd);
570 : : }
571 : 2 : return TRACE_INC_INVALID;
572 : : }
573 : :
574 : 624 : TraceIncStatus TransitionInference::incrementTrace(DetTrace& dt, bool fwd)
575 : : {
576 [ + - ]: 624 : if (d_trans.d_conjuncts.size() == 1)
577 : : {
578 : 624 : return incrementTrace(dt, d_trans.d_conjuncts[0], fwd);
579 : : }
580 : 0 : return TRACE_INC_INVALID;
581 : : }
582 : :
583 : 4 : Node TransitionInference::constructFormulaTrace(DetTrace& dt) const
584 : : {
585 : 4 : return dt.constructFormula(nodeManager(), d_vars);
586 : : }
587 : :
588 : : } // namespace quantifiers
589 : : } // namespace theory
590 : : } // namespace cvc5::internal
|
