From 8a7e611fb40bb96faf85c1532fa778c47d83a899 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 6 Nov 2018 17:28:41 -0600 Subject: Incorporate static PBE symmetry breaking lemmas into SygusEnumerator (#2690) --- src/theory/quantifiers/sygus/sygus_pbe.cpp | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) (limited to 'src/theory/quantifiers/sygus/sygus_pbe.cpp') 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() -- cgit v1.2.3