adding resolution

3 files changed, 29 insertions, 0 deletions

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index e96f23603..e5e1b4292 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -35,6 +35,7 @@ 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 d32206cb4..7a826aec7 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -176,6 +176,15 @@ 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 48ea256a5..300fd4071 100644
--- a/src/theory/booleans/proof_checker.cpp
+++ b/src/theory/booleans/proof_checker.cpp
@@ -20,6 +20,7 @@ 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);
@@ -44,6 +45,24 @@ 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());