src/smt/preprocess_proof_generator.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Gereon Kremer
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   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.
  11  * ****************************************************************************
  12  *
  13  * The implementation of the module for proofs for preprocessing in an
  14  * SMT engine.
  15  */
  16
  17 #include "smt/preprocess_proof_generator.h"
  18
  19 #include <sstream>
  20
  21 #include "options/proof_options.h"
  22 #include "proof/proof.h"
  23 #include "proof/proof_checker.h"
  24 #include "proof/proof_node.h"
  25 #include "theory/rewriter.h"
  26
  27 namespace cvc5 {
  28 namespace smt {
  29
  30 PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm,
  31                                                    context::Context* c,
  32                                                    std::string name,
  33                                                    PfRule ra,
  34                                                    PfRule rpp)
  35     : d_pnm(pnm),
  36       d_ctx(c ? c : &d_context),
  37       d_src(d_ctx),
  38       d_helperProofs(pnm, d_ctx),
  39       d_inputPf(pnm, c, "InputProof"),
  40       d_name(name),
  41       d_ra(ra),
  42       d_rpp(rpp)
  43 {
  44 }
  45
  46 void PreprocessProofGenerator::notifyInput(Node n)
  47 {
  48   notifyNewAssert(n, &d_inputPf);
  49 }
  50
  51 void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg)
  52 {
  53   if (n.isConst() && n.getConst<bool>())
  54   {
  55     // ignore true assertions
  56     return;
  57   }
  58   Trace("smt-proof-pp-debug")
  59       << "PreprocessProofGenerator::notifyNewAssert: " << identify() << " " << n
  60       << " from " << (pg == nullptr ? "null" : pg->identify()) << std::endl;
  61   if (d_src.find(n) == d_src.end())
  62   {
  63     // if no proof generator provided for (non-true) assertion
  64     if (pg == nullptr)
  65     {
  66       checkEagerPedantic(d_ra);
  67     }
  68     d_src[n] = TrustNode::mkTrustLemma(n, pg);
  69   }
  70   else
  71   {
  72     Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
  73   }
  74 }
  75
  76 void PreprocessProofGenerator::notifyNewTrustedAssert(TrustNode tn)
  77 {
  78   notifyNewAssert(tn.getProven(), tn.getGenerator());
  79 }
  80
  81 void PreprocessProofGenerator::notifyPreprocessed(Node n,
  82                                                   Node np,
  83                                                   ProofGenerator* pg)
  84 {
  85   // only do anything if indeed it rewrote
  86   if (n == np)
  87   {
  88     return;
  89   }
  90   // call the trusted version
  91   notifyTrustedPreprocessed(TrustNode::mkTrustRewrite(n, np, pg));
  92 }
  93
  94 void PreprocessProofGenerator::notifyTrustedPreprocessed(TrustNode tnp)
  95 {
  96   if (tnp.isNull())
  97   {
  98     // no rewrite, nothing to do
  99     return;
 100   }
 101   Assert(tnp.getKind() == TrustNodeKind::REWRITE);
 102   Node np = tnp.getNode();
 103   Trace("smt-proof-pp-debug")
 104       << "PreprocessProofGenerator::notifyPreprocessed: " << tnp << std::endl;
 105   if (d_src.find(np) == d_src.end())
 106   {
 107     if (tnp.getGenerator() == nullptr)
 108     {
 109       checkEagerPedantic(d_rpp);
 110     }
 111     d_src[np] = tnp;
 112   }
 113   else
 114   {
 115     Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
 116   }
 117 }
 118
 119 std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
 120 {
 121   Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name
 122                     << ") input " << f << std::endl;
 123   NodeTrustNodeMap::iterator it = d_src.find(f);
 124   if (it == d_src.end())
 125   {
 126     Trace("smt-pppg") << "...no proof for " << identify() << " " << f
 127                       << std::endl;
 128     // could be an assumption, return nullptr
 129     return nullptr;
 130   }
 131   // make CDProof to construct the proof below
 132   CDProof cdp(d_pnm);
 133
 134   Node curr = f;
 135   std::vector<Node> transChildren;
 136   std::unordered_set<Node> processed;
 137   bool success;
 138   // we connect the proof of f to its source via the map d_src until we
 139   // discover that its source is a preprocessing lemma (a lemma stored in d_src)
 140   // or otherwise it is assumed to be an input assumption.
 141   do
 142   {
 143     success = false;
 144     if (it != d_src.end())
 145     {
 146       Assert((*it).second.getNode() == curr);
 147       // get the proven node
 148       Node proven = (*it).second.getProven();
 149       Assert(!proven.isNull());
 150       Trace("smt-pppg") << "...process proven " << proven << std::endl;
 151       if (processed.find(proven) != processed.end())
 152       {
 153         Unhandled() << "Cyclic steps in preprocess proof generator";
 154         continue;
 155       }
 156       processed.insert(proven);
 157       bool proofStepProcessed = false;
 158
 159       // if a generator for the step was provided, it is stored in the proof
 160       Trace("smt-pppg-debug")
 161           << "...get provided proof " << (*it).second << std::endl;
 162       std::shared_ptr<ProofNode> pfr = (*it).second.toProofNode();
 163       if (pfr != nullptr)
 164       {
 165         Trace("smt-pppg-debug") << "...add provided " << *pfr << std::endl;
 166         Assert(pfr->getResult() == proven);
 167         cdp.addProof(pfr);
 168         proofStepProcessed = true;
 169       }
 170
 171       Trace("smt-pppg-debug") << "...update" << std::endl;
 172       TrustNodeKind tnk = (*it).second.getKind();
 173       if (tnk == TrustNodeKind::REWRITE)
 174       {
 175         Trace("smt-pppg-debug")
 176             << "...rewritten from " << proven[0] << std::endl;
 177         Assert(proven.getKind() == kind::EQUAL);
 178         if (!proofStepProcessed)
 179         {
 180           // maybe its just a simple rewrite?
 181           if (proven[1] == theory::Rewriter::rewrite(proven[0]))
 182           {
 183             Trace("smt-pppg-debug") << "...add simple rewrite" << std::endl;
 184             cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0]});
 185             proofStepProcessed = true;
 186           }
 187         }
 188         transChildren.push_back(proven);
 189         // continue with source
 190         curr = proven[0];
 191         success = true;
 192         // find the next node
 193         Trace("smt-pppg") << "...continue " << curr << std::endl;
 194         it = d_src.find(curr);
 195       }
 196       else
 197       {
 198         Trace("smt-pppg") << "...lemma" << std::endl;
 199         Assert(tnk == TrustNodeKind::LEMMA);
 200       }
 201
 202       if (!proofStepProcessed)
 203       {
 204         Trace("smt-pppg-debug")
 205             << "...justify missing step with "
 206             << (tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp) << std::endl;
 207         // add trusted step, the rule depends on the kind of trust node
 208         cdp.addStep(
 209             proven, tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp, {}, {proven});
 210       }
 211     }
 212   } while (success);
 213
 214   // prove ( curr == f ), which is not necessary if they are the same
 215   // modulo symmetry.
 216   if (!CDProof::isSame(f, curr))
 217   {
 218     Node fullRewrite = curr.eqNode(f);
 219     if (transChildren.size() >= 2)
 220     {
 221       Trace("smt-pppg") << "...apply trans to get " << fullRewrite << std::endl;
 222       std::reverse(transChildren.begin(), transChildren.end());
 223       cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {});
 224     }
 225     Trace("smt-pppg") << "...eq_resolve to prove" << std::endl;
 226     // prove f
 227     cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {});
 228     Trace("smt-pppg") << "...finished" << std::endl;
 229   }
 230
 231   // overall, proof is:
 232   //        --------- from proof generator       ---------- from proof generator
 233   //        F_1 = F_2          ...               F_{n-1} = F_n
 234   // ---?   -------------------------------------------------- TRANS
 235   // F_1    F_1 = F_n
 236   // ---------------- EQ_RESOLVE
 237   // F_n
 238   // Note F_1 may have been given a proof if it was not an input assumption.
 239
 240   return cdp.getProofFor(f);
 241 }
 242
 243 ProofNodeManager* PreprocessProofGenerator::getManager() { return d_pnm; }
 244
 245 LazyCDProof* PreprocessProofGenerator::allocateHelperProof()
 246 {
 247   return d_helperProofs.allocateProof(nullptr, d_ctx);
 248 }
 249
 250 std::string PreprocessProofGenerator::identify() const { return d_name; }
 251
 252 void PreprocessProofGenerator::checkEagerPedantic(PfRule r)
 253 {
 254   if (options::proofEagerChecking())
 255   {
 256     // catch a pedantic failure now, which otherwise would not be
 257     // triggered since we are doing lazy proof generation
 258     ProofChecker* pc = d_pnm->getChecker();
 259     std::stringstream serr;
 260     if (pc->isPedanticFailure(r, serr))
 261     {
 262       Unhandled() << "PreprocessProofGenerator::checkEagerPedantic: "
 263                   << serr.str();
 264     }
 265   }
 266 }
 267
 268 }  // namespace smt
 269 }  // namespace cvc5