From 2a19474cdb6761fd4c9aeb0165e661c531ba3e38 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 2 Dec 2018 08:49:17 -0600 Subject: [PATCH] Optimizations for PBE strings (#2728) --- .../quantifiers/sygus/sygus_invariance.cpp | 19 ++- .../quantifiers/sygus/sygus_invariance.h | 16 +- .../quantifiers/sygus/sygus_unif_io.cpp | 142 +++++++++++++++--- src/theory/quantifiers/sygus/sygus_unif_io.h | 25 ++- 4 files changed, 168 insertions(+), 34 deletions(-) diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index 24b47b216..5ea01ef57 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -218,15 +218,22 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, out, nbvre); Trace("sygus-pbe-cterm-debug") << "Check: " << cont << std::endl; Node contr = Rewriter::rewrite(cont); - if (contr == tds->d_false) + if (!contr.isConst()) + { + if (d_isUniversal) + { + return false; + } + } + else if (contr.getConst() == d_isUniversal) { if (Trace.isOn("sygus-pbe-cterm")) { Trace("sygus-pbe-cterm") << "PBE-cterm : enumerator : do not consider "; - Trace("sygus-pbe-cterm") << nbv << " for any " - << tds->sygusToBuiltin(x) << " since " - << std::endl; + Trace("sygus-pbe-cterm") + << nbv << " for any " << tds->sygusToBuiltin(x) << " since " + << std::endl; Trace("sygus-pbe-cterm") << " PBE-cterm : for input example : "; for (unsigned j = 0, size = d_ex[ii].size(); j < size; j++) { @@ -238,13 +245,13 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, Trace("sygus-pbe-cterm") << " PBE-cterm : and is not in output : " << out << std::endl; } - return true; + return !d_isUniversal; } Trace("sygus-pbe-cterm-debug2") << "...check failed, rewrites to : " << contr << std::endl; } } - return false; + return d_isUniversal; } } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index 59761da5c..02c249411 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -249,7 +249,7 @@ class DivByZeroSygusInvarianceTest : public SygusInvarianceTest class NegContainsSygusInvarianceTest : public SygusInvarianceTest { public: - NegContainsSygusInvarianceTest() {} + NegContainsSygusInvarianceTest() : d_isUniversal(false) {} /** initialize this invariance test * e is the enumerator which we are reasoning about (associated with a synth @@ -266,9 +266,19 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest std::vector >& ex, std::vector& exo, std::vector& ncind); + /** set universal + * + * This updates the semantics of this check such that *all* instead of some + * examples must fail the containment test. + */ + void setUniversal() { d_isUniversal = true; } protected: - /** checks if contains( out_i, nvn[in_i] ) --> false for some I/O pair i. */ + /** + * Checks if contains( out_i, nvn[in_i] ) --> false for some I/O pair i; if + * d_isUniversal is true, then we check if the rewrite holds for *all* I/O + * pairs. + */ bool invariant(TermDbSygus* tds, Node nvn, Node x) override; private: @@ -282,6 +292,8 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest * contains( out_i, nvn[in_i] ) ---> false */ std::vector d_neg_con_indices; + /** requires not being in all examples */ + bool d_isUniversal; }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 89619639d..a6e6b54c6 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -431,10 +431,13 @@ void SubsumeTrie::getLeavesInternal(const std::vector& vals, { if (index == vals.size()) { + // by convention, if we did not test any points, then we consider the + // evaluation along the current path to be always false. + int rstatus = status == -2 ? -1 : status; Assert(!d_term.isNull()); - Assert(std::find(v[status].begin(), v[status].end(), d_term) - == v[status].end()); - v[status].push_back(d_term); + Assert(std::find(v[rstatus].begin(), v[rstatus].end(), d_term) + == v[rstatus].end()); + v[rstatus].push_back(d_term); } else { @@ -806,9 +809,13 @@ Node SygusUnifIo::constructSolutionNode(std::vector& lemmas) || (!d_solution.isNull() && d_tds->getSygusTermSize(vcc) < d_sol_term_size))) { - Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = " << vcc - << std::endl; - Trace("sygus-pbe") << "...solved at iteration " << i << std::endl; + if (Trace.isOn("sygus-pbe")) + { + Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = "; + TermDbSygus::toStreamSygus("sygus-pbe", vcc); + Trace("sygus-pbe") << std::endl; + Trace("sygus-pbe") << "...solved at iteration " << i << std::endl; + } d_solution = vcc; newSolution = vcc; d_sol_term_size = d_tds->getSygusTermSize(vcc); @@ -867,12 +874,12 @@ bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e) d_use_str_contains_eexc[e] = false; return false; } + d_use_str_contains_eexc_conditional[e] = false; if (eis.isConditional()) { Trace("sygus-sui-enum-debug") << " conditional slave : " << sn << std::endl; - d_use_str_contains_eexc[e] = false; - return false; + d_use_str_contains_eexc_conditional[e] = true; } } Trace("sygus-sui-enum-debug") @@ -895,6 +902,9 @@ bool SygusUnifIo::getExplanationForEnumeratorExclude( // the output for some input/output pair. If so, then this term is never // useful. We generalize its explanation below. + // if the enumerator is in a conditional context, then we are stricter + // about when to exclude + bool isConditional = d_use_str_contains_eexc_conditional[e]; if (Trace.isOn("sygus-sui-cterm-debug")) { Trace("sygus-sui-enum") << std::endl; @@ -921,12 +931,20 @@ bool SygusUnifIo::getExplanationForEnumeratorExclude( else { Trace("sygus-sui-cterm-debug") << "...contained." << std::endl; + if (isConditional) + { + return false; + } } } if (!cmp_indices.empty()) { // we check invariance with respect to a negative contains test NegContainsSygusInvarianceTest ncset; + if (isConditional) + { + ncset.setUniversal(); + } ncset.init(e, d_examples, d_examples_out, cmp_indices); // construct the generalized explanation d_tds->getExplain()->getExplanationFor(e, v, exp, ncset); @@ -992,10 +1010,12 @@ Node SygusUnifIo::constructSol( EnumCache& ecache = d_ecache[e]; + bool retValMod = x.isReturnValueModified(); + Node ret_dt; if (nrole == role_equal) { - if (!x.isReturnValueModified()) + if (!retValMod) { if (ecache.isSolved()) { @@ -1069,11 +1089,67 @@ Node SygusUnifIo::constructSol( } } } + // maybe we can find one in the cache + if (ret_dt.isNull() && !retValMod) + { + bool firstTime = true; + std::unordered_set intersection; + std::map>::iterator + pit; + for (size_t i = 0, nvals = x.d_vals.size(); i < nvals; i++) + { + if (x.d_vals[i].getConst()) + { + pit = d_psolutions.find(i); + if (pit == d_psolutions.end()) + { + // no cached solution + intersection.clear(); + break; + } + if (firstTime) + { + intersection = pit->second; + firstTime = false; + } + else + { + std::vector rm; + for (const Node& a : intersection) + { + if (pit->second.find(a) == pit->second.end()) + { + rm.push_back(a); + } + } + for (const Node& a : rm) + { + intersection.erase(a); + } + if (intersection.empty()) + { + break; + } + } + } + } + if (!intersection.empty()) + { + ret_dt = *intersection.begin(); + if (Trace.isOn("sygus-sui-dt")) + { + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") << "ConstructPBE: found in cache: "; + TermDbSygus::toStreamSygus("sygus-sui-dt", ret_dt); + Trace("sygus-sui-dt") << std::endl; + } + } + } } else if (nrole == role_string_prefix || nrole == role_string_suffix) { // check if each return value is a prefix/suffix of all open examples - if (!x.isReturnValueModified() || x.getCurrentRole() == nrole) + if (!retValMod || x.getCurrentRole() == nrole) { std::map > incr; bool isPrefix = nrole == role_string_prefix; @@ -1264,11 +1340,12 @@ Node SygusUnifIo::constructSol( Assert(set_split_cond_res_index); Assert(split_cond_res_index < ecache_cond.d_enum_vals_res.size()); prev = x.d_vals; - bool ret = x.updateContext( - this, - ecache_cond.d_enum_vals_res[split_cond_res_index], - sc == 1); - AlwaysAssert(ret); + x.updateContext(this, + ecache_cond.d_enum_vals_res[split_cond_res_index], + sc == 1); + // return value of above call may be false in corner cases where we + // must choose a non-separating condition to traverse to another + // strategy node } // recurse @@ -1284,7 +1361,7 @@ Node SygusUnifIo::constructSol( std::map solved_cond; // stores branch ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond); - std::map >::iterator itpc = + std::map>::iterator itpc = possible_cond.find(0); if (itpc != possible_cond.end()) { @@ -1301,8 +1378,6 @@ Node SygusUnifIo::constructSol( << d_tds->sygusToBuiltin(cond) << std::endl; } } - - // otherwise, guess a conditional if (rec_c.isNull()) { rec_c = constructBestConditional(ce, itpc->second); @@ -1381,8 +1456,35 @@ Node SygusUnifIo::constructSol( } Assert(ret_dt.isNull() || ret_dt.getType() == e.getType()); - indent("sygus-sui-dt", ind); - Trace("sygus-sui-dt") << "ConstructPBE: returned " << ret_dt << std::endl; + if (Trace.isOn("sygus-sui-dt")) + { + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") << "ConstructPBE: returned "; + TermDbSygus::toStreamSygus("sygus-sui-dt", ret_dt); + Trace("sygus-sui-dt") << std::endl; + } + // remember the solution + if (nrole == role_equal) + { + if (!retValMod && !ret_dt.isNull()) + { + for (size_t i = 0, nvals = x.d_vals.size(); i < nvals; i++) + { + if (x.d_vals[i].getConst()) + { + if (Trace.isOn("sygus-sui-cache")) + { + indent("sygus-sui-cache", ind); + Trace("sygus-sui-cache") << "Cache solution (#" << i << ") : "; + TermDbSygus::toStreamSygus("sygus-sui-cache", ret_dt); + Trace("sygus-sui-cache") << std::endl; + } + d_psolutions[i].insert(ret_dt); + } + } + } + } + return ret_dt; } diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 2f87c0552..f189353b0 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -183,12 +183,14 @@ class SubsumeTrie bool pol, std::vector& subsumed_by); /** - * Get the leaves of the trie, which we store in the map v. - * v[-1] stores the children that always evaluate to !pol, - * v[1] stores the children that always evaluate to pol, - * v[0] stores the children that both evaluate to true and false for at least - * one example. - */ + * Get the leaves of the trie, which we store in the map v. We consider their + * evaluation on points such that (pol ? vals : !vals) is true. + * + * v[-1] stores the children that always evaluate to !pol, + * v[1] stores the children that always evaluate to pol, + * v[0] stores the children that both evaluate to true and false for at least + * one example. + */ void getLeaves(const std::vector& vals, bool pol, std::map>& v); @@ -300,6 +302,11 @@ class SygusUnifIo : public SygusUnif Node d_solution; /** the term size of the above solution */ unsigned d_sol_term_size; + /** partial solutions + * + * Maps indices for I/O points to a list of solutions for that point. + */ + std::map> d_psolutions; /** * This flag is set to true if the solution construction was * non-deterministic with respect to failure/success. @@ -427,6 +434,12 @@ class SygusUnifIo : public SygusUnif bool useStrContainsEnumeratorExclude(Node e); /** cache for the above function */ std::map d_use_str_contains_eexc; + /** + * cache for the above function, stores whether enumerators e are in + * a conditional context, e.g. used for enumerating the return values for + * leaves of ITE trees. + */ + std::map d_use_str_contains_eexc_conditional; /** the unification context used within constructSolution */ UnifContextIo d_context; -- 2.30.2