Skip `str.code` inferences for sequence eqcs (#7644)

Fixes cvc5/cvc5-projects#340. Type checking
failed because cvc5 was trying to construct a term (str.to_code (seq.unit false)). We do not allow the construction of terms
(str.to_code t) where t is not of type string. This commit fixes the
issue by skipping sequence equivalence classes when doing inferences
related to str.to_code.

Note that the regression test is slightly different from the original
unit test. It asserts that the index passed to seq.nth is
non-negative, which ensures that we can check the resulting model. I
have checked that the modified regression test triggers the issue before
the change in this commit.

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 69d41e9d7c82520df8768546f77a9aced914cb98..69d50a7d98ef0b8ff4527dacdb1d540b82b23758 100644 (file)
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -46,7 +46,7 @@ void BaseSolver::checkInit()
   // build term index
   d_eqcInfo.clear();
   d_termIndex.clear();
-  d_stringsEqc.clear();
+  d_stringLikeEqc.clear();
 
   Trace("strings-base") << "BaseSolver::checkInit" << std::endl;
   // count of congruent, non-congruent per operator (independent of type),
@@ -65,7 +65,7 @@ void BaseSolver::checkInit()
       std::map<Kind, TermIndex>& tti = d_termIndex[tn];
       if (tn.isStringLike())
       {
-        d_stringsEqc.push_back(eqc);
+        d_stringLikeEqc.push_back(eqc);
         emps = Word::mkEmptyWord(tn);
       }
       Node var;
@@ -512,7 +512,7 @@ void BaseSolver::checkCardinality()
   // between lengths of string terms that are disequal (DEQ-LENGTH-SP).
   std::map<TypeNode, std::vector<std::vector<Node> > > cols;
   std::map<TypeNode, std::vector<Node> > lts;
-  d_state.separateByLength(d_stringsEqc, cols, lts);
+  d_state.separateByLength(d_stringLikeEqc, cols, lts);
   for (std::pair<const TypeNode, std::vector<std::vector<Node> > >& c : cols)
   {
     checkCardinalityType(c.first, c.second, lts[c.first]);
@@ -759,9 +759,9 @@ Node BaseSolver::explainBestContentEqc(Node n, Node eqc, std::vector<Node>& exp)
   return Node::null();
 }
 
-const std::vector<Node>& BaseSolver::getStringEqc() const
+const std::vector<Node>& BaseSolver::getStringLikeEqc() const
 {
-  return d_stringsEqc;
+  return d_stringLikeEqc;
 }
 
 Node BaseSolver::TermIndex::add(TNode n,

diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h
index bf61b93b24a86264c7b6e6f44996e44f1cff11c4..96d275cd52d485d46082ea51877f30288d8ae690 100644 (file)
--- a/src/theory/strings/base_solver.h
+++ b/src/theory/strings/base_solver.h
@@ -106,7 +106,7 @@ class BaseSolver : protected EnvObj
   /**
    * Get the set of equivalence classes of type string.
    */
-  const std::vector<Node>& getStringEqc() const;
+  const std::vector<Node>& getStringLikeEqc() const;
   //-----------------------end query functions
 
  private:
@@ -236,8 +236,8 @@ class BaseSolver : protected EnvObj
    * for more information.
    */
   std::map<Node, BaseEqcInfo> d_eqcInfo;
-  /** The list of equivalence classes of type string */
-  std::vector<Node> d_stringsEqc;
+  /** The list of equivalence classes of string-like types */
+  std::vector<Node> d_stringLikeEqc;
   /** A term index for each type, function kind pair */
   std::map<TypeNode, std::map<Kind, TermIndex> > d_termIndex;
   /** the cardinality of the alphabet */

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index cc9365d38a2834b345a1a1ac9e612205005a9435..46f75bd10c724db24738112e3259e1fdfa70d646 100644 (file)
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -131,7 +131,7 @@ void CoreSolver::checkCycles()
   d_eqc.clear();
   // Rebuild strings eqc based on acyclic ordering, first copy the equivalence
   // classes from the base solver.
-  const std::vector<Node>& eqc = d_bsolver.getStringEqc();
+  const std::vector<Node>& eqc = d_bsolver.getStringLikeEqc();
   d_strings_eqc.clear();
   for (const Node& r : eqc)
   {

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 8324e3edbd488287c4c17b372aebd1366cfac6a7..ed00758a85730e41a47370ce96afaacfb156b08d 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -877,7 +877,7 @@ void TheoryStrings::computeCareGraph(){
 
 void TheoryStrings::checkRegisterTermsPreNormalForm()
 {
-  const std::vector<Node>& seqc = d_bsolver.getStringEqc();
+  const std::vector<Node>& seqc = d_bsolver.getStringLikeEqc();
   for (const Node& eqc : seqc)
   {
     eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
@@ -906,9 +906,14 @@ void TheoryStrings::checkCodes()
     // str.code applied to the proxy variables for each equivalence classes that
     // are constants of size one
     std::vector<Node> const_codes;
-    const std::vector<Node>& seqc = d_bsolver.getStringEqc();
+    const std::vector<Node>& seqc = d_bsolver.getStringLikeEqc();
     for (const Node& eqc : seqc)
     {
+      if (!eqc.getType().isString())
+      {
+        continue;
+      }
+
       NormalForm& nfe = d_csolver.getNormalForm(eqc);
       if (nfe.d_nf.size() == 1 && nfe.d_nf[0].isConst())
       {
@@ -972,7 +977,7 @@ void TheoryStrings::checkCodes()
 
 void TheoryStrings::checkRegisterTermsNormalForms()
 {
-  const std::vector<Node>& seqc = d_bsolver.getStringEqc();
+  const std::vector<Node>& seqc = d_bsolver.getStringLikeEqc();
   for (const Node& eqc : seqc)
   {
     NormalForm& nfi = d_csolver.getNormalForm(eqc);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4937c8481ac9d2f1974772db1a79d4061defbef0..bffb3e8cb55181f9a19d133944cc924df5d25b6d 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1087,6 +1087,7 @@ set(regress_0_tests
   regress0/seq/issue5665-invalid-model.smt2
   regress0/seq/issue6337-seq.smt2
   regress0/seq/len_simplify.smt2
+  regress0/seq/proj-issue340.smt2
   regress0/seq/seq-2var.smt2
   regress0/seq/seq-ex1.smt2
   regress0/seq/seq-ex2.smt2

diff --git a/test/regress/regress0/seq/proj-issue340.smt2 b/test/regress/regress0/seq/proj-issue340.smt2
new file mode 100644 (file)
index 0000000..75a4fb3
--- /dev/null
+++ b/test/regress/regress0/seq/proj-issue340.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_SLIA)
+(declare-const x0 Bool)
+(declare-const x2 (Seq Bool))
+(declare-const i Int)
+(assert (= i (str.to_int (str.from_code (seq.len x2)))))
+(assert (not (seq.nth x2 i)))
+(assert (>= i 0))
+(set-info :status sat)
+(check-sat)