Setting up TRUE_ELIM

3 files changed, 30 insertions, 2 deletions

diff --git a/src/rewriter/rewrite_db_proof_cons.cpp b/src/rewriter/rewrite_db_proof_cons.cpp
index 7396c8a9b..7a0c68ba0 100644
--- a/src/rewriter/rewrite_db_proof_cons.cpp
+++ b/src/rewriter/rewrite_db_proof_cons.cpp
@@ -133,6 +133,14 @@ DslPfRule RewriteDbProofCons::proveInternal(Node eqi)
         << "unexpected failure for " << eqi;
     return it->second.d_id;
   }
+  // TRUE_ELIM
+  /*
+  if (proveWithRule(DslPfRule::TRUE_ELIM, eqi, {}, {}, false, false, true))
+  {
+    Trace("rpc-debug2") << "...proved via true-elim" << std::endl;
+    return DslPfRule::TRUE_ELIM;
+  }
+  */
   // store failure, and its maximum depth
   ProvenInfo& pi = d_pcache[eqi];
   pi.d_id = DslPfRule::FAIL;
@@ -213,7 +221,6 @@ bool RewriteDbProofCons::proveWithRule(DslPfRule id,
   if (id == DslPfRule::CONG)
   {
     Trace("rpc-debug2") << "Check rule " << id << std::endl;
-    pic.d_id = id;
     size_t nchild = target[0].getNumChildren();
     if (nchild == 0 || nchild != target[1].getNumChildren()
         || target[0].getOperator() != target[1].getOperator())
@@ -221,6 +228,7 @@ bool RewriteDbProofCons::proveWithRule(DslPfRule id,
       // cannot show congruence between different operators
       return false;
     }
+    pic.d_id = id;
     for (size_t i = 0; i < nchild; i++)
     {
       if (!target[0][i].getType().isComparableTo(target[1][i].getType()))
@@ -233,6 +241,19 @@ bool RewriteDbProofCons::proveWithRule(DslPfRule id,
       pic.d_vars.push_back(eq);
     }
   }
+  else if (id == DslPfRule::TRUE_ELIM)
+  {
+    return false;
+    if (target[0].getType().isBoolean())
+    {
+      // don't do for Boolean
+      return false;
+    }
+    pic.d_id = id;
+    Node eq = target.eqNode(d_true);
+    vcs.push_back(eq);
+    pic.d_vars.push_back(eq);
+  }
   else
   {
     const RewriteProofRule& rpr = d_db->getRule(id);
@@ -579,6 +600,11 @@ bool RewriteDbProofCons::ensureProofInternal(CDProof* cdp, Node eqi)
       {
         cdp->addStep(cur, PfRule::CONG, ps, pfArgs[cur]);
       }
+      else if (itd->second.d_id == DslPfRule::TRUE_ELIM)
+      {
+        conc = ps[0][0];
+        cdp->addStep(conc, PfRule::TRUE_ELIM, ps, {});
+      }
       else
       {
         Assert(pfArgs.find(cur) != pfArgs.end());
diff --git a/src/rewriter/rewrites_template.cpp b/src/rewriter/rewrites_template.cpp
index fc6f489cb..badaddb1f 100644
--- a/src/rewriter/rewrites_template.cpp
+++ b/src/rewriter/rewrites_template.cpp
@@ -43,7 +43,7 @@ bool isInternalDslPfRule(DslPfRule drule)
 {
   return drule == DslPfRule::FAIL || drule == DslPfRule::REFL
          || drule == DslPfRule::EVAL || drule == DslPfRule::TRANS
-         || drule == DslPfRule::CONG;
+         || drule == DslPfRule::CONG || drule == DslPfRule::TRUE_ELIM;
 }
 const char* toString(DslPfRule drule)
 {
@@ -55,6 +55,7 @@ const char* toString(DslPfRule drule)
     case DslPfRule::TRANS: return "TRANS";
     case DslPfRule::CONG:
       return "CONG";
+    case DslPfRule::TRUE_ELIM: return "TRUE_ELIM";
       // clang-format off
 ${printer}$
     default : Unreachable();
diff --git a/src/rewriter/rewrites_template.h b/src/rewriter/rewrites_template.h
index 273e1f542..9bea6b8bf 100644
--- a/src/rewriter/rewrites_template.h
+++ b/src/rewriter/rewrites_template.h
@@ -32,6 +32,7 @@ enum class DslPfRule : uint32_t
   EVAL,
   TRANS,  // internal-only
   CONG,   // internal-only
+  TRUE_ELIM,   // internal-only
   // Generated rule ids
   // clang-format off
   ${rule_ids}$