From 3aae63919df61895d956f9cca5049bfac7980b9c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 28 Jun 2018 15:44:45 -0500 Subject: [PATCH] sygusComp2018: optimization for invariance test (#2104) --- .../quantifiers/sygus/sygus_invariance.cpp | 49 +++++++++++++++---- .../quantifiers/sygus/sygus_invariance.h | 30 ++++++++---- 2 files changed, 60 insertions(+), 19 deletions(-) diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index 4c638be0a..54a3cce50 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -27,7 +27,22 @@ namespace quantifiers { void EvalSygusInvarianceTest::init(Node conj, Node var, Node res) { - d_conj = conj; + d_terms.clear(); + // simple miniscope + if ((conj.getKind() == AND || conj.getKind() == OR) && res.isConst()) + { + for (const Node& c : conj) + { + d_terms.push_back(c); + } + d_kind = conj.getKind(); + d_is_conjunctive = res.getConst() == (d_kind == AND); + } + else + { + d_terms.push_back(conj); + d_is_conjunctive = true; + } d_var = var; d_result = res; } @@ -40,21 +55,35 @@ Node EvalSygusInvarianceTest::doEvaluateWithUnfolding(TermDbSygus* tds, Node n) bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) { TNode tnvn = nvn; - Node conj_subs = d_conj.substitute(d_var, tnvn); - Node conj_subs_unfold = doEvaluateWithUnfolding(tds, conj_subs); - Trace("sygus-cref-eval2-debug") - << " ...check unfolding : " << conj_subs_unfold << std::endl; - Trace("sygus-cref-eval2-debug") << " ......from : " << conj_subs - << std::endl; - if (conj_subs_unfold == d_result) + std::unordered_map cache; + for (const Node& c : d_terms) { + Node conj_subs = c.substitute(d_var, tnvn, cache); + Node conj_subs_unfold = doEvaluateWithUnfolding(tds, conj_subs); + Trace("sygus-cref-eval2-debug") + << " ...check unfolding : " << conj_subs_unfold << std::endl; + Trace("sygus-cref-eval2-debug") + << " ......from : " << conj_subs << std::endl; + if (conj_subs_unfold != d_result) + { + if (d_is_conjunctive) + { + // ti /--> true implies and( t1, ..., tn ) /--> true, where "/-->" is + // "does not evaluate to". + return false; + } + } + else if (!d_is_conjunctive) + { + // ti --> true implies or( t1, ..., tn ) --> true + return true; + } Trace("sygus-cref-eval2") << "Evaluation min explain : " << conj_subs << " still evaluates to " << d_result << " regardless of "; Trace("sygus-cref-eval2") << x << std::endl; - return true; } - return false; + return d_is_conjunctive; } void EquivSygusInvarianceTest::init( diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index 02bba55a1..9e3553a0b 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -97,30 +97,42 @@ class SygusInvarianceTest class EvalSygusInvarianceTest : public SygusInvarianceTest { public: - EvalSygusInvarianceTest() {} + EvalSygusInvarianceTest() : d_kind(kind::UNDEFINED_KIND) {} /** initialize this invariance test - * This sets d_conj/d_var/d_result, where - * we are checking whether: - * d_conj { d_var -> n } ----> d_result. - * for terms n. - */ + * + * This sets d_terms/d_var/d_result, where we are checking whether: + * (d_terms) { d_var -> n } ----> d_result. + * for terms n. + */ void init(Node conj, Node var, Node res); /** do evaluate with unfolding, using the cache of this class */ Node doEvaluateWithUnfolding(TermDbSygus* tds, Node n); protected: - /** does d_conj{ d_var -> nvn } still rewrite to d_result? */ + /** does d_terms{ d_var -> nvn } still rewrite to d_result? */ bool invariant(TermDbSygus* tds, Node nvn, Node x) override; private: - /** the formula we are evaluating */ - Node d_conj; + /** the formulas we are evaluating */ + std::vector d_terms; /** the variable */ TNode d_var; /** the result of the evaluation */ Node d_result; + /** the parent kind we are checking, undefined if size(d_terms) is 1. */ + Kind d_kind; + /** whether we are conjunctive + * + * If this flag is true, then the evaluation tests: + * d_terms[1] {d_var -> n} = d_result ... d_term[k] {d_var -> n} = d_result + * should be processed conjunctively, that is, + * (d_terms) { d_var -> n } = d_result only if each of the above + * holds. If this flag is false, then these tests are interpreted + * disjunctively, i.e. if one child test succeeds, the overall test succeeds. + */ + bool d_is_conjunctive; /** cache of n -> the simplified form of eval( n ) */ std::unordered_map d_visited; }; -- 2.30.2