From 65431e88f8e0c48c90bc540b95c63b67d8387219 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Oct 2021 04:53:59 -0500
Subject: [PATCH] Miscellaneous fixes from proof-new (#7313)

Includes a few fixes for strings and datatypes theory lemma proofs.
---
 src/theory/datatypes/infer_proof_cons.cpp | 51 +++++++++++++----------
 src/theory/strings/infer_proof_cons.cpp   | 25 ++++++++++-
 src/theory/strings/term_registry.cpp      |  2 +-
 3 files changed, 54 insertions(+), 24 deletions(-)

diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index afbfd16c1..4aace5f1c 100644
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -169,30 +169,37 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
         Node concAtom = concPol ? conc : conc[0];
         concEq = concAtom.eqNode(nm->mkConst(concPol));
       }
-      Assert(concEq.getKind() == EQUAL
-             && concEq[0].getKind() == APPLY_SELECTOR_TOTAL);
-      Assert(exp[0].getType().isDatatype());
-      Node sop = concEq[0].getOperator();
-      Node sl = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[0]);
-      Node sr = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[1]);
-      // exp[0] = exp[1]
-      // --------------------- CONG        ----------------- DT_COLLAPSE
-      // s(exp[0]) = s(exp[1])             s(exp[1]) = r
-      // --------------------------------------------------- TRANS
-      // s(exp[0]) = r
-      Node asn = ProofRuleChecker::mkKindNode(APPLY_SELECTOR_TOTAL);
-      Node seq = sl.eqNode(sr);
-      cdp->addStep(seq, PfRule::CONG, {exp}, {asn, sop});
-      Node sceq = sr.eqNode(concEq[1]);
-      cdp->addStep(sceq, PfRule::DT_COLLAPSE, {}, {sr});
-      cdp->addStep(sl.eqNode(concEq[1]), PfRule::TRANS, {seq, sceq}, {});
-      if (conc.getKind() != EQUAL)
+      if (concEq[0].getKind() != APPLY_SELECTOR_TOTAL)
       {
-        PfRule eid =
-            conc.getKind() == NOT ? PfRule::FALSE_ELIM : PfRule::TRUE_ELIM;
-        cdp->addStep(conc, eid, {concEq}, {});
+        // can happen for Boolean term variables, which are not currently
+        // supported.
+        success = false;
+      }
+      else
+      {
+        Assert(exp[0].getType().isDatatype());
+        Node sop = concEq[0].getOperator();
+        Node sl = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[0]);
+        Node sr = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[1]);
+        // exp[0] = exp[1]
+        // --------------------- CONG        ----------------- DT_COLLAPSE
+        // s(exp[0]) = s(exp[1])             s(exp[1]) = r
+        // --------------------------------------------------- TRANS
+        // s(exp[0]) = r
+        Node asn = ProofRuleChecker::mkKindNode(APPLY_SELECTOR_TOTAL);
+        Node seq = sl.eqNode(sr);
+        cdp->addStep(seq, PfRule::CONG, {exp}, {asn, sop});
+        Node sceq = sr.eqNode(concEq[1]);
+        cdp->addStep(sceq, PfRule::DT_COLLAPSE, {}, {sr});
+        cdp->addStep(sl.eqNode(concEq[1]), PfRule::TRANS, {seq, sceq}, {});
+        if (conc.getKind() != EQUAL)
+        {
+          PfRule eid =
+              conc.getKind() == NOT ? PfRule::FALSE_ELIM : PfRule::TRUE_ELIM;
+          cdp->addStep(conc, eid, {concEq}, {});
+        }
+        success = true;
       }
-      success = true;
     }
     break;
     case InferenceId::DATATYPES_CLASH_CONFLICT:
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index e9a6da104..34597c8be 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -396,6 +396,25 @@ void InferProofCons::convert(InferenceId infer,
           Trace("strings-ipc-core") << "...success!" << std::endl;
         }
       }
+      else if (infer == InferenceId::STRINGS_F_NCTN
+               || infer == InferenceId::STRINGS_N_NCTN)
+      {
+        // May require extended equality rewrite, applied after the rewrite
+        // above. Notice we need both in sequence since ext equality rewriting
+        // is not recursive.
+        std::vector<Node> argsERew;
+        addMethodIds(argsERew,
+                     MethodId::SB_DEFAULT,
+                     MethodId::SBA_SEQUENTIAL,
+                     MethodId::RW_REWRITE_EQ_EXT);
+        Node mainEqERew =
+            psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, {mainEqCeq}, argsERew);
+        if (mainEqERew == conc)
+        {
+          useBuffer = true;
+          Trace("strings-ipc-core") << "...success!" << std::endl;
+        }
+      }
       else
       {
         std::vector<Node> tvec;
@@ -845,7 +864,11 @@ void InferProofCons::convert(InferenceId infer,
       Trace("strings-ipc-prefix")
           << "- Possible conflicting equality : " << curr << std::endl;
       std::vector<Node> emp;
-      Node concE = psb.applyPredElim(curr, emp);
+      Node concE = psb.applyPredElim(curr,
+                                     emp,
+                                     MethodId::SB_DEFAULT,
+                                     MethodId::SBA_SEQUENTIAL,
+                                     MethodId::RW_REWRITE_EQ_EXT);
       Trace("strings-ipc-prefix")
           << "- After pred elim: " << concE << std::endl;
       if (concE == conc)
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 9252babba..2fc86a5a5 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -104,7 +104,7 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc)
     lemma = nm->mkNode(
         AND,
         nm->mkNode(
-            OR, nm->mkConst(Rational(-1)).eqNode(t), nm->mkNode(GEQ, t, t[2])),
+            OR, t.eqNode(nm->mkConst(Rational(-1))), nm->mkNode(GEQ, t, t[2])),
         nm->mkNode(LEQ, t, l));
   }
   else if (tk == STRING_STOI)
-- 
2.30.2