More fixes

4 files changed, 101 insertions, 46 deletions

diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index aacb8f5dd..8e53827d5 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -317,6 +317,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     if (res1.isNull() || res1 != res2)
     {
       Trace("builtin-pfcheck") << "Failed to match results" << std::endl;
+      Trace("builtin-pfcheck-debug") <<  res1 << " vs " << res2 << std::endl;
       return Node::null();
     }
     return args[0];
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index f0d470655..9f09dd7f2 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1436,7 +1436,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
             Trace("strings-entail")
                 << "  explanation was : " << et.second << std::endl;
             lentTestSuccess = e;
-            lenConstraint = et.second;
+            lenConstraint = entLit;//et.second;
             // its not explained by the equality engine of this class
             iinfo.d_noExplain.push_back(lenConstraint);
             break;
@@ -1458,6 +1458,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
 
     NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, iinfo.d_ant);
     // Add premises for x != "" ^ y != ""
+    // TODO: necessary?
+    /*
     for (unsigned xory = 0; xory < 2; xory++)
     {
       Node t = xory == 0 ? x : y;
@@ -1473,13 +1475,17 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
         iinfo.d_noExplain.push_back(tnz);
       }
     }
+    */
     SkolemCache* skc = d_termReg.getSkolemCache();
     Node sk1;
     Node sk2;
-    if (options::stringUnifiedVSpt())
+    if (options::stringUnifiedVSpt() && lentTestSuccess == -1)
     {
-      Node sk = skc->mkSkolemCached(x,
-                                    y,
+      // must order so that we cache in a deterministic way
+      Node ux = x<y ? x : y;
+      Node uy = x<y ? y : x;
+      Node sk = skc->mkSkolemCached(ux,
+                                    uy,
                                     isRev ? SkolemCache::SK_ID_V_UNIFIED_SPT_REV
                                           : SkolemCache::SK_ID_V_UNIFIED_SPT,
                                     "v_spt");
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index ed83d396b..77b8dbcb7 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -327,22 +327,20 @@ Node InferProofCons::convert(Inference infer,
         utils::getConcat(mainEqCeq[1], svec);
         Node t0 = tvec[isRev ? tvec.size() - 1 : 0];
         Node s0 = svec[isRev ? svec.size() - 1 : 0];
+        bool applySym = false;
         // may need to apply symmetry
         if ((infer == Inference::SSPLIT_CST
              || infer == Inference::SSPLIT_CST_PROP)
             && t0.isConst())
         {
           Assert(!s0.isConst());
-          std::vector<Node> childrenSymm;
-          childrenSymm.push_back(mainEqCeq);
-          mainEqCeq = d_psb.tryStep(PfRule::SYMM, childrenSymm, emptyVec);
-          Trace("strings-ipc-core")
-              << "Main equality after SYMM " << mainEqCeq << std::endl;
+          applySym = true;
           std::swap(t0, s0);
         }
         PfRule rule = PfRule::UNKNOWN;
         // the form of the required length constraint expected by the proof
         Node lenReq;
+        bool lenSuccess = false;
         if (infer == Inference::N_UNIFY || infer == Inference::F_UNIFY)
         {
           // the required premise for unify is always len(x) = len(y),
@@ -351,6 +349,7 @@ Node InferProofCons::convert(Inference infer,
           // it should be the case that lenConstraint => lenReq
           lenReq = nm->mkNode(STRING_LENGTH, t0)
                        .eqNode(nm->mkNode(STRING_LENGTH, s0));
+          lenSuccess = convertLengthPf(lenReq, lenConstraint);
           rule = PfRule::CONCAT_UNIFY;
         }
         else if (infer == Inference::SSPLIT_VAR)
@@ -358,6 +357,7 @@ Node InferProofCons::convert(Inference infer,
           // it should be the case that lenConstraint => lenReq
           lenReq = nm->mkNode(STRING_LENGTH, t0)
                        .eqNode(nm->mkNode(STRING_LENGTH, s0));
+          lenSuccess = convertLengthPf(lenReq, lenConstraint);
           rule = PfRule::CONCAT_SPLIT;
         }
         else if (infer == Inference::SSPLIT_CST)
@@ -366,13 +366,28 @@ Node InferProofCons::convert(Inference infer,
           lenReq = nm->mkNode(STRING_LENGTH, t0)
                        .eqNode(nm->mkConst(Rational(0)))
                        .notNode();
+          lenSuccess = convertLengthPf(lenReq, lenConstraint);
           rule = PfRule::CONCAT_CSPLIT;
         }
         else if (infer == Inference::SSPLIT_VAR_PROP)
         {
           // it should be the case that lenConstraint => lenReq
-          lenReq = nm->mkNode(
-              GT, nm->mkNode(STRING_LENGTH, t0), nm->mkNode(STRING_LENGTH, s0));
+          for (unsigned r=0; r<2; r++)
+          {
+            lenReq = nm->mkNode(
+                GT, nm->mkNode(STRING_LENGTH, t0), nm->mkNode(STRING_LENGTH, s0));
+            if (convertLengthPf(lenReq, lenConstraint))
+            {
+              lenSuccess = true;
+              break;
+            }
+            if (r==0)
+            {
+              // may be the other direction
+              applySym = true;
+              std::swap(t0, s0);
+            }
+          }
           rule = PfRule::CONCAT_LPROP;
         }
         else if (infer == Inference::SSPLIT_CST_PROP)
@@ -381,14 +396,29 @@ Node InferProofCons::convert(Inference infer,
           lenReq = nm->mkNode(STRING_LENGTH, t0)
                        .eqNode(nm->mkConst(Rational(0)))
                        .notNode();
+          lenSuccess = convertLengthPf(lenReq, lenConstraint);
           rule = PfRule::CONCAT_CPROP;
         }
+        if (!lenSuccess)
+        {
+          Trace("strings-ipc-core")
+              << "...failed due to length constraint" << std::endl;
+          break;
+        }
+        // apply symmetry if necessary
+        if (applySym)
+        {
+          std::vector<Node> childrenSymm;
+          childrenSymm.push_back(mainEqCeq);
+          // TODO: this explicit step may not be necessary
+          mainEqCeq = d_psb.tryStep(PfRule::SYMM, childrenSymm, emptyVec);
+          Trace("strings-ipc-core")
+              << "Main equality after SYMM " << mainEqCeq << std::endl;
+        }
         if (rule != PfRule::UNKNOWN)
         {
           Trace("strings-ipc-core")
               << "Core rule length requirement is " << lenReq << std::endl;
-          // must verify it
-          bool lenSuccess = convertLengthPf(lenReq, lenConstraint);
           // apply the given rule
           std::vector<Node> childrenMain;
           childrenMain.push_back(mainEqCeq);
@@ -404,15 +434,13 @@ Node InferProofCons::convert(Inference infer,
           if (convertPredTransform(mainEqMain, conc, cexp))
           {
             // requires that length success is also true
-            useBuffer = lenSuccess;
-            Trace("strings-ipc-core") << "...success";
+            useBuffer = true;
+            Trace("strings-ipc-core") << "...success" << std::endl;
           }
           else
           {
-            Trace("strings-ipc-core") << "...fail";
+            Trace("strings-ipc-core") << "...fail" << std::endl;
           }
-          Trace("strings-ipc-core")
-              << ", length success = " << lenSuccess << std::endl;
         }
         else
         {
@@ -796,24 +824,27 @@ bool InferProofCons::convertLengthPf(Node lenReq,
   }
   Trace("strings-ipc-len") << "Must explain " << lenReq << " by " << lenExp
                            << std::endl;
-  if (lenExp.size() == 1)
+  for (const Node& le : lenExp)
   {
     // probably rewrites to it?
     std::vector<Node> exp;
-    if (convertPredTransform(lenExp[0], lenReq, exp))
+    if (convertPredTransform(le, lenReq, exp))
     {
+      Trace("strings-ipc-len") << "...success by rewrite" << std::endl;
       return true;
     }
     // maybe x != "" => len(x) != 0
     std::vector<Node> children;
-    children.push_back(lenExp[0]);
+    children.push_back(le);
     std::vector<Node> args;
     Node res = d_psb.tryStep(PfRule::LENGTH_NON_EMPTY, children, args);
     if (res == lenReq)
     {
+      Trace("strings-ipc-len") << "...success by LENGTH_NON_EMPTY" << std::endl;
       return true;
     }
   }
+  Trace("strings-ipc-len") << "...failed" << std::endl;
   return false;
 }
 
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index 6de596309..c482556c4 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -20,6 +20,7 @@
 #include "theory/strings/theory_strings_preprocess.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
+#include "options/strings_options.h"
 
 using namespace CVC4::kind;
 
@@ -178,20 +179,31 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
       {
         return Node::null();
       }
-      Node rbodyt =
-          isRev ? utils::mkPrefix(t0,
-                                  nm->mkNode(MINUS,
-                                             nm->mkNode(STRING_LENGTH, t0),
-                                             nm->mkNode(STRING_LENGTH, s0)))
-                : utils::mkSuffix(t0, nm->mkNode(STRING_LENGTH, s0));
-      Node rbodys =
-          isRev ? utils::mkPrefix(s0,
-                                  nm->mkNode(MINUS,
-                                             nm->mkNode(STRING_LENGTH, s0),
-                                             nm->mkNode(STRING_LENGTH, t0)))
-                : utils::mkSuffix(s0, nm->mkNode(STRING_LENGTH, t0));
-      Node rt = ProofSkolemCache::mkPurifySkolem(rbodyt, "rt");
-      Node rs = ProofSkolemCache::mkPurifySkolem(rbodys, "rs");
+      SkolemCache skc(false);
+      Node rt;
+      Node rs;
+      if (options::stringUnifiedVSpt())
+      {
+        Node kt0 = ProofSkolemCache::getSkolemForm(t0);
+        Node ks0 = ProofSkolemCache::getSkolemForm(s0);
+        Node ut = kt0<ks0 ? kt0 : ks0;
+        Node us = kt0<ks0 ? ks0 : kt0;
+        // use unified version?
+        Node r = skc.mkSkolemCached(t0,
+                                    s0,
+                                    isRev ? SkolemCache::SK_ID_V_UNIFIED_SPT_REV
+                                          : SkolemCache::SK_ID_V_UNIFIED_SPT,
+                                    "r");
+        r = ProofSkolemCache::getWitnessForm(r);
+        rt = r;
+        rs = r;
+      }
+      else
+      {
+        // FIXME?
+        return Node::null();
+      }
+      
       Node conc;
       if (isRev)
       {
@@ -250,21 +262,22 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
       {
         return Node::null();
       }
-      Node rbody =
-          isRev ? utils::mkPrefix(t0,
-                                  nm->mkNode(MINUS,
-                                             nm->mkNode(STRING_LENGTH, t0),
-                                             nm->mkNode(STRING_LENGTH, s0)))
-                : utils::mkSuffix(t0, nm->mkNode(STRING_LENGTH, s0));
-      Node r = ProofSkolemCache::mkPurifySkolem(rbody, "r");
+      // use skolem cache
+      SkolemCache skc(false);
+      Node r = skc.mkSkolemCached(t0,
+                                  s0,
+                                  isRev ? SkolemCache::SK_ID_V_SPT_REV
+                                        : SkolemCache::SK_ID_V_SPT,
+                                  "r");
+      r = ProofSkolemCache::getWitnessForm(r);
       Node conc;
       if (isRev)
       {
-        conc = t0.eqNode(nm->mkNode(STRING_CONCAT, s0, r));
+        conc = t0.eqNode(nm->mkNode(STRING_CONCAT, r, s0));
       }
       else
       {
-        conc = t0.eqNode(nm->mkNode(STRING_CONCAT, r, s0));
+        conc = t0.eqNode(nm->mkNode(STRING_CONCAT, s0, r));
       }
       return conc;
     }
@@ -396,8 +409,12 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
     Assert(children.size() == 1);
     Assert(args.empty());
     Node nemp = children[0];
-    if (nemp.getKind() != NOT || nemp[0].getKind() != EQUAL
-        || !Word::isEmpty(nemp[0][1]))
+    if (nemp.getKind() != NOT || nemp[0].getKind() != EQUAL || 
+      !nemp[0][1].isConst())
+    {
+      return Node::null();
+    }
+    if (!Word::isEmpty(nemp[0][1]))
     {
       return Node::null();
     }