1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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 the sygus extension of the theory of datatypes. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/datatypes/sygus_extension.h" |
17 |
|
|
18 |
|
#include "expr/dtype.h" |
19 |
|
#include "expr/dtype_cons.h" |
20 |
|
#include "expr/node_manager.h" |
21 |
|
#include "expr/skolem_manager.h" |
22 |
|
#include "expr/sygus_datatype.h" |
23 |
|
#include "options/base_options.h" |
24 |
|
#include "options/datatypes_options.h" |
25 |
|
#include "options/quantifiers_options.h" |
26 |
|
#include "printer/printer.h" |
27 |
|
#include "smt/logic_exception.h" |
28 |
|
#include "theory/datatypes/inference_manager.h" |
29 |
|
#include "theory/datatypes/sygus_datatype_utils.h" |
30 |
|
#include "theory/datatypes/theory_datatypes_utils.h" |
31 |
|
#include "theory/quantifiers/sygus/sygus_explain.h" |
32 |
|
#include "theory/quantifiers/sygus/synth_conjecture.h" |
33 |
|
#include "theory/quantifiers/sygus/term_database_sygus.h" |
34 |
|
#include "theory/quantifiers/term_util.h" |
35 |
|
#include "theory/rewriter.h" |
36 |
|
#include "theory/theory_model.h" |
37 |
|
#include "theory/theory_state.h" |
38 |
|
|
39 |
|
using namespace cvc5; |
40 |
|
using namespace cvc5::kind; |
41 |
|
using namespace cvc5::context; |
42 |
|
using namespace cvc5::theory; |
43 |
|
using namespace cvc5::theory::datatypes; |
44 |
|
|
45 |
1228 |
SygusExtension::SygusExtension(Env& env, |
46 |
|
TheoryState& s, |
47 |
|
InferenceManager& im, |
48 |
1228 |
quantifiers::TermDbSygus* tds) |
49 |
|
: EnvObj(env), |
50 |
|
d_state(s), |
51 |
|
d_im(im), |
52 |
|
d_tds(tds), |
53 |
|
d_ssb(tds), |
54 |
|
d_testers(s.getSatContext()), |
55 |
|
d_testers_exp(s.getSatContext()), |
56 |
|
d_active_terms(s.getSatContext()), |
57 |
1228 |
d_currTermSize(s.getSatContext()) |
58 |
|
{ |
59 |
1228 |
d_zero = NodeManager::currentNM()->mkConst(Rational(0)); |
60 |
1228 |
d_true = NodeManager::currentNM()->mkConst(true); |
61 |
1228 |
} |
62 |
|
|
63 |
2452 |
SygusExtension::~SygusExtension() { |
64 |
|
|
65 |
2452 |
} |
66 |
|
|
67 |
|
/** add tester */ |
68 |
308373 |
void SygusExtension::assertTester(int tindex, TNode n, Node exp) |
69 |
|
{ |
70 |
308373 |
registerTerm(n); |
71 |
|
// check if this is a relevant (sygus) term |
72 |
308373 |
if( d_term_to_anchor.find( n )!=d_term_to_anchor.end() ){ |
73 |
286597 |
Trace("sygus-sb-debug2") << "Sygus : process tester : " << exp << std::endl; |
74 |
|
// if not already active (may have duplicate calls for the same tester) |
75 |
286597 |
if( d_active_terms.find( n )==d_active_terms.end() ) { |
76 |
255908 |
d_testers[n] = tindex; |
77 |
255908 |
d_testers_exp[n] = exp; |
78 |
|
|
79 |
|
// check if parent is active |
80 |
255908 |
bool do_add = true; |
81 |
255908 |
if( options::sygusSymBreakLazy() ){ |
82 |
255900 |
if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){ |
83 |
235664 |
NodeSet::const_iterator it = d_active_terms.find( n[0] ); |
84 |
235664 |
if( it==d_active_terms.end() ){ |
85 |
143302 |
do_add = false; |
86 |
|
}else{ |
87 |
|
//this must be a proper selector |
88 |
92362 |
IntMap::const_iterator itt = d_testers.find( n[0] ); |
89 |
92362 |
Assert(itt != d_testers.end()); |
90 |
92362 |
int ptindex = (*itt).second; |
91 |
184724 |
TypeNode ptn = n[0].getType(); |
92 |
92362 |
const DType& pdt = ptn.getDType(); |
93 |
|
int sindex_in_parent = |
94 |
92362 |
pdt[ptindex].getSelectorIndexInternal(n.getOperator()); |
95 |
|
// the tester is irrelevant in this branch |
96 |
92362 |
if( sindex_in_parent==-1 ){ |
97 |
51568 |
do_add = false; |
98 |
|
} |
99 |
|
} |
100 |
|
} |
101 |
|
} |
102 |
255908 |
if( do_add ){ |
103 |
61038 |
assertTesterInternal(tindex, n, exp); |
104 |
|
}else{ |
105 |
194870 |
Trace("sygus-sb-debug2") << "...ignore inactive tester : " << exp << std::endl; |
106 |
|
} |
107 |
|
}else{ |
108 |
30689 |
Trace("sygus-sb-debug2") << "...ignore repeated tester : " << exp << std::endl; |
109 |
|
} |
110 |
|
}else{ |
111 |
21776 |
Trace("sygus-sb-debug2") << "...ignore non-sygus tester : " << exp << std::endl; |
112 |
|
} |
113 |
308373 |
} |
114 |
|
|
115 |
1994636 |
void SygusExtension::assertFact(Node n, bool polarity) |
116 |
|
{ |
117 |
1994636 |
if (n.getKind() == kind::DT_SYGUS_BOUND) |
118 |
|
{ |
119 |
17644 |
Node m = n[0]; |
120 |
8822 |
Trace("sygus-fair") << "Have sygus bound : " << n << ", polarity=" << polarity << " on measure " << m << std::endl; |
121 |
8822 |
registerMeasureTerm( m ); |
122 |
8822 |
if (options::sygusFair() == options::SygusFairMode::DT_SIZE) |
123 |
|
{ |
124 |
|
std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator its = |
125 |
8819 |
d_szinfo.find(m); |
126 |
8819 |
Assert(its != d_szinfo.end()); |
127 |
17638 |
Node mt = its->second->getOrMkMeasureValue(); |
128 |
|
//it relates the measure term to arithmetic |
129 |
17638 |
Node blem = n.eqNode( NodeManager::currentNM()->mkNode( kind::LEQ, mt, n[1] ) ); |
130 |
8819 |
d_im.lemma(blem, InferenceId::DATATYPES_SYGUS_FAIR_SIZE); |
131 |
|
} |
132 |
8822 |
if( polarity ){ |
133 |
6441 |
uint64_t s = n[1].getConst<Rational>().getNumerator().toUnsignedInt(); |
134 |
6441 |
notifySearchSize(m, s, n); |
135 |
|
} |
136 |
1985814 |
}else if( n.getKind() == kind::DT_HEIGHT_BOUND || n.getKind()==DT_SIZE_BOUND ){ |
137 |
|
//reduce to arithmetic TODO ? |
138 |
|
|
139 |
|
} |
140 |
1994636 |
} |
141 |
|
|
142 |
219 |
Node SygusExtension::getTermOrderPredicate( Node n1, Node n2 ) { |
143 |
219 |
NodeManager* nm = NodeManager::currentNM(); |
144 |
438 |
std::vector< Node > comm_disj; |
145 |
|
// size of left is greater than or equal to the size of right |
146 |
|
Node szGeq = |
147 |
219 |
nm->mkNode(GEQ, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2)); |
148 |
438 |
return szGeq; |
149 |
|
} |
150 |
|
|
151 |
309762 |
void SygusExtension::registerTerm(Node n) |
152 |
|
{ |
153 |
309762 |
if( d_is_top_level.find( n )==d_is_top_level.end() ){ |
154 |
1904 |
d_is_top_level[n] = false; |
155 |
3808 |
TypeNode tn = n.getType(); |
156 |
1904 |
unsigned d = 0; |
157 |
1904 |
bool is_top_level = false; |
158 |
1904 |
bool success = false; |
159 |
1904 |
if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){ |
160 |
1389 |
registerTerm(n[0]); |
161 |
1389 |
std::unordered_map<Node, Node>::iterator it = d_term_to_anchor.find(n[0]); |
162 |
1389 |
if( it!=d_term_to_anchor.end() ) { |
163 |
1331 |
d_term_to_anchor[n] = it->second; |
164 |
|
unsigned sel_weight = |
165 |
1331 |
d_tds->getSelectorWeight(n[0].getType(), n.getOperator()); |
166 |
1331 |
d = d_term_to_depth[n[0]] + sel_weight; |
167 |
1331 |
is_top_level = computeTopLevel( tn, n[0] ); |
168 |
1331 |
success = true; |
169 |
|
} |
170 |
515 |
}else if( n.isVar() ){ |
171 |
497 |
registerSizeTerm(n); |
172 |
497 |
if( d_register_st[n] ){ |
173 |
446 |
d_term_to_anchor[n] = n; |
174 |
446 |
d_anchor_to_conj[n] = d_tds->getConjectureForEnumerator(n); |
175 |
|
// this assertion fails if we have a sygus term in the search that is unmeasured |
176 |
446 |
d = 0; |
177 |
446 |
is_top_level = true; |
178 |
446 |
success = true; |
179 |
|
} |
180 |
|
} |
181 |
1904 |
if( success ){ |
182 |
3554 |
Trace("sygus-sb-debug") |
183 |
1777 |
<< "Register : " << n << ", depth : " << d |
184 |
1777 |
<< ", top level = " << is_top_level |
185 |
1777 |
<< ", type = " << tn.getDType().getName() << std::endl; |
186 |
1777 |
d_term_to_depth[n] = d; |
187 |
1777 |
d_is_top_level[n] = is_top_level; |
188 |
1777 |
registerSearchTerm(tn, d, n, is_top_level); |
189 |
|
}else{ |
190 |
127 |
Trace("sygus-sb-debug2") << "Term " << n << " is not part of sygus search." << std::endl; |
191 |
|
} |
192 |
|
} |
193 |
309762 |
} |
194 |
|
|
195 |
1834 |
bool SygusExtension::computeTopLevel( TypeNode tn, Node n ){ |
196 |
1834 |
if( n.getType()==tn ){ |
197 |
899 |
return false; |
198 |
935 |
}else if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){ |
199 |
503 |
return computeTopLevel( tn, n[0] ); |
200 |
|
}else{ |
201 |
432 |
return true; |
202 |
|
} |
203 |
|
} |
204 |
|
|
205 |
67485 |
void SygusExtension::assertTesterInternal(int tindex, TNode n, Node exp) |
206 |
|
{ |
207 |
134970 |
TypeNode ntn = n.getType(); |
208 |
67485 |
if (!ntn.isDatatype()) |
209 |
|
{ |
210 |
|
// nothing to do for non-datatype types |
211 |
|
return; |
212 |
|
} |
213 |
67485 |
const DType& dt = ntn.getDType(); |
214 |
67485 |
if (!dt.isSygus()) |
215 |
|
{ |
216 |
|
// nothing to do for non-sygus-datatype type |
217 |
|
return; |
218 |
|
} |
219 |
67485 |
d_active_terms.insert(n); |
220 |
134970 |
Trace("sygus-sb-debug2") << "Sygus : activate term : " << n << " : " << exp |
221 |
67485 |
<< std::endl; |
222 |
|
|
223 |
|
// get the search size for this |
224 |
67485 |
Assert(d_term_to_anchor.find(n) != d_term_to_anchor.end()); |
225 |
134970 |
Node a = d_term_to_anchor[n]; |
226 |
67485 |
Assert(d_anchor_to_measure_term.find(a) != d_anchor_to_measure_term.end()); |
227 |
134970 |
Node m = d_anchor_to_measure_term[a]; |
228 |
|
std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator itsz = |
229 |
67485 |
d_szinfo.find(m); |
230 |
67485 |
Assert(itsz != d_szinfo.end()); |
231 |
67485 |
unsigned ssz = itsz->second->d_curr_search_size; |
232 |
|
|
233 |
67485 |
if (options::sygusFair() == options::SygusFairMode::DIRECT) |
234 |
|
{ |
235 |
3 |
if( dt[tindex].getNumArgs()>0 ){ |
236 |
|
quantifiers::SygusTypeInfo& nti = d_tds->getTypeInfo(ntn); |
237 |
|
// consider lower bounds for size of types |
238 |
|
unsigned lb_add = nti.getMinConsTermSize(tindex); |
239 |
|
unsigned lb_rem = n == a ? 0 : nti.getMinTermSize(); |
240 |
|
Assert(lb_add >= lb_rem); |
241 |
|
d_currTermSize[a].set( d_currTermSize[a].get() + ( lb_add - lb_rem ) ); |
242 |
|
} |
243 |
3 |
if( (unsigned)d_currTermSize[a].get()>ssz ){ |
244 |
|
if( Trace.isOn("sygus-sb-fair") ){ |
245 |
|
std::map< TypeNode, int > var_count; |
246 |
|
Node templ = getCurrentTemplate( a, var_count ); |
247 |
|
Trace("sygus-sb-fair") << "FAIRNESS : we have " << d_currTermSize[a].get() << " at search size " << ssz << ", template is " << templ << std::endl; |
248 |
|
} |
249 |
|
// conflict |
250 |
|
std::vector< Node > conflict; |
251 |
|
for( NodeSet::const_iterator its = d_active_terms.begin(); its != d_active_terms.end(); ++its ){ |
252 |
|
Node x = *its; |
253 |
|
Node xa = d_term_to_anchor[x]; |
254 |
|
if( xa==a ){ |
255 |
|
IntMap::const_iterator ittv = d_testers.find( x ); |
256 |
|
Assert(ittv != d_testers.end()); |
257 |
|
int tidx = (*ittv).second; |
258 |
|
const DType& dti = x.getType().getDType(); |
259 |
|
if (dti[tidx].getNumArgs() > 0) |
260 |
|
{ |
261 |
|
NodeMap::const_iterator itt = d_testers_exp.find( x ); |
262 |
|
Assert(itt != d_testers_exp.end()); |
263 |
|
conflict.push_back( (*itt).second ); |
264 |
|
} |
265 |
|
} |
266 |
|
} |
267 |
|
Assert(conflict.size() == (unsigned)d_currTermSize[a].get()); |
268 |
|
Assert(itsz->second->d_search_size_exp.find(ssz) |
269 |
|
!= itsz->second->d_search_size_exp.end()); |
270 |
|
conflict.push_back( itsz->second->d_search_size_exp[ssz] ); |
271 |
|
Node conf = NodeManager::currentNM()->mkNode( kind::AND, conflict ); |
272 |
|
Trace("sygus-sb-fair") << "Conflict is : " << conf << std::endl; |
273 |
|
Node confn = conf.negate(); |
274 |
|
d_im.lemma(confn, InferenceId::DATATYPES_SYGUS_FAIR_SIZE_CONFLICT); |
275 |
|
return; |
276 |
|
} |
277 |
|
} |
278 |
|
|
279 |
|
// now, add all applicable symmetry breaking lemmas for this term |
280 |
67485 |
Assert(d_term_to_depth.find(n) != d_term_to_depth.end()); |
281 |
67485 |
unsigned d = d_term_to_depth[n]; |
282 |
67485 |
Trace("sygus-sb-fair-debug") << "Tester " << exp << " is for depth " << d << " term in search size " << ssz << std::endl; |
283 |
|
//Assert( d<=ssz ); |
284 |
67485 |
if( options::sygusSymBreakLazy() ){ |
285 |
|
// dynamic symmetry breaking |
286 |
67477 |
addSymBreakLemmasFor(ntn, n, d); |
287 |
|
} |
288 |
|
|
289 |
67485 |
Trace("sygus-sb-debug") << "Get simple symmetry breaking predicates...\n"; |
290 |
67485 |
unsigned max_depth = ssz>=d ? ssz-d : 0; |
291 |
67485 |
unsigned min_depth = d_simple_proc[exp]; |
292 |
67485 |
NodeManager* nm = NodeManager::currentNM(); |
293 |
67485 |
if( min_depth<=max_depth ){ |
294 |
11424 |
TNode x = getFreeVar( ntn ); |
295 |
11424 |
std::vector<std::pair<Node, InferenceId>> sbLemmas; |
296 |
|
// symmetry breaking lemmas requiring predicate elimination |
297 |
11424 |
std::map<Node, bool> sb_elim_pred; |
298 |
5712 |
bool usingSymCons = d_tds->usingSymbolicConsForEnumerator(m); |
299 |
5712 |
bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(m); |
300 |
14984 |
for (unsigned ds = 0; ds <= max_depth; ds++) |
301 |
|
{ |
302 |
|
// static conjecture-independent symmetry breaking |
303 |
9272 |
Trace("sygus-sb-debug") << " simple symmetry breaking...\n"; |
304 |
|
Node ipred = getSimpleSymBreakPred( |
305 |
18544 |
m, ntn, tindex, ds, usingSymCons, isVarAgnostic); |
306 |
9272 |
if (!ipred.isNull()) |
307 |
|
{ |
308 |
6731 |
sbLemmas.emplace_back(ipred, |
309 |
13462 |
InferenceId::DATATYPES_SYGUS_SIMPLE_SYM_BREAK); |
310 |
6731 |
if (ds == 0 && isVarAgnostic) |
311 |
|
{ |
312 |
3 |
sb_elim_pred[ipred] = true; |
313 |
|
} |
314 |
|
} |
315 |
|
// static conjecture-dependent symmetry breaking |
316 |
18544 |
Trace("sygus-sb-debug") |
317 |
9272 |
<< " conjecture-dependent symmetry breaking...\n"; |
318 |
|
std::map<Node, quantifiers::SynthConjecture*>::iterator itc = |
319 |
9272 |
d_anchor_to_conj.find(a); |
320 |
9272 |
if (itc != d_anchor_to_conj.end()) |
321 |
|
{ |
322 |
9272 |
quantifiers::SynthConjecture* conj = itc->second; |
323 |
9272 |
if (conj) |
324 |
|
{ |
325 |
|
Node dpred = |
326 |
17838 |
conj->getSymmetryBreakingPredicate(x, a, ntn, tindex, ds); |
327 |
8919 |
if (!dpred.isNull()) |
328 |
|
{ |
329 |
|
sbLemmas.emplace_back(dpred, |
330 |
|
InferenceId::DATATYPES_SYGUS_CDEP_SYM_BREAK); |
331 |
|
} |
332 |
|
} |
333 |
|
} |
334 |
|
} |
335 |
|
|
336 |
|
// add the above symmetry breaking predicates to lemmas |
337 |
11424 |
std::unordered_map<TNode, TNode> cache; |
338 |
11424 |
Node rlv = getRelevancyCondition(n); |
339 |
12443 |
for (std::pair<Node, InferenceId>& sbl : sbLemmas) |
340 |
|
{ |
341 |
13462 |
Node slem = sbl.first; |
342 |
13462 |
Node sslem = slem.substitute(x, n, cache); |
343 |
|
// if we require predicate elimination |
344 |
6731 |
if (sb_elim_pred.find(slem) != sb_elim_pred.end()) |
345 |
|
{ |
346 |
6 |
Trace("sygus-sb-tp") << "Eliminate traversal predicates: start " |
347 |
3 |
<< sslem << std::endl; |
348 |
3 |
sslem = eliminateTraversalPredicates(sslem); |
349 |
6 |
Trace("sygus-sb-tp") << "Eliminate traversal predicates: finish " |
350 |
3 |
<< sslem << std::endl; |
351 |
|
} |
352 |
6731 |
if (!rlv.isNull()) |
353 |
|
{ |
354 |
4063 |
sslem = nm->mkNode(OR, rlv, sslem); |
355 |
|
} |
356 |
6731 |
d_im.lemma(sslem, sbl.second); |
357 |
|
} |
358 |
|
} |
359 |
67485 |
d_simple_proc[exp] = max_depth + 1; |
360 |
|
|
361 |
|
// now activate the children those testers were previously asserted in this |
362 |
|
// context and are awaiting activation, if they exist. |
363 |
67485 |
if( options::sygusSymBreakLazy() ){ |
364 |
67477 |
Trace("sygus-sb-debug") << "Do lazy symmetry breaking...\n"; |
365 |
118391 |
for( unsigned j=0; j<dt[tindex].getNumArgs(); j++ ){ |
366 |
|
Node sel = nm->mkNode( |
367 |
101828 |
APPLY_SELECTOR_TOTAL, dt[tindex].getSelectorInternal(ntn, j), n); |
368 |
50914 |
Trace("sygus-sb-debug2") << " activate child sel : " << sel << std::endl; |
369 |
50914 |
Assert(d_active_terms.find(sel) == d_active_terms.end()); |
370 |
50914 |
IntMap::const_iterator itt = d_testers.find( sel ); |
371 |
50914 |
if( itt != d_testers.end() ){ |
372 |
6447 |
Assert(d_testers_exp.find(sel) != d_testers_exp.end()); |
373 |
6447 |
assertTesterInternal((*itt).second, sel, d_testers_exp[sel]); |
374 |
|
} |
375 |
|
} |
376 |
67477 |
Trace("sygus-sb-debug") << "...finished" << std::endl; |
377 |
|
} |
378 |
|
} |
379 |
|
|
380 |
75875 |
Node SygusExtension::getRelevancyCondition( Node n ) { |
381 |
75875 |
if (!options::sygusSymBreakRlv()) |
382 |
|
{ |
383 |
6 |
return Node::null(); |
384 |
|
} |
385 |
75869 |
std::map< Node, Node >::iterator itr = d_rlv_cond.find( n ); |
386 |
75869 |
if( itr==d_rlv_cond.end() ){ |
387 |
2676 |
Node cond; |
388 |
1338 |
if (n.getKind() == APPLY_SELECTOR_TOTAL) |
389 |
|
{ |
390 |
1788 |
TypeNode ntn = n[0].getType(); |
391 |
894 |
const DType& dt = ntn.getDType(); |
392 |
1788 |
Node sel = n.getOperator(); |
393 |
894 |
if( options::dtSharedSelectors() ){ |
394 |
1312 |
std::vector< Node > disj; |
395 |
656 |
bool excl = false; |
396 |
3805 |
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ |
397 |
3149 |
int sindexi = dt[i].getSelectorIndexInternal(sel); |
398 |
3149 |
if (sindexi != -1) |
399 |
|
{ |
400 |
1342 |
disj.push_back(utils::mkTester(n[0], i, dt).negate()); |
401 |
|
} |
402 |
|
else |
403 |
|
{ |
404 |
1807 |
excl = true; |
405 |
|
} |
406 |
|
} |
407 |
656 |
Assert(!disj.empty()); |
408 |
656 |
if( excl ){ |
409 |
509 |
cond = disj.size() == 1 ? disj[0] : NodeManager::currentNM()->mkNode( |
410 |
|
kind::AND, disj); |
411 |
|
} |
412 |
|
}else{ |
413 |
238 |
int sindex = utils::cindexOf(sel); |
414 |
238 |
Assert(sindex != -1); |
415 |
238 |
cond = utils::mkTester(n[0], sindex, dt).negate(); |
416 |
|
} |
417 |
1788 |
Node c1 = getRelevancyCondition( n[0] ); |
418 |
894 |
if( cond.isNull() ){ |
419 |
147 |
cond = c1; |
420 |
747 |
}else if( !c1.isNull() ){ |
421 |
428 |
cond = NodeManager::currentNM()->mkNode(kind::OR, cond, c1); |
422 |
|
} |
423 |
|
} |
424 |
1338 |
Trace("sygus-sb-debug2") << "Relevancy condition for " << n << " is " << cond << std::endl; |
425 |
1338 |
d_rlv_cond[n] = cond; |
426 |
1338 |
return cond; |
427 |
|
}else{ |
428 |
74531 |
return itr->second; |
429 |
|
} |
430 |
|
} |
431 |
|
|
432 |
23 |
Node SygusExtension::getTraversalPredicate(TypeNode tn, Node n, bool isPre) |
433 |
|
{ |
434 |
23 |
unsigned index = isPre ? 0 : 1; |
435 |
23 |
std::map<Node, Node>::iterator itt = d_traversal_pred[index][tn].find(n); |
436 |
23 |
if (itt != d_traversal_pred[index][tn].end()) |
437 |
|
{ |
438 |
19 |
return itt->second; |
439 |
|
} |
440 |
4 |
NodeManager* nm = NodeManager::currentNM(); |
441 |
4 |
SkolemManager* sm = nm->getSkolemManager(); |
442 |
8 |
std::vector<TypeNode> types; |
443 |
4 |
types.push_back(tn); |
444 |
8 |
TypeNode ptn = nm->mkPredicateType(types); |
445 |
8 |
Node pred = sm->mkDummySkolem(isPre ? "pre" : "post", ptn); |
446 |
4 |
d_traversal_pred[index][tn][n] = pred; |
447 |
4 |
return pred; |
448 |
|
} |
449 |
|
|
450 |
4 |
Node SygusExtension::eliminateTraversalPredicates(Node n) |
451 |
|
{ |
452 |
4 |
NodeManager* nm = NodeManager::currentNM(); |
453 |
4 |
SkolemManager* sm = nm->getSkolemManager(); |
454 |
8 |
std::unordered_map<TNode, Node> visited; |
455 |
4 |
std::unordered_map<TNode, Node>::iterator it; |
456 |
4 |
std::map<Node, Node>::iterator ittb; |
457 |
8 |
std::vector<TNode> visit; |
458 |
8 |
TNode cur; |
459 |
4 |
visit.push_back(n); |
460 |
110 |
do |
461 |
|
{ |
462 |
114 |
cur = visit.back(); |
463 |
114 |
visit.pop_back(); |
464 |
114 |
it = visited.find(cur); |
465 |
|
|
466 |
114 |
if (it == visited.end()) |
467 |
|
{ |
468 |
64 |
if (cur.getKind() == APPLY_UF) |
469 |
|
{ |
470 |
20 |
Assert(cur.getType().isBoolean()); |
471 |
20 |
Assert(cur.getNumChildren() == 1 |
472 |
|
&& (cur[0].isVar() || cur[0].getKind() == APPLY_SELECTOR_TOTAL)); |
473 |
20 |
ittb = d_traversal_bool.find(cur); |
474 |
40 |
Node ret; |
475 |
20 |
if (ittb == d_traversal_bool.end()) |
476 |
|
{ |
477 |
24 |
std::stringstream ss; |
478 |
12 |
ss << "v_" << cur; |
479 |
12 |
ret = sm->mkDummySkolem(ss.str(), cur.getType()); |
480 |
12 |
d_traversal_bool[cur] = ret; |
481 |
|
} |
482 |
|
else |
483 |
|
{ |
484 |
8 |
ret = ittb->second; |
485 |
|
} |
486 |
20 |
visited[cur] = ret; |
487 |
|
} |
488 |
|
else |
489 |
|
{ |
490 |
44 |
visited[cur] = Node::null(); |
491 |
44 |
visit.push_back(cur); |
492 |
110 |
for (const Node& cn : cur) |
493 |
|
{ |
494 |
66 |
visit.push_back(cn); |
495 |
|
} |
496 |
|
} |
497 |
|
} |
498 |
50 |
else if (it->second.isNull()) |
499 |
|
{ |
500 |
88 |
Node ret = cur; |
501 |
44 |
bool childChanged = false; |
502 |
88 |
std::vector<Node> children; |
503 |
44 |
if (cur.getMetaKind() == metakind::PARAMETERIZED) |
504 |
|
{ |
505 |
5 |
children.push_back(cur.getOperator()); |
506 |
|
} |
507 |
110 |
for (const Node& cn : cur) |
508 |
|
{ |
509 |
66 |
it = visited.find(cn); |
510 |
66 |
Assert(it != visited.end()); |
511 |
66 |
Assert(!it->second.isNull()); |
512 |
66 |
childChanged = childChanged || cn != it->second; |
513 |
66 |
children.push_back(it->second); |
514 |
|
} |
515 |
44 |
if (childChanged) |
516 |
|
{ |
517 |
19 |
ret = nm->mkNode(cur.getKind(), children); |
518 |
|
} |
519 |
44 |
visited[cur] = ret; |
520 |
|
} |
521 |
114 |
} while (!visit.empty()); |
522 |
4 |
Assert(visited.find(n) != visited.end()); |
523 |
4 |
Assert(!visited.find(n)->second.isNull()); |
524 |
8 |
return visited[n]; |
525 |
|
} |
526 |
|
|
527 |
9272 |
Node SygusExtension::getSimpleSymBreakPred(Node e, |
528 |
|
TypeNode tn, |
529 |
|
int tindex, |
530 |
|
unsigned depth, |
531 |
|
bool usingSymCons, |
532 |
|
bool isVarAgnostic) |
533 |
|
{ |
534 |
|
// Compute the tuple of expressions we hash the predicate for. |
535 |
|
|
536 |
|
// The hash value in d_simple_sb_pred for the given options |
537 |
9272 |
unsigned optHashVal = usingSymCons ? 1 : 0; |
538 |
9272 |
if (isVarAgnostic && depth == 0) |
539 |
|
{ |
540 |
|
// variable agnostic symmetry breaking only applies at depth 0 |
541 |
3 |
optHashVal = optHashVal + 2; |
542 |
|
} |
543 |
|
else |
544 |
|
{ |
545 |
|
// enumerator is only specific to variable agnostic symmetry breaking |
546 |
9269 |
e = Node::null(); |
547 |
|
} |
548 |
|
std::map<unsigned, Node>& ssbCache = |
549 |
9272 |
d_simple_sb_pred[e][tn][tindex][optHashVal]; |
550 |
9272 |
std::map<unsigned, Node>::iterator it = ssbCache.find(depth); |
551 |
9272 |
if (it != ssbCache.end()) |
552 |
|
{ |
553 |
6356 |
return it->second; |
554 |
|
} |
555 |
|
// this function is only called on sygus datatype types |
556 |
2916 |
Assert(tn.isDatatype()); |
557 |
2916 |
NodeManager* nm = NodeManager::currentNM(); |
558 |
5832 |
Node n = getFreeVar(tn); |
559 |
2916 |
const DType& dt = tn.getDType(); |
560 |
2916 |
Assert(dt.isSygus()); |
561 |
2916 |
Assert(tindex >= 0 && tindex < static_cast<int>(dt.getNumConstructors())); |
562 |
|
|
563 |
5832 |
Trace("sygus-sb-simple-debug") |
564 |
5832 |
<< "Simple symmetry breaking for " << dt.getName() << ", constructor " |
565 |
2916 |
<< dt[tindex].getName() << ", at depth " << depth << std::endl; |
566 |
|
|
567 |
2916 |
quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn); |
568 |
|
// get the sygus operator |
569 |
5832 |
Node sop = dt[tindex].getSygusOp(); |
570 |
|
// get the kind of the constructor operator |
571 |
2916 |
Kind nk = ti.getConsNumKind(tindex); |
572 |
|
// is this the any-constant constructor? |
573 |
2916 |
bool isAnyConstant = sop.getAttribute(SygusAnyConstAttribute()); |
574 |
|
|
575 |
|
// conjunctive conclusion of lemma |
576 |
5832 |
std::vector<Node> sbp_conj; |
577 |
|
|
578 |
|
// the number of (sygus) arguments |
579 |
|
// Notice if this is an any-constant constructor, its child is not a |
580 |
|
// sygus child, hence we set to 0 here. |
581 |
2916 |
unsigned dt_index_nargs = isAnyConstant ? 0 : dt[tindex].getNumArgs(); |
582 |
|
|
583 |
|
// builtin type |
584 |
5832 |
TypeNode tnb = dt.getSygusType(); |
585 |
|
// get children |
586 |
5832 |
std::vector<Node> children; |
587 |
5833 |
for (unsigned j = 0; j < dt_index_nargs; j++) |
588 |
|
{ |
589 |
|
Node sel = nm->mkNode( |
590 |
5834 |
APPLY_SELECTOR_TOTAL, dt[tindex].getSelectorInternal(tn, j), n); |
591 |
2917 |
Assert(sel.getType().isDatatype()); |
592 |
2917 |
children.push_back(sel); |
593 |
|
} |
594 |
|
|
595 |
2916 |
if (depth == 0) |
596 |
|
{ |
597 |
1798 |
Trace("sygus-sb-simple-debug") << " Size..." << std::endl; |
598 |
|
// fairness |
599 |
3596 |
if (options::sygusFair() == options::SygusFairMode::DT_SIZE |
600 |
1798 |
&& !isAnyConstant) |
601 |
|
{ |
602 |
3546 |
Node szl = nm->mkNode(DT_SIZE, n); |
603 |
3546 |
Node szr = nm->mkNode(DT_SIZE, utils::getInstCons(n, dt, tindex)); |
604 |
1773 |
szr = Rewriter::rewrite(szr); |
605 |
1773 |
sbp_conj.push_back(szl.eqNode(szr)); |
606 |
|
} |
607 |
1798 |
if (isVarAgnostic) |
608 |
|
{ |
609 |
|
// Enforce symmetry breaking lemma template for each x_i: |
610 |
|
// template z. |
611 |
|
// is-x_i( z ) => pre_{x_{i-1}}( z ) |
612 |
|
// for args a = 1...n |
613 |
|
// // pre-definition |
614 |
|
// pre_{x_i}( z.a ) = a=0 ? pre_{x_i}( z ) : post_{x_i}( z.{a-1} ) |
615 |
|
// post_{x_i}( z ) = post_{x_i}( z.n ) OR is-x_i( z ) |
616 |
|
|
617 |
|
// Notice that we are constructing a symmetry breaking template |
618 |
|
// under the condition that is-C( z ) holds in this method, where C |
619 |
|
// is the tindex^{th} constructor of dt. Thus, is-x_i( z ) is either |
620 |
|
// true or false below. |
621 |
|
|
622 |
6 |
Node svl = dt.getSygusVarList(); |
623 |
|
// for each variable |
624 |
3 |
Assert(!e.isNull()); |
625 |
6 |
TypeNode etn = e.getType(); |
626 |
|
// for each variable in the sygus type |
627 |
9 |
for (const Node& var : svl) |
628 |
|
{ |
629 |
6 |
quantifiers::SygusTypeInfo& eti = d_tds->getTypeInfo(etn); |
630 |
6 |
unsigned sc = eti.getSubclassForVar(var); |
631 |
6 |
if (eti.getNumSubclassVars(sc) == 1) |
632 |
|
{ |
633 |
|
// unique variable in singleton subclass, skip |
634 |
|
continue; |
635 |
|
} |
636 |
|
// Compute the "predecessor" variable in the subclass of var. |
637 |
12 |
Node predVar; |
638 |
6 |
unsigned scindex = 0; |
639 |
6 |
if (eti.getIndexInSubclassForVar(var, scindex)) |
640 |
|
{ |
641 |
6 |
if (scindex > 0) |
642 |
|
{ |
643 |
3 |
predVar = eti.getVarSubclassIndex(sc, scindex - 1); |
644 |
|
} |
645 |
|
} |
646 |
12 |
Node preParentOp = getTraversalPredicate(tn, var, true); |
647 |
12 |
Node preParent = nm->mkNode(APPLY_UF, preParentOp, n); |
648 |
12 |
Node prev = preParent; |
649 |
|
// for each child |
650 |
10 |
for (const Node& child : children) |
651 |
|
{ |
652 |
8 |
TypeNode ctn = child.getType(); |
653 |
|
// my pre is equal to the previous |
654 |
8 |
Node preCurrOp = getTraversalPredicate(ctn, var, true); |
655 |
8 |
Node preCurr = nm->mkNode(APPLY_UF, preCurrOp, child); |
656 |
|
// definition of pre, for each argument |
657 |
4 |
sbp_conj.push_back(preCurr.eqNode(prev)); |
658 |
8 |
Node postCurrOp = getTraversalPredicate(ctn, var, false); |
659 |
4 |
prev = nm->mkNode(APPLY_UF, postCurrOp, child); |
660 |
|
} |
661 |
12 |
Node postParent = getTraversalPredicate(tn, var, false); |
662 |
12 |
Node finish = nm->mkNode(APPLY_UF, postParent, n); |
663 |
|
// check if we are constructing the symmetry breaking predicate for the |
664 |
|
// variable in question. If so, is-{x_i}( z ) is true. |
665 |
6 |
int varCn = ti.getOpConsNum(var); |
666 |
6 |
if (varCn == static_cast<int>(tindex)) |
667 |
|
{ |
668 |
|
// the post value is true |
669 |
2 |
prev = d_true; |
670 |
|
// requirement : If I am the variable, I must have seen |
671 |
|
// the variable before this one in its type class. |
672 |
2 |
if (!predVar.isNull()) |
673 |
|
{ |
674 |
2 |
Node preParentPredVarOp = getTraversalPredicate(tn, predVar, true); |
675 |
2 |
Node preParentPredVar = nm->mkNode(APPLY_UF, preParentPredVarOp, n); |
676 |
1 |
sbp_conj.push_back(preParentPredVar); |
677 |
|
} |
678 |
|
} |
679 |
|
// definition of post |
680 |
6 |
sbp_conj.push_back(finish.eqNode(prev)); |
681 |
|
} |
682 |
|
} |
683 |
|
} |
684 |
|
|
685 |
|
// if we are the "any constant" constructor, we do no symmetry breaking |
686 |
|
// only do simple symmetry breaking up to depth 2 |
687 |
2916 |
bool doSymBreak = options::sygusSymBreak(); |
688 |
2916 |
if (isAnyConstant || depth > 2) |
689 |
|
{ |
690 |
257 |
doSymBreak = false; |
691 |
|
} |
692 |
|
// symmetry breaking |
693 |
2916 |
if (doSymBreak) |
694 |
|
{ |
695 |
|
// direct solving for children |
696 |
|
// for instance, we may want to insist that the LHS of MINUS is 0 |
697 |
2622 |
Trace("sygus-sb-simple-debug") << " Solve children..." << std::endl; |
698 |
5244 |
std::map<unsigned, unsigned> children_solved; |
699 |
5217 |
for (unsigned j = 0; j < dt_index_nargs; j++) |
700 |
|
{ |
701 |
2595 |
int i = d_ssb.solveForArgument(tn, tindex, j); |
702 |
2595 |
if (i >= 0) |
703 |
|
{ |
704 |
|
children_solved[j] = i; |
705 |
|
TypeNode ctn = children[j].getType(); |
706 |
|
const DType& cdt = ctn.getDType(); |
707 |
|
Assert(i < static_cast<int>(cdt.getNumConstructors())); |
708 |
|
sbp_conj.push_back(utils::mkTester(children[j], i, cdt)); |
709 |
|
} |
710 |
|
} |
711 |
|
|
712 |
|
// depth 1 symmetry breaking : talks about direct children |
713 |
2622 |
if (depth == 1) |
714 |
|
{ |
715 |
618 |
if (nk != UNDEFINED_KIND) |
716 |
|
{ |
717 |
720 |
Trace("sygus-sb-simple-debug") |
718 |
360 |
<< " Equality reasoning about children..." << std::endl; |
719 |
|
// commutative operators |
720 |
360 |
if (quantifiers::TermUtil::isComm(nk)) |
721 |
|
{ |
722 |
358 |
if (children.size() == 2 |
723 |
358 |
&& children[0].getType() == children[1].getType()) |
724 |
|
{ |
725 |
346 |
Node order_pred = getTermOrderPredicate(children[0], children[1]); |
726 |
173 |
sbp_conj.push_back(order_pred); |
727 |
|
} |
728 |
|
} |
729 |
|
// operators whose arguments are non-additive (e.g. should be different) |
730 |
720 |
std::vector<unsigned> deq_child[2]; |
731 |
360 |
if (children.size() == 2 && children[0].getType() == tn) |
732 |
|
{ |
733 |
153 |
bool argDeq = false; |
734 |
153 |
if (quantifiers::TermUtil::isNonAdditive(nk)) |
735 |
|
{ |
736 |
50 |
argDeq = true; |
737 |
|
} |
738 |
|
else |
739 |
|
{ |
740 |
|
// other cases of rewriting x k x -> x' |
741 |
206 |
Node req_const; |
742 |
103 |
if (nk == GT || nk == LT || nk == XOR || nk == MINUS |
743 |
72 |
|| nk == BITVECTOR_SUB || nk == BITVECTOR_XOR |
744 |
71 |
|| nk == BITVECTOR_UREM) |
745 |
|
{ |
746 |
|
// must have the zero element |
747 |
33 |
req_const = quantifiers::TermUtil::mkTypeValue(tnb, 0); |
748 |
|
} |
749 |
70 |
else if (nk == EQUAL || nk == LEQ || nk == GEQ |
750 |
70 |
|| nk == BITVECTOR_XNOR) |
751 |
|
{ |
752 |
|
req_const = quantifiers::TermUtil::mkTypeMaxValue(tnb); |
753 |
|
} |
754 |
|
// cannot do division since we have to consider when both are zero |
755 |
103 |
if (!req_const.isNull()) |
756 |
|
{ |
757 |
33 |
if (ti.hasConst(req_const)) |
758 |
|
{ |
759 |
27 |
argDeq = true; |
760 |
|
} |
761 |
|
} |
762 |
|
} |
763 |
153 |
if (argDeq) |
764 |
|
{ |
765 |
77 |
deq_child[0].push_back(0); |
766 |
77 |
deq_child[1].push_back(1); |
767 |
|
} |
768 |
|
} |
769 |
360 |
if (nk == ITE || nk == STRING_REPLACE || nk == STRING_REPLACE_ALL) |
770 |
|
{ |
771 |
37 |
deq_child[0].push_back(1); |
772 |
37 |
deq_child[1].push_back(2); |
773 |
|
} |
774 |
360 |
if (nk == STRING_REPLACE || nk == STRING_REPLACE_ALL) |
775 |
|
{ |
776 |
|
deq_child[0].push_back(0); |
777 |
|
deq_child[1].push_back(1); |
778 |
|
} |
779 |
|
// this code adds simple symmetry breaking predicates of the form |
780 |
|
// d.i != d.j, for example if we are considering an ITE constructor, |
781 |
|
// we enforce that d.1 != d.2 since otherwise the ITE can be |
782 |
|
// simplified. |
783 |
474 |
for (unsigned i = 0, size = deq_child[0].size(); i < size; i++) |
784 |
|
{ |
785 |
114 |
unsigned c1 = deq_child[0][i]; |
786 |
114 |
unsigned c2 = deq_child[1][i]; |
787 |
228 |
TypeNode tnc = children[c1].getType(); |
788 |
|
// we may only apply this symmetry breaking scheme (which introduces |
789 |
|
// disequalities) if the types are infinite. |
790 |
114 |
if (tnc == children[c2].getType() && !d_state.isFiniteType(tnc)) |
791 |
|
{ |
792 |
228 |
Node sym_lem_deq = children[c1].eqNode(children[c2]).negate(); |
793 |
|
// notice that this symmetry breaking still allows for |
794 |
|
// ite( C, any_constant(x), any_constant(y) ) |
795 |
|
// since any_constant takes a builtin argument. |
796 |
114 |
sbp_conj.push_back(sym_lem_deq); |
797 |
|
} |
798 |
|
} |
799 |
|
|
800 |
720 |
Trace("sygus-sb-simple-debug") << " Redundant operators..." |
801 |
360 |
<< std::endl; |
802 |
|
// singular arguments (e.g. 0 for mult) |
803 |
|
// redundant arguments (e.g. 0 for plus, 1 for mult) |
804 |
|
// right-associativity |
805 |
|
// simple rewrites |
806 |
|
// explanation of why not all children of this are constant |
807 |
720 |
std::vector<Node> exp_not_all_const; |
808 |
|
// is the above explanation valid? This is set to false if |
809 |
|
// one child does not have a constant, hence making the explanation |
810 |
|
// false. |
811 |
360 |
bool exp_not_all_const_valid = dt_index_nargs > 0; |
812 |
|
// does the parent have an any constant constructor? |
813 |
|
bool usingAnyConstCons = |
814 |
360 |
usingSymCons && (ti.getAnyConstantConsNum() != -1); |
815 |
1084 |
for (unsigned j = 0; j < dt_index_nargs; j++) |
816 |
|
{ |
817 |
1448 |
Node nc = children[j]; |
818 |
|
// if not already solved |
819 |
724 |
if (children_solved.find(j) != children_solved.end()) |
820 |
|
{ |
821 |
|
continue; |
822 |
|
} |
823 |
1448 |
TypeNode tnc = nc.getType(); |
824 |
724 |
quantifiers::SygusTypeInfo& cti = d_tds->getTypeInfo(tnc); |
825 |
724 |
int anyc_cons_num = cti.getAnyConstantConsNum(); |
826 |
724 |
const DType& cdt = tnc.getDType(); |
827 |
1448 |
std::vector<Node> exp_const; |
828 |
5308 |
for (unsigned k = 0, ncons = cdt.getNumConstructors(); k < ncons; k++) |
829 |
|
{ |
830 |
4584 |
Kind nck = cti.getConsNumKind(k); |
831 |
4584 |
bool red = false; |
832 |
9168 |
Node tester = utils::mkTester(nc, k, cdt); |
833 |
|
// check if the argument is redundant |
834 |
4584 |
if (static_cast<int>(k) == anyc_cons_num) |
835 |
|
{ |
836 |
48 |
exp_const.push_back(tester); |
837 |
|
} |
838 |
4536 |
else if (nck != UNDEFINED_KIND) |
839 |
|
{ |
840 |
4968 |
Trace("sygus-sb-simple-debug") << " argument " << j << " " << k |
841 |
2484 |
<< " is : " << nck << std::endl; |
842 |
2484 |
red = !d_ssb.considerArgKind(tnc, tn, nck, nk, j); |
843 |
|
} |
844 |
|
else |
845 |
|
{ |
846 |
4104 |
Node cc = cti.getConsNumConst(k); |
847 |
2052 |
if (!cc.isNull()) |
848 |
|
{ |
849 |
2366 |
Trace("sygus-sb-simple-debug") |
850 |
1183 |
<< " argument " << j << " " << k << " is constant : " << cc |
851 |
1183 |
<< std::endl; |
852 |
1183 |
red = !d_ssb.considerConst(tnc, tn, cc, nk, j); |
853 |
1183 |
if (usingAnyConstCons) |
854 |
|
{ |
855 |
|
// we only consider concrete constant constructors |
856 |
|
// of children if we have the "any constant" constructor |
857 |
|
// otherwise, we would disallow solutions for grammars |
858 |
|
// like the following: |
859 |
|
// A -> B+B |
860 |
|
// B -> 4 | 8 | 100 |
861 |
|
// where A allows all constants but is not using the |
862 |
|
// any constant constructor. |
863 |
|
exp_const.push_back(tester); |
864 |
|
} |
865 |
|
} |
866 |
|
else |
867 |
|
{ |
868 |
|
// defined function? |
869 |
|
} |
870 |
|
} |
871 |
4584 |
if (red) |
872 |
|
{ |
873 |
1078 |
Trace("sygus-sb-simple-debug") << " ...redundant." << std::endl; |
874 |
1078 |
sbp_conj.push_back(tester.negate()); |
875 |
|
} |
876 |
|
} |
877 |
724 |
if (exp_const.empty()) |
878 |
|
{ |
879 |
676 |
exp_not_all_const_valid = false; |
880 |
|
} |
881 |
|
else |
882 |
|
{ |
883 |
96 |
Node ecn = exp_const.size() == 1 ? exp_const[0] |
884 |
144 |
: nm->mkNode(OR, exp_const); |
885 |
48 |
exp_not_all_const.push_back(ecn.negate()); |
886 |
|
} |
887 |
|
} |
888 |
|
// explicitly handle constants and "any constant" constructors |
889 |
|
// if this type admits any constant, then at least one of my |
890 |
|
// children must not be a constant or the "any constant" constructor |
891 |
360 |
if (dt.getSygusAllowConst() && exp_not_all_const_valid) |
892 |
|
{ |
893 |
18 |
Assert(!exp_not_all_const.empty()); |
894 |
18 |
Node expaan = exp_not_all_const.size() == 1 |
895 |
1 |
? exp_not_all_const[0] |
896 |
37 |
: nm->mkNode(OR, exp_not_all_const); |
897 |
36 |
Trace("sygus-sb-simple-debug") |
898 |
18 |
<< "Ensure not all constant: " << expaan << std::endl; |
899 |
18 |
sbp_conj.push_back(expaan); |
900 |
|
} |
901 |
|
} |
902 |
|
else |
903 |
|
{ |
904 |
|
// defined function? |
905 |
|
} |
906 |
|
} |
907 |
2004 |
else if (depth == 2) |
908 |
|
{ |
909 |
|
// commutative operators |
910 |
612 |
if (quantifiers::TermUtil::isComm(nk) && children.size() == 2 |
911 |
612 |
&& children[0].getType() == tn && children[1].getType() == tn) |
912 |
|
{ |
913 |
|
// chainable |
914 |
|
Node child11 = nm->mkNode(APPLY_SELECTOR_TOTAL, |
915 |
92 |
dt[tindex].getSelectorInternal(tn, 1), |
916 |
184 |
children[0]); |
917 |
46 |
Assert(child11.getType() == children[1].getType()); |
918 |
|
Node order_pred_trans = |
919 |
|
nm->mkNode(OR, |
920 |
92 |
utils::mkTester(children[0], tindex, dt).negate(), |
921 |
184 |
getTermOrderPredicate(child11, children[1])); |
922 |
46 |
sbp_conj.push_back(order_pred_trans); |
923 |
|
} |
924 |
|
} |
925 |
|
} |
926 |
|
|
927 |
5832 |
Node sb_pred; |
928 |
2916 |
if (!sbp_conj.empty()) |
929 |
|
{ |
930 |
2135 |
sb_pred = |
931 |
4270 |
sbp_conj.size() == 1 ? sbp_conj[0] : nm->mkNode(kind::AND, sbp_conj); |
932 |
4270 |
Trace("sygus-sb-simple") |
933 |
2135 |
<< "Simple predicate for " << tn << " index " << tindex << " (" << nk |
934 |
2135 |
<< ") at depth " << depth << " : " << std::endl; |
935 |
2135 |
Trace("sygus-sb-simple") << " " << sb_pred << std::endl; |
936 |
2135 |
sb_pred = nm->mkNode(OR, utils::mkTester(n, tindex, dt).negate(), sb_pred); |
937 |
|
} |
938 |
2916 |
d_simple_sb_pred[e][tn][tindex][optHashVal][depth] = sb_pred; |
939 |
2916 |
return sb_pred; |
940 |
|
} |
941 |
|
|
942 |
59440 |
TNode SygusExtension::getFreeVar( TypeNode tn ) { |
943 |
59440 |
return d_tds->getFreeVar(tn, 0); |
944 |
|
} |
945 |
|
|
946 |
1777 |
void SygusExtension::registerSearchTerm(TypeNode tn, |
947 |
|
unsigned d, |
948 |
|
Node n, |
949 |
|
bool topLevel) |
950 |
|
{ |
951 |
|
//register this term |
952 |
1777 |
std::unordered_map<Node, Node>::iterator ita = d_term_to_anchor.find(n); |
953 |
1777 |
Assert(ita != d_term_to_anchor.end()); |
954 |
3554 |
Node a = ita->second; |
955 |
1777 |
Assert(!a.isNull()); |
956 |
1777 |
SearchCache& sca = d_cache[a]; |
957 |
5331 |
if (std::find( |
958 |
1777 |
sca.d_search_terms[tn][d].begin(), sca.d_search_terms[tn][d].end(), n) |
959 |
5331 |
== sca.d_search_terms[tn][d].end()) |
960 |
|
{ |
961 |
1777 |
Trace("sygus-sb-debug") << " register search term : " << n << " at depth " << d << ", type=" << tn << ", tl=" << topLevel << std::endl; |
962 |
1777 |
sca.d_search_terms[tn][d].push_back(n); |
963 |
1777 |
if( !options::sygusSymBreakLazy() ){ |
964 |
2 |
addSymBreakLemmasFor(tn, n, d); |
965 |
|
} |
966 |
|
} |
967 |
1777 |
} |
968 |
|
|
969 |
28433 |
Node SygusExtension::registerSearchValue(Node a, |
970 |
|
Node n, |
971 |
|
Node nv, |
972 |
|
unsigned d, |
973 |
|
bool isVarAgnostic, |
974 |
|
bool doSym) |
975 |
|
{ |
976 |
28433 |
Assert(n.getType().isComparableTo(nv.getType())); |
977 |
56866 |
TypeNode tn = n.getType(); |
978 |
28433 |
if (!tn.isDatatype()) |
979 |
|
{ |
980 |
|
// don't register non-datatype terms, instead we return the |
981 |
|
// selector chain n. |
982 |
469 |
return n; |
983 |
|
} |
984 |
27964 |
const DType& dt = tn.getDType(); |
985 |
27964 |
if (!dt.isSygus()) |
986 |
|
{ |
987 |
|
// don't register non-sygus-datatype terms |
988 |
|
return n; |
989 |
|
} |
990 |
27964 |
Assert(nv.getKind() == APPLY_CONSTRUCTOR); |
991 |
27964 |
NodeManager* nm = NodeManager::currentNM(); |
992 |
|
// we call the body of this function in a bottom-up fashion |
993 |
|
// this ensures that the "abstraction" of the model value is available |
994 |
27964 |
if( nv.getNumChildren()>0 ){ |
995 |
10266 |
unsigned cindex = utils::indexOf(nv.getOperator()); |
996 |
20224 |
std::vector<Node> rcons_children; |
997 |
10266 |
rcons_children.push_back(nv.getOperator()); |
998 |
10266 |
bool childrenChanged = false; |
999 |
29729 |
for (unsigned i = 0, nchild = nv.getNumChildren(); i < nchild; i++) |
1000 |
|
{ |
1001 |
|
Node sel = nm->mkNode( |
1002 |
39234 |
APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), n); |
1003 |
|
Node nvc = registerSearchValue(a, |
1004 |
|
sel, |
1005 |
|
nv[i], |
1006 |
|
d + 1, |
1007 |
|
isVarAgnostic, |
1008 |
39234 |
doSym && (!isVarAgnostic || i == 0)); |
1009 |
19771 |
if (nvc.isNull()) |
1010 |
|
{ |
1011 |
308 |
return Node::null(); |
1012 |
|
} |
1013 |
19463 |
rcons_children.push_back(nvc); |
1014 |
19463 |
childrenChanged = childrenChanged || nvc != nv[i]; |
1015 |
|
} |
1016 |
|
// reconstruct the value, which may be a skeleton |
1017 |
9958 |
if (childrenChanged) |
1018 |
|
{ |
1019 |
843 |
nv = nm->mkNode(APPLY_CONSTRUCTOR, rcons_children); |
1020 |
|
} |
1021 |
|
} |
1022 |
27656 |
if (!doSym) |
1023 |
|
{ |
1024 |
|
return nv; |
1025 |
|
} |
1026 |
27656 |
Trace("sygus-sb-debug2") << "Registering search value " << n << " -> " << nv << std::endl; |
1027 |
55312 |
std::map<TypeNode, int> var_count; |
1028 |
55312 |
Node cnv = d_tds->canonizeBuiltin(nv, var_count); |
1029 |
27656 |
Trace("sygus-sb-debug") << " ...canonized value is " << cnv << std::endl; |
1030 |
27656 |
SearchCache& sca = d_cache[a]; |
1031 |
|
// must do this for all nodes, regardless of top-level |
1032 |
27656 |
if (sca.d_search_val_proc.find(cnv) == sca.d_search_val_proc.end()) |
1033 |
|
{ |
1034 |
4971 |
sca.d_search_val_proc.insert(cnv); |
1035 |
|
// get the root (for PBE symmetry breaking) |
1036 |
4971 |
Assert(d_anchor_to_conj.find(a) != d_anchor_to_conj.end()); |
1037 |
4971 |
quantifiers::SynthConjecture* aconj = d_anchor_to_conj[a]; |
1038 |
9942 |
Trace("sygus-sb-debug") << " ...register search value " << cnv |
1039 |
4971 |
<< ", type=" << tn << std::endl; |
1040 |
8299 |
Node bv = d_tds->sygusToBuiltin(cnv, tn); |
1041 |
4971 |
Trace("sygus-sb-debug") << " ......builtin is " << bv << std::endl; |
1042 |
8299 |
Node bvr = extendedRewrite(bv); |
1043 |
4971 |
Trace("sygus-sb-debug") << " ......search value rewrites to " << bvr << std::endl; |
1044 |
4971 |
Trace("dt-sygus") << " * DT builtin : " << n << " -> " << bvr << std::endl; |
1045 |
4971 |
unsigned sz = utils::getSygusTermSize(nv); |
1046 |
4971 |
if( d_tds->involvesDivByZero( bvr ) ){ |
1047 |
2 |
quantifiers::DivByZeroSygusInvarianceTest dbzet; |
1048 |
2 |
Trace("sygus-sb-mexp-debug") << "Minimize explanation for div-by-zero in " |
1049 |
1 |
<< bv << std::endl; |
1050 |
1 |
registerSymBreakLemmaForValue(a, nv, dbzet, Node::null(), var_count); |
1051 |
1 |
return Node::null(); |
1052 |
|
}else{ |
1053 |
4970 |
std::unordered_map<Node, Node>& scasv = sca.d_search_val[tn]; |
1054 |
4970 |
std::unordered_map<Node, unsigned>& scasvs = sca.d_search_val_sz[tn]; |
1055 |
4970 |
std::unordered_map<Node, Node>::iterator itsv = scasv.find(bvr); |
1056 |
8298 |
Node bad_val_bvr; |
1057 |
4970 |
bool by_examples = false; |
1058 |
4970 |
if (itsv == scasv.end()) |
1059 |
|
{ |
1060 |
|
// Is it equivalent under examples? |
1061 |
6676 |
Node bvr_equiv; |
1062 |
3338 |
if (aconj != nullptr && options::sygusSymBreakPbe()) |
1063 |
|
{ |
1064 |
|
// If the enumerator has examples, see if it is equivalent up to its |
1065 |
|
// examples with a previous term. |
1066 |
3041 |
quantifiers::ExampleEvalCache* eec = aconj->getExampleEvalCache(a); |
1067 |
3041 |
if (eec != nullptr) |
1068 |
|
{ |
1069 |
439 |
bvr_equiv = eec->addSearchVal(tn, bvr); |
1070 |
|
} |
1071 |
|
} |
1072 |
3338 |
if( !bvr_equiv.isNull() ){ |
1073 |
439 |
if( bvr_equiv!=bvr ){ |
1074 |
15 |
Trace("sygus-sb-debug") << "......adding search val for " << bvr << " returned " << bvr_equiv << std::endl; |
1075 |
15 |
Assert(scasv.find(bvr_equiv) != scasv.end()); |
1076 |
30 |
Trace("sygus-sb-debug") |
1077 |
15 |
<< "......search value was " << scasv[bvr_equiv] << std::endl; |
1078 |
15 |
if( Trace.isOn("sygus-sb-exc") ){ |
1079 |
|
Node prev = d_tds->sygusToBuiltin(scasv[bvr_equiv], tn); |
1080 |
|
Trace("sygus-sb-exc") << " ......programs " << prev << " and " << bv << " are equivalent up to examples." << std::endl; |
1081 |
|
} |
1082 |
15 |
bad_val_bvr = bvr_equiv; |
1083 |
15 |
by_examples = true; |
1084 |
|
} |
1085 |
|
} |
1086 |
|
//store rewritten values, regardless of whether it will be considered |
1087 |
3338 |
scasv[bvr] = nv; |
1088 |
3338 |
scasvs[bvr] = sz; |
1089 |
|
} |
1090 |
|
else |
1091 |
|
{ |
1092 |
1632 |
bad_val_bvr = bvr; |
1093 |
1632 |
if( Trace.isOn("sygus-sb-exc") ){ |
1094 |
|
Node prev_bv = d_tds->sygusToBuiltin( itsv->second, tn ); |
1095 |
|
Trace("sygus-sb-exc") << " ......programs " << prev_bv << " and " << bv << " rewrite to " << bvr << "." << std::endl; |
1096 |
|
} |
1097 |
|
} |
1098 |
|
|
1099 |
4970 |
if (options::sygusRewVerify()) |
1100 |
|
{ |
1101 |
7 |
if (bv != bvr) |
1102 |
|
{ |
1103 |
|
// add to the sampler database object |
1104 |
|
std::map<TypeNode, quantifiers::SygusSampler>::iterator its = |
1105 |
1 |
d_sampler[a].find(tn); |
1106 |
1 |
if (its == d_sampler[a].end()) |
1107 |
|
{ |
1108 |
2 |
d_sampler[a][tn].initializeSygus( |
1109 |
1 |
d_tds, nv, options::sygusSamples(), false); |
1110 |
1 |
its = d_sampler[a].find(tn); |
1111 |
|
} |
1112 |
|
// check equivalent |
1113 |
1 |
its->second.checkEquivalent(bv, bvr, *options().base.out); |
1114 |
|
} |
1115 |
|
} |
1116 |
|
|
1117 |
4970 |
if( !bad_val_bvr.isNull() ){ |
1118 |
1652 |
Node bad_val = nv; |
1119 |
1652 |
Node bad_val_o = scasv[bad_val_bvr]; |
1120 |
1647 |
Assert(scasvs.find(bad_val_bvr) != scasvs.end()); |
1121 |
1647 |
unsigned prev_sz = scasvs[bad_val_bvr]; |
1122 |
1647 |
bool doFlip = (prev_sz > sz); |
1123 |
1647 |
if (doFlip) |
1124 |
|
{ |
1125 |
|
//swap : the excluded value is the previous |
1126 |
5 |
scasvs[bad_val_bvr] = sz; |
1127 |
5 |
bad_val = scasv[bad_val_bvr]; |
1128 |
5 |
bad_val_o = nv; |
1129 |
5 |
if (Trace.isOn("sygus-sb-exc")) |
1130 |
|
{ |
1131 |
|
Trace("sygus-sb-exc") << "Flip : exclude "; |
1132 |
|
quantifiers::TermDbSygus::toStreamSygus("sygus-sb-exc", bad_val); |
1133 |
|
Trace("sygus-sb-exc") << " instead of "; |
1134 |
|
quantifiers::TermDbSygus::toStreamSygus("sygus-sb-exc", bad_val_o); |
1135 |
|
Trace("sygus-sb-exc") << ", since its size is " << sz << " < " |
1136 |
|
<< prev_sz << std::endl; |
1137 |
|
} |
1138 |
5 |
sz = prev_sz; |
1139 |
|
} |
1140 |
1647 |
if( Trace.isOn("sygus-sb-exc") ){ |
1141 |
|
Node bad_val_bv = d_tds->sygusToBuiltin( bad_val, tn ); |
1142 |
|
Trace("sygus-sb-exc") << " ........exclude : " << bad_val_bv; |
1143 |
|
if( by_examples ){ |
1144 |
|
Trace("sygus-sb-exc") << " (by examples)"; |
1145 |
|
} |
1146 |
|
Trace("sygus-sb-exc") << std::endl; |
1147 |
|
} |
1148 |
1647 |
Assert(utils::getSygusTermSize(bad_val) == sz); |
1149 |
|
|
1150 |
|
// generalize the explanation for why the analog of bad_val |
1151 |
|
// is equivalent to bvr |
1152 |
1652 |
quantifiers::EquivSygusInvarianceTest eset; |
1153 |
1647 |
eset.init(d_tds, tn, aconj, a, bvr); |
1154 |
|
|
1155 |
1647 |
Trace("sygus-sb-mexp-debug") << "Minimize explanation for eval[" << d_tds->sygusToBuiltin( bad_val ) << "] = " << bvr << std::endl; |
1156 |
1647 |
registerSymBreakLemmaForValue(a, bad_val, eset, bad_val_o, var_count); |
1157 |
|
|
1158 |
|
// other generalization criteria go here |
1159 |
|
|
1160 |
|
// If the exclusion was flipped, we are excluding a previous value |
1161 |
|
// instead of the current one. Hence, the current value is a legal |
1162 |
|
// value that we will consider. |
1163 |
1647 |
if (!doFlip) |
1164 |
|
{ |
1165 |
1642 |
return Node::null(); |
1166 |
|
} |
1167 |
|
} |
1168 |
|
} |
1169 |
|
} |
1170 |
26013 |
return nv; |
1171 |
|
} |
1172 |
|
|
1173 |
1648 |
void SygusExtension::registerSymBreakLemmaForValue( |
1174 |
|
Node a, |
1175 |
|
Node val, |
1176 |
|
quantifiers::SygusInvarianceTest& et, |
1177 |
|
Node valr, |
1178 |
|
std::map<TypeNode, int>& var_count) |
1179 |
|
{ |
1180 |
3296 |
TypeNode tn = val.getType(); |
1181 |
3296 |
Node x = getFreeVar(tn); |
1182 |
1648 |
unsigned sz = utils::getSygusTermSize(val); |
1183 |
3296 |
std::vector<Node> exp; |
1184 |
1648 |
d_tds->getExplain()->getExplanationFor(x, val, exp, et, valr, var_count, sz); |
1185 |
|
Node lem = |
1186 |
3296 |
exp.size() == 1 ? exp[0] : NodeManager::currentNM()->mkNode(AND, exp); |
1187 |
1648 |
lem = lem.negate(); |
1188 |
3296 |
Trace("sygus-sb-exc") << " ........exc lemma is " << lem << ", size = " << sz |
1189 |
1648 |
<< std::endl; |
1190 |
1648 |
registerSymBreakLemma(tn, lem, sz, a); |
1191 |
1648 |
} |
1192 |
|
|
1193 |
1657 |
void SygusExtension::registerSymBreakLemma(TypeNode tn, |
1194 |
|
Node lem, |
1195 |
|
unsigned sz, |
1196 |
|
Node a) |
1197 |
|
{ |
1198 |
|
// lem holds for all terms of type tn, and is applicable to terms of size sz |
1199 |
3314 |
Trace("sygus-sb-debug") << " register sym break lemma : " << lem |
1200 |
1657 |
<< std::endl; |
1201 |
1657 |
Trace("sygus-sb-debug") << " anchor : " << a << std::endl; |
1202 |
1657 |
Trace("sygus-sb-debug") << " type : " << tn << std::endl; |
1203 |
1657 |
Trace("sygus-sb-debug") << " size : " << sz << std::endl; |
1204 |
1657 |
Assert(!a.isNull()); |
1205 |
1657 |
SearchCache& sca = d_cache[a]; |
1206 |
1657 |
sca.d_sbLemmas[tn][sz].push_back(lem); |
1207 |
3314 |
TNode x = getFreeVar( tn ); |
1208 |
1657 |
unsigned csz = getSearchSizeForAnchor( a ); |
1209 |
1657 |
int max_depth = ((int)csz)-((int)sz); |
1210 |
1657 |
NodeManager* nm = NodeManager::currentNM(); |
1211 |
3832 |
for( int d=0; d<=max_depth; d++ ){ |
1212 |
|
std::map<unsigned, std::vector<Node>>::iterator itt = |
1213 |
2175 |
sca.d_search_terms[tn].find(d); |
1214 |
2175 |
if (itt != sca.d_search_terms[tn].end()) |
1215 |
|
{ |
1216 |
3707 |
for (const Node& t : itt->second) |
1217 |
|
{ |
1218 |
3996 |
if (!options::sygusSymBreakLazy() |
1219 |
1998 |
|| d_active_terms.find(t) != d_active_terms.end()) |
1220 |
|
{ |
1221 |
3580 |
Node slem = lem.substitute(x, t); |
1222 |
3580 |
Node rlv = getRelevancyCondition(t); |
1223 |
1790 |
if (!rlv.isNull()) |
1224 |
|
{ |
1225 |
290 |
slem = nm->mkNode(OR, rlv, slem); |
1226 |
|
} |
1227 |
1790 |
d_im.lemma(slem, InferenceId::DATATYPES_SYGUS_SYM_BREAK); |
1228 |
|
} |
1229 |
|
} |
1230 |
|
} |
1231 |
|
} |
1232 |
1657 |
} |
1233 |
|
|
1234 |
67479 |
void SygusExtension::addSymBreakLemmasFor(TypeNode tn, TNode t, unsigned d) |
1235 |
|
{ |
1236 |
67479 |
Assert(d_term_to_anchor.find(t) != d_term_to_anchor.end()); |
1237 |
134958 |
Node a = d_term_to_anchor[t]; |
1238 |
67479 |
addSymBreakLemmasFor(tn, t, d, a); |
1239 |
67479 |
} |
1240 |
|
|
1241 |
67479 |
void SygusExtension::addSymBreakLemmasFor(TypeNode tn, |
1242 |
|
TNode t, |
1243 |
|
unsigned d, |
1244 |
|
Node a) |
1245 |
|
{ |
1246 |
67479 |
Assert(t.getType() == tn); |
1247 |
67479 |
Assert(!a.isNull()); |
1248 |
134958 |
Trace("sygus-sb-debug2") << "add sym break lemmas for " << t << " " << d |
1249 |
67479 |
<< " " << a << std::endl; |
1250 |
67479 |
SearchCache& sca = d_cache[a]; |
1251 |
|
std::map<TypeNode, std::map<uint64_t, std::vector<Node>>>::iterator its = |
1252 |
67479 |
sca.d_sbLemmas.find(tn); |
1253 |
134958 |
Node rlv = getRelevancyCondition(t); |
1254 |
67479 |
NodeManager* nm = NodeManager::currentNM(); |
1255 |
67479 |
if (its != sca.d_sbLemmas.end()) |
1256 |
|
{ |
1257 |
94874 |
TNode x = getFreeVar( tn ); |
1258 |
|
//get symmetry breaking lemmas for this term |
1259 |
47437 |
unsigned csz = getSearchSizeForAnchor( a ); |
1260 |
47437 |
uint64_t max_sz = d > csz ? 0 : (csz - d); |
1261 |
94874 |
Trace("sygus-sb-debug2") |
1262 |
47437 |
<< "add lemmas up to size " << max_sz << ", which is (search_size) " |
1263 |
47437 |
<< csz << " - (depth) " << d << std::endl; |
1264 |
94874 |
std::unordered_map<TNode, TNode> cache; |
1265 |
145191 |
for (std::pair<const uint64_t, std::vector<Node>>& sbls : its->second) |
1266 |
|
{ |
1267 |
97754 |
if (sbls.first <= max_sz) |
1268 |
|
{ |
1269 |
422287 |
for (const Node& lem : sbls.second) |
1270 |
|
{ |
1271 |
733288 |
Node slem = lem.substitute(x, t, cache); |
1272 |
|
// add the relevancy condition for t |
1273 |
366644 |
if (!rlv.isNull()) |
1274 |
|
{ |
1275 |
188755 |
slem = nm->mkNode(OR, rlv, slem); |
1276 |
|
} |
1277 |
366644 |
d_im.lemma(slem, InferenceId::DATATYPES_SYGUS_SYM_BREAK); |
1278 |
|
} |
1279 |
|
} |
1280 |
|
} |
1281 |
|
} |
1282 |
67479 |
Trace("sygus-sb-debug2") << "...finished." << std::endl; |
1283 |
67479 |
} |
1284 |
|
|
1285 |
23748 |
void SygusExtension::preRegisterTerm(TNode n) |
1286 |
|
{ |
1287 |
23748 |
if( n.isVar() ){ |
1288 |
1257 |
Trace("sygus-sb-debug") << "Pre-register variable : " << n << std::endl; |
1289 |
1257 |
registerSizeTerm(n); |
1290 |
|
} |
1291 |
23748 |
} |
1292 |
|
|
1293 |
2040 |
void SygusExtension::registerSizeTerm(Node e) |
1294 |
|
{ |
1295 |
2040 |
if (d_register_st.find(e) != d_register_st.end()) |
1296 |
|
{ |
1297 |
|
// already registered |
1298 |
2821 |
return; |
1299 |
|
} |
1300 |
1259 |
TypeNode etn = e.getType(); |
1301 |
807 |
if (!etn.isDatatype()) |
1302 |
|
{ |
1303 |
|
// not a datatype term |
1304 |
33 |
d_register_st[e] = false; |
1305 |
33 |
return; |
1306 |
|
} |
1307 |
774 |
const DType& dt = etn.getDType(); |
1308 |
774 |
if (!dt.isSygus()) |
1309 |
|
{ |
1310 |
|
// not a sygus datatype term |
1311 |
160 |
d_register_st[e] = false; |
1312 |
160 |
return; |
1313 |
|
} |
1314 |
614 |
if (!d_tds->isEnumerator(e)) |
1315 |
|
{ |
1316 |
|
// not sure if it is a size term or not (may be registered later?) |
1317 |
162 |
return; |
1318 |
|
} |
1319 |
452 |
d_register_st[e] = true; |
1320 |
904 |
Node ag = d_tds->getActiveGuardForEnumerator(e); |
1321 |
452 |
if (!ag.isNull()) |
1322 |
|
{ |
1323 |
117 |
d_anchor_to_active_guard[e] = ag; |
1324 |
|
std::map<Node, std::unique_ptr<DecisionStrategy>>::iterator itaas = |
1325 |
117 |
d_anchor_to_ag_strategy.find(e); |
1326 |
117 |
if (itaas == d_anchor_to_ag_strategy.end()) |
1327 |
|
{ |
1328 |
351 |
d_anchor_to_ag_strategy[e].reset( |
1329 |
|
new DecisionStrategySingleton("sygus_enum_active", |
1330 |
|
ag, |
1331 |
117 |
d_state.getSatContext(), |
1332 |
234 |
d_state.getValuation())); |
1333 |
|
} |
1334 |
234 |
d_im.getDecisionManager()->registerStrategy( |
1335 |
|
DecisionManager::STRAT_DT_SYGUS_ENUM_ACTIVE, |
1336 |
117 |
d_anchor_to_ag_strategy[e].get()); |
1337 |
|
} |
1338 |
904 |
Node m; |
1339 |
452 |
if (!ag.isNull()) |
1340 |
|
{ |
1341 |
|
// if it has an active guard (it is an enumerator), use itself as measure |
1342 |
|
// term. This will enforce fairness on it independently. |
1343 |
117 |
m = e; |
1344 |
|
} |
1345 |
|
else |
1346 |
|
{ |
1347 |
|
// otherwise we enforce fairness in a unified way for all |
1348 |
335 |
if (d_generic_measure_term.isNull()) |
1349 |
|
{ |
1350 |
|
// choose e as master for all future terms |
1351 |
153 |
d_generic_measure_term = e; |
1352 |
|
} |
1353 |
335 |
m = d_generic_measure_term; |
1354 |
|
} |
1355 |
904 |
Trace("sygus-sb") << "Sygus : register size term : " << e << " with measure " |
1356 |
452 |
<< m << std::endl; |
1357 |
452 |
registerMeasureTerm(m); |
1358 |
452 |
d_szinfo[m]->d_anchors.push_back(e); |
1359 |
452 |
d_anchor_to_measure_term[e] = m; |
1360 |
452 |
NodeManager* nm = NodeManager::currentNM(); |
1361 |
452 |
if (options::sygusFair() == options::SygusFairMode::DT_SIZE) |
1362 |
|
{ |
1363 |
|
// update constraints on the measure term |
1364 |
898 |
Node slem; |
1365 |
449 |
if (options::sygusFairMax()) |
1366 |
|
{ |
1367 |
898 |
Node ds = nm->mkNode(DT_SIZE, e); |
1368 |
449 |
slem = nm->mkNode(LEQ, ds, d_szinfo[m]->getOrMkMeasureValue()); |
1369 |
|
}else{ |
1370 |
|
Node mt = d_szinfo[m]->getOrMkActiveMeasureValue(); |
1371 |
|
Node newMt = d_szinfo[m]->getOrMkActiveMeasureValue(true); |
1372 |
|
Node ds = nm->mkNode(DT_SIZE, e); |
1373 |
|
slem = mt.eqNode(nm->mkNode(PLUS, newMt, ds)); |
1374 |
|
} |
1375 |
449 |
Trace("sygus-sb") << "...size lemma : " << slem << std::endl; |
1376 |
449 |
d_im.lemma(slem, InferenceId::DATATYPES_SYGUS_MT_BOUND); |
1377 |
|
} |
1378 |
452 |
if (d_tds->isVariableAgnosticEnumerator(e)) |
1379 |
|
{ |
1380 |
|
// if it is variable agnostic, enforce top-level constraint that says no |
1381 |
|
// variables occur pre-traversal at top-level |
1382 |
2 |
Node varList = dt.getSygusVarList(); |
1383 |
2 |
std::vector<Node> constraints; |
1384 |
1 |
quantifiers::SygusTypeInfo& eti = d_tds->getTypeInfo(etn); |
1385 |
3 |
for (const Node& v : varList) |
1386 |
|
{ |
1387 |
2 |
unsigned sc = eti.getSubclassForVar(v); |
1388 |
|
// no symmetry breaking occurs for variables in singleton subclasses |
1389 |
2 |
if (eti.getNumSubclassVars(sc) > 1) |
1390 |
|
{ |
1391 |
4 |
Node preRootOp = getTraversalPredicate(etn, v, true); |
1392 |
4 |
Node preRoot = nm->mkNode(APPLY_UF, preRootOp, e); |
1393 |
2 |
constraints.push_back(preRoot.negate()); |
1394 |
|
} |
1395 |
|
} |
1396 |
1 |
if (!constraints.empty()) |
1397 |
|
{ |
1398 |
1 |
Node preNoVar = constraints.size() == 1 ? constraints[0] |
1399 |
2 |
: nm->mkNode(AND, constraints); |
1400 |
2 |
Node preNoVarProc = eliminateTraversalPredicates(preNoVar); |
1401 |
1 |
Trace("sygus-sb") << "...variable order : " << preNoVarProc << std::endl; |
1402 |
2 |
Trace("sygus-sb-tp") << "...variable order : " << preNoVarProc |
1403 |
1 |
<< std::endl; |
1404 |
1 |
d_im.lemma(preNoVarProc, InferenceId::DATATYPES_SYGUS_VAR_AGNOSTIC); |
1405 |
|
} |
1406 |
|
} |
1407 |
|
} |
1408 |
|
|
1409 |
9274 |
void SygusExtension::registerMeasureTerm( Node m ) { |
1410 |
|
std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator it = |
1411 |
9274 |
d_szinfo.find(m); |
1412 |
9274 |
if( it==d_szinfo.end() ){ |
1413 |
270 |
Trace("sygus-sb") << "Sygus : register measure term : " << m << std::endl; |
1414 |
270 |
d_szinfo[m].reset(new SygusSizeDecisionStrategy(d_im, m, d_state)); |
1415 |
|
// register this as a decision strategy |
1416 |
540 |
d_im.getDecisionManager()->registerStrategy( |
1417 |
270 |
DecisionManager::STRAT_DT_SYGUS_ENUM_SIZE, d_szinfo[m].get()); |
1418 |
|
} |
1419 |
9274 |
} |
1420 |
|
|
1421 |
6441 |
void SygusExtension::notifySearchSize(TNode m, uint64_t s, Node exp) |
1422 |
|
{ |
1423 |
|
std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator its = |
1424 |
6441 |
d_szinfo.find(m); |
1425 |
6441 |
Assert(its != d_szinfo.end()); |
1426 |
6441 |
if( its->second->d_search_size.find( s )==its->second->d_search_size.end() ){ |
1427 |
478 |
its->second->d_search_size[s] = true; |
1428 |
478 |
its->second->d_search_size_exp[s] = exp; |
1429 |
478 |
Assert(s == 0 |
1430 |
|
|| its->second->d_search_size.find(s - 1) |
1431 |
|
!= its->second->d_search_size.end()); |
1432 |
478 |
Trace("sygus-fair") << "SygusExtension:: now considering term measure : " << s << " for " << m << std::endl; |
1433 |
478 |
Assert(s >= its->second->d_curr_search_size); |
1434 |
894 |
while( s>its->second->d_curr_search_size ){ |
1435 |
208 |
incrementCurrentSearchSize(m); |
1436 |
|
} |
1437 |
478 |
Trace("sygus-fair") << "...finish increment for term measure : " << s << std::endl; |
1438 |
|
} |
1439 |
6441 |
} |
1440 |
|
|
1441 |
|
unsigned SygusExtension::getSearchSizeFor( Node n ) { |
1442 |
|
Trace("sygus-sb-debug2") << "get search size for term : " << n << std::endl; |
1443 |
|
std::unordered_map<Node, Node>::iterator ita = d_term_to_anchor.find(n); |
1444 |
|
Assert(ita != d_term_to_anchor.end()); |
1445 |
|
return getSearchSizeForAnchor( ita->second ); |
1446 |
|
} |
1447 |
|
|
1448 |
57753 |
unsigned SygusExtension::getSearchSizeForAnchor( Node a ) { |
1449 |
57753 |
Trace("sygus-sb-debug2") << "get search size for anchor : " << a << std::endl; |
1450 |
57753 |
std::map< Node, Node >::iterator it = d_anchor_to_measure_term.find( a ); |
1451 |
57753 |
Assert(it != d_anchor_to_measure_term.end()); |
1452 |
57753 |
return getSearchSizeForMeasureTerm(it->second); |
1453 |
|
} |
1454 |
|
|
1455 |
57753 |
unsigned SygusExtension::getSearchSizeForMeasureTerm(Node m) |
1456 |
|
{ |
1457 |
57753 |
Trace("sygus-sb-debug2") << "get search size for measure : " << m << std::endl; |
1458 |
|
std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator its = |
1459 |
57753 |
d_szinfo.find(m); |
1460 |
57753 |
Assert(its != d_szinfo.end()); |
1461 |
57753 |
return its->second->d_curr_search_size; |
1462 |
|
} |
1463 |
|
|
1464 |
208 |
void SygusExtension::incrementCurrentSearchSize(TNode m) |
1465 |
|
{ |
1466 |
|
std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator itsz = |
1467 |
208 |
d_szinfo.find(m); |
1468 |
208 |
Assert(itsz != d_szinfo.end()); |
1469 |
208 |
itsz->second->d_curr_search_size++; |
1470 |
208 |
Trace("sygus-fair") << " register search size " << itsz->second->d_curr_search_size << " for " << m << std::endl; |
1471 |
208 |
NodeManager* nm = NodeManager::currentNM(); |
1472 |
496 |
for( std::map< Node, SearchCache >::iterator itc = d_cache.begin(); itc != d_cache.end(); ++itc ){ |
1473 |
576 |
Node a = itc->first; |
1474 |
288 |
Trace("sygus-fair-debug") << " look at anchor " << a << "..." << std::endl; |
1475 |
|
// check whether a is bounded by m |
1476 |
288 |
Assert(d_anchor_to_measure_term.find(a) != d_anchor_to_measure_term.end()); |
1477 |
288 |
if( d_anchor_to_measure_term[a]==m ){ |
1478 |
70 |
for (std::pair<const TypeNode, std::map<uint64_t, std::vector<Node>>>& |
1479 |
285 |
sbl : itc->second.d_sbLemmas) |
1480 |
|
{ |
1481 |
140 |
TypeNode tn = sbl.first; |
1482 |
140 |
TNode x = getFreeVar( tn ); |
1483 |
163 |
for (std::pair<const uint64_t, std::vector<Node>>& s : sbl.second) |
1484 |
|
{ |
1485 |
93 |
unsigned sz = s.first; |
1486 |
93 |
int new_depth = ((int)itsz->second->d_curr_search_size) - ((int)sz); |
1487 |
93 |
std::map< unsigned, std::vector< Node > >::iterator itt = itc->second.d_search_terms[tn].find( new_depth ); |
1488 |
93 |
if( itt!=itc->second.d_search_terms[tn].end() ){ |
1489 |
315 |
for (const Node& t : itt->second) |
1490 |
|
{ |
1491 |
488 |
if (!options::sygusSymBreakLazy() |
1492 |
244 |
|| (d_active_terms.find(t) != d_active_terms.end() |
1493 |
|
&& !s.second.empty())) |
1494 |
|
{ |
1495 |
|
Node rlv = getRelevancyCondition(t); |
1496 |
|
std::unordered_map<TNode, TNode> cache; |
1497 |
|
for (const Node& lem : s.second) |
1498 |
|
{ |
1499 |
|
Node slem = lem.substitute(x, t, cache); |
1500 |
|
if (!rlv.isNull()) |
1501 |
|
{ |
1502 |
|
slem = nm->mkNode(OR, rlv, slem); |
1503 |
|
} |
1504 |
|
d_im.lemma(slem, InferenceId::DATATYPES_SYGUS_SYM_BREAK); |
1505 |
|
} |
1506 |
|
} |
1507 |
|
} |
1508 |
|
} |
1509 |
|
} |
1510 |
|
} |
1511 |
|
} |
1512 |
|
} |
1513 |
208 |
} |
1514 |
|
|
1515 |
5517 |
void SygusExtension::check() |
1516 |
|
{ |
1517 |
5517 |
Trace("sygus-sb") << "SygusExtension::check" << std::endl; |
1518 |
|
|
1519 |
|
// reset the count of lemmas sent |
1520 |
5517 |
d_im.reset(); |
1521 |
|
|
1522 |
|
// check for externally registered symmetry breaking lemmas |
1523 |
10829 |
std::vector<Node> anchors; |
1524 |
5517 |
if (d_tds->hasSymBreakLemmas(anchors)) |
1525 |
|
{ |
1526 |
384 |
for (const Node& a : anchors) |
1527 |
|
{ |
1528 |
|
// is this a registered enumerator? |
1529 |
198 |
if (d_register_st.find(a) != d_register_st.end()) |
1530 |
|
{ |
1531 |
|
// symmetry breaking lemmas should only be for enumerators |
1532 |
147 |
Assert(d_register_st[a]); |
1533 |
|
// If this is a non-basic enumerator, process its symmetry breaking |
1534 |
|
// clauses. Since this class is not responsible for basic enumerators, |
1535 |
|
// their symmetry breaking clauses are ignored. |
1536 |
147 |
if (!d_tds->isBasicEnumerator(a)) |
1537 |
|
{ |
1538 |
8 |
std::vector<Node> sbl; |
1539 |
4 |
d_tds->getSymBreakLemmas(a, sbl); |
1540 |
13 |
for (const Node& lem : sbl) |
1541 |
|
{ |
1542 |
9 |
if (d_tds->isSymBreakLemmaTemplate(lem)) |
1543 |
|
{ |
1544 |
|
// register the lemma template |
1545 |
18 |
TypeNode tn = d_tds->getTypeForSymBreakLemma(lem); |
1546 |
9 |
unsigned sz = d_tds->getSizeForSymBreakLemma(lem); |
1547 |
9 |
registerSymBreakLemma(tn, lem, sz, a); |
1548 |
|
} |
1549 |
|
else |
1550 |
|
{ |
1551 |
|
Trace("dt-sygus-debug") |
1552 |
|
<< "DT sym break lemma : " << lem << std::endl; |
1553 |
|
// it is a normal lemma |
1554 |
|
d_im.lemma(lem, InferenceId::DATATYPES_SYGUS_ENUM_SYM_BREAK); |
1555 |
|
} |
1556 |
|
} |
1557 |
4 |
d_tds->clearSymBreakLemmas(a); |
1558 |
|
} |
1559 |
|
} |
1560 |
|
} |
1561 |
186 |
if (d_im.hasSentLemma()) |
1562 |
|
{ |
1563 |
|
return; |
1564 |
|
} |
1565 |
|
} |
1566 |
|
|
1567 |
|
// register search values, add symmetry breaking lemmas if applicable |
1568 |
10829 |
std::vector<Node> es; |
1569 |
5517 |
d_tds->getEnumerators(es); |
1570 |
5517 |
bool needsRecheck = false; |
1571 |
|
// for each enumerator registered to d_tds |
1572 |
14759 |
for (Node& prog : es) |
1573 |
|
{ |
1574 |
9242 |
if (d_register_st.find(prog) == d_register_st.end()) |
1575 |
|
{ |
1576 |
|
// not yet registered, do so now |
1577 |
286 |
registerSizeTerm(prog); |
1578 |
286 |
needsRecheck = true; |
1579 |
|
} |
1580 |
|
else |
1581 |
|
{ |
1582 |
17912 |
Trace("dt-sygus-debug") << "Checking model value of " << prog << "..." |
1583 |
8956 |
<< std::endl; |
1584 |
8956 |
Assert(prog.getType().isDatatype()); |
1585 |
17912 |
Node progv = d_state.getValuation().getModel()->getValue(prog); |
1586 |
8956 |
if (Trace.isOn("dt-sygus")) |
1587 |
|
{ |
1588 |
|
Trace("dt-sygus") << "* DT model : " << prog << " -> "; |
1589 |
|
std::stringstream ss; |
1590 |
|
quantifiers::TermDbSygus::toStreamSygus(ss, progv); |
1591 |
|
Trace("dt-sygus") << ss.str() << std::endl; |
1592 |
|
} |
1593 |
|
// first check that the value progv for prog is what we expected |
1594 |
8956 |
bool isExc = true; |
1595 |
8956 |
if (checkValue(prog, progv, 0)) |
1596 |
|
{ |
1597 |
8662 |
isExc = false; |
1598 |
|
//debugging : ensure fairness was properly handled |
1599 |
8662 |
if (options::sygusFair() == options::SygusFairMode::DT_SIZE) |
1600 |
|
{ |
1601 |
17318 |
Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, prog ); |
1602 |
17318 |
Node prog_szv = d_state.getValuation().getModel()->getValue(prog_sz); |
1603 |
17318 |
Node progv_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, progv ); |
1604 |
|
|
1605 |
8659 |
Trace("sygus-sb") << " Mv[" << prog << "] = " << progv << ", size = " << prog_szv << std::endl; |
1606 |
8659 |
if( prog_szv.getConst<Rational>().getNumerator().toUnsignedInt() > getSearchSizeForAnchor( prog ) ){ |
1607 |
|
AlwaysAssert(false); |
1608 |
|
Node szlem = NodeManager::currentNM()->mkNode( kind::OR, prog.eqNode( progv ).negate(), |
1609 |
|
prog_sz.eqNode( progv_sz ) ); |
1610 |
|
Trace("sygus-sb-warn") << "SygusSymBreak : WARNING : adding size correction : " << szlem << std::endl; |
1611 |
|
d_im.lemma(szlem, InferenceId::DATATYPES_SYGUS_SIZE_CORRECTION); |
1612 |
|
isExc = true; |
1613 |
|
} |
1614 |
|
} |
1615 |
|
|
1616 |
|
// register the search value ( prog -> progv ), this may invoke symmetry |
1617 |
|
// breaking |
1618 |
8662 |
if (!isExc && options::sygusSymBreakDynamic()) |
1619 |
|
{ |
1620 |
8662 |
bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(prog); |
1621 |
|
// check that it is unique up to theory-specific rewriting and |
1622 |
|
// conjecture-specific symmetry breaking. |
1623 |
|
Node rsv = |
1624 |
17324 |
registerSearchValue(prog, prog, progv, 0, isVarAgnostic, true); |
1625 |
8662 |
if (rsv.isNull()) |
1626 |
|
{ |
1627 |
1643 |
isExc = true; |
1628 |
1643 |
Trace("sygus-sb") << " SygusExtension::check: ...added new symmetry breaking lemma for " << prog << "." << std::endl; |
1629 |
|
} |
1630 |
|
else |
1631 |
|
{ |
1632 |
7019 |
Trace("dt-sygus") << " ...success." << std::endl; |
1633 |
|
} |
1634 |
|
} |
1635 |
|
} |
1636 |
|
SygusSymBreakOkAttribute ssbo; |
1637 |
8956 |
prog.setAttribute(ssbo, !isExc); |
1638 |
|
} |
1639 |
|
} |
1640 |
5517 |
Trace("sygus-sb") << "SygusExtension::check: finished." << std::endl; |
1641 |
5517 |
if (needsRecheck) |
1642 |
|
{ |
1643 |
205 |
Trace("sygus-sb") << " SygusExtension::rechecking..." << std::endl; |
1644 |
205 |
return check(); |
1645 |
|
} |
1646 |
|
|
1647 |
5312 |
if (Trace.isOn("sygus-engine") && !d_szinfo.empty()) |
1648 |
|
{ |
1649 |
|
if (d_im.hasSentLemma()) |
1650 |
|
{ |
1651 |
|
Trace("sygus-engine") << "*** Sygus : passed datatypes check. term size(s) : "; |
1652 |
|
for (std::pair<const Node, std::unique_ptr<SygusSizeDecisionStrategy>>& |
1653 |
|
p : d_szinfo) |
1654 |
|
{ |
1655 |
|
SygusSizeDecisionStrategy* s = p.second.get(); |
1656 |
|
Trace("sygus-engine") << s->d_curr_search_size << " "; |
1657 |
|
} |
1658 |
|
Trace("sygus-engine") << std::endl; |
1659 |
|
} |
1660 |
|
else |
1661 |
|
{ |
1662 |
|
Trace("sygus-engine") |
1663 |
|
<< "*** Sygus : produced symmetry breaking lemmas" << std::endl; |
1664 |
|
} |
1665 |
|
} |
1666 |
|
} |
1667 |
|
|
1668 |
29310 |
bool SygusExtension::checkValue(Node n, TNode vn, int ind) |
1669 |
|
{ |
1670 |
29310 |
if (vn.getKind() != kind::APPLY_CONSTRUCTOR) |
1671 |
|
{ |
1672 |
|
// all datatype terms should be constant here |
1673 |
477 |
Assert(!vn.getType().isDatatype()); |
1674 |
477 |
return true; |
1675 |
|
} |
1676 |
28833 |
NodeManager* nm = NodeManager::currentNM(); |
1677 |
28833 |
if (Trace.isOn("sygus-sb-check-value")) |
1678 |
|
{ |
1679 |
|
Node prog_sz = nm->mkNode(DT_SIZE, n); |
1680 |
|
Node prog_szv = d_state.getValuation().getModel()->getValue(prog_sz); |
1681 |
|
for( int i=0; i<ind; i++ ){ |
1682 |
|
Trace("sygus-sb-check-value") << " "; |
1683 |
|
} |
1684 |
|
Trace("sygus-sb-check-value") << n << " : " << vn << " : " << prog_szv |
1685 |
|
<< std::endl; |
1686 |
|
} |
1687 |
57666 |
TypeNode tn = n.getType(); |
1688 |
28833 |
const DType& dt = tn.getDType(); |
1689 |
|
|
1690 |
|
// ensure that the expected size bound is met |
1691 |
28833 |
int cindex = utils::indexOf(vn.getOperator()); |
1692 |
57666 |
Node tst = utils::mkTester(n, cindex, dt); |
1693 |
28833 |
bool hastst = d_state.getEqualityEngine()->hasTerm(tst); |
1694 |
57666 |
Node tstrep; |
1695 |
28833 |
if (hastst) |
1696 |
|
{ |
1697 |
28539 |
tstrep = d_state.getEqualityEngine()->getRepresentative(tst); |
1698 |
|
} |
1699 |
28833 |
if (!hastst || tstrep != d_true) |
1700 |
|
{ |
1701 |
588 |
Trace("sygus-check-value") << "- has tester : " << tst << " : " |
1702 |
294 |
<< (hastst ? "true" : "false"); |
1703 |
294 |
Trace("sygus-check-value") << ", value=" << tstrep << std::endl; |
1704 |
294 |
if( !hastst ){ |
1705 |
|
// This should not happen generally, it is caused by a sygus term not |
1706 |
|
// being assigned a tester. |
1707 |
588 |
Node split = utils::mkSplit(n, dt); |
1708 |
588 |
Trace("sygus-sb") << " SygusExtension::check: ...WARNING: considered " |
1709 |
294 |
"missing split for " |
1710 |
294 |
<< n << "." << std::endl; |
1711 |
294 |
Assert(!split.isNull()); |
1712 |
294 |
d_im.lemma(split, InferenceId::DATATYPES_SYGUS_VALUE_CORRECTION); |
1713 |
294 |
return false; |
1714 |
|
} |
1715 |
|
} |
1716 |
48882 |
for( unsigned i=0; i<vn.getNumChildren(); i++ ){ |
1717 |
|
Node sel = nm->mkNode( |
1718 |
40697 |
APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), n); |
1719 |
20354 |
if (!checkValue(sel, vn[i], ind + 1)) |
1720 |
|
{ |
1721 |
11 |
return false; |
1722 |
|
} |
1723 |
|
} |
1724 |
28528 |
return true; |
1725 |
|
} |
1726 |
|
|
1727 |
|
Node SygusExtension::getCurrentTemplate( Node n, std::map< TypeNode, int >& var_count ) { |
1728 |
|
if( d_active_terms.find( n )!=d_active_terms.end() ){ |
1729 |
|
TypeNode tn = n.getType(); |
1730 |
|
IntMap::const_iterator it = d_testers.find( n ); |
1731 |
|
Assert(it != d_testers.end()); |
1732 |
|
const DType& dt = tn.getDType(); |
1733 |
|
int tindex = (*it).second; |
1734 |
|
Assert(tindex >= 0); |
1735 |
|
Assert(tindex < (int)dt.getNumConstructors()); |
1736 |
|
std::vector< Node > children; |
1737 |
|
children.push_back(dt[tindex].getConstructor()); |
1738 |
|
for( unsigned i=0; i<dt[tindex].getNumArgs(); i++ ){ |
1739 |
|
Node sel = NodeManager::currentNM()->mkNode( |
1740 |
|
APPLY_SELECTOR_TOTAL, dt[tindex].getSelectorInternal(tn, i), n); |
1741 |
|
Node cc = getCurrentTemplate( sel, var_count ); |
1742 |
|
children.push_back( cc ); |
1743 |
|
} |
1744 |
|
return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); |
1745 |
|
}else{ |
1746 |
|
return d_tds->getFreeVarInc( n.getType(), var_count ); |
1747 |
|
} |
1748 |
|
} |
1749 |
|
|
1750 |
270 |
SygusExtension::SygusSizeDecisionStrategy::SygusSizeDecisionStrategy( |
1751 |
270 |
InferenceManager& im, Node t, TheoryState& s) |
1752 |
270 |
: DecisionStrategyFmf(s.getSatContext(), s.getValuation()), |
1753 |
|
d_this(t), |
1754 |
|
d_curr_search_size(0), |
1755 |
540 |
d_im(im) |
1756 |
|
{ |
1757 |
270 |
} |
1758 |
|
|
1759 |
9268 |
Node SygusExtension::SygusSizeDecisionStrategy::getOrMkMeasureValue() |
1760 |
|
{ |
1761 |
9268 |
if (d_measure_value.isNull()) |
1762 |
|
{ |
1763 |
267 |
NodeManager* nm = NodeManager::currentNM(); |
1764 |
267 |
SkolemManager* sm = nm->getSkolemManager(); |
1765 |
267 |
d_measure_value = sm->mkDummySkolem("mt", nm->integerType()); |
1766 |
|
Node mtlem = |
1767 |
534 |
nm->mkNode(kind::GEQ, d_measure_value, nm->mkConst(Rational(0))); |
1768 |
267 |
d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS); |
1769 |
|
} |
1770 |
9268 |
return d_measure_value; |
1771 |
|
} |
1772 |
|
|
1773 |
|
Node SygusExtension::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue( |
1774 |
|
bool mkNew) |
1775 |
|
{ |
1776 |
|
if (mkNew) |
1777 |
|
{ |
1778 |
|
NodeManager* nm = NodeManager::currentNM(); |
1779 |
|
SkolemManager* sm = nm->getSkolemManager(); |
1780 |
|
Node new_mt = sm->mkDummySkolem("mt", nm->integerType()); |
1781 |
|
Node mtlem = nm->mkNode(kind::GEQ, new_mt, nm->mkConst(Rational(0))); |
1782 |
|
d_measure_value_active = new_mt; |
1783 |
|
d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS); |
1784 |
|
} |
1785 |
|
else if (d_measure_value_active.isNull()) |
1786 |
|
{ |
1787 |
|
d_measure_value_active = getOrMkMeasureValue(); |
1788 |
|
} |
1789 |
|
return d_measure_value_active; |
1790 |
|
} |
1791 |
|
|
1792 |
480 |
Node SygusExtension::SygusSizeDecisionStrategy::mkLiteral(unsigned s) |
1793 |
|
{ |
1794 |
480 |
if (options::sygusFair() == options::SygusFairMode::NONE) |
1795 |
|
{ |
1796 |
|
return Node::null(); |
1797 |
|
} |
1798 |
960 |
if (options::sygusAbortSize() != -1 |
1799 |
480 |
&& static_cast<int>(s) > options::sygusAbortSize()) |
1800 |
|
{ |
1801 |
4 |
std::stringstream ss; |
1802 |
2 |
ss << "Maximum term size (" << options::sygusAbortSize() |
1803 |
2 |
<< ") for enumerative SyGuS exceeded."; |
1804 |
2 |
throw LogicException(ss.str()); |
1805 |
|
} |
1806 |
478 |
Assert(!d_this.isNull()); |
1807 |
478 |
NodeManager* nm = NodeManager::currentNM(); |
1808 |
956 |
Trace("sygus-engine") << "******* Sygus : allocate size literal " << s |
1809 |
478 |
<< " for " << d_this << std::endl; |
1810 |
478 |
return nm->mkNode(DT_SYGUS_BOUND, d_this, nm->mkConst(Rational(s))); |
1811 |
|
} |
1812 |
|
|
1813 |
|
int SygusExtension::getGuardStatus( Node g ) { |
1814 |
|
bool value; |
1815 |
|
if (d_state.getValuation().hasSatValue(g, value)) |
1816 |
|
{ |
1817 |
|
if( value ){ |
1818 |
|
return 1; |
1819 |
|
}else{ |
1820 |
|
return -1; |
1821 |
|
} |
1822 |
|
}else{ |
1823 |
|
return 0; |
1824 |
|
} |
1825 |
29511 |
} |
1826 |
|
|