src/theory/theory_engine_proof_generator.cpp

   1 /*********************                                                        */
   2 /*! \file theory_engine_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 The theory engine proof generator
  13  **/
  14
  15 #include "theory/theory_engine_proof_generator.h"
  16
  17 using namespace CVC4::kind;
  18
  19 namespace CVC4 {
  20
  21 TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm,
  22                                                        context::UserContext* u)
  23     : d_pnm(pnm), d_proofs(u)
  24 {
  25   d_false = NodeManager::currentNM()->mkConst(false);
  26 }
  27
  28 theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain(
  29     TNode lit, Node exp, std::shared_ptr<LazyCDProof> lpf)
  30 {
  31   Node p;
  32   theory::TrustNode trn;
  33   if (lit == d_false)
  34   {
  35     // propagation of false is a conflict
  36     trn = theory::TrustNode::mkTrustConflict(exp, this);
  37     p = trn.getProven();
  38     Assert(p.getKind() == NOT);
  39   }
  40   else
  41   {
  42     trn = theory::TrustNode::mkTrustPropExp(lit, exp, this);
  43     p = trn.getProven();
  44     Assert(p.getKind() == IMPLIES && p.getNumChildren() == 2);
  45   }
  46   // should not already be proven
  47   NodeLazyCDProofMap::iterator it = d_proofs.find(p);
  48   if (it == d_proofs.end())
  49   {
  50     // we will prove the fact p using the proof from lpf.
  51     d_proofs.insert(p, lpf);
  52   }
  53   return trn;
  54 }
  55
  56 std::shared_ptr<ProofNode> TheoryEngineProofGenerator::getProofFor(Node f)
  57 {
  58   Trace("tepg-debug") << "TheoryEngineProofGenerator::getProofFor: " << f
  59                       << std::endl;
  60   NodeLazyCDProofMap::iterator it = d_proofs.find(f);
  61   if (it == d_proofs.end())
  62   {
  63     Trace("tepg-debug") << "...null" << std::endl;
  64     return nullptr;
  65   }
  66   std::shared_ptr<LazyCDProof> lcp = (*it).second;
  67   // finalize it via scope
  68   std::vector<Node> scopeAssumps;
  69   // should only ask this generator for proofs of implications, or conflicts
  70   Node exp;
  71   Node conclusion;
  72   if (f.getKind() == IMPLIES && f.getNumChildren() == 2)
  73   {
  74     exp = f[0];
  75     conclusion = f[1];
  76   }
  77   else if (f.getKind() == NOT)
  78   {
  79     exp = f[0];
  80     conclusion = d_false;
  81   }
  82   else
  83   {
  84     Unhandled() << "TheoryEngineProofGenerator::getProofFor: unexpected fact "
  85                 << f << std::endl;
  86     return nullptr;
  87   }
  88   // get the assumptions to assume in a scope
  89   if (exp.getKind() == AND)
  90   {
  91     for (const Node& fc : exp)
  92     {
  93       scopeAssumps.push_back(fc);
  94     }
  95   }
  96   else
  97   {
  98     scopeAssumps.push_back(exp);
  99   }
 100   Trace("tepg-debug") << "...get proof body" << std::endl;
 101   // get the proof for conclusion
 102   std::shared_ptr<ProofNode> pfb = lcp->getProofFor(conclusion);
 103   Trace("tepg-debug") << "...mkScope" << std::endl;
 104   // call the scope method of proof node manager
 105   std::shared_ptr<ProofNode> pf = d_pnm->mkScope(pfb, scopeAssumps);
 106
 107   if (pf->getResult() != f)
 108   {
 109     std::stringstream serr;
 110     serr << "TheoryEngineProofGenerator::getProofFor: Proof: " << std::endl;
 111     serr << *pf << std::endl;
 112     serr << "TheoryEngineProofGenerator::getProofFor: unexpected return proof"
 113          << std::endl;
 114     serr << "  Expected: " << f << std::endl;
 115     serr << "       Got: " << pf->getResult() << std::endl;
 116     Unhandled() << serr.str();
 117   }
 118   Trace("tepg-debug") << "...finished" << std::endl;
 119   return pf;
 120 }
 121
 122 std::string TheoryEngineProofGenerator::identify() const
 123 {
 124   return "TheoryEngineProofGenerator";
 125 }
 126
 127 }  // namespace CVC4