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