From a657bb589acc5b994b911e6f48b413e85aee6bc1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 15 Feb 2022 18:59:33 -0600 Subject: [PATCH] Only consider relevant terms in the array-inspired sequence solver (#8105) Avoids segfault in model construction due to asking for the value of irrelevant (non-shared) term. --- src/theory/strings/array_solver.cpp | 38 ++++++++++++++----- src/theory/strings/array_solver.h | 4 +- src/theory/strings/term_registry.cpp | 19 ++++++++-- src/theory/strings/term_registry.h | 9 +++++ src/theory/strings/theory_strings.cpp | 2 +- test/regress/CMakeLists.txt | 1 + .../seq/shared-term-registration.smt2 | 23 +++++++++++ 7 files changed, 80 insertions(+), 16 deletions(-) create mode 100644 test/regress/regress0/seq/shared-term-registration.smt2 diff --git a/src/theory/strings/array_solver.cpp b/src/theory/strings/array_solver.cpp index cc844b229..867a91cae 100644 --- a/src/theory/strings/array_solver.cpp +++ b/src/theory/strings/array_solver.cpp @@ -60,8 +60,11 @@ void ArraySolver::checkArrayConcat() } d_currTerms.clear(); Trace("seq-array") << "ArraySolver::checkArrayConcat..." << std::endl; - checkTerms(STRING_UPDATE); - checkTerms(SEQ_NTH); + // Get the set of relevant terms. The core array solver requires knowing this + // set to ensure its write model is only over relevant terms. + std::set termSet; + d_termReg.getRelevantTermSet(termSet); + checkTerms(termSet); } void ArraySolver::checkArray() @@ -85,21 +88,34 @@ void ArraySolver::checkArrayEager() return; } Trace("seq-array") << "ArraySolver::checkArray..." << std::endl; - std::vector nthTerms = d_esolver.getActive(SEQ_NTH); - std::vector updateTerms = d_esolver.getActive(STRING_UPDATE); + // get the set of relevant terms, for reasons described above + std::set termSet; + d_termReg.getRelevantTermSet(termSet); + std::vector nthTerms; + std::vector updateTerms; + for (const Node& n : termSet) + { + Kind k = n.getKind(); + if (k == STRING_UPDATE) + { + updateTerms.push_back(n); + } + else if (k == SEQ_NTH) + { + nthTerms.push_back(n); + } + } d_coreSolver.check(nthTerms, updateTerms); } -void ArraySolver::checkTerms(Kind k) +void ArraySolver::checkTerms(const std::set& termSet) { - Assert(k == STRING_UPDATE || k == SEQ_NTH); // get all the active update terms that have not been reduced in the // current context by context-dependent simplification - std::vector terms = d_esolver.getActive(k); - for (const Node& t : terms) + for (const Node& t : termSet) { + Kind k = t.getKind(); Trace("seq-array-debug") << "check term " << t << "..." << std::endl; - Assert(t.getKind() == k); if (k == STRING_UPDATE) { if (!d_termReg.isHandledUpdate(t)) @@ -111,6 +127,10 @@ void ArraySolver::checkTerms(Kind k) // for update terms, also check the inverse inference checkTerm(t, true); } + else if (k != SEQ_NTH) + { + continue; + } // check the normal inference checkTerm(t, false); } diff --git a/src/theory/strings/array_solver.h b/src/theory/strings/array_solver.h index c129f4837..39293720b 100644 --- a/src/theory/strings/array_solver.h +++ b/src/theory/strings/array_solver.h @@ -83,8 +83,8 @@ class ArraySolver : protected EnvObj const std::map& getConnectedSequences(); private: - /** check terms of given kind */ - void checkTerms(Kind k); + /** check terms of nth or update kind that occur in termSet */ + void checkTerms(const std::set& termSet); /** check inferences for the given term * * @param t the term to check diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index d648a9287..fff869c7d 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -23,6 +23,7 @@ #include "theory/strings/inference_manager.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "theory/theory.h" #include "util/rational.h" #include "util/string.h" @@ -35,10 +36,12 @@ namespace theory { namespace strings { TermRegistry::TermRegistry(Env& env, + Theory& t, SolverState& s, SequencesStatistics& statistics, ProofNodeManager* pnm) : EnvObj(env), + d_theory(t), d_state(s), d_im(nullptr), d_statistics(statistics), @@ -54,10 +57,11 @@ TermRegistry::TermRegistry(Env& env, d_proxyVar(userContext()), d_proxyVarToLength(userContext()), d_lengthLemmaTermsCache(userContext()), - d_epg( - pnm ? new EagerProofGenerator( - pnm, userContext(), "strings::TermRegistry::EagerProofGenerator") - : nullptr) + d_epg(pnm ? new EagerProofGenerator( + pnm, + userContext(), + "strings::TermRegistry::EagerProofGenerator") + : nullptr) { NodeManager* nm = NodeManager::currentNM(); d_zero = nm->mkConstInt(Rational(0)); @@ -670,6 +674,13 @@ void TermRegistry::removeProxyEqs(Node n, std::vector& unproc) const } } +void TermRegistry::getRelevantTermSet(std::set& termSet) +{ + d_theory.collectAssertedTerms(termSet); + // also, get the additionally relevant terms + d_theory.computeRelevantTerms(termSet); +} + Node TermRegistry::mkNConcat(Node n1, Node n2) const { return rewrite(NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2)); diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index 338e528fe..5dd038ad3 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -33,6 +33,9 @@ namespace cvc5 { namespace theory { + +class Theory; + namespace strings { class InferenceManager; @@ -54,6 +57,7 @@ class TermRegistry : protected EnvObj public: TermRegistry(Env& env, + Theory& t, SolverState& s, SequencesStatistics& statistics, ProofNodeManager* pnm); @@ -229,7 +233,12 @@ class TermRegistry : protected EnvObj */ Node mkNConcat(const std::vector& c, TypeNode tn) const; + /** compute relevant terms of the theory of strings */ + void getRelevantTermSet(std::set& termSet); + private: + /** Reference to theory of strings, for computing relevant terms */ + Theory& d_theory; /** Common constants */ Node d_zero; Node d_one; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index f4833ca11..b14621f07 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -55,7 +55,7 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_notify(*this), d_statistics(), d_state(env, d_valuation), - d_termReg(env, d_state, d_statistics, d_pnm), + d_termReg(env, *this, d_state, d_statistics, d_pnm), d_rewriter(env.getRewriter(), &d_statistics.d_rewrites, d_termReg.getAlphabetCardinality()), diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 9d925f97c..3cdb878df 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1153,6 +1153,7 @@ set(regress_0_tests regress0/seq/seq-nth.smt2 regress0/seq/seq-rewrites.smt2 regress0/seq/seq-types.smt2 + regress0/seq/shared-term-registration.smt2 regress0/seq/update-concat-non-atomic.smt2 regress0/seq/update-concat-non-atomic2.smt2 regress0/seq/update-eq.smt2 diff --git a/test/regress/regress0/seq/shared-term-registration.smt2 b/test/regress/regress0/seq/shared-term-registration.smt2 new file mode 100644 index 000000000..25f7ffcca --- /dev/null +++ b/test/regress/regress0/seq/shared-term-registration.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --strings-exp --seq-array=lazy +; EXPECT: unknown +(set-logic ALL) +(declare-sort T@$ 0) +(declare-sort |T@[| 0) +(declare-sort T 0) +(declare-sort T@ 0) +(declare-datatypes ((@ 0)) ((($1 (l Int))))) +(declare-datatypes (($1 0)) ((($1 (v (Seq @)))))) +(declare-datatypes ((@$ 0)) ((($1 (p $1))))) +(declare-datatypes ((M 0)) (((M (c T@))))) +(declare-datatypes ((E 0)) (((T)))) +(declare-datatypes ((@M 0)) (((M (|#| T))))) +(declare-datatypes (($E 0)) ((($E (s |T@[|))))) +(declare-fun S (|T@[| T@$) @M) +(declare-fun S (T E) Int) +(declare-fun |1| () M) +(declare-fun S (T@ Int) @$) +(declare-fun $ () Int) +(declare-fun e () $E) +(declare-fun t () Bool) +(assert (not (=> (and (forall ((h T@$)) (and (forall ((v E)) (= 0 (S (|#| (S (s e) h)) T)))))) (< 0 (seq.len (v (p (S (c |1|) 1))))) (and t (= 0 (l (seq.nth (v (p (S (c |1|) 1))) $))))))) +(check-sat) -- 2.30.2