From: Andrew Reynolds Date: Tue, 6 Nov 2018 23:28:41 +0000 (-0600) Subject: Incorporate static PBE symmetry breaking lemmas into SygusEnumerator (#2690) X-Git-Tag: cvc5-1.0.0~4373 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8a7e611fb40bb96faf85c1532fa778c47d83a899;p=cvc5.git Incorporate static PBE symmetry breaking lemmas into SygusEnumerator (#2690) --- diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index a7763bff1..4c7dcec9a 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -1304,7 +1304,8 @@ void SygusSymBreakNew::preRegisterTerm( TNode n, std::vector< Node >& lemmas ) } } -void SygusSymBreakNew::registerSizeTerm( Node e, std::vector< Node >& lemmas ) { +void SygusSymBreakNew::registerSizeTerm(Node e, std::vector& lemmas) +{ if (d_register_st.find(e) != d_register_st.end()) { // already registered @@ -1545,15 +1546,32 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { { // symmetry breaking lemmas should only be for enumerators Assert(d_register_st[a]); - std::vector sbl; - d_tds->getSymBreakLemmas(a, sbl); - for (const Node& lem : sbl) + // If this is a non-basic enumerator, process its symmetry breaking + // clauses. Since this class is not responsible for basic enumerators, + // their symmetry breaking clauses are ignored. + if (!d_tds->isBasicEnumerator(a)) { - TypeNode tn = d_tds->getTypeForSymBreakLemma(lem); - unsigned sz = d_tds->getSizeForSymBreakLemma(lem); - registerSymBreakLemma(tn, lem, sz, a, lemmas); + std::vector sbl; + d_tds->getSymBreakLemmas(a, sbl); + for (const Node& lem : sbl) + { + if (d_tds->isSymBreakLemmaTemplate(lem)) + { + // register the lemma template + TypeNode tn = d_tds->getTypeForSymBreakLemma(lem); + unsigned sz = d_tds->getSizeForSymBreakLemma(lem); + registerSymBreakLemma(tn, lem, sz, a, lemmas); + } + else + { + Trace("dt-sygus-debug") + << "DT sym break lemma : " << lem << std::endl; + // it is a normal lemma + lemmas.push_back(lem); + } + } + d_tds->clearSymBreakLemmas(a); } - d_tds->clearSymBreakLemmas(a); } } if (!lemmas.empty()) @@ -1563,9 +1581,20 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { } // register search values, add symmetry breaking lemmas if applicable - for( std::map< Node, bool >::iterator it = d_register_st.begin(); it != d_register_st.end(); ++it ){ - if( it->second ){ - Node prog = it->first; + std::vector es; + d_tds->getEnumerators(es); + bool needsRecheck = false; + // for each enumerator registered to d_tds + for (Node& prog : es) + { + if (d_register_st.find(prog) == d_register_st.end()) + { + // not yet registered, do so now + registerSizeTerm(prog, lemmas); + needsRecheck = true; + } + else + { Trace("dt-sygus-debug") << "Checking model value of " << prog << "..." << std::endl; Assert(prog.getType().isDatatype()); @@ -1624,14 +1653,12 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { prog.setAttribute(ssbo, !isExc); } } - //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 sbl; + d_tds->getSymBreakLemmas(e, sbl); + Node ag = d_tds->getActiveGuardForEnumerator(e); + Node truen = nm->mkConst(true); + // use TNode for substitute below + TNode agt = ag; + TNode truent = truen; + Assert(d_tcache.find(d_etype) != d_tcache.end()); + const Datatype& dt = d_etype.getDatatype(); + for (const Node& lem : sbl) + { + if (!d_tds->isSymBreakLemmaTemplate(lem)) + { + // substitute its active guard by true and rewrite + Node slem = lem.substitute(agt, truent); + slem = Rewriter::rewrite(slem); + // break into conjuncts + std::vector sblc; + if (slem.getKind() == AND) + { + for (const Node& slemc : slem) + { + sblc.push_back(slemc); + } + } + else + { + sblc.push_back(slem); + } + for (const Node& sbl : sblc) + { + Trace("sygus-enum") + << " symmetry breaking lemma : " << sbl << std::endl; + // if its a negation of a unit top-level tester, then this specifies + // that we should not enumerate terms whose top symbol is that + // constructor + if (sbl.getKind() == NOT) + { + Node a; + int tst = datatypes::DatatypesRewriter::isTester(sbl[0], a); + if (tst >= 0) + { + if (a == e) + { + Node cons = Node::fromExpr(dt[tst].getConstructor()); + Trace("sygus-enum") << " ...unit exclude constructor #" << tst + << ", constructor " << cons << std::endl; + d_sbExcTlCons.insert(cons); + } + } + } + // other symmetry breaking lemmas such as disjunctions are not used + } + } + } } void SygusEnumerator::addValue(Node v) @@ -57,6 +119,17 @@ Node SygusEnumerator::getCurrent() } } Node ret = d_tlEnum->getCurrent(); + if (!ret.isNull() && !d_sbExcTlCons.empty()) + { + Assert(ret.hasOperator()); + // might be excluded by an externally provided symmetry breaking clause + if (d_sbExcTlCons.find(ret.getOperator()) != d_sbExcTlCons.end()) + { + Trace("sygus-enum-exc") + << "Exclude (external) : " << d_tds->sygusToBuiltin(ret) << std::endl; + ret = Node::null(); + } + } if (Trace.isOn("sygus-enum")) { Trace("sygus-enum") << "Enumerate : "; diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index 28f8f4126..af6bb03f0 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -435,6 +435,15 @@ class SygusEnumerator : public EnumValGenerator int d_abortSize; /** get master enumerator for type tn */ TermEnum* getMasterEnumForType(TypeNode tn); + //-------------------------------- externally specified symmetry breaking + /** set of constructors we disallow at top level + * + * A constructor C is disallowed at the top level if a symmetry breaking + * lemma that entails ~is-C( d_enum ) was registered to + * TermDbSygus::registerSymBreakLemma. + */ + std::unordered_set d_sbExcTlCons; + //-------------------------------- end externally specified symmetry breaking }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index f91dd5d30..ee7247121 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -228,13 +228,24 @@ bool SygusPbe::initialize(Node n, { lem = lem.substitute(tsp, te); } - disj.push_back(lem); + if (std::find(disj.begin(), disj.end(), lem) == disj.end()) + { + disj.push_back(lem); + } } } + // add its active guard + Node ag = d_tds->getActiveGuardForEnumerator(e); + Assert(!ag.isNull()); + disj.push_back(ag.negate()); Node lem = disj.size() == 1 ? disj[0] : nm->mkNode(OR, disj); Trace("sygus-pbe") << " static redundant op lemma : " << lem << std::endl; - lemmas.push_back(lem); + // Register as a symmetry breaking lemma with the term database. + // This will either be processed via a lemma on the output channel + // of the sygus extension of the datatypes solver, or internally + // encoded as a constraint to an active enumerator. + d_tds->registerSymBreakLemma(e, lem, etn, 0, false); } } Trace("sygus-pbe") << "Initialize " << d_examples[c].size() diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 5cf230820..9198f7e56 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -682,6 +682,10 @@ void TermDbSygus::registerEnumerator(Node e, Node ag = nm->mkSkolem("eG", nm->booleanType()); // must ensure it is a literal immediately here ag = d_quantEngine->getValuation().ensureLiteral(ag); + // must ensure that it is asserted as a literal before we begin solving + Node lem = nm->mkNode(OR, ag, ag.negate()); + d_quantEngine->getOutputChannel().requirePhase(ag, true); + d_quantEngine->getOutputChannel().lemma(lem); d_enum_to_active_guard[e] = ag; } } @@ -771,14 +775,13 @@ void TermDbSygus::getEnumerators(std::vector& mts) } } -void TermDbSygus::registerSymBreakLemma(Node e, - Node lem, - TypeNode tn, - unsigned sz) +void TermDbSygus::registerSymBreakLemma( + Node e, Node lem, TypeNode tn, unsigned sz, bool isTempl) { d_enum_to_sb_lemmas[e].push_back(lem); d_sb_lemma_to_type[lem] = tn; d_sb_lemma_to_size[lem] = sz; + d_sb_lemma_to_isTempl[lem] = isTempl; } bool TermDbSygus::hasSymBreakLemmas(std::vector& enums) const @@ -817,6 +820,13 @@ unsigned TermDbSygus::getSizeForSymBreakLemma(Node lem) const return it->second; } +bool TermDbSygus::isSymBreakLemmaTemplate(Node lem) const +{ + std::map::const_iterator it = d_sb_lemma_to_isTempl.find(lem); + Assert(it != d_sb_lemma_to_isTempl.end()); + return it->second; +} + void TermDbSygus::clearSymBreakLemmas(Node e) { d_enum_to_sb_lemmas.erase(e); } bool TermDbSygus::isRegistered(TypeNode tn) const diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 2e8604411..7a522ded6 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -170,12 +170,13 @@ class TermDbSygus { * * 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. + * sz : the minimum size of terms that the lem blocks, + * isTempl : if this flag is false, then lem is a (concrete) lemma. + * If this flag is true, then lem is a symmetry breaking lemma template + * over x, where x is returned by the call to getFreeVar( tn, 0 ). */ - void registerSymBreakLemma(Node e, Node lem, TypeNode tn, unsigned sz); + void registerSymBreakLemma( + Node e, Node lem, TypeNode tn, unsigned sz, bool isTempl = true); /** Has symmetry breaking lemmas been added for any enumerator? */ bool hasSymBreakLemmas(std::vector& enums) const; /** Get symmetry breaking lemmas @@ -188,6 +189,8 @@ class TermDbSygus { TypeNode getTypeForSymBreakLemma(Node lem) const; /** Get the minimum size of terms symmetry breaking lemma lem applies to */ unsigned getSizeForSymBreakLemma(Node lem) const; + /** Returns true if lem is a lemma template, false if lem is a lemma */ + bool isSymBreakLemmaTemplate(Node lem) const; /** Clear information about symmetry breaking lemmas for enumerator e */ void clearSymBreakLemmas(Node e); //------------------------------end enumerators @@ -344,6 +347,8 @@ class TermDbSygus { std::map d_sb_lemma_to_type; /** mapping from symmetry breaking lemmas to size */ std::map d_sb_lemma_to_size; + /** mapping from symmetry breaking lemmas to whether they are templates */ + std::map d_sb_lemma_to_isTempl; /** enumerators to whether they are actively-generated */ std::map d_enum_active_gen; /** enumerators to whether they are variable agnostic */