Unify checker for constant split

2 files changed, 31 insertions, 53 deletions

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index f9f4a064f..a95c9b5f7 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -717,6 +717,7 @@ Node CoreSolver::getConclusion(Node x,
   Trace("strings-csolver") << "CoreSolver::getConclusion: " << x << " " << y
                            << " " << rule << " " << isRev << std::endl;
   NodeManager* nm = NodeManager::currentNM();
+  Node conc;
   if (rule == PfRule::CONCAT_SPLIT || rule == PfRule::CONCAT_LPROP)
   {
     Node sk1;
@@ -757,7 +758,6 @@ Node CoreSolver::getConclusion(Node x,
         x.eqNode(isRev ? utils::mkNConcat(sk1, y) : utils::mkNConcat(y, sk1));
     // eq1 = nm->mkNode(AND, eq1, nm->mkNode(GEQ, sk1, d_one));
 
-    Node conc;
     if (rule == PfRule::CONCAT_LPROP)
     {
       conc = eq1;
@@ -775,13 +775,27 @@ Node CoreSolver::getConclusion(Node x,
       // we can assume its length is greater than zero
       Node emp = Word::mkEmptyWord(sk1.getType());
       conc = nm->mkNode(AND, conc, sk1.eqNode(emp).negate(),
-    nm->mkNode(GT,nm->mkNode(STRING_LENGTH,sk1), nm->mkConst(Rational(0))));
+      nm->mkNode(GT,nm->mkNode(STRING_LENGTH,sk1), nm->mkConst(Rational(0))));
     }
     */
-    return conc;
+  }
+  else if (rule==PfRule::CONCAT_CSPLIT)
+  {
+    Assert (y.isConst());
+    size_t yLen = Word::getLength(y);
+    Node firstChar = yLen == 1 ? y
+                                  : (isRev ? Word::suffix(y, 1)
+                                            : Word::prefix(y, 1));
+    Node sk = skc->mkSkolemCached(
+        x,
+        isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT,
+        "c_spt");
+    newSkolems.push_back(sk);
+    conc = x.eqNode(isRev ? utils::mkNConcat(sk, firstChar)
+                          : utils::mkNConcat(firstChar, sk));
   }
 
-  return Node::null();
+  return conc;
 }
 
 void CoreSolver::getNormalForms(Node eqc,
@@ -1530,25 +1544,14 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       // to start with the first character of the constant.
       //
       // E.g. "abc" ++ ... = nc ++ ... ---> nc = "a" ++ k
-      Node stra = nfcv[index];
-      size_t straLen = Word::getLength(stra);
-      Node firstChar = straLen == 1 ? stra
-                                    : (isRev ? Word::suffix(stra, 1)
-                                             : Word::prefix(stra, 1));
       SkolemCache* skc = d_termReg.getSkolemCache();
-      Node sk = skc->mkSkolemCached(
-          nc,
-          isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT,
-          "c_spt");
-      Trace("strings-csp") << "Const Split: " << firstChar
-                           << " is removed from " << stra << " (serial) "
-                           << std::endl;
+      std::vector<Node> newSkolems;
+      iinfo.d_conc = getConclusion(nc,nfcv[index],PfRule::CONCAT_CSPLIT,isRev,skc,newSkolems);
       NormalForm::getExplanationForPrefixEq(
           nfi, nfj, index, index, iinfo.d_ant);
       iinfo.d_ant.push_back(expNonEmpty);
-      iinfo.d_conc = nc.eqNode(isRev ? utils::mkNConcat(sk, firstChar)
-                                     : utils::mkNConcat(firstChar, sk));
-      iinfo.d_new_skolem[LENGTH_SPLIT].push_back(sk);
+      Assert(newSkolems.size()==1);
+      iinfo.d_new_skolem[LENGTH_SPLIT].push_back(newSkolems[0]);
       iinfo.d_id = Inference::SSPLIT_CST;
       iinfo.d_idRev = isRev;
       pinfer.push_back(info);
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index b7cbf6037..a5a22dfa0 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -198,15 +198,6 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
       {
         return Node::null();
       }
-      // use skolem cache
-      SkolemCache skc(false);
-      std::vector<Node> newSkolems;
-      Node kt0 = ProofSkolemCache::getSkolemForm(t0);
-      Node ks0 = ProofSkolemCache::getSkolemForm(s0);
-      Node conc = CoreSolver::getConclusion(
-          kt0, ks0, PfRule::CONCAT_SPLIT, isRev, &skc, newSkolems);
-      conc = ProofSkolemCache::getWitnessForm(conc);
-      return conc;
     }
     else if (id == PfRule::CONCAT_CSPLIT)
     {
@@ -223,22 +214,6 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
       {
         return Node::null();
       }
-      Node c = isRev ? Word::suffix(s0, 1) : Word::prefix(s0, 1);
-      Node rbody =
-          isRev ? utils::mkPrefix(
-                      t0, nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, t0), one))
-                : utils::mkSuffix(t0, one);
-      Node r = ProofSkolemCache::mkPurifySkolem(rbody, "r");
-      Node conc;
-      if (isRev)
-      {
-        conc = t0.eqNode(nm->mkNode(STRING_CONCAT, r, c));
-      }
-      else
-      {
-        conc = t0.eqNode(nm->mkNode(STRING_CONCAT, c, r));
-      }
-      return conc;
     }
     else if (id == PfRule::CONCAT_LPROP)
     {
@@ -251,15 +226,6 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
       {
         return Node::null();
       }
-      // use skolem cache
-      SkolemCache skc(false);
-      std::vector<Node> newSkolems;
-      Node kt0 = ProofSkolemCache::getSkolemForm(t0);
-      Node ks0 = ProofSkolemCache::getSkolemForm(s0);
-      Node conc = CoreSolver::getConclusion(
-          kt0, ks0, PfRule::CONCAT_LPROP, isRev, &skc, newSkolems);
-      conc = ProofSkolemCache::getWitnessForm(conc);
-      return conc;
     }
     else if (id == PfRule::CONCAT_CPROP)
     {
@@ -336,6 +302,15 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
       }
       return conc;
     }
+    // use skolem cache
+    SkolemCache skc(false);
+    std::vector<Node> newSkolems;
+    Node kt0 = ProofSkolemCache::getSkolemForm(t0);
+    Node ks0 = ProofSkolemCache::getSkolemForm(s0);
+    Node conc = CoreSolver::getConclusion(
+        kt0, ks0, id, isRev, &skc, newSkolems);
+    conc = ProofSkolemCache::getWitnessForm(conc);
+    return conc;
   }
   else if (id == PfRule::CTN_NOT_EQUAL)
   {