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