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