[proof-new] Resolution rules and checkers (#5070)

3 files changed, 180 insertions, 0 deletions

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 1d46b183f..57dd3e0bd 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -42,6 +42,10 @@ const char* toString(PfRule id)
     case PfRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA";
     case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM";
     //================================================= Boolean rules
+    case PfRule::RESOLUTION: return "RESOLUTION";
+    case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION";
+    case PfRule::FACTORING: return "FACTORING";
+    case PfRule::REORDERING: return "REORDERING";
     case PfRule::SPLIT: return "SPLIT";
     case PfRule::EQ_RESOLVE: return "EQ_RESOLVE";
     case PfRule::AND_ELIM: return "AND_ELIM";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 825503d5d..c02292dab 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -226,6 +226,45 @@ enum class PfRule : uint32_t
   WITNESS_AXIOM,
 
   //================================================= Boolean rules
+  // ======== Resolution
+  // Children:
+  //  (P1:(or F_1 ... F_i-1 F_i F_i+1 ... F_n),
+  //   P2:(or G_1 ... G_j-1 G_j G_j+1 ... G_m))
+  //
+  // Arguments: (F_i)
+  // ---------------------
+  // Conclusion: (or F_1 ... F_i-1 F_i+1 ... F_n G_1 ... G_j-1 G_j+1 ... G_m)
+  // where
+  //   G_j = (not F_i)
+  RESOLUTION,
+  // ======== Chain Resolution
+  // Children: (P1:(or F_{1,1} ... F_{1,n1}), ..., Pm:(or F_{m,1} ... F_{m,nm}))
+  // Arguments: (L_1, ..., L_{m-1})
+  // ---------------------
+  // Conclusion: C_m'
+  // where
+  //   let "C_1 <>_l C_2" represent the resolution of C_1 with C_2 with pivot l,
+  //   let C_1' = C_1 (from P_1),
+  //   for each i > 1, C_i' = C_i <>_L_i C_{i-1}'
+  CHAIN_RESOLUTION,
+  // ======== Factoring
+  // Children: (P:C1)
+  // Arguments: ()
+  // ---------------------
+  // Conclusion: C2
+  // where
+  //  Set representations of C1 and C2 is the same and the number of literals in
+  //  C2 is smaller than that of C1
+  FACTORING,
+  // ======== Reordering
+  // Children: (P:C1)
+  // Arguments: (C2)
+  // ---------------------
+  // Conclusion: C2
+  // where
+  //  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)
diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp
index 6a8244ce0..e9dafdad6 100644
--- a/src/theory/booleans/proof_checker.cpp
+++ b/src/theory/booleans/proof_checker.cpp
@@ -21,6 +21,10 @@ namespace booleans {
 void BoolProofRuleChecker::registerTo(ProofChecker* pc)
 {
   pc->registerChecker(PfRule::SPLIT, this);
+  pc->registerChecker(PfRule::RESOLUTION, this);
+  pc->registerChecker(PfRule::CHAIN_RESOLUTION, this);
+  pc->registerChecker(PfRule::FACTORING, this);
+  pc->registerChecker(PfRule::REORDERING, this);
   pc->registerChecker(PfRule::EQ_RESOLVE, this);
   pc->registerChecker(PfRule::AND_ELIM, this);
   pc->registerChecker(PfRule::AND_INTRO, this);
@@ -68,6 +72,139 @@ 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)
+    {
+      // if first clause, eliminate pivot, otherwise its negation
+      Node elim = i == 0 ? args[0] : args[0].notNode();
+      for (unsigned j = 0, size = children[i].getNumChildren(); j < size; ++j)
+      {
+        if (elim != children[i][j])
+        {
+          disjuncts.push_back(children[i][j]);
+        }
+      }
+    }
+    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::FACTORING)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::OR)
+    {
+      return Node::null();
+    }
+    // remove duplicates while keeping the order of children
+    std::unordered_set<TNode, TNodeHashFunction> clauseSet;
+    std::vector<Node> disjuncts;
+    unsigned size = children[0].getNumChildren();
+    for (unsigned i = 0; i < size; ++i)
+    {
+      if (clauseSet.count(children[0][i]))
+      {
+        continue;
+      }
+      disjuncts.push_back(children[0][i]);
+      clauseSet.insert(children[0][i]);
+    }
+    if (disjuncts.size() == size)
+    {
+      return Node::null();
+    }
+    NodeManager* nm = NodeManager::currentNM();
+    return disjuncts.empty()
+               ? nm->mkConst<bool>(false)
+               : disjuncts.size() == 1 ? disjuncts[0]
+                                       : nm->mkNode(kind::OR, disjuncts);
+  }
+  if (id == PfRule::REORDERING)
+  {
+    Assert(children.size() == 1);
+    Assert(args.size() == 1);
+    std::unordered_set<Node, NodeHashFunction> clauseSet1, clauseSet2;
+    if (children[0].getKind() == kind::OR)
+    {
+      clauseSet1.insert(children[0].begin(), children[0].end());
+    }
+    else
+    {
+      clauseSet1.insert(children[0]);
+    }
+    if (args[0].getKind() == kind::OR)
+    {
+      clauseSet2.insert(args[0].begin(), args[0].end());
+    }
+    else
+    {
+      clauseSet2.insert(args[0]);
+    }
+    if (clauseSet1 != clauseSet2)
+    {
+      Trace("bool-pfcheck") << id << ": clause set1: " << clauseSet1 << "\n"
+                            << id << ": clause set2: " << clauseSet2 << "\n";
+      return Node::null();
+    }
+    return args[0];
+  }
+  if (id == PfRule::CHAIN_RESOLUTION)
+  {
+    Assert(children.size() > 1);
+    Assert(args.size() == children.size() - 1);
+    Trace("bool-pfcheck") << "chain_res:\n" << push;
+    std::vector<Node> clauseNodes;
+    for (unsigned i = 0, childrenSize = children.size(); i < childrenSize; ++i)
+    {
+      std::unordered_set<Node, NodeHashFunction> elim;
+      // literals to be removed from "first" clause
+      if (i < childrenSize - 1)
+      {
+        elim.insert(args.begin() + i, args.end());
+      }
+      // literal to be removed from "second" clause. They will be negated
+      if (i > 0)
+      {
+        elim.insert(args[i - 1].negate());
+      }
+      Trace("bool-pfcheck") << i << ": elimination set: " << elim << "\n";
+      // only add to conclusion nodes that are not in elimination set. First get
+      // the nodes.
+      //
+      // Since unit clauses can also be OR nodes, we rely on the invariant that
+      // non-unit clauses will not occur themselves in their elimination sets.
+      // If they do then they must be unit.
+      std::vector<Node> lits;
+      if (children[i].getKind() == kind::OR && elim.count(children[i]) == 0)
+      {
+        lits.insert(lits.end(), children[i].begin(), children[i].end());
+      }
+      else
+      {
+        lits.push_back(children[i]);
+      }
+      Trace("bool-pfcheck") << i << ": clause lits: " << lits << "\n";
+      std::vector<Node> added;
+      for (unsigned j = 0, size = lits.size(); j < size; ++j)
+      {
+        if (elim.count(lits[j]) == 0)
+        {
+          clauseNodes.push_back(lits[j]);
+          added.push_back(lits[j]);
+        }
+      }
+      Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n";
+    }
+    Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n" << pop;
+    NodeManager* nm = NodeManager::currentNM();
+    return clauseNodes.empty()
+               ? nm->mkConst<bool>(false)
+               : clauseNodes.size() == 1 ? clauseNodes[0]
+                                         : nm->mkNode(kind::OR, clauseNodes);
+  }
   if (id == PfRule::SPLIT)
   {
     Assert(children.empty());