(proof-new) Minor updates to strings base solver (#4606)

In preparation for proofs, this PR involves flattening AND and removing spurious true literals in conjunctions.

This also updates our policy for applying cardinality, where in some rare cases we were applying cardinality for pairs of string terms for length 0 (e.g. "there is at most 1 eqc of length 0"), which is spurious due to our term registry which always splits on emptiness.

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 4a03637d0fa3e42aded3c1c9359bd53d7220fde1..e2d1fbb3ef02a7400f2d6b8372c425578e5b3c86 100644 (file)
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -27,11 +27,8 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-BaseSolver::BaseSolver(context::Context* c,
-                       context::UserContext* u,
-                       SolverState& s,
-                       InferenceManager& im)
-    : d_state(s), d_im(im), d_congruent(c)
+BaseSolver::BaseSolver(SolverState& s, InferenceManager& im)
+    : d_state(s), d_im(im), d_congruent(s.getSatContext())
 {
   d_false = NodeManager::currentNM()->mkConst(false);
   d_cardSize = utils::getAlphabetCardinality();
@@ -323,8 +320,10 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
               Node nrr = d_state.getRepresentative(n[count]);
               Assert(!d_eqcInfo[nrr].d_bestContent.isNull()
                      && d_eqcInfo[nrr].d_bestContent.isConst());
+              // must flatten to avoid nested AND in explanations
+              utils::flattenOp(AND, d_eqcInfo[nrr].d_exp, exp);
+              // now explain equality to base
               d_im.addToExplanation(n[count], d_eqcInfo[nrr].d_base, exp);
-              exp.push_back(d_eqcInfo[nrr].d_exp);
             }
             else
             {
@@ -353,9 +352,13 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
             Assert(!nct.isConst());
             bei.d_bestContent = nct;
             bei.d_base = n;
-            bei.d_exp = utils::mkAnd(exp);
+            if (!exp.empty())
+            {
+              bei.d_exp = utils::mkAnd(exp);
+            }
             Trace("strings-debug")
-                << "Set eqc best content " << n << " to " << nct << std::endl;
+                << "Set eqc best content " << n << " to " << nct
+                << ", explanation = " << bei.d_exp << std::endl;
           }
         }
       }
@@ -370,11 +373,12 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
         BaseEqcInfo& bei = d_eqcInfo[nr];
         if (!bei.d_bestContent.isConst())
         {
-          Trace("strings-debug")
-              << "Set eqc const " << n << " to " << c << std::endl;
           bei.d_bestContent = c;
           bei.d_base = n;
           bei.d_exp = utils::mkAnd(exp);
+          Trace("strings-debug")
+              << "Set eqc const " << n << " to " << c
+              << ", explanation = " << bei.d_exp << std::endl;
         }
         else if (c != bei.d_bestContent)
         {
@@ -487,8 +491,10 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
     else
     {
       // find the minimimum constant that we are unknown to be disequal from, or
-      // otherwise stop if we increment such that cardinality does not apply
-      unsigned r = 0;
+      // otherwise stop if we increment such that cardinality does not apply.
+      // We always start with r=1 since by the invariants of our term registry,
+      // a term is either equal to the empty string, or has length >= 1.
+      unsigned r = 1;
       bool success = true;
       while (r < card_need && success)
       {
@@ -545,8 +551,8 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
       Node k_node = nm->mkConst(Rational(int_k));
       // add cardinality lemma
       Node dist = nm->mkNode(DISTINCT, cols[i]);
-      std::vector<Node> vec_node;
-      vec_node.push_back(dist);
+      std::vector<Node> expn;
+      expn.push_back(dist);
       for (std::vector<Node>::iterator itr1 = cols[i].begin();
            itr1 != cols[i].end();
            ++itr1)
@@ -555,7 +561,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
         if (len != lr)
         {
           Node len_eq_lr = len.eqNode(lr);
-          vec_node.push_back(len_eq_lr);
+          expn.push_back(len_eq_lr);
         }
       }
       Node len = nm->mkNode(STRING_LENGTH, cols[i][0]);
@@ -566,7 +572,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
       {
         std::vector<Node> emptyVec;
         d_im.sendInference(
-            emptyVec, vec_node, cons, Inference::CARDINALITY, true);
+            emptyVec, expn, cons, Inference::CARDINALITY, true);
         return;
       }
     }

diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h
index 334fdf5966db4f16a5fa8145aa1eae2495da57cf..b8fb71dd3ff06b0cc4e96879b477c86fc3cbf3a5 100644 (file)
--- a/src/theory/strings/base_solver.h
+++ b/src/theory/strings/base_solver.h
@@ -41,10 +41,7 @@ class BaseSolver
   using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
 
  public:
-  BaseSolver(context::Context* c,
-             context::UserContext* u,
-             SolverState& s,
-             InferenceManager& im);
+  BaseSolver(SolverState& s, InferenceManager& im);
   ~BaseSolver();
 
   //-----------------------inference steps

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 5ac8b8f7e81ea2368e8fe234ce21894010d5e9bf..61980be3ea24553f626ce73a8c1b0bce5a8da49c 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -88,7 +88,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
   d_im.reset(
       new InferenceManager(c, u, d_state, d_termReg, *extt, out, d_statistics));
   // initialize the solvers
-  d_bsolver.reset(new BaseSolver(c, u, d_state, *d_im));
+  d_bsolver.reset(new BaseSolver(d_state, *d_im));
   d_csolver.reset(new CoreSolver(c, u, d_state, *d_im, d_termReg, *d_bsolver));
   d_esolver.reset(new ExtfSolver(c,
                                  u,