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.

diff --git a/src/theory/strings/array_solver.cpp b/src/theory/strings/array_solver.cpp
index cc844b229f800214d87b87898af9061c9210e654..867a91caefbfb6c74bd395f567a574f768f5d75d 100644 (file)
--- 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<Node> 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<Node> nthTerms = d_esolver.getActive(SEQ_NTH);
-  std::vector<Node> updateTerms = d_esolver.getActive(STRING_UPDATE);
+  // get the set of relevant terms, for reasons described above
+  std::set<Node> termSet;
+  d_termReg.getRelevantTermSet(termSet);
+  std::vector<Node> nthTerms;
+  std::vector<Node> 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<Node>& 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<Node> 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 c129f48373363b0f5ab19d481e8fe05e306579b9..39293720bca767a158db370c70137eb4efd7a48a 100644 (file)
--- 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<Node, Node>& 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<Node>& 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 d648a9287d5502f1c6e55d695e3bdb33813b7a1e..fff869c7d8a124b062f9221d6459d04de3f93fe3 100644 (file)
--- 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<Node>& unproc) const
   }
 }
 
+void TermRegistry::getRelevantTermSet(std::set<Node>& 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 338e528fecf79c587e2d4abec0d855efbe3c522a..5dd038ad35a2f42cf9a75a8330fa9568e099ff9c 100644 (file)
--- 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<Node>& c, TypeNode tn) const;
 
+  /** compute relevant terms of the theory of strings */
+  void getRelevantTermSet(std::set<Node>& 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 f4833ca11e26d02800e5c264d869a485ab405cb6..b14621f0744139b6ad0718fcbb1e248e33bb36f8 100644 (file)
--- 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 9d925f97ca789a26735ef108d74c95d40c587507..3cdb878dfc80206244825409ac2bea523fe7c511 100644 (file)
--- 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 (file)
index 0000000..25f7ffc
--- /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)