(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.

3 files changed, 24 insertions, 21 deletions

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 4a03637d0..e2d1fbb3e 100644
--- 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 334fdf596..b8fb71dd3 100644
--- 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 5ac8b8f7e..61980be3e 100644
--- 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,