src/theory/theory_proof_step_buffer.cpp

   1 /*********************                                                        */
   2 /*! \file theory_proof_step_buffer.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implementation of theory proof step buffer utility
  13  **/
  14
  15 #include "theory/theory_proof_step_buffer.h"
  16
  17 #include "expr/proof.h"
  18
  19 using namespace CVC4::kind;
  20
  21 namespace CVC4 {
  22 namespace theory {
  23
  24 TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc)
  25     : ProofStepBuffer(pc)
  26 {
  27 }
  28
  29 bool TheoryProofStepBuffer::applyEqIntro(Node src,
  30                                          Node tgt,
  31                                          const std::vector<Node>& exp,
  32                                          MethodId ids,
  33                                          MethodId idr)
  34 {
  35   std::vector<Node> args;
  36   args.push_back(src);
  37   builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, idr);
  38   Node res = tryStep(PfRule::MACRO_SR_EQ_INTRO, exp, args);
  39   if (res.isNull())
  40   {
  41     // failed to apply
  42     return false;
  43   }
  44   // should have concluded the expected equality
  45   Node expected = src.eqNode(tgt);
  46   if (res != expected)
  47   {
  48     // did not provide the correct target
  49     popStep();
  50     return false;
  51   }
  52   // successfully proved src == tgt.
  53   return true;
  54 }
  55
  56 bool TheoryProofStepBuffer::applyPredTransform(Node src,
  57                                                Node tgt,
  58                                                const std::vector<Node>& exp,
  59                                                MethodId ids,
  60                                                MethodId idr)
  61 {
  62   // symmetric equalities
  63   if (CDProof::isSame(src, tgt))
  64   {
  65     return true;
  66   }
  67   std::vector<Node> children;
  68   children.push_back(src);
  69   std::vector<Node> args;
  70   // try to prove that tgt rewrites to src
  71   children.insert(children.end(), exp.begin(), exp.end());
  72   args.push_back(tgt);
  73   builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, idr);
  74   Node res = tryStep(PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
  75   if (res.isNull())
  76   {
  77     // failed to apply
  78     return false;
  79   }
  80   // should definitely have concluded tgt
  81   Assert(res == tgt);
  82   return true;
  83 }
  84
  85 bool TheoryProofStepBuffer::applyPredIntro(Node tgt,
  86                                            const std::vector<Node>& exp,
  87                                            MethodId ids,
  88                                            MethodId idr)
  89 {
  90   std::vector<Node> args;
  91   args.push_back(tgt);
  92   builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, idr);
  93   Node res = tryStep(PfRule::MACRO_SR_PRED_INTRO, exp, args);
  94   if (res.isNull())
  95   {
  96     return false;
  97   }
  98   Assert(res == tgt);
  99   return true;
 100 }
 101
 102 Node TheoryProofStepBuffer::applyPredElim(Node src,
 103                                           const std::vector<Node>& exp,
 104                                           MethodId ids,
 105                                           MethodId idr)
 106 {
 107   std::vector<Node> children;
 108   children.push_back(src);
 109   children.insert(children.end(), exp.begin(), exp.end());
 110   std::vector<Node> args;
 111   builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, idr);
 112   Node srcRew = tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args);
 113   if (CDProof::isSame(src, srcRew))
 114   {
 115     popStep();
 116   }
 117   return srcRew;
 118 }
 119
 120 Node TheoryProofStepBuffer::factorReorderElimDoubleNeg(Node n)
 121 {
 122   if (n.getKind() != kind::OR)
 123   {
 124     return elimDoubleNegLit(n);
 125   }
 126   NodeManager* nm = NodeManager::currentNM();
 127   std::vector<Node> children{n.begin(), n.end()};
 128   std::vector<Node> childrenEqs;
 129   // eliminate double neg for each lit. Do it first because it may expose
 130   // duplicates
 131   bool hasDoubleNeg = false;
 132   for (unsigned i = 0; i < children.size(); ++i)
 133   {
 134     if (children[i].getKind() == kind::NOT
 135         && children[i][0].getKind() == kind::NOT)
 136     {
 137       hasDoubleNeg = true;
 138       childrenEqs.push_back(children[i].eqNode(children[i][0][0]));
 139       addStep(PfRule::MACRO_SR_PRED_INTRO,
 140               {},
 141               {childrenEqs.back()},
 142               childrenEqs.back());
 143       // update child
 144       children[i] = children[i][0][0];
 145     }
 146     else
 147     {
 148       childrenEqs.push_back(children[i].eqNode(children[i]));
 149       addStep(PfRule::REFL, {}, {children[i]}, childrenEqs.back());
 150     }
 151   }
 152   if (hasDoubleNeg)
 153   {
 154     Node oldn = n;
 155     n = nm->mkNode(kind::OR, children);
 156     // Create a congruence step to justify replacement of each doubly negated
 157     // literal. This is done to avoid having to use MACRO_SR_PRED_TRANSFORM
 158     // from the old clause to the new one, which, under the standard rewriter,
 159     // may not hold. An example is
 160     //
 161     //   ---------------------------------------------------------------------
 162     //   (or (or (not x2) x1 x2) (not (not x2))) = (or (or (not x2) x1 x2) x2)
 163     //
 164     // which fails due to factoring not happening after flattening.
 165     //
 166     // Using congruence only the
 167     //
 168     //  ------------------ MACRO_SR_PRED_INTRO
 169     //  (not (not t)) = t
 170     //
 171     // steps are added, which, since double negation is eliminated in a
 172     // pre-rewrite in the Boolean rewriter, will always hold under the
 173     // standard rewriter.
 174     Node congEq = oldn.eqNode(n);
 175     addStep(PfRule::CONG,
 176             childrenEqs,
 177             {ProofRuleChecker::mkKindNode(kind::OR)},
 178             congEq);
 179     // add an equality resolution step to derive normalize clause
 180     addStep(PfRule::EQ_RESOLVE, {oldn, congEq}, {}, n);
 181   }
 182   children.clear();
 183   // remove duplicates while keeping the order of children
 184   std::unordered_set<TNode, TNodeHashFunction> clauseSet;
 185   unsigned size = n.getNumChildren();
 186   for (unsigned i = 0; i < size; ++i)
 187   {
 188     if (clauseSet.count(n[i]))
 189     {
 190       continue;
 191     }
 192     children.push_back(n[i]);
 193     clauseSet.insert(n[i]);
 194   }
 195   // if factoring changed
 196   if (children.size() < size)
 197   {
 198     Node factored = children.empty()
 199                         ? nm->mkConst<bool>(false)
 200                         : children.size() == 1 ? children[0]
 201                                                : nm->mkNode(kind::OR, children);
 202     // don't overwrite what already has a proof step to avoid cycles
 203     addStep(PfRule::FACTORING, {n}, {}, factored);
 204     n = factored;
 205   }
 206   // nothing to order
 207   if (children.size() < 2)
 208   {
 209     return n;
 210   }
 211   // order
 212   std::sort(children.begin(), children.end());
 213   Node ordered = nm->mkNode(kind::OR, children);
 214   // if ordering changed
 215   if (ordered != n)
 216   {
 217     // don't overwrite what already has a proof step to avoid cycles
 218     addStep(PfRule::REORDERING, {n}, {ordered}, ordered);
 219   }
 220   return ordered;
 221 }
 222
 223 Node TheoryProofStepBuffer::elimDoubleNegLit(Node n)
 224 {
 225   // eliminate double neg
 226   if (n.getKind() == kind::NOT && n[0].getKind() == kind::NOT)
 227   {
 228     addStep(PfRule::NOT_NOT_ELIM, {n}, {}, n[0][0]);
 229     return n[0][0];
 230   }
 231   return n;
 232 }
 233
 234 }  // namespace theory
 235 }  // namespace CVC4