1 /********************* */
2 /*! \file term_database_sygus.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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 term database sygus class
15 #include "theory/quantifiers/sygus/term_database_sygus.h"
17 #include "base/check.h"
18 #include "expr/sygus_datatype.h"
19 #include "options/base_options.h"
20 #include "options/datatypes_options.h"
21 #include "options/quantifiers_options.h"
22 #include "printer/printer.h"
23 #include "theory/arith/arith_msum.h"
24 #include "theory/datatypes/theory_datatypes_utils.h"
25 #include "theory/quantifiers/quantifiers_attributes.h"
26 #include "theory/quantifiers/term_database.h"
27 #include "theory/quantifiers/term_util.h"
28 #include "theory/quantifiers_engine.h"
30 using namespace CVC4::kind
;
34 namespace quantifiers
{
36 std::ostream
& operator<<(std::ostream
& os
, EnumeratorRole r
)
40 case ROLE_ENUM_POOL
: os
<< "POOL"; break;
41 case ROLE_ENUM_SINGLE_SOLUTION
: os
<< "SINGLE_SOLUTION"; break;
42 case ROLE_ENUM_MULTI_SOLUTION
: os
<< "MULTI_SOLUTION"; break;
43 case ROLE_ENUM_CONSTRAINED
: os
<< "CONSTRAINED"; break;
44 default: os
<< "enum_" << static_cast<unsigned>(r
); break;
49 TermDbSygus::TermDbSygus(context::Context
* c
, QuantifiersEngine
* qe
)
51 d_syexp(new SygusExplain(this)),
52 d_ext_rw(new ExtendedRewriter(true)),
53 d_eval(new Evaluator
),
54 d_funDefEval(new FunDefEvaluator
),
55 d_eval_unfold(new SygusEvalUnfold(this))
57 d_true
= NodeManager::currentNM()->mkConst( true );
58 d_false
= NodeManager::currentNM()->mkConst( false );
61 bool TermDbSygus::reset( Theory::Effort e
) {
65 TNode
TermDbSygus::getFreeVar( TypeNode tn
, int i
, bool useSygusType
) {
69 if( tn
.isDatatype() ){
70 const DType
& dt
= tn
.getDType();
71 if( !dt
.getSygusType().isNull() ){
72 vtn
= dt
.getSygusType();
77 while( i
>=(int)d_fv
[sindex
][tn
].size() ){
79 if( tn
.isDatatype() ){
80 const DType
& dt
= tn
.getDType();
81 ss
<< "fv_" << dt
.getName() << "_" << i
;
83 ss
<< "fv_" << tn
<< "_" << i
;
85 Assert(!vtn
.isNull());
86 Node v
= NodeManager::currentNM()->mkSkolem( ss
.str(), vtn
, "for sygus normal form testing" );
89 d_fv
[sindex
][tn
].push_back( v
);
91 return d_fv
[sindex
][tn
][i
];
94 TNode
TermDbSygus::getFreeVarInc( TypeNode tn
, std::map
< TypeNode
, int >& var_count
, bool useSygusType
) {
95 std::map
< TypeNode
, int >::iterator it
= var_count
.find( tn
);
96 if( it
==var_count
.end() ){
98 return getFreeVar( tn
, 0, useSygusType
);
100 int index
= it
->second
;
102 return getFreeVar( tn
, index
, useSygusType
);
106 bool TermDbSygus::hasFreeVar( Node n
, std::map
< Node
, bool >& visited
){
107 if( visited
.find( n
)==visited
.end() ){
109 if( isFreeVar( n
) ){
112 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
113 if( hasFreeVar( n
[i
], visited
) ){
121 bool TermDbSygus::hasFreeVar( Node n
) {
122 std::map
< Node
, bool > visited
;
123 return hasFreeVar( n
, visited
);
126 Node
TermDbSygus::getProxyVariable(TypeNode tn
, Node c
)
128 Assert(tn
.isDatatype());
129 Assert(tn
.getDType().isSygus());
130 Assert(tn
.getDType().getSygusType().isComparableTo(c
.getType()));
132 std::map
<Node
, Node
>::iterator it
= d_proxy_vars
[tn
].find(c
);
133 if (it
== d_proxy_vars
[tn
].end())
135 SygusTypeInfo
& ti
= getTypeInfo(tn
);
136 int anyC
= ti
.getAnyConstantConsNum();
140 k
= NodeManager::currentNM()->mkSkolem("sy", tn
, "sygus proxy");
141 SygusPrintProxyAttribute spa
;
142 k
.setAttribute(spa
, c
);
146 const DType
& dt
= tn
.getDType();
147 k
= NodeManager::currentNM()->mkNode(
148 APPLY_CONSTRUCTOR
, dt
[anyC
].getConstructor(), c
);
150 d_proxy_vars
[tn
][c
] = k
;
156 TypeNode
TermDbSygus::getSygusTypeForVar( Node v
) {
157 Assert(d_fv_stype
.find(v
) != d_fv_stype
.end());
158 return d_fv_stype
[v
];
161 Node
TermDbSygus::mkGeneric(const DType
& dt
,
163 std::map
<TypeNode
, int>& var_count
,
164 std::map
<int, Node
>& pre
,
167 Assert(c
< dt
.getNumConstructors());
168 Assert(dt
.isSygus());
169 Assert(!dt
[c
].getSygusOp().isNull());
170 std::vector
< Node
> children
;
171 Trace("sygus-db-debug") << "mkGeneric " << dt
.getName() << " " << c
<< "..."
173 for (unsigned i
= 0, nargs
= dt
[c
].getNumArgs(); i
< nargs
; i
++)
176 std::map
< int, Node
>::iterator it
= pre
.find( i
);
179 Trace("sygus-db-debug") << "From pre: " << a
<< std::endl
;
181 TypeNode tna
= dt
[c
].getArgType(i
);
182 a
= getFreeVarInc( tna
, var_count
, true );
184 Trace("sygus-db-debug")
185 << " child " << i
<< " : " << a
<< " : " << a
.getType() << std::endl
;
187 children
.push_back( a
);
189 Node ret
= datatypes::utils::mkSygusTerm(dt
, c
, children
, doBetaRed
);
190 Trace("sygus-db-debug") << "mkGeneric returns " << ret
<< std::endl
;
194 Node
TermDbSygus::mkGeneric(const DType
& dt
,
196 std::map
<int, Node
>& pre
,
199 std::map
<TypeNode
, int> var_count
;
200 return mkGeneric(dt
, c
, var_count
, pre
, doBetaRed
);
203 Node
TermDbSygus::mkGeneric(const DType
& dt
, int c
, bool doBetaRed
)
205 std::map
<int, Node
> pre
;
206 return mkGeneric(dt
, c
, pre
, doBetaRed
);
209 struct CanonizeBuiltinAttributeId
212 using CanonizeBuiltinAttribute
=
213 expr::Attribute
<CanonizeBuiltinAttributeId
, Node
>;
215 Node
TermDbSygus::canonizeBuiltin(Node n
)
217 std::map
<TypeNode
, int> var_count
;
218 return canonizeBuiltin(n
, var_count
);
221 Node
TermDbSygus::canonizeBuiltin(Node n
, std::map
<TypeNode
, int>& var_count
)
223 // has it already been computed?
224 if (var_count
.empty() && n
.hasAttribute(CanonizeBuiltinAttribute()))
226 Node ret
= n
.getAttribute(CanonizeBuiltinAttribute());
227 Trace("sygus-db-canon") << "cached " << n
<< " : " << ret
<< "\n";
230 Trace("sygus-db-canon") << " CanonizeBuiltin : compute for " << n
<< "\n";
232 // it is symbolic if it represents "any constant"
233 if (n
.getKind() == APPLY_SELECTOR_TOTAL
)
235 ret
= getFreeVarInc(n
[0].getType(), var_count
, true);
237 else if (n
.getKind() != APPLY_CONSTRUCTOR
)
243 Assert(n
.getKind() == APPLY_CONSTRUCTOR
);
244 bool childChanged
= false;
245 std::vector
<Node
> children
;
246 children
.push_back(n
.getOperator());
247 for (unsigned j
= 0, size
= n
.getNumChildren(); j
< size
; ++j
)
249 Node child
= canonizeBuiltin(n
[j
], var_count
);
250 children
.push_back(child
);
251 childChanged
= childChanged
|| child
!= n
[j
];
255 ret
= NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR
, children
);
258 // cache if we had a fresh variable count
259 if (var_count
.empty())
261 n
.setAttribute(CanonizeBuiltinAttribute(), ret
);
263 Trace("sygus-db-canon") << " ...normalized " << n
<< " --> " << ret
265 Assert(ret
.getType().isComparableTo(n
.getType()));
269 struct SygusToBuiltinAttributeId
272 typedef expr::Attribute
<SygusToBuiltinAttributeId
, Node
>
273 SygusToBuiltinAttribute
;
275 Node
TermDbSygus::sygusToBuiltin(Node n
, TypeNode tn
)
279 // if its a constant, we use the datatype utility version
280 return datatypes::utils::sygusToBuiltin(n
);
282 Assert(n
.getType().isComparableTo(tn
));
283 if (!tn
.isDatatype())
287 // has it already been computed?
288 if (n
.hasAttribute(SygusToBuiltinAttribute()))
290 return n
.getAttribute(SygusToBuiltinAttribute());
292 Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n
293 << ", type = " << tn
<< std::endl
;
294 const DType
& dt
= tn
.getDType();
299 if (n
.getKind() == APPLY_CONSTRUCTOR
)
301 unsigned i
= datatypes::utils::indexOf(n
.getOperator());
302 Assert(n
.getNumChildren() == dt
[i
].getNumArgs());
303 std::map
<int, Node
> pre
;
304 for (unsigned j
= 0, size
= n
.getNumChildren(); j
< size
; j
++)
306 pre
[j
] = sygusToBuiltin(n
[j
], dt
[i
].getArgType(j
));
307 Trace("sygus-db-debug")
308 << "sygus to builtin " << n
[j
] << " is " << pre
[j
] << std::endl
;
310 Node ret
= mkGeneric(dt
, i
, pre
);
311 Trace("sygus-db-debug")
312 << "SygusToBuiltin : Generic is " << ret
<< std::endl
;
314 n
.setAttribute(SygusToBuiltinAttribute(), ret
);
317 if (n
.hasAttribute(SygusPrintProxyAttribute()))
319 // this variable was associated by an attribute to a builtin node
320 return n
.getAttribute(SygusPrintProxyAttribute());
322 Assert(isFreeVar(n
));
323 // map to builtin variable type
324 int fv_num
= getVarNum(n
);
325 Assert(!dt
.getSygusType().isNull());
326 TypeNode vtn
= dt
.getSygusType();
327 Node ret
= getFreeVar(vtn
, fv_num
);
331 unsigned TermDbSygus::getSygusTermSize( Node n
){
332 if (n
.getKind() != APPLY_CONSTRUCTOR
)
337 for (unsigned i
= 0; i
< n
.getNumChildren(); i
++)
339 sum
+= getSygusTermSize(n
[i
]);
341 const DType
& dt
= datatypes::utils::datatypeOf(n
.getOperator());
342 int cindex
= datatypes::utils::indexOf(n
.getOperator());
343 Assert(cindex
>= 0 && cindex
< (int)dt
.getNumConstructors());
344 unsigned weight
= dt
[cindex
].getWeight();
348 bool TermDbSygus::registerSygusType(TypeNode tn
)
350 std::map
<TypeNode
, bool>::iterator it
= d_registerStatus
.find(tn
);
351 if (it
!= d_registerStatus
.end())
353 // already registered
356 d_registerStatus
[tn
] = false;
357 // it must be a sygus datatype
358 if (!tn
.isDatatype())
362 const DType
& dt
= tn
.getDType();
367 d_registerStatus
[tn
] = true;
368 SygusTypeInfo
& sti
= d_tinfo
[tn
];
369 sti
.initialize(this, tn
);
373 void TermDbSygus::registerEnumerator(Node e
,
375 SynthConjecture
* conj
,
376 EnumeratorRole erole
,
377 bool useSymbolicCons
)
379 if (d_enum_to_conjecture
.find(e
) != d_enum_to_conjecture
.end())
381 // already registered
384 Trace("sygus-db") << "Register enumerator : " << e
<< std::endl
;
386 TypeNode et
= e
.getType();
387 registerSygusType(et
);
388 d_enum_to_conjecture
[e
] = conj
;
389 d_enum_to_synth_fun
[e
] = f
;
390 NodeManager
* nm
= NodeManager::currentNM();
392 Trace("sygus-db") << " registering symmetry breaking clauses..."
394 d_enum_to_using_sym_cons
[e
] = useSymbolicCons
;
395 // depending on if we are using symbolic constructors, introduce symmetry
396 // breaking lemma templates for each relevant subtype of the grammar
397 SygusTypeInfo
& eti
= getTypeInfo(et
);
398 std::vector
<TypeNode
> sf_types
;
399 eti
.getSubfieldTypes(sf_types
);
400 // for each type of subfield type of this enumerator
401 for (unsigned i
= 0, ntypes
= sf_types
.size(); i
< ntypes
; i
++)
403 std::vector
<unsigned> rm_indices
;
404 TypeNode stn
= sf_types
[i
];
405 Assert(stn
.isDatatype());
406 SygusTypeInfo
& sti
= getTypeInfo(stn
);
407 const DType
& dt
= stn
.getDType();
408 int anyC
= sti
.getAnyConstantConsNum();
409 for (unsigned i
= 0, ncons
= dt
.getNumConstructors(); i
< ncons
; i
++)
411 bool isAnyC
= static_cast<int>(i
) == anyC
;
412 if (isAnyC
&& !useSymbolicCons
)
414 // if we are not using the any constant constructor
415 // do not use the symbolic constructor
416 rm_indices
.push_back(i
);
418 else if (anyC
!= -1 && !isAnyC
&& useSymbolicCons
)
420 // if we are using the any constant constructor, do not use any
422 Node c_op
= sti
.getConsNumConst(i
);
425 rm_indices
.push_back(i
);
429 for (unsigned& rindex
: rm_indices
)
431 // make the apply-constructor corresponding to an application of the
432 // constant or "any constant" constructor
433 // we call getInstCons since in the case of any constant constructors, it
434 // is necessary to generate a term of the form any_constant( x.0 ) for a
435 // fresh variable x.0.
436 Node fv
= getFreeVar(stn
, 0);
437 Node exc_val
= datatypes::utils::getInstCons(fv
, dt
, rindex
);
438 // should not include the constuctor in any subterm
439 Node x
= getFreeVar(stn
, 0);
440 Trace("sygus-db") << "Construct symmetry breaking lemma from " << x
441 << " == " << exc_val
<< std::endl
;
442 Node lem
= getExplain()->getExplanationForEquality(x
, exc_val
);
445 << "Cegqi::Lemma : exclude symbolic cons lemma (template) : " << lem
447 // the size of the subterm we are blocking is the weight of the
448 // constructor (usually zero)
449 registerSymBreakLemma(e
, lem
, stn
, dt
[rindex
].getWeight());
452 Trace("sygus-db") << " ...finished" << std::endl
;
454 // determine if we are actively-generated
455 bool isActiveGen
= false;
456 if (options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE
)
458 if (erole
== ROLE_ENUM_MULTI_SOLUTION
|| erole
== ROLE_ENUM_CONSTRAINED
)
460 // If the enumerator is a solution for a conjecture with multiple
461 // functions, we do not use active generation. If we did, we would have to
462 // generate a "product" of two actively-generated enumerators. That is,
463 // given a conjecture with two functions-to-synthesize with enumerators
464 // e_f and e_g, and if these enumerators generated:
465 // e_f -> t1, ..., tn
466 // e_g -> s1, ..., sm
467 // The sygus module in charge of this conjecture would expect
468 // constructCandidates calls of the form
469 // (e_f,e_g) -> (ti, sj)
470 // for each i,j. We instead use passive enumeration in this case.
472 // If the enumerator is constrained, it cannot be actively generated.
474 else if (erole
== ROLE_ENUM_POOL
)
476 // If the enumerator is used for generating a pool of values, we always
477 // use active generation.
480 else if (erole
== ROLE_ENUM_SINGLE_SOLUTION
)
482 // If the enumerator is the single function-to-synthesize, if auto is
483 // enabled, we infer whether it is better to enable active generation.
484 if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO
)
486 // We use active generation if the grammar of the enumerator does not
487 // have ITE and is not Boolean. Experimentally, it is better to
488 // use passive generation for these cases since it enables useful
489 // search space pruning techniques, e.g. evaluation unfolding,
490 // conjecture-specific symmetry breaking. Also, if sygus-stream is
491 // enabled, we always use active generation, since the use cases of
492 // sygus stream are to find many solutions to an easy problem, where
493 // the bottleneck often becomes the large number of "exclude the current
494 // solution" clauses.
495 const DType
& dt
= et
.getDType();
496 if (options::sygusStream()
497 || (!eti
.hasIte() && !dt
.getSygusType().isBoolean()))
509 Unreachable() << "Unknown enumerator mode in registerEnumerator";
512 Trace("sygus-db") << "isActiveGen for " << e
<< ", role = " << erole
513 << " returned " << isActiveGen
<< std::endl
;
514 // Currently, actively-generated enumerators are either basic or variable
518 && options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_VAR_AGNOSTIC
;
519 d_enum_var_agnostic
[e
] = isVarAgnostic
;
522 // requires variable subclasses
523 eti
.initializeVarSubclasses();
524 // If no subclass has more than one variable, do not use variable agnostic
526 bool useVarAgnostic
= !eti
.isSubclassVarTrivial();
530 << "...disabling variable agnostic for " << e
531 << " since it has no subclass with more than one variable."
533 d_enum_var_agnostic
[e
] = false;
537 d_enum_active_gen
[e
] = isActiveGen
;
538 d_enum_basic
[e
] = isActiveGen
&& !isVarAgnostic
;
540 // We make an active guard if we will be explicitly blocking solutions for
541 // the enumerator. This is the case if the role of the enumerator is to
542 // populate a pool of terms, or (some cases) of when it is actively generated.
543 if (isActiveGen
|| erole
== ROLE_ENUM_POOL
)
546 Node ag
= nm
->mkSkolem("eG", nm
->booleanType());
547 // must ensure it is a literal immediately here
548 ag
= d_quantEngine
->getValuation().ensureLiteral(ag
);
549 // must ensure that it is asserted as a literal before we begin solving
550 Node lem
= nm
->mkNode(OR
, ag
, ag
.negate());
551 d_quantEngine
->getOutputChannel().requirePhase(ag
, true);
552 d_quantEngine
->getOutputChannel().lemma(lem
);
553 d_enum_to_active_guard
[e
] = ag
;
557 bool TermDbSygus::isEnumerator(Node e
) const
559 return d_enum_to_conjecture
.find(e
) != d_enum_to_conjecture
.end();
562 SynthConjecture
* TermDbSygus::getConjectureForEnumerator(Node e
) const
564 std::map
<Node
, SynthConjecture
*>::const_iterator itm
=
565 d_enum_to_conjecture
.find(e
);
566 if (itm
!= d_enum_to_conjecture
.end()) {
572 Node
TermDbSygus::getSynthFunForEnumerator(Node e
) const
574 std::map
<Node
, Node
>::const_iterator itsf
= d_enum_to_synth_fun
.find(e
);
575 if (itsf
!= d_enum_to_synth_fun
.end())
582 Node
TermDbSygus::getActiveGuardForEnumerator(Node e
) const
584 std::map
<Node
, Node
>::const_iterator itag
= d_enum_to_active_guard
.find(e
);
585 if (itag
!= d_enum_to_active_guard
.end()) {
591 bool TermDbSygus::usingSymbolicConsForEnumerator(Node e
) const
593 std::map
<Node
, bool>::const_iterator itus
= d_enum_to_using_sym_cons
.find(e
);
594 if (itus
!= d_enum_to_using_sym_cons
.end())
601 bool TermDbSygus::isVariableAgnosticEnumerator(Node e
) const
603 std::map
<Node
, bool>::const_iterator itus
= d_enum_var_agnostic
.find(e
);
604 if (itus
!= d_enum_var_agnostic
.end())
611 bool TermDbSygus::isBasicEnumerator(Node e
) const
613 std::map
<Node
, bool>::const_iterator itus
= d_enum_basic
.find(e
);
614 if (itus
!= d_enum_basic
.end())
621 bool TermDbSygus::isPassiveEnumerator(Node e
) const
623 std::map
<Node
, bool>::const_iterator itus
= d_enum_active_gen
.find(e
);
624 if (itus
!= d_enum_active_gen
.end())
626 return !itus
->second
;
631 void TermDbSygus::getEnumerators(std::vector
<Node
>& mts
)
633 for (std::map
<Node
, SynthConjecture
*>::iterator itm
=
634 d_enum_to_conjecture
.begin();
635 itm
!= d_enum_to_conjecture
.end();
638 mts
.push_back( itm
->first
);
642 void TermDbSygus::registerSymBreakLemma(
643 Node e
, Node lem
, TypeNode tn
, unsigned sz
, bool isTempl
)
645 d_enum_to_sb_lemmas
[e
].push_back(lem
);
646 d_sb_lemma_to_type
[lem
] = tn
;
647 d_sb_lemma_to_size
[lem
] = sz
;
648 d_sb_lemma_to_isTempl
[lem
] = isTempl
;
651 bool TermDbSygus::hasSymBreakLemmas(std::vector
<Node
>& enums
) const
653 if (!d_enum_to_sb_lemmas
.empty())
655 for (std::pair
<const Node
, std::vector
<Node
> > sb
: d_enum_to_sb_lemmas
)
657 enums
.push_back(sb
.first
);
664 void TermDbSygus::getSymBreakLemmas(Node e
, std::vector
<Node
>& lemmas
) const
666 std::map
<Node
, std::vector
<Node
> >::const_iterator itsb
=
667 d_enum_to_sb_lemmas
.find(e
);
668 if (itsb
!= d_enum_to_sb_lemmas
.end())
670 lemmas
.insert(lemmas
.end(), itsb
->second
.begin(), itsb
->second
.end());
674 TypeNode
TermDbSygus::getTypeForSymBreakLemma(Node lem
) const
676 std::map
<Node
, TypeNode
>::const_iterator it
= d_sb_lemma_to_type
.find(lem
);
677 Assert(it
!= d_sb_lemma_to_type
.end());
680 unsigned TermDbSygus::getSizeForSymBreakLemma(Node lem
) const
682 std::map
<Node
, unsigned>::const_iterator it
= d_sb_lemma_to_size
.find(lem
);
683 Assert(it
!= d_sb_lemma_to_size
.end());
687 bool TermDbSygus::isSymBreakLemmaTemplate(Node lem
) const
689 std::map
<Node
, bool>::const_iterator it
= d_sb_lemma_to_isTempl
.find(lem
);
690 Assert(it
!= d_sb_lemma_to_isTempl
.end());
694 void TermDbSygus::clearSymBreakLemmas(Node e
) { d_enum_to_sb_lemmas
.erase(e
); }
696 bool TermDbSygus::isRegistered(TypeNode tn
) const
698 return d_tinfo
.find(tn
) != d_tinfo
.end();
701 TypeNode
TermDbSygus::sygusToBuiltinType( TypeNode tn
) {
702 std::map
<TypeNode
, SygusTypeInfo
>::iterator it
= d_tinfo
.find(tn
);
703 Assert(it
!= d_tinfo
.end());
704 return it
->second
.getBuiltinType();
707 void TermDbSygus::toStreamSygus(const char* c
, Node n
)
717 std::stringstream ss
;
718 Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss
, n
);
719 Trace(c
) << ss
.str();
724 SygusTypeInfo
& TermDbSygus::getTypeInfo(TypeNode tn
)
726 AlwaysAssert(d_tinfo
.find(tn
) != d_tinfo
.end());
730 Node
TermDbSygus::rewriteNode(Node n
) const
732 Node res
= Rewriter::rewrite(n
);
735 // constant, we are done
738 if (options::sygusRecFun())
740 if (d_funDefEval
->hasDefinitions())
742 // If recursive functions are enabled, then we use the recursive function
743 // evaluation utility.
744 Node fres
= d_funDefEval
->evaluate(res
);
749 // It may have failed, in which case there are undefined symbols in res or
750 // we reached the limit of evaluations. In this case, we revert to the
751 // result of rewriting in the return statement below.
757 unsigned TermDbSygus::getSelectorWeight(TypeNode tn
, Node sel
)
759 std::map
<TypeNode
, std::map
<Node
, unsigned> >::iterator itsw
=
760 d_sel_weight
.find(tn
);
761 if (itsw
== d_sel_weight
.end())
763 d_sel_weight
[tn
].clear();
764 itsw
= d_sel_weight
.find(tn
);
765 const DType
& dt
= tn
.getDType();
766 Trace("sygus-db") << "Compute selector weights for " << dt
.getName()
768 for (unsigned i
= 0, size
= dt
.getNumConstructors(); i
< size
; i
++)
770 unsigned cw
= dt
[i
].getWeight();
771 for (unsigned j
= 0, size2
= dt
[i
].getNumArgs(); j
< size2
; j
++)
773 Node csel
= dt
[i
].getSelectorInternal(tn
, j
);
774 std::map
<Node
, unsigned>::iterator its
= itsw
->second
.find(csel
);
775 if (its
== itsw
->second
.end() || cw
< its
->second
)
777 d_sel_weight
[tn
][csel
] = cw
;
778 Trace("sygus-db") << " w(" << csel
<< ") <= " << cw
<< std::endl
;
783 Assert(itsw
->second
.find(sel
) != itsw
->second
.end());
784 return itsw
->second
[sel
];
787 TypeNode
TermDbSygus::getArgType(const DTypeConstructor
& c
, unsigned i
) const
789 Assert(i
< c
.getNumArgs());
790 return c
.getArgType(i
);
793 bool TermDbSygus::isTypeMatch(const DTypeConstructor
& c1
,
794 const DTypeConstructor
& c2
)
796 if( c1
.getNumArgs()!=c2
.getNumArgs() ){
799 for( unsigned i
=0; i
<c1
.getNumArgs(); i
++ ){
800 if( getArgType( c1
, i
)!=getArgType( c2
, i
) ){
808 bool TermDbSygus::isSymbolicConsApp(Node n
) const
810 if (n
.getKind() != APPLY_CONSTRUCTOR
)
814 TypeNode tn
= n
.getType();
815 Assert(tn
.isDatatype());
816 const DType
& dt
= tn
.getDType();
817 Assert(dt
.isSygus());
818 unsigned cindex
= datatypes::utils::indexOf(n
.getOperator());
819 Node sygusOp
= dt
[cindex
].getSygusOp();
820 // it is symbolic if it represents "any constant"
821 return sygusOp
.getAttribute(SygusAnyConstAttribute());
824 bool TermDbSygus::canConstructKind(TypeNode tn
,
826 std::vector
<TypeNode
>& argts
,
829 Assert(isRegistered(tn
));
830 SygusTypeInfo
& ti
= getTypeInfo(tn
);
831 int c
= ti
.getKindConsNum(k
);
832 const DType
& dt
= tn
.getDType();
835 for (unsigned i
= 0, nargs
= dt
[c
].getNumArgs(); i
< nargs
; i
++)
837 argts
.push_back(dt
[c
].getArgType(i
));
841 if (!options::sygusSymBreakAgg())
845 if (sygusToBuiltinType(tn
).isBoolean())
849 // ite( b1, b2, b3 ) <---- and( or( ~b1, b2 ), or( b1, b3 ) )
850 std::vector
<TypeNode
> conj_types
;
851 if (canConstructKind(tn
, AND
, conj_types
, true) && conj_types
.size() == 2)
854 std::vector
<TypeNode
> disj_types
[2];
855 for (unsigned c
= 0; c
< 2; c
++)
857 if (!canConstructKind(conj_types
[c
], OR
, disj_types
[c
], true)
858 || disj_types
[c
].size() != 2)
866 for (unsigned r
= 0; r
< 2; r
++)
868 for (unsigned d
= 0, size
= disj_types
[r
].size(); d
< size
; d
++)
870 TypeNode dtn
= disj_types
[r
][d
];
871 // must have negation that occurs in the other conjunct
872 std::vector
<TypeNode
> ntypes
;
873 if (canConstructKind(dtn
, NOT
, ntypes
) && ntypes
.size() == 1)
875 TypeNode ntn
= ntypes
[0];
876 for (unsigned dd
= 0, size
= disj_types
[1 - r
].size();
880 if (disj_types
[1 - r
][dd
] == ntn
)
882 argts
.push_back(ntn
);
883 argts
.push_back(disj_types
[r
][d
]);
884 argts
.push_back(disj_types
[1 - r
][1 - dd
]);
885 if (Trace
.isOn("sygus-cons-kind"))
887 Trace("sygus-cons-kind")
888 << "Can construct kind " << k
<< " in " << tn
889 << " via child types:" << std::endl
;
890 for (unsigned i
= 0; i
< 3; i
++)
892 Trace("sygus-cons-kind")
893 << " " << argts
[i
] << std::endl
;
906 // could try aggressive inferences here, such as
907 // (and b1 b2) <---- (not (or (not b1) (not b2)))
908 // (or b1 b2) <---- (not (and (not b1) (not b2)))
912 bool TermDbSygus::involvesDivByZero( Node n
, std::map
< Node
, bool >& visited
){
913 if( visited
.find( n
)==visited
.end() ){
915 Kind k
= n
.getKind();
916 if( k
==DIVISION
|| k
==DIVISION_TOTAL
|| k
==INTS_DIVISION
|| k
==INTS_DIVISION_TOTAL
||
917 k
==INTS_MODULUS
|| k
==INTS_MODULUS_TOTAL
){
918 if( n
[1].isConst() ){
920 == d_quantEngine
->getTermUtil()->getTypeValue(n
[1].getType(), 0))
925 // if it has free variables it might be a non-zero constant
926 if( !hasFreeVar( n
[1] ) ){
931 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
932 if( involvesDivByZero( n
[i
], visited
) ){
940 bool TermDbSygus::involvesDivByZero( Node n
) {
941 std::map
< Node
, bool > visited
;
942 return involvesDivByZero( n
, visited
);
945 Node
TermDbSygus::getAnchor( Node n
) {
946 if( n
.getKind()==APPLY_SELECTOR_TOTAL
){
947 return getAnchor( n
[0] );
953 unsigned TermDbSygus::getAnchorDepth( Node n
) {
954 if( n
.getKind()==APPLY_SELECTOR_TOTAL
){
955 return 1+getAnchorDepth( n
[0] );
961 Node
TermDbSygus::evaluateBuiltin(TypeNode tn
,
963 std::vector
<Node
>& args
,
968 return Rewriter::rewrite( bn
);
970 Assert(isRegistered(tn
));
971 SygusTypeInfo
& ti
= getTypeInfo(tn
);
972 const std::vector
<Node
>& varlist
= ti
.getVarList();
973 Assert(varlist
.size() == args
.size());
976 if (tryEval
&& options::sygusEvalOpt())
978 // Try evaluating, which is much faster than substitution+rewriting.
979 // This may fail if there is a subterm of bn under the
980 // substitution that is not constant, or if an operator in bn is not
981 // supported by the evaluator
982 res
= d_eval
->eval(bn
, varlist
, args
);
987 == Rewriter::rewrite(bn
.substitute(
988 varlist
.begin(), varlist
.end(), args
.begin(), args
.end())));
991 res
= bn
.substitute(varlist
.begin(), varlist
.end(), args
.begin(), args
.end());
992 // Call the rewrite node function, which may involve recursive function
994 return rewriteNode(res
);
997 Node
TermDbSygus::evaluateWithUnfolding(
998 Node n
, std::unordered_map
<Node
, Node
, NodeHashFunction
>& visited
)
1000 std::unordered_map
<Node
, Node
, NodeHashFunction
>::iterator it
=
1002 if( it
==visited
.end() ){
1004 while (ret
.getKind() == DT_SYGUS_EVAL
1005 && ret
[0].getKind() == APPLY_CONSTRUCTOR
)
1007 if (ret
== n
&& ret
[0].isConst())
1009 // use rewriting, possibly involving recursive functions
1010 ret
= rewriteNode(ret
);
1014 ret
= d_eval_unfold
->unfold(ret
);
1017 if( ret
.getNumChildren()>0 ){
1018 std::vector
< Node
> children
;
1019 if( ret
.getMetaKind() == kind::metakind::PARAMETERIZED
){
1020 children
.push_back( ret
.getOperator() );
1022 bool childChanged
= false;
1023 for( unsigned i
=0; i
<ret
.getNumChildren(); i
++ ){
1024 Node nc
= evaluateWithUnfolding(ret
[i
], visited
);
1025 childChanged
= childChanged
|| nc
!=ret
[i
];
1026 children
.push_back( nc
);
1029 ret
= NodeManager::currentNM()->mkNode( ret
.getKind(), children
);
1031 ret
= getExtRewriter()->extendedRewrite(ret
);
1032 // use rewriting, possibly involving recursive functions
1033 ret
= rewriteNode(ret
);
1042 Node
TermDbSygus::evaluateWithUnfolding(Node n
)
1044 std::unordered_map
<Node
, Node
, NodeHashFunction
> visited
;
1045 return evaluateWithUnfolding(n
, visited
);
1048 bool TermDbSygus::isEvaluationPoint(Node n
) const
1050 if (n
.getKind() != DT_SYGUS_EVAL
)
1058 for (unsigned i
= 1, nchild
= n
.getNumChildren(); i
< nchild
; i
++)
1060 if (!n
[i
].isConst())
1068 }/* CVC4::theory::quantifiers namespace */
1069 }/* CVC4::theory namespace */
1070 }/* CVC4 namespace */