diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-19 17:40:18 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-19 17:40:18 -0500 |
commit | a517757f04e519259dde9ed7309168e7475354e3 (patch) | |
tree | 504775b98d19c878e5ec77119c623b006f5a6378 /src/theory | |
parent | 22780596b561dff9b0eb5b0620252280a678944e (diff) |
(proof-new) Updates to strings term registry (#4599)
This makes it so that methods for constructing term registration lemmas are made into static methods, so that they can be used by both the term registry and proof checker.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/term_registry.cpp | 137 | ||||
-rw-r--r-- | src/theory/strings/term_registry.h | 35 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 2 |
3 files changed, 118 insertions, 56 deletions
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 90ebc4f8b..b4fbbed98 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -15,6 +15,7 @@ #include "theory/strings/term_registry.h" #include "expr/attribute.h" +#include "options/smt_options.h" #include "options/strings_options.h" #include "smt/logic_exception.h" #include "theory/rewriter.h" @@ -35,23 +36,25 @@ struct StringsProxyVarAttributeId typedef expr::Attribute<StringsProxyVarAttributeId, bool> StringsProxyVarAttribute; -TermRegistry::TermRegistry(context::Context* c, - context::UserContext* u, +TermRegistry::TermRegistry(SolverState& s, eq::EqualityEngine& ee, OutputChannel& out, - SequencesStatistics& statistics) - : d_ee(ee), + SequencesStatistics& statistics, + ProofNodeManager* pnm) + : d_state(s), + d_ee(ee), d_out(out), d_statistics(statistics), d_hasStrCode(false), - d_functionsTerms(c), - d_inputVars(u), - d_preregisteredTerms(u), - d_registeredTerms(u), - d_registeredTypes(u), - d_proxyVar(u), - d_proxyVarToLength(u), - d_lengthLemmaTermsCache(u) + d_functionsTerms(s.getSatContext()), + d_inputVars(s.getUserContext()), + d_preregisteredTerms(s.getUserContext()), + d_registeredTerms(s.getUserContext()), + d_registeredTypes(s.getUserContext()), + d_proxyVar(s.getUserContext()), + d_proxyVarToLength(s.getUserContext()), + d_lengthLemmaTermsCache(s.getUserContext()), + d_epg(nullptr) { NodeManager* nm = NodeManager::currentNM(); d_zero = nm->mkConst(Rational(0)); @@ -62,6 +65,64 @@ TermRegistry::TermRegistry(context::Context* c, TermRegistry::~TermRegistry() {} +Node TermRegistry::eagerReduce(Node t, SkolemCache* sc) +{ + NodeManager* nm = NodeManager::currentNM(); + Node lemma; + Kind tk = t.getKind(); + if (tk == STRING_TO_CODE) + { + // ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 ) + Node code_len = utils::mkNLength(t[0]).eqNode(nm->mkConst(Rational(1))); + Node code_eq_neg1 = t.eqNode(nm->mkConst(Rational(-1))); + Node code_range = nm->mkNode( + AND, + nm->mkNode(GEQ, t, nm->mkConst(Rational(0))), + nm->mkNode( + LT, t, nm->mkConst(Rational(utils::getAlphabetCardinality())))); + lemma = nm->mkNode(ITE, code_len, code_range, code_eq_neg1); + } + else if (tk == STRING_STRIDOF) + { + // (and (>= (str.indexof x y n) (- 1)) (<= (str.indexof x y n) (str.len + // x))) + Node l = utils::mkNLength(t[0]); + lemma = nm->mkNode(AND, + nm->mkNode(GEQ, t, nm->mkConst(Rational(-1))), + nm->mkNode(LEQ, t, l)); + } + else if (tk == STRING_STOI) + { + // (>= (str.to_int x) (- 1)) + lemma = nm->mkNode(GEQ, t, nm->mkConst(Rational(-1))); + } + else if (tk == STRING_STRCTN) + { + // ite( (str.contains s r), (= s (str.++ sk1 r sk2)), (not (= s r))) + Node sk1 = + sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_PRE, "sc1"); + Node sk2 = + sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_POST, "sc2"); + lemma = t[0].eqNode(utils::mkNConcat(sk1, t[1], sk2)); + lemma = nm->mkNode(ITE, t, lemma, t[0].eqNode(t[1]).notNode()); + } + return lemma; +} + +Node TermRegistry::lengthPositive(Node t) +{ + NodeManager* nm = NodeManager::currentNM(); + Node zero = nm->mkConst(Rational(0)); + Node emp = Word::mkEmptyWord(t.getType()); + Node tlen = nm->mkNode(STRING_LENGTH, t); + Node tlenEqZero = tlen.eqNode(zero); + Node tEqEmp = t.eqNode(emp); + Node caseEmpty = nm->mkNode(AND, tlenEqZero, tEqEmp); + Node caseNEmpty = nm->mkNode(GT, tlen, zero); + // (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0)) + return nm->mkNode(OR, caseEmpty, caseNEmpty); +} + void TermRegistry::preRegisterTerm(TNode n) { if (d_preregisteredTerms.find(n) != d_preregisteredTerms.end()) @@ -202,7 +263,6 @@ void TermRegistry::registerTerm(Node n, int effort) d_registeredTerms.insert(n); // ensure the type is registered registerType(tn); - NodeManager* nm = NodeManager::currentNM(); Debug("strings-register") << "TheoryStrings::registerTerm() " << n << ", effort = " << effort << std::endl; Node regTermLem; @@ -213,28 +273,10 @@ void TermRegistry::registerTerm(Node n, int effort) // for concat/const/replace, introduce proxy var and state length relation regTermLem = getRegisterTermLemma(n); } - else if (n.getKind() == STRING_TO_CODE) - { - // ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 ) - Node code_len = utils::mkNLength(n[0]).eqNode(d_one); - Node code_eq_neg1 = n.eqNode(d_negOne); - Node code_range = nm->mkNode( - AND, - nm->mkNode(GEQ, n, d_zero), - nm->mkNode( - LT, n, nm->mkConst(Rational(utils::getAlphabetCardinality())))); - regTermLem = nm->mkNode(ITE, code_len, code_range, code_eq_neg1); - } - else if (n.getKind() == STRING_STRIDOF) + else if (n.getKind() != STRING_STRCTN) { - Node len = utils::mkNLength(n[0]); - regTermLem = nm->mkNode(AND, - nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))), - nm->mkNode(LEQ, n, len)); - } - else if (n.getKind() == STRING_STOI) - { - regTermLem = nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))); + // we don't send out eager reduction lemma for str.contains currently + regTermLem = eagerReduce(n, &d_skCache); } if (!regTermLem.isNull()) { @@ -324,7 +366,9 @@ Node TermRegistry::getRegisterTermLemma(Node n) d_proxyVarToLength[sk] = lsum; Node ceq = Rewriter::rewrite(skl.eqNode(lsum)); - return nm->mkNode(AND, eq, ceq); + Node ret = nm->mkNode(AND, eq, ceq); + + return ret; } void TermRegistry::registerTermAtomic(Node n, LengthStatus s) @@ -407,17 +451,15 @@ Node TermRegistry::getRegisterTermAtomicLemma(Node n, } Assert(s == LENGTH_SPLIT); - std::vector<Node> lems; + // get the positive length lemma + Node lenLemma = lengthPositive(n); // split whether the string is empty Node n_len_eq_z = n_len.eqNode(d_zero); Node n_len_eq_z_2 = n.eqNode(emp); Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2); - case_empty = Rewriter::rewrite(case_empty); - Node case_nempty = nm->mkNode(GT, n_len, d_zero); - if (!case_empty.isConst()) + Node case_emptyr = Rewriter::rewrite(case_empty); + if (!case_emptyr.isConst()) { - Node lem = nm->mkNode(OR, case_empty, case_nempty); - lems.push_back(lem); // prefer trying the empty case first // notice that requirePhase must only be called on rewritten literals that // occur in the CNF stream. @@ -428,24 +470,15 @@ Node TermRegistry::getRegisterTermAtomicLemma(Node n, Assert(!n_len_eq_z_2.isConst()); reqPhase[n_len_eq_z_2] = true; } - else if (!case_empty.getConst<bool>()) - { - // the rewriter knows that n is non-empty - lems.push_back(case_nempty); - } else { // If n = "" ---> true or len( n ) = 0 ----> true, then we expect that // n ---> "". Since this method is only called on non-constants n, it must // be that n = "" ^ len( n ) = 0 does not rewrite to true. - Assert(false); + Assert(!case_emptyr.getConst<bool>()); } - if (lems.empty()) - { - return Node::null(); - } - return lems.size() == 1 ? lems[0] : nm->mkNode(AND, lems); + return lenLemma; } Node TermRegistry::getSymbolicDefinition(Node n, std::vector<Node>& exp) const diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index f0b4a74c6..d0589be90 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -19,10 +19,13 @@ #include "context/cdhashset.h" #include "context/cdlist.h" +#include "expr/proof_node_manager.h" +#include "theory/eager_proof_generator.h" #include "theory/output_channel.h" #include "theory/strings/infer_info.h" #include "theory/strings/sequences_stats.h" #include "theory/strings/skolem_cache.h" +#include "theory/strings/solver_state.h" #include "theory/uf/equality_engine.h" namespace CVC4 { @@ -46,12 +49,34 @@ class TermRegistry typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; public: - TermRegistry(context::Context* c, - context::UserContext* u, + TermRegistry(SolverState& s, eq::EqualityEngine& ee, OutputChannel& out, - SequencesStatistics& statistics); + SequencesStatistics& statistics, + ProofNodeManager* pnm); ~TermRegistry(); + /** The eager reduce routine + * + * Constructs a lemma for t that is incomplete, but communicates pertinent + * information about t. This is analogous to StringsPreprocess::reduce. + * + * In practice, we send this lemma eagerly, as soon as t is registered. + * + * @param t The node to reduce, + * @param sc The Skolem cache to use for new variables, + * @return The eager reduction for t. + */ + static Node eagerReduce(Node t, SkolemCache* sc); + /** + * Returns a lemma indicating that the length of a term t whose type is + * string-like has positive length. The exact form of this lemma depends + * on what works best in practice, currently: + * (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0)) + * + * @param t The node to reduce, + * @return The positive length lemma for t. + */ + static Node lengthPositive(Node t); /** * Preregister term, called when TheoryStrings::preRegisterTerm(n) is called. * This does the following: @@ -184,6 +209,8 @@ class TermRegistry Node d_negOne; /** the cardinality of the alphabet */ uint32_t d_cardSize; + /** Reference to the solver state of the theory of strings. */ + SolverState& d_state; /** Reference to equality engine of the theory of strings. */ eq::EqualityEngine& d_ee; /** Reference to the output channel of the theory of strings. */ @@ -224,6 +251,8 @@ class TermRegistry NodeNodeMap d_proxyVarToLength; /** List of terms that we have register length for */ NodeSet d_lengthLemmaTermsCache; + /** Proof generator, manages proofs for lemmas generated by this class */ + std::unique_ptr<EagerProofGenerator> d_epg; /** Register type * * Ensures the theory solver is setup to handle string-like type tn. In diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 562d8eab8..ae8b3b682 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -44,7 +44,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_statistics(), d_equalityEngine(d_notify, c, "theory::strings::ee", true), d_state(c, u, d_equalityEngine, d_valuation), - d_termReg(c, u, d_equalityEngine, out, d_statistics), + d_termReg(d_state, d_equalityEngine, out, d_statistics, nullptr), d_im(nullptr), d_rewriter(&d_statistics.d_rewrites), d_bsolver(nullptr), |