diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-06 17:28:41 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-11-06 17:28:41 -0600 |
commit | 8a7e611fb40bb96faf85c1532fa778c47d83a899 (patch) | |
tree | e9f2b98b15e64c810d323118e530e9cbeff58b26 /src/theory/quantifiers/sygus/sygus_pbe.cpp | |
parent | 2ef5f132c1169cbeadd580638cbc35b6e454d6a5 (diff) |
Incorporate static PBE symmetry breaking lemmas into SygusEnumerator (#2690)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_pbe.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 15 |
1 files changed, 13 insertions, 2 deletions
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() |