From c3a075c82c6ba038bfb58a8ef7dfb3bb2fc244c0 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 13 Oct 2020 18:33:57 -0500
Subject: [PATCH] (proof-new) New rules for Booleans (#5243)

This adds 2 new rules for convenience to the Boolean checker.
---
 src/expr/proof_rule.cpp               |  4 +++-
 src/expr/proof_rule.h                 | 26 +++++++++++++++-----
 src/theory/booleans/proof_checker.cpp | 34 +++++++++++++++++++++++++++
 3 files changed, 57 insertions(+), 7 deletions(-)

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index a6ecd9bcb..e4719ff30 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -50,6 +50,9 @@ const char* toString(PfRule id)
     case PfRule::REORDERING: return "REORDERING";
     case PfRule::SPLIT: return "SPLIT";
     case PfRule::EQ_RESOLVE: return "EQ_RESOLVE";
+    case PfRule::MODUS_PONENS: return "MODUS_PONENS";
+    case PfRule::NOT_NOT_ELIM: return "NOT_NOT_ELIM";
+    case PfRule::CONTRA: return "CONTRA";
     case PfRule::AND_ELIM: return "AND_ELIM";
     case PfRule::AND_INTRO: return "AND_INTRO";
     case PfRule::NOT_OR_ELIM: return "NOT_OR_ELIM";
@@ -68,7 +71,6 @@ const char* toString(PfRule id)
     case PfRule::ITE_ELIM2: return "ITE_ELIM2";
     case PfRule::NOT_ITE_ELIM1: return "NOT_ITE_ELIM1";
     case PfRule::NOT_ITE_ELIM2: return "NOT_ITE_ELIM2";
-    case PfRule::CONTRA: return "CONTRA";
     //================================================= De Morgan rules
     case PfRule::NOT_AND: return "NOT_AND";
     //================================================= CNF rules
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 1583bdc3d..340b636ae 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -280,6 +280,7 @@ enum class PfRule : uint32_t
   //  Set representations of C1 and C2 is the same but the number of literals in
   //  C2 is the same of that of C1
   REORDERING,
+
   // ======== Split
   // Children: none
   // Arguments: (F)
@@ -293,6 +294,25 @@ enum class PfRule : uint32_t
   // Conclusion: (F2)
   // Note this can optionally be seen as a macro for EQUIV_ELIM1+RESOLUTION.
   EQ_RESOLVE,
+  // ======== Modus ponens
+  // Children: (P1:F1, P2:(=> F1 F2))
+  // Arguments: none
+  // ---------------------
+  // Conclusion: (F2)
+  // Note this can optionally be seen as a macro for IMPLIES_ELIM+RESOLUTION.
+  MODUS_PONENS,
+  // ======== Double negation elimination
+  // Children: (P:(not (not F)))
+  // Arguments: none
+  // ---------------------
+  // Conclusion: (F)
+  NOT_NOT_ELIM,
+  // ======== Contradiction
+  // Children: (P1:F P2:(not F))
+  // Arguments: ()
+  // ---------------------
+  // Conclusion: false
+  CONTRA,
   // ======== And elimination
   // Children: (P:(and F1 ... Fn))
   // Arguments: (i)
@@ -401,12 +421,6 @@ enum class PfRule : uint32_t
   // ---------------------
   // Conclusion: (or C (not F2))
   NOT_ITE_ELIM2,
-  // ======== Not ITE elimination version 1
-  // Children: (P1:P P2:(not P))
-  // Arguments: ()
-  // ---------------------
-  // Conclusion: (false)
-  CONTRA,
 
   //================================================= De Morgan rules
   // ======== Not And
diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp
index eded6b9fa..2f06995e3 100644
--- a/src/theory/booleans/proof_checker.cpp
+++ b/src/theory/booleans/proof_checker.cpp
@@ -13,6 +13,8 @@
  **/
 
 #include "theory/booleans/proof_checker.h"
+#include "expr/skolem_manager.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
@@ -26,6 +28,9 @@ void BoolProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::FACTORING, this);
   pc->registerChecker(PfRule::REORDERING, this);
   pc->registerChecker(PfRule::EQ_RESOLVE, this);
+  pc->registerChecker(PfRule::MODUS_PONENS, this);
+  pc->registerChecker(PfRule::NOT_NOT_ELIM, this);
+  pc->registerChecker(PfRule::CONTRA, this);
   pc->registerChecker(PfRule::AND_ELIM, this);
   pc->registerChecker(PfRule::AND_INTRO, this);
   pc->registerChecker(PfRule::NOT_OR_ELIM, this);
@@ -212,6 +217,15 @@ Node BoolProofRuleChecker::checkInternal(PfRule id,
     return NodeManager::currentNM()->mkNode(
         kind::OR, args[0], args[0].notNode());
   }
+  if (id == PfRule::CONTRA)
+  {
+    Assert(children.size() == 2);
+    if (children[1].getKind() == Kind::NOT && children[0] == children[1][0])
+    {
+      return NodeManager::currentNM()->mkConst(false);
+    }
+    return Node::null();
+  }
   if (id == PfRule::EQ_RESOLVE)
   {
     Assert(children.size() == 2);
@@ -222,6 +236,26 @@ Node BoolProofRuleChecker::checkInternal(PfRule id,
     }
     return children[1][1];
   }
+  if (id == PfRule::MODUS_PONENS)
+  {
+    Assert(children.size() == 2);
+    Assert(args.empty());
+    if (children[1].getKind() != kind::IMPLIES || children[0] != children[1][0])
+    {
+      return Node::null();
+    }
+    return children[1][1];
+  }
+  if (id == PfRule::NOT_NOT_ELIM)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::NOT || children[0][0].getKind() != kind::NOT)
+    {
+      return Node::null();
+    }
+    return children[0][0][0];
+  }
   // natural deduction rules
   if (id == PfRule::AND_ELIM)
   {
-- 
2.30.2