src/theory/eager_proof_generator.cpp

   1 /*********************                                                        */
   2 /*! \file eager_proof_generator.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 the abstract proof generator class
  13  **/
  14
  15 #include "theory/eager_proof_generator.h"
  16
  17 #include "expr/proof.h"
  18 #include "expr/proof_node_manager.h"
  19
  20 namespace CVC4 {
  21 namespace theory {
  22
  23 EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm,
  24                                          context::Context* c,
  25                                          std::string name)
  26     : d_pnm(pnm), d_name(name), d_proofs(c == nullptr ? &d_context : c)
  27 {
  28 }
  29
  30 void EagerProofGenerator::setProofFor(Node f, std::shared_ptr<ProofNode> pf)
  31 {
  32   // pf should prove f
  33   Assert(pf->getResult() == f);
  34   d_proofs[f] = pf;
  35 }
  36 void EagerProofGenerator::setProofForConflict(Node conf,
  37                                               std::shared_ptr<ProofNode> pf)
  38 {
  39   // Normalize based on key
  40   Node ckey = TrustNode::getConflictProven(conf);
  41   setProofFor(ckey, pf);
  42 }
  43
  44 void EagerProofGenerator::setProofForLemma(Node lem,
  45                                            std::shared_ptr<ProofNode> pf)
  46 {
  47   // Normalize based on key
  48   Node lkey = TrustNode::getLemmaProven(lem);
  49   setProofFor(lkey, pf);
  50 }
  51
  52 void EagerProofGenerator::setProofForPropExp(TNode lit,
  53                                              Node exp,
  54                                              std::shared_ptr<ProofNode> pf)
  55 {
  56   // Normalize based on key
  57   Node pekey = TrustNode::getPropExpProven(lit, exp);
  58   setProofFor(pekey, pf);
  59 }
  60
  61 std::shared_ptr<ProofNode> EagerProofGenerator::getProofFor(Node f)
  62 {
  63   NodeProofNodeMap::iterator it = d_proofs.find(f);
  64   if (it == d_proofs.end())
  65   {
  66     return nullptr;
  67   }
  68   return (*it).second;
  69 }
  70
  71 bool EagerProofGenerator::hasProofFor(Node f)
  72 {
  73   return d_proofs.find(f) != d_proofs.end();
  74 }
  75
  76 TrustNode EagerProofGenerator::mkTrustNode(Node n,
  77                                            std::shared_ptr<ProofNode> pf,
  78                                            bool isConflict)
  79 {
  80   if (pf == nullptr)
  81   {
  82     return TrustNode::null();
  83   }
  84   if (isConflict)
  85   {
  86     // this shouldnt modify the key
  87     setProofForConflict(n, pf);
  88     // we can now return the trust node
  89     return TrustNode::mkTrustConflict(n, this);
  90   }
  91   // this shouldnt modify the key
  92   setProofForLemma(n, pf);
  93   // we can now return the trust node
  94   return TrustNode::mkTrustLemma(n, this);
  95 }
  96
  97 TrustNode EagerProofGenerator::mkTrustNode(Node conc,
  98                                            PfRule id,
  99                                            const std::vector<Node>& exp,
 100                                            const std::vector<Node>& args,
 101                                            bool isConflict)
 102 {
 103   // if no children, its easy
 104   if (exp.empty())
 105   {
 106     std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, conc);
 107     return mkTrustNode(conc, pf, isConflict);
 108   }
 109   // otherwise, we use CDProof + SCOPE
 110   CDProof cdp(d_pnm);
 111   cdp.addStep(conc, id, exp, args);
 112   std::shared_ptr<ProofNode> pf = cdp.getProofFor(conc);
 113   // We use mkNode instead of mkScope, since there is no reason to check
 114   // whether the free assumptions of pf are in exp, since they are by the
 115   // construction above.
 116   std::shared_ptr<ProofNode> pfs = d_pnm->mkNode(PfRule::SCOPE, {pf}, exp);
 117   return mkTrustNode(pfs->getResult(), pfs, isConflict);
 118 }
 119
 120 TrustNode EagerProofGenerator::mkTrustedPropagation(
 121     Node n, Node exp, std::shared_ptr<ProofNode> pf)
 122 {
 123   if (pf == nullptr)
 124   {
 125     return TrustNode::null();
 126   }
 127   setProofForPropExp(n, exp, pf);
 128   return TrustNode::mkTrustPropExp(n, exp, this);
 129 }
 130
 131 TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f)
 132 {
 133   // make the lemma
 134   Node lem = f.orNode(f.notNode());
 135   return mkTrustNode(lem, PfRule::SPLIT, {}, {f}, false);
 136 }
 137
 138 std::string EagerProofGenerator::identify() const { return d_name; }
 139
 140 }  // namespace theory
 141 }  // namespace CVC4