diff options
Diffstat (limited to 'src/theory/quantifiers/sygus')
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_explain.cpp | 37 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_explain.h | 27 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 55 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 72 |
6 files changed, 154 insertions, 46 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 1dd4dcbeb..2273db5ea 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -547,9 +547,8 @@ void CegConjecture::printAndContinueStream() { sol = d_cinfo[cprog].d_inst.back(); // add to explanation of exclusion - d_qe->getTermDatabaseSygus() - ->getExplain() - ->getExplanationForConstantEquality(cprog, sol, exp); + d_qe->getTermDatabaseSygus()->getExplain()->getExplanationForEquality( + cprog, sol, exp); } } Assert(!exp.empty()); @@ -612,6 +611,8 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation if (eq_sol != sol) { ++(cei->d_statistics.d_candidate_rewrites); + // if eq_sol is null, then we have an uninteresting candidate rewrite, + // e.g. one that is alpha-equivalent to another. if (!eq_sol.isNull()) { // The analog of terms sol and eq_sol are equivalent under sample diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index aafaa07e1..f76edb1c3 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -110,19 +110,25 @@ Node TermRecBuild::build(unsigned d) return NodeManager::currentNM()->mkNode(d_kind[d], children); } -void SygusExplain::getExplanationForConstantEquality(Node n, - Node vn, - std::vector<Node>& exp) +void SygusExplain::getExplanationForEquality(Node n, + Node vn, + std::vector<Node>& exp) { std::map<unsigned, bool> cexc; - getExplanationForConstantEquality(n, vn, exp, cexc); + getExplanationForEquality(n, vn, exp, cexc); } -void SygusExplain::getExplanationForConstantEquality( - Node n, Node vn, std::vector<Node>& exp, std::map<unsigned, bool>& cexc) +void SygusExplain::getExplanationForEquality(Node n, + Node vn, + std::vector<Node>& exp, + std::map<unsigned, bool>& cexc) { - Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR); Assert(n.getType() == vn.getType()); + if (n == vn) + { + return; + } + Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR); TypeNode tn = n.getType(); Assert(tn.isDatatype()); const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); @@ -137,22 +143,23 @@ void SygusExplain::getExplanationForConstantEquality( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[i].getSelectorInternal(tn.toType(), j)), n); - getExplanationForConstantEquality(sel, vn[j], exp); + getExplanationForEquality(sel, vn[j], exp); } } } -Node SygusExplain::getExplanationForConstantEquality(Node n, Node vn) +Node SygusExplain::getExplanationForEquality(Node n, Node vn) { std::map<unsigned, bool> cexc; - return getExplanationForConstantEquality(n, vn, cexc); + return getExplanationForEquality(n, vn, cexc); } -Node SygusExplain::getExplanationForConstantEquality( - Node n, Node vn, std::map<unsigned, bool>& cexc) +Node SygusExplain::getExplanationForEquality(Node n, + Node vn, + std::map<unsigned, bool>& cexc) { std::vector<Node> exp; - getExplanationForConstantEquality(n, vn, exp, cexc); + getExplanationForEquality(n, vn, exp, cexc); Assert(!exp.empty()); return exp.size() == 1 ? exp[0] : NodeManager::currentNM()->mkNode(kind::AND, exp); @@ -250,7 +257,7 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb, // if excluded, we may need to add the explanation for this if (vnr_exp.isNull() && !vnr_c.isNull()) { - vnr_exp = getExplanationForConstantEquality(sel, vnr[i]); + vnr_exp = getExplanationForEquality(sel, vnr[i]); } } } @@ -264,7 +271,7 @@ void SygusExplain::getExplanationFor(Node n, unsigned& sz) { // naive : - // return getExplanationForConstantEquality( n, vn, exp ); + // return getExplanationForEquality( n, vn, exp ); // set up the recursion object std::map<TypeNode, int> var_count; diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h index ad26f29e4..818f51438 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.h +++ b/src/theory/quantifiers/sygus/sygus_explain.h @@ -100,7 +100,7 @@ class TermRecBuild * (datatype) sygus term n is: * (if (gt x 0) 0 0) * where if, gt, x, 0 are datatype constructors. - * The explanation returned by getExplanationForConstantEquality + * The explanation returned by getExplanationForEquality * below for n and the above term is: * { ((_ is if) n), ((_ is geq) n.0), * ((_ is x) n.0.0), ((_ is 0) n.0.1), @@ -142,20 +142,19 @@ class SygusExplain public: SygusExplain(TermDbSygus* tdb) : d_tdb(tdb) {} ~SygusExplain() {} - /** get explanation for constant equality + /** get explanation for equality * * This function constructs an explanation, stored in exp, such that: * - All formulas in exp are of the form ((_ is C) ns), where ns * is a chain of selectors applied to n, and * - exp => ( n = vn ) */ - void getExplanationForConstantEquality(Node n, - Node vn, - std::vector<Node>& exp); + void getExplanationForEquality(Node n, Node vn, std::vector<Node>& exp); /** returns the conjunction of exp computed in the above function */ - Node getExplanationForConstantEquality(Node n, Node vn); + Node getExplanationForEquality(Node n, Node vn); - /** get explanation for constant equality + /** get explanation for equality + * * This is identical to the above function except that we * take an additional argument cexc, which says which * children of vn should be excluded from the explanation. @@ -165,14 +164,14 @@ class SygusExplain * { ((_ is plus) n), ((_ is y) n.1) } * where notice that the 0^th argument of vn is excluded. */ - void getExplanationForConstantEquality(Node n, - Node vn, - std::vector<Node>& exp, - std::map<unsigned, bool>& cexc); + void getExplanationForEquality(Node n, + Node vn, + std::vector<Node>& exp, + std::map<unsigned, bool>& cexc); /** returns the conjunction of exp computed in the above function */ - Node getExplanationForConstantEquality(Node n, - Node vn, - std::map<unsigned, bool>& cexc); + Node getExplanationForEquality(Node n, + Node vn, + std::map<unsigned, bool>& cexc); /** get explanation for * diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 36e883848..1c61544e1 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -1303,7 +1303,7 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& if (exp_exc.isNull()) { // if we did not already explain why this should be excluded, use default - exp_exc = d_tds->getExplain()->getExplanationForConstantEquality(x, v); + exp_exc = d_tds->getExplain()->getExplanationForEquality(x, v); } Node exlem = NodeManager::currentNM()->mkNode(OR, g.negate(), exp_exc.negate()); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index b12a23c83..e8bdf2083 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -733,6 +733,59 @@ void TermDbSygus::getEnumerators(std::vector<Node>& mts) } } +void TermDbSygus::registerSymBreakLemma(Node e, + Node lem, + TypeNode tn, + unsigned sz) +{ + d_enum_to_sb_lemmas[e].push_back(lem); + d_sb_lemma_to_type[lem] = tn; + d_sb_lemma_to_size[lem] = sz; +} + +bool TermDbSygus::hasSymBreakLemmas(std::vector<Node>& enums) const +{ + if (!d_enum_to_sb_lemmas.empty()) + { + for (std::pair<const Node, std::vector<Node> > sb : d_enum_to_sb_lemmas) + { + enums.push_back(sb.first); + } + return true; + } + return false; +} + +void TermDbSygus::getSymBreakLemmas(Node e, std::vector<Node>& lemmas) const +{ + std::map<Node, std::vector<Node> >::const_iterator itsb = + d_enum_to_sb_lemmas.find(e); + if (itsb != d_enum_to_sb_lemmas.end()) + { + lemmas.insert(lemmas.end(), itsb->second.begin(), itsb->second.end()); + } +} + +TypeNode TermDbSygus::getTypeForSymBreakLemma(Node lem) const +{ + std::map<Node, TypeNode>::const_iterator it = d_sb_lemma_to_type.find(lem); + Assert(it != d_sb_lemma_to_type.end()); + return it->second; +} +unsigned TermDbSygus::getSizeForSymBreakLemma(Node lem) const +{ + std::map<Node, unsigned>::const_iterator it = d_sb_lemma_to_size.find(lem); + Assert(it != d_sb_lemma_to_size.end()); + return it->second; +} + +void TermDbSygus::clearSymBreakLemmas() +{ + d_enum_to_sb_lemmas.clear(); + d_sb_lemma_to_type.clear(); + d_sb_lemma_to_size.clear(); +} + bool TermDbSygus::isRegistered( TypeNode tn ) { return d_register.find( tn )!=d_register.end(); } @@ -1202,7 +1255,7 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& terms unsigned start = d_node_mv_args_proc[n][vn]; // get explanation in terms of testers std::vector< Node > antec_exp; - d_syexp->getExplanationForConstantEquality(n, vn, antec_exp); + d_syexp->getExplanationForEquality(n, vn, antec_exp); Node antec = antec_exp.size()==1 ? antec_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, antec_exp ); //Node antec = n.eqNode( vn ); TypeNode tn = n.getType(); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index e796a3adc..7ef9e6151 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -40,21 +40,31 @@ class TermDbSygus { std::string identify() const { return "TermDbSygus"; } /** register the sygus type */ void registerSygusType(TypeNode tn); - /** register a variable e that we will do enumerative search on - * conj is the conjecture that the enumeration of e is for. - * f is the synth-fun that the enumeration of e is for. - * mkActiveGuard is whether we want to make an active guard for e + + //------------------------------utilities + /** get the explanation utility */ + SygusExplain* getExplain() { return d_syexp.get(); } + /** get the extended rewrite utility */ + ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); } + //------------------------------end utilities + + //------------------------------enumerators + /** + * Register a variable e that we will do enumerative search on. + * conj : the conjecture that the enumeration of e is for. + * f : the synth-fun that the enumeration of e is for. + * mkActiveGuard : whether we want to make an active guard for e * (see d_enum_to_active_guard). * - * Notice that enumerator e may not be equivalent - * to f in synthesis-through-unification approaches - * (e.g. decision tree construction for PBE synthesis). + * Notice that enumerator e may not be one-to-one with f in + * synthesis-through-unification approaches (e.g. decision tree construction + * for PBE synthesis). */ void registerEnumerator(Node e, Node f, CegConjecture* conj, bool mkActiveGuard = false); - /** is e an enumerator? */ + /** is e an enumerator registered with this class? */ bool isEnumerator(Node e) const; /** return the conjecture e is associated with */ CegConjecture* getConjectureForEnumerator(Node e); @@ -64,10 +74,36 @@ class TermDbSygus { Node getActiveGuardForEnumerator(Node e); /** get all registered enumerators */ void getEnumerators(std::vector<Node>& mts); - /** get the explanation utility */ - SygusExplain* getExplain() { return d_syexp.get(); } - /** get the extended rewrite utility */ - ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); } + /** Register symmetry breaking lemma + * + * This function registers lem as a symmetry breaking lemma template for + * subterms of enumerator e. For more information on symmetry breaking + * lemma templates, see datatypes/datatypes_sygus.h. + * + * tn : the (sygus datatype) type that lem applies to, i.e. the + * type of terms that lem blocks models for, + * sz : the minimum size of terms that the lem blocks. + * + * Notice that the symmetry breaking lemma template should be relative to x, + * where x is returned by the call to getFreeVar( tn, 0 ) in this class. + */ + void registerSymBreakLemma(Node e, Node lem, TypeNode tn, unsigned sz); + /** Has symmetry breaking lemmas been added for any enumerator? */ + bool hasSymBreakLemmas(std::vector<Node>& enums) const; + /** Get symmetry breaking lemmas + * + * Returns the set of symmetry breaking lemmas that have been registered + * for enumerator e. It adds these to lemmas. + */ + void getSymBreakLemmas(Node e, std::vector<Node>& lemmas) const; + /** Get the type of term symmetry breaking lemma lem applies to */ + TypeNode getTypeForSymBreakLemma(Node lem) const; + /** Get the minimum size of terms symmetry breaking lemma lem applies to */ + unsigned getSizeForSymBreakLemma(Node lem) const; + /** Clear information about symmetry breaking lemmas */ + void clearSymBreakLemmas(); + //------------------------------end enumerators + //-----------------------------conversion from sygus to builtin /** get free variable * @@ -121,10 +157,15 @@ class TermDbSygus { private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; + + //------------------------------utilities /** sygus explanation */ std::unique_ptr<SygusExplain> d_syexp; /** sygus explanation */ std::unique_ptr<ExtendedRewriter> d_ext_rw; + //------------------------------end utilities + + //------------------------------enumerators /** mapping from enumerator terms to the conjecture they are associated with */ std::map<Node, CegConjecture*> d_enum_to_conjecture; @@ -137,6 +178,13 @@ class TermDbSygus { * if G is true, then there are more values of e to enumerate". */ std::map<Node, Node> d_enum_to_active_guard; + /** mapping from enumerators to symmetry breaking clauses for them */ + std::map<Node, std::vector<Node> > d_enum_to_sb_lemmas; + /** mapping from symmetry breaking lemmas to type */ + std::map<Node, TypeNode> d_sb_lemma_to_type; + /** mapping from symmetry breaking lemmas to size */ + std::map<Node, unsigned> d_sb_lemma_to_size; + //------------------------------end enumerators //-----------------------------conversion from sygus to builtin /** cache for sygusToBuiltin */ |