reverting unnecessary for fix

3 files changed, 0 insertions, 29 deletions

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index e5e1b4292..e96f23603 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -35,7 +35,6 @@ const char* toString(PfRule id)
     case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM";
     case PfRule::THEORY_LEMMA: return "THEORY_LEMMA";
     //================================================= Boolean rules
-    case PfRule::RESOLUTION: return "RESOLUTION";
     case PfRule::SPLIT: return "SPLIT";
     case PfRule::AND_ELIM: return "AND_ELIM";
     case PfRule::NOT_OR_ELIM: return "NOT_OR_ELIM";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 7a826aec7..d32206cb4 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -176,15 +176,6 @@ enum class PfRule : uint32_t
 
   //================================================= Boolean rules
   // ======== Split
-  // Children: (P1:(or F_1 ... F_i-1 F_i F_i+1 ... F_n),
-  //            P2:(or G_1 ... G_i-1 G_i G_i+1 ... G_n) )
-  // Arguments: (F_i)
-  // ---------------------
-  // Conclusion: (or F_1 ... F_i-1 F_i+1 ... F_n G_1 ... G_i-1 G_i+1 ... G_n)
-  // where
-  //   G_i is synctatically equal to (not F_i)
-  RESOLUTION,
-  // ======== Split
   // Children: none
   // Arguments: (F)
   // ---------------------
diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp
index 300fd4071..48ea256a5 100644
--- a/src/theory/booleans/proof_checker.cpp
+++ b/src/theory/booleans/proof_checker.cpp
@@ -20,7 +20,6 @@ namespace booleans {
 
 void BoolProofRuleChecker::registerTo(ProofChecker* pc)
 {
-  pc->registerChecker(PfRule::RESOLUTION, this);
   pc->registerChecker(PfRule::SPLIT, this);
   pc->registerChecker(PfRule::AND_ELIM, this);
   pc->registerChecker(PfRule::NOT_OR_ELIM, this);
@@ -45,24 +44,6 @@ Node BoolProofRuleChecker::checkInternal(PfRule id,
                                          const std::vector<Node>& children,
                                          const std::vector<Node>& args)
 {
-  if (id == PfRule::RESOLUTION)
-  {
-    Assert(children.size() == 2);
-    Assert(args.size() == 1);
-    std::vector<Node> disjuncts;
-    for (unsigned i = 0; i < 2; ++i)
-    {
-      Node piv = i == 0 ? args[0] : args[0].notNode();
-      for (unsigned j = 0, size = children[i].size(); j < size; ++j)
-      {
-        if (children[i][j] != piv)
-        {
-          disjuncts.push_back(children[0][i]);
-        }
-      }
-    }
-    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
-  }
   if (id == PfRule::SPLIT)
   {
     Assert(children.empty());