Fixes for reduction, duplicate literals in lemmas/conflicts, word checks.

4 files changed, 19 insertions, 12 deletions

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index d182f20f2..d8d75ea24 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1518,8 +1518,6 @@ 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;
@@ -1535,7 +1533,6 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
         iinfo.d_noExplain.push_back(tnz);
       }
     }
-    */
     SkolemCache* skc = d_termReg.getSkolemCache();
     std::vector<Node> newSkolems;
     // make the conclusion
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 77b8dbcb7..548fa757e 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -514,14 +514,24 @@ Node InferProofCons::convert(Inference infer,
     case Inference::REDUCTION:
     {
       size_t nchild = conc.getNumChildren();
-      if (conc.getKind() != AND || conc[nchild - 1].getKind() != EQUAL)
+      Node mainEq;
+      if (conc.getKind()==EQUAL)
+      {
+        mainEq = conc;
+      }
+      else if (conc.getKind()== AND && conc[nchild - 1].getKind() == EQUAL)
+      {
+        mainEq = conc[nchild - 1];
+      }
+      if (mainEq.isNull())
       {
+        Trace("strings-ipc-red") << "Bad Reduction: " << conc << std::endl;
         Assert(false);
         break;
       }
       std::vector<Node> argsRed;
       // the left hand side of the last conjunct is the term we are reducing
-      argsRed.push_back(conc[nchild - 1][0]);
+      argsRed.push_back(mainEq[0]);
       Node red = d_psb.tryStep(PfRule::STRINGS_REDUCTION, emptyVec, argsRed);
       Trace("strings-ipc-red") << "Reduction : " << red << std::endl;
       if (!red.isNull())
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index 983ef9acf..5394d7193 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -200,7 +200,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
       {
         return Node::null();
       }
-      if (!s0.isConst() || Word::isEmpty(s0))
+      if (!s0.isConst() || !s0.getType().isStringLike() || Word::isEmpty(s0))
       {
         return Node::null();
       }
@@ -263,14 +263,14 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
         return Node::null();
       }
       Node w1 = tvec[isRev ? nchildt - 2 : 1];
-      if (!w1.isConst() || Word::isEmpty(w1))
+      if (!w1.isConst() || !w1.getType().isStringLike() || Word::isEmpty(w1))
       {
         Trace("pfcheck-strings-cprop")
             << "...failed adjacent constant content" << std::endl;
         return Node::null();
       }
       Node w2 = s0;
-      if (!w2.isConst() || Word::isEmpty(w2))
+      if (!w2.isConst() || !w2.getType().isStringLike() || Word::isEmpty(w2))
       {
         Trace("pfcheck-strings-cprop") << "...failed constant" << std::endl;
         return Node::null();
@@ -370,7 +370,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
     Assert(args.empty());
     Node nemp = children[0];
     if (nemp.getKind() != NOT || nemp[0].getKind() != EQUAL || 
-      !nemp[0][1].isConst())
+      !nemp[0][1].isConst() || !nemp[0][1].getType().isStringLike())
     {
       return Node::null();
     }
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 3ba250714..3bd723511 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -406,16 +406,16 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc,
     std::map<Node, std::vector<ProofNode*>> famap;
     pfConc->getFreeAssumptionsMap(famap);
     // we first ensure the assumptions are flattened
-    std::vector<Node> ac;
+    std::unordered_set<Node, NodeHashFunction> ac;
     for (const TNode& a : assumps)
     {
       if (a.getKind() == AND)
       {
-        ac.insert(ac.end(), a.begin(), a.end());
+        ac.insert(a.begin(), a.end());
       }
       else
       {
-        ac.push_back(a);
+        ac.insert(a);
       }
     }
     std::map<Node, std::vector<ProofNode*>>::iterator itf;