1 /********************* */
2 /*! \file datatypes_sygus.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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.\endverbatim
12 ** \brief Implementation of sygus utilities for theory of datatypes
14 ** Implementation of sygus utilities for theory of datatypes
17 #include "theory/datatypes/datatypes_sygus.h"
19 #include "expr/node_manager.h"
20 #include "options/base_options.h"
21 #include "options/quantifiers_options.h"
22 #include "printer/printer.h"
23 #include "theory/datatypes/datatypes_rewriter.h"
24 #include "theory/datatypes/theory_datatypes.h"
25 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
26 #include "theory/quantifiers/sygus/sygus_explain.h"
27 #include "theory/quantifiers/sygus/term_database_sygus.h"
28 #include "theory/quantifiers/term_util.h"
29 #include "theory/theory_model.h"
32 using namespace CVC4::kind
;
33 using namespace CVC4::context
;
34 using namespace CVC4::theory
;
35 using namespace CVC4::theory::datatypes
;
37 SygusSymBreakNew::SygusSymBreakNew(TheoryDatatypes
* td
,
38 QuantifiersEngine
* qe
,
41 d_tds(qe
->getTermDatabaseSygus()),
48 d_zero
= NodeManager::currentNM()->mkConst(Rational(0));
49 d_true
= NodeManager::currentNM()->mkConst(true);
52 SygusSymBreakNew::~SygusSymBreakNew() {
57 void SygusSymBreakNew::assertTester( int tindex
, TNode n
, Node exp
, std::vector
< Node
>& lemmas
) {
58 registerTerm( n
, lemmas
);
59 // check if this is a relevant (sygus) term
60 if( d_term_to_anchor
.find( n
)!=d_term_to_anchor
.end() ){
61 Trace("sygus-sb-debug2") << "Sygus : process tester : " << exp
<< std::endl
;
62 // if not already active (may have duplicate calls for the same tester)
63 if( d_active_terms
.find( n
)==d_active_terms
.end() ) {
64 d_testers
[n
] = tindex
;
65 d_testers_exp
[n
] = exp
;
67 // check if parent is active
69 if( options::sygusSymBreakLazy() ){
70 if( n
.getKind()==kind::APPLY_SELECTOR_TOTAL
){
71 NodeSet::const_iterator it
= d_active_terms
.find( n
[0] );
72 if( it
==d_active_terms
.end() ){
75 //this must be a proper selector
76 IntMap::const_iterator itt
= d_testers
.find( n
[0] );
77 Assert( itt
!=d_testers
.end() );
78 int ptindex
= (*itt
).second
;
79 TypeNode ptn
= n
[0].getType();
80 const Datatype
& pdt
= ((DatatypeType
)ptn
.toType()).getDatatype();
81 int sindex_in_parent
= pdt
[ptindex
].getSelectorIndexInternal( n
.getOperator().toExpr() );
82 // the tester is irrelevant in this branch
83 if( sindex_in_parent
==-1 ){
90 assertTesterInternal( tindex
, n
, exp
, lemmas
);
92 Trace("sygus-sb-debug2") << "...ignore inactive tester : " << exp
<< std::endl
;
95 Trace("sygus-sb-debug2") << "...ignore repeated tester : " << exp
<< std::endl
;
98 Trace("sygus-sb-debug2") << "...ignore non-sygus tester : " << exp
<< std::endl
;
102 void SygusSymBreakNew::assertFact( Node n
, bool polarity
, std::vector
< Node
>& lemmas
) {
103 if (n
.getKind() == kind::DT_SYGUS_BOUND
)
106 Trace("sygus-fair") << "Have sygus bound : " << n
<< ", polarity=" << polarity
<< " on measure " << m
<< std::endl
;
107 registerMeasureTerm( m
);
108 if( options::sygusFair()==SYGUS_FAIR_DT_SIZE
){
109 std::map
<Node
, std::unique_ptr
<SygusSizeDecisionStrategy
>>::iterator its
=
111 Assert( its
!=d_szinfo
.end() );
112 Node mt
= its
->second
->getOrMkMeasureValue(lemmas
);
113 //it relates the measure term to arithmetic
114 Node blem
= n
.eqNode( NodeManager::currentNM()->mkNode( kind::LEQ
, mt
, n
[1] ) );
115 lemmas
.push_back( blem
);
118 unsigned s
= n
[1].getConst
<Rational
>().getNumerator().toUnsignedInt();
119 notifySearchSize( m
, s
, n
, lemmas
);
121 }else if( n
.getKind() == kind::DT_HEIGHT_BOUND
|| n
.getKind()==DT_SIZE_BOUND
){
122 //reduce to arithmetic TODO ?
127 Node
SygusSymBreakNew::getTermOrderPredicate( Node n1
, Node n2
) {
128 NodeManager
* nm
= NodeManager::currentNM();
129 std::vector
< Node
> comm_disj
;
130 // (1) size of left is greater than size of right
132 nm
->mkNode(GT
, nm
->mkNode(DT_SIZE
, n1
), nm
->mkNode(DT_SIZE
, n2
));
133 comm_disj
.push_back( sz_less
);
134 // (2) ...or sizes are equal and first child is less by term order
135 std::vector
<Node
> sz_eq_cases
;
137 nm
->mkNode(EQUAL
, nm
->mkNode(DT_SIZE
, n1
), nm
->mkNode(DT_SIZE
, n2
));
138 sz_eq_cases
.push_back( sz_eq
);
139 if( options::sygusOpt1() ){
140 TypeNode tnc
= n1
.getType();
141 const Datatype
& cdt
= ((DatatypeType
)(tnc
).toType()).getDatatype();
142 for( unsigned j
=0; j
<cdt
.getNumConstructors(); j
++ ){
143 std::vector
<Node
> case_conj
;
144 for (unsigned k
= 0; k
< j
; k
++)
146 case_conj
.push_back(DatatypesRewriter::mkTester(n2
, k
, cdt
).negate());
148 if (!case_conj
.empty())
150 Node corder
= nm
->mkNode(
152 DatatypesRewriter::mkTester(n1
, j
, cdt
).negate(),
153 case_conj
.size() == 1 ? case_conj
[0]
154 : nm
->mkNode(kind::AND
, case_conj
));
155 sz_eq_cases
.push_back(corder
);
159 Node sz_eqc
= sz_eq_cases
.size() == 1 ? sz_eq_cases
[0]
160 : nm
->mkNode(kind::AND
, sz_eq_cases
);
161 comm_disj
.push_back( sz_eqc
);
163 return nm
->mkNode(kind::OR
, comm_disj
);
166 void SygusSymBreakNew::registerTerm( Node n
, std::vector
< Node
>& lemmas
) {
167 if( d_is_top_level
.find( n
)==d_is_top_level
.end() ){
168 d_is_top_level
[n
] = false;
169 TypeNode tn
= n
.getType();
171 bool is_top_level
= false;
172 bool success
= false;
173 if( n
.getKind()==kind::APPLY_SELECTOR_TOTAL
){
174 registerTerm( n
[0], lemmas
);
175 std::unordered_map
<Node
, Node
, NodeHashFunction
>::iterator it
=
176 d_term_to_anchor
.find(n
[0]);
177 if( it
!=d_term_to_anchor
.end() ) {
178 d_term_to_anchor
[n
] = it
->second
;
179 unsigned sel_weight
=
180 d_tds
->getSelectorWeight(n
[0].getType(), n
.getOperator());
181 d
= d_term_to_depth
[n
[0]] + sel_weight
;
182 is_top_level
= computeTopLevel( tn
, n
[0] );
185 }else if( n
.isVar() ){
186 registerSizeTerm( n
, lemmas
);
187 if( d_register_st
[n
] ){
188 d_term_to_anchor
[n
] = n
;
189 d_anchor_to_conj
[n
] = d_tds
->getConjectureForEnumerator(n
);
190 // this assertion fails if we have a sygus term in the search that is unmeasured
191 Assert(d_anchor_to_conj
[n
] != NULL
);
198 Trace("sygus-sb-debug") << "Register : " << n
<< ", depth : " << d
<< ", top level = " << is_top_level
<< ", type = " << ((DatatypeType
)tn
.toType()).getDatatype().getName() << std::endl
;
199 d_term_to_depth
[n
] = d
;
200 d_is_top_level
[n
] = is_top_level
;
201 registerSearchTerm( tn
, d
, n
, is_top_level
, lemmas
);
203 Trace("sygus-sb-debug2") << "Term " << n
<< " is not part of sygus search." << std::endl
;
208 bool SygusSymBreakNew::computeTopLevel( TypeNode tn
, Node n
){
209 if( n
.getType()==tn
){
211 }else if( n
.getKind()==kind::APPLY_SELECTOR_TOTAL
){
212 return computeTopLevel( tn
, n
[0] );
218 void SygusSymBreakNew::assertTesterInternal( int tindex
, TNode n
, Node exp
, std::vector
< Node
>& lemmas
) {
219 TypeNode ntn
= n
.getType();
220 if (!ntn
.isDatatype())
222 // nothing to do for non-datatype types
225 const Datatype
& dt
= static_cast<DatatypeType
>(ntn
.toType()).getDatatype();
228 // nothing to do for non-sygus-datatype type
231 d_active_terms
.insert(n
);
232 Trace("sygus-sb-debug2") << "Sygus : activate term : " << n
<< " : " << exp
235 // get the search size for this
236 Assert( d_term_to_anchor
.find( n
)!=d_term_to_anchor
.end() );
237 Node a
= d_term_to_anchor
[n
];
238 Assert( d_anchor_to_measure_term
.find( a
)!=d_anchor_to_measure_term
.end() );
239 Node m
= d_anchor_to_measure_term
[a
];
240 std::map
<Node
, std::unique_ptr
<SygusSizeDecisionStrategy
>>::iterator itsz
=
242 Assert( itsz
!=d_szinfo
.end() );
243 unsigned ssz
= itsz
->second
->d_curr_search_size
;
245 if( options::sygusFair()==SYGUS_FAIR_DIRECT
){
246 if( dt
[tindex
].getNumArgs()>0 ){
247 // consider lower bounds for size of types
248 unsigned lb_add
= d_tds
->getMinConsTermSize( ntn
, tindex
);
249 unsigned lb_rem
= n
==a
? 0 : d_tds
->getMinTermSize( ntn
);
250 Assert( lb_add
>=lb_rem
);
251 d_currTermSize
[a
].set( d_currTermSize
[a
].get() + ( lb_add
- lb_rem
) );
253 if( (unsigned)d_currTermSize
[a
].get()>ssz
){
254 if( Trace
.isOn("sygus-sb-fair") ){
255 std::map
< TypeNode
, int > var_count
;
256 Node templ
= getCurrentTemplate( a
, var_count
);
257 Trace("sygus-sb-fair") << "FAIRNESS : we have " << d_currTermSize
[a
].get() << " at search size " << ssz
<< ", template is " << templ
<< std::endl
;
260 std::vector
< Node
> conflict
;
261 for( NodeSet::const_iterator its
= d_active_terms
.begin(); its
!= d_active_terms
.end(); ++its
){
263 Node xa
= d_term_to_anchor
[x
];
265 IntMap::const_iterator ittv
= d_testers
.find( x
);
266 Assert( ittv
!= d_testers
.end() );
267 int tindex
= (*ittv
).second
;
268 const Datatype
& dti
= ((DatatypeType
)x
.getType().toType()).getDatatype();
269 if( dti
[tindex
].getNumArgs()>0 ){
270 NodeMap::const_iterator itt
= d_testers_exp
.find( x
);
271 Assert( itt
!= d_testers_exp
.end() );
272 conflict
.push_back( (*itt
).second
);
276 Assert( conflict
.size()==(unsigned)d_currTermSize
[a
].get() );
277 Assert( itsz
->second
->d_search_size_exp
.find( ssz
)!=itsz
->second
->d_search_size_exp
.end() );
278 conflict
.push_back( itsz
->second
->d_search_size_exp
[ssz
] );
279 Node conf
= NodeManager::currentNM()->mkNode( kind::AND
, conflict
);
280 Trace("sygus-sb-fair") << "Conflict is : " << conf
<< std::endl
;
281 lemmas
.push_back( conf
.negate() );
286 // now, add all applicable symmetry breaking lemmas for this term
287 Assert( d_term_to_depth
.find( n
)!=d_term_to_depth
.end() );
288 unsigned d
= d_term_to_depth
[n
];
289 Trace("sygus-sb-fair-debug") << "Tester " << exp
<< " is for depth " << d
<< " term in search size " << ssz
<< std::endl
;
291 if( options::sygusSymBreakLazy() ){
292 // dynamic symmetry breaking
293 addSymBreakLemmasFor( ntn
, n
, d
, lemmas
);
296 Trace("sygus-sb-debug") << "Get simple symmetry breaking predicates...\n";
297 unsigned max_depth
= ssz
>=d
? ssz
-d
: 0;
298 unsigned min_depth
= d_simple_proc
[exp
];
299 NodeManager
* nm
= NodeManager::currentNM();
300 if( min_depth
<=max_depth
){
301 TNode x
= getFreeVar( ntn
);
302 std::vector
<Node
> sb_lemmas
;
303 bool usingSymCons
= d_tds
->usingSymbolicConsForEnumerator(m
);
304 for (unsigned ds
= 0; ds
<= max_depth
; ds
++)
306 // static conjecture-independent symmetry breaking
307 Trace("sygus-sb-debug") << " simple symmetry breaking...\n";
308 Node ipred
= getSimpleSymBreakPred(ntn
, tindex
, ds
, usingSymCons
);
311 sb_lemmas
.push_back(ipred
);
313 // static conjecture-dependent symmetry breaking
314 Trace("sygus-sb-debug")
315 << " conjecture-dependent symmetry breaking...\n";
316 std::map
<Node
, quantifiers::CegConjecture
*>::iterator itc
=
317 d_anchor_to_conj
.find(a
);
318 if (itc
!= d_anchor_to_conj
.end())
320 quantifiers::CegConjecture
* conj
= itc
->second
;
321 Assert(conj
!= NULL
);
322 Node dpred
= conj
->getSymmetryBreakingPredicate(x
, a
, ntn
, tindex
, ds
);
325 sb_lemmas
.push_back(dpred
);
330 // add the above symmetry breaking predicates to lemmas
331 std::unordered_map
<TNode
, TNode
, TNodeHashFunction
> cache
;
332 Node rlv
= getRelevancyCondition(n
);
333 for (const Node
& slem
: sb_lemmas
)
335 Node sslem
= slem
.substitute(x
, n
, cache
);
338 sslem
= nm
->mkNode(OR
, rlv
, sslem
);
340 lemmas
.push_back(sslem
);
343 d_simple_proc
[exp
] = max_depth
+ 1;
345 // now activate the children those testers were previously asserted in this
346 // context and are awaiting activation, if they exist.
347 if( options::sygusSymBreakLazy() ){
348 Trace("sygus-sb-debug") << "Do lazy symmetry breaking...\n";
349 for( unsigned j
=0; j
<dt
[tindex
].getNumArgs(); j
++ ){
350 Node sel
= NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL
, Node::fromExpr( dt
[tindex
].getSelectorInternal( ntn
.toType(), j
) ), n
);
351 Trace("sygus-sb-debug2") << " activate child sel : " << sel
<< std::endl
;
352 Assert( d_active_terms
.find( sel
)==d_active_terms
.end() );
353 IntMap::const_iterator itt
= d_testers
.find( sel
);
354 if( itt
!= d_testers
.end() ){
355 Assert( d_testers_exp
.find( sel
) != d_testers_exp
.end() );
356 assertTesterInternal( (*itt
).second
, sel
, d_testers_exp
[sel
], lemmas
);
359 Trace("sygus-sb-debug") << "...finished" << std::endl
;
363 Node
SygusSymBreakNew::getRelevancyCondition( Node n
) {
364 std::map
< Node
, Node
>::iterator itr
= d_rlv_cond
.find( n
);
365 if( itr
==d_rlv_cond
.end() ){
367 if( n
.getKind()==APPLY_SELECTOR_TOTAL
&& options::sygusSymBreakRlv() ){
368 TypeNode ntn
= n
[0].getType();
369 Type nt
= ntn
.toType();
370 const Datatype
& dt
= ((DatatypeType
)nt
).getDatatype();
371 Expr selExpr
= n
.getOperator().toExpr();
372 if( options::dtSharedSelectors() ){
373 std::vector
< Node
> disj
;
375 for( unsigned i
=0; i
<dt
.getNumConstructors(); i
++ ){
376 int sindexi
= dt
[i
].getSelectorIndexInternal(selExpr
);
379 disj
.push_back(DatatypesRewriter::mkTester(n
[0], i
, dt
).negate());
386 Assert( !disj
.empty() );
388 cond
= disj
.size() == 1 ? disj
[0] : NodeManager::currentNM()->mkNode(
392 int sindex
= Datatype::cindexOf( selExpr
);
393 Assert( sindex
!=-1 );
394 cond
= DatatypesRewriter::mkTester(n
[0], sindex
, dt
).negate();
396 Node c1
= getRelevancyCondition( n
[0] );
399 }else if( !c1
.isNull() ){
400 cond
= NodeManager::currentNM()->mkNode(kind::OR
, cond
, c1
);
403 Trace("sygus-sb-debug2") << "Relevancy condition for " << n
<< " is " << cond
<< std::endl
;
404 d_rlv_cond
[n
] = cond
;
411 Node
SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn
,
416 std::map
<unsigned, Node
>::iterator it
=
417 d_simple_sb_pred
[tn
][tindex
][usingSymCons
].find(depth
);
418 if (it
!= d_simple_sb_pred
[tn
][tindex
][usingSymCons
].end())
422 // this function is only called on sygus datatype types
423 Assert(tn
.isDatatype());
424 NodeManager
* nm
= NodeManager::currentNM();
425 Node n
= getFreeVar(tn
);
426 const Datatype
& dt
= static_cast<DatatypeType
>(tn
.toType()).getDatatype();
427 Assert(dt
.isSygus());
428 Assert(tindex
>= 0 && tindex
< static_cast<int>(dt
.getNumConstructors()));
430 Trace("sygus-sb-simple-debug")
431 << "Simple symmetry breaking for " << dt
.getName() << ", constructor "
432 << dt
[tindex
].getName() << ", at depth " << depth
<< std::endl
;
434 // if we are the "any constant" constructor, we do no symmetry breaking
435 // only do simple symmetry breaking up to depth 2
436 Node sop
= Node::fromExpr(dt
[tindex
].getSygusOp());
437 if (sop
.getAttribute(SygusAnyConstAttribute()) || depth
> 2)
439 d_simple_sb_pred
[tn
][tindex
][usingSymCons
][depth
] = Node::null();
442 // conjunctive conclusion of lemma
443 std::vector
<Node
> sbp_conj
;
447 Trace("sygus-sb-simple-debug") << " Size..." << std::endl
;
449 if (options::sygusFair() == SYGUS_FAIR_DT_SIZE
)
451 Node szl
= nm
->mkNode(DT_SIZE
, n
);
453 nm
->mkNode(DT_SIZE
, DatatypesRewriter::getInstCons(n
, dt
, tindex
));
454 szr
= Rewriter::rewrite(szr
);
455 sbp_conj
.push_back(szl
.eqNode(szr
));
460 Kind nk
= d_tds
->getConsNumKind(tn
, tindex
);
461 if (options::sygusSymBreak())
463 // the number of (sygus) arguments
464 unsigned dt_index_nargs
= dt
[tindex
].getNumArgs();
467 TypeNode tnb
= TypeNode::fromType(dt
.getSygusType());
469 std::vector
<Node
> children
;
470 for (unsigned j
= 0; j
< dt_index_nargs
; j
++)
472 Node sel
= nm
->mkNode(
473 APPLY_SELECTOR_TOTAL
,
474 Node::fromExpr(dt
[tindex
].getSelectorInternal(tn
.toType(), j
)),
476 Assert(sel
.getType().isDatatype());
477 children
.push_back(sel
);
480 // direct solving for children
481 // for instance, we may want to insist that the LHS of MINUS is 0
482 Trace("sygus-sb-simple-debug") << " Solve children..." << std::endl
;
483 std::map
<unsigned, unsigned> children_solved
;
484 for (unsigned j
= 0; j
< dt_index_nargs
; j
++)
486 int i
= d_ssb
.solveForArgument(tn
, tindex
, j
);
489 children_solved
[j
] = i
;
490 TypeNode ctn
= children
[j
].getType();
491 const Datatype
& cdt
=
492 static_cast<DatatypeType
>(ctn
.toType()).getDatatype();
493 Assert(i
< static_cast<int>(cdt
.getNumConstructors()));
494 sbp_conj
.push_back(DatatypesRewriter::mkTester(children
[j
], i
, cdt
));
497 // depth 1 symmetry breaking : talks about direct children
500 if (nk
!= UNDEFINED_KIND
)
502 Trace("sygus-sb-simple-debug")
503 << " Equality reasoning about children..." << std::endl
;
504 // commutative operators
505 if (quantifiers::TermUtil::isComm(nk
))
507 if (children
.size() == 2
508 && children
[0].getType() == children
[1].getType())
510 Node order_pred
= getTermOrderPredicate(children
[0], children
[1]);
511 sbp_conj
.push_back(order_pred
);
514 // operators whose arguments are non-additive (e.g. should be different)
515 std::vector
<unsigned> deq_child
[2];
516 if (children
.size() == 2 && children
[0].getType() == tn
)
519 if (quantifiers::TermUtil::isNonAdditive(nk
))
525 // other cases of rewriting x k x -> x'
527 if (nk
== GT
|| nk
== LT
|| nk
== XOR
|| nk
== MINUS
528 || nk
== BITVECTOR_SUB
|| nk
== BITVECTOR_XOR
529 || nk
== BITVECTOR_UREM_TOTAL
)
531 // must have the zero element
532 req_const
= quantifiers::TermUtil::mkTypeValue(tnb
, 0);
534 else if (nk
== EQUAL
|| nk
== LEQ
|| nk
== GEQ
535 || nk
== BITVECTOR_XNOR
)
537 req_const
= quantifiers::TermUtil::mkTypeMaxValue(tnb
);
539 // cannot do division since we have to consider when both are zero
540 if (!req_const
.isNull())
542 if (d_tds
->hasConst(tn
, req_const
))
550 deq_child
[0].push_back(0);
551 deq_child
[1].push_back(1);
554 if (nk
== ITE
|| nk
== STRING_STRREPL
)
556 deq_child
[0].push_back(1);
557 deq_child
[1].push_back(2);
559 if (nk
== STRING_STRREPL
)
561 deq_child
[0].push_back(0);
562 deq_child
[1].push_back(1);
564 // this code adds simple symmetry breaking predicates of the form
565 // d.i != d.j, for example if we are considering an ITE constructor,
566 // we enforce that d.1 != d.2 since otherwise the ITE can be
568 for (unsigned i
= 0, size
= deq_child
[0].size(); i
< size
; i
++)
570 unsigned c1
= deq_child
[0][i
];
571 unsigned c2
= deq_child
[1][i
];
572 TypeNode tnc
= children
[c1
].getType();
573 // we may only apply this symmetry breaking scheme (which introduces
574 // disequalities) if the types are infinite.
575 if (tnc
== children
[c2
].getType() && !tnc
.isInterpretedFinite())
577 Node sym_lem_deq
= children
[c1
].eqNode(children
[c2
]).negate();
578 // notice that this symmetry breaking still allows for
579 // ite( C, any_constant(x), any_constant(y) )
580 // since any_constant takes a builtin argument.
581 sbp_conj
.push_back(sym_lem_deq
);
585 Trace("sygus-sb-simple-debug") << " Redundant operators..."
587 // singular arguments (e.g. 0 for mult)
588 // redundant arguments (e.g. 0 for plus, 1 for mult)
589 // right-associativity
591 // explanation of why not all children of this are constant
592 std::vector
<Node
> exp_not_all_const
;
593 // is the above explanation valid? This is set to false if
594 // one child does not have a constant, hence making the explanation
596 bool exp_not_all_const_valid
= dt_index_nargs
> 0;
597 // does the parent have an any constant constructor?
598 bool usingAnyConstCons
=
599 usingSymCons
&& (d_tds
->getAnyConstantConsNum(tn
) != -1);
600 for (unsigned j
= 0; j
< dt_index_nargs
; j
++)
602 Node nc
= children
[j
];
603 // if not already solved
604 if (children_solved
.find(j
) != children_solved
.end())
608 TypeNode tnc
= nc
.getType();
609 int anyc_cons_num
= d_tds
->getAnyConstantConsNum(tnc
);
610 const Datatype
& cdt
=
611 static_cast<DatatypeType
>(tnc
.toType()).getDatatype();
612 std::vector
<Node
> exp_const
;
613 for (unsigned k
= 0, ncons
= cdt
.getNumConstructors(); k
< ncons
; k
++)
615 Kind nck
= d_tds
->getConsNumKind(tnc
, k
);
617 Node tester
= DatatypesRewriter::mkTester(nc
, k
, cdt
);
618 // check if the argument is redundant
619 if (static_cast<int>(k
) == anyc_cons_num
)
621 exp_const
.push_back(tester
);
623 else if (nck
!= UNDEFINED_KIND
)
625 Trace("sygus-sb-simple-debug") << " argument " << j
<< " " << k
626 << " is : " << nck
<< std::endl
;
627 red
= !d_ssb
.considerArgKind(tnc
, tn
, nck
, nk
, j
);
631 Node cc
= d_tds
->getConsNumConst(tnc
, k
);
634 Trace("sygus-sb-simple-debug")
635 << " argument " << j
<< " " << k
<< " is constant : " << cc
637 red
= !d_ssb
.considerConst(tnc
, tn
, cc
, nk
, j
);
638 if (usingAnyConstCons
)
640 // we only consider concrete constant constructors
641 // of children if we have the "any constant" constructor
642 // otherwise, we would disallow solutions for grammars
643 // like the following:
646 // where A allows all constants but is not using the
647 // any constant constructor.
648 exp_const
.push_back(tester
);
658 Trace("sygus-sb-simple-debug") << " ...redundant." << std::endl
;
659 sbp_conj
.push_back(tester
.negate());
662 if (exp_const
.empty())
664 exp_not_all_const_valid
= false;
668 Node ecn
= exp_const
.size() == 1 ? exp_const
[0]
669 : nm
->mkNode(OR
, exp_const
);
670 exp_not_all_const
.push_back(ecn
.negate());
673 // explicitly handle constants and "any constant" constructors
674 // if this type admits any constant, then at least one of my
675 // children must not be a constant or the "any constant" constructor
676 if (dt
.getSygusAllowConst() && exp_not_all_const_valid
)
678 Assert(!exp_not_all_const
.empty());
679 Node expaan
= exp_not_all_const
.size() == 1
680 ? exp_not_all_const
[0]
681 : nm
->mkNode(OR
, exp_not_all_const
);
682 Trace("sygus-sb-simple-debug")
683 << "Ensure not all constant: " << expaan
<< std::endl
;
684 sbp_conj
.push_back(expaan
);
694 // commutative operators
695 if (quantifiers::TermUtil::isComm(nk
) && children
.size() == 2
696 && children
[0].getType() == tn
&& children
[1].getType() == tn
)
699 Node child11
= nm
->mkNode(
700 APPLY_SELECTOR_TOTAL
,
701 Node::fromExpr(dt
[tindex
].getSelectorInternal(tn
.toType(), 1)),
703 Assert(child11
.getType() == children
[1].getType());
704 Node order_pred_trans
= nm
->mkNode(
706 DatatypesRewriter::mkTester(children
[0], tindex
, dt
).negate(),
707 getTermOrderPredicate(child11
, children
[1]));
708 sbp_conj
.push_back(order_pred_trans
);
714 if (!sbp_conj
.empty())
717 sbp_conj
.size() == 1 ? sbp_conj
[0] : nm
->mkNode(kind::AND
, sbp_conj
);
718 Trace("sygus-sb-simple")
719 << "Simple predicate for " << tn
<< " index " << tindex
<< " (" << nk
720 << ") at depth " << depth
<< " : " << std::endl
;
721 Trace("sygus-sb-simple") << " " << sb_pred
<< std::endl
;
722 sb_pred
= nm
->mkNode(
723 kind::OR
, DatatypesRewriter::mkTester(n
, tindex
, dt
).negate(), sb_pred
);
725 d_simple_sb_pred
[tn
][tindex
][usingSymCons
][depth
] = sb_pred
;
729 TNode
SygusSymBreakNew::getFreeVar( TypeNode tn
) {
730 return d_tds
->getFreeVar(tn
, 0);
733 void SygusSymBreakNew::registerSearchTerm( TypeNode tn
, unsigned d
, Node n
, bool topLevel
, std::vector
< Node
>& lemmas
) {
735 std::unordered_map
<Node
, Node
, NodeHashFunction
>::iterator ita
=
736 d_term_to_anchor
.find(n
);
737 Assert( ita
!= d_term_to_anchor
.end() );
738 Node a
= ita
->second
;
739 Assert( !a
.isNull() );
740 if( std::find( d_cache
[a
].d_search_terms
[tn
][d
].begin(), d_cache
[a
].d_search_terms
[tn
][d
].end(), n
)==d_cache
[a
].d_search_terms
[tn
][d
].end() ){
741 Trace("sygus-sb-debug") << " register search term : " << n
<< " at depth " << d
<< ", type=" << tn
<< ", tl=" << topLevel
<< std::endl
;
742 d_cache
[a
].d_search_terms
[tn
][d
].push_back( n
);
743 if( !options::sygusSymBreakLazy() ){
744 addSymBreakLemmasFor( tn
, n
, d
, lemmas
);
749 Node
SygusSymBreakNew::registerSearchValue(
750 Node a
, Node n
, Node nv
, unsigned d
, std::vector
<Node
>& lemmas
)
752 Assert(n
.getType().isComparableTo(nv
.getType()));
753 TypeNode tn
= n
.getType();
754 if (!tn
.isDatatype())
756 // don't register non-datatype terms, instead we return the
760 const Datatype
& dt
= ((DatatypeType
)tn
.toType()).getDatatype();
763 // don't register non-sygus-datatype terms
766 Assert(nv
.getKind() == APPLY_CONSTRUCTOR
);
767 NodeManager
* nm
= NodeManager::currentNM();
768 // we call the body of this function in a bottom-up fashion
769 // this ensures that the "abstraction" of the model value is available
770 if( nv
.getNumChildren()>0 ){
771 unsigned cindex
= DatatypesRewriter::indexOf(nv
.getOperator());
772 std::vector
<Node
> rcons_children
;
773 rcons_children
.push_back(nv
.getOperator());
774 bool childrenChanged
= false;
775 for (unsigned i
= 0, nchild
= nv
.getNumChildren(); i
< nchild
; i
++)
777 Node sel
= nm
->mkNode(
778 APPLY_SELECTOR_TOTAL
,
779 Node::fromExpr(dt
[cindex
].getSelectorInternal(tn
.toType(), i
)),
781 Node nvc
= registerSearchValue(a
, sel
, nv
[i
], d
+ 1, lemmas
);
786 rcons_children
.push_back(nvc
);
787 childrenChanged
= childrenChanged
|| nvc
!= nv
[i
];
789 // reconstruct the value, which may be a skeleton
792 nv
= nm
->mkNode(APPLY_CONSTRUCTOR
, rcons_children
);
795 Trace("sygus-sb-debug2") << "Registering search value " << n
<< " -> " << nv
<< std::endl
;
796 std::map
<TypeNode
, int> var_count
;
797 Node cnv
= d_tds
->canonizeBuiltin(nv
, var_count
);
798 Trace("sygus-sb-debug") << " ...canonized value is " << cnv
<< std::endl
;
799 // must do this for all nodes, regardless of top-level
800 if (d_cache
[a
].d_search_val_proc
.find(cnv
)
801 == d_cache
[a
].d_search_val_proc
.end())
803 d_cache
[a
].d_search_val_proc
.insert(cnv
);
804 // get the root (for PBE symmetry breaking)
805 Assert(d_anchor_to_conj
.find(a
) != d_anchor_to_conj
.end());
806 quantifiers::CegConjecture
* aconj
= d_anchor_to_conj
[a
];
807 Assert(aconj
!= NULL
);
808 Trace("sygus-sb-debug") << " ...register search value " << cnv
809 << ", type=" << tn
<< std::endl
;
810 Node bv
= d_tds
->sygusToBuiltin(cnv
, tn
);
811 Trace("sygus-sb-debug") << " ......builtin is " << bv
<< std::endl
;
812 Node bvr
= d_tds
->getExtRewriter()->extendedRewrite(bv
);
813 Trace("sygus-sb-debug") << " ......rewrites to " << bvr
<< std::endl
;
814 Trace("dt-sygus") << " * DT builtin : " << n
<< " -> " << bvr
<< std::endl
;
815 unsigned sz
= d_tds
->getSygusTermSize( nv
);
816 if( d_tds
->involvesDivByZero( bvr
) ){
817 quantifiers::DivByZeroSygusInvarianceTest dbzet
;
818 Trace("sygus-sb-mexp-debug") << "Minimize explanation for div-by-zero in "
820 registerSymBreakLemmaForValue(
821 a
, nv
, dbzet
, Node::null(), var_count
, lemmas
);
824 std::unordered_map
<Node
, Node
, NodeHashFunction
>::iterator itsv
=
825 d_cache
[a
].d_search_val
[tn
].find(bvr
);
827 bool by_examples
= false;
828 if( itsv
==d_cache
[a
].d_search_val
[tn
].end() ){
829 // TODO (github #1210) conjecture-specific symmetry breaking
830 // this should be generalized and encapsulated within the CegConjecture
832 // is it equivalent under examples?
834 if (options::sygusSymBreakPbe())
836 if (aconj
->getPbe()->hasExamples(a
))
838 bvr_equiv
= aconj
->getPbe()->addSearchVal(tn
, a
, bvr
);
841 if( !bvr_equiv
.isNull() ){
842 if( bvr_equiv
!=bvr
){
843 Trace("sygus-sb-debug") << "......adding search val for " << bvr
<< " returned " << bvr_equiv
<< std::endl
;
844 Assert( d_cache
[a
].d_search_val
[tn
].find( bvr_equiv
)!=d_cache
[a
].d_search_val
[tn
].end() );
845 Trace("sygus-sb-debug") << "......search value was " << d_cache
[a
].d_search_val
[tn
][bvr_equiv
] << std::endl
;
846 if( Trace
.isOn("sygus-sb-exc") ){
847 Node prev
= d_tds
->sygusToBuiltin( d_cache
[a
].d_search_val
[tn
][bvr_equiv
], tn
);
848 Trace("sygus-sb-exc") << " ......programs " << prev
<< " and " << bv
<< " are equivalent up to examples." << std::endl
;
850 bad_val_bvr
= bvr_equiv
;
854 //store rewritten values, regardless of whether it will be considered
855 d_cache
[a
].d_search_val
[tn
][bvr
] = nv
;
856 d_cache
[a
].d_search_val_sz
[tn
][bvr
] = sz
;
859 if( Trace
.isOn("sygus-sb-exc") ){
860 Node prev_bv
= d_tds
->sygusToBuiltin( itsv
->second
, tn
);
861 Trace("sygus-sb-exc") << " ......programs " << prev_bv
<< " and " << bv
<< " rewrite to " << bvr
<< "." << std::endl
;
865 if (options::sygusRewVerify())
867 // add to the sampler database object
868 std::map
<TypeNode
, quantifiers::SygusSampler
>::iterator its
=
869 d_sampler
[a
].find(tn
);
870 if (its
== d_sampler
[a
].end())
872 d_sampler
[a
][tn
].initializeSygus(
873 d_tds
, nv
, options::sygusSamples(), false);
874 its
= d_sampler
[a
].find(tn
);
877 // register the rewritten node with the sampler
878 Node bvr_sample_ret
= its
->second
.registerTerm(bvr
);
879 // register the current node with the sampler
880 Node sample_ret
= its
->second
.registerTerm(bv
);
882 // bv and bvr should be equivalent under examples
883 if (sample_ret
!= bvr_sample_ret
)
885 // we have detected unsoundness in the rewriter
886 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
887 std::ostream
* out
= nodeManagerOptions
.getOut();
888 (*out
) << "(unsound-rewrite " << bv
<< " " << bvr
<< ")" << std::endl
;
889 // debugging information
890 int pt_index
= its
->second
.getDiffSamplePointIndex(bv
, bvr
);
893 (*out
) << "; unsound: are not equivalent for : " << std::endl
;
894 std::vector
<Node
> vars
;
895 its
->second
.getVariables(vars
);
896 std::vector
<Node
> pt
;
897 its
->second
.getSamplePoint(pt_index
, pt
);
898 Assert(vars
.size() == pt
.size());
899 for (unsigned i
= 0, size
= pt
.size(); i
< size
; i
++)
901 (*out
) << "; unsound: " << vars
[i
] << " -> " << pt
[i
]
904 Node bv_e
= its
->second
.evaluate(bv
, pt_index
);
905 Node pbv_e
= its
->second
.evaluate(bvr
, pt_index
);
906 Assert(bv_e
!= pbv_e
);
907 (*out
) << "; unsound: where they evaluate to " << bv_e
<< " and "
908 << pbv_e
<< std::endl
;
912 // no witness point found?
915 if (options::sygusRewVerifyAbort())
919 "--sygus-rr-verify detected unsoundness in the rewriter!");
924 if( !bad_val_bvr
.isNull() ){
926 Node bad_val_o
= d_cache
[a
].d_search_val
[tn
][bad_val_bvr
];
927 Assert( d_cache
[a
].d_search_val_sz
[tn
].find( bad_val_bvr
)!=d_cache
[a
].d_search_val_sz
[tn
].end() );
928 unsigned prev_sz
= d_cache
[a
].d_search_val_sz
[tn
][bad_val_bvr
];
930 //swap : the excluded value is the previous
931 d_cache
[a
].d_search_val_sz
[tn
][bad_val_bvr
] = sz
;
932 bad_val
= d_cache
[a
].d_search_val
[tn
][bad_val_bvr
];
936 if( Trace
.isOn("sygus-sb-exc") ){
937 Node bad_val_bv
= d_tds
->sygusToBuiltin( bad_val
, tn
);
938 Trace("sygus-sb-exc") << " ........exclude : " << bad_val_bv
;
940 Trace("sygus-sb-exc") << " (by examples)";
942 Trace("sygus-sb-exc") << std::endl
;
944 Assert( d_tds
->getSygusTermSize( bad_val
)==sz
);
946 // generalize the explanation for why the analog of bad_val
947 // is equivalent to bvr
948 quantifiers::EquivSygusInvarianceTest eset
;
949 eset
.init(d_tds
, tn
, aconj
, a
, bvr
);
951 Trace("sygus-sb-mexp-debug") << "Minimize explanation for eval[" << d_tds
->sygusToBuiltin( bad_val
) << "] = " << bvr
<< std::endl
;
952 registerSymBreakLemmaForValue(
953 a
, bad_val
, eset
, bad_val_o
, var_count
, lemmas
);
955 // other generalization criteria go here
963 void SygusSymBreakNew::registerSymBreakLemmaForValue(
966 quantifiers::SygusInvarianceTest
& et
,
968 std::map
<TypeNode
, int>& var_count
,
969 std::vector
<Node
>& lemmas
)
971 TypeNode tn
= val
.getType();
972 Node x
= getFreeVar(tn
);
973 unsigned sz
= d_tds
->getSygusTermSize(val
);
974 std::vector
<Node
> exp
;
975 d_tds
->getExplain()->getExplanationFor(x
, val
, exp
, et
, valr
, var_count
, sz
);
977 exp
.size() == 1 ? exp
[0] : NodeManager::currentNM()->mkNode(AND
, exp
);
979 Trace("sygus-sb-exc") << " ........exc lemma is " << lem
<< ", size = " << sz
981 registerSymBreakLemma(tn
, lem
, sz
, a
, lemmas
);
984 void SygusSymBreakNew::registerSymBreakLemma( TypeNode tn
, Node lem
, unsigned sz
, Node a
, std::vector
< Node
>& lemmas
) {
985 // lem holds for all terms of type tn, and is applicable to terms of size sz
986 Trace("sygus-sb-debug") << " register sym break lemma : " << lem
988 Trace("sygus-sb-debug") << " anchor : " << a
<< std::endl
;
989 Trace("sygus-sb-debug") << " type : " << tn
<< std::endl
;
990 Trace("sygus-sb-debug") << " size : " << sz
<< std::endl
;
991 Assert( !a
.isNull() );
992 d_cache
[a
].d_sb_lemmas
[tn
][sz
].push_back( lem
);
993 TNode x
= getFreeVar( tn
);
994 unsigned csz
= getSearchSizeForAnchor( a
);
995 int max_depth
= ((int)csz
)-((int)sz
);
996 NodeManager
* nm
= NodeManager::currentNM();
997 for( int d
=0; d
<=max_depth
; d
++ ){
998 std::map
< unsigned, std::vector
< Node
> >::iterator itt
= d_cache
[a
].d_search_terms
[tn
].find( d
);
999 if( itt
!=d_cache
[a
].d_search_terms
[tn
].end() ){
1000 for (const TNode
& t
: itt
->second
)
1002 if (!options::sygusSymBreakLazy()
1003 || d_active_terms
.find(t
) != d_active_terms
.end())
1005 Node slem
= lem
.substitute(x
, t
);
1006 Node rlv
= getRelevancyCondition(t
);
1009 slem
= nm
->mkNode(OR
, rlv
, slem
);
1011 lemmas
.push_back(slem
);
1017 void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn
, Node t
, unsigned d
, std::vector
< Node
>& lemmas
) {
1018 Assert( d_term_to_anchor
.find( t
)!=d_term_to_anchor
.end() );
1019 Node a
= d_term_to_anchor
[t
];
1020 addSymBreakLemmasFor( tn
, t
, d
, a
, lemmas
);
1023 void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn
, Node t
, unsigned d
, Node a
, std::vector
< Node
>& lemmas
) {
1024 Assert( t
.getType()==tn
);
1025 Assert( !a
.isNull() );
1026 Trace("sygus-sb-debug2") << "add sym break lemmas for " << t
<< " " << d
1027 << " " << a
<< std::endl
;
1028 std::map
< TypeNode
, std::map
< unsigned, std::vector
< Node
> > >::iterator its
= d_cache
[a
].d_sb_lemmas
.find( tn
);
1029 Node rlv
= getRelevancyCondition(t
);
1030 NodeManager
* nm
= NodeManager::currentNM();
1031 if( its
!= d_cache
[a
].d_sb_lemmas
.end() ){
1032 TNode x
= getFreeVar( tn
);
1033 //get symmetry breaking lemmas for this term
1034 unsigned csz
= getSearchSizeForAnchor( a
);
1035 int max_sz
= ((int)csz
) - ((int)d
);
1036 Trace("sygus-sb-debug2")
1037 << "add lemmas up to size " << max_sz
<< ", which is (search_size) "
1038 << csz
<< " - (depth) " << d
<< std::endl
;
1039 std::unordered_map
<TNode
, TNode
, TNodeHashFunction
> cache
;
1040 for( std::map
< unsigned, std::vector
< Node
> >::iterator it
= its
->second
.begin(); it
!= its
->second
.end(); ++it
){
1041 if( (int)it
->first
<=max_sz
){
1042 for (const Node
& lem
: it
->second
)
1044 Node slem
= lem
.substitute(x
, t
, cache
);
1045 // add the relevancy condition for t
1048 slem
= nm
->mkNode(OR
, rlv
, slem
);
1050 lemmas
.push_back(slem
);
1055 Trace("sygus-sb-debug2") << "...finished." << std::endl
;
1058 void SygusSymBreakNew::preRegisterTerm( TNode n
, std::vector
< Node
>& lemmas
) {
1060 Trace("sygus-sb-debug") << "Pre-register variable : " << n
<< std::endl
;
1061 registerSizeTerm( n
, lemmas
);
1065 void SygusSymBreakNew::registerSizeTerm( Node e
, std::vector
< Node
>& lemmas
) {
1066 if( d_register_st
.find( e
)==d_register_st
.end() ){
1067 if( e
.getType().isDatatype() ){
1068 const Datatype
& dt
= ((DatatypeType
)(e
.getType()).toType()).getDatatype();
1070 if (d_tds
->isEnumerator(e
))
1072 d_register_st
[e
] = true;
1073 Node ag
= d_tds
->getActiveGuardForEnumerator(e
);
1075 d_anchor_to_active_guard
[e
] = ag
;
1076 std::map
<Node
, std::unique_ptr
<DecisionStrategy
>>::iterator itaas
=
1077 d_anchor_to_ag_strategy
.find(e
);
1078 if (itaas
== d_anchor_to_ag_strategy
.end())
1080 d_anchor_to_ag_strategy
[e
].reset(
1081 new DecisionStrategySingleton("sygus_enum_active",
1083 d_td
->getSatContext(),
1084 d_td
->getValuation()));
1086 d_td
->getDecisionManager()->registerStrategy(
1087 DecisionManager::STRAT_DT_SYGUS_ENUM_ACTIVE
,
1088 d_anchor_to_ag_strategy
[e
].get());
1092 // if it has an active guard (it is an enumerator), use itself as measure term. This will enforce fairness on it independently.
1095 // otherwise we enforce fairness in a unified way for all
1096 if( d_generic_measure_term
.isNull() ){
1097 // choose e as master for all future terms
1098 d_generic_measure_term
= e
;
1100 m
= d_generic_measure_term
;
1102 Trace("sygus-sb") << "Sygus : register size term : " << e
<< " with measure " << m
<< std::endl
;
1103 registerMeasureTerm( m
);
1104 d_szinfo
[m
]->d_anchors
.push_back( e
);
1105 d_anchor_to_measure_term
[e
] = m
;
1106 if( options::sygusFair()==SYGUS_FAIR_DT_SIZE
){
1107 // update constraints on the measure term
1108 if( options::sygusFairMax() ){
1109 Node ds
= NodeManager::currentNM()->mkNode(kind::DT_SIZE
, e
);
1110 Node slem
= NodeManager::currentNM()->mkNode(
1111 kind::LEQ
, ds
, d_szinfo
[m
]->getOrMkMeasureValue(lemmas
));
1112 lemmas
.push_back(slem
);
1114 Node mt
= d_szinfo
[m
]->getOrMkActiveMeasureValue(lemmas
);
1116 d_szinfo
[m
]->getOrMkActiveMeasureValue(lemmas
, true);
1117 Node ds
= NodeManager::currentNM()->mkNode(kind::DT_SIZE
, e
);
1118 lemmas
.push_back(mt
.eqNode(
1119 NodeManager::currentNM()->mkNode(kind::PLUS
, new_mt
, ds
)));
1123 // not sure if it is a size term or not (may be registered later?)
1126 d_register_st
[e
] = false;
1129 d_register_st
[e
] = false;
1134 void SygusSymBreakNew::registerMeasureTerm( Node m
) {
1135 std::map
<Node
, std::unique_ptr
<SygusSizeDecisionStrategy
>>::iterator it
=
1137 if( it
==d_szinfo
.end() ){
1138 Trace("sygus-sb") << "Sygus : register measure term : " << m
<< std::endl
;
1139 d_szinfo
[m
].reset(new SygusSizeDecisionStrategy(
1140 m
, d_td
->getSatContext(), d_td
->getValuation()));
1141 // register this as a decision strategy
1142 d_td
->getDecisionManager()->registerStrategy(
1143 DecisionManager::STRAT_DT_SYGUS_ENUM_SIZE
, d_szinfo
[m
].get());
1147 void SygusSymBreakNew::notifySearchSize( Node m
, unsigned s
, Node exp
, std::vector
< Node
>& lemmas
) {
1148 std::map
<Node
, std::unique_ptr
<SygusSizeDecisionStrategy
>>::iterator its
=
1150 Assert( its
!=d_szinfo
.end() );
1151 if( its
->second
->d_search_size
.find( s
)==its
->second
->d_search_size
.end() ){
1152 its
->second
->d_search_size
[s
] = true;
1153 its
->second
->d_search_size_exp
[s
] = exp
;
1154 Assert( s
==0 || its
->second
->d_search_size
.find( s
-1 )!=its
->second
->d_search_size
.end() );
1155 Trace("sygus-fair") << "SygusSymBreakNew:: now considering term measure : " << s
<< " for " << m
<< std::endl
;
1156 Assert( s
>=its
->second
->d_curr_search_size
);
1157 while( s
>its
->second
->d_curr_search_size
){
1158 incrementCurrentSearchSize( m
, lemmas
);
1160 Trace("sygus-fair") << "...finish increment for term measure : " << s
<< std::endl
;
1162 //re-add all testers (some may now be relevant) TODO
1163 for( IntMap::const_iterator it = d_testers.begin(); it != d_testers.end(); ++it ){
1164 Node n = (*it).first;
1165 NodeMap::const_iterator itx = d_testers_exp.find( n );
1166 if( itx!=d_testers_exp.end() ){
1167 int tindex = (*it).second;
1168 Node exp = (*itx).second;
1169 assertTester( tindex, n, exp, lemmas );
1178 unsigned SygusSymBreakNew::getSearchSizeFor( Node n
) {
1179 Trace("sygus-sb-debug2") << "get search size for term : " << n
<< std::endl
;
1180 std::unordered_map
<Node
, Node
, NodeHashFunction
>::iterator ita
=
1181 d_term_to_anchor
.find(n
);
1182 Assert( ita
!= d_term_to_anchor
.end() );
1183 return getSearchSizeForAnchor( ita
->second
);
1186 unsigned SygusSymBreakNew::getSearchSizeForAnchor( Node a
) {
1187 Trace("sygus-sb-debug2") << "get search size for anchor : " << a
<< std::endl
;
1188 std::map
< Node
, Node
>::iterator it
= d_anchor_to_measure_term
.find( a
);
1189 Assert( it
!=d_anchor_to_measure_term
.end() );
1190 return getSearchSizeForMeasureTerm(it
->second
);
1193 unsigned SygusSymBreakNew::getSearchSizeForMeasureTerm(Node m
)
1195 Trace("sygus-sb-debug2") << "get search size for measure : " << m
<< std::endl
;
1196 std::map
<Node
, std::unique_ptr
<SygusSizeDecisionStrategy
>>::iterator its
=
1198 Assert( its
!=d_szinfo
.end() );
1199 return its
->second
->d_curr_search_size
;
1202 void SygusSymBreakNew::incrementCurrentSearchSize( Node m
, std::vector
< Node
>& lemmas
) {
1203 std::map
<Node
, std::unique_ptr
<SygusSizeDecisionStrategy
>>::iterator itsz
=
1205 Assert( itsz
!=d_szinfo
.end() );
1206 itsz
->second
->d_curr_search_size
++;
1207 Trace("sygus-fair") << " register search size " << itsz
->second
->d_curr_search_size
<< " for " << m
<< std::endl
;
1208 NodeManager
* nm
= NodeManager::currentNM();
1209 for( std::map
< Node
, SearchCache
>::iterator itc
= d_cache
.begin(); itc
!= d_cache
.end(); ++itc
){
1210 Node a
= itc
->first
;
1211 Trace("sygus-fair-debug") << " look at anchor " << a
<< "..." << std::endl
;
1212 // check whether a is bounded by m
1213 Assert( d_anchor_to_measure_term
.find( a
)!=d_anchor_to_measure_term
.end() );
1214 if( d_anchor_to_measure_term
[a
]==m
){
1215 for( std::map
< TypeNode
, std::map
< unsigned, std::vector
< Node
> > >::iterator its
= itc
->second
.d_sb_lemmas
.begin();
1216 its
!= itc
->second
.d_sb_lemmas
.end(); ++its
){
1217 TypeNode tn
= its
->first
;
1218 TNode x
= getFreeVar( tn
);
1219 for( std::map
< unsigned, std::vector
< Node
> >::iterator it
= its
->second
.begin(); it
!= its
->second
.end(); ++it
){
1220 unsigned sz
= it
->first
;
1221 int new_depth
= ((int)itsz
->second
->d_curr_search_size
) - ((int)sz
);
1222 std::map
< unsigned, std::vector
< Node
> >::iterator itt
= itc
->second
.d_search_terms
[tn
].find( new_depth
);
1223 if( itt
!=itc
->second
.d_search_terms
[tn
].end() ){
1224 for (const TNode
& t
: itt
->second
)
1226 if (!options::sygusSymBreakLazy()
1227 || d_active_terms
.find(t
) != d_active_terms
.end()
1228 && !it
->second
.empty())
1230 Node rlv
= getRelevancyCondition(t
);
1231 std::unordered_map
<TNode
, TNode
, TNodeHashFunction
> cache
;
1232 for (const Node
& lem
: it
->second
)
1234 Node slem
= lem
.substitute(x
, t
, cache
);
1235 slem
= nm
->mkNode(OR
, rlv
, slem
);
1236 lemmas
.push_back(slem
);
1247 void SygusSymBreakNew::check( std::vector
< Node
>& lemmas
) {
1248 Trace("sygus-sb") << "SygusSymBreakNew::check" << std::endl
;
1250 // check for externally registered symmetry breaking lemmas
1251 std::vector
<Node
> anchors
;
1252 if (d_tds
->hasSymBreakLemmas(anchors
))
1254 for (const Node
& a
: anchors
)
1256 // is this a registered enumerator?
1257 if (d_register_st
.find(a
) != d_register_st
.end())
1259 // symmetry breaking lemmas should only be for enumerators
1260 Assert(d_register_st
[a
]);
1261 std::vector
<Node
> sbl
;
1262 d_tds
->getSymBreakLemmas(a
, sbl
);
1263 for (const Node
& lem
: sbl
)
1265 TypeNode tn
= d_tds
->getTypeForSymBreakLemma(lem
);
1266 unsigned sz
= d_tds
->getSizeForSymBreakLemma(lem
);
1267 registerSymBreakLemma(tn
, lem
, sz
, a
, lemmas
);
1269 d_tds
->clearSymBreakLemmas(a
);
1272 if (!lemmas
.empty())
1278 // register search values, add symmetry breaking lemmas if applicable
1279 for( std::map
< Node
, bool >::iterator it
= d_register_st
.begin(); it
!= d_register_st
.end(); ++it
){
1281 Node prog
= it
->first
;
1282 Trace("dt-sygus-debug") << "Checking model value of " << prog
<< "..."
1284 Assert(prog
.getType().isDatatype());
1285 Node progv
= d_td
->getValuation().getModel()->getValue( prog
);
1286 if (Trace
.isOn("dt-sygus"))
1288 Trace("dt-sygus") << "* DT model : " << prog
<< " -> ";
1289 std::stringstream ss
;
1290 Printer::getPrinter(options::outputLanguage())
1291 ->toStreamSygus(ss
, progv
);
1292 Trace("dt-sygus") << ss
.str() << std::endl
;
1294 // TODO : remove this step (ensure there is no way a sygus term cannot be assigned a tester before this point)
1295 if (!checkTesters(prog
, progv
, 0, lemmas
))
1297 Trace("sygus-sb") << " SygusSymBreakNew::check: ...WARNING: considered missing split for " << prog
<< "." << std::endl
;
1298 // this should not happen generally, it is caused by a sygus term not being assigned a tester
1301 //debugging : ensure fairness was properly handled
1302 if( options::sygusFair()==SYGUS_FAIR_DT_SIZE
){
1303 Node prog_sz
= NodeManager::currentNM()->mkNode( kind::DT_SIZE
, prog
);
1304 Node prog_szv
= d_td
->getValuation().getModel()->getValue( prog_sz
);
1305 Node progv_sz
= NodeManager::currentNM()->mkNode( kind::DT_SIZE
, progv
);
1307 Trace("sygus-sb") << " Mv[" << prog
<< "] = " << progv
<< ", size = " << prog_szv
<< std::endl
;
1308 if( prog_szv
.getConst
<Rational
>().getNumerator().toUnsignedInt() > getSearchSizeForAnchor( prog
) ){
1309 AlwaysAssert( false );
1310 Node szlem
= NodeManager::currentNM()->mkNode( kind::OR
, prog
.eqNode( progv
).negate(),
1311 prog_sz
.eqNode( progv_sz
) );
1312 Trace("sygus-sb-warn") << "SygusSymBreak : WARNING : adding size correction : " << szlem
<< std::endl
;
1313 lemmas
.push_back( szlem
);
1318 // register the search value ( prog -> progv ), this may invoke symmetry breaking
1319 if( options::sygusSymBreakDynamic() ){
1320 Node rsv
= registerSearchValue(prog
, prog
, progv
, 0, lemmas
);
1323 Trace("sygus-sb") << " SygusSymBreakNew::check: ...added new symmetry breaking lemma for " << prog
<< "." << std::endl
;
1327 Trace("dt-sygus") << " ...success." << std::endl
;
1333 //register any measured terms that we haven't encountered yet (should only be invoked on first call to check
1334 Trace("sygus-sb") << "Register size terms..." << std::endl
;
1335 std::vector
< Node
> mts
;
1336 d_tds
->getEnumerators(mts
);
1337 for( unsigned i
=0; i
<mts
.size(); i
++ ){
1338 registerSizeTerm( mts
[i
], lemmas
);
1340 Trace("sygus-sb") << " SygusSymBreakNew::check: finished." << std::endl
;
1342 if( Trace
.isOn("cegqi-engine") ){
1343 if (lemmas
.empty() && !d_szinfo
.empty())
1345 Trace("cegqi-engine") << "*** Sygus : passed datatypes check. term size(s) : ";
1346 for (std::pair
<const Node
, std::unique_ptr
<SygusSizeDecisionStrategy
>>&
1349 SygusSizeDecisionStrategy
* s
= p
.second
.get();
1350 Trace("cegqi-engine") << s
->d_curr_search_size
<< " ";
1352 Trace("cegqi-engine") << std::endl
;
1357 bool SygusSymBreakNew::checkTesters(Node n
,
1360 std::vector
<Node
>& lemmas
)
1362 if (vn
.getKind() != kind::APPLY_CONSTRUCTOR
)
1364 // all datatype terms should be constant here
1365 Assert(!vn
.getType().isDatatype());
1368 if( Trace
.isOn("sygus-sb-warn") ){
1369 Node prog_sz
= NodeManager::currentNM()->mkNode( kind::DT_SIZE
, n
);
1370 Node prog_szv
= d_td
->getValuation().getModel()->getValue( prog_sz
);
1371 for( int i
=0; i
<ind
; i
++ ){
1372 Trace("sygus-sb-warn") << " ";
1374 Trace("sygus-sb-warn") << n
<< " : " << vn
<< " : " << prog_szv
<< std::endl
;
1376 TypeNode tn
= n
.getType();
1377 const Datatype
& dt
= ((DatatypeType
)tn
.toType()).getDatatype();
1378 int cindex
= DatatypesRewriter::indexOf(vn
.getOperator());
1379 Node tst
= DatatypesRewriter::mkTester( n
, cindex
, dt
);
1380 bool hastst
= d_td
->getEqualityEngine()->hasTerm(tst
);
1384 tstrep
= d_td
->getEqualityEngine()->getRepresentative(tst
);
1386 if (!hastst
|| tstrep
!= d_true
)
1388 Trace("sygus-sb-warn") << "- has tester : " << tst
<< " : " << ( hastst
? "true" : "false" );
1389 Trace("sygus-sb-warn") << ", value=" << tstrep
<< std::endl
;
1391 Node split
= DatatypesRewriter::mkSplit(n
, dt
);
1392 Assert( !split
.isNull() );
1393 lemmas
.push_back( split
);
1397 for( unsigned i
=0; i
<vn
.getNumChildren(); i
++ ){
1398 Node sel
= NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL
, Node::fromExpr( dt
[cindex
].getSelectorInternal( tn
.toType(), i
) ), n
);
1399 if (!checkTesters(sel
, vn
[i
], ind
+ 1, lemmas
))
1407 Node
SygusSymBreakNew::getCurrentTemplate( Node n
, std::map
< TypeNode
, int >& var_count
) {
1408 if( d_active_terms
.find( n
)!=d_active_terms
.end() ){
1409 TypeNode tn
= n
.getType();
1410 IntMap::const_iterator it
= d_testers
.find( n
);
1411 Assert( it
!= d_testers
.end() );
1412 const Datatype
& dt
= ((DatatypeType
)tn
.toType()).getDatatype();
1413 int tindex
= (*it
).second
;
1414 Assert( tindex
>=0 );
1415 Assert( tindex
<(int)dt
.getNumConstructors() );
1416 std::vector
< Node
> children
;
1417 children
.push_back( Node::fromExpr( dt
[tindex
].getConstructor() ) );
1418 for( unsigned i
=0; i
<dt
[tindex
].getNumArgs(); i
++ ){
1419 Node sel
= NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL
, Node::fromExpr( dt
[tindex
].getSelectorInternal( tn
.toType(), i
) ), n
);
1420 Node cc
= getCurrentTemplate( sel
, var_count
);
1421 children
.push_back( cc
);
1423 return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR
, children
);
1425 return d_tds
->getFreeVarInc( n
.getType(), var_count
);
1429 Node
SygusSymBreakNew::SygusSizeDecisionStrategy::getOrMkMeasureValue(
1430 std::vector
<Node
>& lemmas
)
1432 if (d_measure_value
.isNull())
1434 d_measure_value
= NodeManager::currentNM()->mkSkolem(
1435 "mt", NodeManager::currentNM()->integerType());
1436 lemmas
.push_back(NodeManager::currentNM()->mkNode(
1439 NodeManager::currentNM()->mkConst(Rational(0))));
1441 return d_measure_value
;
1444 Node
SygusSymBreakNew::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue(
1445 std::vector
<Node
>& lemmas
, bool mkNew
)
1449 Node new_mt
= NodeManager::currentNM()->mkSkolem(
1450 "mt", NodeManager::currentNM()->integerType());
1451 lemmas
.push_back(NodeManager::currentNM()->mkNode(
1452 kind::GEQ
, new_mt
, NodeManager::currentNM()->mkConst(Rational(0))));
1453 d_measure_value_active
= new_mt
;
1455 else if (d_measure_value_active
.isNull())
1457 d_measure_value_active
= getOrMkMeasureValue(lemmas
);
1459 return d_measure_value_active
;
1462 Node
SygusSymBreakNew::SygusSizeDecisionStrategy::mkLiteral(unsigned s
)
1464 if (options::sygusFair() == SYGUS_FAIR_NONE
)
1466 return Node::null();
1468 if (options::sygusAbortSize() != -1
1469 && static_cast<int>(s
) > options::sygusAbortSize())
1471 std::stringstream ss
;
1472 ss
<< "Maximum term size (" << options::sygusAbortSize()
1473 << ") for enumerative SyGuS exceeded.";
1474 throw LogicException(ss
.str());
1476 Assert(!d_this
.isNull());
1477 NodeManager
* nm
= NodeManager::currentNM();
1478 return nm
->mkNode(DT_SYGUS_BOUND
, d_this
, nm
->mkConst(Rational(s
)));
1481 int SygusSymBreakNew::getGuardStatus( Node g
) {
1483 if( d_td
->getValuation().hasSatValue( g
, value
) ) {