From: Andrew Reynolds Date: Fri, 19 Jun 2020 22:40:18 +0000 (-0500) Subject: (proof-new) Updates to strings term registry (#4599) X-Git-Tag: cvc5-1.0.0~3192 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a517757f04e519259dde9ed7309168e7475354e3;p=cvc5.git (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. --- 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 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 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()) - { - // 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()); } - 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& 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 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 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),