diff options
| -rw-r--r-- | src/options/quantifiers_options.toml | 8 | ||||
| -rw-r--r-- | src/theory/quantifiers/extended_rewrite.cpp | 40 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_invariance.cpp | 36 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_invariance.h | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.cpp | 162 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.h | 5 |
6 files changed, 223 insertions, 32 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 3a77a4957..a2bbce1f8 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -968,6 +968,14 @@ header = "options/quantifiers_options.h" default = "false" read_only = true help = "abort if synthesis conjecture is not single invocation" + +[[option]] + name = "sygusExcInvPred" + category = "regular" + long = "sygus-exc-inv-pred" + type = "bool" + default = "false" + help = "Use exclusion invariance predicates" [[option]] name = "sygusUnif" diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index abaf608cc..4a082f2aa 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -1464,7 +1464,13 @@ bool ExtendedRewriter::inferSubstitution(Node n, Node v[2]; for (unsigned i = 0; i < 2; i++) { - if (n[i].isVar() || n[i].isConst()) + if( n[i].isConst() ) + { + vars.push_back(n[1-i]); + subs.push_back(n[i]); + return true; + } + if (n[i].isVar()) { v[i] = n[i]; } @@ -1832,6 +1838,38 @@ Node ExtendedRewriter::extendedRewriteBv(Node ret) } } } + else if( ck==BITVECTOR_CONCAT ) + { + // -concat( t, 1 ) ---> concat( ~t, 1 ) + // if its last bit is one + Node last_child = ret[0][ret[0].getNumChildren()-1]; + if( last_child.isConst() ) + { + if( bv::utils::getBit(last_child,0) ) + { + std::vector< Node > children; + for( unsigned j=0, size=ret[0].getNumChildren(); j<size-1; j++ ) + { + children.push_back(TermUtil::mkNegate(BITVECTOR_NOT,ret[0][j])); + } + unsigned size = bv::utils::getSize(last_child); + if( size>1 ) + { + Node extract = + bv::utils::mkExtract(last_child, size-1, 1); + extract = TermUtil::mkNegate(BITVECTOR_NOT,extract); + children.push_back(extract); + children.push_back(bv::utils::mkOnes(1)); + } + else + { + children.push_back(last_child); + } + new_ret = nm->mkNode(BITVECTOR_CONCAT,children); + debugExtendedRewrite(ret, new_ret, "NEG-odd"); + } + } + } else { new_ret = normalizeBvMonomial(ret); diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index f4aa07673..277a443c5 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -27,7 +27,19 @@ namespace quantifiers { void EvalSygusInvarianceTest::init(Node conj, Node var, Node res) { - d_conj = conj; + d_conj.clear(); + // simple miniscope + if( ( conj.getKind()==AND || conj.getKind()==OR ) && res.isConst() && res.getConst<bool>()==(conj.getKind()==AND) ) + { + for( const Node& c : conj ) + { + d_conj.push_back(c); + } + } + else + { + d_conj.push_back(conj); + } d_var = var; d_result = res; } @@ -40,21 +52,25 @@ 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<TNode, TNode, TNodeHashFunction> cache; + for( const Node& c : d_conj ) { + 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) + { + return false; + } 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 true; } void EquivSygusInvarianceTest::init( diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index 577923f5b..d9ff98c2a 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -115,8 +115,8 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest 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< Node > d_conj; /** the variable */ TNode d_var; /** the result of the evaluation */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 5e578d70b..dee9c6e4f 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_unif_io.h" #include "theory/datatypes/datatypes_rewriter.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "util/random.h" @@ -512,9 +513,35 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) << "...got res = " << res << " from " << bv << std::endl; base_results.push_back(res); } + // get the results for each slave enumerator + std::map<Node, std::vector< Node > > srmap; + for( const Node& xs : ei.d_enum_slave ) + { + Assert( srmap.find(xs)==srmap.end()); + EnumInfo& eiv = d_strategy[c].getEnumInfo(xs); + Node templ = eiv.d_template; + if( !templ.isNull() ) + { + TNode templ_var = eiv.d_template_arg; + std::vector< Node > sresults; + for( const Node& res : base_results ) + { + TNode tres = res; + Node sres = templ.substitute(templ_var,tres); + sresults.push_back(Rewriter::rewrite(sres)); + } + srmap[xs] = sresults; + } + else + { + srmap[xs] = base_results; + } + } + + // is it excluded for domain-specific reason? std::vector<Node> exp_exc_vec; - if (getExplanationForEnumeratorExclude(e, v, base_results, exp_exc_vec)) + if (getExplanationForEnumeratorExclude(e, v, base_results, srmap, true, exp_exc_vec)) { Assert(!exp_exc_vec.empty()); exp_exc = exp_exc_vec.size() == 1 @@ -531,11 +558,8 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) for (unsigned s = 0; s < ei.d_enum_slave.size(); s++) { Node xs = ei.d_enum_slave[s]; - EnumInfo& eiv = d_strategy[c].getEnumInfo(xs); - EnumCache& ecv = d_ecache[xs]; - Trace("sygus-sui-enum") << "Process " << xs << " from " << s << std::endl; // bool prevIsCover = false; if (eiv.getRole() == enum_io) @@ -550,20 +574,13 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) Trace("sygus-sui-enum") << xs << " : "; // evaluate all input/output examples std::vector<Node> results; - Node templ = eiv.d_template; - TNode templ_var = eiv.d_template_arg; std::map<Node, bool> cond_vals; - for (unsigned j = 0, size = base_results.size(); j < size; j++) + std::map<Node, std::vector< Node > >::iterator itsr = srmap.find(xs); + Assert( itsr!=srmap.end()); + for (unsigned j=0, size=itsr->second.size(); j<size; j++ ) { - Node res = base_results[j]; + Node res = itsr->second[j]; Assert(res.isConst()); - if (!templ.isNull()) - { - TNode tres = res; - res = templ.substitute(templ_var, res); - res = Rewriter::rewrite(res); - Assert(res.isConst()); - } Node resb; if (eiv.getRole() == enum_io) { @@ -672,8 +689,19 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) // exclude this value on subsequent iterations if (exp_exc.isNull()) { - // if we did not already explain why this should be excluded, use default - exp_exc = d_tds->getExplain()->getExplanationForEquality(e, v); + std::vector<Node> exp_exc_vec; + if (getExplanationForEnumeratorExclude(e, v, base_results, srmap, false, exp_exc_vec)) + { + Assert(!exp_exc_vec.empty()); + exp_exc = exp_exc_vec.size() == 1 + ? exp_exc_vec[0] + : NodeManager::currentNM()->mkNode(AND, exp_exc_vec); + } + else + { + // if we did not already explain why this should be excluded, use default + exp_exc = d_tds->getExplain()->getExplanationForEquality(e, v); + } } exp_exc = exp_exc.negate(); Trace("sygus-sui-enum-lemma") @@ -789,14 +817,93 @@ bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e) return false; } +Node SygusUnifIo::getExclusionInvariancePredicate(Node e, Node v, + std::map< Node, std::vector< Node > >& srmap, + bool prereg + ) +{ + if( prereg ) + { + return Node::null(); + } + Node c = d_candidate; + std::vector< Node > conj; + NodeManager* nm = NodeManager::currentNM(); + //if (useStrContainsEnumeratorExclude(e)) + //{ + //} + bool invariant_eval_role = true; + EnumInfo& ei = d_strategy[c].getEnumInfo(e); + for (const Node& sn : ei.d_enum_slave) + { + EnumInfo& eis = d_strategy[c].getEnumInfo(sn); + EnumRole er = eis.getRole(); + if( er!=enum_io && er!=enum_ite_condition ) + { + invariant_eval_role = false; + break; + } + } + if( invariant_eval_role ) + { + for (const Node& sn : ei.d_enum_slave) + { + EnumInfo& eis = d_strategy[c].getEnumInfo(sn); + EnumRole er = eis.getRole(); + Node templ = eis.d_template; + TNode templ_var = eis.d_template_arg; + // get the results + std::vector< Node >& sresults = srmap[sn]; + Assert( d_examples_out.size()==sresults.size() ); + + for( unsigned j=0, size = sresults.size(); j<size; j++ ) + { + std::vector< Node > echildren; + echildren.push_back(e); + echildren.insert(echildren.end(),d_examples[j].begin(),d_examples[j].end()); + Node dte = nm->mkNode( DT_SYGUS_EVAL, echildren ); + if( !templ.isNull() ) + { + dte = templ.substitute(templ_var,dte); + } + Assert( sresults[j].isConst() ); + if( er==enum_io ) + { + // it is being used as i/o, we must maintain the false examples + if( sresults[j]!=d_examples_out[j] ) + { + conj.push_back(dte.eqNode(d_examples_out[j]).negate()); + } + } + else if( er==enum_ite_condition ) + { + // must remain the same evaluation + Assert( dte.getType().isBoolean() ); + conj.push_back( sresults[j].getConst<bool>() ? dte : dte.negate() ); + } + } + } + } + if( !conj.empty() ) + { + Node eip = conj.size()==1 ? conj[0] : nm->mkNode( AND, conj ); + Trace("sygus-io-eip") << "Exclusion invariance predicate for " << v << " is : " << eip << std::endl; + return eip; + } + + return Node::null(); +} + bool SygusUnifIo::getExplanationForEnumeratorExclude(Node e, Node v, std::vector<Node>& results, + std::map< Node, std::vector< Node > >& srmap, + bool prereg, std::vector<Node>& exp) { - if (useStrContainsEnumeratorExclude(e)) + NodeManager* nm = NodeManager::currentNM(); + if (prereg && useStrContainsEnumeratorExclude(e)) { - NodeManager* nm = NodeManager::currentNM(); // This check whether the example evaluates to something that is larger than // the output for some input/output pair. If so, then this term is never // useful. We generalize its explanation below. @@ -842,6 +949,23 @@ bool SygusUnifIo::getExplanationForEnumeratorExclude(Node e, return true; } } + if( options::sygusExcInvPred() ) + { + Node pred = getExclusionInvariancePredicate(e,v, srmap, prereg); + if( !pred.isNull() ) + { + EvalSygusInvarianceTest esit; + esit.init(pred,e,nm->mkConst(true)); + // construct the generalized explanation + d_tds->getExplain()->getExplanationFor(e, v, exp, esit); + std::vector< Node > triv_exp; + d_tds->getExplain()->getExplanationForEquality(e, v, triv_exp); + Trace("sygus-io-eip2") + << "Generalized explanation of " << d_tds->sygusToBuiltin(v) + << ": " << exp.size() << "/" << triv_exp.size() << std::endl; + return true; + } + } return false; } diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 0aca9ebe2..f7faab389 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -412,7 +412,12 @@ class SygusUnifIo : public SygusUnif bool getExplanationForEnumeratorExclude(Node e, Node v, std::vector<Node>& results, + std::map< Node, std::vector< Node > >& srmap, + bool prereg, std::vector<Node>& exp); + Node getExclusionInvariancePredicate(Node e, Node v, + std::map< Node, std::vector< Node > >& srmap, + bool prereg); /** returns true if we can exlude values of e based on negative str.contains * * Values v for e may be excluded if we realize that the value of v under the |