From 74c1ad7e4a8e93316b7555ac8a1b88ee777335e2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 28 May 2018 10:35:17 -0500 Subject: [PATCH] Builtin evaluation functions for sygus (#1991) --- src/expr/datatype.cpp | 9 + src/expr/datatype.h | 7 + src/options/datatypes_options.toml | 9 + src/theory/datatypes/datatypes_rewriter.cpp | 199 ++++++++++- src/theory/datatypes/datatypes_rewriter.h | 38 +++ src/theory/datatypes/datatypes_sygus.cpp | 137 ++++++-- src/theory/datatypes/datatypes_sygus.h | 17 +- src/theory/datatypes/kinds | 3 + src/theory/datatypes/theory_datatypes.cpp | 22 +- .../datatypes/theory_datatypes_type_rules.h | 46 +++ src/theory/datatypes/type_enumerator.cpp | 2 +- .../sygus/ce_guided_conjecture.cpp | 85 +++-- .../quantifiers/sygus/ce_guided_conjecture.h | 15 +- .../sygus/ce_guided_single_inv_sol.cpp | 18 +- .../quantifiers/sygus/sygus_eval_unfold.cpp | 51 ++- .../quantifiers/sygus/sygus_explain.cpp | 27 +- .../quantifiers/sygus/sygus_grammar_cons.cpp | 23 +- .../quantifiers/sygus/sygus_grammar_norm.cpp | 8 +- .../quantifiers/sygus/sygus_grammar_norm.h | 6 - src/theory/quantifiers/sygus/sygus_pbe.cpp | 77 +++-- .../quantifiers/sygus/sygus_process_conj.cpp | 1 + .../quantifiers/sygus/sygus_repair_const.cpp | 27 +- .../quantifiers/sygus/sygus_unif_rl.cpp | 31 +- .../quantifiers/sygus/sygus_unif_strat.cpp | 15 +- .../quantifiers/sygus/term_database_sygus.cpp | 317 +++++++++--------- .../quantifiers/sygus/term_database_sygus.h | 42 ++- src/theory/quantifiers/sygus_sampler.cpp | 20 +- src/theory/quantifiers/term_util.h | 4 - 28 files changed, 837 insertions(+), 419 deletions(-) diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index d697a6aaf..f19955d19 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -77,6 +77,11 @@ size_t Datatype::indexOf(Expr item) { item.getType().isSelector(), item, "arg must be a datatype constructor, selector, or tester"); + return indexOfInternal(item); +} + +size_t Datatype::indexOfInternal(Expr item) +{ TNode n = Node::fromExpr(item); if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){ return indexOf( item[0] ); @@ -91,6 +96,10 @@ size_t Datatype::cindexOf(Expr item) { PrettyCheckArgument(item.getType().isSelector(), item, "arg must be a datatype selector"); + return cindexOfInternal(item); +} +size_t Datatype::cindexOfInternal(Expr item) +{ TNode n = Node::fromExpr(item); if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){ return cindexOf( item[0] ); diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 826711897..990548979 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -615,6 +615,13 @@ public: */ static size_t cindexOf(Expr item) CVC4_PUBLIC; + /** + * Same as above, but without checks. These methods should be used by + * internal (Node-level) code. + */ + static size_t indexOfInternal(Expr item); + static size_t cindexOfInternal(Expr item); + /** The type for iterators over constructors. */ typedef DatatypeConstructorIterator iterator; /** The (const) type for iterators over constructors. */ diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index 8d6f0baf3..b74244fe1 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -175,3 +175,12 @@ header = "options/datatypes_options.h" default = "-1" read_only = true help = "tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)" + +[[option]] + name = "sygusEvalBuiltin" + category = "regular" + long = "sygus-eval-builtin" + type = "bool" + default = "true" + read_only = true + help = "use builtin kind for evaluation functions in sygus" diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index cc8edadd0..90f0494d8 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -16,6 +16,9 @@ #include "theory/datatypes/datatypes_rewriter.h" +using namespace CVC4; +using namespace CVC4::kind; + namespace CVC4 { namespace theory { namespace datatypes { @@ -50,7 +53,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) } } TNode constructor = in[0].getOperator(); - size_t constructorIndex = Datatype::indexOf(constructor.toExpr()); + size_t constructorIndex = indexOf(constructor); const Datatype& dt = Datatype::datatypeOf(constructor.toExpr()); const DatatypeConstructor& c = dt[constructorIndex]; unsigned weight = c.getWeight(); @@ -105,6 +108,51 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) return RewriteResponse(REWRITE_AGAIN_FULL, res); } } + else if (k == DT_SYGUS_EVAL) + { + // sygus evaluation function + Node ev = in[0]; + if (ev.getKind() == APPLY_CONSTRUCTOR) + { + Trace("dt-sygus-util") << "Rewrite " << in << " by unfolding...\n"; + const Datatype& dt = + static_cast(ev.getType().toType()).getDatatype(); + unsigned i = indexOf(ev.getOperator()); + Node op = Node::fromExpr(dt[i].getSygusOp()); + // if it is the "any constant" constructor, return its argument + if (op.getAttribute(SygusAnyConstAttribute())) + { + Assert(ev.getNumChildren() == 1); + Assert(ev[0].getType().isComparableTo(in.getType())); + return RewriteResponse(REWRITE_AGAIN_FULL, ev[0]); + } + std::vector args; + for (unsigned j = 1, nchild = in.getNumChildren(); j < nchild; j++) + { + args.push_back(in[j]); + } + Assert(!dt.isParametric()); + std::vector children; + for (const Node& evc : ev) + { + std::vector cc; + cc.push_back(evc); + cc.insert(cc.end(), args.begin(), args.end()); + children.push_back(nm->mkNode(DT_SYGUS_EVAL, cc)); + } + Node ret = mkSygusTerm(dt, i, children); + // if it is a variable, apply the substitution + if (ret.getKind() == BOUND_VARIABLE) + { + Assert(ret.hasAttribute(SygusVarNumAttribute())); + int vn = ret.getAttribute(SygusVarNumAttribute()); + Assert(Node::fromExpr(dt.getSygusVarList())[vn] == ret); + ret = args[vn]; + } + Trace("dt-sygus-util") << "...got " << ret << "\n"; + return RewriteResponse(REWRITE_AGAIN_FULL, ret); + } + } if (k == kind::EQUAL) { @@ -138,6 +186,119 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) return RewriteResponse(REWRITE_DONE, in); } +Kind getOperatorKindForSygusBuiltin(Node op) +{ + Assert(op.getKind() != BUILTIN); + if (op.getKind() == LAMBDA) + { + // we use APPLY_UF instead of APPLY, since the rewriter for APPLY_UF + // does beta-reduction but does not for APPLY + return APPLY_UF; + } + TypeNode tn = op.getType(); + if (tn.isConstructor()) + { + return APPLY_CONSTRUCTOR; + } + else if (tn.isSelector()) + { + return APPLY_SELECTOR; + } + else if (tn.isTester()) + { + return APPLY_TESTER; + } + else if (tn.isFunction()) + { + return APPLY_UF; + } + return NodeManager::operatorToKind(op); +} + +Node DatatypesRewriter::mkSygusTerm(const Datatype& dt, + unsigned i, + const std::vector& children) +{ + Trace("dt-sygus-util") << "Make sygus term " << dt.getName() << "[" << i + << "] with children: " << children << std::endl; + Assert(i < dt.getNumConstructors()); + Assert(dt.isSygus()); + Assert(!dt[i].getSygusOp().isNull()); + std::vector schildren; + Node op = Node::fromExpr(dt[i].getSygusOp()); + // if it is the any constant, we simply return the child + if (op.getAttribute(SygusAnyConstAttribute())) + { + Assert(children.size() == 1); + return children[0]; + } + if (op.getKind() != BUILTIN) + { + schildren.push_back(op); + } + schildren.insert(schildren.end(), children.begin(), children.end()); + Node ret; + if (op.getKind() == BUILTIN) + { + ret = NodeManager::currentNM()->mkNode(op, schildren); + Trace("dt-sygus-util") << "...return (builtin) " << ret << std::endl; + return ret; + } + Kind ok = getOperatorKindForSygusBuiltin(op); + if (schildren.size() == 1 && ok == kind::UNDEFINED_KIND) + { + ret = schildren[0]; + } + else + { + ret = NodeManager::currentNM()->mkNode(ok, schildren); + } + Trace("dt-sygus-util") << "...return " << ret << std::endl; + return ret; +} +Node DatatypesRewriter::mkSygusEvalApp(const std::vector& children) +{ + if (options::sygusEvalBuiltin()) + { + return NodeManager::currentNM()->mkNode(DT_SYGUS_EVAL, children); + } + // otherwise, using APPLY_UF + Assert(!children.empty()); + Assert(children[0].getType().isDatatype()); + const Datatype& dt = + static_cast(children[0].getType().toType()).getDatatype(); + Assert(dt.isSygus()); + std::vector schildren; + schildren.push_back(Node::fromExpr(dt.getSygusEvaluationFunc())); + schildren.insert(schildren.end(), children.begin(), children.end()); + return NodeManager::currentNM()->mkNode(APPLY_UF, schildren); +} + +bool DatatypesRewriter::isSygusEvalApp(Node n) +{ + if (options::sygusEvalBuiltin()) + { + return n.getKind() == DT_SYGUS_EVAL; + } + // otherwise, using APPLY_UF + if (n.getKind() != APPLY_UF || n.getNumChildren() == 0) + { + return false; + } + TypeNode tn = n[0].getType(); + if (!tn.isDatatype()) + { + return false; + } + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + if (!dt.isSygus()) + { + return false; + } + Node eval_op = Node::fromExpr(dt.getSygusEvaluationFunc()); + return eval_op == n.getOperator(); +} + RewriteResponse DatatypesRewriter::preRewrite(TNode in) { Trace("datatypes-rewrite-debug") << "pre-rewriting " << in << std::endl; @@ -162,7 +323,7 @@ RewriteResponse DatatypesRewriter::preRewrite(TNode in) Node op = in.getOperator(); // get the constructor object const DatatypeConstructor& dtc = - Datatype::datatypeOf(op.toExpr())[Datatype::indexOf(op.toExpr())]; + Datatype::datatypeOf(op.toExpr())[indexOf(op)]; // create ascribed constructor type Node tc = NodeManager::currentNM()->mkConst( AscriptionType(dtc.getSpecializedConstructorType(t))); @@ -214,7 +375,7 @@ RewriteResponse DatatypesRewriter::rewriteSelector(TNode in) TypeNode argType = in[0].getType(); TNode selector = in.getOperator(); TNode constructor = in[0].getOperator(); - size_t constructorIndex = Datatype::indexOf(constructor.toExpr()); + size_t constructorIndex = indexOf(constructor); const Datatype& dt = Datatype::datatypeOf(selector.toExpr()); const DatatypeConstructor& c = dt[constructorIndex]; Trace("datatypes-rewrite-debug") << "Rewriting collapsable selector : " @@ -294,8 +455,7 @@ RewriteResponse DatatypesRewriter::rewriteTester(TNode in) { if (in[0].getKind() == kind::APPLY_CONSTRUCTOR) { - bool result = Datatype::indexOf(in.getOperator().toExpr()) - == Datatype::indexOf(in[0].getOperator().toExpr()); + bool result = indexOf(in.getOperator()) == indexOf(in[0].getOperator()); Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " << "Rewrite trivial tester " << in << " " << result << std::endl; @@ -313,11 +473,10 @@ RewriteResponse DatatypesRewriter::rewriteTester(TNode in) return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); } - // could try dt.getNumConstructors()==2 && - // Datatype::indexOf(in.getOperator())==1 ? + // could try dt.getNumConstructors()==2 && indexOf(in.getOperator())==1 ? else if (!options::dtUseTesters()) { - unsigned tindex = Datatype::indexOf(in.getOperator().toExpr()); + unsigned tindex = indexOf(in.getOperator()); Trace("datatypes-rewrite-debug") << "Convert " << in << " to equality " << in[0] << " " << tindex << std::endl; Node neq = mkTester(in[0], tindex, dt); @@ -416,7 +575,7 @@ int DatatypesRewriter::isInstCons(Node t, Node n, const Datatype& dt) { if (n.getKind() == kind::APPLY_CONSTRUCTOR) { - int index = Datatype::indexOf(n.getOperator().toExpr()); + int index = indexOf(n.getOperator()); const DatatypeConstructor& c = dt[index]; Type nt = n.getType().toType(); for (unsigned i = 0, size = n.getNumChildren(); i < size; i++) @@ -440,7 +599,7 @@ int DatatypesRewriter::isTester(Node n, Node& a) if (n.getKind() == kind::APPLY_TESTER) { a = n[0]; - return Datatype::indexOf(n.getOperator().toExpr()); + return indexOf(n.getOperator()); } } else @@ -472,7 +631,7 @@ int DatatypesRewriter::isTester(Node n) { if (n.getKind() == kind::APPLY_TESTER) { - return Datatype::indexOf(n.getOperator().toExpr()); + return indexOf(n.getOperator().toExpr()); } } else @@ -497,6 +656,24 @@ int DatatypesRewriter::isTester(Node n) return -1; } +struct DtIndexAttributeId +{ +}; +typedef expr::Attribute DtIndexAttribute; + +unsigned DatatypesRewriter::indexOf(Node n) +{ + if (!n.hasAttribute(DtIndexAttribute())) + { + Assert(n.getType().isConstructor() || n.getType().isTester() + || n.getType().isSelector()); + unsigned index = Datatype::indexOfInternal(n.toExpr()); + n.setAttribute(DtIndexAttribute(), index); + return index; + } + return n.getAttribute(DtIndexAttribute()); +} + Node DatatypesRewriter::mkTester(Node n, int i, const Datatype& dt) { if (options::dtUseTesters()) diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 8d9ddbf50..ed504e6bf 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -26,6 +26,19 @@ namespace CVC4 { namespace theory { + +/** sygus var num */ +struct SygusVarNumAttributeId +{ +}; +typedef expr::Attribute SygusVarNumAttribute; + +/** Attribute true for variables that represent any constant */ +struct SygusAnyConstAttributeId +{ +}; +typedef expr::Attribute SygusAnyConstAttribute; + namespace datatypes { class DatatypesRewriter { @@ -59,6 +72,12 @@ public: static int isTester(Node n, Node& a); /** is tester, same as above but does not update an argument */ static int isTester(Node n); + /** + * Get the index of a constructor or tester in its datatype, or the + * index of a selector in its constructor. (Zero is always the + * first index.) + */ + static unsigned indexOf(Node n); /** make tester is-C( n ), where C is the i^{th} constructor of dt */ static Node mkTester(Node n, int i, const Datatype& dt); /** make tester split @@ -102,6 +121,25 @@ public: * C( x, y ) and z */ static bool checkClash(Node n1, Node n2, std::vector& rew); + /** make sygus term + * + * This function returns a builtin term f( children[0], ..., children[n] ) + * where f is the builtin op that the i^th constructor of sygus datatype dt + * encodes. + */ + static Node mkSygusTerm(const Datatype& dt, + unsigned i, + const std::vector& children); + /** make sygus evaluation function application */ + static Node mkSygusEvalApp(const std::vector& children); + /** is sygus evaluation function */ + static bool isSygusEvalApp(Node n); + /** + * Get the builtin sygus operator for constructor term n of sygus datatype + * type. For example, if n is the term C_+( d1, d2 ) where C_+ is a sygus + * constructor whose sygus op is the builtin operator +, this method returns +. + */ + static Node getSygusOpForCTerm(Node n); private: /** rewrite constructor term in */ diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 328ef03d4..7773e7c5f 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -214,12 +214,22 @@ bool SygusSymBreakNew::computeTopLevel( TypeNode tn, Node n ){ } void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std::vector< Node >& lemmas ) { - d_active_terms.insert( n ); - Trace("sygus-sb-debug2") << "Sygus : activate term : " << n << " : " << exp << std::endl; - TypeNode ntn = n.getType(); - const Datatype& dt = ((DatatypeType)ntn.toType()).getDatatype(); - + 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]; @@ -280,6 +290,7 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std: 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]; if( min_depth<=max_depth ){ @@ -289,12 +300,15 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std: for (unsigned ds = 0; ds <= max_depth; ds++) { // static conjecture-independent symmetry breaking + Trace("sygus-sb-debug") << " simple symmetry breaking...\n"; Node ipred = getSimpleSymBreakPred(ntn, tindex, ds, usingSymCons); if (!ipred.isNull()) { sb_lemmas.push_back(ipred); } // 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()) @@ -326,6 +340,7 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std: // 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; @@ -336,6 +351,7 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std: assertTesterInternal( (*itt).second, sel, d_testers_exp[sel], lemmas ); } } + Trace("sygus-sb-debug") << "...finished" << std::endl; } } @@ -397,15 +413,32 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn, { 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; + + // if we are the "any constant" constructor, we do no symmetry breaking + // only do simple symmetry breaking up to depth 2 + Node sop = Node::fromExpr(dt[tindex].getSygusOp()); + if (sop.getAttribute(SygusAnyConstAttribute()) || depth > 2) + { + d_simple_sb_pred[tn][tindex][usingSymCons][depth] = Node::null(); + return Node::null(); + } // conjunctive conclusion of lemma std::vector sbp_conj; if (depth == 0) { + Trace("sygus-sb-simple-debug") << " Size..." << std::endl; // fairness if (options::sygusFair() == SYGUS_FAIR_DT_SIZE) { @@ -419,10 +452,11 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn, // symmetry breaking Kind nk = d_tds->getConsNumKind(tn, tindex); - // only do simple symmetry breaking up to depth 2 - if (options::sygusSymBreak() && depth < 2) + if (options::sygusSymBreak()) { + // the number of (sygus) arguments unsigned dt_index_nargs = dt[tindex].getNumArgs(); + // builtin type TypeNode tnb = TypeNode::fromType(dt.getSygusType()); // get children @@ -439,6 +473,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn, // 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++) { @@ -458,6 +493,8 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn, { if (nk != UNDEFINED_KIND) { + Trace("sygus-sb-simple-debug") + << " Equality reasoning about children..." << std::endl; // commutative operators if (quantifiers::TermUtil::isComm(nk)) { @@ -541,9 +578,9 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn, { const Datatype& cdt = static_cast(tnc.toType()).getDatatype(); - Node guard_val = nm->mkNode( - APPLY_CONSTRUCTOR, - Node::fromExpr(cdt[anyc_cons_num_c].getConstructor())); + Node fv = d_tds->getFreeVar(tnc, 0); + Node guard_val = datatypes::DatatypesRewriter::getInstCons( + fv, cdt, anyc_cons_num_c); Node exp = d_tds->getExplain()->getExplanationForEquality( children[c1], guard_val); sym_lem_deq = nm->mkNode(OR, exp, sym_lem_deq); @@ -552,8 +589,8 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn, } } - Trace("sygus-sb-simple-debug") << "Process arguments for " << tn - << " : " << nk << " : " << std::endl; + 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 @@ -716,19 +753,50 @@ void SygusSymBreakNew::registerSearchTerm( TypeNode tn, unsigned d, Node n, bool } } -bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d, std::vector< Node >& lemmas ) { - Assert( n.getType()==nv.getType() ); - Assert( nv.getKind()==APPLY_CONSTRUCTOR ); - TypeNode tn = n.getType(); - // currently bottom-up, could be top-down? +Node SygusSymBreakNew::registerSearchValue( + Node a, Node n, Node nv, unsigned d, std::vector& lemmas) +{ + 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 ){ - const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); - unsigned cindex = Datatype::indexOf( nv.getOperator().toExpr() ); - for( unsigned i=0; imkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex].getSelectorInternal( tn.toType(), i ) ), n ); - if( !registerSearchValue( a, sel, nv[i], d+1, lemmas ) ){ - return false; + unsigned cindex = DatatypesRewriter::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); + 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); } } Trace("sygus-sb-debug2") << "Registering search value " << n << " -> " << nv << std::endl; @@ -750,7 +818,7 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d, quantifiers::DivByZeroSygusInvarianceTest dbzet; Trace("sygus-sb-mexp-debug") << "Minimize explanation for div-by-zero in " << d_tds->sygusToBuiltin( nv ) << std::endl; registerSymBreakLemmaForValue(a, nv, dbzet, Node::null(), lemmas); - return false; + return Node::null(); }else{ std::unordered_map::iterator itsv = d_cache[a].d_search_val[tn].find(bvr); @@ -885,11 +953,11 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d, 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, lemmas); - return false; + return Node::null(); } } } - return true; + return nv; } void SygusSymBreakNew::registerSymBreakLemmaForValue( @@ -1179,6 +1247,9 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { for( std::map< Node, bool >::iterator it = d_register_st.begin(); it != d_register_st.end(); ++it ){ if( it->second ){ Node prog = it->first; + 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")) { @@ -1214,7 +1285,9 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { // register the search value ( prog -> progv ), this may invoke symmetry breaking if( options::sygusSymBreakDynamic() ){ - if( !registerSearchValue( prog, prog, progv, 0, lemmas ) ){ + Node rsv = registerSearchValue(prog, prog, progv, 0, lemmas); + if (rsv.isNull()) + { Trace("sygus-sb") << " SygusSymBreakNew::check: ...added new symmetry breaking lemma for " << prog << "." << std::endl; } else @@ -1226,6 +1299,7 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { } } //register any measured terms that we haven't encountered yet (should only be invoked on first call to check + Trace("sygus-sb") << "Register size terms..." << std::endl; std::vector< Node > mts; d_tds->getEnumerators(mts); for( unsigned i=0; i& lemmas) { - Assert( vn.getKind()==kind::APPLY_CONSTRUCTOR ); + if (vn.getKind() != kind::APPLY_CONSTRUCTOR) + { + // all datatype terms should be constant here + Assert(!vn.getType().isDatatype()); + return true; + } if( Trace.isOn("sygus-sb-warn") ){ Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, n ); Node prog_szv = d_td->getValuation().getModel()->getValue( prog_sz ); @@ -1262,7 +1341,7 @@ bool SygusSymBreakNew::checkTesters(Node n, } TypeNode tn = n.getType(); const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); - int cindex = Datatype::indexOf( vn.getOperator().toExpr() ); + int cindex = DatatypesRewriter::indexOf(vn.getOperator()); Node tst = DatatypesRewriter::mkTester( n, cindex, dt ); bool hastst = d_td->getValuation().getModel()->hasTerm( tst ); Node tstrep = d_td->getValuation().getModel()->getRepresentative( tst ); diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index eaed2a866..d08150a15 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -283,8 +283,21 @@ private: * 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. - */ - bool registerSearchValue( Node a, Node n, Node nv, unsigned d, std::vector< Node >& lemmas ); + * + * 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. + */ + Node registerSearchValue( + Node a, Node n, Node nv, unsigned d, std::vector& lemmas); /** Register symmetry breaking lemma * * This function adds the symmetry breaking lemma template lem for terms of diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 65f258de1..9c7365ac1 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -114,4 +114,7 @@ typerule DT_SIZE_BOUND ::CVC4::theory::datatypes::DtBoundTypeRule operator DT_SYGUS_BOUND 2 "datatypes sygus bound" typerule DT_SYGUS_BOUND ::CVC4::theory::datatypes::DtSygusBoundTypeRule +operator DT_SYGUS_EVAL 1: "datatypes sygus evaluation function" +typerule DT_SYGUS_EVAL ::CVC4::theory::datatypes::DtSyguEvalTypeRule + endtheory diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 18fadd052..4c79a31e9 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -65,8 +65,6 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL); //d_equalityEngine.addFunctionKind(kind::DT_SIZE); //d_equalityEngine.addFunctionKind(kind::DT_HEIGHT_BOUND); - //d_equalityEngine.addFunctionKind(kind::DT_SYGUS_TERM_ORDER); - //d_equalityEngine.addFunctionKind(kind::DT_SYGUS_IS_CONST); d_equalityEngine.addFunctionKind(kind::APPLY_TESTER); //d_equalityEngine.addFunctionKind(kind::APPLY_UF); @@ -530,6 +528,8 @@ void TheoryDatatypes::finishInit() { quantifiers::TermDbSygus * tds = getQuantifiersEngine()->getTermDatabaseSygus(); Assert( tds!=NULL ); d_sygus_sym_break = new SygusSymBreakNew( this, tds, getSatContext() ); + // do congruence on evaluation functions + d_equalityEngine.addFunctionKind(kind::DT_SYGUS_EVAL); } } @@ -546,7 +546,7 @@ Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { Node selector_use; TypeNode ndt = n[0].getType(); if( options::dtSharedSelectors() ){ - size_t selectorIndex = Datatype::indexOf(selectorExpr); + size_t selectorIndex = DatatypesRewriter::indexOf(selector); Trace("dt-expand") << "...selector index = " << selectorIndex << std::endl; Assert( selectorIndexd_constructor.get().isNull() ){ - return Datatype::indexOf( eqc->d_constructor.get().getOperator().toExpr() ); + return DatatypesRewriter::indexOf(eqc->d_constructor.get().getOperator()); }else{ Node lbl = getLabel( n ); if( lbl.isNull() ){ @@ -970,7 +970,6 @@ int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){ int tindex = DatatypesRewriter::isTester( lbl ); Assert( tindex!=-1 ); return tindex; - //return Datatype::indexOf( getLabel( n ).getOperator().toExpr() ); } } } @@ -998,7 +997,6 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool > for( int i=0; imkNode( kind::APPLY_UF, d_exp_def_skolem[s.getOperator().toExpr()], s[0] ); - //}else{ r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c ); if( options::dtRefIntro() ){ use_s = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), use_s ); @@ -2267,7 +2260,8 @@ std::pair TheoryDatatypes::entailmentCheck(TNode lit, const Entailme Node r = d_equalityEngine.getRepresentative( n ); EqcInfo * ei = getOrMakeEqcInfo( r, false ); int l_index = getLabelIndex( ei, r ); - int t_index = (int)Datatype::indexOf( atom.getOperator().toExpr() ); + int t_index = + static_cast(DatatypesRewriter::indexOf(atom.getOperator())); Trace("dt-entail") << " Tester indices are " << t_index << " and " << l_index << std::endl; if( l_index!=-1 && (l_index==t_index)==pol ){ std::vector< TNode > exp_c; diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 6ba64d8dd..94a99d46e 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -359,6 +359,52 @@ class DtSygusBoundTypeRule { } }; /* class DtSygusBoundTypeRule */ +class DtSyguEvalTypeRule +{ + public: + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) + { + TypeNode headType = n[0].getType(check); + if (!headType.isDatatype()) + { + throw TypeCheckingExceptionPrivate( + n, "datatype sygus eval takes a datatype head"); + } + const Datatype& dt = + static_cast(headType.toType()).getDatatype(); + if (!dt.isSygus()) + { + throw TypeCheckingExceptionPrivate( + n, "datatype sygus eval must have a datatype head that is sygus"); + } + if (check) + { + Node svl = Node::fromExpr(dt.getSygusVarList()); + if (svl.getNumChildren() + 1 != n.getNumChildren()) + { + throw TypeCheckingExceptionPrivate(n, + "wrong number of arguments to a " + "datatype sygus evaluation " + "function"); + } + for (unsigned i = 0, nvars = svl.getNumChildren(); i < nvars; i++) + { + TypeNode vtype = svl[i].getType(check); + TypeNode atype = n[i + 1].getType(check); + if (!vtype.isComparableTo(atype)) + { + throw TypeCheckingExceptionPrivate( + n, + "argument type mismatch in a datatype sygus evaluation function"); + } + } + } + return TypeNode::fromType(dt.getSygusType()); + } +}; /* class DtSygusBoundTypeRule */ + } /* CVC4::theory::datatypes namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index ee03b7815..a3d205a12 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -188,7 +188,7 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ Debug("dt-enum-debug") << "done : " << t << std::endl; Assert( t.getKind()==kind::APPLY_CONSTRUCTOR ); // start with the constructor for which a ground term is constructed - d_zeroCtor = Datatype::indexOf( t.getOperator().toExpr() ); + d_zeroCtor = datatypes::DatatypesRewriter::indexOf(t.getOperator()); d_has_debruijn = 0; } Debug("dt-enum") << "zero ctor : " << d_zeroCtor << std::endl; diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index ecb6db2fb..0f3dd74ae 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -23,7 +23,6 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/sygus/ce_guided_instantiation.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -46,6 +45,7 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe) d_ceg_cegis(new Cegis(qe, this)), d_ceg_cegisUnif(new CegisUnif(qe, this)), d_master(nullptr), + d_set_ce_sk_vars(false), d_repair_index(0), d_refine_count(0), d_syntax_guided(false) @@ -239,10 +239,7 @@ void CegConjecture::doBasicCheck(std::vector< Node >& lems) { } } -bool CegConjecture::needsRefinement() { - return !d_ce_sk.empty(); -} - +bool CegConjecture::needsRefinement() const { return d_set_ce_sk_vars; } void CegConjecture::doCheck(std::vector& lems) { Assert(d_master != nullptr); @@ -278,7 +275,7 @@ void CegConjecture::doCheck(std::vector& lems) } d_repair_index++; if (d_sygus_rconst->repairSolution( - d_candidates, fail_cvs, candidate_values)) + d_candidates, fail_cvs, candidate_values, true)) { constructed_cand = true; } @@ -332,7 +329,7 @@ void CegConjecture::doCheck(std::vector& lems) recordInstantiation(candidate_values); return; } - Assert( d_ce_sk.empty() ); + Assert(!d_set_ce_sk_vars); }else{ if( !constructed_cand ){ return; @@ -340,33 +337,40 @@ void CegConjecture::doCheck(std::vector& lems) } //immediately skolemize inner existentials - Node instr = Rewriter::rewrite(inst); + d_set_ce_sk_vars = sk_refine; Node lem; - if (instr.getKind() == NOT && instr[0].getKind() == FORALL) + if (inst.getKind() == NOT && inst[0].getKind() == FORALL) { + // introduce the skolem variables + std::vector sks; if (constructed_cand) { - lem = d_qe->getSkolemize()->getSkolemizedBody(instr[0]).negate(); + std::vector vars; + for (const Node& v : inst[0][0]) + { + Node sk = nm->mkSkolem("rsk", v.getType()); + sks.push_back(sk); + vars.push_back(v); + } + lem = inst[0][1].substitute( + vars.begin(), vars.end(), sks.begin(), sks.end()); + lem = lem.negate(); } if (sk_refine) { - Assert(!isGround()); - d_ce_sk.push_back(instr[0]); + d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end()); } + Assert(!isGround()); } else { if (constructed_cand) { // use the instance itself - lem = instr; - } - if (sk_refine) - { - // we add null so that one test of the conjecture for the empty - // substitution is checked - d_ce_sk.push_back(Node::null()); + lem = inst; } + // we add null so that one test of the conjecture for the empty + // substitution is checked } if (!lem.isNull()) { @@ -399,21 +403,19 @@ void CegConjecture::doCheck(std::vector& lems) void CegConjecture::doRefine( std::vector< Node >& lems ){ Assert( lems.empty() ); - Assert( d_ce_sk.size()==1 ); + Assert(d_set_ce_sk_vars); //first, make skolem substitution Trace("cegqi-refine") << "doRefine : construct skolem substitution..." << std::endl; std::vector< Node > sk_vars; std::vector< Node > sk_subs; //collect the substitution over all disjuncts - Node ce_q = d_ce_sk[0]; - if (!ce_q.isNull()) + if (!d_ce_sk_vars.empty()) { - std::vector skolems; - d_qe->getSkolemize()->getSkolemConstants(ce_q, skolems); - Assert(d_inner_vars.size() == skolems.size()); + Trace("cegqi-refine") << "Get model values for skolems..." << std::endl; + Assert(d_inner_vars.size() == d_ce_sk_vars.size()); std::vector model_values; - getModelValues(skolems, model_values); + getModelValues(d_ce_sk_vars, model_values); sk_vars.insert(sk_vars.end(), d_inner_vars.begin(), d_inner_vars.end()); sk_subs.insert(sk_subs.end(), model_values.begin(), model_values.end()); } @@ -425,12 +427,10 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){ std::vector< Node > lem_c; Trace("cegqi-refine") << "doRefine : Construct refinement lemma..." << std::endl; Trace("cegqi-refine-debug") - << " For counterexample point : " << ce_q << std::endl; + << " For counterexample skolems : " << d_ce_sk_vars << std::endl; Node base_lem; - if (!ce_q.isNull()) + if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL) { - Assert(d_base_inst.getKind() == kind::NOT - && d_base_inst[0].getKind() == kind::FORALL); base_lem = d_base_inst[0][1]; } else @@ -440,13 +440,16 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){ Assert( sk_vars.size()==sk_subs.size() ); - Trace("cegqi-refine") << "doRefine : construct and finalize lemmas..." << std::endl; - + Trace("cegqi-refine") << "doRefine : substitute..." << std::endl; base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); + Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl; base_lem = Rewriter::rewrite( base_lem ); + Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem + << "..." << std::endl; d_master->registerRefinementLemma(sk_vars, base_lem, lems); - - d_ce_sk.clear(); + Trace("cegqi-refine") << "doRefine : finished" << std::endl; + d_set_ce_sk_vars = false; + d_ce_sk_vars.clear(); } void CegConjecture::preregisterConjecture( Node q ) { @@ -483,15 +486,8 @@ Node CegConjecture::getModelValue( Node n ) { void CegConjecture::debugPrint( const char * c ) { Trace(c) << "Synthesis conjecture : " << d_embed_quant << std::endl; - Trace(c) << " * Candidate program/output symbol : "; - for( unsigned i=0; i terms; diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h index 231f9f14e..bf0ca4b16 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h @@ -60,7 +60,7 @@ public: /** whether the conjecture is waiting for a call to doCheck below */ bool needsCheck( std::vector< Node >& lem ); /** whether the conjecture is waiting for a call to doRefine below */ - bool needsRefinement(); + bool needsRefinement() const; /** do single invocation check * This updates Gamma for an iteration of step 2 of Figure 1 of Reynolds et al CAV 2015. */ @@ -173,11 +173,16 @@ private: /** list of variables on inner quantification */ std::vector< Node > d_inner_vars; /** - * The set of current existentially quantified formulas whose couterexamples - * we must refine. This may be added to during calls to doCheck(). The model - * values for skolems of these formulas are analyzed during doRefine(). + * The set of skolems for the current "verification" lemma, if one exists. + * This may be added to during calls to doCheck(). The model values for these + * skolems are analyzed during doRefine(). */ - std::vector d_ce_sk; + std::vector d_ce_sk_vars; + /** + * Whether the above vector has been set. We have this flag since the above + * vector may be set to empty (e.g. for ground synthesis conjectures). + */ + bool d_set_ce_sk_vars; /** the asserted (negated) conjecture */ Node d_quant; diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index 24b57d025..8b15d241e 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -1211,11 +1211,21 @@ Node CegConjectureSingleInvSol::builtinToSygusConst(Node c, Node sc; d_builtin_const_to_sygus[tn][c] = sc; Assert(c.isConst()); - Assert(tn.isDatatype()); + if (!tn.isDatatype()) + { + // if we've traversed to a builtin type, simply return c + d_builtin_const_to_sygus[tn][c] = c; + return c; + } const Datatype& dt = static_cast(tn.toType()).getDatatype(); Trace("csi-rcons-debug") << "Try to reconstruct " << c << " in " << dt.getName() << std::endl; - Assert(dt.isSygus()); + if (!dt.isSygus()) + { + // if we've traversed to a builtin datatype type, simply return c + d_builtin_const_to_sygus[tn][c] = c; + return c; + } // if we are not interested in reconstructing constants, or the grammar allows // them, return a proxy if (!options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst()) @@ -1496,9 +1506,7 @@ Node CegConjectureSingleInvSol::getGenericBase(TypeNode tn, } TermDbSygus* tds = d_qe->getTermDatabaseSygus(); Assert(tds->isRegistered(tn)); - std::map var_count; - std::map pre; - Node g = tds->mkGeneric(dt, c, var_count, pre); + Node g = tds->mkGeneric(dt, c); Trace("csi-sol-debug") << "Generic is " << g << std::endl; Node gr = Rewriter::rewrite(g); Trace("csi-sol-debug") << "Generic rewritten is " << gr << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 09df1eeab..36cbb89fe 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_eval_unfold.h" #include "options/quantifiers_options.h" +#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/sygus/term_database_sygus.h" using namespace std; @@ -30,27 +31,11 @@ SygusEvalUnfold::SygusEvalUnfold(TermDbSygus* tds) : d_tds(tds) {} void SygusEvalUnfold::registerEvalTerm(Node n) { Assert(options::sygusEvalUnfold()); - // is this an APPLY_UF term with head that is a sygus datatype term? - if (n.getKind() != APPLY_UF) + // is this a sygus evaluation function application? + if (!datatypes::DatatypesRewriter::isSygusEvalApp(n)) { return; } - TypeNode tn = n[0].getType(); - if (!tn.isDatatype()) - { - return; - } - const Datatype& dt = static_cast(tn.toType()).getDatatype(); - if (!dt.isSygus()) - { - return; - } - Node f = n.getOperator(); - if (n[0].getKind() == APPLY_CONSTRUCTOR) - { - // constructors should be unfolded and reduced already - return; - } if (d_eval_processed.find(n) != d_eval_processed.end()) { return; @@ -58,10 +43,15 @@ void SygusEvalUnfold::registerEvalTerm(Node n) Trace("sygus-eval-unfold") << "SygusEvalUnfold: register eval term : " << n << std::endl; d_eval_processed.insert(n); - // is it the sygus evaluation function? - Node eval_op = Node::fromExpr(dt.getSygusEvaluationFunc()); - if (n.getOperator() != eval_op) + TypeNode tn = n[0].getType(); + // since n[0] is an evaluation head, we know tn is a sygus datatype + Assert(tn.isDatatype()); + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + Assert(dt.isSygus()); + if (n[0].getKind() == APPLY_CONSTRUCTOR) { + // constructors should be unfolded and reduced already + Assert(false); return; } // register this evaluation term with its head @@ -112,6 +102,7 @@ void SygusEvalUnfold::registerModelValue(Node a, antec_exp.size() == 1 ? antec_exp[0] : nm->mkNode(AND, antec_exp); // Node antec = n.eqNode( vn ); TypeNode tn = n.getType(); + // n occurs as an evaluation head, thus it has sygus datatype type Assert(tn.isDatatype()); const Datatype& dt = static_cast(tn.toType()).getDatatype(); Assert(dt.isSygus()); @@ -132,7 +123,6 @@ void SygusEvalUnfold::registerModelValue(Node a, } // evaluation children std::vector eval_children; - eval_children.push_back(Node::fromExpr(dt.getSygusEvaluationFunc())); eval_children.push_back(n); // for each evaluation for (unsigned i = start; i < curr_size; i++) @@ -157,8 +147,9 @@ void SygusEvalUnfold::registerModelValue(Node a, vtm[n] = vn; eval_children.insert( eval_children.end(), it->second[i].begin(), it->second[i].end()); - Node eval_fun = nm->mkNode(APPLY_UF, eval_children); - eval_children.resize(2); + Node eval_fun = + datatypes::DatatypesRewriter::mkSygusEvalApp(eval_children); + eval_children.resize(1); res = d_tds->unfold(eval_fun, vtm, exp); expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp); } @@ -167,13 +158,15 @@ void SygusEvalUnfold::registerModelValue(Node a, EvalSygusInvarianceTest esit; eval_children.insert( eval_children.end(), it->second[i].begin(), it->second[i].end()); - Node conj = nm->mkNode(APPLY_UF, eval_children); - eval_children[1] = vn; - Node eval_fun = nm->mkNode(APPLY_UF, eval_children); + Node conj = + datatypes::DatatypesRewriter::mkSygusEvalApp(eval_children); + eval_children[0] = vn; + Node eval_fun = + datatypes::DatatypesRewriter::mkSygusEvalApp(eval_children); res = d_tds->evaluateWithUnfolding(eval_fun); esit.init(conj, n, res); - eval_children.resize(2); - eval_children[1] = n; + eval_children.resize(1); + eval_children[0] = n; // evaluate with minimal explanation std::vector mexp; diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index 2be6c9d91..f472353e5 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -123,16 +123,23 @@ void SygusExplain::getExplanationForEquality(Node n, std::vector& exp, std::map& cexc) { - Assert(n.getType() == vn.getType()); + // since builtin types occur in grammar, types are comparable but not + // necessarily equal + Assert(n.getType().isComparableTo(n.getType())); if (n == vn) { return; } - Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR); TypeNode tn = n.getType(); - Assert(tn.isDatatype()); + if (!tn.isDatatype()) + { + // sygus datatype fields that are not sygus datatypes are treated as + // abstractions only, hence we disregard this field + return; + } + Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR); const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); - int i = Datatype::indexOf(vn.getOperator().toExpr()); + int i = datatypes::DatatypesRewriter::indexOf(vn.getOperator()); Node tst = datatypes::DatatypesRewriter::mkTester(n, i, dt); exp.push_back(tst); for (unsigned j = 0; j < vn.getNumChildren(); j++) @@ -178,10 +185,16 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb, int& sz) { Assert(vnr.isNull() || vn != vnr); + Assert(n.getType().isComparableTo(vn.getType())); + TypeNode ntn = n.getType(); + if (!ntn.isDatatype()) + { + // sygus datatype fields that are not sygus datatypes are treated as + // abstractions only, hence we disregard this field + return; + } Assert(vn.getKind() == APPLY_CONSTRUCTOR); Assert(vnr.isNull() || vnr.getKind() == APPLY_CONSTRUCTOR); - Assert(n.getType() == vn.getType()); - TypeNode ntn = n.getType(); std::map cexc; // for each child, // check whether replacing that child by a fresh variable @@ -210,7 +223,7 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb, } } const Datatype& dt = ((DatatypeType)ntn.toType()).getDatatype(); - int cindex = Datatype::indexOf(vn.getOperator().toExpr()); + int cindex = datatypes::DatatypesRewriter::indexOf(vn.getOperator()); Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors()); Node tst = datatypes::DatatypesRewriter::mkTester(n, cindex, dt); exp.push_back(tst); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index d745cb6da..79db09175 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -18,9 +18,10 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" +#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/sygus/ce_guided_conjecture.h" -#include "theory/quantifiers/sygus/sygus_process_conj.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" +#include "theory/quantifiers/sygus/sygus_process_conj.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -302,20 +303,16 @@ Node CegGrammarConstructor::convertToEmbedding( Node n, std::map< Node, Node >& op = cur; } // is the operator a synth function? + bool makeEvalFun = false; if( !op.isNull() ){ std::map< Node, Node >::iterator its = synth_fun_vars.find( op ); if( its!=synth_fun_vars.end() ){ - Assert( its->second.getType().isDatatype() ); - // will make into an application of an evaluation function - const Datatype& dt = ((DatatypeType)its->second.getType().toType()).getDatatype(); - Assert( dt.isSygus() ); - children.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) ); children.push_back( its->second ); - childChanged = true; - ret_k = kind::APPLY_UF; + makeEvalFun = true; } } - if( !childChanged ){ + if (!makeEvalFun) + { // otherwise, we apply the previous operator if( cur.getMetaKind() == kind::metakind::PARAMETERIZED ){ children.push_back( cur.getOperator() ); @@ -328,7 +325,13 @@ Node CegGrammarConstructor::convertToEmbedding( Node n, std::map< Node, Node >& childChanged = childChanged || cur[i] != it->second; children.push_back(it->second); } - if (childChanged) { + if (makeEvalFun) + { + // will make into an application of an evaluation function + ret = datatypes::DatatypesRewriter::mkSygusEvalApp(children); + } + else if (childChanged) + { ret = NodeManager::currentNM()->mkNode(ret_k, children); } visited[cur] = ret; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index a468e1383..d1990d6c7 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -20,6 +20,7 @@ #include "printer/sygus_print_callback.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" #include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_grammar_red.h" @@ -125,11 +126,14 @@ void SygusGrammarNorm::TypeObject::buildDatatype(SygusGrammarNorm* sygus_norm, std::stringstream ss; ss << d_unres_tn << "_any_constant"; std::string cname(ss.str()); - std::vector empty_arg_types; + std::vector builtin_arg; + builtin_arg.push_back(dt.getSygusType()); // we add this constructor first since we use left associative chains // and our symmetry breaking should group any constants together // beneath the same application - d_dt.addSygusConstructor(av.toExpr(), cname, empty_arg_types); + // we set its weight to zero since it should be considered at the + // same level as constants. + d_dt.addSygusConstructor(av.toExpr(), cname, builtin_arg, nullptr, 0); } } for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i) diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index 47cc19377..f72a83e5a 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -36,12 +36,6 @@ namespace quantifiers { class SygusGrammarNorm; -/** Attribute true for variables that represent any constant */ -struct SygusAnyConstAttributeId -{ -}; -typedef expr::Attribute SygusAnyConstAttribute; - /** Operator position trie class * * This data structure stores an unresolved type corresponding to the diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 9919dff49..80d41a73d 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -47,55 +47,64 @@ void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited, visited[n] = true; Node neval; Node n_output; - if( n.getKind()==APPLY_UF && n.getNumChildren()>0 ){ + bool neval_is_evalapp = false; + if (datatypes::DatatypesRewriter::isSygusEvalApp(n)) + { neval = n; if( hasPol ){ n_output = !pol ? d_true : d_false; } + neval_is_evalapp = true; }else if( n.getKind()==EQUAL && hasPol && !pol ){ for( unsigned r=0; r<2; r++ ){ - if( n[r].getKind()==APPLY_UF && n[r].getNumChildren()>0 ){ + if (datatypes::DatatypesRewriter::isSygusEvalApp(n[r])) + { neval = n[r]; if( n[1-r].isConst() ){ n_output = n[1-r]; } + neval_is_evalapp = true; } } } - if( !neval.isNull() ){ - if( neval.getKind()==APPLY_UF && neval.getNumChildren()>0 ){ - // is it an evaluation function? - if( d_examples.find( neval[0] )!=d_examples.end() ){ - std::map< Node, bool >::iterator itx = d_examples_invalid.find( neval[0] ); - if( itx==d_examples_invalid.end() ){ - //collect example - bool success = true; - std::vector< Node > ex; - for( unsigned j=1; j::iterator itx = d_examples_invalid.find(eh); + if (itx == d_examples_invalid.end()) + { + // collect example + bool success = true; + std::vector ex; + for (unsigned j = 1, nchild = neval.getNumChildren(); j < nchild; j++) + { + if (!neval[j].isConst()) + { + success = false; + break; + } + ex.push_back(neval[j]); + } + if (success) + { + d_examples[eh].push_back(ex); + d_examples_out[eh].push_back(n_output); + d_examples_term[eh].push_back(neval); + if (n_output.isNull()) + { + d_examples_out_invalid[eh] = true; + } + else + { + Assert(n_output.isConst()); } + // finished processing this node + return; } + d_examples_invalid[eh] = true; + d_examples_out_invalid[eh] = true; } } for( unsigned i=0; i #include "expr/datatype.h" +#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 77930fb42..4aaccc71e 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -19,6 +19,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -61,9 +62,18 @@ void SygusRepairConst::registerSygusType(TypeNode tn, if (tprocessed.find(tn) == tprocessed.end()) { tprocessed[tn] = true; - Assert(tn.isDatatype()); + if (!tn.isDatatype()) + { + // may have recursed to a non-datatype, e.g. in the case that we have + // "any constant" constructors + return; + } const Datatype& dt = static_cast(tn.toType()).getDatatype(); - Assert(dt.isSygus()); + if (!dt.isSygus()) + { + // may have recursed to a non-sygus-datatype + return; + } // check if this datatype allows all constants if (dt.getSygusAllowConst()) { @@ -292,19 +302,22 @@ bool SygusRepairConst::isRepairable(Node n, bool useConstantsAsHoles) TypeNode tn = n.getType(); Assert(tn.isDatatype()); const Datatype& dt = static_cast(tn.toType()).getDatatype(); - Assert(dt.isSygus()); - Node op = n.getOperator(); - unsigned cindex = Datatype::indexOf(op.toExpr()); - if (dt[cindex].getNumArgs() > 0) + if (!dt.isSygus()) { return false; } + Node op = n.getOperator(); + unsigned cindex = datatypes::DatatypesRewriter::indexOf(op); Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp()); if (sygusOp.getAttribute(SygusAnyConstAttribute())) { // if it represents "any constant" then it is repairable return true; } + if (dt[cindex].getNumArgs() > 0) + { + return false; + } if (useConstantsAsHoles && dt.getSygusAllowConst()) { if (sygusOp.isConst()) @@ -445,7 +458,7 @@ Node SygusRepairConst::getFoQuery(const std::vector& candidates, if (it == visited.end()) { visited[cur] = Node::null(); - if (cur.getKind() == APPLY_UF && cur.getNumChildren() > 0) + if (datatypes::DatatypesRewriter::isSygusEvalApp(cur)) { Node v = cur[0]; if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end()) diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index a96505ce4..759ee6ffa 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -17,6 +17,7 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" +#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -80,7 +81,7 @@ Node SygusUnifRl::purifyLemma(Node n, // We retrive model value now because purified node may not have a value Node nv = n; // Whether application of a function-to-synthesize - bool fapp = k == APPLY_UF && size > 0; + bool fapp = datatypes::DatatypesRewriter::isSygusEvalApp(n); bool u_fapp = false; bool nu_fapp = false; if (fapp) @@ -135,10 +136,10 @@ Node SygusUnifRl::purifyLemma(Node n, Node nb; if (childChanged) { - if (fapp && n.hasOperator()) + if (n.getMetaKind() == metakind::PARAMETERIZED) { Trace("sygus-unif-rl-purify-debug") << "Node " << n - << " has operator and fapp is true\n"; + << " is parameterized\n"; children.insert(children.begin(), n.getOperator()); } if (Trace.isOn("sygus-unif-rl-purify-debug")) @@ -165,11 +166,6 @@ Node SygusUnifRl::purifyLemma(Node n, std::map::const_iterator it = d_app_to_purified.find(nb); if (it == d_app_to_purified.end()) { - if (!childChanged) - { - Assert(nb.hasOperator()); - children.insert(children.begin(), n.getOperator()); - } // Build purified head with fresh skolem and recreate node std::stringstream ss; ss << nb[0] << "_" << d_cand_to_hd_count[nb[0]]++; @@ -183,10 +179,10 @@ Node SygusUnifRl::purifyLemma(Node n, d_cand_to_eval_hds[nb[0]].push_back(new_f); // Maps new enumerator to its respective tuple of arguments d_hd_to_pt[new_f] = - std::vector(children.begin() + 2, children.end()); + std::vector(children.begin() + 1, children.end()); if (Trace.isOn("sygus-unif-rl-purify-debug")) { - Trace("sygus-unif-rl-purify-debug") << "...[" << new_f << "] --> ("; + Trace("sygus-unif-rl-purify-debug") << "...[" << new_f << "] --> ( "; for (const Node& pt_i : d_hd_to_pt[new_f]) { Trace("sygus-unif-rl-purify-debug") << pt_i << " "; @@ -194,9 +190,11 @@ Node SygusUnifRl::purifyLemma(Node n, Trace("sygus-unif-rl-purify-debug") << ")\n"; } // replace first child and rebulid node - children[1] = new_f; - Assert(children.size() > 1); - np = NodeManager::currentNM()->mkNode(k, children); + Assert(children.size() > 0); + children[0] = new_f; + Trace("sygus-unif-rl-purify-debug") << "Make sygus eval app " << children + << std::endl; + np = datatypes::DatatypesRewriter::mkSygusEvalApp(children); d_app_to_purified[nb] = np; } else @@ -846,17 +844,18 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::evaluate(Node n, Assert(d_dt->d_unif->d_hd_to_pt.find(n) != d_dt->d_unif->d_hd_to_pt.end()); std::vector pt = d_dt->d_unif->d_hd_to_pt[n]; // compute the result - Node res = d_dt->d_unif->d_tds->evaluateBuiltin(tn, builtin_cond, pt); if (Trace.isOn("sygus-unif-rl-sep")) { - Trace("sygus-unif-rl-sep") << "...got res = " << res << " from cond " - << builtin_cond << " on pt " << n << " ( "; + Trace("sygus-unif-rl-sep") << "Evaluate cond " << builtin_cond << " on pt " + << n << " ( "; for (const Node& pti : pt) { Trace("sygus-unif-rl-sep") << pti << " "; } Trace("sygus-unif-rl-sep") << ")\n"; } + Node res = d_dt->d_unif->d_tds->evaluateBuiltin(tn, builtin_cond, pt); + Trace("sygus-unif-rl-sep") << "...got res = " << res << "\n"; // If condition is templated, recompute result accordingly Node templ = d_dt->d_template.first; TNode templ_var = d_dt->d_template.second; diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index e236613c0..5a5ca1719 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -208,6 +208,8 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) } // look at information on how we will construct solutions for this type + // we know this is a sygus datatype since it is either the top-level type + // in the strategy graph, or was recursed by a strategy we inferred. Assert(tn.isDatatype()); const Datatype& dt = static_cast(tn.toType()).getDatatype(); Assert(dt.isSygus()); @@ -246,14 +248,13 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) } Node ut = nm->mkNode(APPLY_CONSTRUCTOR, utchildren); std::vector echildren; - echildren.push_back(Node::fromExpr(dt.getSygusEvaluationFunc())); echildren.push_back(ut); Node sbvl = Node::fromExpr(dt.getSygusVarList()); for (const Node& sbv : sbvl) { echildren.push_back(sbv); } - Node eut = nm->mkNode(APPLY_UF, echildren); + Node eut = datatypes::DatatypesRewriter::mkSygusEvalApp(echildren); Trace("sygus-unif-debug2") << " Test evaluation of " << eut << "..." << std::endl; eut = d_qe->getTermDatabaseSygus()->unfold(eut); @@ -292,13 +293,10 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) for (unsigned k = 0, sksize = sks.size(); k < sksize; k++) { Assert(sks[k].getType().isDatatype()); - const Datatype& cdt = - static_cast(sks[k].getType().toType()).getDatatype(); - echildren[0] = Node::fromExpr(cdt.getSygusEvaluationFunc()); - echildren[1] = sks[k]; + echildren[0] = sks[k]; Trace("sygus-unif-debug2") << "...set eval dt to " << sks[k] << std::endl; - Node esk = nm->mkNode(APPLY_UF, echildren); + Node esk = datatypes::DatatypesRewriter::mkSygusEvalApp(echildren); vs.push_back(esk); Node tvar = nm->mkSkolem("templ", esk.getType()); templ_var_index[tvar] = k; @@ -803,8 +801,7 @@ void SygusUnifStrategy::staticLearnRedundantOps( continue; } EnumTypeInfoStrat* etis = snode.d_strats[j]; - unsigned cindex = - static_cast(Datatype::indexOf(etis->d_cons.toExpr())); + unsigned cindex = datatypes::DatatypesRewriter::indexOf(etis->d_cons); // constructors that correspond to strategies are not needed // the intuition is that the strategy itself is responsible for constructing // all terms that use the given constructor diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 8f20e2ffc..76836d838 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -17,8 +17,8 @@ #include "base/cvc4_check.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" +#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -139,19 +139,16 @@ Node TermDbSygus::mkGeneric(const Datatype& dt, Assert( dt.isSygus() ); Assert( !dt[c].getSygusOp().isNull() ); std::vector< Node > children; - Node op = Node::fromExpr( dt[c].getSygusOp() ); - if( op.getKind()!=BUILTIN ){ - children.push_back( op ); - } - Trace("sygus-db-debug") << "mkGeneric " << dt.getName() << " " << op << " " << op.getKind() << "..." << std::endl; + Trace("sygus-db-debug") << "mkGeneric " << dt.getName() << " " << c << "..." + << std::endl; for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++) { - TypeNode tna = getArgType( dt[c], i ); Node a; std::map< int, Node >::iterator it = pre.find( i ); if( it!=pre.end() ){ a = it->second; }else{ + TypeNode tna = TypeNode::fromType(dt[c].getArgType(i)); a = getFreeVarInc( tna, var_count, true ); } Trace("sygus-db-debug") @@ -159,21 +156,7 @@ Node TermDbSygus::mkGeneric(const Datatype& dt, Assert( !a.isNull() ); children.push_back( a ); } - Node ret; - if( op.getKind()==BUILTIN ){ - Trace("sygus-db-debug") << "Make builtin node..." << std::endl; - ret = NodeManager::currentNM()->mkNode( op, children ); - }else{ - Kind ok = getOperatorKind( op ); - Trace("sygus-db-debug") << "Operator kind is " << ok << std::endl; - if( children.size()==1 && ok==kind::UNDEFINED_KIND ){ - ret = children[0]; - }else{ - ret = NodeManager::currentNM()->mkNode( ok, children ); - } - } - Trace("sygus-db-debug") << "...returning " << ret << std::endl; - return ret; + return datatypes::DatatypesRewriter::mkSygusTerm(dt, c, children); } Node TermDbSygus::mkGeneric(const Datatype& dt, int c, std::map& pre) @@ -194,49 +177,39 @@ struct SygusToBuiltinAttributeId typedef expr::Attribute SygusToBuiltinAttribute; -Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) { - std::map var_count; - return sygusToBuiltin(n, tn, var_count); -} - -Node TermDbSygus::sygusToBuiltin(Node n, - TypeNode tn, - std::map& var_count) +Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn) { Assert( n.getType()==tn ); - Assert( tn.isDatatype() ); - + if (!tn.isDatatype()) + { + return n; + } // has it already been computed? - if (var_count.empty() && n.hasAttribute(SygusToBuiltinAttribute())) + if (n.hasAttribute(SygusToBuiltinAttribute())) { return n.getAttribute(SygusToBuiltinAttribute()); } Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n << ", type = " << tn << std::endl; const Datatype& dt = static_cast(tn.toType()).getDatatype(); + if (!dt.isSygus()) + { + return n; + } if (n.getKind() == APPLY_CONSTRUCTOR) { - bool var_count_empty = var_count.empty(); - unsigned i = Datatype::indexOf(n.getOperator().toExpr()); + unsigned i = datatypes::DatatypesRewriter::indexOf(n.getOperator()); Assert(n.getNumChildren() == dt[i].getNumArgs()); std::map pre; for (unsigned j = 0, size = n.getNumChildren(); j < size; j++) { - // if the child is a symbolic constructor, do not include it - if (!isSymbolicConsApp(n[j])) - { - pre[j] = sygusToBuiltin( - n[j], TypeNode::fromType(dt[i].getArgType(j)), var_count); - } + pre[j] = sygusToBuiltin(n[j], TypeNode::fromType(dt[i].getArgType(j))); } - Node ret = mkGeneric(dt, i, var_count, pre); + Node ret = mkGeneric(dt, i, pre); Trace("sygus-db-debug") << "SygusToBuiltin : Generic is " << ret << std::endl; - // cache if we had a fresh variable count - if (var_count_empty) - { - n.setAttribute(SygusToBuiltinAttribute(), ret); - } + // cache + n.setAttribute(SygusToBuiltinAttribute(), ret); return ret; } if (n.hasAttribute(SygusPrintProxyAttribute())) @@ -259,20 +232,20 @@ Node TermDbSygus::sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& ar } unsigned TermDbSygus::getSygusTermSize( Node n ){ - if( n.getNumChildren()==0 ){ + if (n.getKind() != APPLY_CONSTRUCTOR) + { return 0; - }else{ - Assert(n.getKind() == APPLY_CONSTRUCTOR); - unsigned sum = 0; - for( unsigned i=0; i= 0 && cindex < (int)dt.getNumConstructors()); - unsigned weight = dt[cindex].getWeight(); - return weight + sum; } + unsigned sum = 0; + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + sum += getSygusTermSize(n[i]); + } + const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); + int cindex = datatypes::DatatypesRewriter::indexOf(n.getOperator()); + Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors()); + unsigned weight = dt[cindex].getWeight(); + return weight + sum; } class ReqTrie { @@ -778,6 +751,7 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { CVC4_CHECK(gtn.isSubtypeOf(btn)) << "Sygus datatype " << dt.getName() << " encodes terms that are not of type " << btn << std::endl; + Trace("sygus-db") << "...done register Operator #" << i << std::endl; } // compute min type depth information computeMinTypeDepthInternal(tn, tn, 0); @@ -817,6 +791,8 @@ void TermDbSygus::registerEnumerator(Node e, d_enum_to_active_guard[e] = eg; } + Trace("sygus-db") << " registering symmetry breaking clauses..." + << std::endl; d_enum_to_using_sym_cons[e] = useSymbolicCons; // depending on if we are using symbolic constructors, introduce symmetry // breaking lemma templates for each relevant subtype of the grammar @@ -858,9 +834,12 @@ void TermDbSygus::registerEnumerator(Node e, for (unsigned& rindex : rm_indices) { // make the apply-constructor corresponding to an application of the - // "any constant" constructor - Node exc_val = nm->mkNode(APPLY_CONSTRUCTOR, - Node::fromExpr(dt[rindex].getConstructor())); + // constant or "any constant" constructor + // we call getInstCons since in the case of any constant constructors, it + // is necessary to generate a term of the form any_constant( x.0 ) for a + // fresh variable x.0. + Node fv = getFreeVar(stn, 0); + Node exc_val = datatypes::DatatypesRewriter::getInstCons(fv, dt, rindex); // should not include the constuctor in any subterm Node x = getFreeVar(stn, 0); Trace("sygus-db") << "Construct symmetry breaking lemma from " << x @@ -875,6 +854,7 @@ void TermDbSygus::registerEnumerator(Node e, registerSymBreakLemma(e, lem, stn, dt[rindex].getWeight()); } } + Trace("sygus-db") << " ...finished" << std::endl; } bool TermDbSygus::isEnumerator(Node e) const @@ -991,8 +971,12 @@ TypeNode TermDbSygus::sygusToBuiltinType( TypeNode tn ) { void TermDbSygus::computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth ) { std::map< TypeNode, unsigned >::iterator it = d_min_type_depth[root_tn].find( tn ); if( it==d_min_type_depth[root_tn].end() || type_depthsecond ){ + if (!tn.isDatatype()) + { + // do not recurse to non-datatype types + return; + } d_min_type_depth[root_tn][tn] = type_depth; - Assert( tn.isDatatype() ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); //compute for connected types for( unsigned i=0; i(tn.toType()).getDatatype(); Assert(dt.isSygus()); - unsigned cindex = Datatype::indexOf(n.getOperator().toExpr()); + unsigned cindex = datatypes::DatatypesRewriter::indexOf(n.getOperator()); Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp()); // it is symbolic if it represents "any constant" return sygusOp.getAttribute(SygusAnyConstAttribute()); @@ -1377,34 +1362,6 @@ void doStrReplace(std::string& str, const std::string& oldStr, const std::string } } -Kind TermDbSygus::getOperatorKind( Node op ) { - Assert( op.getKind()!=BUILTIN ); - if (op.getKind() == LAMBDA) - { - // we use APPLY_UF instead of APPLY, since the rewriter for APPLY_UF - // does beta-reduction but does not for APPLY - return APPLY_UF; - }else{ - TypeNode tn = op.getType(); - if( tn.isConstructor() ){ - return APPLY_CONSTRUCTOR; - } - else if (tn.isSelector()) - { - return APPLY_SELECTOR; - } - else if (tn.isTester()) - { - return APPLY_TESTER; - } - else if (tn.isFunction()) - { - return APPLY_UF; - } - return NodeManager::operatorToKind(op); - } -} - Node TermDbSygus::getAnchor( Node n ) { if( n.getKind()==APPLY_SELECTOR_TOTAL ){ return getAnchor( n[0] ); @@ -1422,81 +1379,118 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) { } Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp ) { - if( en.getKind()==kind::APPLY_UF ){ - Trace("sygus-db-debug") << "Unfold : " << en << std::endl; - Node ev = en[0]; - if( track_exp ){ - std::map< Node, Node >::iterator itv = vtm.find( en[0] ); - if( itv!=vtm.end() ){ - ev = itv->second; - }else{ - Assert( false ); - } - Assert( en[0].getType()==ev.getType() ); - Assert( ev.isConst() ); + if (!datatypes::DatatypesRewriter::isSygusEvalApp(en)) + { + Assert(en.isConst()); + return en; + } + Trace("sygus-db-debug") << "Unfold : " << en << std::endl; + Node ev = en[0]; + if (track_exp) + { + std::map::iterator itv = vtm.find(en[0]); + Assert(itv != vtm.end()); + if (itv != vtm.end()) + { + ev = itv->second; } - Assert( ev.getKind()==kind::APPLY_CONSTRUCTOR ); - std::vector< Node > args; - for( unsigned i=1; i args; + for (unsigned i = 1, nchild = en.getNumChildren(); i < nchild; i++) + { + args.push_back(en[i]); + } + + Type headType = en[0].getType().toType(); + NodeManager* nm = NodeManager::currentNM(); + const Datatype& dt = static_cast(headType).getDatatype(); + unsigned i = datatypes::DatatypesRewriter::indexOf(ev.getOperator()); + if (track_exp) + { + // explanation + Node ee = nm->mkNode( + kind::APPLY_TESTER, Node::fromExpr(dt[i].getTester()), en[0]); + if (std::find(exp.begin(), exp.end(), ee) == exp.end()) + { + exp.push_back(ee); } - const Datatype& dt = ((DatatypeType)(ev.getType()).toType()).getDatatype(); - unsigned i = Datatype::indexOf( ev.getOperator().toExpr() ); - if( track_exp ){ - //explanation - Node ee = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), en[0] ); - if( std::find( exp.begin(), exp.end(), ee )==exp.end() ){ - exp.push_back( ee ); - } + } + // if we are a symbolic constructor, unfolding returns the subterm itself + Node sop = Node::fromExpr(dt[i].getSygusOp()); + if (sop.getAttribute(SygusAnyConstAttribute())) + { + Trace("sygus-db-debug") << "...it is an any-constant constructor" + << std::endl; + Assert(dt[i].getNumArgs() == 1); + if (en[0].getKind() == APPLY_CONSTRUCTOR) + { + return en[0][0]; } - Assert( !dt.isParametric() ); - std::map< int, Node > pre; - for( unsigned j=0; j cc; - //get the evaluation argument for the selector - Type rt = dt[i][j].getRangeType(); - const Datatype & ad = ((DatatypeType)dt[i][j].getRangeType()).getDatatype(); - cc.push_back( Node::fromExpr( ad.getSygusEvaluationFunc() ) ); - Node s; - if( en[0].getKind()==kind::APPLY_CONSTRUCTOR ){ - s = en[0][j]; - }else{ - s = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal( en[0].getType().toType(), j ), en[0] ); - } - cc.push_back( s ); - if( track_exp ){ - //update vtm map - vtm[s] = ev[j]; - } - cc.insert( cc.end(), args.begin(), args.end() ); - pre[j] = NodeManager::currentNM()->mkNode( kind::APPLY_UF, cc ); + else + { + return nm->mkNode( + APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, 0), en[0]); } - Node ret = mkGeneric(dt, i, pre); - // if it is a variable, apply the substitution - if( ret.getKind()==kind::BOUND_VARIABLE ){ - Assert( ret.hasAttribute(SygusVarNumAttribute()) ); - int i = ret.getAttribute(SygusVarNumAttribute()); - Assert( Node::fromExpr( dt.getSygusVarList() )[i]==ret ); - ret = args[i]; + } + + Assert(!dt.isParametric()); + std::map pre; + for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) + { + std::vector cc; + Node s; + // get the j^th subfield of en + if (en[0].getKind() == kind::APPLY_CONSTRUCTOR) + { + // if it is a concrete constructor application, as an optimization, + // just return the argument + s = en[0][j]; } else { - ret = Rewriter::rewrite(ret); + s = nm->mkNode(kind::APPLY_SELECTOR_TOTAL, + dt[i].getSelectorInternal(headType, j), + en[0]); } - return ret; - }else{ - Assert( en.isConst() ); + cc.push_back(s); + if (track_exp) + { + // update vtm map + vtm[s] = ev[j]; + } + cc.insert(cc.end(), args.begin(), args.end()); + pre[j] = datatypes::DatatypesRewriter::mkSygusEvalApp(cc); + } + Node ret = mkGeneric(dt, i, pre); + // if it is a variable, apply the substitution + if (ret.getKind() == kind::BOUND_VARIABLE) + { + Assert(ret.hasAttribute(SygusVarNumAttribute())); + int i = ret.getAttribute(SygusVarNumAttribute()); + Assert(Node::fromExpr(dt.getSygusVarList())[i] == ret); + return args[i]; } - return en; + ret = Rewriter::rewrite(ret); + return ret; } +Node TermDbSygus::unfold(Node en) +{ + std::map vtm; + std::vector exp; + return unfold(en, vtm, exp, false); +} Node TermDbSygus::getEagerUnfold( Node n, std::map< Node, Node >& visited ) { std::map< Node, Node >::iterator itv = visited.find( n ); if( itv==visited.end() ){ Trace("cegqi-eager-debug") << "getEagerUnfold " << n << std::endl; Node ret; - if( n.getKind()==APPLY_UF ){ + if (datatypes::DatatypesRewriter::isSygusEvalApp(n)) + { TypeNode tn = n[0].getType(); Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl; if( tn.isDatatype() ){ @@ -1573,7 +1567,9 @@ Node TermDbSygus::evaluateWithUnfolding( visited.find(n); if( it==visited.end() ){ Node ret = n; - while( ret.getKind()==APPLY_UF && ret[0].getKind()==APPLY_CONSTRUCTOR ){ + while (datatypes::DatatypesRewriter::isSygusEvalApp(ret) + && ret[0].getKind() == APPLY_CONSTRUCTOR) + { ret = unfold( ret ); } if( ret.getNumChildren()>0 ){ @@ -1606,7 +1602,11 @@ Node TermDbSygus::evaluateWithUnfolding( Node n ) { bool TermDbSygus::isEvaluationPoint(Node n) const { - if (n.getKind() != APPLY_UF || n.getNumChildren() == 0 || !n[0].isVar()) + if (!datatypes::DatatypesRewriter::isSygusEvalApp(n)) + { + return false; + } + if (!n[0].isVar()) { return false; } @@ -1617,18 +1617,7 @@ bool TermDbSygus::isEvaluationPoint(Node n) const return false; } } - TypeNode tn = n[0].getType(); - if (!tn.isDatatype()) - { - return false; - } - const Datatype& dt = static_cast(tn.toType()).getDatatype(); - if (!dt.isSygus()) - { - return false; - } - Node eval_op = Node::fromExpr(dt.getSygusEvaluationFunc()); - return eval_op == n.getOperator(); + return true; } }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 163d65d19..c4a035e2c 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -172,13 +172,8 @@ class TermDbSygus { * * Given a sygus datatype term n of type tn, this function returns its analog, * that is, the term that n encodes. - * - * Notice that each occurrence of a symbolic constructor application is - * replaced by a unique variable. To track counters for introducing unique - * variables, we use the var_count map. */ Node sygusToBuiltin(Node n, TypeNode tn); - Node sygusToBuiltin(Node n, TypeNode tn, std::map& var_count); /** same as above, but without tn */ Node sygusToBuiltin(Node n) { return sygusToBuiltin(n, n.getType()); } /** evaluate builtin @@ -385,10 +380,6 @@ class TermDbSygus { Node getSemanticSkolem( TypeNode tn, Node n, bool doMk = true ); /** involves div-by-zero */ bool involvesDivByZero( Node n ); - - /** get operator kind */ - static Kind getOperatorKind( Node op ); - /** get anchor */ static Node getAnchor( Node n ); static unsigned getAnchorDepth( Node n ); @@ -398,13 +389,32 @@ public: // for symmetry breaking bool considerConst( TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg ); bool considerConst( const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg ); int solveForArgument( TypeNode tnp, unsigned cindex, unsigned arg ); -public: - Node unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp = true ); - Node unfold( Node en ){ - std::map< Node, Node > vtm; - std::vector< Node > exp; - return unfold( en, vtm, exp, false ); - } + + public: + /** unfold + * + * This method returns the one-step unfolding of an evaluation function + * application. An example of a one step unfolding is: + * eval( C_+( d1, d2 ), t ) ---> +( eval( d1, t ), eval( d2, t ) ) + * + * This function does this unfolding for a (possibly symbolic) evaluation + * head, where the argument "variable to model" vtm stores the model value of + * variables from this head. This allows us to track an explanation of the + * unfolding in the vector exp when track_exp is true. + * + * For example, if vtm[d] = C_+( C_x(), C_0() ) and track_exp is true, then + * this method applied to eval( d, t ) will return + * +( eval( d.0, t ), eval( d.1, t ) ), and is-C_+( d ) is added to exp. + */ + Node unfold(Node en, + std::map& vtm, + std::vector& exp, + bool track_exp = true); + /** + * Same as above, but without explanation tracking. This is used for concrete + * evaluation heads + */ + Node unfold(Node en); Node getEagerUnfold( Node n, std::map< Node, Node >& visited ); }; diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index fb4f7e831..c1daa9288 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -605,9 +605,15 @@ Node SygusSampler::getSygusRandomValue(TypeNode tn, double rinc, unsigned depth) { - Assert(tn.isDatatype()); + if (!tn.isDatatype()) + { + return getRandomValue(tn); + } const Datatype& dt = static_cast(tn.toType()).getDatatype(); - Assert(dt.isSygus()); + if (!dt.isSygus()) + { + return getRandomValue(tn); + } Assert(d_rvalue_cindices.find(tn) != d_rvalue_cindices.end()); Trace("sygus-sample-grammar") << "Sygus random value " << tn << ", depth = " << depth @@ -671,9 +677,15 @@ void SygusSampler::registerSygusType(TypeNode tn) if (d_rvalue_cindices.find(tn) == d_rvalue_cindices.end()) { d_rvalue_cindices[tn].clear(); - Assert(tn.isDatatype()); + if (!tn.isDatatype()) + { + return; + } const Datatype& dt = static_cast(tn.toType()).getDatatype(); - Assert(dt.isSygus()); + if (!dt.isSygus()) + { + return; + } for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) { const DatatypeConstructor& dtc = dt[i]; diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 70f8bbcee..2880713af 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -76,10 +76,6 @@ typedef expr::Attribute AbsTypeFunDefAttribute; struct QuantIdNumAttributeId {}; typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute; -/** sygus var num */ -struct SygusVarNumAttributeId {}; -typedef expr::Attribute SygusVarNumAttribute; - /** Attribute to mark Skolems as virtual terms */ struct VirtualTermSkolemAttributeId {}; typedef expr::Attribute< VirtualTermSkolemAttributeId, bool > VirtualTermSkolemAttribute; -- 2.30.2