From eaca3c11b3c2546f6ee0f840eae8e86c9d1d55ec Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 31 Oct 2019 23:37:16 -0500 Subject: Rename datatypes sygus solver (#3417) --- src/CMakeLists.txt | 4 +- src/theory/datatypes/datatypes_sygus.cpp | 1805 ----------------------------- src/theory/datatypes/datatypes_sygus.h | 723 ------------ src/theory/datatypes/sygus_extension.cpp | 1804 ++++++++++++++++++++++++++++ src/theory/datatypes/sygus_extension.h | 721 ++++++++++++ src/theory/datatypes/theory_datatypes.cpp | 31 +- src/theory/datatypes/theory_datatypes.h | 4 +- 7 files changed, 2545 insertions(+), 2547 deletions(-) delete mode 100644 src/theory/datatypes/datatypes_sygus.cpp delete mode 100644 src/theory/datatypes/datatypes_sygus.h create mode 100644 src/theory/datatypes/sygus_extension.cpp create mode 100644 src/theory/datatypes/sygus_extension.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index dd2b7eaea..f2ccbd765 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -401,8 +401,8 @@ libcvc4_add_sources( theory/care_graph.h theory/datatypes/datatypes_rewriter.cpp theory/datatypes/datatypes_rewriter.h - theory/datatypes/datatypes_sygus.cpp - theory/datatypes/datatypes_sygus.h + theory/datatypes/sygus_extension.cpp + theory/datatypes/sygus_extension.h theory/datatypes/sygus_simple_sym.cpp theory/datatypes/sygus_simple_sym.h theory/datatypes/theory_datatypes.cpp diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp deleted file mode 100644 index 4cc9e4640..000000000 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ /dev/null @@ -1,1805 +0,0 @@ -/********************* */ -/*! \file datatypes_sygus.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of sygus utilities for theory of datatypes - ** - ** Implementation of sygus utilities for theory of datatypes - **/ - -#include "theory/datatypes/datatypes_sygus.h" - -#include "expr/node_manager.h" -#include "options/base_options.h" -#include "options/datatypes_options.h" -#include "options/quantifiers_options.h" -#include "printer/printer.h" -#include "theory/datatypes/theory_datatypes.h" -#include "theory/datatypes/theory_datatypes_utils.h" -#include "theory/quantifiers/sygus/sygus_explain.h" -#include "theory/quantifiers/sygus/term_database_sygus.h" -#include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" -#include "theory/theory_model.h" - -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::datatypes; - -SygusSymBreakNew::SygusSymBreakNew(TheoryDatatypes* td, - QuantifiersEngine* qe, - context::Context* c) - : d_td(td), - d_tds(qe->getTermDatabaseSygus()), - d_ssb(qe), - d_testers(c), - d_testers_exp(c), - d_active_terms(c), - d_currTermSize(c) -{ - d_zero = NodeManager::currentNM()->mkConst(Rational(0)); - d_true = NodeManager::currentNM()->mkConst(true); -} - -SygusSymBreakNew::~SygusSymBreakNew() { - -} - -/** add tester */ -void SygusSymBreakNew::assertTester( int tindex, TNode n, Node exp, std::vector< Node >& lemmas ) { - registerTerm( n, lemmas ); - // check if this is a relevant (sygus) term - if( d_term_to_anchor.find( n )!=d_term_to_anchor.end() ){ - Trace("sygus-sb-debug2") << "Sygus : process tester : " << exp << std::endl; - // if not already active (may have duplicate calls for the same tester) - if( d_active_terms.find( n )==d_active_terms.end() ) { - d_testers[n] = tindex; - d_testers_exp[n] = exp; - - // check if parent is active - bool do_add = true; - if( options::sygusSymBreakLazy() ){ - if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){ - NodeSet::const_iterator it = d_active_terms.find( n[0] ); - if( it==d_active_terms.end() ){ - do_add = false; - }else{ - //this must be a proper selector - IntMap::const_iterator itt = d_testers.find( n[0] ); - Assert(itt != d_testers.end()); - int ptindex = (*itt).second; - TypeNode ptn = n[0].getType(); - const Datatype& pdt = ((DatatypeType)ptn.toType()).getDatatype(); - int sindex_in_parent = pdt[ptindex].getSelectorIndexInternal( n.getOperator().toExpr() ); - // the tester is irrelevant in this branch - if( sindex_in_parent==-1 ){ - do_add = false; - } - } - } - } - if( do_add ){ - assertTesterInternal( tindex, n, exp, lemmas ); - }else{ - Trace("sygus-sb-debug2") << "...ignore inactive tester : " << exp << std::endl; - } - }else{ - Trace("sygus-sb-debug2") << "...ignore repeated tester : " << exp << std::endl; - } - }else{ - Trace("sygus-sb-debug2") << "...ignore non-sygus tester : " << exp << std::endl; - } -} - -void SygusSymBreakNew::assertFact( Node n, bool polarity, std::vector< Node >& lemmas ) { - if (n.getKind() == kind::DT_SYGUS_BOUND) - { - Node m = n[0]; - Trace("sygus-fair") << "Have sygus bound : " << n << ", polarity=" << polarity << " on measure " << m << std::endl; - registerMeasureTerm( m ); - if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){ - std::map>::iterator its = - d_szinfo.find(m); - Assert(its != d_szinfo.end()); - Node mt = its->second->getOrMkMeasureValue(lemmas); - //it relates the measure term to arithmetic - Node blem = n.eqNode( NodeManager::currentNM()->mkNode( kind::LEQ, mt, n[1] ) ); - lemmas.push_back( blem ); - } - if( polarity ){ - unsigned s = n[1].getConst().getNumerator().toUnsignedInt(); - notifySearchSize( m, s, n, lemmas ); - } - }else if( n.getKind() == kind::DT_HEIGHT_BOUND || n.getKind()==DT_SIZE_BOUND ){ - //reduce to arithmetic TODO ? - - } -} - -Node SygusSymBreakNew::getTermOrderPredicate( Node n1, Node n2 ) { - NodeManager* nm = NodeManager::currentNM(); - std::vector< Node > comm_disj; - // (1) size of left is greater than size of right - Node sz_less = - nm->mkNode(GT, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2)); - comm_disj.push_back( sz_less ); - // (2) ...or sizes are equal and first child is less by term order - std::vector sz_eq_cases; - Node sz_eq = - nm->mkNode(EQUAL, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2)); - sz_eq_cases.push_back( sz_eq ); - if( options::sygusOpt1() ){ - TypeNode tnc = n1.getType(); - const Datatype& cdt = ((DatatypeType)(tnc).toType()).getDatatype(); - for( unsigned j=0; j case_conj; - for (unsigned k = 0; k < j; k++) - { - case_conj.push_back(utils::mkTester(n2, k, cdt).negate()); - } - if (!case_conj.empty()) - { - Node corder = nm->mkNode( - OR, - utils::mkTester(n1, j, cdt).negate(), - case_conj.size() == 1 ? case_conj[0] : nm->mkNode(AND, case_conj)); - sz_eq_cases.push_back(corder); - } - } - } - Node sz_eqc = sz_eq_cases.size() == 1 ? sz_eq_cases[0] - : nm->mkNode(kind::AND, sz_eq_cases); - comm_disj.push_back( sz_eqc ); - - return nm->mkNode(kind::OR, comm_disj); -} - -void SygusSymBreakNew::registerTerm( Node n, std::vector< Node >& lemmas ) { - if( d_is_top_level.find( n )==d_is_top_level.end() ){ - d_is_top_level[n] = false; - TypeNode tn = n.getType(); - unsigned d = 0; - bool is_top_level = false; - bool success = false; - if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){ - registerTerm( n[0], lemmas ); - std::unordered_map::iterator it = - d_term_to_anchor.find(n[0]); - if( it!=d_term_to_anchor.end() ) { - d_term_to_anchor[n] = it->second; - unsigned sel_weight = - d_tds->getSelectorWeight(n[0].getType(), n.getOperator()); - d = d_term_to_depth[n[0]] + sel_weight; - is_top_level = computeTopLevel( tn, n[0] ); - success = true; - } - }else if( n.isVar() ){ - registerSizeTerm( n, lemmas ); - if( d_register_st[n] ){ - d_term_to_anchor[n] = n; - d_anchor_to_conj[n] = d_tds->getConjectureForEnumerator(n); - // this assertion fails if we have a sygus term in the search that is unmeasured - Assert(d_anchor_to_conj[n] != NULL); - d = 0; - is_top_level = true; - success = true; - } - } - if( success ){ - Trace("sygus-sb-debug") << "Register : " << n << ", depth : " << d << ", top level = " << is_top_level << ", type = " << ((DatatypeType)tn.toType()).getDatatype().getName() << std::endl; - d_term_to_depth[n] = d; - d_is_top_level[n] = is_top_level; - registerSearchTerm( tn, d, n, is_top_level, lemmas ); - }else{ - Trace("sygus-sb-debug2") << "Term " << n << " is not part of sygus search." << std::endl; - } - } -} - -bool SygusSymBreakNew::computeTopLevel( TypeNode tn, Node n ){ - if( n.getType()==tn ){ - return false; - }else if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){ - return computeTopLevel( tn, n[0] ); - }else{ - return true; - } -} - -void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std::vector< Node >& lemmas ) { - TypeNode ntn = n.getType(); - if (!ntn.isDatatype()) - { - // nothing to do for non-datatype types - return; - } - const Datatype& dt = static_cast(ntn.toType()).getDatatype(); - if (!dt.isSygus()) - { - // nothing to do for non-sygus-datatype type - return; - } - d_active_terms.insert(n); - Trace("sygus-sb-debug2") << "Sygus : activate term : " << n << " : " << exp - << std::endl; - - // get the search size for this - Assert(d_term_to_anchor.find(n) != d_term_to_anchor.end()); - Node a = d_term_to_anchor[n]; - Assert(d_anchor_to_measure_term.find(a) != d_anchor_to_measure_term.end()); - Node m = d_anchor_to_measure_term[a]; - std::map>::iterator itsz = - d_szinfo.find(m); - Assert(itsz != d_szinfo.end()); - unsigned ssz = itsz->second->d_curr_search_size; - - if( options::sygusFair()==SYGUS_FAIR_DIRECT ){ - if( dt[tindex].getNumArgs()>0 ){ - quantifiers::SygusTypeInfo& nti = d_tds->getTypeInfo(ntn); - // consider lower bounds for size of types - unsigned lb_add = nti.getMinConsTermSize(tindex); - unsigned lb_rem = n == a ? 0 : nti.getMinTermSize(); - Assert(lb_add >= lb_rem); - d_currTermSize[a].set( d_currTermSize[a].get() + ( lb_add - lb_rem ) ); - } - if( (unsigned)d_currTermSize[a].get()>ssz ){ - if( Trace.isOn("sygus-sb-fair") ){ - std::map< TypeNode, int > var_count; - Node templ = getCurrentTemplate( a, var_count ); - Trace("sygus-sb-fair") << "FAIRNESS : we have " << d_currTermSize[a].get() << " at search size " << ssz << ", template is " << templ << std::endl; - } - // conflict - std::vector< Node > conflict; - for( NodeSet::const_iterator its = d_active_terms.begin(); its != d_active_terms.end(); ++its ){ - Node x = *its; - Node xa = d_term_to_anchor[x]; - if( xa==a ){ - IntMap::const_iterator ittv = d_testers.find( x ); - Assert(ittv != d_testers.end()); - int tindex = (*ittv).second; - const Datatype& dti = ((DatatypeType)x.getType().toType()).getDatatype(); - if( dti[tindex].getNumArgs()>0 ){ - NodeMap::const_iterator itt = d_testers_exp.find( x ); - Assert(itt != d_testers_exp.end()); - conflict.push_back( (*itt).second ); - } - } - } - Assert(conflict.size() == (unsigned)d_currTermSize[a].get()); - Assert(itsz->second->d_search_size_exp.find(ssz) - != itsz->second->d_search_size_exp.end()); - conflict.push_back( itsz->second->d_search_size_exp[ssz] ); - Node conf = NodeManager::currentNM()->mkNode( kind::AND, conflict ); - Trace("sygus-sb-fair") << "Conflict is : " << conf << std::endl; - lemmas.push_back( conf.negate() ); - return; - } - } - - // now, add all applicable symmetry breaking lemmas for this term - Assert(d_term_to_depth.find(n) != d_term_to_depth.end()); - unsigned d = d_term_to_depth[n]; - Trace("sygus-sb-fair-debug") << "Tester " << exp << " is for depth " << d << " term in search size " << ssz << std::endl; - //Assert( d<=ssz ); - if( options::sygusSymBreakLazy() ){ - // dynamic symmetry breaking - addSymBreakLemmasFor( ntn, n, d, lemmas ); - } - - Trace("sygus-sb-debug") << "Get simple symmetry breaking predicates...\n"; - unsigned max_depth = ssz>=d ? ssz-d : 0; - unsigned min_depth = d_simple_proc[exp]; - NodeManager* nm = NodeManager::currentNM(); - if( min_depth<=max_depth ){ - TNode x = getFreeVar( ntn ); - std::vector sb_lemmas; - // symmetry breaking lemmas requiring predicate elimination - std::map sb_elim_pred; - bool usingSymCons = d_tds->usingSymbolicConsForEnumerator(m); - bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(m); - for (unsigned ds = 0; ds <= max_depth; ds++) - { - // static conjecture-independent symmetry breaking - Trace("sygus-sb-debug") << " simple symmetry breaking...\n"; - Node ipred = getSimpleSymBreakPred( - m, ntn, tindex, ds, usingSymCons, isVarAgnostic); - if (!ipred.isNull()) - { - sb_lemmas.push_back(ipred); - if (ds == 0 && isVarAgnostic) - { - sb_elim_pred[ipred] = true; - } - } - // static conjecture-dependent symmetry breaking - Trace("sygus-sb-debug") - << " conjecture-dependent symmetry breaking...\n"; - std::map::iterator itc = - d_anchor_to_conj.find(a); - if (itc != d_anchor_to_conj.end()) - { - quantifiers::SynthConjecture* conj = itc->second; - Assert(conj != NULL); - Node dpred = conj->getSymmetryBreakingPredicate(x, a, ntn, tindex, ds); - if (!dpred.isNull()) - { - sb_lemmas.push_back(dpred); - } - } - } - - // add the above symmetry breaking predicates to lemmas - std::unordered_map cache; - Node rlv = getRelevancyCondition(n); - for (const Node& slem : sb_lemmas) - { - Node sslem = slem.substitute(x, n, cache); - // if we require predicate elimination - if (sb_elim_pred.find(slem) != sb_elim_pred.end()) - { - Trace("sygus-sb-tp") << "Eliminate traversal predicates: start " - << sslem << std::endl; - sslem = eliminateTraversalPredicates(sslem); - Trace("sygus-sb-tp") << "Eliminate traversal predicates: finish " - << sslem << std::endl; - } - if (!rlv.isNull()) - { - sslem = nm->mkNode(OR, rlv, sslem); - } - lemmas.push_back(sslem); - } - } - d_simple_proc[exp] = max_depth + 1; - - // now activate the children those testers were previously asserted in this - // context and are awaiting activation, if they exist. - if( options::sygusSymBreakLazy() ){ - Trace("sygus-sb-debug") << "Do lazy symmetry breaking...\n"; - for( unsigned j=0; jmkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( ntn.toType(), j ) ), n ); - Trace("sygus-sb-debug2") << " activate child sel : " << sel << std::endl; - Assert(d_active_terms.find(sel) == d_active_terms.end()); - IntMap::const_iterator itt = d_testers.find( sel ); - if( itt != d_testers.end() ){ - Assert(d_testers_exp.find(sel) != d_testers_exp.end()); - assertTesterInternal( (*itt).second, sel, d_testers_exp[sel], lemmas ); - } - } - Trace("sygus-sb-debug") << "...finished" << std::endl; - } -} - -Node SygusSymBreakNew::getRelevancyCondition( Node n ) { - std::map< Node, Node >::iterator itr = d_rlv_cond.find( n ); - if( itr==d_rlv_cond.end() ){ - Node cond; - if( n.getKind()==APPLY_SELECTOR_TOTAL && options::sygusSymBreakRlv() ){ - TypeNode ntn = n[0].getType(); - Type nt = ntn.toType(); - const Datatype& dt = ((DatatypeType)nt).getDatatype(); - Expr selExpr = n.getOperator().toExpr(); - if( options::dtSharedSelectors() ){ - std::vector< Node > disj; - bool excl = false; - for( unsigned i=0; imkNode( - kind::AND, disj); - } - }else{ - int sindex = Datatype::cindexOf( selExpr ); - Assert(sindex != -1); - cond = utils::mkTester(n[0], sindex, dt).negate(); - } - Node c1 = getRelevancyCondition( n[0] ); - if( cond.isNull() ){ - cond = c1; - }else if( !c1.isNull() ){ - cond = NodeManager::currentNM()->mkNode(kind::OR, cond, c1); - } - } - Trace("sygus-sb-debug2") << "Relevancy condition for " << n << " is " << cond << std::endl; - d_rlv_cond[n] = cond; - return cond; - }else{ - return itr->second; - } -} - -Node SygusSymBreakNew::getTraversalPredicate(TypeNode tn, Node n, bool isPre) -{ - unsigned index = isPre ? 0 : 1; - std::map::iterator itt = d_traversal_pred[index][tn].find(n); - if (itt != d_traversal_pred[index][tn].end()) - { - return itt->second; - } - NodeManager* nm = NodeManager::currentNM(); - std::vector types; - types.push_back(tn); - TypeNode ptn = nm->mkPredicateType(types); - Node pred = nm->mkSkolem(isPre ? "pre" : "post", ptn); - d_traversal_pred[index][tn][n] = pred; - return pred; -} - -Node SygusSymBreakNew::eliminateTraversalPredicates(Node n) -{ - NodeManager* nm = NodeManager::currentNM(); - std::unordered_map visited; - std::unordered_map::iterator it; - std::map::iterator ittb; - std::vector visit; - TNode cur; - visit.push_back(n); - do - { - cur = visit.back(); - visit.pop_back(); - it = visited.find(cur); - - if (it == visited.end()) - { - if (cur.getKind() == APPLY_UF) - { - Assert(cur.getType().isBoolean()); - Assert(cur.getNumChildren() == 1 - && (cur[0].isVar() || cur[0].getKind() == APPLY_SELECTOR_TOTAL)); - ittb = d_traversal_bool.find(cur); - Node ret; - if (ittb == d_traversal_bool.end()) - { - std::stringstream ss; - ss << "v_" << cur; - ret = nm->mkSkolem(ss.str(), cur.getType()); - d_traversal_bool[cur] = ret; - } - else - { - ret = ittb->second; - } - visited[cur] = ret; - } - else - { - visited[cur] = Node::null(); - visit.push_back(cur); - for (const Node& cn : cur) - { - visit.push_back(cn); - } - } - } - else if (it->second.isNull()) - { - Node ret = cur; - bool childChanged = false; - std::vector children; - if (cur.getMetaKind() == metakind::PARAMETERIZED) - { - children.push_back(cur.getOperator()); - } - for (const Node& cn : cur) - { - it = visited.find(cn); - Assert(it != visited.end()); - Assert(!it->second.isNull()); - childChanged = childChanged || cn != it->second; - children.push_back(it->second); - } - if (childChanged) - { - ret = nm->mkNode(cur.getKind(), children); - } - visited[cur] = ret; - } - } while (!visit.empty()); - Assert(visited.find(n) != visited.end()); - Assert(!visited.find(n)->second.isNull()); - return visited[n]; -} - -Node SygusSymBreakNew::getSimpleSymBreakPred(Node e, - TypeNode tn, - int tindex, - unsigned depth, - bool usingSymCons, - bool isVarAgnostic) -{ - // Compute the tuple of expressions we hash the predicate for. - - // The hash value in d_simple_sb_pred for the given options - unsigned optHashVal = usingSymCons ? 1 : 0; - if (isVarAgnostic && depth == 0) - { - // variable agnostic symmetry breaking only applies at depth 0 - optHashVal = optHashVal + 2; - } - else - { - // enumerator is only specific to variable agnostic symmetry breaking - e = Node::null(); - } - std::map& ssbCache = - d_simple_sb_pred[e][tn][tindex][optHashVal]; - std::map::iterator it = ssbCache.find(depth); - if (it != ssbCache.end()) - { - return it->second; - } - // this function is only called on sygus datatype types - Assert(tn.isDatatype()); - NodeManager* nm = NodeManager::currentNM(); - Node n = getFreeVar(tn); - const Datatype& dt = static_cast(tn.toType()).getDatatype(); - Assert(dt.isSygus()); - Assert(tindex >= 0 && tindex < static_cast(dt.getNumConstructors())); - - Trace("sygus-sb-simple-debug") - << "Simple symmetry breaking for " << dt.getName() << ", constructor " - << dt[tindex].getName() << ", at depth " << depth << std::endl; - - quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn); - // get the sygus operator - Node sop = Node::fromExpr(dt[tindex].getSygusOp()); - // get the kind of the constructor operator - Kind nk = ti.getConsNumKind(tindex); - // is this the any-constant constructor? - bool isAnyConstant = sop.getAttribute(SygusAnyConstAttribute()); - - // conjunctive conclusion of lemma - std::vector sbp_conj; - - // the number of (sygus) arguments - // Notice if this is an any-constant constructor, its child is not a - // sygus child, hence we set to 0 here. - unsigned dt_index_nargs = isAnyConstant ? 0 : dt[tindex].getNumArgs(); - - // builtin type - TypeNode tnb = TypeNode::fromType(dt.getSygusType()); - // get children - std::vector children; - for (unsigned j = 0; j < dt_index_nargs; j++) - { - Node sel = nm->mkNode( - APPLY_SELECTOR_TOTAL, - Node::fromExpr(dt[tindex].getSelectorInternal(tn.toType(), j)), - n); - Assert(sel.getType().isDatatype()); - children.push_back(sel); - } - - if (depth == 0) - { - Trace("sygus-sb-simple-debug") << " Size..." << std::endl; - // fairness - if (options::sygusFair() == SYGUS_FAIR_DT_SIZE && !isAnyConstant) - { - Node szl = nm->mkNode(DT_SIZE, n); - Node szr = nm->mkNode(DT_SIZE, utils::getInstCons(n, dt, tindex)); - szr = Rewriter::rewrite(szr); - sbp_conj.push_back(szl.eqNode(szr)); - } - if (isVarAgnostic) - { - // Enforce symmetry breaking lemma template for each x_i: - // template z. - // is-x_i( z ) => pre_{x_{i-1}}( z ) - // for args a = 1...n - // // pre-definition - // pre_{x_i}( z.a ) = a=0 ? pre_{x_i}( z ) : post_{x_i}( z.{a-1} ) - // post_{x_i}( z ) = post_{x_i}( z.n ) OR is-x_i( z ) - - // Notice that we are constructing a symmetry breaking template - // under the condition that is-C( z ) holds in this method, where C - // is the tindex^{th} constructor of dt. Thus, is-x_i( z ) is either - // true or false below. - - Node svl = Node::fromExpr(dt.getSygusVarList()); - // for each variable - Assert(!e.isNull()); - TypeNode etn = e.getType(); - // for each variable in the sygus type - for (const Node& var : svl) - { - quantifiers::SygusTypeInfo& eti = d_tds->getTypeInfo(etn); - unsigned sc = eti.getSubclassForVar(var); - if (eti.getNumSubclassVars(sc) == 1) - { - // unique variable in singleton subclass, skip - continue; - } - // Compute the "predecessor" variable in the subclass of var. - Node predVar; - unsigned scindex = 0; - if (eti.getIndexInSubclassForVar(var, scindex)) - { - if (scindex > 0) - { - predVar = eti.getVarSubclassIndex(sc, scindex - 1); - } - } - Node preParentOp = getTraversalPredicate(tn, var, true); - Node preParent = nm->mkNode(APPLY_UF, preParentOp, n); - Node prev = preParent; - // for each child - for (const Node& child : children) - { - TypeNode ctn = child.getType(); - // my pre is equal to the previous - Node preCurrOp = getTraversalPredicate(ctn, var, true); - Node preCurr = nm->mkNode(APPLY_UF, preCurrOp, child); - // definition of pre, for each argument - sbp_conj.push_back(preCurr.eqNode(prev)); - Node postCurrOp = getTraversalPredicate(ctn, var, false); - prev = nm->mkNode(APPLY_UF, postCurrOp, child); - } - Node postParent = getTraversalPredicate(tn, var, false); - Node finish = nm->mkNode(APPLY_UF, postParent, n); - // check if we are constructing the symmetry breaking predicate for the - // variable in question. If so, is-{x_i}( z ) is true. - int varCn = ti.getOpConsNum(var); - if (varCn == static_cast(tindex)) - { - // the post value is true - prev = d_true; - // requirement : If I am the variable, I must have seen - // the variable before this one in its type class. - if (!predVar.isNull()) - { - Node preParentPredVarOp = getTraversalPredicate(tn, predVar, true); - Node preParentPredVar = nm->mkNode(APPLY_UF, preParentPredVarOp, n); - sbp_conj.push_back(preParentPredVar); - } - } - // definition of post - sbp_conj.push_back(finish.eqNode(prev)); - } - } - } - - // if we are the "any constant" constructor, we do no symmetry breaking - // only do simple symmetry breaking up to depth 2 - bool doSymBreak = options::sygusSymBreak(); - if (isAnyConstant || depth > 2) - { - doSymBreak = false; - } - // symmetry breaking - if (doSymBreak) - { - // direct solving for children - // for instance, we may want to insist that the LHS of MINUS is 0 - Trace("sygus-sb-simple-debug") << " Solve children..." << std::endl; - std::map children_solved; - for (unsigned j = 0; j < dt_index_nargs; j++) - { - int i = d_ssb.solveForArgument(tn, tindex, j); - if (i >= 0) - { - children_solved[j] = i; - TypeNode ctn = children[j].getType(); - const Datatype& cdt = - static_cast(ctn.toType()).getDatatype(); - Assert(i < static_cast(cdt.getNumConstructors())); - sbp_conj.push_back(utils::mkTester(children[j], i, cdt)); - } - } - - // depth 1 symmetry breaking : talks about direct children - if (depth == 1) - { - if (nk != UNDEFINED_KIND) - { - Trace("sygus-sb-simple-debug") - << " Equality reasoning about children..." << std::endl; - // commutative operators - if (quantifiers::TermUtil::isComm(nk)) - { - if (children.size() == 2 - && children[0].getType() == children[1].getType()) - { - Node order_pred = getTermOrderPredicate(children[0], children[1]); - sbp_conj.push_back(order_pred); - } - } - // operators whose arguments are non-additive (e.g. should be different) - std::vector deq_child[2]; - if (children.size() == 2 && children[0].getType() == tn) - { - bool argDeq = false; - if (quantifiers::TermUtil::isNonAdditive(nk)) - { - argDeq = true; - } - else - { - // other cases of rewriting x k x -> x' - Node req_const; - if (nk == GT || nk == LT || nk == XOR || nk == MINUS - || nk == BITVECTOR_SUB || nk == BITVECTOR_XOR - || nk == BITVECTOR_UREM_TOTAL) - { - // must have the zero element - req_const = quantifiers::TermUtil::mkTypeValue(tnb, 0); - } - else if (nk == EQUAL || nk == LEQ || nk == GEQ - || nk == BITVECTOR_XNOR) - { - req_const = quantifiers::TermUtil::mkTypeMaxValue(tnb); - } - // cannot do division since we have to consider when both are zero - if (!req_const.isNull()) - { - if (ti.hasConst(req_const)) - { - argDeq = true; - } - } - } - if (argDeq) - { - deq_child[0].push_back(0); - deq_child[1].push_back(1); - } - } - if (nk == ITE || nk == STRING_STRREPL || nk == STRING_STRREPLALL) - { - deq_child[0].push_back(1); - deq_child[1].push_back(2); - } - if (nk == STRING_STRREPL || nk == STRING_STRREPLALL) - { - deq_child[0].push_back(0); - deq_child[1].push_back(1); - } - // this code adds simple symmetry breaking predicates of the form - // d.i != d.j, for example if we are considering an ITE constructor, - // we enforce that d.1 != d.2 since otherwise the ITE can be - // simplified. - for (unsigned i = 0, size = deq_child[0].size(); i < size; i++) - { - unsigned c1 = deq_child[0][i]; - unsigned c2 = deq_child[1][i]; - TypeNode tnc = children[c1].getType(); - // we may only apply this symmetry breaking scheme (which introduces - // disequalities) if the types are infinite. - if (tnc == children[c2].getType() && !tnc.isInterpretedFinite()) - { - Node sym_lem_deq = children[c1].eqNode(children[c2]).negate(); - // notice that this symmetry breaking still allows for - // ite( C, any_constant(x), any_constant(y) ) - // since any_constant takes a builtin argument. - sbp_conj.push_back(sym_lem_deq); - } - } - - Trace("sygus-sb-simple-debug") << " Redundant operators..." - << std::endl; - // singular arguments (e.g. 0 for mult) - // redundant arguments (e.g. 0 for plus, 1 for mult) - // right-associativity - // simple rewrites - // explanation of why not all children of this are constant - std::vector exp_not_all_const; - // is the above explanation valid? This is set to false if - // one child does not have a constant, hence making the explanation - // false. - bool exp_not_all_const_valid = dt_index_nargs > 0; - // does the parent have an any constant constructor? - bool usingAnyConstCons = - usingSymCons && (ti.getAnyConstantConsNum() != -1); - for (unsigned j = 0; j < dt_index_nargs; j++) - { - Node nc = children[j]; - // if not already solved - if (children_solved.find(j) != children_solved.end()) - { - continue; - } - TypeNode tnc = nc.getType(); - quantifiers::SygusTypeInfo& cti = d_tds->getTypeInfo(tnc); - int anyc_cons_num = cti.getAnyConstantConsNum(); - const Datatype& cdt = - static_cast(tnc.toType()).getDatatype(); - std::vector exp_const; - for (unsigned k = 0, ncons = cdt.getNumConstructors(); k < ncons; k++) - { - Kind nck = cti.getConsNumKind(k); - bool red = false; - Node tester = utils::mkTester(nc, k, cdt); - // check if the argument is redundant - if (static_cast(k) == anyc_cons_num) - { - exp_const.push_back(tester); - } - else if (nck != UNDEFINED_KIND) - { - Trace("sygus-sb-simple-debug") << " argument " << j << " " << k - << " is : " << nck << std::endl; - red = !d_ssb.considerArgKind(tnc, tn, nck, nk, j); - } - else - { - Node cc = cti.getConsNumConst(k); - if (!cc.isNull()) - { - Trace("sygus-sb-simple-debug") - << " argument " << j << " " << k << " is constant : " << cc - << std::endl; - red = !d_ssb.considerConst(tnc, tn, cc, nk, j); - if (usingAnyConstCons) - { - // we only consider concrete constant constructors - // of children if we have the "any constant" constructor - // otherwise, we would disallow solutions for grammars - // like the following: - // A -> B+B - // B -> 4 | 8 | 100 - // where A allows all constants but is not using the - // any constant constructor. - exp_const.push_back(tester); - } - } - else - { - // defined function? - } - } - if (red) - { - Trace("sygus-sb-simple-debug") << " ...redundant." << std::endl; - sbp_conj.push_back(tester.negate()); - } - } - if (exp_const.empty()) - { - exp_not_all_const_valid = false; - } - else - { - Node ecn = exp_const.size() == 1 ? exp_const[0] - : nm->mkNode(OR, exp_const); - exp_not_all_const.push_back(ecn.negate()); - } - } - // explicitly handle constants and "any constant" constructors - // if this type admits any constant, then at least one of my - // children must not be a constant or the "any constant" constructor - if (dt.getSygusAllowConst() && exp_not_all_const_valid) - { - Assert(!exp_not_all_const.empty()); - Node expaan = exp_not_all_const.size() == 1 - ? exp_not_all_const[0] - : nm->mkNode(OR, exp_not_all_const); - Trace("sygus-sb-simple-debug") - << "Ensure not all constant: " << expaan << std::endl; - sbp_conj.push_back(expaan); - } - } - else - { - // defined function? - } - } - else if (depth == 2) - { - // commutative operators - if (quantifiers::TermUtil::isComm(nk) && children.size() == 2 - && children[0].getType() == tn && children[1].getType() == tn) - { - // chainable - Node child11 = nm->mkNode( - APPLY_SELECTOR_TOTAL, - Node::fromExpr(dt[tindex].getSelectorInternal(tn.toType(), 1)), - children[0]); - Assert(child11.getType() == children[1].getType()); - Node order_pred_trans = - nm->mkNode(OR, - utils::mkTester(children[0], tindex, dt).negate(), - getTermOrderPredicate(child11, children[1])); - sbp_conj.push_back(order_pred_trans); - } - } - } - - Node sb_pred; - if (!sbp_conj.empty()) - { - sb_pred = - sbp_conj.size() == 1 ? sbp_conj[0] : nm->mkNode(kind::AND, sbp_conj); - Trace("sygus-sb-simple") - << "Simple predicate for " << tn << " index " << tindex << " (" << nk - << ") at depth " << depth << " : " << std::endl; - Trace("sygus-sb-simple") << " " << sb_pred << std::endl; - sb_pred = nm->mkNode(OR, utils::mkTester(n, tindex, dt).negate(), sb_pred); - } - d_simple_sb_pred[e][tn][tindex][optHashVal][depth] = sb_pred; - return sb_pred; -} - -TNode SygusSymBreakNew::getFreeVar( TypeNode tn ) { - return d_tds->getFreeVar(tn, 0); -} - -void SygusSymBreakNew::registerSearchTerm( TypeNode tn, unsigned d, Node n, bool topLevel, std::vector< Node >& lemmas ) { - //register this term - std::unordered_map::iterator ita = - d_term_to_anchor.find(n); - Assert(ita != d_term_to_anchor.end()); - Node a = ita->second; - Assert(!a.isNull()); - 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() ){ - Trace("sygus-sb-debug") << " register search term : " << n << " at depth " << d << ", type=" << tn << ", tl=" << topLevel << std::endl; - d_cache[a].d_search_terms[tn][d].push_back( n ); - if( !options::sygusSymBreakLazy() ){ - addSymBreakLemmasFor( tn, n, d, lemmas ); - } - } -} - -Node SygusSymBreakNew::registerSearchValue(Node a, - Node n, - Node nv, - unsigned d, - std::vector& lemmas, - bool isVarAgnostic, - bool doSym) -{ - Assert(n.getType().isComparableTo(nv.getType())); - TypeNode tn = n.getType(); - if (!tn.isDatatype()) - { - // don't register non-datatype terms, instead we return the - // selector chain n. - return n; - } - const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); - if (!dt.isSygus()) - { - // don't register non-sygus-datatype terms - return n; - } - Assert(nv.getKind() == APPLY_CONSTRUCTOR); - NodeManager* nm = NodeManager::currentNM(); - // we call the body of this function in a bottom-up fashion - // this ensures that the "abstraction" of the model value is available - if( nv.getNumChildren()>0 ){ - unsigned cindex = utils::indexOf(nv.getOperator()); - std::vector rcons_children; - rcons_children.push_back(nv.getOperator()); - bool childrenChanged = false; - for (unsigned i = 0, nchild = nv.getNumChildren(); i < nchild; i++) - { - Node sel = nm->mkNode( - APPLY_SELECTOR_TOTAL, - Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)), - n); - Node nvc = registerSearchValue(a, - sel, - nv[i], - d + 1, - lemmas, - isVarAgnostic, - doSym && (!isVarAgnostic || i == 0)); - if (nvc.isNull()) - { - return Node::null(); - } - rcons_children.push_back(nvc); - childrenChanged = childrenChanged || nvc != nv[i]; - } - // reconstruct the value, which may be a skeleton - if (childrenChanged) - { - nv = nm->mkNode(APPLY_CONSTRUCTOR, rcons_children); - } - } - if (!doSym) - { - return nv; - } - Trace("sygus-sb-debug2") << "Registering search value " << n << " -> " << nv << std::endl; - std::map var_count; - Node cnv = d_tds->canonizeBuiltin(nv, var_count); - Trace("sygus-sb-debug") << " ...canonized value is " << cnv << std::endl; - // must do this for all nodes, regardless of top-level - if (d_cache[a].d_search_val_proc.find(cnv) - == d_cache[a].d_search_val_proc.end()) - { - d_cache[a].d_search_val_proc.insert(cnv); - // get the root (for PBE symmetry breaking) - Assert(d_anchor_to_conj.find(a) != d_anchor_to_conj.end()); - quantifiers::SynthConjecture* aconj = d_anchor_to_conj[a]; - Assert(aconj != NULL); - Trace("sygus-sb-debug") << " ...register search value " << cnv - << ", type=" << tn << std::endl; - Node bv = d_tds->sygusToBuiltin(cnv, tn); - Trace("sygus-sb-debug") << " ......builtin is " << bv << std::endl; - Node bvr = d_tds->getExtRewriter()->extendedRewrite(bv); - Trace("sygus-sb-debug") << " ......search value rewrites to " << bvr << std::endl; - Trace("dt-sygus") << " * DT builtin : " << n << " -> " << bvr << std::endl; - unsigned sz = d_tds->getSygusTermSize( nv ); - if( d_tds->involvesDivByZero( bvr ) ){ - quantifiers::DivByZeroSygusInvarianceTest dbzet; - Trace("sygus-sb-mexp-debug") << "Minimize explanation for div-by-zero in " - << bv << std::endl; - registerSymBreakLemmaForValue( - a, nv, dbzet, Node::null(), var_count, lemmas); - return Node::null(); - }else{ - std::unordered_map::iterator itsv = - d_cache[a].d_search_val[tn].find(bvr); - Node bad_val_bvr; - bool by_examples = false; - if( itsv==d_cache[a].d_search_val[tn].end() ){ - // TODO (github #1210) conjecture-specific symmetry breaking - // this should be generalized and encapsulated within the - // SynthConjecture class. - // Is it equivalent under examples? - Node bvr_equiv; - if (options::sygusSymBreakPbe()) - { - if (aconj->getPbe()->hasExamples(a)) - { - bvr_equiv = aconj->getPbe()->addSearchVal(tn, a, bvr); - } - } - if( !bvr_equiv.isNull() ){ - if( bvr_equiv!=bvr ){ - Trace("sygus-sb-debug") << "......adding search val for " << bvr << " returned " << bvr_equiv << std::endl; - Assert(d_cache[a].d_search_val[tn].find(bvr_equiv) - != d_cache[a].d_search_val[tn].end()); - Trace("sygus-sb-debug") << "......search value was " << d_cache[a].d_search_val[tn][bvr_equiv] << std::endl; - if( Trace.isOn("sygus-sb-exc") ){ - Node prev = d_tds->sygusToBuiltin( d_cache[a].d_search_val[tn][bvr_equiv], tn ); - Trace("sygus-sb-exc") << " ......programs " << prev << " and " << bv << " are equivalent up to examples." << std::endl; - } - bad_val_bvr = bvr_equiv; - by_examples = true; - } - } - //store rewritten values, regardless of whether it will be considered - d_cache[a].d_search_val[tn][bvr] = nv; - d_cache[a].d_search_val_sz[tn][bvr] = sz; - }else{ - bad_val_bvr = bvr; - if( Trace.isOn("sygus-sb-exc") ){ - Node prev_bv = d_tds->sygusToBuiltin( itsv->second, tn ); - Trace("sygus-sb-exc") << " ......programs " << prev_bv << " and " << bv << " rewrite to " << bvr << "." << std::endl; - } - } - - if (options::sygusRewVerify()) - { - if (bv != bvr) - { - // add to the sampler database object - std::map::iterator its = - d_sampler[a].find(tn); - if (its == d_sampler[a].end()) - { - d_sampler[a][tn].initializeSygus( - d_tds, nv, options::sygusSamples(), false); - its = d_sampler[a].find(tn); - } - // check equivalent - its->second.checkEquivalent(bv, bvr); - } - } - - if( !bad_val_bvr.isNull() ){ - Node bad_val = nv; - Node bad_val_o = d_cache[a].d_search_val[tn][bad_val_bvr]; - Assert(d_cache[a].d_search_val_sz[tn].find(bad_val_bvr) - != d_cache[a].d_search_val_sz[tn].end()); - unsigned prev_sz = d_cache[a].d_search_val_sz[tn][bad_val_bvr]; - bool doFlip = (prev_sz > sz); - if (doFlip) - { - //swap : the excluded value is the previous - d_cache[a].d_search_val_sz[tn][bad_val_bvr] = sz; - bad_val = d_cache[a].d_search_val[tn][bad_val_bvr]; - bad_val_o = nv; - if (Trace.isOn("sygus-sb-exc")) - { - Trace("sygus-sb-exc") << "Flip : exclude "; - quantifiers::TermDbSygus::toStreamSygus("sygus-sb-exc", bad_val); - Trace("sygus-sb-exc") << " instead of "; - quantifiers::TermDbSygus::toStreamSygus("sygus-sb-exc", bad_val_o); - Trace("sygus-sb-exc") << ", since its size is " << sz << " < " - << prev_sz << std::endl; - } - sz = prev_sz; - } - if( Trace.isOn("sygus-sb-exc") ){ - Node bad_val_bv = d_tds->sygusToBuiltin( bad_val, tn ); - Trace("sygus-sb-exc") << " ........exclude : " << bad_val_bv; - if( by_examples ){ - Trace("sygus-sb-exc") << " (by examples)"; - } - Trace("sygus-sb-exc") << std::endl; - } - Assert(d_tds->getSygusTermSize(bad_val) == sz); - - // generalize the explanation for why the analog of bad_val - // is equivalent to bvr - quantifiers::EquivSygusInvarianceTest eset; - eset.init(d_tds, tn, aconj, a, bvr); - - Trace("sygus-sb-mexp-debug") << "Minimize explanation for eval[" << d_tds->sygusToBuiltin( bad_val ) << "] = " << bvr << std::endl; - registerSymBreakLemmaForValue( - a, bad_val, eset, bad_val_o, var_count, lemmas); - - // other generalization criteria go here - - // If the exclusion was flipped, we are excluding a previous value - // instead of the current one. Hence, the current value is a legal - // value that we will consider. - if (!doFlip) - { - return Node::null(); - } - } - } - } - return nv; -} - -void SygusSymBreakNew::registerSymBreakLemmaForValue( - Node a, - Node val, - quantifiers::SygusInvarianceTest& et, - Node valr, - std::map& var_count, - std::vector& lemmas) -{ - TypeNode tn = val.getType(); - Node x = getFreeVar(tn); - unsigned sz = d_tds->getSygusTermSize(val); - std::vector exp; - d_tds->getExplain()->getExplanationFor(x, val, exp, et, valr, var_count, sz); - Node lem = - exp.size() == 1 ? exp[0] : NodeManager::currentNM()->mkNode(AND, exp); - lem = lem.negate(); - Trace("sygus-sb-exc") << " ........exc lemma is " << lem << ", size = " << sz - << std::endl; - registerSymBreakLemma(tn, lem, sz, a, lemmas); -} - -void SygusSymBreakNew::registerSymBreakLemma( TypeNode tn, Node lem, unsigned sz, Node a, std::vector< Node >& lemmas ) { - // lem holds for all terms of type tn, and is applicable to terms of size sz - Trace("sygus-sb-debug") << " register sym break lemma : " << lem - << std::endl; - Trace("sygus-sb-debug") << " anchor : " << a << std::endl; - Trace("sygus-sb-debug") << " type : " << tn << std::endl; - Trace("sygus-sb-debug") << " size : " << sz << std::endl; - Assert(!a.isNull()); - d_cache[a].d_sb_lemmas[tn][sz].push_back( lem ); - TNode x = getFreeVar( tn ); - unsigned csz = getSearchSizeForAnchor( a ); - int max_depth = ((int)csz)-((int)sz); - NodeManager* nm = NodeManager::currentNM(); - for( int d=0; d<=max_depth; d++ ){ - std::map< unsigned, std::vector< Node > >::iterator itt = d_cache[a].d_search_terms[tn].find( d ); - if( itt!=d_cache[a].d_search_terms[tn].end() ){ - for (const TNode& t : itt->second) - { - if (!options::sygusSymBreakLazy() - || d_active_terms.find(t) != d_active_terms.end()) - { - Node slem = lem.substitute(x, t); - Node rlv = getRelevancyCondition(t); - if (!rlv.isNull()) - { - slem = nm->mkNode(OR, rlv, slem); - } - lemmas.push_back(slem); - } - } - } - } -} -void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, std::vector< Node >& lemmas ) { - Assert(d_term_to_anchor.find(t) != d_term_to_anchor.end()); - Node a = d_term_to_anchor[t]; - addSymBreakLemmasFor( tn, t, d, a, lemmas ); -} - -void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, Node a, std::vector< Node >& lemmas ) { - Assert(t.getType() == tn); - Assert(!a.isNull()); - Trace("sygus-sb-debug2") << "add sym break lemmas for " << t << " " << d - << " " << a << std::endl; - std::map< TypeNode, std::map< unsigned, std::vector< Node > > >::iterator its = d_cache[a].d_sb_lemmas.find( tn ); - Node rlv = getRelevancyCondition(t); - NodeManager* nm = NodeManager::currentNM(); - if( its != d_cache[a].d_sb_lemmas.end() ){ - TNode x = getFreeVar( tn ); - //get symmetry breaking lemmas for this term - unsigned csz = getSearchSizeForAnchor( a ); - int max_sz = ((int)csz) - ((int)d); - Trace("sygus-sb-debug2") - << "add lemmas up to size " << max_sz << ", which is (search_size) " - << csz << " - (depth) " << d << std::endl; - std::unordered_map cache; - for( std::map< unsigned, std::vector< Node > >::iterator it = its->second.begin(); it != its->second.end(); ++it ){ - if( (int)it->first<=max_sz ){ - for (const Node& lem : it->second) - { - Node slem = lem.substitute(x, t, cache); - // add the relevancy condition for t - if (!rlv.isNull()) - { - slem = nm->mkNode(OR, rlv, slem); - } - lemmas.push_back(slem); - } - } - } - } - Trace("sygus-sb-debug2") << "...finished." << std::endl; -} - -void SygusSymBreakNew::preRegisterTerm( TNode n, std::vector< Node >& lemmas ) { - if( n.isVar() ){ - Trace("sygus-sb-debug") << "Pre-register variable : " << n << std::endl; - registerSizeTerm( n, lemmas ); - } -} - -void SygusSymBreakNew::registerSizeTerm(Node e, std::vector& lemmas) -{ - if (d_register_st.find(e) != d_register_st.end()) - { - // already registered - return; - } - TypeNode etn = e.getType(); - if (!etn.isDatatype()) - { - // not a datatype term - d_register_st[e] = false; - return; - } - const Datatype& dt = etn.getDatatype(); - if (!dt.isSygus()) - { - // not a sygus datatype term - d_register_st[e] = false; - return; - } - if (!d_tds->isEnumerator(e)) - { - // not sure if it is a size term or not (may be registered later?) - return; - } - d_register_st[e] = true; - Node ag = d_tds->getActiveGuardForEnumerator(e); - if (!ag.isNull()) - { - d_anchor_to_active_guard[e] = ag; - std::map>::iterator itaas = - d_anchor_to_ag_strategy.find(e); - if (itaas == d_anchor_to_ag_strategy.end()) - { - d_anchor_to_ag_strategy[e].reset( - new DecisionStrategySingleton("sygus_enum_active", - ag, - d_td->getSatContext(), - d_td->getValuation())); - } - d_td->getDecisionManager()->registerStrategy( - DecisionManager::STRAT_DT_SYGUS_ENUM_ACTIVE, - d_anchor_to_ag_strategy[e].get()); - } - Node m; - if (!ag.isNull()) - { - // if it has an active guard (it is an enumerator), use itself as measure - // term. This will enforce fairness on it independently. - m = e; - } - else - { - // otherwise we enforce fairness in a unified way for all - if (d_generic_measure_term.isNull()) - { - // choose e as master for all future terms - d_generic_measure_term = e; - } - m = d_generic_measure_term; - } - Trace("sygus-sb") << "Sygus : register size term : " << e << " with measure " - << m << std::endl; - registerMeasureTerm(m); - d_szinfo[m]->d_anchors.push_back(e); - d_anchor_to_measure_term[e] = m; - NodeManager* nm = NodeManager::currentNM(); - if (options::sygusFair() == SYGUS_FAIR_DT_SIZE) - { - // update constraints on the measure term - Node slem; - if (options::sygusFairMax()) - { - Node ds = nm->mkNode(DT_SIZE, e); - slem = nm->mkNode(LEQ, ds, d_szinfo[m]->getOrMkMeasureValue(lemmas)); - }else{ - Node mt = d_szinfo[m]->getOrMkActiveMeasureValue(lemmas); - Node new_mt = d_szinfo[m]->getOrMkActiveMeasureValue(lemmas, true); - Node ds = nm->mkNode(DT_SIZE, e); - slem = mt.eqNode(nm->mkNode(PLUS, new_mt, ds)); - } - Trace("sygus-sb") << "...size lemma : " << slem << std::endl; - lemmas.push_back(slem); - } - if (d_tds->isVariableAgnosticEnumerator(e)) - { - // if it is variable agnostic, enforce top-level constraint that says no - // variables occur pre-traversal at top-level - Node varList = Node::fromExpr(dt.getSygusVarList()); - std::vector constraints; - quantifiers::SygusTypeInfo& eti = d_tds->getTypeInfo(etn); - for (const Node& v : varList) - { - unsigned sc = eti.getSubclassForVar(v); - // no symmetry breaking occurs for variables in singleton subclasses - if (eti.getNumSubclassVars(sc) > 1) - { - Node preRootOp = getTraversalPredicate(etn, v, true); - Node preRoot = nm->mkNode(APPLY_UF, preRootOp, e); - constraints.push_back(preRoot.negate()); - } - } - if (!constraints.empty()) - { - Node preNoVar = constraints.size() == 1 ? constraints[0] - : nm->mkNode(AND, constraints); - Node preNoVarProc = eliminateTraversalPredicates(preNoVar); - Trace("sygus-sb") << "...variable order : " << preNoVarProc << std::endl; - Trace("sygus-sb-tp") << "...variable order : " << preNoVarProc - << std::endl; - lemmas.push_back(preNoVarProc); - } - } -} - -void SygusSymBreakNew::registerMeasureTerm( Node m ) { - std::map>::iterator it = - d_szinfo.find(m); - if( it==d_szinfo.end() ){ - Trace("sygus-sb") << "Sygus : register measure term : " << m << std::endl; - d_szinfo[m].reset(new SygusSizeDecisionStrategy( - m, d_td->getSatContext(), d_td->getValuation())); - // register this as a decision strategy - d_td->getDecisionManager()->registerStrategy( - DecisionManager::STRAT_DT_SYGUS_ENUM_SIZE, d_szinfo[m].get()); - } -} - -void SygusSymBreakNew::notifySearchSize( Node m, unsigned s, Node exp, std::vector< Node >& lemmas ) { - std::map>::iterator its = - d_szinfo.find(m); - Assert(its != d_szinfo.end()); - if( its->second->d_search_size.find( s )==its->second->d_search_size.end() ){ - its->second->d_search_size[s] = true; - its->second->d_search_size_exp[s] = exp; - Assert(s == 0 - || its->second->d_search_size.find(s - 1) - != its->second->d_search_size.end()); - Trace("sygus-fair") << "SygusSymBreakNew:: now considering term measure : " << s << " for " << m << std::endl; - Assert(s >= its->second->d_curr_search_size); - while( s>its->second->d_curr_search_size ){ - incrementCurrentSearchSize( m, lemmas ); - } - Trace("sygus-fair") << "...finish increment for term measure : " << s << std::endl; - /* - //re-add all testers (some may now be relevant) TODO - for( IntMap::const_iterator it = d_testers.begin(); it != d_testers.end(); - ++it ){ Node n = (*it).first; NodeMap::const_iterator itx = - d_testers_exp.find( n ); if( itx!=d_testers_exp.end() ){ int tindex = - (*it).second; Node exp = (*itx).second; assertTester( tindex, n, exp, lemmas - ); }else{ Assert( false ); - } - } - */ - } -} - -unsigned SygusSymBreakNew::getSearchSizeFor( Node n ) { - Trace("sygus-sb-debug2") << "get search size for term : " << n << std::endl; - std::unordered_map::iterator ita = - d_term_to_anchor.find(n); - Assert(ita != d_term_to_anchor.end()); - return getSearchSizeForAnchor( ita->second ); -} - -unsigned SygusSymBreakNew::getSearchSizeForAnchor( Node a ) { - Trace("sygus-sb-debug2") << "get search size for anchor : " << a << std::endl; - std::map< Node, Node >::iterator it = d_anchor_to_measure_term.find( a ); - Assert(it != d_anchor_to_measure_term.end()); - return getSearchSizeForMeasureTerm(it->second); -} - -unsigned SygusSymBreakNew::getSearchSizeForMeasureTerm(Node m) -{ - Trace("sygus-sb-debug2") << "get search size for measure : " << m << std::endl; - std::map>::iterator its = - d_szinfo.find(m); - Assert(its != d_szinfo.end()); - return its->second->d_curr_search_size; -} - -void SygusSymBreakNew::incrementCurrentSearchSize( Node m, std::vector< Node >& lemmas ) { - std::map>::iterator itsz = - d_szinfo.find(m); - Assert(itsz != d_szinfo.end()); - itsz->second->d_curr_search_size++; - Trace("sygus-fair") << " register search size " << itsz->second->d_curr_search_size << " for " << m << std::endl; - NodeManager* nm = NodeManager::currentNM(); - for( std::map< Node, SearchCache >::iterator itc = d_cache.begin(); itc != d_cache.end(); ++itc ){ - Node a = itc->first; - Trace("sygus-fair-debug") << " look at anchor " << a << "..." << std::endl; - // check whether a is bounded by m - Assert(d_anchor_to_measure_term.find(a) != d_anchor_to_measure_term.end()); - if( d_anchor_to_measure_term[a]==m ){ - for( std::map< TypeNode, std::map< unsigned, std::vector< Node > > >::iterator its = itc->second.d_sb_lemmas.begin(); - its != itc->second.d_sb_lemmas.end(); ++its ){ - TypeNode tn = its->first; - TNode x = getFreeVar( tn ); - for( std::map< unsigned, std::vector< Node > >::iterator it = its->second.begin(); it != its->second.end(); ++it ){ - unsigned sz = it->first; - int new_depth = ((int)itsz->second->d_curr_search_size) - ((int)sz); - std::map< unsigned, std::vector< Node > >::iterator itt = itc->second.d_search_terms[tn].find( new_depth ); - if( itt!=itc->second.d_search_terms[tn].end() ){ - for (const TNode& t : itt->second) - { - if (!options::sygusSymBreakLazy() - || (d_active_terms.find(t) != d_active_terms.end() - && !it->second.empty())) - { - Node rlv = getRelevancyCondition(t); - std::unordered_map cache; - for (const Node& lem : it->second) - { - Node slem = lem.substitute(x, t, cache); - slem = nm->mkNode(OR, rlv, slem); - lemmas.push_back(slem); - } - } - } - } - } - } - } - } -} - -void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { - Trace("sygus-sb") << "SygusSymBreakNew::check" << std::endl; - - // check for externally registered symmetry breaking lemmas - std::vector anchors; - if (d_tds->hasSymBreakLemmas(anchors)) - { - for (const Node& a : anchors) - { - // is this a registered enumerator? - if (d_register_st.find(a) != d_register_st.end()) - { - // symmetry breaking lemmas should only be for enumerators - Assert(d_register_st[a]); - // If this is a non-basic enumerator, process its symmetry breaking - // clauses. Since this class is not responsible for basic enumerators, - // their symmetry breaking clauses are ignored. - if (!d_tds->isBasicEnumerator(a)) - { - std::vector sbl; - d_tds->getSymBreakLemmas(a, sbl); - for (const Node& lem : sbl) - { - if (d_tds->isSymBreakLemmaTemplate(lem)) - { - // register the lemma template - TypeNode tn = d_tds->getTypeForSymBreakLemma(lem); - unsigned sz = d_tds->getSizeForSymBreakLemma(lem); - registerSymBreakLemma(tn, lem, sz, a, lemmas); - } - else - { - Trace("dt-sygus-debug") - << "DT sym break lemma : " << lem << std::endl; - // it is a normal lemma - lemmas.push_back(lem); - } - } - d_tds->clearSymBreakLemmas(a); - } - } - } - if (!lemmas.empty()) - { - return; - } - } - - // register search values, add symmetry breaking lemmas if applicable - std::vector es; - d_tds->getEnumerators(es); - bool needsRecheck = false; - // for each enumerator registered to d_tds - for (Node& prog : es) - { - if (d_register_st.find(prog) == d_register_st.end()) - { - // not yet registered, do so now - registerSizeTerm(prog, lemmas); - needsRecheck = true; - } - else - { - Trace("dt-sygus-debug") << "Checking model value of " << prog << "..." - << std::endl; - Assert(prog.getType().isDatatype()); - Node progv = d_td->getValuation().getModel()->getValue( prog ); - if (Trace.isOn("dt-sygus")) - { - Trace("dt-sygus") << "* DT model : " << prog << " -> "; - std::stringstream ss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(ss, progv); - Trace("dt-sygus") << ss.str() << std::endl; - } - // first check that the value progv for prog is what we expected - bool isExc = true; - if (checkValue(prog, progv, 0, lemmas)) - { - isExc = false; - //debugging : ensure fairness was properly handled - if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){ - Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, prog ); - Node prog_szv = d_td->getValuation().getModel()->getValue( prog_sz ); - Node progv_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, progv ); - - Trace("sygus-sb") << " Mv[" << prog << "] = " << progv << ", size = " << prog_szv << std::endl; - if( prog_szv.getConst().getNumerator().toUnsignedInt() > getSearchSizeForAnchor( prog ) ){ - AlwaysAssert(false); - Node szlem = NodeManager::currentNM()->mkNode( kind::OR, prog.eqNode( progv ).negate(), - prog_sz.eqNode( progv_sz ) ); - Trace("sygus-sb-warn") << "SygusSymBreak : WARNING : adding size correction : " << szlem << std::endl; - lemmas.push_back(szlem); - isExc = true; - } - } - - // register the search value ( prog -> progv ), this may invoke symmetry - // breaking - if (!isExc && options::sygusSymBreakDynamic()) - { - bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(prog); - // check that it is unique up to theory-specific rewriting and - // conjecture-specific symmetry breaking. - Node rsv = registerSearchValue( - prog, prog, progv, 0, lemmas, isVarAgnostic, true); - if (rsv.isNull()) - { - isExc = true; - Trace("sygus-sb") << " SygusSymBreakNew::check: ...added new symmetry breaking lemma for " << prog << "." << std::endl; - } - else - { - Trace("dt-sygus") << " ...success." << std::endl; - } - } - } - SygusSymBreakOkAttribute ssbo; - prog.setAttribute(ssbo, !isExc); - } - } - Trace("sygus-sb") << "SygusSymBreakNew::check: finished." << std::endl; - if (needsRecheck) - { - Trace("sygus-sb") << " SygusSymBreakNew::rechecking..." << std::endl; - return check(lemmas); - } - - if (Trace.isOn("cegqi-engine") && !d_szinfo.empty()) - { - if (lemmas.empty()) - { - Trace("cegqi-engine") << "*** Sygus : passed datatypes check. term size(s) : "; - for (std::pair>& - p : d_szinfo) - { - SygusSizeDecisionStrategy* s = p.second.get(); - Trace("cegqi-engine") << s->d_curr_search_size << " "; - } - Trace("cegqi-engine") << std::endl; - } - else - { - Trace("cegqi-engine") - << "*** Sygus : produced symmetry breaking lemmas" << std::endl; - for (const Node& lem : lemmas) - { - Trace("cegqi-engine-debug") << " " << lem << std::endl; - } - } - } -} - -bool SygusSymBreakNew::checkValue(Node n, - Node vn, - int ind, - std::vector& lemmas) -{ - if (vn.getKind() != kind::APPLY_CONSTRUCTOR) - { - // all datatype terms should be constant here - Assert(!vn.getType().isDatatype()); - return true; - } - NodeManager* nm = NodeManager::currentNM(); - if (Trace.isOn("sygus-sb-check-value")) - { - Node prog_sz = nm->mkNode(DT_SIZE, n); - Node prog_szv = d_td->getValuation().getModel()->getValue( prog_sz ); - for( int i=0; igetEqualityEngine()->hasTerm(tst); - Node tstrep; - if (hastst) - { - tstrep = d_td->getEqualityEngine()->getRepresentative(tst); - } - if (!hastst || tstrep != d_true) - { - Trace("sygus-check-value") << "- has tester : " << tst << " : " - << (hastst ? "true" : "false"); - Trace("sygus-check-value") << ", value=" << tstrep << std::endl; - if( !hastst ){ - // This should not happen generally, it is caused by a sygus term not - // being assigned a tester. - Node split = utils::mkSplit(n, dt); - Trace("sygus-sb") << " SygusSymBreakNew::check: ...WARNING: considered " - "missing split for " - << n << "." << std::endl; - Assert(!split.isNull()); - lemmas.push_back( split ); - return false; - } - } - for( unsigned i=0; imkNode( - APPLY_SELECTOR_TOTAL, - Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)), - n); - if (!checkValue(sel, vn[i], ind + 1, lemmas)) - { - return false; - } - } - return true; -} - -Node SygusSymBreakNew::getCurrentTemplate( Node n, std::map< TypeNode, int >& var_count ) { - if( d_active_terms.find( n )!=d_active_terms.end() ){ - TypeNode tn = n.getType(); - IntMap::const_iterator it = d_testers.find( n ); - Assert(it != d_testers.end()); - const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); - int tindex = (*it).second; - Assert(tindex >= 0); - Assert(tindex < (int)dt.getNumConstructors()); - std::vector< Node > children; - children.push_back( Node::fromExpr( dt[tindex].getConstructor() ) ); - for( unsigned i=0; imkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( tn.toType(), i ) ), n ); - Node cc = getCurrentTemplate( sel, var_count ); - children.push_back( cc ); - } - return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); - }else{ - return d_tds->getFreeVarInc( n.getType(), var_count ); - } -} - -Node SygusSymBreakNew::SygusSizeDecisionStrategy::getOrMkMeasureValue( - std::vector& lemmas) -{ - if (d_measure_value.isNull()) - { - d_measure_value = NodeManager::currentNM()->mkSkolem( - "mt", NodeManager::currentNM()->integerType()); - lemmas.push_back(NodeManager::currentNM()->mkNode( - kind::GEQ, - d_measure_value, - NodeManager::currentNM()->mkConst(Rational(0)))); - } - return d_measure_value; -} - -Node SygusSymBreakNew::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue( - std::vector& lemmas, bool mkNew) -{ - if (mkNew) - { - Node new_mt = NodeManager::currentNM()->mkSkolem( - "mt", NodeManager::currentNM()->integerType()); - lemmas.push_back(NodeManager::currentNM()->mkNode( - kind::GEQ, new_mt, NodeManager::currentNM()->mkConst(Rational(0)))); - d_measure_value_active = new_mt; - } - else if (d_measure_value_active.isNull()) - { - d_measure_value_active = getOrMkMeasureValue(lemmas); - } - return d_measure_value_active; -} - -Node SygusSymBreakNew::SygusSizeDecisionStrategy::mkLiteral(unsigned s) -{ - if (options::sygusFair() == SYGUS_FAIR_NONE) - { - return Node::null(); - } - if (options::sygusAbortSize() != -1 - && static_cast(s) > options::sygusAbortSize()) - { - std::stringstream ss; - ss << "Maximum term size (" << options::sygusAbortSize() - << ") for enumerative SyGuS exceeded."; - throw LogicException(ss.str()); - } - Assert(!d_this.isNull()); - NodeManager* nm = NodeManager::currentNM(); - Trace("cegqi-engine") << "******* Sygus : allocate size literal " << s - << " for " << d_this << std::endl; - return nm->mkNode(DT_SYGUS_BOUND, d_this, nm->mkConst(Rational(s))); -} - -int SygusSymBreakNew::getGuardStatus( Node g ) { - bool value; - if( d_td->getValuation().hasSatValue( g, value ) ) { - if( value ){ - return 1; - }else{ - return -1; - } - }else{ - return 0; - } -} - diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h deleted file mode 100644 index 95c259f2b..000000000 --- a/src/theory/datatypes/datatypes_sygus.h +++ /dev/null @@ -1,723 +0,0 @@ -/********************* */ -/*! \file datatypes_sygus.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Sygus utilities for theory of datatypes - ** - ** Theory of datatypes. - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__THEORY__DATATYPES__DATATYPES_SYGUS_NEW_H -#define CVC4__THEORY__DATATYPES__DATATYPES_SYGUS_NEW_H - -#include -#include - -#include "context/cdhashmap.h" -#include "context/cdhashset.h" -#include "context/cdlist.h" -#include "context/cdo.h" -#include "context/context.h" -#include "expr/datatype.h" -#include "expr/node.h" -#include "theory/datatypes/sygus_simple_sym.h" -#include "theory/quantifiers/sygus/sygus_explain.h" -#include "theory/quantifiers/sygus/synth_conjecture.h" -#include "theory/quantifiers/sygus_sampler.h" -#include "theory/quantifiers/term_database.h" - -namespace CVC4 { -namespace theory { -namespace datatypes { - -class TheoryDatatypes; - -/** - * This is the sygus extension of the decision procedure for quantifier-free - * inductive datatypes. At a high level, this class takes as input a - * set of asserted testers is-C1( x ), is-C2( x.1 ), is-C3( x.2 ), and - * generates lemmas that restrict the models of x, if x is a "sygus enumerator" - * (see TermDbSygus::registerEnumerator). - * - * Some of these techniques are described in these papers: - * "Refutation-Based Synthesis in SMT", Reynolds et al 2017. - * "Sygus Techniques in the Core of an SMT Solver", Reynolds et al 2017. - * - * This class enforces two decisions stragies via calls to registerStrategy - * of the owning theory's DecisionManager: - * (1) Positive decisions on the active guards G of enumerators e registered - * to this class. These assert "there are more values to enumerate for e". - * (2) Positive bounds (DT_SYGUS_BOUND m n) for "measure terms" m (see below), - * where n is a non-negative integer. This asserts "the measure of terms - * we are enumerating for enumerators whose measure term m is at most n", - * where measure is commonly term size, but can also be height. - * - * We prioritize decisions of form (1) before (2). Both kinds of decision are - * critical for solution completeness, which is enforced by DecisionManager. - */ -class SygusSymBreakNew -{ - typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap; - typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; - typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; - typedef context::CDHashSet NodeSet; - - public: - SygusSymBreakNew(TheoryDatatypes* td, - QuantifiersEngine* qe, - context::Context* c); - ~SygusSymBreakNew(); - /** - * Notify this class that tester for constructor tindex has been asserted for - * n. Exp is the literal corresponding to this tester. This method may add - * lemmas to the vector lemmas, for details see assertTesterInternal below. - * These lemmas are sent out on the output channel of datatypes by the caller. - */ - void assertTester(int tindex, TNode n, Node exp, std::vector& lemmas); - /** - * Notify this class that literal n has been asserted with the given - * polarity. This method may add lemmas to the vector lemmas, for instance - * based on inferring consequences of (not) n. One example is if n is - * (DT_SIZE_BOUND x n), we add the lemma: - * (DT_SIZE_BOUND x n) <=> ((DT_SIZE x) <= n ) - */ - void assertFact(Node n, bool polarity, std::vector& lemmas); - /** pre-register term n - * - * This is called when n is pre-registered with the theory of datatypes. - * If n is a sygus enumerator, then we may add lemmas to the vector lemmas - * that are used to enforce fairness regarding the size of n. - */ - void preRegisterTerm(TNode n, std::vector& lemmas); - /** check - * - * This is called at last call effort, when the current model assignment is - * satisfiable according to the quantifier-free decision procedures and a - * model is built. This method may add lemmas to the vector lemmas based - * on dynamic symmetry breaking techniques, based on the model values of - * all preregistered enumerators. - */ - void check(std::vector& lemmas); - private: - /** Pointer to the datatype theory that owns this class. */ - TheoryDatatypes* d_td; - /** Pointer to the sygus term database */ - quantifiers::TermDbSygus* d_tds; - /** the simple symmetry breaking utility */ - SygusSimpleSymBreak d_ssb; - /** - * Map from terms to the index of the tester that is asserted for them in - * the current SAT context. In other words, if d_testers[n] = 2, then the - * tester is-C_2(n) is asserted in this SAT context. - */ - IntMap d_testers; - /** - * Map from terms to the tester asserted for them. In the example above, - * d_testers[n] = is-C_2(n). - */ - NodeMap d_testers_exp; - /** - * The set of (selector chain) terms that are active in the current SAT - * context. A selector chain term S_n( ... S_1( x )... ) is active if either: - * (1) n=0 and x is a sygus enumerator, - * or: - * (2.1) S_{n-1}( ... S_1( x )) is active, - * (2.2) is-C( S_{n-1}( ... S_1( x )) ) is asserted in this SAT context, and - * (2.3) S_n is a selector for constructor C. - */ - NodeSet d_active_terms; - /** - * Map from enumerators to a lower bound on their size in the current SAT - * context. - */ - IntMap d_currTermSize; - /** zero */ - Node d_zero; - /** true */ - Node d_true; - /** - * Map from terms (selector chains) to their anchors. The anchor of a - * selector chain S1( ... Sn( x ) ... ) is x. - */ - std::unordered_map d_term_to_anchor; - /** - * Map from anchors to the conjecture they are associated with. - */ - std::map d_anchor_to_conj; - /** - * Map from terms (selector chains) to their depth. The depth of a selector - * chain S1( ... Sn( x ) ... ) is: - * weight( S1 ) + ... + weight( Sn ), - * where weight is the selector weight of Si - * (see SygusTermDatabase::getSelectorWeight). - */ - std::unordered_map d_term_to_depth; - /** - * Map from terms (selector chains) to whether they are the topmost term - * of their type. For example, if: - * S1 : T1 -> T2 - * S2 : T2 -> T2 - * S3 : T2 -> T1 - * S4 : T1 -> T3 - * Then, x, S1( x ), and S4( S3( S2( S1( x ) ) ) ) are top-level terms, - * whereas S2( S1( x ) ) and S3( S2( S1( x ) ) ) are not. - */ - std::unordered_map d_is_top_level; - /** - * Returns true if the selector chain n is top-level based on the above - * definition, when tn is the type of n. - */ - bool computeTopLevel( TypeNode tn, Node n ); -private: - /** This caches all information regarding symmetry breaking for an anchor. */ - class SearchCache - { - public: - SearchCache(){} - /** - * A cache of all search terms for (types, sizes). See registerSearchTerm - * for definition of search terms. - */ - std::map< TypeNode, std::map< unsigned, std::vector< Node > > > d_search_terms; - /** A cache of all symmetry breaking lemma templates for (types, sizes). */ - std::map< TypeNode, std::map< unsigned, std::vector< Node > > > d_sb_lemmas; - /** search value - * - * For each sygus type, a map from a builtin term to a sygus term for that - * type that we encountered during the search whose analog rewrites to that - * term. The range of this map can be updated if we later encounter a sygus - * term that also rewrites to the builtin value but has a smaller term size. - */ - std::map> - d_search_val; - /** the size of terms in the range of d_search val. */ - std::map> - d_search_val_sz; - /** For each term, whether this cache has processed that term */ - std::unordered_set d_search_val_proc; - }; - /** An instance of the above cache, for each anchor */ - std::map< Node, SearchCache > d_cache; - //-----------------------------------traversal predicates - /** pre/post traversal predicates for each type, variable - * - * This stores predicates (pre, post) whose semantics correspond to whether - * a variable has occurred by a (pre, post) traversal of a symbolic term, - * where index = 0 corresponds to pre, index = 1 corresponds to post. For - * details, see getTraversalPredicate below. - */ - std::map> d_traversal_pred[2]; - /** traversal applications to Boolean variables - * - * This maps each application of a traversal predicate pre_x( t ) or - * post_x( t ) to a fresh Boolean variable. - */ - std::map d_traversal_bool; - /** get traversal predicate - * - * Get the predicates (pre, post) whose semantics correspond to whether - * a variable has occurred by this point in a (pre, post) traversal of a term. - * The type of getTraversalPredicate(tn, n, _) is tn -> Bool. - * - * For example, consider the term: - * f( x_1, g( x_2, x_3 ) ) - * and a left-to-right, depth-first traversal of this term. Let e be - * a variable of the same type as this term. We say that for the above term: - * pre_{x_1} is false for e, e.1 and true for e.2, e.2.1, e.2.2 - * pre_{x_2} is false for e, e.1, e.2, e.2.1, and true for e.2.2 - * pre_{x_3} is false for e, e.1, e.2, e.2.1, e.2.2 - * post_{x_1} is true for e.1, e.2.1, e.2.2, e.2, e - * post_{x_2} is false for e.1 and true for e.2.1, e.2.2, e.2, e - * post_{x_3} is false for e.1, e.2.1 and true for e.2.2, e.2, e - * - * We enforce a symmetry breaking scheme for each enumerator e that is - * "variable-agnostic" (see argument isVarAgnostic in registerEnumerator) - * that ensures the variables are ordered. This scheme makes use of these - * predicates, described in the following: - * - * Let x_1, ..., x_m be variables that occur in the same subclass in the type - * of e (see TermDbSygus::getSubclassForVar). - * For i = 1, ..., m: - * // each variable does not occur initially in a traversal of e - * ~pre_{x_i}( e ) AND - * // for each subterm of e - * template z. - * // if this is variable x_i, then x_{i-1} must have already occurred - * is-x_i( z ) => pre_{x_{i-1}}( z ) AND - * for args a = 1...n - * // pre-definition for each argument of this term - * pre_{x_i}( z.a ) = a=0 ? pre_{x_i}( z ) : post_{x_i}( z.{a-1} ) AND - * // post-definition for this term - * post_{x_i}( z ) = post_{x_i}( z.n ) OR is-x_i( z ) - * - * For clarity, above we have written pre and post as first-order predicates. - * However, applications of pre/post should be seen as indexed Boolean - * variables. The reason for this is pre and post cannot be given a consistent - * semantics. For example, consider term f( x_1, x_1 ) and enumerator variable - * e of the same type over which we are encoding a traversal. We have that - * pre_{x_1}( e.1 ) is false and pre_{x_1}( e.2 ) is true, although the model - * values for e.1 and e.2 are equal. Instead, pre_{x_1}( e.1 ) should be seen - * as a Boolean variable V_pre_{x_1,e.1} indexed by x_1 and e.1. and likewise - * for e.2. We convert all applications of pre/post to Boolean variables in - * the method eliminateTraversalPredicates below. Nevertheless, it is - * important that applications pre and post are encoded as APPLY_UF - * applications so that they behave as expected under substitutions. For - * example, pre_{x_1}( z.1 ) { z -> e.2 } results in pre_{x_1}( e.2.1 ), which - * after eliminateTraversalPredicates is V_pre_{x_1, e.2.1}. - */ - Node getTraversalPredicate(TypeNode tn, Node n, bool isPre); - /** eliminate traversal predicates - * - * This replaces all applications of traversal predicates P( x ) in n with - * unique Boolean variables, given by d_traversal_bool[ P( x ) ], and - * returns the result. - */ - Node eliminateTraversalPredicates(Node n); - //-----------------------------------end traversal predicates - /** a sygus sampler object for each (anchor, sygus type) pair - * - * This is used for the sygusRewVerify() option to verify the correctness of - * the rewriter. - */ - std::map> d_sampler; - /** Assert tester internal - * - * This function is called when the tester with index tindex is asserted for - * n, exp is the tester predicate. For example, for grammar: - * A -> A+A | x | 1 | 0 - * when is_+( d ) is asserted, - * assertTesterInternal(0, s( d ), is_+( s( d ) ),...) is called. This - * function may add lemmas to lemmas, which are sent out on the output - * channel of datatypes by the caller. - * - * These lemmas are of various forms, including: - * (1) dynamic symmetry breaking clauses for subterms of n (those added to - * lemmas on calls to addSymBreakLemmasFor, see function below), - * (2) static symmetry breaking clauses for subterms of n (those added to - * lemmas on getSimpleSymBreakPred, see function below), - * (3) conjecture-specific symmetry breaking lemmas, see - * SynthConjecture::getSymmetryBreakingPredicate, - * (4) fairness conflicts if sygusFair() is SYGUS_FAIR_DIRECT, e.g.: - * size( d ) <= 1 V ~is-C1( d ) V ~is-C2( d.1 ) - * where C1 and C2 are non-nullary constructors. - */ - void assertTesterInternal( int tindex, TNode n, Node exp, std::vector< Node >& lemmas ); - /** - * This function is called when term n is registered to the theory of - * datatypes. It makes the appropriate call to registerSearchTerm below, - * if applicable. - */ - void registerTerm(Node n, std::vector& lemmas); - - //------------------------dynamic symmetry breaking - /** Register search term - * - * This function is called when selector chain n of the form - * S_1( ... S_m( x ) ... ) is registered to the theory of datatypes, where - * tn is the type of n, d indicates the depth of n (the sum of weights of the - * selectors S_1...S_m), and topLevel is whether n is a top-level term - * (see d_is_top_level). We refer to n as a "search term". - * - * The purpose of this function is to notify this class that symmetry breaking - * lemmas should be instantiated for n. Any symmetry breaking lemmas that - * are active for n (see description of addSymBreakLemmasFor) are added to - * lemmas in this call. - */ - void registerSearchTerm( TypeNode tn, unsigned d, Node n, bool topLevel, std::vector< Node >& lemmas ); - /** Register search value - * - * This function is called when a selector chain n has been assigned a model - * value nv. This function calls itself recursively so that extensions of the - * selector chain n are registered with all the subterms of nv. For example, - * if we call this function with: - * n = x, nv = +( 1(), x() ) - * we make recursive calls with: - * n = x.1, nv = 1() and n = x.2, nv = x() - * - * a : the anchor of n, - * d : the depth of n. - * - * This function determines if the value nv is equivalent via rewriting to - * any previously registered search values for anchor a. If so, we construct - * a symmetry breaking lemma template and register it in d_cache[a]. For - * example, for grammar: - * A -> A+A | x | 1 | 0 - * Registering search value d -> x followed by d -> +( x, 0 ) results in the - * construction of the symmetry breaking lemma template: - * ~is_+( z ) V ~is_x( z.1 ) V ~is_0( z.2 ) - * which is stored in d_cache[a].d_sb_lemmas. This lemma is instantiated with - * z -> t for all terms t of appropriate depth, including d. - * This function strengthens blocking clauses using generalization techniques - * described in Reynolds et al SYNT 2017. - * - * The return value of this function is an abstraction of model assignment - * of nv to n, or null if we wish to exclude the model assignment nv to n. - * The return value of this method is different from nv itself, e.g. if it - * contains occurrences of the "any constant" constructor. For example, if - * nv is C_+( C_x(), C_{any_constant}( 5 ) ), then the return value of this - * function will either be null, or C_+( C_x(), C_{any_constant}( n.1.0 ) ), - * where n.1.0 is the appropriate selector chain applied to n. We build this - * abstraction since the semantics of C_{any_constant} is "any constant" and - * not "some constant". Thus, we should consider the subterm - * C_{any_constant}( 5 ) above to be an unconstrained variable (as represented - * by a selector chain), instead of the concrete value 5. - * - * The flag isVarAgnostic is whether "a" is a variable agnostic enumerator. If - * this is the case, we restrict symmetry breaking to subterms of n on its - * leftmost subchain. For example, consider the grammar: - * A -> B=B - * B -> B+B | x | y | 0 - * Say we are registering the search value x = y+x. Notice that this value is - * ordered. If a were a variable-agnostic enumerator of type A in this - * case, we would only register x = y+x and x, and not y+x or y, since the - * latter two terms are not leftmost subterms in this value. If we did on the - * other hand register y+x, we would be prevented from solutions like x+y = 0 - * later, since x+y is equivalent to (the already registered value) y+x. - * - * If doSym is false, we are not performing symmetry breaking on n. This flag - * is set to false on branches of n that are not leftmost. - */ - Node registerSearchValue(Node a, - Node n, - Node nv, - unsigned d, - std::vector& lemmas, - bool isVarAgnostic, - bool doSym); - /** Register symmetry breaking lemma - * - * This function adds the symmetry breaking lemma template lem for terms of - * type tn with anchor a. This is added to d_cache[a].d_sb_lemmas. Notice that - * we use lem as a template with free variable x, e.g. our template is: - * (lambda ((x tn)) lem) - * where x = getFreeVar( tn ). For all search terms t of the appropriate - * depth, - * we add the lemma lem{ x -> t } to lemmas. - * - * The argument sz indicates the size of terms that the lemma applies to, e.g. - * ~is_+( z ) has size 1 - * ~is_+( z ) V ~is_x( z.1 ) V ~is_0( z.2 ) has size 1 - * ~is_+( z ) V ~is_+( z.1 ) has size 2 - * This is equivalent to sum of weights of constructors corresponding to each - * tester, e.g. above + has weight 1, and x and 0 have weight 0. - */ - void registerSymBreakLemma( - TypeNode tn, Node lem, unsigned sz, Node a, std::vector& lemmas); - /** Register symmetry breaking lemma for value - * - * This function adds a symmetry breaking lemma template for selector chains - * with anchor a, that effectively states that val should never be a subterm - * of any value for a. - * - * et : an "invariance test" (see sygus/sygus_invariance.h) which states a - * criterion that val meets, which is the reason for its exclusion. This is - * used for generalizing the symmetry breaking lemma template. - * valr : if non-null, this states a value that should *not* be excluded by - * the symmetry breaking lemma template, which is a restriction to the above - * generalization. - * - * This function may add instances of the symmetry breaking template for - * existing search terms, which are added to lemmas. - */ - void registerSymBreakLemmaForValue(Node a, - Node val, - quantifiers::SygusInvarianceTest& et, - Node valr, - std::map& var_count, - std::vector& lemmas); - /** Add symmetry breaking lemmas for term - * - * Adds all active symmetry breaking lemmas for selector chain t to lemmas. A - * symmetry breaking lemma L is active for t based on three factors: - * (1) the current search size sz(a) for its anchor a, - * (2) the depth d of term t (see d_term_to_depth), - * (3) the size sz(L) of the symmetry breaking lemma L. - * In particular, L is active if sz(L) <= sz(a) - d. In other words, a - * symmetry breaking lemma is active if it is intended to block terms of - * size sz(L), and the maximum size that t can take in the current search, - * sz(a)-d, is greater than or equal to this value. - * - * tn : the type of term t, - * a : the anchor of term t, - * d : the depth of term t. - */ - void addSymBreakLemmasFor( - TypeNode tn, Node t, unsigned d, Node a, std::vector& lemmas); - /** calls the above function where a is the anchor t */ - void addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, std::vector< Node >& lemmas ); - //------------------------end dynamic symmetry breaking - - /** Get relevancy condition - * - * This returns (the negation of) a predicate that holds in the contexts in - * which the selector chain n is specified. For example, the negation of the - * relevancy condition for sel_{C2,1}( sel_{C1,1}( d ) ) is - * ~( is-C1( d ) ^ is-C2( sel_{C1,1}( d ) ) ) - * If shared selectors are enabled, this is a conjunction of disjunctions, - * since shared selectors may apply to multiple constructors. - */ - Node getRelevancyCondition( Node n ); - /** Cache of the above function */ - std::map d_rlv_cond; - - //------------------------static symmetry breaking - /** Get simple symmetry breakind predicate - * - * This function returns the "static" symmetry breaking lemma template for - * terms with type tn and constructor index tindex, for the given depth. This - * includes inferences about size with depth=0. Given grammar: - * A -> ite( B, A, A ) | A+A | x | 1 | 0 - * B -> A = A - * Examples of static symmetry breaking lemma templates are: - * for +, depth 0: size(z)=size(z.1)+size(z.2)+1 - * for +, depth 1: ~is-0( z.1 ) ^ ~is-0( z.2 ) ^ F - * where F ensures the constructor of z.1 is less than that of z.2 based - * on some ordering. - * for ite, depth 1: z.2 != z.3 - * These templates can be thought of as "hard-coded" cases of dynamic symmetry - * breaking lemma templates. Notice that the above lemma templates are in - * terms of getFreeVar( tn ), hence only one is created per - * (constructor, depth). A static symmetry break lemma template F[z] for - * constructor C are included in lemmas of the form: - * is-C( t ) => F[t] - * where t is a search term, see registerSearchTerm for definition of search - * term. - * - * usingSymCons: whether we are using symbolic constructors for subterms in - * the type tn, - * isVarAgnostic: whether the terms we are enumerating are agnostic to - * variables. - * - * The latter two options may affect the form of the predicate we construct. - */ - Node getSimpleSymBreakPred(Node e, - TypeNode tn, - int tindex, - unsigned depth, - bool usingSymCons, - bool isVarAgnostic); - /** Cache of the above function */ - std::map>>>> - d_simple_sb_pred; - /** - * For each search term, this stores the maximum depth for which we have added - * a static symmetry breaking lemma. - * - * This should be user context-dependent if sygus is updated to work in - * incremental mode. - */ - std::unordered_map d_simple_proc; - //------------------------end static symmetry breaking - - /** Get the canonical free variable for type tn */ - TNode getFreeVar( TypeNode tn ); - /** get term order predicate - * - * Assuming that n1 and n2 are children of a commutative operator, this - * returns a symmetry breaking predicate that can be instantiated for n1 and - * n2 while preserving satisfiability. By default, this is the predicate - * ( DT_SIZE n1 ) >= ( DT_SIZE n2 ) - */ - Node getTermOrderPredicate( Node n1, Node n2 ); - - private: - /** - * Map from registered variables to whether they are a sygus enumerator. - * - * This should be user context-dependent if sygus is updated to work in - * incremental mode. - */ - std::map d_register_st; - //----------------------search size information - /** - * Checks whether e is a sygus enumerator, that is, a term for which this - * class will track size for. - * - * We associate each sygus enumerator e with a "measure term", which is used - * for bounding the size of terms for the models of e. The measure term for a - * sygus enumerator may be e itself (if e has an active guard), or an - * arbitrary sygus variable otherwise. A measure term m is one for which our - * decision strategy decides on literals of the form (DT_SYGUS_BOUND m n). - * - * After determining the measure term m for e, if applicable, we initialize - * SygusSizeDecisionStrategy for m below. This may result in lemmas - */ - void registerSizeTerm(Node e, std::vector& lemmas); - /** A decision strategy for each measure term allocated by this class */ - class SygusSizeDecisionStrategy : public DecisionStrategyFmf - { - public: - SygusSizeDecisionStrategy(Node t, context::Context* c, Valuation valuation) - : DecisionStrategyFmf(c, valuation), d_this(t), d_curr_search_size(0) - { - } - /** the measure term */ - Node d_this; - /** - * For each size n, an explanation for why this measure term has size at - * most n. This is typically the literal (DT_SYGUS_BOUND m n), which - * we call the (n^th) "fairness literal" for m. - */ - std::map< unsigned, Node > d_search_size_exp; - /** - * For each size, whether we have called SygusSymBreakNew::notifySearchSize. - */ - std::map< unsigned, bool > d_search_size; - /** - * The current search size. This corresponds to the number of times - * incrementCurrentSearchSize has been called for this measure term. - */ - unsigned d_curr_search_size; - /** the list of all enumerators whose measure term is this */ - std::vector< Node > d_anchors; - /** get or make the measure value - * - * The measure value is an integer variable v that is a (symbolic) integer - * value that is constrained to be less than or equal to the current search - * size. For example, if we are using the fairness strategy - * SYGUS_FAIR_DT_SIZE (see options/datatype_options.h), then we constrain: - * (DT_SYGUS_BOUND m n) <=> (v <= n) - * for all asserted fairness literals. Then, if we are enforcing fairness - * based on the maximum size, we assert: - * (DT_SIZE e) <= v - * for all enumerators e. - */ - Node getOrMkMeasureValue(std::vector& lemmas); - /** get or make the active measure value - * - * The active measure value av is an integer variable that corresponds to - * the (symbolic) value of the sum of enumerators that are yet to be - * registered. This is to enforce the "sum of measures" strategy. For - * example, if we are using the fairness strategy SYGUS_FAIR_DT_SIZE, - * then initially av is equal to the measure value v, and the constraints - * (DT_SYGUS_BOUND m n) <=> (v <= n) - * are added as before. When an enumerator e is registered, we add the - * lemma: - * av = (DT_SIZE e) + av' - * and update the active measure value to av'. This ensures that the sum - * of sizes of active enumerators is at most n. - * - * If the flag mkNew is set to true, then we return a fresh variable and - * update the active measure value. - */ - Node getOrMkActiveMeasureValue(std::vector& lemmas, - bool mkNew = false); - /** Returns the s^th fairness literal for this measure term. */ - Node mkLiteral(unsigned s) override; - /** identify */ - std::string identify() const override - { - return std::string("sygus_enum_size"); - } - - private: - /** the measure value */ - Node d_measure_value; - /** the sygus measure value */ - Node d_measure_value_active; - }; - /** the above information for each registered measure term */ - std::map> d_szinfo; - /** map from enumerators (anchors) to their associated measure term */ - std::map< Node, Node > d_anchor_to_measure_term; - /** map from enumerators (anchors) to their active guard*/ - std::map< Node, Node > d_anchor_to_active_guard; - /** map from enumerators (anchors) to a decision stratregy for that guard */ - std::map> d_anchor_to_ag_strategy; - /** generic measure term - * - * This is a global term that is used as the measure term for all sygus - * enumerators that do not have active guards. This class enforces that - * all enumerators have size at most n, where n is the minimal integer - * such that (DT_SYGUS_BOUND d_generic_measure_term n) is asserted. - */ - Node d_generic_measure_term; - /** - * This increments the current search size for measure term m. This may - * cause lemmas to be added to lemmas based on the fact that symmetry - * breaking lemmas are now relevant for new search terms, see discussion - * of how search size affects which lemmas are relevant above - * addSymBreakLemmasFor. - */ - void incrementCurrentSearchSize( Node m, std::vector< Node >& lemmas ); - /** - * Notify this class that we are currently searching for terms of size at - * most s as model values for measure term m. Literal exp corresponds to the - * explanation of why the measure term has size at most n. This calls - * incrementSearchSize above, until the total number of times we have called - * incrementSearchSize so far is at least s. - */ - void notifySearchSize( Node m, unsigned s, Node exp, std::vector< Node >& lemmas ); - /** Allocates a SygusSizeDecisionStrategy object in d_szinfo. */ - void registerMeasureTerm( Node m ); - /** - * Return the current search size for arbitrary term n. This is the current - * search size of the anchor of n. - */ - unsigned getSearchSizeFor( Node n ); - /** return the current search size for enumerator (anchor) e */ - unsigned getSearchSizeForAnchor(Node e); - /** Get the current search size for measure term m in this SAT context. */ - unsigned getSearchSizeForMeasureTerm(Node m); - /** get current template - * - * For debugging. This returns a term that corresponds to the current - * inferred shape of n. For example, if the testers - * is-C1( n ) and is-C2( n.1 ) - * have been asserted where C1 and C2 are binary constructors, then this - * method may return a term of the form: - * C1( C2( x1, x2 ), x3 ) - * for fresh variables x1, x2, x3. The map var_count maintains the variable - * count for generating these fresh variables. - */ - Node getCurrentTemplate( Node n, std::map< TypeNode, int >& var_count ); - //----------------------end search size information - /** check value - * - * This is called when we have a model assignment vn for n, where n is - * a selector chain applied to an enumerator (a search term). This function - * ensures that testers have been asserted for each subterm of vn. This is - * critical for ensuring that the proper steps have been taken by this class - * regarding whether or not vn is a legal value for n (not greater than the - * current search size and not a value that can be blocked by symmetry - * breaking). - * - * For example, if vn = +( x(), x() ), then we ensure that the testers - * is-+( n ), is-x( n.1 ), is-x( n.2 ) - * have been asserted to this class. If a tester is not asserted for some - * relevant selector chain S( n ) of n, then we add a lemma L for that - * selector chain to lemmas, where L is the "splitting lemma" for S( n ), that - * states that the top symbol of S( n ) must be one of the constructors of - * its type. - * - * Notice that this function is a sanity check. Typically, it should be the - * case that testers are asserted for all subterms of vn, and hence this - * method should not ever add anything to lemmas. However, due to its - * importance, we check this regardless. - */ - bool checkValue(Node n, Node vn, int ind, std::vector& lemmas); - /** - * Get the current SAT status of the guard g. - * In particular, this returns 1 if g is asserted true, -1 if it is asserted - * false, and 0 if it is not asserted. - */ - int getGuardStatus( Node g ); -}; - -} -} -} - -#endif - diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp new file mode 100644 index 000000000..7e5a3ae98 --- /dev/null +++ b/src/theory/datatypes/sygus_extension.cpp @@ -0,0 +1,1804 @@ +/********************* */ +/*! \file sygus_extension.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of the sygus extension of the theory of datatypes. + **/ + +#include "theory/datatypes/sygus_extension.h" + +#include "expr/node_manager.h" +#include "options/base_options.h" +#include "options/datatypes_options.h" +#include "options/quantifiers_options.h" +#include "printer/printer.h" +#include "theory/datatypes/theory_datatypes.h" +#include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/quantifiers/sygus/sygus_explain.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" +#include "theory/theory_model.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::datatypes; + +SygusExtension::SygusExtension(TheoryDatatypes* td, + QuantifiersEngine* qe, + context::Context* c) + : d_td(td), + d_tds(qe->getTermDatabaseSygus()), + d_ssb(qe), + d_testers(c), + d_testers_exp(c), + d_active_terms(c), + d_currTermSize(c) +{ + d_zero = NodeManager::currentNM()->mkConst(Rational(0)); + d_true = NodeManager::currentNM()->mkConst(true); +} + +SygusExtension::~SygusExtension() { + +} + +/** add tester */ +void SygusExtension::assertTester( int tindex, TNode n, Node exp, std::vector< Node >& lemmas ) { + registerTerm( n, lemmas ); + // check if this is a relevant (sygus) term + if( d_term_to_anchor.find( n )!=d_term_to_anchor.end() ){ + Trace("sygus-sb-debug2") << "Sygus : process tester : " << exp << std::endl; + // if not already active (may have duplicate calls for the same tester) + if( d_active_terms.find( n )==d_active_terms.end() ) { + d_testers[n] = tindex; + d_testers_exp[n] = exp; + + // check if parent is active + bool do_add = true; + if( options::sygusSymBreakLazy() ){ + if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){ + NodeSet::const_iterator it = d_active_terms.find( n[0] ); + if( it==d_active_terms.end() ){ + do_add = false; + }else{ + //this must be a proper selector + IntMap::const_iterator itt = d_testers.find( n[0] ); + Assert(itt != d_testers.end()); + int ptindex = (*itt).second; + TypeNode ptn = n[0].getType(); + const Datatype& pdt = ((DatatypeType)ptn.toType()).getDatatype(); + int sindex_in_parent = pdt[ptindex].getSelectorIndexInternal( n.getOperator().toExpr() ); + // the tester is irrelevant in this branch + if( sindex_in_parent==-1 ){ + do_add = false; + } + } + } + } + if( do_add ){ + assertTesterInternal( tindex, n, exp, lemmas ); + }else{ + Trace("sygus-sb-debug2") << "...ignore inactive tester : " << exp << std::endl; + } + }else{ + Trace("sygus-sb-debug2") << "...ignore repeated tester : " << exp << std::endl; + } + }else{ + Trace("sygus-sb-debug2") << "...ignore non-sygus tester : " << exp << std::endl; + } +} + +void SygusExtension::assertFact( Node n, bool polarity, std::vector< Node >& lemmas ) { + if (n.getKind() == kind::DT_SYGUS_BOUND) + { + Node m = n[0]; + Trace("sygus-fair") << "Have sygus bound : " << n << ", polarity=" << polarity << " on measure " << m << std::endl; + registerMeasureTerm( m ); + if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){ + std::map>::iterator its = + d_szinfo.find(m); + Assert(its != d_szinfo.end()); + Node mt = its->second->getOrMkMeasureValue(lemmas); + //it relates the measure term to arithmetic + Node blem = n.eqNode( NodeManager::currentNM()->mkNode( kind::LEQ, mt, n[1] ) ); + lemmas.push_back( blem ); + } + if( polarity ){ + unsigned s = n[1].getConst().getNumerator().toUnsignedInt(); + notifySearchSize( m, s, n, lemmas ); + } + }else if( n.getKind() == kind::DT_HEIGHT_BOUND || n.getKind()==DT_SIZE_BOUND ){ + //reduce to arithmetic TODO ? + + } +} + +Node SygusExtension::getTermOrderPredicate( Node n1, Node n2 ) { + NodeManager* nm = NodeManager::currentNM(); + std::vector< Node > comm_disj; + // (1) size of left is greater than size of right + Node sz_less = + nm->mkNode(GT, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2)); + comm_disj.push_back( sz_less ); + // (2) ...or sizes are equal and first child is less by term order + std::vector sz_eq_cases; + Node sz_eq = + nm->mkNode(EQUAL, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2)); + sz_eq_cases.push_back( sz_eq ); + if( options::sygusOpt1() ){ + TypeNode tnc = n1.getType(); + const Datatype& cdt = ((DatatypeType)(tnc).toType()).getDatatype(); + for( unsigned j=0; j case_conj; + for (unsigned k = 0; k < j; k++) + { + case_conj.push_back(utils::mkTester(n2, k, cdt).negate()); + } + if (!case_conj.empty()) + { + Node corder = nm->mkNode( + OR, + utils::mkTester(n1, j, cdt).negate(), + case_conj.size() == 1 ? case_conj[0] : nm->mkNode(AND, case_conj)); + sz_eq_cases.push_back(corder); + } + } + } + Node sz_eqc = sz_eq_cases.size() == 1 ? sz_eq_cases[0] + : nm->mkNode(kind::AND, sz_eq_cases); + comm_disj.push_back( sz_eqc ); + + return nm->mkNode(kind::OR, comm_disj); +} + +void SygusExtension::registerTerm( Node n, std::vector< Node >& lemmas ) { + if( d_is_top_level.find( n )==d_is_top_level.end() ){ + d_is_top_level[n] = false; + TypeNode tn = n.getType(); + unsigned d = 0; + bool is_top_level = false; + bool success = false; + if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){ + registerTerm( n[0], lemmas ); + std::unordered_map::iterator it = + d_term_to_anchor.find(n[0]); + if( it!=d_term_to_anchor.end() ) { + d_term_to_anchor[n] = it->second; + unsigned sel_weight = + d_tds->getSelectorWeight(n[0].getType(), n.getOperator()); + d = d_term_to_depth[n[0]] + sel_weight; + is_top_level = computeTopLevel( tn, n[0] ); + success = true; + } + }else if( n.isVar() ){ + registerSizeTerm( n, lemmas ); + if( d_register_st[n] ){ + d_term_to_anchor[n] = n; + d_anchor_to_conj[n] = d_tds->getConjectureForEnumerator(n); + // this assertion fails if we have a sygus term in the search that is unmeasured + Assert(d_anchor_to_conj[n] != NULL); + d = 0; + is_top_level = true; + success = true; + } + } + if( success ){ + Trace("sygus-sb-debug") << "Register : " << n << ", depth : " << d << ", top level = " << is_top_level << ", type = " << ((DatatypeType)tn.toType()).getDatatype().getName() << std::endl; + d_term_to_depth[n] = d; + d_is_top_level[n] = is_top_level; + registerSearchTerm( tn, d, n, is_top_level, lemmas ); + }else{ + Trace("sygus-sb-debug2") << "Term " << n << " is not part of sygus search." << std::endl; + } + } +} + +bool SygusExtension::computeTopLevel( TypeNode tn, Node n ){ + if( n.getType()==tn ){ + return false; + }else if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){ + return computeTopLevel( tn, n[0] ); + }else{ + return true; + } +} + +void SygusExtension::assertTesterInternal( int tindex, TNode n, Node exp, std::vector< Node >& lemmas ) { + TypeNode ntn = n.getType(); + if (!ntn.isDatatype()) + { + // nothing to do for non-datatype types + return; + } + const Datatype& dt = static_cast(ntn.toType()).getDatatype(); + if (!dt.isSygus()) + { + // nothing to do for non-sygus-datatype type + return; + } + d_active_terms.insert(n); + Trace("sygus-sb-debug2") << "Sygus : activate term : " << n << " : " << exp + << std::endl; + + // get the search size for this + Assert(d_term_to_anchor.find(n) != d_term_to_anchor.end()); + Node a = d_term_to_anchor[n]; + Assert(d_anchor_to_measure_term.find(a) != d_anchor_to_measure_term.end()); + Node m = d_anchor_to_measure_term[a]; + std::map>::iterator itsz = + d_szinfo.find(m); + Assert(itsz != d_szinfo.end()); + unsigned ssz = itsz->second->d_curr_search_size; + + if( options::sygusFair()==SYGUS_FAIR_DIRECT ){ + if( dt[tindex].getNumArgs()>0 ){ + quantifiers::SygusTypeInfo& nti = d_tds->getTypeInfo(ntn); + // consider lower bounds for size of types + unsigned lb_add = nti.getMinConsTermSize(tindex); + unsigned lb_rem = n == a ? 0 : nti.getMinTermSize(); + Assert(lb_add >= lb_rem); + d_currTermSize[a].set( d_currTermSize[a].get() + ( lb_add - lb_rem ) ); + } + if( (unsigned)d_currTermSize[a].get()>ssz ){ + if( Trace.isOn("sygus-sb-fair") ){ + std::map< TypeNode, int > var_count; + Node templ = getCurrentTemplate( a, var_count ); + Trace("sygus-sb-fair") << "FAIRNESS : we have " << d_currTermSize[a].get() << " at search size " << ssz << ", template is " << templ << std::endl; + } + // conflict + std::vector< Node > conflict; + for( NodeSet::const_iterator its = d_active_terms.begin(); its != d_active_terms.end(); ++its ){ + Node x = *its; + Node xa = d_term_to_anchor[x]; + if( xa==a ){ + IntMap::const_iterator ittv = d_testers.find( x ); + Assert(ittv != d_testers.end()); + int tindex = (*ittv).second; + const Datatype& dti = ((DatatypeType)x.getType().toType()).getDatatype(); + if( dti[tindex].getNumArgs()>0 ){ + NodeMap::const_iterator itt = d_testers_exp.find( x ); + Assert(itt != d_testers_exp.end()); + conflict.push_back( (*itt).second ); + } + } + } + Assert(conflict.size() == (unsigned)d_currTermSize[a].get()); + Assert(itsz->second->d_search_size_exp.find(ssz) + != itsz->second->d_search_size_exp.end()); + conflict.push_back( itsz->second->d_search_size_exp[ssz] ); + Node conf = NodeManager::currentNM()->mkNode( kind::AND, conflict ); + Trace("sygus-sb-fair") << "Conflict is : " << conf << std::endl; + lemmas.push_back( conf.negate() ); + return; + } + } + + // now, add all applicable symmetry breaking lemmas for this term + Assert(d_term_to_depth.find(n) != d_term_to_depth.end()); + unsigned d = d_term_to_depth[n]; + Trace("sygus-sb-fair-debug") << "Tester " << exp << " is for depth " << d << " term in search size " << ssz << std::endl; + //Assert( d<=ssz ); + if( options::sygusSymBreakLazy() ){ + // dynamic symmetry breaking + addSymBreakLemmasFor( ntn, n, d, lemmas ); + } + + Trace("sygus-sb-debug") << "Get simple symmetry breaking predicates...\n"; + unsigned max_depth = ssz>=d ? ssz-d : 0; + unsigned min_depth = d_simple_proc[exp]; + NodeManager* nm = NodeManager::currentNM(); + if( min_depth<=max_depth ){ + TNode x = getFreeVar( ntn ); + std::vector sb_lemmas; + // symmetry breaking lemmas requiring predicate elimination + std::map sb_elim_pred; + bool usingSymCons = d_tds->usingSymbolicConsForEnumerator(m); + bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(m); + for (unsigned ds = 0; ds <= max_depth; ds++) + { + // static conjecture-independent symmetry breaking + Trace("sygus-sb-debug") << " simple symmetry breaking...\n"; + Node ipred = getSimpleSymBreakPred( + m, ntn, tindex, ds, usingSymCons, isVarAgnostic); + if (!ipred.isNull()) + { + sb_lemmas.push_back(ipred); + if (ds == 0 && isVarAgnostic) + { + sb_elim_pred[ipred] = true; + } + } + // static conjecture-dependent symmetry breaking + Trace("sygus-sb-debug") + << " conjecture-dependent symmetry breaking...\n"; + std::map::iterator itc = + d_anchor_to_conj.find(a); + if (itc != d_anchor_to_conj.end()) + { + quantifiers::SynthConjecture* conj = itc->second; + Assert(conj != NULL); + Node dpred = conj->getSymmetryBreakingPredicate(x, a, ntn, tindex, ds); + if (!dpred.isNull()) + { + sb_lemmas.push_back(dpred); + } + } + } + + // add the above symmetry breaking predicates to lemmas + std::unordered_map cache; + Node rlv = getRelevancyCondition(n); + for (const Node& slem : sb_lemmas) + { + Node sslem = slem.substitute(x, n, cache); + // if we require predicate elimination + if (sb_elim_pred.find(slem) != sb_elim_pred.end()) + { + Trace("sygus-sb-tp") << "Eliminate traversal predicates: start " + << sslem << std::endl; + sslem = eliminateTraversalPredicates(sslem); + Trace("sygus-sb-tp") << "Eliminate traversal predicates: finish " + << sslem << std::endl; + } + if (!rlv.isNull()) + { + sslem = nm->mkNode(OR, rlv, sslem); + } + lemmas.push_back(sslem); + } + } + d_simple_proc[exp] = max_depth + 1; + + // now activate the children those testers were previously asserted in this + // context and are awaiting activation, if they exist. + if( options::sygusSymBreakLazy() ){ + Trace("sygus-sb-debug") << "Do lazy symmetry breaking...\n"; + for( unsigned j=0; jmkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( ntn.toType(), j ) ), n ); + Trace("sygus-sb-debug2") << " activate child sel : " << sel << std::endl; + Assert(d_active_terms.find(sel) == d_active_terms.end()); + IntMap::const_iterator itt = d_testers.find( sel ); + if( itt != d_testers.end() ){ + Assert(d_testers_exp.find(sel) != d_testers_exp.end()); + assertTesterInternal( (*itt).second, sel, d_testers_exp[sel], lemmas ); + } + } + Trace("sygus-sb-debug") << "...finished" << std::endl; + } +} + +Node SygusExtension::getRelevancyCondition( Node n ) { + std::map< Node, Node >::iterator itr = d_rlv_cond.find( n ); + if( itr==d_rlv_cond.end() ){ + Node cond; + if( n.getKind()==APPLY_SELECTOR_TOTAL && options::sygusSymBreakRlv() ){ + TypeNode ntn = n[0].getType(); + Type nt = ntn.toType(); + const Datatype& dt = ((DatatypeType)nt).getDatatype(); + Expr selExpr = n.getOperator().toExpr(); + if( options::dtSharedSelectors() ){ + std::vector< Node > disj; + bool excl = false; + for( unsigned i=0; imkNode( + kind::AND, disj); + } + }else{ + int sindex = Datatype::cindexOf( selExpr ); + Assert(sindex != -1); + cond = utils::mkTester(n[0], sindex, dt).negate(); + } + Node c1 = getRelevancyCondition( n[0] ); + if( cond.isNull() ){ + cond = c1; + }else if( !c1.isNull() ){ + cond = NodeManager::currentNM()->mkNode(kind::OR, cond, c1); + } + } + Trace("sygus-sb-debug2") << "Relevancy condition for " << n << " is " << cond << std::endl; + d_rlv_cond[n] = cond; + return cond; + }else{ + return itr->second; + } +} + +Node SygusExtension::getTraversalPredicate(TypeNode tn, Node n, bool isPre) +{ + unsigned index = isPre ? 0 : 1; + std::map::iterator itt = d_traversal_pred[index][tn].find(n); + if (itt != d_traversal_pred[index][tn].end()) + { + return itt->second; + } + NodeManager* nm = NodeManager::currentNM(); + std::vector types; + types.push_back(tn); + TypeNode ptn = nm->mkPredicateType(types); + Node pred = nm->mkSkolem(isPre ? "pre" : "post", ptn); + d_traversal_pred[index][tn][n] = pred; + return pred; +} + +Node SygusExtension::eliminateTraversalPredicates(Node n) +{ + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map visited; + std::unordered_map::iterator it; + std::map::iterator ittb; + std::vector visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + + if (it == visited.end()) + { + if (cur.getKind() == APPLY_UF) + { + Assert(cur.getType().isBoolean()); + Assert(cur.getNumChildren() == 1 + && (cur[0].isVar() || cur[0].getKind() == APPLY_SELECTOR_TOTAL)); + ittb = d_traversal_bool.find(cur); + Node ret; + if (ittb == d_traversal_bool.end()) + { + std::stringstream ss; + ss << "v_" << cur; + ret = nm->mkSkolem(ss.str(), cur.getType()); + d_traversal_bool[cur] = ret; + } + else + { + ret = ittb->second; + } + visited[cur] = ret; + } + else + { + visited[cur] = Node::null(); + visit.push_back(cur); + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } + else if (it->second.isNull()) + { + Node ret = cur; + bool childChanged = false; + std::vector children; + if (cur.getMetaKind() == metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + for (const Node& cn : cur) + { + it = visited.find(cn); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + } + if (childChanged) + { + ret = nm->mkNode(cur.getKind(), children); + } + visited[cur] = ret; + } + } while (!visit.empty()); + Assert(visited.find(n) != visited.end()); + Assert(!visited.find(n)->second.isNull()); + return visited[n]; +} + +Node SygusExtension::getSimpleSymBreakPred(Node e, + TypeNode tn, + int tindex, + unsigned depth, + bool usingSymCons, + bool isVarAgnostic) +{ + // Compute the tuple of expressions we hash the predicate for. + + // The hash value in d_simple_sb_pred for the given options + unsigned optHashVal = usingSymCons ? 1 : 0; + if (isVarAgnostic && depth == 0) + { + // variable agnostic symmetry breaking only applies at depth 0 + optHashVal = optHashVal + 2; + } + else + { + // enumerator is only specific to variable agnostic symmetry breaking + e = Node::null(); + } + std::map& ssbCache = + d_simple_sb_pred[e][tn][tindex][optHashVal]; + std::map::iterator it = ssbCache.find(depth); + if (it != ssbCache.end()) + { + return it->second; + } + // this function is only called on sygus datatype types + Assert(tn.isDatatype()); + NodeManager* nm = NodeManager::currentNM(); + Node n = getFreeVar(tn); + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + Assert(dt.isSygus()); + Assert(tindex >= 0 && tindex < static_cast(dt.getNumConstructors())); + + Trace("sygus-sb-simple-debug") + << "Simple symmetry breaking for " << dt.getName() << ", constructor " + << dt[tindex].getName() << ", at depth " << depth << std::endl; + + quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn); + // get the sygus operator + Node sop = Node::fromExpr(dt[tindex].getSygusOp()); + // get the kind of the constructor operator + Kind nk = ti.getConsNumKind(tindex); + // is this the any-constant constructor? + bool isAnyConstant = sop.getAttribute(SygusAnyConstAttribute()); + + // conjunctive conclusion of lemma + std::vector sbp_conj; + + // the number of (sygus) arguments + // Notice if this is an any-constant constructor, its child is not a + // sygus child, hence we set to 0 here. + unsigned dt_index_nargs = isAnyConstant ? 0 : dt[tindex].getNumArgs(); + + // builtin type + TypeNode tnb = TypeNode::fromType(dt.getSygusType()); + // get children + std::vector children; + for (unsigned j = 0; j < dt_index_nargs; j++) + { + Node sel = nm->mkNode( + APPLY_SELECTOR_TOTAL, + Node::fromExpr(dt[tindex].getSelectorInternal(tn.toType(), j)), + n); + Assert(sel.getType().isDatatype()); + children.push_back(sel); + } + + if (depth == 0) + { + Trace("sygus-sb-simple-debug") << " Size..." << std::endl; + // fairness + if (options::sygusFair() == SYGUS_FAIR_DT_SIZE && !isAnyConstant) + { + Node szl = nm->mkNode(DT_SIZE, n); + Node szr = nm->mkNode(DT_SIZE, utils::getInstCons(n, dt, tindex)); + szr = Rewriter::rewrite(szr); + sbp_conj.push_back(szl.eqNode(szr)); + } + if (isVarAgnostic) + { + // Enforce symmetry breaking lemma template for each x_i: + // template z. + // is-x_i( z ) => pre_{x_{i-1}}( z ) + // for args a = 1...n + // // pre-definition + // pre_{x_i}( z.a ) = a=0 ? pre_{x_i}( z ) : post_{x_i}( z.{a-1} ) + // post_{x_i}( z ) = post_{x_i}( z.n ) OR is-x_i( z ) + + // Notice that we are constructing a symmetry breaking template + // under the condition that is-C( z ) holds in this method, where C + // is the tindex^{th} constructor of dt. Thus, is-x_i( z ) is either + // true or false below. + + Node svl = Node::fromExpr(dt.getSygusVarList()); + // for each variable + Assert(!e.isNull()); + TypeNode etn = e.getType(); + // for each variable in the sygus type + for (const Node& var : svl) + { + quantifiers::SygusTypeInfo& eti = d_tds->getTypeInfo(etn); + unsigned sc = eti.getSubclassForVar(var); + if (eti.getNumSubclassVars(sc) == 1) + { + // unique variable in singleton subclass, skip + continue; + } + // Compute the "predecessor" variable in the subclass of var. + Node predVar; + unsigned scindex = 0; + if (eti.getIndexInSubclassForVar(var, scindex)) + { + if (scindex > 0) + { + predVar = eti.getVarSubclassIndex(sc, scindex - 1); + } + } + Node preParentOp = getTraversalPredicate(tn, var, true); + Node preParent = nm->mkNode(APPLY_UF, preParentOp, n); + Node prev = preParent; + // for each child + for (const Node& child : children) + { + TypeNode ctn = child.getType(); + // my pre is equal to the previous + Node preCurrOp = getTraversalPredicate(ctn, var, true); + Node preCurr = nm->mkNode(APPLY_UF, preCurrOp, child); + // definition of pre, for each argument + sbp_conj.push_back(preCurr.eqNode(prev)); + Node postCurrOp = getTraversalPredicate(ctn, var, false); + prev = nm->mkNode(APPLY_UF, postCurrOp, child); + } + Node postParent = getTraversalPredicate(tn, var, false); + Node finish = nm->mkNode(APPLY_UF, postParent, n); + // check if we are constructing the symmetry breaking predicate for the + // variable in question. If so, is-{x_i}( z ) is true. + int varCn = ti.getOpConsNum(var); + if (varCn == static_cast(tindex)) + { + // the post value is true + prev = d_true; + // requirement : If I am the variable, I must have seen + // the variable before this one in its type class. + if (!predVar.isNull()) + { + Node preParentPredVarOp = getTraversalPredicate(tn, predVar, true); + Node preParentPredVar = nm->mkNode(APPLY_UF, preParentPredVarOp, n); + sbp_conj.push_back(preParentPredVar); + } + } + // definition of post + sbp_conj.push_back(finish.eqNode(prev)); + } + } + } + + // if we are the "any constant" constructor, we do no symmetry breaking + // only do simple symmetry breaking up to depth 2 + bool doSymBreak = options::sygusSymBreak(); + if (isAnyConstant || depth > 2) + { + doSymBreak = false; + } + // symmetry breaking + if (doSymBreak) + { + // direct solving for children + // for instance, we may want to insist that the LHS of MINUS is 0 + Trace("sygus-sb-simple-debug") << " Solve children..." << std::endl; + std::map children_solved; + for (unsigned j = 0; j < dt_index_nargs; j++) + { + int i = d_ssb.solveForArgument(tn, tindex, j); + if (i >= 0) + { + children_solved[j] = i; + TypeNode ctn = children[j].getType(); + const Datatype& cdt = + static_cast(ctn.toType()).getDatatype(); + Assert(i < static_cast(cdt.getNumConstructors())); + sbp_conj.push_back(utils::mkTester(children[j], i, cdt)); + } + } + + // depth 1 symmetry breaking : talks about direct children + if (depth == 1) + { + if (nk != UNDEFINED_KIND) + { + Trace("sygus-sb-simple-debug") + << " Equality reasoning about children..." << std::endl; + // commutative operators + if (quantifiers::TermUtil::isComm(nk)) + { + if (children.size() == 2 + && children[0].getType() == children[1].getType()) + { + Node order_pred = getTermOrderPredicate(children[0], children[1]); + sbp_conj.push_back(order_pred); + } + } + // operators whose arguments are non-additive (e.g. should be different) + std::vector deq_child[2]; + if (children.size() == 2 && children[0].getType() == tn) + { + bool argDeq = false; + if (quantifiers::TermUtil::isNonAdditive(nk)) + { + argDeq = true; + } + else + { + // other cases of rewriting x k x -> x' + Node req_const; + if (nk == GT || nk == LT || nk == XOR || nk == MINUS + || nk == BITVECTOR_SUB || nk == BITVECTOR_XOR + || nk == BITVECTOR_UREM_TOTAL) + { + // must have the zero element + req_const = quantifiers::TermUtil::mkTypeValue(tnb, 0); + } + else if (nk == EQUAL || nk == LEQ || nk == GEQ + || nk == BITVECTOR_XNOR) + { + req_const = quantifiers::TermUtil::mkTypeMaxValue(tnb); + } + // cannot do division since we have to consider when both are zero + if (!req_const.isNull()) + { + if (ti.hasConst(req_const)) + { + argDeq = true; + } + } + } + if (argDeq) + { + deq_child[0].push_back(0); + deq_child[1].push_back(1); + } + } + if (nk == ITE || nk == STRING_STRREPL || nk == STRING_STRREPLALL) + { + deq_child[0].push_back(1); + deq_child[1].push_back(2); + } + if (nk == STRING_STRREPL || nk == STRING_STRREPLALL) + { + deq_child[0].push_back(0); + deq_child[1].push_back(1); + } + // this code adds simple symmetry breaking predicates of the form + // d.i != d.j, for example if we are considering an ITE constructor, + // we enforce that d.1 != d.2 since otherwise the ITE can be + // simplified. + for (unsigned i = 0, size = deq_child[0].size(); i < size; i++) + { + unsigned c1 = deq_child[0][i]; + unsigned c2 = deq_child[1][i]; + TypeNode tnc = children[c1].getType(); + // we may only apply this symmetry breaking scheme (which introduces + // disequalities) if the types are infinite. + if (tnc == children[c2].getType() && !tnc.isInterpretedFinite()) + { + Node sym_lem_deq = children[c1].eqNode(children[c2]).negate(); + // notice that this symmetry breaking still allows for + // ite( C, any_constant(x), any_constant(y) ) + // since any_constant takes a builtin argument. + sbp_conj.push_back(sym_lem_deq); + } + } + + Trace("sygus-sb-simple-debug") << " Redundant operators..." + << std::endl; + // singular arguments (e.g. 0 for mult) + // redundant arguments (e.g. 0 for plus, 1 for mult) + // right-associativity + // simple rewrites + // explanation of why not all children of this are constant + std::vector exp_not_all_const; + // is the above explanation valid? This is set to false if + // one child does not have a constant, hence making the explanation + // false. + bool exp_not_all_const_valid = dt_index_nargs > 0; + // does the parent have an any constant constructor? + bool usingAnyConstCons = + usingSymCons && (ti.getAnyConstantConsNum() != -1); + for (unsigned j = 0; j < dt_index_nargs; j++) + { + Node nc = children[j]; + // if not already solved + if (children_solved.find(j) != children_solved.end()) + { + continue; + } + TypeNode tnc = nc.getType(); + quantifiers::SygusTypeInfo& cti = d_tds->getTypeInfo(tnc); + int anyc_cons_num = cti.getAnyConstantConsNum(); + const Datatype& cdt = + static_cast(tnc.toType()).getDatatype(); + std::vector exp_const; + for (unsigned k = 0, ncons = cdt.getNumConstructors(); k < ncons; k++) + { + Kind nck = cti.getConsNumKind(k); + bool red = false; + Node tester = utils::mkTester(nc, k, cdt); + // check if the argument is redundant + if (static_cast(k) == anyc_cons_num) + { + exp_const.push_back(tester); + } + else if (nck != UNDEFINED_KIND) + { + Trace("sygus-sb-simple-debug") << " argument " << j << " " << k + << " is : " << nck << std::endl; + red = !d_ssb.considerArgKind(tnc, tn, nck, nk, j); + } + else + { + Node cc = cti.getConsNumConst(k); + if (!cc.isNull()) + { + Trace("sygus-sb-simple-debug") + << " argument " << j << " " << k << " is constant : " << cc + << std::endl; + red = !d_ssb.considerConst(tnc, tn, cc, nk, j); + if (usingAnyConstCons) + { + // we only consider concrete constant constructors + // of children if we have the "any constant" constructor + // otherwise, we would disallow solutions for grammars + // like the following: + // A -> B+B + // B -> 4 | 8 | 100 + // where A allows all constants but is not using the + // any constant constructor. + exp_const.push_back(tester); + } + } + else + { + // defined function? + } + } + if (red) + { + Trace("sygus-sb-simple-debug") << " ...redundant." << std::endl; + sbp_conj.push_back(tester.negate()); + } + } + if (exp_const.empty()) + { + exp_not_all_const_valid = false; + } + else + { + Node ecn = exp_const.size() == 1 ? exp_const[0] + : nm->mkNode(OR, exp_const); + exp_not_all_const.push_back(ecn.negate()); + } + } + // explicitly handle constants and "any constant" constructors + // if this type admits any constant, then at least one of my + // children must not be a constant or the "any constant" constructor + if (dt.getSygusAllowConst() && exp_not_all_const_valid) + { + Assert(!exp_not_all_const.empty()); + Node expaan = exp_not_all_const.size() == 1 + ? exp_not_all_const[0] + : nm->mkNode(OR, exp_not_all_const); + Trace("sygus-sb-simple-debug") + << "Ensure not all constant: " << expaan << std::endl; + sbp_conj.push_back(expaan); + } + } + else + { + // defined function? + } + } + else if (depth == 2) + { + // commutative operators + if (quantifiers::TermUtil::isComm(nk) && children.size() == 2 + && children[0].getType() == tn && children[1].getType() == tn) + { + // chainable + Node child11 = nm->mkNode( + APPLY_SELECTOR_TOTAL, + Node::fromExpr(dt[tindex].getSelectorInternal(tn.toType(), 1)), + children[0]); + Assert(child11.getType() == children[1].getType()); + Node order_pred_trans = + nm->mkNode(OR, + utils::mkTester(children[0], tindex, dt).negate(), + getTermOrderPredicate(child11, children[1])); + sbp_conj.push_back(order_pred_trans); + } + } + } + + Node sb_pred; + if (!sbp_conj.empty()) + { + sb_pred = + sbp_conj.size() == 1 ? sbp_conj[0] : nm->mkNode(kind::AND, sbp_conj); + Trace("sygus-sb-simple") + << "Simple predicate for " << tn << " index " << tindex << " (" << nk + << ") at depth " << depth << " : " << std::endl; + Trace("sygus-sb-simple") << " " << sb_pred << std::endl; + sb_pred = nm->mkNode(OR, utils::mkTester(n, tindex, dt).negate(), sb_pred); + } + d_simple_sb_pred[e][tn][tindex][optHashVal][depth] = sb_pred; + return sb_pred; +} + +TNode SygusExtension::getFreeVar( TypeNode tn ) { + return d_tds->getFreeVar(tn, 0); +} + +void SygusExtension::registerSearchTerm( TypeNode tn, unsigned d, Node n, bool topLevel, std::vector< Node >& lemmas ) { + //register this term + std::unordered_map::iterator ita = + d_term_to_anchor.find(n); + Assert(ita != d_term_to_anchor.end()); + Node a = ita->second; + Assert(!a.isNull()); + 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() ){ + Trace("sygus-sb-debug") << " register search term : " << n << " at depth " << d << ", type=" << tn << ", tl=" << topLevel << std::endl; + d_cache[a].d_search_terms[tn][d].push_back( n ); + if( !options::sygusSymBreakLazy() ){ + addSymBreakLemmasFor( tn, n, d, lemmas ); + } + } +} + +Node SygusExtension::registerSearchValue(Node a, + Node n, + Node nv, + unsigned d, + std::vector& lemmas, + bool isVarAgnostic, + bool doSym) +{ + Assert(n.getType().isComparableTo(nv.getType())); + TypeNode tn = n.getType(); + if (!tn.isDatatype()) + { + // don't register non-datatype terms, instead we return the + // selector chain n. + return n; + } + const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); + if (!dt.isSygus()) + { + // don't register non-sygus-datatype terms + return n; + } + Assert(nv.getKind() == APPLY_CONSTRUCTOR); + NodeManager* nm = NodeManager::currentNM(); + // we call the body of this function in a bottom-up fashion + // this ensures that the "abstraction" of the model value is available + if( nv.getNumChildren()>0 ){ + unsigned cindex = utils::indexOf(nv.getOperator()); + std::vector rcons_children; + rcons_children.push_back(nv.getOperator()); + bool childrenChanged = false; + for (unsigned i = 0, nchild = nv.getNumChildren(); i < nchild; i++) + { + Node sel = nm->mkNode( + APPLY_SELECTOR_TOTAL, + Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)), + n); + Node nvc = registerSearchValue(a, + sel, + nv[i], + d + 1, + lemmas, + isVarAgnostic, + doSym && (!isVarAgnostic || i == 0)); + if (nvc.isNull()) + { + return Node::null(); + } + rcons_children.push_back(nvc); + childrenChanged = childrenChanged || nvc != nv[i]; + } + // reconstruct the value, which may be a skeleton + if (childrenChanged) + { + nv = nm->mkNode(APPLY_CONSTRUCTOR, rcons_children); + } + } + if (!doSym) + { + return nv; + } + Trace("sygus-sb-debug2") << "Registering search value " << n << " -> " << nv << std::endl; + std::map var_count; + Node cnv = d_tds->canonizeBuiltin(nv, var_count); + Trace("sygus-sb-debug") << " ...canonized value is " << cnv << std::endl; + // must do this for all nodes, regardless of top-level + if (d_cache[a].d_search_val_proc.find(cnv) + == d_cache[a].d_search_val_proc.end()) + { + d_cache[a].d_search_val_proc.insert(cnv); + // get the root (for PBE symmetry breaking) + Assert(d_anchor_to_conj.find(a) != d_anchor_to_conj.end()); + quantifiers::SynthConjecture* aconj = d_anchor_to_conj[a]; + Assert(aconj != NULL); + Trace("sygus-sb-debug") << " ...register search value " << cnv + << ", type=" << tn << std::endl; + Node bv = d_tds->sygusToBuiltin(cnv, tn); + Trace("sygus-sb-debug") << " ......builtin is " << bv << std::endl; + Node bvr = d_tds->getExtRewriter()->extendedRewrite(bv); + Trace("sygus-sb-debug") << " ......search value rewrites to " << bvr << std::endl; + Trace("dt-sygus") << " * DT builtin : " << n << " -> " << bvr << std::endl; + unsigned sz = d_tds->getSygusTermSize( nv ); + if( d_tds->involvesDivByZero( bvr ) ){ + quantifiers::DivByZeroSygusInvarianceTest dbzet; + Trace("sygus-sb-mexp-debug") << "Minimize explanation for div-by-zero in " + << bv << std::endl; + registerSymBreakLemmaForValue( + a, nv, dbzet, Node::null(), var_count, lemmas); + return Node::null(); + }else{ + std::unordered_map::iterator itsv = + d_cache[a].d_search_val[tn].find(bvr); + Node bad_val_bvr; + bool by_examples = false; + if( itsv==d_cache[a].d_search_val[tn].end() ){ + // TODO (github #1210) conjecture-specific symmetry breaking + // this should be generalized and encapsulated within the + // SynthConjecture class. + // Is it equivalent under examples? + Node bvr_equiv; + if (options::sygusSymBreakPbe()) + { + if (aconj->getPbe()->hasExamples(a)) + { + bvr_equiv = aconj->getPbe()->addSearchVal(tn, a, bvr); + } + } + if( !bvr_equiv.isNull() ){ + if( bvr_equiv!=bvr ){ + Trace("sygus-sb-debug") << "......adding search val for " << bvr << " returned " << bvr_equiv << std::endl; + Assert(d_cache[a].d_search_val[tn].find(bvr_equiv) + != d_cache[a].d_search_val[tn].end()); + Trace("sygus-sb-debug") << "......search value was " << d_cache[a].d_search_val[tn][bvr_equiv] << std::endl; + if( Trace.isOn("sygus-sb-exc") ){ + Node prev = d_tds->sygusToBuiltin( d_cache[a].d_search_val[tn][bvr_equiv], tn ); + Trace("sygus-sb-exc") << " ......programs " << prev << " and " << bv << " are equivalent up to examples." << std::endl; + } + bad_val_bvr = bvr_equiv; + by_examples = true; + } + } + //store rewritten values, regardless of whether it will be considered + d_cache[a].d_search_val[tn][bvr] = nv; + d_cache[a].d_search_val_sz[tn][bvr] = sz; + }else{ + bad_val_bvr = bvr; + if( Trace.isOn("sygus-sb-exc") ){ + Node prev_bv = d_tds->sygusToBuiltin( itsv->second, tn ); + Trace("sygus-sb-exc") << " ......programs " << prev_bv << " and " << bv << " rewrite to " << bvr << "." << std::endl; + } + } + + if (options::sygusRewVerify()) + { + if (bv != bvr) + { + // add to the sampler database object + std::map::iterator its = + d_sampler[a].find(tn); + if (its == d_sampler[a].end()) + { + d_sampler[a][tn].initializeSygus( + d_tds, nv, options::sygusSamples(), false); + its = d_sampler[a].find(tn); + } + // check equivalent + its->second.checkEquivalent(bv, bvr); + } + } + + if( !bad_val_bvr.isNull() ){ + Node bad_val = nv; + Node bad_val_o = d_cache[a].d_search_val[tn][bad_val_bvr]; + Assert(d_cache[a].d_search_val_sz[tn].find(bad_val_bvr) + != d_cache[a].d_search_val_sz[tn].end()); + unsigned prev_sz = d_cache[a].d_search_val_sz[tn][bad_val_bvr]; + bool doFlip = (prev_sz > sz); + if (doFlip) + { + //swap : the excluded value is the previous + d_cache[a].d_search_val_sz[tn][bad_val_bvr] = sz; + bad_val = d_cache[a].d_search_val[tn][bad_val_bvr]; + bad_val_o = nv; + if (Trace.isOn("sygus-sb-exc")) + { + Trace("sygus-sb-exc") << "Flip : exclude "; + quantifiers::TermDbSygus::toStreamSygus("sygus-sb-exc", bad_val); + Trace("sygus-sb-exc") << " instead of "; + quantifiers::TermDbSygus::toStreamSygus("sygus-sb-exc", bad_val_o); + Trace("sygus-sb-exc") << ", since its size is " << sz << " < " + << prev_sz << std::endl; + } + sz = prev_sz; + } + if( Trace.isOn("sygus-sb-exc") ){ + Node bad_val_bv = d_tds->sygusToBuiltin( bad_val, tn ); + Trace("sygus-sb-exc") << " ........exclude : " << bad_val_bv; + if( by_examples ){ + Trace("sygus-sb-exc") << " (by examples)"; + } + Trace("sygus-sb-exc") << std::endl; + } + Assert(d_tds->getSygusTermSize(bad_val) == sz); + + // generalize the explanation for why the analog of bad_val + // is equivalent to bvr + quantifiers::EquivSygusInvarianceTest eset; + eset.init(d_tds, tn, aconj, a, bvr); + + Trace("sygus-sb-mexp-debug") << "Minimize explanation for eval[" << d_tds->sygusToBuiltin( bad_val ) << "] = " << bvr << std::endl; + registerSymBreakLemmaForValue( + a, bad_val, eset, bad_val_o, var_count, lemmas); + + // other generalization criteria go here + + // If the exclusion was flipped, we are excluding a previous value + // instead of the current one. Hence, the current value is a legal + // value that we will consider. + if (!doFlip) + { + return Node::null(); + } + } + } + } + return nv; +} + +void SygusExtension::registerSymBreakLemmaForValue( + Node a, + Node val, + quantifiers::SygusInvarianceTest& et, + Node valr, + std::map& var_count, + std::vector& lemmas) +{ + TypeNode tn = val.getType(); + Node x = getFreeVar(tn); + unsigned sz = d_tds->getSygusTermSize(val); + std::vector exp; + d_tds->getExplain()->getExplanationFor(x, val, exp, et, valr, var_count, sz); + Node lem = + exp.size() == 1 ? exp[0] : NodeManager::currentNM()->mkNode(AND, exp); + lem = lem.negate(); + Trace("sygus-sb-exc") << " ........exc lemma is " << lem << ", size = " << sz + << std::endl; + registerSymBreakLemma(tn, lem, sz, a, lemmas); +} + +void SygusExtension::registerSymBreakLemma( TypeNode tn, Node lem, unsigned sz, Node a, std::vector< Node >& lemmas ) { + // lem holds for all terms of type tn, and is applicable to terms of size sz + Trace("sygus-sb-debug") << " register sym break lemma : " << lem + << std::endl; + Trace("sygus-sb-debug") << " anchor : " << a << std::endl; + Trace("sygus-sb-debug") << " type : " << tn << std::endl; + Trace("sygus-sb-debug") << " size : " << sz << std::endl; + Assert(!a.isNull()); + d_cache[a].d_sb_lemmas[tn][sz].push_back( lem ); + TNode x = getFreeVar( tn ); + unsigned csz = getSearchSizeForAnchor( a ); + int max_depth = ((int)csz)-((int)sz); + NodeManager* nm = NodeManager::currentNM(); + for( int d=0; d<=max_depth; d++ ){ + std::map< unsigned, std::vector< Node > >::iterator itt = d_cache[a].d_search_terms[tn].find( d ); + if( itt!=d_cache[a].d_search_terms[tn].end() ){ + for (const TNode& t : itt->second) + { + if (!options::sygusSymBreakLazy() + || d_active_terms.find(t) != d_active_terms.end()) + { + Node slem = lem.substitute(x, t); + Node rlv = getRelevancyCondition(t); + if (!rlv.isNull()) + { + slem = nm->mkNode(OR, rlv, slem); + } + lemmas.push_back(slem); + } + } + } + } +} + +void SygusExtension::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, std::vector< Node >& lemmas ) { + Assert(d_term_to_anchor.find(t) != d_term_to_anchor.end()); + Node a = d_term_to_anchor[t]; + addSymBreakLemmasFor( tn, t, d, a, lemmas ); +} + +void SygusExtension::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, Node a, std::vector< Node >& lemmas ) { + Assert(t.getType() == tn); + Assert(!a.isNull()); + Trace("sygus-sb-debug2") << "add sym break lemmas for " << t << " " << d + << " " << a << std::endl; + std::map< TypeNode, std::map< unsigned, std::vector< Node > > >::iterator its = d_cache[a].d_sb_lemmas.find( tn ); + Node rlv = getRelevancyCondition(t); + NodeManager* nm = NodeManager::currentNM(); + if( its != d_cache[a].d_sb_lemmas.end() ){ + TNode x = getFreeVar( tn ); + //get symmetry breaking lemmas for this term + unsigned csz = getSearchSizeForAnchor( a ); + int max_sz = ((int)csz) - ((int)d); + Trace("sygus-sb-debug2") + << "add lemmas up to size " << max_sz << ", which is (search_size) " + << csz << " - (depth) " << d << std::endl; + std::unordered_map cache; + for( std::map< unsigned, std::vector< Node > >::iterator it = its->second.begin(); it != its->second.end(); ++it ){ + if( (int)it->first<=max_sz ){ + for (const Node& lem : it->second) + { + Node slem = lem.substitute(x, t, cache); + // add the relevancy condition for t + if (!rlv.isNull()) + { + slem = nm->mkNode(OR, rlv, slem); + } + lemmas.push_back(slem); + } + } + } + } + Trace("sygus-sb-debug2") << "...finished." << std::endl; +} + +void SygusExtension::preRegisterTerm( TNode n, std::vector< Node >& lemmas ) { + if( n.isVar() ){ + Trace("sygus-sb-debug") << "Pre-register variable : " << n << std::endl; + registerSizeTerm( n, lemmas ); + } +} + +void SygusExtension::registerSizeTerm(Node e, std::vector& lemmas) +{ + if (d_register_st.find(e) != d_register_st.end()) + { + // already registered + return; + } + TypeNode etn = e.getType(); + if (!etn.isDatatype()) + { + // not a datatype term + d_register_st[e] = false; + return; + } + const Datatype& dt = etn.getDatatype(); + if (!dt.isSygus()) + { + // not a sygus datatype term + d_register_st[e] = false; + return; + } + if (!d_tds->isEnumerator(e)) + { + // not sure if it is a size term or not (may be registered later?) + return; + } + d_register_st[e] = true; + Node ag = d_tds->getActiveGuardForEnumerator(e); + if (!ag.isNull()) + { + d_anchor_to_active_guard[e] = ag; + std::map>::iterator itaas = + d_anchor_to_ag_strategy.find(e); + if (itaas == d_anchor_to_ag_strategy.end()) + { + d_anchor_to_ag_strategy[e].reset( + new DecisionStrategySingleton("sygus_enum_active", + ag, + d_td->getSatContext(), + d_td->getValuation())); + } + d_td->getDecisionManager()->registerStrategy( + DecisionManager::STRAT_DT_SYGUS_ENUM_ACTIVE, + d_anchor_to_ag_strategy[e].get()); + } + Node m; + if (!ag.isNull()) + { + // if it has an active guard (it is an enumerator), use itself as measure + // term. This will enforce fairness on it independently. + m = e; + } + else + { + // otherwise we enforce fairness in a unified way for all + if (d_generic_measure_term.isNull()) + { + // choose e as master for all future terms + d_generic_measure_term = e; + } + m = d_generic_measure_term; + } + Trace("sygus-sb") << "Sygus : register size term : " << e << " with measure " + << m << std::endl; + registerMeasureTerm(m); + d_szinfo[m]->d_anchors.push_back(e); + d_anchor_to_measure_term[e] = m; + NodeManager* nm = NodeManager::currentNM(); + if (options::sygusFair() == SYGUS_FAIR_DT_SIZE) + { + // update constraints on the measure term + Node slem; + if (options::sygusFairMax()) + { + Node ds = nm->mkNode(DT_SIZE, e); + slem = nm->mkNode(LEQ, ds, d_szinfo[m]->getOrMkMeasureValue(lemmas)); + }else{ + Node mt = d_szinfo[m]->getOrMkActiveMeasureValue(lemmas); + Node new_mt = d_szinfo[m]->getOrMkActiveMeasureValue(lemmas, true); + Node ds = nm->mkNode(DT_SIZE, e); + slem = mt.eqNode(nm->mkNode(PLUS, new_mt, ds)); + } + Trace("sygus-sb") << "...size lemma : " << slem << std::endl; + lemmas.push_back(slem); + } + if (d_tds->isVariableAgnosticEnumerator(e)) + { + // if it is variable agnostic, enforce top-level constraint that says no + // variables occur pre-traversal at top-level + Node varList = Node::fromExpr(dt.getSygusVarList()); + std::vector constraints; + quantifiers::SygusTypeInfo& eti = d_tds->getTypeInfo(etn); + for (const Node& v : varList) + { + unsigned sc = eti.getSubclassForVar(v); + // no symmetry breaking occurs for variables in singleton subclasses + if (eti.getNumSubclassVars(sc) > 1) + { + Node preRootOp = getTraversalPredicate(etn, v, true); + Node preRoot = nm->mkNode(APPLY_UF, preRootOp, e); + constraints.push_back(preRoot.negate()); + } + } + if (!constraints.empty()) + { + Node preNoVar = constraints.size() == 1 ? constraints[0] + : nm->mkNode(AND, constraints); + Node preNoVarProc = eliminateTraversalPredicates(preNoVar); + Trace("sygus-sb") << "...variable order : " << preNoVarProc << std::endl; + Trace("sygus-sb-tp") << "...variable order : " << preNoVarProc + << std::endl; + lemmas.push_back(preNoVarProc); + } + } +} + +void SygusExtension::registerMeasureTerm( Node m ) { + std::map>::iterator it = + d_szinfo.find(m); + if( it==d_szinfo.end() ){ + Trace("sygus-sb") << "Sygus : register measure term : " << m << std::endl; + d_szinfo[m].reset(new SygusSizeDecisionStrategy( + m, d_td->getSatContext(), d_td->getValuation())); + // register this as a decision strategy + d_td->getDecisionManager()->registerStrategy( + DecisionManager::STRAT_DT_SYGUS_ENUM_SIZE, d_szinfo[m].get()); + } +} + +void SygusExtension::notifySearchSize( Node m, unsigned s, Node exp, std::vector< Node >& lemmas ) { + std::map>::iterator its = + d_szinfo.find(m); + Assert(its != d_szinfo.end()); + if( its->second->d_search_size.find( s )==its->second->d_search_size.end() ){ + its->second->d_search_size[s] = true; + its->second->d_search_size_exp[s] = exp; + Assert(s == 0 + || its->second->d_search_size.find(s - 1) + != its->second->d_search_size.end()); + Trace("sygus-fair") << "SygusExtension:: now considering term measure : " << s << " for " << m << std::endl; + Assert(s >= its->second->d_curr_search_size); + while( s>its->second->d_curr_search_size ){ + incrementCurrentSearchSize( m, lemmas ); + } + Trace("sygus-fair") << "...finish increment for term measure : " << s << std::endl; + /* + //re-add all testers (some may now be relevant) TODO + for( IntMap::const_iterator it = d_testers.begin(); it != d_testers.end(); + ++it ){ Node n = (*it).first; NodeMap::const_iterator itx = + d_testers_exp.find( n ); if( itx!=d_testers_exp.end() ){ int tindex = + (*it).second; Node exp = (*itx).second; assertTester( tindex, n, exp, lemmas + ); }else{ Assert( false ); + } + } + */ + } +} + +unsigned SygusExtension::getSearchSizeFor( Node n ) { + Trace("sygus-sb-debug2") << "get search size for term : " << n << std::endl; + std::unordered_map::iterator ita = + d_term_to_anchor.find(n); + Assert(ita != d_term_to_anchor.end()); + return getSearchSizeForAnchor( ita->second ); +} + +unsigned SygusExtension::getSearchSizeForAnchor( Node a ) { + Trace("sygus-sb-debug2") << "get search size for anchor : " << a << std::endl; + std::map< Node, Node >::iterator it = d_anchor_to_measure_term.find( a ); + Assert(it != d_anchor_to_measure_term.end()); + return getSearchSizeForMeasureTerm(it->second); +} + +unsigned SygusExtension::getSearchSizeForMeasureTerm(Node m) +{ + Trace("sygus-sb-debug2") << "get search size for measure : " << m << std::endl; + std::map>::iterator its = + d_szinfo.find(m); + Assert(its != d_szinfo.end()); + return its->second->d_curr_search_size; +} + +void SygusExtension::incrementCurrentSearchSize( Node m, std::vector< Node >& lemmas ) { + std::map>::iterator itsz = + d_szinfo.find(m); + Assert(itsz != d_szinfo.end()); + itsz->second->d_curr_search_size++; + Trace("sygus-fair") << " register search size " << itsz->second->d_curr_search_size << " for " << m << std::endl; + NodeManager* nm = NodeManager::currentNM(); + for( std::map< Node, SearchCache >::iterator itc = d_cache.begin(); itc != d_cache.end(); ++itc ){ + Node a = itc->first; + Trace("sygus-fair-debug") << " look at anchor " << a << "..." << std::endl; + // check whether a is bounded by m + Assert(d_anchor_to_measure_term.find(a) != d_anchor_to_measure_term.end()); + if( d_anchor_to_measure_term[a]==m ){ + for( std::map< TypeNode, std::map< unsigned, std::vector< Node > > >::iterator its = itc->second.d_sb_lemmas.begin(); + its != itc->second.d_sb_lemmas.end(); ++its ){ + TypeNode tn = its->first; + TNode x = getFreeVar( tn ); + for( std::map< unsigned, std::vector< Node > >::iterator it = its->second.begin(); it != its->second.end(); ++it ){ + unsigned sz = it->first; + int new_depth = ((int)itsz->second->d_curr_search_size) - ((int)sz); + std::map< unsigned, std::vector< Node > >::iterator itt = itc->second.d_search_terms[tn].find( new_depth ); + if( itt!=itc->second.d_search_terms[tn].end() ){ + for (const TNode& t : itt->second) + { + if (!options::sygusSymBreakLazy() + || (d_active_terms.find(t) != d_active_terms.end() + && !it->second.empty())) + { + Node rlv = getRelevancyCondition(t); + std::unordered_map cache; + for (const Node& lem : it->second) + { + Node slem = lem.substitute(x, t, cache); + slem = nm->mkNode(OR, rlv, slem); + lemmas.push_back(slem); + } + } + } + } + } + } + } + } +} + +void SygusExtension::check( std::vector< Node >& lemmas ) { + Trace("sygus-sb") << "SygusExtension::check" << std::endl; + + // check for externally registered symmetry breaking lemmas + std::vector anchors; + if (d_tds->hasSymBreakLemmas(anchors)) + { + for (const Node& a : anchors) + { + // is this a registered enumerator? + if (d_register_st.find(a) != d_register_st.end()) + { + // symmetry breaking lemmas should only be for enumerators + Assert(d_register_st[a]); + // If this is a non-basic enumerator, process its symmetry breaking + // clauses. Since this class is not responsible for basic enumerators, + // their symmetry breaking clauses are ignored. + if (!d_tds->isBasicEnumerator(a)) + { + std::vector sbl; + d_tds->getSymBreakLemmas(a, sbl); + for (const Node& lem : sbl) + { + if (d_tds->isSymBreakLemmaTemplate(lem)) + { + // register the lemma template + TypeNode tn = d_tds->getTypeForSymBreakLemma(lem); + unsigned sz = d_tds->getSizeForSymBreakLemma(lem); + registerSymBreakLemma(tn, lem, sz, a, lemmas); + } + else + { + Trace("dt-sygus-debug") + << "DT sym break lemma : " << lem << std::endl; + // it is a normal lemma + lemmas.push_back(lem); + } + } + d_tds->clearSymBreakLemmas(a); + } + } + } + if (!lemmas.empty()) + { + return; + } + } + + // register search values, add symmetry breaking lemmas if applicable + std::vector es; + d_tds->getEnumerators(es); + bool needsRecheck = false; + // for each enumerator registered to d_tds + for (Node& prog : es) + { + if (d_register_st.find(prog) == d_register_st.end()) + { + // not yet registered, do so now + registerSizeTerm(prog, lemmas); + needsRecheck = true; + } + else + { + Trace("dt-sygus-debug") << "Checking model value of " << prog << "..." + << std::endl; + Assert(prog.getType().isDatatype()); + Node progv = d_td->getValuation().getModel()->getValue( prog ); + if (Trace.isOn("dt-sygus")) + { + Trace("dt-sygus") << "* DT model : " << prog << " -> "; + std::stringstream ss; + Printer::getPrinter(options::outputLanguage()) + ->toStreamSygus(ss, progv); + Trace("dt-sygus") << ss.str() << std::endl; + } + // first check that the value progv for prog is what we expected + bool isExc = true; + if (checkValue(prog, progv, 0, lemmas)) + { + isExc = false; + //debugging : ensure fairness was properly handled + if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){ + Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, prog ); + Node prog_szv = d_td->getValuation().getModel()->getValue( prog_sz ); + Node progv_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, progv ); + + Trace("sygus-sb") << " Mv[" << prog << "] = " << progv << ", size = " << prog_szv << std::endl; + if( prog_szv.getConst().getNumerator().toUnsignedInt() > getSearchSizeForAnchor( prog ) ){ + AlwaysAssert(false); + Node szlem = NodeManager::currentNM()->mkNode( kind::OR, prog.eqNode( progv ).negate(), + prog_sz.eqNode( progv_sz ) ); + Trace("sygus-sb-warn") << "SygusSymBreak : WARNING : adding size correction : " << szlem << std::endl; + lemmas.push_back(szlem); + isExc = true; + } + } + + // register the search value ( prog -> progv ), this may invoke symmetry + // breaking + if (!isExc && options::sygusSymBreakDynamic()) + { + bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(prog); + // check that it is unique up to theory-specific rewriting and + // conjecture-specific symmetry breaking. + Node rsv = registerSearchValue( + prog, prog, progv, 0, lemmas, isVarAgnostic, true); + if (rsv.isNull()) + { + isExc = true; + Trace("sygus-sb") << " SygusExtension::check: ...added new symmetry breaking lemma for " << prog << "." << std::endl; + } + else + { + Trace("dt-sygus") << " ...success." << std::endl; + } + } + } + SygusSymBreakOkAttribute ssbo; + prog.setAttribute(ssbo, !isExc); + } + } + Trace("sygus-sb") << "SygusExtension::check: finished." << std::endl; + if (needsRecheck) + { + Trace("sygus-sb") << " SygusExtension::rechecking..." << std::endl; + return check(lemmas); + } + + if (Trace.isOn("cegqi-engine") && !d_szinfo.empty()) + { + if (lemmas.empty()) + { + Trace("cegqi-engine") << "*** Sygus : passed datatypes check. term size(s) : "; + for (std::pair>& + p : d_szinfo) + { + SygusSizeDecisionStrategy* s = p.second.get(); + Trace("cegqi-engine") << s->d_curr_search_size << " "; + } + Trace("cegqi-engine") << std::endl; + } + else + { + Trace("cegqi-engine") + << "*** Sygus : produced symmetry breaking lemmas" << std::endl; + for (const Node& lem : lemmas) + { + Trace("cegqi-engine-debug") << " " << lem << std::endl; + } + } + } +} + +bool SygusExtension::checkValue(Node n, + Node vn, + int ind, + std::vector& lemmas) +{ + if (vn.getKind() != kind::APPLY_CONSTRUCTOR) + { + // all datatype terms should be constant here + Assert(!vn.getType().isDatatype()); + return true; + } + NodeManager* nm = NodeManager::currentNM(); + if (Trace.isOn("sygus-sb-check-value")) + { + Node prog_sz = nm->mkNode(DT_SIZE, n); + Node prog_szv = d_td->getValuation().getModel()->getValue( prog_sz ); + for( int i=0; igetEqualityEngine()->hasTerm(tst); + Node tstrep; + if (hastst) + { + tstrep = d_td->getEqualityEngine()->getRepresentative(tst); + } + if (!hastst || tstrep != d_true) + { + Trace("sygus-check-value") << "- has tester : " << tst << " : " + << (hastst ? "true" : "false"); + Trace("sygus-check-value") << ", value=" << tstrep << std::endl; + if( !hastst ){ + // This should not happen generally, it is caused by a sygus term not + // being assigned a tester. + Node split = utils::mkSplit(n, dt); + Trace("sygus-sb") << " SygusExtension::check: ...WARNING: considered " + "missing split for " + << n << "." << std::endl; + Assert(!split.isNull()); + lemmas.push_back( split ); + return false; + } + } + for( unsigned i=0; imkNode( + APPLY_SELECTOR_TOTAL, + Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)), + n); + if (!checkValue(sel, vn[i], ind + 1, lemmas)) + { + return false; + } + } + return true; +} + +Node SygusExtension::getCurrentTemplate( Node n, std::map< TypeNode, int >& var_count ) { + if( d_active_terms.find( n )!=d_active_terms.end() ){ + TypeNode tn = n.getType(); + IntMap::const_iterator it = d_testers.find( n ); + Assert(it != d_testers.end()); + const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); + int tindex = (*it).second; + Assert(tindex >= 0); + Assert(tindex < (int)dt.getNumConstructors()); + std::vector< Node > children; + children.push_back( Node::fromExpr( dt[tindex].getConstructor() ) ); + for( unsigned i=0; imkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( tn.toType(), i ) ), n ); + Node cc = getCurrentTemplate( sel, var_count ); + children.push_back( cc ); + } + return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); + }else{ + return d_tds->getFreeVarInc( n.getType(), var_count ); + } +} + +Node SygusExtension::SygusSizeDecisionStrategy::getOrMkMeasureValue( + std::vector& lemmas) +{ + if (d_measure_value.isNull()) + { + d_measure_value = NodeManager::currentNM()->mkSkolem( + "mt", NodeManager::currentNM()->integerType()); + lemmas.push_back(NodeManager::currentNM()->mkNode( + kind::GEQ, + d_measure_value, + NodeManager::currentNM()->mkConst(Rational(0)))); + } + return d_measure_value; +} + +Node SygusExtension::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue( + std::vector& lemmas, bool mkNew) +{ + if (mkNew) + { + Node new_mt = NodeManager::currentNM()->mkSkolem( + "mt", NodeManager::currentNM()->integerType()); + lemmas.push_back(NodeManager::currentNM()->mkNode( + kind::GEQ, new_mt, NodeManager::currentNM()->mkConst(Rational(0)))); + d_measure_value_active = new_mt; + } + else if (d_measure_value_active.isNull()) + { + d_measure_value_active = getOrMkMeasureValue(lemmas); + } + return d_measure_value_active; +} + +Node SygusExtension::SygusSizeDecisionStrategy::mkLiteral(unsigned s) +{ + if (options::sygusFair() == SYGUS_FAIR_NONE) + { + return Node::null(); + } + if (options::sygusAbortSize() != -1 + && static_cast(s) > options::sygusAbortSize()) + { + std::stringstream ss; + ss << "Maximum term size (" << options::sygusAbortSize() + << ") for enumerative SyGuS exceeded."; + throw LogicException(ss.str()); + } + Assert(!d_this.isNull()); + NodeManager* nm = NodeManager::currentNM(); + Trace("cegqi-engine") << "******* Sygus : allocate size literal " << s + << " for " << d_this << std::endl; + return nm->mkNode(DT_SYGUS_BOUND, d_this, nm->mkConst(Rational(s))); +} + +int SygusExtension::getGuardStatus( Node g ) { + bool value; + if( d_td->getValuation().hasSatValue( g, value ) ) { + if( value ){ + return 1; + }else{ + return -1; + } + }else{ + return 0; + } +} + diff --git a/src/theory/datatypes/sygus_extension.h b/src/theory/datatypes/sygus_extension.h new file mode 100644 index 000000000..631f11040 --- /dev/null +++ b/src/theory/datatypes/sygus_extension.h @@ -0,0 +1,721 @@ +/********************* */ +/*! \file sygus_extension.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The sygus extension of the theory of datatypes. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__DATATYPES__SYGUS_EXTENSION_H +#define CVC4__THEORY__DATATYPES__SYGUS_EXTENSION_H + +#include +#include + +#include "context/cdhashmap.h" +#include "context/cdhashset.h" +#include "context/cdlist.h" +#include "context/cdo.h" +#include "context/context.h" +#include "expr/datatype.h" +#include "expr/node.h" +#include "theory/datatypes/sygus_simple_sym.h" +#include "theory/quantifiers/sygus/sygus_explain.h" +#include "theory/quantifiers/sygus/synth_conjecture.h" +#include "theory/quantifiers/sygus_sampler.h" +#include "theory/quantifiers/term_database.h" + +namespace CVC4 { +namespace theory { +namespace datatypes { + +class TheoryDatatypes; + +/** + * This is the sygus extension of the decision procedure for quantifier-free + * inductive datatypes. At a high level, this class takes as input a + * set of asserted testers is-C1( x ), is-C2( x.1 ), is-C3( x.2 ), and + * generates lemmas that restrict the models of x, if x is a "sygus enumerator" + * (see TermDbSygus::registerEnumerator). + * + * Some of these techniques are described in these papers: + * "Refutation-Based Synthesis in SMT", Reynolds et al 2017. + * "Sygus Techniques in the Core of an SMT Solver", Reynolds et al 2017. + * + * This class enforces two decisions stragies via calls to registerStrategy + * of the owning theory's DecisionManager: + * (1) Positive decisions on the active guards G of enumerators e registered + * to this class. These assert "there are more values to enumerate for e". + * (2) Positive bounds (DT_SYGUS_BOUND m n) for "measure terms" m (see below), + * where n is a non-negative integer. This asserts "the measure of terms + * we are enumerating for enumerators whose measure term m is at most n", + * where measure is commonly term size, but can also be height. + * + * We prioritize decisions of form (1) before (2). Both kinds of decision are + * critical for solution completeness, which is enforced by DecisionManager. + */ +class SygusExtension +{ + typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap; + typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; + typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; + typedef context::CDHashSet NodeSet; + + public: + SygusExtension(TheoryDatatypes* td, + QuantifiersEngine* qe, + context::Context* c); + ~SygusExtension(); + /** + * Notify this class that tester for constructor tindex has been asserted for + * n. Exp is the literal corresponding to this tester. This method may add + * lemmas to the vector lemmas, for details see assertTesterInternal below. + * These lemmas are sent out on the output channel of datatypes by the caller. + */ + void assertTester(int tindex, TNode n, Node exp, std::vector& lemmas); + /** + * Notify this class that literal n has been asserted with the given + * polarity. This method may add lemmas to the vector lemmas, for instance + * based on inferring consequences of (not) n. One example is if n is + * (DT_SIZE_BOUND x n), we add the lemma: + * (DT_SIZE_BOUND x n) <=> ((DT_SIZE x) <= n ) + */ + void assertFact(Node n, bool polarity, std::vector& lemmas); + /** pre-register term n + * + * This is called when n is pre-registered with the theory of datatypes. + * If n is a sygus enumerator, then we may add lemmas to the vector lemmas + * that are used to enforce fairness regarding the size of n. + */ + void preRegisterTerm(TNode n, std::vector& lemmas); + /** check + * + * This is called at last call effort, when the current model assignment is + * satisfiable according to the quantifier-free decision procedures and a + * model is built. This method may add lemmas to the vector lemmas based + * on dynamic symmetry breaking techniques, based on the model values of + * all preregistered enumerators. + */ + void check(std::vector& lemmas); + private: + /** Pointer to the datatype theory that owns this class. */ + TheoryDatatypes* d_td; + /** Pointer to the sygus term database */ + quantifiers::TermDbSygus* d_tds; + /** the simple symmetry breaking utility */ + SygusSimpleSymBreak d_ssb; + /** + * Map from terms to the index of the tester that is asserted for them in + * the current SAT context. In other words, if d_testers[n] = 2, then the + * tester is-C_2(n) is asserted in this SAT context. + */ + IntMap d_testers; + /** + * Map from terms to the tester asserted for them. In the example above, + * d_testers[n] = is-C_2(n). + */ + NodeMap d_testers_exp; + /** + * The set of (selector chain) terms that are active in the current SAT + * context. A selector chain term S_n( ... S_1( x )... ) is active if either: + * (1) n=0 and x is a sygus enumerator, + * or: + * (2.1) S_{n-1}( ... S_1( x )) is active, + * (2.2) is-C( S_{n-1}( ... S_1( x )) ) is asserted in this SAT context, and + * (2.3) S_n is a selector for constructor C. + */ + NodeSet d_active_terms; + /** + * Map from enumerators to a lower bound on their size in the current SAT + * context. + */ + IntMap d_currTermSize; + /** zero */ + Node d_zero; + /** true */ + Node d_true; + /** + * Map from terms (selector chains) to their anchors. The anchor of a + * selector chain S1( ... Sn( x ) ... ) is x. + */ + std::unordered_map d_term_to_anchor; + /** + * Map from anchors to the conjecture they are associated with. + */ + std::map d_anchor_to_conj; + /** + * Map from terms (selector chains) to their depth. The depth of a selector + * chain S1( ... Sn( x ) ... ) is: + * weight( S1 ) + ... + weight( Sn ), + * where weight is the selector weight of Si + * (see SygusTermDatabase::getSelectorWeight). + */ + std::unordered_map d_term_to_depth; + /** + * Map from terms (selector chains) to whether they are the topmost term + * of their type. For example, if: + * S1 : T1 -> T2 + * S2 : T2 -> T2 + * S3 : T2 -> T1 + * S4 : T1 -> T3 + * Then, x, S1( x ), and S4( S3( S2( S1( x ) ) ) ) are top-level terms, + * whereas S2( S1( x ) ) and S3( S2( S1( x ) ) ) are not. + */ + std::unordered_map d_is_top_level; + /** + * Returns true if the selector chain n is top-level based on the above + * definition, when tn is the type of n. + */ + bool computeTopLevel( TypeNode tn, Node n ); +private: + /** This caches all information regarding symmetry breaking for an anchor. */ + class SearchCache + { + public: + SearchCache(){} + /** + * A cache of all search terms for (types, sizes). See registerSearchTerm + * for definition of search terms. + */ + std::map< TypeNode, std::map< unsigned, std::vector< Node > > > d_search_terms; + /** A cache of all symmetry breaking lemma templates for (types, sizes). */ + std::map< TypeNode, std::map< unsigned, std::vector< Node > > > d_sb_lemmas; + /** search value + * + * For each sygus type, a map from a builtin term to a sygus term for that + * type that we encountered during the search whose analog rewrites to that + * term. The range of this map can be updated if we later encounter a sygus + * term that also rewrites to the builtin value but has a smaller term size. + */ + std::map> + d_search_val; + /** the size of terms in the range of d_search val. */ + std::map> + d_search_val_sz; + /** For each term, whether this cache has processed that term */ + std::unordered_set d_search_val_proc; + }; + /** An instance of the above cache, for each anchor */ + std::map< Node, SearchCache > d_cache; + //-----------------------------------traversal predicates + /** pre/post traversal predicates for each type, variable + * + * This stores predicates (pre, post) whose semantics correspond to whether + * a variable has occurred by a (pre, post) traversal of a symbolic term, + * where index = 0 corresponds to pre, index = 1 corresponds to post. For + * details, see getTraversalPredicate below. + */ + std::map> d_traversal_pred[2]; + /** traversal applications to Boolean variables + * + * This maps each application of a traversal predicate pre_x( t ) or + * post_x( t ) to a fresh Boolean variable. + */ + std::map d_traversal_bool; + /** get traversal predicate + * + * Get the predicates (pre, post) whose semantics correspond to whether + * a variable has occurred by this point in a (pre, post) traversal of a term. + * The type of getTraversalPredicate(tn, n, _) is tn -> Bool. + * + * For example, consider the term: + * f( x_1, g( x_2, x_3 ) ) + * and a left-to-right, depth-first traversal of this term. Let e be + * a variable of the same type as this term. We say that for the above term: + * pre_{x_1} is false for e, e.1 and true for e.2, e.2.1, e.2.2 + * pre_{x_2} is false for e, e.1, e.2, e.2.1, and true for e.2.2 + * pre_{x_3} is false for e, e.1, e.2, e.2.1, e.2.2 + * post_{x_1} is true for e.1, e.2.1, e.2.2, e.2, e + * post_{x_2} is false for e.1 and true for e.2.1, e.2.2, e.2, e + * post_{x_3} is false for e.1, e.2.1 and true for e.2.2, e.2, e + * + * We enforce a symmetry breaking scheme for each enumerator e that is + * "variable-agnostic" (see argument isVarAgnostic in registerEnumerator) + * that ensures the variables are ordered. This scheme makes use of these + * predicates, described in the following: + * + * Let x_1, ..., x_m be variables that occur in the same subclass in the type + * of e (see TermDbSygus::getSubclassForVar). + * For i = 1, ..., m: + * // each variable does not occur initially in a traversal of e + * ~pre_{x_i}( e ) AND + * // for each subterm of e + * template z. + * // if this is variable x_i, then x_{i-1} must have already occurred + * is-x_i( z ) => pre_{x_{i-1}}( z ) AND + * for args a = 1...n + * // pre-definition for each argument of this term + * pre_{x_i}( z.a ) = a=0 ? pre_{x_i}( z ) : post_{x_i}( z.{a-1} ) AND + * // post-definition for this term + * post_{x_i}( z ) = post_{x_i}( z.n ) OR is-x_i( z ) + * + * For clarity, above we have written pre and post as first-order predicates. + * However, applications of pre/post should be seen as indexed Boolean + * variables. The reason for this is pre and post cannot be given a consistent + * semantics. For example, consider term f( x_1, x_1 ) and enumerator variable + * e of the same type over which we are encoding a traversal. We have that + * pre_{x_1}( e.1 ) is false and pre_{x_1}( e.2 ) is true, although the model + * values for e.1 and e.2 are equal. Instead, pre_{x_1}( e.1 ) should be seen + * as a Boolean variable V_pre_{x_1,e.1} indexed by x_1 and e.1. and likewise + * for e.2. We convert all applications of pre/post to Boolean variables in + * the method eliminateTraversalPredicates below. Nevertheless, it is + * important that applications pre and post are encoded as APPLY_UF + * applications so that they behave as expected under substitutions. For + * example, pre_{x_1}( z.1 ) { z -> e.2 } results in pre_{x_1}( e.2.1 ), which + * after eliminateTraversalPredicates is V_pre_{x_1, e.2.1}. + */ + Node getTraversalPredicate(TypeNode tn, Node n, bool isPre); + /** eliminate traversal predicates + * + * This replaces all applications of traversal predicates P( x ) in n with + * unique Boolean variables, given by d_traversal_bool[ P( x ) ], and + * returns the result. + */ + Node eliminateTraversalPredicates(Node n); + //-----------------------------------end traversal predicates + /** a sygus sampler object for each (anchor, sygus type) pair + * + * This is used for the sygusRewVerify() option to verify the correctness of + * the rewriter. + */ + std::map> d_sampler; + /** Assert tester internal + * + * This function is called when the tester with index tindex is asserted for + * n, exp is the tester predicate. For example, for grammar: + * A -> A+A | x | 1 | 0 + * when is_+( d ) is asserted, + * assertTesterInternal(0, s( d ), is_+( s( d ) ),...) is called. This + * function may add lemmas to lemmas, which are sent out on the output + * channel of datatypes by the caller. + * + * These lemmas are of various forms, including: + * (1) dynamic symmetry breaking clauses for subterms of n (those added to + * lemmas on calls to addSymBreakLemmasFor, see function below), + * (2) static symmetry breaking clauses for subterms of n (those added to + * lemmas on getSimpleSymBreakPred, see function below), + * (3) conjecture-specific symmetry breaking lemmas, see + * SynthConjecture::getSymmetryBreakingPredicate, + * (4) fairness conflicts if sygusFair() is SYGUS_FAIR_DIRECT, e.g.: + * size( d ) <= 1 V ~is-C1( d ) V ~is-C2( d.1 ) + * where C1 and C2 are non-nullary constructors. + */ + void assertTesterInternal( int tindex, TNode n, Node exp, std::vector< Node >& lemmas ); + /** + * This function is called when term n is registered to the theory of + * datatypes. It makes the appropriate call to registerSearchTerm below, + * if applicable. + */ + void registerTerm(Node n, std::vector& lemmas); + + //------------------------dynamic symmetry breaking + /** Register search term + * + * This function is called when selector chain n of the form + * S_1( ... S_m( x ) ... ) is registered to the theory of datatypes, where + * tn is the type of n, d indicates the depth of n (the sum of weights of the + * selectors S_1...S_m), and topLevel is whether n is a top-level term + * (see d_is_top_level). We refer to n as a "search term". + * + * The purpose of this function is to notify this class that symmetry breaking + * lemmas should be instantiated for n. Any symmetry breaking lemmas that + * are active for n (see description of addSymBreakLemmasFor) are added to + * lemmas in this call. + */ + void registerSearchTerm( TypeNode tn, unsigned d, Node n, bool topLevel, std::vector< Node >& lemmas ); + /** Register search value + * + * This function is called when a selector chain n has been assigned a model + * value nv. This function calls itself recursively so that extensions of the + * selector chain n are registered with all the subterms of nv. For example, + * if we call this function with: + * n = x, nv = +( 1(), x() ) + * we make recursive calls with: + * n = x.1, nv = 1() and n = x.2, nv = x() + * + * a : the anchor of n, + * d : the depth of n. + * + * This function determines if the value nv is equivalent via rewriting to + * any previously registered search values for anchor a. If so, we construct + * a symmetry breaking lemma template and register it in d_cache[a]. For + * example, for grammar: + * A -> A+A | x | 1 | 0 + * Registering search value d -> x followed by d -> +( x, 0 ) results in the + * construction of the symmetry breaking lemma template: + * ~is_+( z ) V ~is_x( z.1 ) V ~is_0( z.2 ) + * which is stored in d_cache[a].d_sb_lemmas. This lemma is instantiated with + * z -> t for all terms t of appropriate depth, including d. + * This function strengthens blocking clauses using generalization techniques + * described in Reynolds et al SYNT 2017. + * + * The return value of this function is an abstraction of model assignment + * of nv to n, or null if we wish to exclude the model assignment nv to n. + * The return value of this method is different from nv itself, e.g. if it + * contains occurrences of the "any constant" constructor. For example, if + * nv is C_+( C_x(), C_{any_constant}( 5 ) ), then the return value of this + * function will either be null, or C_+( C_x(), C_{any_constant}( n.1.0 ) ), + * where n.1.0 is the appropriate selector chain applied to n. We build this + * abstraction since the semantics of C_{any_constant} is "any constant" and + * not "some constant". Thus, we should consider the subterm + * C_{any_constant}( 5 ) above to be an unconstrained variable (as represented + * by a selector chain), instead of the concrete value 5. + * + * The flag isVarAgnostic is whether "a" is a variable agnostic enumerator. If + * this is the case, we restrict symmetry breaking to subterms of n on its + * leftmost subchain. For example, consider the grammar: + * A -> B=B + * B -> B+B | x | y | 0 + * Say we are registering the search value x = y+x. Notice that this value is + * ordered. If a were a variable-agnostic enumerator of type A in this + * case, we would only register x = y+x and x, and not y+x or y, since the + * latter two terms are not leftmost subterms in this value. If we did on the + * other hand register y+x, we would be prevented from solutions like x+y = 0 + * later, since x+y is equivalent to (the already registered value) y+x. + * + * If doSym is false, we are not performing symmetry breaking on n. This flag + * is set to false on branches of n that are not leftmost. + */ + Node registerSearchValue(Node a, + Node n, + Node nv, + unsigned d, + std::vector& lemmas, + bool isVarAgnostic, + bool doSym); + /** Register symmetry breaking lemma + * + * This function adds the symmetry breaking lemma template lem for terms of + * type tn with anchor a. This is added to d_cache[a].d_sb_lemmas. Notice that + * we use lem as a template with free variable x, e.g. our template is: + * (lambda ((x tn)) lem) + * where x = getFreeVar( tn ). For all search terms t of the appropriate + * depth, + * we add the lemma lem{ x -> t } to lemmas. + * + * The argument sz indicates the size of terms that the lemma applies to, e.g. + * ~is_+( z ) has size 1 + * ~is_+( z ) V ~is_x( z.1 ) V ~is_0( z.2 ) has size 1 + * ~is_+( z ) V ~is_+( z.1 ) has size 2 + * This is equivalent to sum of weights of constructors corresponding to each + * tester, e.g. above + has weight 1, and x and 0 have weight 0. + */ + void registerSymBreakLemma( + TypeNode tn, Node lem, unsigned sz, Node a, std::vector& lemmas); + /** Register symmetry breaking lemma for value + * + * This function adds a symmetry breaking lemma template for selector chains + * with anchor a, that effectively states that val should never be a subterm + * of any value for a. + * + * et : an "invariance test" (see sygus/sygus_invariance.h) which states a + * criterion that val meets, which is the reason for its exclusion. This is + * used for generalizing the symmetry breaking lemma template. + * valr : if non-null, this states a value that should *not* be excluded by + * the symmetry breaking lemma template, which is a restriction to the above + * generalization. + * + * This function may add instances of the symmetry breaking template for + * existing search terms, which are added to lemmas. + */ + void registerSymBreakLemmaForValue(Node a, + Node val, + quantifiers::SygusInvarianceTest& et, + Node valr, + std::map& var_count, + std::vector& lemmas); + /** Add symmetry breaking lemmas for term + * + * Adds all active symmetry breaking lemmas for selector chain t to lemmas. A + * symmetry breaking lemma L is active for t based on three factors: + * (1) the current search size sz(a) for its anchor a, + * (2) the depth d of term t (see d_term_to_depth), + * (3) the size sz(L) of the symmetry breaking lemma L. + * In particular, L is active if sz(L) <= sz(a) - d. In other words, a + * symmetry breaking lemma is active if it is intended to block terms of + * size sz(L), and the maximum size that t can take in the current search, + * sz(a)-d, is greater than or equal to this value. + * + * tn : the type of term t, + * a : the anchor of term t, + * d : the depth of term t. + */ + void addSymBreakLemmasFor( + TypeNode tn, Node t, unsigned d, Node a, std::vector& lemmas); + /** calls the above function where a is the anchor t */ + void addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, std::vector< Node >& lemmas ); + //------------------------end dynamic symmetry breaking + + /** Get relevancy condition + * + * This returns (the negation of) a predicate that holds in the contexts in + * which the selector chain n is specified. For example, the negation of the + * relevancy condition for sel_{C2,1}( sel_{C1,1}( d ) ) is + * ~( is-C1( d ) ^ is-C2( sel_{C1,1}( d ) ) ) + * If shared selectors are enabled, this is a conjunction of disjunctions, + * since shared selectors may apply to multiple constructors. + */ + Node getRelevancyCondition( Node n ); + /** Cache of the above function */ + std::map d_rlv_cond; + + //------------------------static symmetry breaking + /** Get simple symmetry breakind predicate + * + * This function returns the "static" symmetry breaking lemma template for + * terms with type tn and constructor index tindex, for the given depth. This + * includes inferences about size with depth=0. Given grammar: + * A -> ite( B, A, A ) | A+A | x | 1 | 0 + * B -> A = A + * Examples of static symmetry breaking lemma templates are: + * for +, depth 0: size(z)=size(z.1)+size(z.2)+1 + * for +, depth 1: ~is-0( z.1 ) ^ ~is-0( z.2 ) ^ F + * where F ensures the constructor of z.1 is less than that of z.2 based + * on some ordering. + * for ite, depth 1: z.2 != z.3 + * These templates can be thought of as "hard-coded" cases of dynamic symmetry + * breaking lemma templates. Notice that the above lemma templates are in + * terms of getFreeVar( tn ), hence only one is created per + * (constructor, depth). A static symmetry break lemma template F[z] for + * constructor C are included in lemmas of the form: + * is-C( t ) => F[t] + * where t is a search term, see registerSearchTerm for definition of search + * term. + * + * usingSymCons: whether we are using symbolic constructors for subterms in + * the type tn, + * isVarAgnostic: whether the terms we are enumerating are agnostic to + * variables. + * + * The latter two options may affect the form of the predicate we construct. + */ + Node getSimpleSymBreakPred(Node e, + TypeNode tn, + int tindex, + unsigned depth, + bool usingSymCons, + bool isVarAgnostic); + /** Cache of the above function */ + std::map>>>> + d_simple_sb_pred; + /** + * For each search term, this stores the maximum depth for which we have added + * a static symmetry breaking lemma. + * + * This should be user context-dependent if sygus is updated to work in + * incremental mode. + */ + std::unordered_map d_simple_proc; + //------------------------end static symmetry breaking + + /** Get the canonical free variable for type tn */ + TNode getFreeVar( TypeNode tn ); + /** get term order predicate + * + * Assuming that n1 and n2 are children of a commutative operator, this + * returns a symmetry breaking predicate that can be instantiated for n1 and + * n2 while preserving satisfiability. By default, this is the predicate + * ( DT_SIZE n1 ) >= ( DT_SIZE n2 ) + */ + Node getTermOrderPredicate( Node n1, Node n2 ); + + private: + /** + * Map from registered variables to whether they are a sygus enumerator. + * + * This should be user context-dependent if sygus is updated to work in + * incremental mode. + */ + std::map d_register_st; + //----------------------search size information + /** + * Checks whether e is a sygus enumerator, that is, a term for which this + * class will track size for. + * + * We associate each sygus enumerator e with a "measure term", which is used + * for bounding the size of terms for the models of e. The measure term for a + * sygus enumerator may be e itself (if e has an active guard), or an + * arbitrary sygus variable otherwise. A measure term m is one for which our + * decision strategy decides on literals of the form (DT_SYGUS_BOUND m n). + * + * After determining the measure term m for e, if applicable, we initialize + * SygusSizeDecisionStrategy for m below. This may result in lemmas + */ + void registerSizeTerm(Node e, std::vector& lemmas); + /** A decision strategy for each measure term allocated by this class */ + class SygusSizeDecisionStrategy : public DecisionStrategyFmf + { + public: + SygusSizeDecisionStrategy(Node t, context::Context* c, Valuation valuation) + : DecisionStrategyFmf(c, valuation), d_this(t), d_curr_search_size(0) + { + } + /** the measure term */ + Node d_this; + /** + * For each size n, an explanation for why this measure term has size at + * most n. This is typically the literal (DT_SYGUS_BOUND m n), which + * we call the (n^th) "fairness literal" for m. + */ + std::map< unsigned, Node > d_search_size_exp; + /** + * For each size, whether we have called SygusExtension::notifySearchSize. + */ + std::map< unsigned, bool > d_search_size; + /** + * The current search size. This corresponds to the number of times + * incrementCurrentSearchSize has been called for this measure term. + */ + unsigned d_curr_search_size; + /** the list of all enumerators whose measure term is this */ + std::vector< Node > d_anchors; + /** get or make the measure value + * + * The measure value is an integer variable v that is a (symbolic) integer + * value that is constrained to be less than or equal to the current search + * size. For example, if we are using the fairness strategy + * SYGUS_FAIR_DT_SIZE (see options/datatype_options.h), then we constrain: + * (DT_SYGUS_BOUND m n) <=> (v <= n) + * for all asserted fairness literals. Then, if we are enforcing fairness + * based on the maximum size, we assert: + * (DT_SIZE e) <= v + * for all enumerators e. + */ + Node getOrMkMeasureValue(std::vector& lemmas); + /** get or make the active measure value + * + * The active measure value av is an integer variable that corresponds to + * the (symbolic) value of the sum of enumerators that are yet to be + * registered. This is to enforce the "sum of measures" strategy. For + * example, if we are using the fairness strategy SYGUS_FAIR_DT_SIZE, + * then initially av is equal to the measure value v, and the constraints + * (DT_SYGUS_BOUND m n) <=> (v <= n) + * are added as before. When an enumerator e is registered, we add the + * lemma: + * av = (DT_SIZE e) + av' + * and update the active measure value to av'. This ensures that the sum + * of sizes of active enumerators is at most n. + * + * If the flag mkNew is set to true, then we return a fresh variable and + * update the active measure value. + */ + Node getOrMkActiveMeasureValue(std::vector& lemmas, + bool mkNew = false); + /** Returns the s^th fairness literal for this measure term. */ + Node mkLiteral(unsigned s) override; + /** identify */ + std::string identify() const override + { + return std::string("sygus_enum_size"); + } + + private: + /** the measure value */ + Node d_measure_value; + /** the sygus measure value */ + Node d_measure_value_active; + }; + /** the above information for each registered measure term */ + std::map> d_szinfo; + /** map from enumerators (anchors) to their associated measure term */ + std::map< Node, Node > d_anchor_to_measure_term; + /** map from enumerators (anchors) to their active guard*/ + std::map< Node, Node > d_anchor_to_active_guard; + /** map from enumerators (anchors) to a decision stratregy for that guard */ + std::map> d_anchor_to_ag_strategy; + /** generic measure term + * + * This is a global term that is used as the measure term for all sygus + * enumerators that do not have active guards. This class enforces that + * all enumerators have size at most n, where n is the minimal integer + * such that (DT_SYGUS_BOUND d_generic_measure_term n) is asserted. + */ + Node d_generic_measure_term; + /** + * This increments the current search size for measure term m. This may + * cause lemmas to be added to lemmas based on the fact that symmetry + * breaking lemmas are now relevant for new search terms, see discussion + * of how search size affects which lemmas are relevant above + * addSymBreakLemmasFor. + */ + void incrementCurrentSearchSize( Node m, std::vector< Node >& lemmas ); + /** + * Notify this class that we are currently searching for terms of size at + * most s as model values for measure term m. Literal exp corresponds to the + * explanation of why the measure term has size at most n. This calls + * incrementSearchSize above, until the total number of times we have called + * incrementSearchSize so far is at least s. + */ + void notifySearchSize( Node m, unsigned s, Node exp, std::vector< Node >& lemmas ); + /** Allocates a SygusSizeDecisionStrategy object in d_szinfo. */ + void registerMeasureTerm( Node m ); + /** + * Return the current search size for arbitrary term n. This is the current + * search size of the anchor of n. + */ + unsigned getSearchSizeFor( Node n ); + /** return the current search size for enumerator (anchor) e */ + unsigned getSearchSizeForAnchor(Node e); + /** Get the current search size for measure term m in this SAT context. */ + unsigned getSearchSizeForMeasureTerm(Node m); + /** get current template + * + * For debugging. This returns a term that corresponds to the current + * inferred shape of n. For example, if the testers + * is-C1( n ) and is-C2( n.1 ) + * have been asserted where C1 and C2 are binary constructors, then this + * method may return a term of the form: + * C1( C2( x1, x2 ), x3 ) + * for fresh variables x1, x2, x3. The map var_count maintains the variable + * count for generating these fresh variables. + */ + Node getCurrentTemplate( Node n, std::map< TypeNode, int >& var_count ); + //----------------------end search size information + /** check value + * + * This is called when we have a model assignment vn for n, where n is + * a selector chain applied to an enumerator (a search term). This function + * ensures that testers have been asserted for each subterm of vn. This is + * critical for ensuring that the proper steps have been taken by this class + * regarding whether or not vn is a legal value for n (not greater than the + * current search size and not a value that can be blocked by symmetry + * breaking). + * + * For example, if vn = +( x(), x() ), then we ensure that the testers + * is-+( n ), is-x( n.1 ), is-x( n.2 ) + * have been asserted to this class. If a tester is not asserted for some + * relevant selector chain S( n ) of n, then we add a lemma L for that + * selector chain to lemmas, where L is the "splitting lemma" for S( n ), that + * states that the top symbol of S( n ) must be one of the constructors of + * its type. + * + * Notice that this function is a sanity check. Typically, it should be the + * case that testers are asserted for all subterms of vn, and hence this + * method should not ever add anything to lemmas. However, due to its + * importance, we check this regardless. + */ + bool checkValue(Node n, Node vn, int ind, std::vector& lemmas); + /** + * Get the current SAT status of the guard g. + * In particular, this returns 1 if g is asserted true, -1 if it is asserted + * false, and 0 if it is not asserted. + */ + int getGuardStatus( Node g ); +}; + +} +} +} + +#endif + diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 8a34d8056..2d6aeae60 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -59,7 +59,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, d_collectTermsCacheU(u), d_functionTerms(c), d_singleton_eq(u), - d_lemmas_produced_c(u) + d_lemmas_produced_c(u), + d_sygusExtension(nullptr) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); @@ -72,8 +73,6 @@ TheoryDatatypes::TheoryDatatypes(Context* c, d_true = NodeManager::currentNM()->mkConst( true ); d_zero = NodeManager::currentNM()->mkConst( Rational(0) ); d_dtfCounter = 0; - - d_sygus_sym_break = NULL; } TheoryDatatypes::~TheoryDatatypes() { @@ -83,7 +82,6 @@ TheoryDatatypes::~TheoryDatatypes() { Assert(current != NULL); delete current; } - delete d_sygus_sym_break; } void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) { @@ -142,9 +140,9 @@ void TheoryDatatypes::check(Effort e) { d_addedLemma = false; if( e == EFFORT_LAST_CALL ){ - Assert(d_sygus_sym_break); + Assert(d_sygusExtension != nullptr); std::vector< Node > lemmas; - d_sygus_sym_break->check( lemmas ); + d_sygusExtension->check(lemmas); doSendLemmas( lemmas ); return; } @@ -376,7 +374,7 @@ void TheoryDatatypes::check(Effort e) { } bool TheoryDatatypes::needsCheckLastEffort() { - return d_sygus_sym_break!=NULL; + return d_sygusExtension != nullptr; } void TheoryDatatypes::flushPendingFacts(){ @@ -483,9 +481,10 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){ } doPendingMerges(); // could be sygus-specific - if( d_sygus_sym_break ){ + if (d_sygusExtension) + { std::vector< Node > lemmas; - d_sygus_sym_break->assertFact( atom, polarity, lemmas ); + d_sygusExtension->assertFact(atom, polarity, lemmas); doSendLemmas( lemmas ); } //add to tester if applicable @@ -502,11 +501,12 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){ doPendingMerges(); Trace("dt-tester") << "Done pending merges." << std::endl; if( !d_conflict && polarity ){ - if( d_sygus_sym_break ){ + if (d_sygusExtension) + { Trace("dt-tester") << "Assert tester to sygus : " << atom << std::endl; //Assert( !d_sygus_util->d_conflict ); std::vector< Node > lemmas; - d_sygus_sym_break->assertTester( tindex, t_arg, atom, lemmas ); + d_sygusExtension->assertTester(tindex, t_arg, atom, lemmas); Trace("dt-tester") << "Done assert tester to sygus." << std::endl; doSendLemmas( lemmas ); } @@ -532,9 +532,10 @@ void TheoryDatatypes::preRegisterTerm(TNode n) { default: // Function applications/predicates d_equalityEngine.addTerm(n); - if( d_sygus_sym_break ){ + if (d_sygusExtension) + { std::vector< Node > lemmas; - d_sygus_sym_break->preRegisterTerm(n, lemmas); + d_sygusExtension->preRegisterTerm(n, lemmas); doSendLemmas( lemmas ); } //d_equalityEngine.addTriggerTerm(n, THEORY_DATATYPES); @@ -545,8 +546,8 @@ void TheoryDatatypes::preRegisterTerm(TNode n) { void TheoryDatatypes::finishInit() { if( getQuantifiersEngine() && options::ceGuidedInst() ){ - d_sygus_sym_break = - new SygusSymBreakNew(this, getQuantifiersEngine(), getSatContext()); + d_sygusExtension.reset( + new SygusExtension(this, getQuantifiersEngine(), getSatContext())); // do congruence on evaluation functions d_equalityEngine.addFunctionKind(kind::DT_SYGUS_EVAL); } diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index e14a78df2..ba09ce89e 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -26,7 +26,7 @@ #include "expr/attribute.h" #include "expr/datatype.h" #include "expr/node_trie.h" -#include "theory/datatypes/datatypes_sygus.h" +#include "theory/datatypes/sygus_extension.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" #include "util/hash.h" @@ -370,7 +370,7 @@ private: TNode getRepresentative( TNode a ); private: /** sygus symmetry breaking utility */ - SygusSymBreakNew* d_sygus_sym_break; + std::unique_ptr d_sygusExtension; };/* class TheoryDatatypes */ -- cgit v1.2.3