}
}
-void SygusSymBreakNew::registerSizeTerm( Node e, std::vector< Node >& lemmas ) {
+void SygusSymBreakNew::registerSizeTerm(Node e, std::vector<Node>& lemmas)
+{
if (d_register_st.find(e) != d_register_st.end())
{
// already registered
{
// symmetry breaking lemmas should only be for enumerators
Assert(d_register_st[a]);
- std::vector<Node> 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<Node> 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())
}
// 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<Node> 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());
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<mts.size(); i++ ){
- registerSizeTerm( mts[i], lemmas );
+ Trace("sygus-sb") << "SygusSymBreakNew::check: finished." << std::endl;
+ if (needsRecheck)
+ {
+ Trace("sygus-sb") << " SygusSymBreakNew::rechecking..." << std::endl;
+ return check(lemmas);
}
- Trace("sygus-sb") << " SygusSymBreakNew::check: finished." << std::endl;
if (Trace.isOn("cegqi-engine") && !d_szinfo.empty())
{
void SygusEnumerator::initialize(Node e)
{
+ Trace("sygus-enum") << "SygusEnumerator::initialize " << e << std::endl;
d_enum = e;
d_etype = d_enum.getType();
+ Assert(d_etype.isDatatype());
+ Assert(d_etype.getDatatype().isSygus());
d_tlEnum = getMasterEnumForType(d_etype);
d_abortSize = options::sygusAbortSize();
+
+ // Get the statically registered symmetry breaking clauses for e, see if they
+ // can be used for speeding up the enumeration.
+ NodeManager* nm = NodeManager::currentNM();
+ std::vector<Node> 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<Node> 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)
}
}
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 : ";
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<Node, NodeHashFunction> d_sbExcTlCons;
+ //-------------------------------- end externally specified symmetry breaking
};
} // namespace quantifiers
{
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()
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;
}
}
}
}
-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<Node>& enums) const
return it->second;
}
+bool TermDbSygus::isSymBreakLemmaTemplate(Node lem) const
+{
+ std::map<Node, bool>::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
*
* 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<Node>& enums) const;
/** Get symmetry breaking lemmas
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
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;
+ /** mapping from symmetry breaking lemmas to whether they are templates */
+ std::map<Node, bool> d_sb_lemma_to_isTempl;
/** enumerators to whether they are actively-generated */
std::map<Node, bool> d_enum_active_gen;
/** enumerators to whether they are variable agnostic */
projects / cvc5.git / commitdiff