Connect sequences array solver to strategy in theory of strings (#7847)

Also corrects an issue with model construction, where SEQ_NTH should be assignable in addition to SEQ_NTH_TOTAL.

seqArray branch (which has regressions) can be merged to master after this PR.

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 52b0a6907f095ea9c02d2eb7bcb6fa9da3f4100b..07105a311e8d048243a2bbee485d8e3c1eade825 100644 (file)
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -16,6 +16,7 @@
 #include "theory/strings/extf_solver.h"
 
 #include "options/strings_options.h"
+#include "theory/strings/array_solver.h"
 #include "theory/strings/sequences_rewriter.h"
 #include "theory/strings/theory_strings_preprocess.h"
 #include "theory/strings/theory_strings_utils.h"
@@ -157,10 +158,28 @@ bool ExtfSolver::doReduction(int effort, Node n)
     // asserted (pol=0).
     return false;
   }
-  else if (effort != 2)
+  else
   {
-    // all other operators reduce at level 2
-    return false;
+    if (options().strings.seqArray != options::SeqArrayMode::NONE)
+    {
+      if (k == SEQ_NTH)
+      {
+        // don't need to reduce seq.nth when sequence update solver is used
+        return false;
+      }
+      else if ((k == STRING_UPDATE || k == STRING_SUBSTR)
+               && d_termReg.isHandledUpdate(n))
+      {
+        // don't need to reduce certain seq.update
+        // don't need to reduce certain seq.extract with length 1
+        return false;
+      }
+    }
+    if (effort != 2)
+    {
+      // all other operators reduce at level 2
+      return false;
+    }
   }
   Node c_n = pol == -1 ? n.negate() : n;
   Trace("strings-process-debug")

diff --git a/src/theory/strings/strategy.cpp b/src/theory/strings/strategy.cpp
index 921a676d77ca05a5f5c54f919b1ab78598d6805d..f5472210404cdfc3eea459391f5cfce0fcfac862 100644 (file)
--- a/src/theory/strings/strategy.cpp
+++ b/src/theory/strings/strategy.cpp
@@ -38,6 +38,13 @@ std::ostream& operator<<(std::ostream& out, InferStep s)
     case CHECK_EXTF_REDUCTION: out << "check_extf_reduction"; break;
     case CHECK_MEMBERSHIP: out << "check_membership"; break;
     case CHECK_CARDINALITY: out << "check_cardinality"; break;
+    case CHECK_SEQUENCES_ARRAY_CONCAT:
+      out << "check_sequences_update_concat_terms";
+      break;
+    case CHECK_SEQUENCES_ARRAY: out << "check_sequences_array"; break;
+    case CHECK_SEQUENCES_ARRAY_EAGER:
+      out << "check_sequences_array_eager";
+      break;
     default: out << "?"; break;
   }
   return out;
@@ -101,6 +108,10 @@ void Strategy::initializeStrategy()
     addStrategyStep(CHECK_INIT);
     addStrategyStep(CHECK_CONST_EQC);
     addStrategyStep(CHECK_EXTF_EVAL, 0);
+    if (options().strings.seqArray == options::SeqArrayMode::EAGER)
+    {
+      addStrategyStep(CHECK_SEQUENCES_ARRAY_EAGER);
+    }
     // we must check cycles before using flat forms
     addStrategyStep(CHECK_CYCLES);
     if (options().strings.stringFlatForms)
@@ -130,6 +141,11 @@ void Strategy::initializeStrategy()
     {
       addStrategyStep(CHECK_LENGTH_EQC);
     }
+    if (options().strings.seqArray != options::SeqArrayMode::NONE)
+    {
+      addStrategyStep(CHECK_SEQUENCES_ARRAY_CONCAT);
+      addStrategyStep(CHECK_SEQUENCES_ARRAY);
+    }
     if (options().strings.stringExp)
     {
       addStrategyStep(CHECK_EXTF_REDUCTION, 2);

diff --git a/src/theory/strings/strategy.h b/src/theory/strings/strategy.h
index 48253c64ae302ced5c8a7542b162798918e76037..e87372c0f681b91e38ca99f6ca62e60db48b0cc9 100644 (file)
--- a/src/theory/strings/strategy.h
+++ b/src/theory/strings/strategy.h
@@ -65,6 +65,12 @@ enum InferStep
   CHECK_MEMBERSHIP,
   // check cardinality
   CHECK_CARDINALITY,
+  // check sequence updates wrt concat
+  CHECK_SEQUENCES_ARRAY_CONCAT,
+  // check sequence array-like reasoning
+  CHECK_SEQUENCES_ARRAY,
+  // check sequence
+  CHECK_SEQUENCES_ARRAY_EAGER,
 };
 std::ostream& operator<<(std::ostream& out, InferStep i);
 

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 6f19a5aaf35597d4017a5abcf9e766e6d159f978..fdc743915c1848318c4efd9f354bc0c2f47b996a 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1264,6 +1264,9 @@ void TheoryStrings::runInferStep(InferStep s, int effort)
     case CHECK_NORMAL_FORMS_DEQ: d_csolver.checkNormalFormsDeq(); break;
     case CHECK_CODES: checkCodes(); break;
     case CHECK_LENGTH_EQC: d_csolver.checkLengthsEqc(); break;
+    case CHECK_SEQUENCES_ARRAY_CONCAT: d_asolver.checkArrayConcat(); break;
+    case CHECK_SEQUENCES_ARRAY: d_asolver.checkArray(); break;
+    case CHECK_SEQUENCES_ARRAY_EAGER: d_asolver.checkArrayEager(); break;
     case CHECK_REGISTER_TERMS_NF: checkRegisterTermsNormalForms(); break;
     case CHECK_EXTF_REDUCTION: d_esolver.checkExtfReductions(effort); break;
     case CHECK_MEMBERSHIP: d_rsolver.checkMemberships(effort); break;

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 96e86e482414c361bb61f47a59c176f86963971c..6a083b7e330a3ffdb68de6d503f5d7e83171c67c 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -60,6 +60,7 @@ void TheoryModel::finishInit(eq::EqualityEngine* ee)
   d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR);
   d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
   d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
+  d_equalityEngine->addFunctionKind(kind::SEQ_NTH);
   d_equalityEngine->addFunctionKind(kind::SEQ_NTH_TOTAL);
   // do not interpret APPLY_UF if we are not assigning function values
   if (!d_enableFuncModels)

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index f80cf515931020adf2d4e786ecb5b011983a0d4b..06b82afd1be6f8ddfba1d147d9a1e99c14ebdeae 100644 (file)
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -133,7 +133,7 @@ bool TheoryEngineModelBuilder::isValue(TNode n)
 bool TheoryEngineModelBuilder::isAssignable(TNode n)
 {
   if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL
-      || n.getKind() == kind::SEQ_NTH_TOTAL)
+      || n.getKind() == kind::SEQ_NTH_TOTAL || n.getKind() == kind::SEQ_NTH)
   {
     // selectors are always assignable (where we guarantee that they are not
     // evaluatable here)