src/preprocessing/assertion_pipeline.cpp

   1 /*********************                                                        */
   2 /*! \file assertion_pipeline.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Andres Noetzli, Haniel Barbosa
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 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 AssertionPipeline stores a list of assertions modified by
  13  ** preprocessing passes
  14  **/
  15
  16 #include "preprocessing/assertion_pipeline.h"
  17
  18 #include "expr/node_manager.h"
  19 #include "options/smt_options.h"
  20 #include "expr/lazy_proof.h"
  21 #include "proof/proof_manager.h"
  22 #include "smt/preprocess_proof_generator.h"
  23 #include "theory/builtin/proof_checker.h"
  24 #include "theory/rewriter.h"
  25
  26 namespace cvc5 {
  27 namespace preprocessing {
  28
  29 AssertionPipeline::AssertionPipeline()
  30     : d_realAssertionsEnd(0),
  31       d_storeSubstsInAsserts(false),
  32       d_substsIndex(0),
  33       d_assumptionsStart(0),
  34       d_numAssumptions(0),
  35       d_pppg(nullptr)
  36 {
  37 }
  38
  39 void AssertionPipeline::clear()
  40 {
  41   d_nodes.clear();
  42   d_realAssertionsEnd = 0;
  43   d_assumptionsStart = 0;
  44   d_numAssumptions = 0;
  45 }
  46
  47 void AssertionPipeline::push_back(Node n,
  48                                   bool isAssumption,
  49                                   bool isInput,
  50                                   ProofGenerator* pgen)
  51 {
  52   d_nodes.push_back(n);
  53   if (isAssumption)
  54   {
  55     Assert(pgen == nullptr);
  56     if (d_numAssumptions == 0)
  57     {
  58       d_assumptionsStart = d_nodes.size() - 1;
  59     }
  60     // Currently, we assume that assumptions are all added one after another
  61     // and that we store them in the same vector as the assertions. Once we
  62     // split the assertions up into multiple vectors (see issue #2473), we will
  63     // not have this limitation anymore.
  64     Assert(d_assumptionsStart + d_numAssumptions == d_nodes.size() - 1);
  65     d_numAssumptions++;
  66   }
  67   Trace("assert-pipeline") << "Assertions: ...new assertion " << n
  68                            << ", isInput=" << isInput << std::endl;
  69   if (isProofEnabled())
  70   {
  71     if (!isInput)
  72     {
  73       // notice this is always called, regardless of whether pgen is nullptr
  74       d_pppg->notifyNewAssert(n, pgen);
  75     }
  76     else
  77     {
  78       Assert(pgen == nullptr);
  79       // n is an input assertion, whose proof should be ASSUME.
  80       d_pppg->notifyInput(n);
  81     }
  82   }
  83 }
  84
  85 void AssertionPipeline::pushBackTrusted(theory::TrustNode trn)
  86 {
  87   Assert(trn.getKind() == theory::TrustNodeKind::LEMMA);
  88   // push back what was proven
  89   push_back(trn.getProven(), false, false, trn.getGenerator());
  90 }
  91
  92 void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
  93 {
  94   if (n == d_nodes[i])
  95   {
  96     // no change, skip
  97     return;
  98   }
  99   Trace("assert-pipeline") << "Assertions: Replace " << d_nodes[i] << " with "
 100                            << n << std::endl;
 101   if (isProofEnabled())
 102   {
 103     d_pppg->notifyPreprocessed(d_nodes[i], n, pgen);
 104   }
 105   else if (options::unsatCores())
 106   {
 107     ProofManager::currentPM()->addDependence(n, d_nodes[i]);
 108   }
 109   d_nodes[i] = n;
 110 }
 111
 112 void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn)
 113 {
 114   if (trn.isNull())
 115   {
 116     // null trust node denotes no change, nothing to do
 117     return;
 118   }
 119   Assert(trn.getKind() == theory::TrustNodeKind::REWRITE);
 120   Assert(trn.getProven()[0] == d_nodes[i]);
 121   replace(i, trn.getNode(), trn.getGenerator());
 122 }
 123
 124 void AssertionPipeline::setProofGenerator(smt::PreprocessProofGenerator* pppg)
 125 {
 126   d_pppg = pppg;
 127 }
 128
 129 bool AssertionPipeline::isProofEnabled() const { return d_pppg != nullptr; }
 130
 131 void AssertionPipeline::enableStoreSubstsInAsserts()
 132 {
 133   d_storeSubstsInAsserts = true;
 134   d_substsIndex = d_nodes.size();
 135   d_nodes.push_back(NodeManager::currentNM()->mkConst<bool>(true));
 136 }
 137
 138 void AssertionPipeline::disableStoreSubstsInAsserts()
 139 {
 140   d_storeSubstsInAsserts = false;
 141 }
 142
 143 void AssertionPipeline::addSubstitutionNode(Node n, ProofGenerator* pg)
 144 {
 145   Assert(d_storeSubstsInAsserts);
 146   Assert(n.getKind() == kind::EQUAL);
 147   conjoin(d_substsIndex, n, pg);
 148 }
 149
 150 void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
 151 {
 152   NodeManager* nm = NodeManager::currentNM();
 153   Node newConj = nm->mkNode(kind::AND, d_nodes[i], n);
 154   Node newConjr = theory::Rewriter::rewrite(newConj);
 155   Trace("assert-pipeline") << "Assertions: conjoin " << n << " to "
 156                            << d_nodes[i] << std::endl;
 157   Trace("assert-pipeline-debug") << "conjoin " << n << " to " << d_nodes[i]
 158                                  << ", got " << newConjr << std::endl;
 159   if (newConjr == d_nodes[i])
 160   {
 161     // trivial, skip
 162     return;
 163   }
 164   if (isProofEnabled())
 165   {
 166     if (newConjr == n)
 167     {
 168       // don't care about the previous proof and can simply plug in the
 169       // proof from pg if the resulting assertion is the same as n.
 170       d_pppg->notifyNewAssert(newConjr, pg);
 171     }
 172     else
 173     {
 174       // ---------- from pppg   --------- from pg
 175       // d_nodes[i]                n
 176       // -------------------------------- AND_INTRO
 177       //      d_nodes[i] ^ n
 178       // -------------------------------- MACRO_SR_PRED_TRANSFORM
 179       //   rewrite( d_nodes[i] ^ n )
 180       // allocate a fresh proof which will act as the proof generator
 181       LazyCDProof* lcp = d_pppg->allocateHelperProof();
 182       lcp->addLazyStep(n, pg, PfRule::PREPROCESS);
 183       if (d_nodes[i].isConst() && d_nodes[i].getConst<bool>())
 184       {
 185         // skip the AND_INTRO if the previous d_nodes[i] was true
 186         newConj = n;
 187       }
 188       else
 189       {
 190         lcp->addLazyStep(d_nodes[i], d_pppg);
 191         lcp->addStep(newConj, PfRule::AND_INTRO, {d_nodes[i], n}, {});
 192       }
 193       if (newConjr != newConj)
 194       {
 195         lcp->addStep(
 196             newConjr, PfRule::MACRO_SR_PRED_TRANSFORM, {newConj}, {newConjr});
 197       }
 198       // Notice we have constructed a proof of a new assertion, where d_pppg
 199       // is referenced in the lazy proof above. If alternatively we had
 200       // constructed a proof of d_nodes[i] = rewrite( d_nodes[i] ^ n ), we would
 201       // have used notifyPreprocessed. However, it is simpler to make the
 202       // above proof.
 203       d_pppg->notifyNewAssert(newConjr, lcp);
 204     }
 205   }
 206   if (options::unsatCores() && !isProofEnabled())
 207   {
 208     ProofManager::currentPM()->addDependence(newConjr, d_nodes[i]);
 209   }
 210   d_nodes[i] = newConjr;
 211   Assert(theory::Rewriter::rewrite(newConjr) == newConjr);
 212 }
 213
 214 }  // namespace preprocessing
 215 }  // namespace cvc5