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-2017 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 quantifiers::TermDbSygus
* tds
,
46 d_zero
= NodeManager::currentNM()->mkConst(Rational(0));
49 SygusSymBreakNew::~SygusSymBreakNew() {
50 for( std::map
< Node
, SearchSizeInfo
* >::iterator it
= d_szinfo
.begin(); it
!= d_szinfo
.end(); ++it
){
56 void SygusSymBreakNew::assertTester( int tindex
, TNode n
, Node exp
, std::vector
< Node
>& lemmas
) {
57 registerTerm( n
, lemmas
);
58 // check if this is a relevant (sygus) term
59 if( d_term_to_anchor
.find( n
)!=d_term_to_anchor
.end() ){
60 Trace("sygus-sb-debug2") << "Sygus : process tester : " << exp
<< std::endl
;
61 // if not already active (may have duplicate calls for the same tester)
62 if( d_active_terms
.find( n
)==d_active_terms
.end() ) {
63 d_testers
[n
] = tindex
;
64 d_testers_exp
[n
] = exp
;
66 // check if parent is active
68 if( options::sygusSymBreakLazy() ){
69 if( n
.getKind()==kind::APPLY_SELECTOR_TOTAL
){
70 NodeSet::const_iterator it
= d_active_terms
.find( n
[0] );
71 if( it
==d_active_terms
.end() ){
74 //this must be a proper selector
75 IntMap::const_iterator itt
= d_testers
.find( n
[0] );
76 Assert( itt
!=d_testers
.end() );
77 int ptindex
= (*itt
).second
;
78 TypeNode ptn
= n
[0].getType();
79 const Datatype
& pdt
= ((DatatypeType
)ptn
.toType()).getDatatype();
80 int sindex_in_parent
= pdt
[ptindex
].getSelectorIndexInternal( n
.getOperator().toExpr() );
81 // the tester is irrelevant in this branch
82 if( sindex_in_parent
==-1 ){
89 assertTesterInternal( tindex
, n
, exp
, lemmas
);
91 Trace("sygus-sb-debug2") << "...ignore inactive tester : " << exp
<< std::endl
;
94 Trace("sygus-sb-debug2") << "...ignore repeated tester : " << exp
<< std::endl
;
97 Trace("sygus-sb-debug2") << "...ignore non-sygus tester : " << exp
<< std::endl
;
101 void SygusSymBreakNew::assertFact( Node n
, bool polarity
, std::vector
< Node
>& lemmas
) {
102 if (n
.getKind() == kind::DT_SYGUS_BOUND
)
105 Trace("sygus-fair") << "Have sygus bound : " << n
<< ", polarity=" << polarity
<< " on measure " << m
<< std::endl
;
106 registerMeasureTerm( m
);
107 if( options::sygusFair()==SYGUS_FAIR_DT_SIZE
){
108 std::map
< Node
, SearchSizeInfo
* >::iterator its
= d_szinfo
.find( m
);
109 Assert( its
!=d_szinfo
.end() );
110 Node mt
= its
->second
->getOrMkMeasureValue(lemmas
);
111 //it relates the measure term to arithmetic
112 Node blem
= n
.eqNode( NodeManager::currentNM()->mkNode( kind::LEQ
, mt
, n
[1] ) );
113 lemmas
.push_back( blem
);
116 unsigned s
= n
[1].getConst
<Rational
>().getNumerator().toUnsignedInt();
117 notifySearchSize( m
, s
, n
, lemmas
);
119 }else if( n
.getKind() == kind::DT_HEIGHT_BOUND
|| n
.getKind()==DT_SIZE_BOUND
){
120 //reduce to arithmetic TODO ?
125 Node
SygusSymBreakNew::getTermOrderPredicate( Node n1
, Node n2
) {
126 NodeManager
* nm
= NodeManager::currentNM();
127 std::vector
< Node
> comm_disj
;
128 // (1) size of left is greater than size of right
130 nm
->mkNode(GT
, nm
->mkNode(DT_SIZE
, n1
), nm
->mkNode(DT_SIZE
, n2
));
131 comm_disj
.push_back( sz_less
);
132 // (2) ...or sizes are equal and first child is less by term order
133 std::vector
<Node
> sz_eq_cases
;
135 nm
->mkNode(EQUAL
, nm
->mkNode(DT_SIZE
, n1
), nm
->mkNode(DT_SIZE
, n2
));
136 sz_eq_cases
.push_back( sz_eq
);
137 if( options::sygusOpt1() ){
138 TypeNode tnc
= n1
.getType();
139 const Datatype
& cdt
= ((DatatypeType
)(tnc
).toType()).getDatatype();
140 for( unsigned j
=0; j
<cdt
.getNumConstructors(); j
++ ){
141 std::vector
<Node
> case_conj
;
142 for (unsigned k
= 0; k
< j
; k
++)
144 case_conj
.push_back(DatatypesRewriter::mkTester(n2
, k
, cdt
).negate());
146 if (!case_conj
.empty())
148 Node corder
= nm
->mkNode(
150 DatatypesRewriter::mkTester(n1
, j
, cdt
).negate(),
151 case_conj
.size() == 1 ? case_conj
[0]
152 : nm
->mkNode(kind::AND
, case_conj
));
153 sz_eq_cases
.push_back(corder
);
157 Node sz_eqc
= sz_eq_cases
.size() == 1 ? sz_eq_cases
[0]
158 : nm
->mkNode(kind::AND
, sz_eq_cases
);
159 comm_disj
.push_back( sz_eqc
);
161 return nm
->mkNode(kind::OR
, comm_disj
);
164 void SygusSymBreakNew::registerTerm( Node n
, std::vector
< Node
>& lemmas
) {
165 if( d_is_top_level
.find( n
)==d_is_top_level
.end() ){
166 d_is_top_level
[n
] = false;
167 TypeNode tn
= n
.getType();
169 bool is_top_level
= false;
170 bool success
= false;
171 if( n
.getKind()==kind::APPLY_SELECTOR_TOTAL
){
172 registerTerm( n
[0], lemmas
);
173 std::unordered_map
<Node
, Node
, NodeHashFunction
>::iterator it
=
174 d_term_to_anchor
.find(n
[0]);
175 if( it
!=d_term_to_anchor
.end() ) {
176 d_term_to_anchor
[n
] = it
->second
;
177 unsigned sel_weight
=
178 d_tds
->getSelectorWeight(n
[0].getType(), n
.getOperator());
179 d
= d_term_to_depth
[n
[0]] + sel_weight
;
180 is_top_level
= computeTopLevel( tn
, n
[0] );
183 }else if( n
.isVar() ){
184 registerSizeTerm( n
, lemmas
);
185 if( d_register_st
[n
] ){
186 d_term_to_anchor
[n
] = n
;
187 d_anchor_to_conj
[n
] = d_tds
->getConjectureForEnumerator(n
);
188 // this assertion fails if we have a sygus term in the search that is unmeasured
189 Assert(d_anchor_to_conj
[n
] != NULL
);
196 Trace("sygus-sb-debug") << "Register : " << n
<< ", depth : " << d
<< ", top level = " << is_top_level
<< ", type = " << ((DatatypeType
)tn
.toType()).getDatatype().getName() << std::endl
;
197 d_term_to_depth
[n
] = d
;
198 d_is_top_level
[n
] = is_top_level
;
199 registerSearchTerm( tn
, d
, n
, is_top_level
, lemmas
);
201 Trace("sygus-sb-debug2") << "Term " << n
<< " is not part of sygus search." << std::endl
;
206 bool SygusSymBreakNew::computeTopLevel( TypeNode tn
, Node n
){
207 if( n
.getType()==tn
){
209 }else if( n
.getKind()==kind::APPLY_SELECTOR_TOTAL
){
210 return computeTopLevel( tn
, n
[0] );
216 void SygusSymBreakNew::assertTesterInternal( int tindex
, TNode n
, Node exp
, std::vector
< Node
>& lemmas
) {
217 d_active_terms
.insert( n
);
218 Trace("sygus-sb-debug2") << "Sygus : activate term : " << n
<< " : " << exp
<< std::endl
;
220 TypeNode ntn
= n
.getType();
221 const Datatype
& dt
= ((DatatypeType
)ntn
.toType()).getDatatype();
223 // get the search size for this
224 Assert( d_term_to_anchor
.find( n
)!=d_term_to_anchor
.end() );
225 Node a
= d_term_to_anchor
[n
];
226 Assert( d_anchor_to_measure_term
.find( a
)!=d_anchor_to_measure_term
.end() );
227 Node m
= d_anchor_to_measure_term
[a
];
228 std::map
< Node
, SearchSizeInfo
* >::iterator itsz
= d_szinfo
.find( m
);
229 Assert( itsz
!=d_szinfo
.end() );
230 unsigned ssz
= itsz
->second
->d_curr_search_size
;
232 if( options::sygusFair()==SYGUS_FAIR_DIRECT
){
233 if( dt
[tindex
].getNumArgs()>0 ){
234 // consider lower bounds for size of types
235 unsigned lb_add
= d_tds
->getMinConsTermSize( ntn
, tindex
);
236 unsigned lb_rem
= n
==a
? 0 : d_tds
->getMinTermSize( ntn
);
237 Assert( lb_add
>=lb_rem
);
238 d_currTermSize
[a
].set( d_currTermSize
[a
].get() + ( lb_add
- lb_rem
) );
240 if( (unsigned)d_currTermSize
[a
].get()>ssz
){
241 if( Trace
.isOn("sygus-sb-fair") ){
242 std::map
< TypeNode
, int > var_count
;
243 Node templ
= getCurrentTemplate( a
, var_count
);
244 Trace("sygus-sb-fair") << "FAIRNESS : we have " << d_currTermSize
[a
].get() << " at search size " << ssz
<< ", template is " << templ
<< std::endl
;
247 std::vector
< Node
> conflict
;
248 for( NodeSet::const_iterator its
= d_active_terms
.begin(); its
!= d_active_terms
.end(); ++its
){
250 Node xa
= d_term_to_anchor
[x
];
252 IntMap::const_iterator ittv
= d_testers
.find( x
);
253 Assert( ittv
!= d_testers
.end() );
254 int tindex
= (*ittv
).second
;
255 const Datatype
& dti
= ((DatatypeType
)x
.getType().toType()).getDatatype();
256 if( dti
[tindex
].getNumArgs()>0 ){
257 NodeMap::const_iterator itt
= d_testers_exp
.find( x
);
258 Assert( itt
!= d_testers_exp
.end() );
259 conflict
.push_back( (*itt
).second
);
263 Assert( conflict
.size()==(unsigned)d_currTermSize
[a
].get() );
264 Assert( itsz
->second
->d_search_size_exp
.find( ssz
)!=itsz
->second
->d_search_size_exp
.end() );
265 conflict
.push_back( itsz
->second
->d_search_size_exp
[ssz
] );
266 Node conf
= NodeManager::currentNM()->mkNode( kind::AND
, conflict
);
267 Trace("sygus-sb-fair") << "Conflict is : " << conf
<< std::endl
;
268 lemmas
.push_back( conf
.negate() );
273 // now, add all applicable symmetry breaking lemmas for this term
274 Assert( d_term_to_depth
.find( n
)!=d_term_to_depth
.end() );
275 unsigned d
= d_term_to_depth
[n
];
276 Trace("sygus-sb-fair-debug") << "Tester " << exp
<< " is for depth " << d
<< " term in search size " << ssz
<< std::endl
;
278 if( options::sygusSymBreakLazy() ){
279 // dynamic symmetry breaking
280 addSymBreakLemmasFor( ntn
, n
, d
, lemmas
);
283 unsigned max_depth
= ssz
>=d
? ssz
-d
: 0;
284 unsigned min_depth
= d_simple_proc
[exp
];
285 if( min_depth
<=max_depth
){
286 TNode x
= getFreeVar( ntn
);
287 std::vector
<Node
> sb_lemmas
;
288 for (unsigned ds
= 0; ds
<= max_depth
; ds
++)
290 // static conjecture-independent symmetry breaking
291 Node ipred
= getSimpleSymBreakPred(ntn
, tindex
, ds
);
294 sb_lemmas
.push_back(ipred
);
296 // static conjecture-dependent symmetry breaking
297 std::map
<Node
, quantifiers::CegConjecture
*>::iterator itc
=
298 d_anchor_to_conj
.find(a
);
299 if (itc
!= d_anchor_to_conj
.end())
301 quantifiers::CegConjecture
* conj
= itc
->second
;
302 Assert(conj
!= NULL
);
303 Node dpred
= conj
->getSymmetryBreakingPredicate(x
, a
, ntn
, tindex
, ds
);
306 sb_lemmas
.push_back(dpred
);
311 // add the above symmetry breaking predicates to lemmas
312 Node rlv
= getRelevancyCondition(n
);
313 for (unsigned i
= 0; i
< sb_lemmas
.size(); i
++)
315 Node pred
= sb_lemmas
[i
].substitute(x
, n
);
318 pred
= NodeManager::currentNM()->mkNode(kind::OR
, rlv
.negate(), pred
);
320 lemmas
.push_back(pred
);
323 d_simple_proc
[exp
] = max_depth
+ 1;
325 // now activate the children those testers were previously asserted in this
326 // context and are awaiting activation, if they exist.
327 if( options::sygusSymBreakLazy() ){
328 for( unsigned j
=0; j
<dt
[tindex
].getNumArgs(); j
++ ){
329 Node sel
= NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL
, Node::fromExpr( dt
[tindex
].getSelectorInternal( ntn
.toType(), j
) ), n
);
330 Trace("sygus-sb-debug2") << " activate child sel : " << sel
<< std::endl
;
331 Assert( d_active_terms
.find( sel
)==d_active_terms
.end() );
332 IntMap::const_iterator itt
= d_testers
.find( sel
);
333 if( itt
!= d_testers
.end() ){
334 Assert( d_testers_exp
.find( sel
) != d_testers_exp
.end() );
335 assertTesterInternal( (*itt
).second
, sel
, d_testers_exp
[sel
], lemmas
);
341 Node
SygusSymBreakNew::getRelevancyCondition( Node n
) {
342 std::map
< Node
, Node
>::iterator itr
= d_rlv_cond
.find( n
);
343 if( itr
==d_rlv_cond
.end() ){
345 if( n
.getKind()==APPLY_SELECTOR_TOTAL
&& options::sygusSymBreakRlv() ){
346 TypeNode ntn
= n
[0].getType();
347 Type nt
= ntn
.toType();
348 const Datatype
& dt
= ((DatatypeType
)nt
).getDatatype();
349 Expr selExpr
= n
.getOperator().toExpr();
350 if( options::dtSharedSelectors() ){
351 std::vector
< Node
> disj
;
353 for( unsigned i
=0; i
<dt
.getNumConstructors(); i
++ ){
354 int sindexi
= dt
[i
].getSelectorIndexInternal(selExpr
);
357 disj
.push_back(DatatypesRewriter::mkTester(n
[0], i
, dt
));
364 Assert( !disj
.empty() );
366 cond
= disj
.size()==1 ? disj
[0] : NodeManager::currentNM()->mkNode( kind::OR
, disj
);
369 int sindex
= Datatype::cindexOf( selExpr
);
370 Assert( sindex
!=-1 );
371 cond
= DatatypesRewriter::mkTester( n
[0], sindex
, dt
);
373 Node c1
= getRelevancyCondition( n
[0] );
376 }else if( !c1
.isNull() ){
377 cond
= NodeManager::currentNM()->mkNode( kind::AND
, cond
, c1
);
380 Trace("sygus-sb-debug2") << "Relevancy condition for " << n
<< " is " << cond
<< std::endl
;
381 d_rlv_cond
[n
] = cond
;
388 Node
SygusSymBreakNew::getSimpleSymBreakPred( TypeNode tn
, int tindex
, unsigned depth
) {
389 std::map
< unsigned, Node
>::iterator it
= d_simple_sb_pred
[tn
][tindex
].find( depth
);
390 if( it
==d_simple_sb_pred
[tn
][tindex
].end() ){
391 Node n
= getFreeVar( tn
);
392 const Datatype
& dt
= ((DatatypeType
)(tn
).toType()).getDatatype();
393 Assert( tindex
>=0 && tindex
<(int)dt
.getNumConstructors() );
394 //conjunctive conclusion of lemma
395 std::vector
< Node
> sbp_conj
;
399 if( options::sygusFair()==SYGUS_FAIR_DT_SIZE
){
400 Node szl
= NodeManager::currentNM()->mkNode( DT_SIZE
, n
);
401 Node szr
= NodeManager::currentNM()->mkNode( DT_SIZE
, DatatypesRewriter::getInstCons( n
, dt
, tindex
) );
402 szr
= Rewriter::rewrite( szr
);
403 sbp_conj
.push_back( szl
.eqNode( szr
) );
404 //sbp_conj.push_back( NodeManager::currentNM()->mkNode( kind::GEQ, szl, NodeManager::currentNM()->mkConst( Rational(0) ) ) );
409 Kind nk
= d_tds
->getConsNumKind( tn
, tindex
);
410 if( options::sygusSymBreak() ){
411 // if less than the maximum depth we consider
414 std::vector
< Node
> children
;
415 for( unsigned j
=0; j
<dt
[tindex
].getNumArgs(); j
++ ){
416 Node sel
= NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL
, Node::fromExpr( dt
[tindex
].getSelectorInternal( tn
.toType(), j
) ), n
);
417 Assert( sel
.getType().isDatatype() );
418 Assert( ((DatatypeType
)sel
.getType().toType()).getDatatype().isSygus() );
419 children
.push_back( sel
);
420 d_tds
->registerSygusType( sel
.getType() );
423 TypeNode tnb
= TypeNode::fromType( dt
.getSygusType() );
425 // direct solving for children
426 // for instance, we may want to insist that the LHS of MINUS is 0
427 std::map
< unsigned, unsigned > children_solved
;
428 for( unsigned j
=0; j
<dt
[tindex
].getNumArgs(); j
++ ){
429 int i
= d_tds
->solveForArgument( tn
, tindex
, j
);
431 children_solved
[j
] = i
;
432 TypeNode ctn
= children
[j
].getType();
433 const Datatype
& cdt
= ((DatatypeType
)(ctn
).toType()).getDatatype();
434 Assert( i
<(int)cdt
.getNumConstructors() );
435 sbp_conj
.push_back( DatatypesRewriter::mkTester( children
[j
], i
, cdt
) );
439 // depth 1 symmetry breaking : talks about direct children
441 if( nk
!=UNDEFINED_KIND
){
442 // commutative operators
443 if( quantifiers::TermUtil::isComm( nk
) ){
444 if( children
.size()==2 ){
445 if( children
[0].getType()==children
[1].getType() ){
446 Node order_pred
= getTermOrderPredicate( children
[0], children
[1] );
447 sbp_conj
.push_back( order_pred
);
451 // operators whose arguments are non-additive (e.g. should be different)
452 std::vector
< unsigned > deq_child
[2];
453 if( children
.size()==2 && children
[0].getType()==tn
){
455 if( quantifiers::TermUtil::isNonAdditive( nk
) ){
458 //other cases of rewriting x k x -> x'
460 if( nk
==GT
|| nk
==LT
|| nk
==XOR
|| nk
==MINUS
|| nk
==BITVECTOR_SUB
|| nk
==BITVECTOR_XOR
|| nk
==BITVECTOR_UREM_TOTAL
){
461 //must have the zero element
462 req_const
= quantifiers::TermUtil::mkTypeValue(tnb
, 0);
463 }else if( nk
==EQUAL
|| nk
==LEQ
|| nk
==GEQ
|| nk
==BITVECTOR_XNOR
){
464 req_const
= quantifiers::TermUtil::mkTypeMaxValue(tnb
);
466 // cannot do division since we have to consider when both are zero
467 if( !req_const
.isNull() ){
468 if( d_tds
->hasConst( tn
, req_const
) ){
474 deq_child
[0].push_back( 0 );deq_child
[1].push_back( 1 );
477 if( nk
==ITE
|| nk
==STRING_STRREPL
){
478 deq_child
[0].push_back( 1 );deq_child
[1].push_back( 2 );
480 if( nk
==STRING_STRREPL
){
481 deq_child
[0].push_back( 0 );deq_child
[1].push_back( 1 );
483 for( unsigned i
=0; i
<deq_child
[0].size(); i
++ ){
484 unsigned c1
= deq_child
[0][i
];
485 unsigned c2
= deq_child
[1][i
];
486 if( children
[c1
].getType()==children
[c2
].getType() ){
487 if( !children
[c1
].getType().getCardinality().isOne() ){
488 sbp_conj
.push_back( children
[c1
].eqNode( children
[c2
] ).negate() );
494 // division by zero TODO ?
495 if( nk==DIVISION || nk==DIVISION_TOTAL || nk==INTS_DIVISION || nk==INTS_DIVISION_TOTAL ||
496 nk==INTS_MODULUS || nk==INTS_MODULUS_TOTAL ){
497 Assert( children.size()==2 );
498 // do not consider non-constant denominators ?
499 sbp_conj.push_back( NodeManager::currentNM()->mkNode( kind::DT_SYGUS_IS_CONST, children[1] ) );
500 // do not consider zero denominator
501 Node tzero = d_tds->getTypeValue( tnb, 0 );
502 int zero_arg = d_tds->getConstConsNum( children[1].getType(), tzero );
506 // semantic skolem for zero?
508 }else if( nk==BITVECTOR_UDIV_TOTAL || nk==BITVECTOR_UDIV || nk==BITVECTOR_SDIV || nk==BITVECTOR_UREM || nk==BITVECTOR_UREM_TOTAL ){
513 Trace("sygus-sb-simple-debug") << "Process arguments for " << tn
<< " : " << nk
<< " : " << std::endl
;
514 // singular arguments (e.g. 0 for mult)
515 // redundant arguments (e.g. 0 for plus, 1 for mult)
516 // right-associativity
518 for( unsigned j
=0; j
<dt
[tindex
].getNumArgs(); j
++ ){
519 Node nc
= children
[j
];
520 // if not already solved
521 if( children_solved
.find( j
)==children_solved
.end() ){
522 TypeNode tnc
= nc
.getType();
523 const Datatype
& cdt
= ((DatatypeType
)(tnc
).toType()).getDatatype();
524 for( unsigned k
=0; k
<cdt
.getNumConstructors(); k
++ ){
525 Kind nck
= d_tds
->getConsNumKind(tnc
, k
);
527 // check if the argument is redundant
528 if (nck
!= UNDEFINED_KIND
)
530 Trace("sygus-sb-simple-debug")
531 << " argument " << j
<< " " << k
<< " is : " << nck
533 red
= !d_tds
->considerArgKind(tnc
, tn
, nck
, nk
, j
);
537 Node cc
= d_tds
->getConsNumConst(tnc
, k
);
540 Trace("sygus-sb-simple-debug")
541 << " argument " << j
<< " " << k
542 << " is constant : " << cc
<< std::endl
;
543 red
= !d_tds
->considerConst(tnc
, tn
, cc
, nk
, j
);
550 Trace("sygus-sb-simple-debug")
551 << " ...redundant." << std::endl
;
553 DatatypesRewriter::mkTester(nc
, k
, cdt
).negate());
561 }else if( depth
==2 ){
562 if( nk
!=UNDEFINED_KIND
){
563 // commutative operators
564 if( quantifiers::TermUtil::isComm( nk
) ){
565 if( children
.size()==2 ){
566 if( children
[0].getType()==children
[1].getType() ){
568 // TODO : this is depth 2
569 if( children
[0].getType()==tn
){
570 Node child11
= NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL
, Node::fromExpr( dt
[tindex
].getSelectorInternal( tn
.toType(), 1 ) ), children
[0] );
571 Assert( child11
.getType()==children
[1].getType() );
572 Node order_pred_trans
= NodeManager::currentNM()->mkNode( OR
, DatatypesRewriter::mkTester( children
[0], tindex
, dt
).negate(),
573 getTermOrderPredicate( child11
, children
[1] ) );
575 sbp_conj
.push_back( order_pred_trans
);
586 if( !sbp_conj
.empty() ){
587 sb_pred
= sbp_conj
.size()==1 ? sbp_conj
[0] : NodeManager::currentNM()->mkNode( kind::AND
, sbp_conj
);
588 Trace("sygus-sb-simple") << "Simple predicate for " << tn
<< " index " << tindex
<< " (" << nk
<< ") at depth " << depth
<< " : " << std::endl
;
589 Trace("sygus-sb-simple") << " " << sb_pred
<< std::endl
;
590 sb_pred
= NodeManager::currentNM()->mkNode( kind::OR
, DatatypesRewriter::mkTester( n
, tindex
, dt
).negate(), sb_pred
);
592 d_simple_sb_pred
[tn
][tindex
][depth
] = sb_pred
;
599 TNode
SygusSymBreakNew::getFreeVar( TypeNode tn
) {
600 return d_tds
->getFreeVar(tn
, 0);
603 void SygusSymBreakNew::registerSearchTerm( TypeNode tn
, unsigned d
, Node n
, bool topLevel
, std::vector
< Node
>& lemmas
) {
605 std::unordered_map
<Node
, Node
, NodeHashFunction
>::iterator ita
=
606 d_term_to_anchor
.find(n
);
607 Assert( ita
!= d_term_to_anchor
.end() );
608 Node a
= ita
->second
;
609 Assert( !a
.isNull() );
610 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() ){
611 Trace("sygus-sb-debug") << " register search term : " << n
<< " at depth " << d
<< ", type=" << tn
<< ", tl=" << topLevel
<< std::endl
;
612 d_cache
[a
].d_search_terms
[tn
][d
].push_back( n
);
613 if( !options::sygusSymBreakLazy() ){
614 addSymBreakLemmasFor( tn
, n
, d
, lemmas
);
619 bool SygusSymBreakNew::registerSearchValue( Node a
, Node n
, Node nv
, unsigned d
, std::vector
< Node
>& lemmas
) {
620 Assert( n
.getType()==nv
.getType() );
621 Assert( nv
.getKind()==APPLY_CONSTRUCTOR
);
622 TypeNode tn
= n
.getType();
623 // currently bottom-up, could be top-down?
624 if( nv
.getNumChildren()>0 ){
625 const Datatype
& dt
= ((DatatypeType
)tn
.toType()).getDatatype();
626 unsigned cindex
= Datatype::indexOf( nv
.getOperator().toExpr() );
627 for( unsigned i
=0; i
<nv
.getNumChildren(); i
++ ){
628 Node sel
= NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL
, Node::fromExpr( dt
[cindex
].getSelectorInternal( tn
.toType(), i
) ), n
);
629 if( !registerSearchValue( a
, sel
, nv
[i
], d
+1, lemmas
) ){
634 Trace("sygus-sb-debug2") << "Registering search value " << n
<< " -> " << nv
<< std::endl
;
635 // must do this for all nodes, regardless of top-level
636 if( d_cache
[a
].d_search_val_proc
.find( nv
)==d_cache
[a
].d_search_val_proc
.end() ){
637 d_cache
[a
].d_search_val_proc
.insert(nv
);
638 // get the root (for PBE symmetry breaking)
639 Assert(d_anchor_to_conj
.find(a
) != d_anchor_to_conj
.end());
640 quantifiers::CegConjecture
* aconj
= d_anchor_to_conj
[a
];
641 Assert(aconj
!= NULL
);
642 Trace("sygus-sb-debug") << " ...register search value " << nv
<< ", type=" << tn
<< std::endl
;
643 Node bv
= d_tds
->sygusToBuiltin( nv
, tn
);
644 Trace("sygus-sb-debug") << " ......builtin is " << bv
<< std::endl
;
645 Node bvr
= d_tds
->getExtRewriter()->extendedRewrite(bv
);
646 Trace("sygus-sb-debug") << " ......rewrites to " << bvr
<< std::endl
;
647 Trace("dt-sygus") << " * DT builtin : " << n
<< " -> " << bvr
<< std::endl
;
648 unsigned sz
= d_tds
->getSygusTermSize( nv
);
649 if( d_tds
->involvesDivByZero( bvr
) ){
650 quantifiers::DivByZeroSygusInvarianceTest dbzet
;
651 Trace("sygus-sb-mexp-debug") << "Minimize explanation for div-by-zero in " << d_tds
->sygusToBuiltin( nv
) << std::endl
;
652 registerSymBreakLemmaForValue(a
, nv
, dbzet
, Node::null(), lemmas
);
655 std::unordered_map
<Node
, Node
, NodeHashFunction
>::iterator itsv
=
656 d_cache
[a
].d_search_val
[tn
].find(bvr
);
658 bool by_examples
= false;
659 if( itsv
==d_cache
[a
].d_search_val
[tn
].end() ){
660 // TODO (github #1210) conjecture-specific symmetry breaking
661 // this should be generalized and encapsulated within the CegConjecture
663 // is it equivalent under examples?
665 if (options::sygusSymBreakPbe())
667 if (aconj
->getPbe()->hasExamples(a
))
669 bvr_equiv
= aconj
->getPbe()->addSearchVal(tn
, a
, bvr
);
672 if( !bvr_equiv
.isNull() ){
673 if( bvr_equiv
!=bvr
){
674 Trace("sygus-sb-debug") << "......adding search val for " << bvr
<< " returned " << bvr_equiv
<< std::endl
;
675 Assert( d_cache
[a
].d_search_val
[tn
].find( bvr_equiv
)!=d_cache
[a
].d_search_val
[tn
].end() );
676 Trace("sygus-sb-debug") << "......search value was " << d_cache
[a
].d_search_val
[tn
][bvr_equiv
] << std::endl
;
677 if( Trace
.isOn("sygus-sb-exc") ){
678 Node prev
= d_tds
->sygusToBuiltin( d_cache
[a
].d_search_val
[tn
][bvr_equiv
], tn
);
679 Trace("sygus-sb-exc") << " ......programs " << prev
<< " and " << bv
<< " are equivalent up to examples." << std::endl
;
681 bad_val_bvr
= bvr_equiv
;
685 //store rewritten values, regardless of whether it will be considered
686 d_cache
[a
].d_search_val
[tn
][bvr
] = nv
;
687 d_cache
[a
].d_search_val_sz
[tn
][bvr
] = sz
;
690 if( Trace
.isOn("sygus-sb-exc") ){
691 Node prev_bv
= d_tds
->sygusToBuiltin( itsv
->second
, tn
);
692 Trace("sygus-sb-exc") << " ......programs " << prev_bv
<< " and " << bv
<< " rewrite to " << bvr
<< "." << std::endl
;
696 if (options::sygusRewVerify())
698 // add to the sampler database object
699 std::map
<TypeNode
, quantifiers::SygusSampler
>::iterator its
=
700 d_sampler
[a
].find(tn
);
701 if (its
== d_sampler
[a
].end())
703 d_sampler
[a
][tn
].initializeSygus(
704 d_tds
, nv
, options::sygusSamples(), false);
705 its
= d_sampler
[a
].find(tn
);
708 // register the rewritten node with the sampler
709 Node bvr_sample_ret
= its
->second
.registerTerm(bvr
);
710 // register the current node with the sampler
711 Node sample_ret
= its
->second
.registerTerm(bv
);
713 // bv and bvr should be equivalent under examples
714 if (sample_ret
!= bvr_sample_ret
)
716 // we have detected unsoundness in the rewriter
717 Options
& nodeManagerOptions
= NodeManager::currentNM()->getOptions();
718 std::ostream
* out
= nodeManagerOptions
.getOut();
719 (*out
) << "(unsound-rewrite " << bv
<< " " << bvr
<< ")" << std::endl
;
720 // debugging information
721 if (Trace
.isOn("sygus-rr-debug"))
723 int pt_index
= its
->second
.getDiffSamplePointIndex(bv
, bvr
);
726 Trace("sygus-rr-debug")
727 << "; unsound: are not equivalent for : " << std::endl
;
728 std::vector
<Node
> vars
;
729 std::vector
<Node
> pt
;
730 its
->second
.getSamplePoint(pt_index
, vars
, pt
);
731 Assert(vars
.size() == pt
.size());
732 for (unsigned i
= 0, size
= pt
.size(); i
< size
; i
++)
734 Trace("sygus-rr-debug") << "; unsound: " << vars
[i
] << " -> "
735 << pt
[i
] << std::endl
;
737 Node bv_e
= its
->second
.evaluate(bv
, pt_index
);
738 Node pbv_e
= its
->second
.evaluate(bvr
, pt_index
);
739 Assert(bv_e
!= pbv_e
);
740 Trace("sygus-rr-debug") << "; unsound: where they evaluate to "
741 << bv_e
<< " and " << pbv_e
<< std::endl
;
745 // no witness point found?
749 if (options::sygusRewVerifyAbort())
753 "--sygus-rr-verify detected unsoundness in the rewriter!");
758 if( !bad_val_bvr
.isNull() ){
760 Node bad_val_o
= d_cache
[a
].d_search_val
[tn
][bad_val_bvr
];
761 Assert( d_cache
[a
].d_search_val_sz
[tn
].find( bad_val_bvr
)!=d_cache
[a
].d_search_val_sz
[tn
].end() );
762 unsigned prev_sz
= d_cache
[a
].d_search_val_sz
[tn
][bad_val_bvr
];
764 //swap : the excluded value is the previous
765 d_cache
[a
].d_search_val_sz
[tn
][bad_val_bvr
] = sz
;
766 bad_val
= d_cache
[a
].d_search_val
[tn
][bad_val_bvr
];
770 if( Trace
.isOn("sygus-sb-exc") ){
771 Node bad_val_bv
= d_tds
->sygusToBuiltin( bad_val
, tn
);
772 Trace("sygus-sb-exc") << " ........exclude : " << bad_val_bv
;
774 Trace("sygus-sb-exc") << " (by examples)";
776 Trace("sygus-sb-exc") << std::endl
;
778 Assert( d_tds
->getSygusTermSize( bad_val
)==sz
);
780 Node x
= getFreeVar( tn
);
782 // do analysis of the evaluation FIXME: does not work (evaluation is non-constant)
783 quantifiers::EquivSygusInvarianceTest eset
;
784 eset
.init(d_tds
, tn
, aconj
, a
, bvr
);
786 Trace("sygus-sb-mexp-debug") << "Minimize explanation for eval[" << d_tds
->sygusToBuiltin( bad_val
) << "] = " << bvr
<< std::endl
;
787 registerSymBreakLemmaForValue(a
, bad_val
, eset
, bad_val_o
, lemmas
);
795 void SygusSymBreakNew::registerSymBreakLemmaForValue(
798 quantifiers::SygusInvarianceTest
& et
,
800 std::vector
<Node
>& lemmas
)
802 TypeNode tn
= val
.getType();
803 Node x
= getFreeVar(tn
);
804 unsigned sz
= d_tds
->getSygusTermSize(val
);
805 std::vector
<Node
> exp
;
806 d_tds
->getExplain()->getExplanationFor(x
, val
, exp
, et
, valr
, sz
);
808 exp
.size() == 1 ? exp
[0] : NodeManager::currentNM()->mkNode(AND
, exp
);
810 Trace("sygus-sb-exc") << " ........exc lemma is " << lem
<< ", size = " << sz
812 registerSymBreakLemma(tn
, lem
, sz
, a
, lemmas
);
815 void SygusSymBreakNew::registerSymBreakLemma( TypeNode tn
, Node lem
, unsigned sz
, Node a
, std::vector
< Node
>& lemmas
) {
816 // lem holds for all terms of type tn, and is applicable to terms of size sz
817 Trace("sygus-sb-debug") << " register sym break lemma : " << lem
819 Trace("sygus-sb-debug") << " anchor : " << a
<< std::endl
;
820 Trace("sygus-sb-debug") << " type : " << tn
<< std::endl
;
821 Trace("sygus-sb-debug") << " size : " << sz
<< std::endl
;
822 Assert( !a
.isNull() );
823 d_cache
[a
].d_sb_lemmas
[tn
][sz
].push_back( lem
);
824 TNode x
= getFreeVar( tn
);
825 unsigned csz
= getSearchSizeForAnchor( a
);
826 int max_depth
= ((int)csz
)-((int)sz
);
827 for( int d
=0; d
<=max_depth
; d
++ ){
828 std::map
< unsigned, std::vector
< Node
> >::iterator itt
= d_cache
[a
].d_search_terms
[tn
].find( d
);
829 if( itt
!=d_cache
[a
].d_search_terms
[tn
].end() ){
830 for( unsigned k
=0; k
<itt
->second
.size(); k
++ ){
831 TNode t
= itt
->second
[k
];
832 if( !options::sygusSymBreakLazy() || d_active_terms
.find( t
)!=d_active_terms
.end() ){
833 addSymBreakLemma(lem
, x
, t
, lemmas
);
839 void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn
, Node t
, unsigned d
, std::vector
< Node
>& lemmas
) {
840 Assert( d_term_to_anchor
.find( t
)!=d_term_to_anchor
.end() );
841 Node a
= d_term_to_anchor
[t
];
842 addSymBreakLemmasFor( tn
, t
, d
, a
, lemmas
);
845 void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn
, Node t
, unsigned d
, Node a
, std::vector
< Node
>& lemmas
) {
846 Assert( t
.getType()==tn
);
847 Assert( !a
.isNull() );
848 std::map
< TypeNode
, std::map
< unsigned, std::vector
< Node
> > >::iterator its
= d_cache
[a
].d_sb_lemmas
.find( tn
);
849 if( its
!= d_cache
[a
].d_sb_lemmas
.end() ){
850 TNode x
= getFreeVar( tn
);
851 //get symmetry breaking lemmas for this term
852 unsigned csz
= getSearchSizeForAnchor( a
);
853 int max_sz
= ((int)csz
) - ((int)d
);
854 for( std::map
< unsigned, std::vector
< Node
> >::iterator it
= its
->second
.begin(); it
!= its
->second
.end(); ++it
){
855 if( (int)it
->first
<=max_sz
){
856 for( unsigned k
=0; k
<it
->second
.size(); k
++ ){
857 Node lem
= it
->second
[k
];
858 addSymBreakLemma(lem
, x
, t
, lemmas
);
865 void SygusSymBreakNew::addSymBreakLemma(Node lem
,
868 std::vector
<Node
>& lemmas
)
870 Assert( !options::sygusSymBreakLazy() || d_active_terms
.find( n
)!=d_active_terms
.end() );
872 Node slem
= lem
.substitute( x
, n
);
873 Trace("sygus-sb-exc-debug") << "SymBreak lemma : " << slem
<< std::endl
;
874 Node rlv
= getRelevancyCondition( n
);
876 slem
= NodeManager::currentNM()->mkNode( kind::OR
, rlv
.negate(), slem
);
878 lemmas
.push_back( slem
);
881 void SygusSymBreakNew::preRegisterTerm( TNode n
, std::vector
< Node
>& lemmas
) {
883 Trace("sygus-sb-debug") << "Pre-register variable : " << n
<< std::endl
;
884 registerSizeTerm( n
, lemmas
);
888 void SygusSymBreakNew::registerSizeTerm( Node e
, std::vector
< Node
>& lemmas
) {
889 if( d_register_st
.find( e
)==d_register_st
.end() ){
890 if( e
.getType().isDatatype() ){
891 const Datatype
& dt
= ((DatatypeType
)(e
.getType()).toType()).getDatatype();
893 if (d_tds
->isEnumerator(e
))
895 d_register_st
[e
] = true;
896 Node ag
= d_tds
->getActiveGuardForEnumerator(e
);
898 d_anchor_to_active_guard
[e
] = ag
;
902 // if it has an active guard (it is an enumerator), use itself as measure term. This will enforce fairness on it independently.
905 // otherwise we enforce fairness in a unified way for all
906 if( d_generic_measure_term
.isNull() ){
907 // choose e as master for all future terms
908 d_generic_measure_term
= e
;
910 m
= d_generic_measure_term
;
912 Trace("sygus-sb") << "Sygus : register size term : " << e
<< " with measure " << m
<< std::endl
;
913 registerMeasureTerm( m
);
914 d_szinfo
[m
]->d_anchors
.push_back( e
);
915 d_anchor_to_measure_term
[e
] = m
;
916 if( options::sygusFair()==SYGUS_FAIR_DT_SIZE
){
917 // update constraints on the measure term
918 if( options::sygusFairMax() ){
919 Node ds
= NodeManager::currentNM()->mkNode(kind::DT_SIZE
, e
);
920 Node slem
= NodeManager::currentNM()->mkNode(
921 kind::LEQ
, ds
, d_szinfo
[m
]->getOrMkMeasureValue(lemmas
));
922 lemmas
.push_back(slem
);
924 Node mt
= d_szinfo
[m
]->getOrMkActiveMeasureValue(lemmas
);
926 d_szinfo
[m
]->getOrMkActiveMeasureValue(lemmas
, true);
927 Node ds
= NodeManager::currentNM()->mkNode(kind::DT_SIZE
, e
);
928 lemmas
.push_back(mt
.eqNode(
929 NodeManager::currentNM()->mkNode(kind::PLUS
, new_mt
, ds
)));
933 // not sure if it is a size term or not (may be registered later?)
936 d_register_st
[e
] = false;
939 d_register_st
[e
] = false;
944 void SygusSymBreakNew::registerMeasureTerm( Node m
) {
945 std::map
< Node
, SearchSizeInfo
* >::iterator it
= d_szinfo
.find( m
);
946 if( it
==d_szinfo
.end() ){
947 Trace("sygus-sb") << "Sygus : register measure term : " << m
<< std::endl
;
948 d_szinfo
[m
] = new SearchSizeInfo( m
, d_td
->getSatContext() );
952 void SygusSymBreakNew::notifySearchSize( Node m
, unsigned s
, Node exp
, std::vector
< Node
>& lemmas
) {
953 std::map
< Node
, SearchSizeInfo
* >::iterator its
= d_szinfo
.find( m
);
954 Assert( its
!=d_szinfo
.end() );
955 if( its
->second
->d_search_size
.find( s
)==its
->second
->d_search_size
.end() ){
956 its
->second
->d_search_size
[s
] = true;
957 its
->second
->d_search_size_exp
[s
] = exp
;
958 Assert( s
==0 || its
->second
->d_search_size
.find( s
-1 )!=its
->second
->d_search_size
.end() );
959 Trace("sygus-fair") << "SygusSymBreakNew:: now considering term measure : " << s
<< " for " << m
<< std::endl
;
960 Assert( s
>=its
->second
->d_curr_search_size
);
961 while( s
>its
->second
->d_curr_search_size
){
962 incrementCurrentSearchSize( m
, lemmas
);
964 Trace("sygus-fair") << "...finish increment for term measure : " << s
<< std::endl
;
966 //re-add all testers (some may now be relevant) TODO
967 for( IntMap::const_iterator it = d_testers.begin(); it != d_testers.end(); ++it ){
968 Node n = (*it).first;
969 NodeMap::const_iterator itx = d_testers_exp.find( n );
970 if( itx!=d_testers_exp.end() ){
971 int tindex = (*it).second;
972 Node exp = (*itx).second;
973 assertTester( tindex, n, exp, lemmas );
982 unsigned SygusSymBreakNew::getSearchSizeFor( Node n
) {
983 Trace("sygus-sb-debug2") << "get search size for term : " << n
<< std::endl
;
984 std::unordered_map
<Node
, Node
, NodeHashFunction
>::iterator ita
=
985 d_term_to_anchor
.find(n
);
986 Assert( ita
!= d_term_to_anchor
.end() );
987 return getSearchSizeForAnchor( ita
->second
);
990 unsigned SygusSymBreakNew::getSearchSizeForAnchor( Node a
) {
991 Trace("sygus-sb-debug2") << "get search size for anchor : " << a
<< std::endl
;
992 std::map
< Node
, Node
>::iterator it
= d_anchor_to_measure_term
.find( a
);
993 Assert( it
!=d_anchor_to_measure_term
.end() );
994 return getSearchSizeForMeasureTerm(it
->second
);
997 unsigned SygusSymBreakNew::getSearchSizeForMeasureTerm(Node m
)
999 Trace("sygus-sb-debug2") << "get search size for measure : " << m
<< std::endl
;
1000 std::map
< Node
, SearchSizeInfo
* >::iterator its
= d_szinfo
.find( m
);
1001 Assert( its
!=d_szinfo
.end() );
1002 return its
->second
->d_curr_search_size
;
1005 void SygusSymBreakNew::incrementCurrentSearchSize( Node m
, std::vector
< Node
>& lemmas
) {
1006 std::map
< Node
, SearchSizeInfo
* >::iterator itsz
= d_szinfo
.find( m
);
1007 Assert( itsz
!=d_szinfo
.end() );
1008 itsz
->second
->d_curr_search_size
++;
1009 Trace("sygus-fair") << " register search size " << itsz
->second
->d_curr_search_size
<< " for " << m
<< std::endl
;
1010 for( std::map
< Node
, SearchCache
>::iterator itc
= d_cache
.begin(); itc
!= d_cache
.end(); ++itc
){
1011 Node a
= itc
->first
;
1012 Trace("sygus-fair-debug") << " look at anchor " << a
<< "..." << std::endl
;
1013 // check whether a is bounded by m
1014 Assert( d_anchor_to_measure_term
.find( a
)!=d_anchor_to_measure_term
.end() );
1015 if( d_anchor_to_measure_term
[a
]==m
){
1016 for( std::map
< TypeNode
, std::map
< unsigned, std::vector
< Node
> > >::iterator its
= itc
->second
.d_sb_lemmas
.begin();
1017 its
!= itc
->second
.d_sb_lemmas
.end(); ++its
){
1018 TypeNode tn
= its
->first
;
1019 TNode x
= getFreeVar( tn
);
1020 for( std::map
< unsigned, std::vector
< Node
> >::iterator it
= its
->second
.begin(); it
!= its
->second
.end(); ++it
){
1021 unsigned sz
= it
->first
;
1022 int new_depth
= ((int)itsz
->second
->d_curr_search_size
) - ((int)sz
);
1023 std::map
< unsigned, std::vector
< Node
> >::iterator itt
= itc
->second
.d_search_terms
[tn
].find( new_depth
);
1024 if( itt
!=itc
->second
.d_search_terms
[tn
].end() ){
1025 for( unsigned k
=0; k
<itt
->second
.size(); k
++ ){
1026 TNode t
= itt
->second
[k
];
1027 if( !options::sygusSymBreakLazy() || d_active_terms
.find( t
)!=d_active_terms
.end() ){
1028 for( unsigned j
=0; j
<it
->second
.size(); j
++ ){
1029 Node lem
= it
->second
[j
];
1030 addSymBreakLemma(lem
, x
, t
, lemmas
);
1041 void SygusSymBreakNew::check( std::vector
< Node
>& lemmas
) {
1042 Trace("sygus-sb") << "SygusSymBreakNew::check" << std::endl
;
1044 // check for externally registered symmetry breaking lemmas
1045 std::vector
<Node
> anchors
;
1046 if (d_tds
->hasSymBreakLemmas(anchors
))
1048 for (const Node
& a
: anchors
)
1050 std::vector
<Node
> sbl
;
1051 d_tds
->getSymBreakLemmas(a
, sbl
);
1052 for (const Node
& lem
: sbl
)
1054 TypeNode tn
= d_tds
->getTypeForSymBreakLemma(lem
);
1055 unsigned sz
= d_tds
->getSizeForSymBreakLemma(lem
);
1056 registerSymBreakLemma(tn
, lem
, sz
, a
, lemmas
);
1059 d_tds
->clearSymBreakLemmas();
1060 if (!lemmas
.empty())
1066 // register search values, add symmetry breaking lemmas if applicable
1067 for( std::map
< Node
, bool >::iterator it
= d_register_st
.begin(); it
!= d_register_st
.end(); ++it
){
1069 Node prog
= it
->first
;
1070 Node progv
= d_td
->getValuation().getModel()->getValue( prog
);
1071 if (Trace
.isOn("dt-sygus"))
1073 Trace("dt-sygus") << "* DT model : " << prog
<< " -> ";
1074 std::stringstream ss
;
1075 Printer::getPrinter(options::outputLanguage())
1076 ->toStreamSygus(ss
, progv
);
1077 Trace("dt-sygus") << ss
.str() << std::endl
;
1079 // TODO : remove this step (ensure there is no way a sygus term cannot be assigned a tester before this point)
1080 if (!checkTesters(prog
, progv
, 0, lemmas
))
1082 Trace("sygus-sb") << " SygusSymBreakNew::check: ...WARNING: considered missing split for " << prog
<< "." << std::endl
;
1083 // this should not happen generally, it is caused by a sygus term not being assigned a tester
1086 //debugging : ensure fairness was properly handled
1087 if( options::sygusFair()==SYGUS_FAIR_DT_SIZE
){
1088 Node prog_sz
= NodeManager::currentNM()->mkNode( kind::DT_SIZE
, prog
);
1089 Node prog_szv
= d_td
->getValuation().getModel()->getValue( prog_sz
);
1090 Node progv_sz
= NodeManager::currentNM()->mkNode( kind::DT_SIZE
, progv
);
1092 Trace("sygus-sb") << " Mv[" << prog
<< "] = " << progv
<< ", size = " << prog_szv
<< std::endl
;
1093 if( prog_szv
.getConst
<Rational
>().getNumerator().toUnsignedInt() > getSearchSizeForAnchor( prog
) ){
1094 AlwaysAssert( false );
1095 Node szlem
= NodeManager::currentNM()->mkNode( kind::OR
, prog
.eqNode( progv
).negate(),
1096 prog_sz
.eqNode( progv_sz
) );
1097 Trace("sygus-sb-warn") << "SygusSymBreak : WARNING : adding size correction : " << szlem
<< std::endl
;
1098 lemmas
.push_back( szlem
);
1103 // register the search value ( prog -> progv ), this may invoke symmetry breaking
1104 if( options::sygusSymBreakDynamic() ){
1105 if( !registerSearchValue( prog
, prog
, progv
, 0, lemmas
) ){
1106 Trace("sygus-sb") << " SygusSymBreakNew::check: ...added new symmetry breaking lemma for " << prog
<< "." << std::endl
;
1110 Trace("dt-sygus") << " ...success." << std::endl
;
1116 //register any measured terms that we haven't encountered yet (should only be invoked on first call to check
1117 std::vector
< Node
> mts
;
1118 d_tds
->getEnumerators(mts
);
1119 for( unsigned i
=0; i
<mts
.size(); i
++ ){
1120 registerSizeTerm( mts
[i
], lemmas
);
1122 Trace("sygus-sb") << " SygusSymBreakNew::check: finished." << std::endl
;
1124 if( Trace
.isOn("cegqi-engine") ){
1125 if( lemmas
.empty() ){
1126 Trace("cegqi-engine") << "*** Sygus : passed datatypes check. term size(s) : ";
1127 for( std::map
< Node
, SearchSizeInfo
* >::iterator it
= d_szinfo
.begin(); it
!= d_szinfo
.end(); ++it
){
1128 SearchSizeInfo
* s
= it
->second
;
1129 Trace("cegqi-engine") << s
->d_curr_search_size
<< " ";
1131 Trace("cegqi-engine") << std::endl
;
1136 bool SygusSymBreakNew::checkTesters(Node n
,
1139 std::vector
<Node
>& lemmas
)
1141 Assert( vn
.getKind()==kind::APPLY_CONSTRUCTOR
);
1142 if( Trace
.isOn("sygus-sb-warn") ){
1143 Node prog_sz
= NodeManager::currentNM()->mkNode( kind::DT_SIZE
, n
);
1144 Node prog_szv
= d_td
->getValuation().getModel()->getValue( prog_sz
);
1145 for( int i
=0; i
<ind
; i
++ ){
1146 Trace("sygus-sb-warn") << " ";
1148 Trace("sygus-sb-warn") << n
<< " : " << vn
<< " : " << prog_szv
<< std::endl
;
1150 TypeNode tn
= n
.getType();
1151 const Datatype
& dt
= ((DatatypeType
)tn
.toType()).getDatatype();
1152 int cindex
= Datatype::indexOf( vn
.getOperator().toExpr() );
1153 Node tst
= DatatypesRewriter::mkTester( n
, cindex
, dt
);
1154 bool hastst
= d_td
->getValuation().getModel()->hasTerm( tst
);
1155 Node tstrep
= d_td
->getValuation().getModel()->getRepresentative( tst
);
1156 if( !hastst
|| tstrep
!=NodeManager::currentNM()->mkConst( true ) ){
1157 Trace("sygus-sb-warn") << "- has tester : " << tst
<< " : " << ( hastst
? "true" : "false" );
1158 Trace("sygus-sb-warn") << ", value=" << tstrep
<< std::endl
;
1160 Node split
= DatatypesRewriter::mkSplit(n
, dt
);
1161 Assert( !split
.isNull() );
1162 lemmas
.push_back( split
);
1166 for( unsigned i
=0; i
<vn
.getNumChildren(); i
++ ){
1167 Node sel
= NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL
, Node::fromExpr( dt
[cindex
].getSelectorInternal( tn
.toType(), i
) ), n
);
1168 if (!checkTesters(sel
, vn
[i
], ind
+ 1, lemmas
))
1176 Node
SygusSymBreakNew::getCurrentTemplate( Node n
, std::map
< TypeNode
, int >& var_count
) {
1177 if( d_active_terms
.find( n
)!=d_active_terms
.end() ){
1178 TypeNode tn
= n
.getType();
1179 IntMap::const_iterator it
= d_testers
.find( n
);
1180 Assert( it
!= d_testers
.end() );
1181 const Datatype
& dt
= ((DatatypeType
)tn
.toType()).getDatatype();
1182 int tindex
= (*it
).second
;
1183 Assert( tindex
>=0 );
1184 Assert( tindex
<(int)dt
.getNumConstructors() );
1185 std::vector
< Node
> children
;
1186 children
.push_back( Node::fromExpr( dt
[tindex
].getConstructor() ) );
1187 for( unsigned i
=0; i
<dt
[tindex
].getNumArgs(); i
++ ){
1188 Node sel
= NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL
, Node::fromExpr( dt
[tindex
].getSelectorInternal( tn
.toType(), i
) ), n
);
1189 Node cc
= getCurrentTemplate( sel
, var_count
);
1190 children
.push_back( cc
);
1192 return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR
, children
);
1194 return d_tds
->getFreeVarInc( n
.getType(), var_count
);
1198 Node
SygusSymBreakNew::SearchSizeInfo::getOrMkMeasureValue(
1199 std::vector
<Node
>& lemmas
)
1201 if (d_measure_value
.isNull())
1203 d_measure_value
= NodeManager::currentNM()->mkSkolem(
1204 "mt", NodeManager::currentNM()->integerType());
1205 lemmas
.push_back(NodeManager::currentNM()->mkNode(
1208 NodeManager::currentNM()->mkConst(Rational(0))));
1210 return d_measure_value
;
1213 Node
SygusSymBreakNew::SearchSizeInfo::getOrMkActiveMeasureValue(
1214 std::vector
<Node
>& lemmas
, bool mkNew
)
1218 Node new_mt
= NodeManager::currentNM()->mkSkolem(
1219 "mt", NodeManager::currentNM()->integerType());
1220 lemmas
.push_back(NodeManager::currentNM()->mkNode(
1221 kind::GEQ
, new_mt
, NodeManager::currentNM()->mkConst(Rational(0))));
1222 d_measure_value_active
= new_mt
;
1224 else if (d_measure_value_active
.isNull())
1226 d_measure_value_active
= getOrMkMeasureValue(lemmas
);
1228 return d_measure_value_active
;
1231 Node
SygusSymBreakNew::SearchSizeInfo::getFairnessLiteral( unsigned s
, TheoryDatatypes
* d
, std::vector
< Node
>& lemmas
) {
1232 if( options::sygusFair()!=SYGUS_FAIR_NONE
){
1233 std::map
< unsigned, Node
>::iterator it
= d_lits
.find( s
);
1234 if( it
==d_lits
.end() ){
1235 if (options::sygusAbortSize() != -1
1236 && static_cast<int>(s
) > options::sygusAbortSize())
1238 std::stringstream ss
;
1239 ss
<< "Maximum term size (" << options::sygusAbortSize()
1240 << ") for enumerative SyGuS exceeded." << std::endl
;
1241 throw LogicException(ss
.str());
1243 Assert( !d_this
.isNull() );
1244 Node c
= NodeManager::currentNM()->mkConst( Rational( s
) );
1245 Node lit
= NodeManager::currentNM()->mkNode( DT_SYGUS_BOUND
, d_this
, c
);
1246 lit
= d
->getValuation().ensureLiteral( lit
);
1248 Trace("sygus-fair") << "******* Sygus : allocate size literal " << s
<< " for " << d_this
<< " : " << lit
<< std::endl
;
1249 Trace("cegqi-engine") << "******* Sygus : allocate size literal " << s
<< " for " << d_this
<< std::endl
;
1250 Node lem
= NodeManager::currentNM()->mkNode( kind::OR
, lit
, lit
.negate() );
1251 Trace("sygus-dec") << "Sygus : Fairness split : " << lem
<< std::endl
;
1252 lemmas
.push_back( lem
);
1253 d
->getOutputChannel().requirePhase( lit
, true );
1261 return Node::null();
1265 Node
SygusSymBreakNew::getNextDecisionRequest( unsigned& priority
, std::vector
< Node
>& lemmas
) {
1266 Trace("sygus-dec-debug") << "SygusSymBreakNew: Get next decision " << std::endl
;
1267 for( std::map
< Node
, Node
>::iterator it
= d_anchor_to_active_guard
.begin(); it
!= d_anchor_to_active_guard
.end(); ++it
){
1268 if( getGuardStatus( it
->second
)==0 ){
1269 Trace("sygus-dec") << "Sygus : Decide next on active guard : " << it
->second
<< "..." << std::endl
;
1274 for( std::map
< Node
, SearchSizeInfo
* >::iterator it
= d_szinfo
.begin(); it
!= d_szinfo
.end(); ++it
){
1275 SearchSizeInfo
* s
= it
->second
;
1276 std::vector
< Node
> new_lit
;
1277 Node c_lit
= s
->getCurrentFairnessLiteral( d_td
, lemmas
);
1278 Assert( !c_lit
.isNull() );
1279 int gstatus
= getGuardStatus( c_lit
);
1281 s
->incrementCurrentLiteral();
1282 c_lit
= s
->getCurrentFairnessLiteral( d_td
, lemmas
);
1283 Assert( !c_lit
.isNull() );
1284 Trace("sygus-dec") << "Sygus : Decide on next lit : " << c_lit
<< "..." << std::endl
;
1287 }else if( gstatus
==0 ){
1288 Trace("sygus-dec") << "Sygus : Decide on current lit : " << c_lit
<< "..." << std::endl
;
1293 return Node::null();
1296 int SygusSymBreakNew::getGuardStatus( Node g
) {
1298 if( d_td
->getValuation().hasSatValue( g
, value
) ) {