src/theory/theory_engine_proof_generator.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   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 theory engine proof generator.
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__THEORY_ENGINE_PROOF_GENERATOR_H
  19 #define CVC5__THEORY_ENGINE_PROOF_GENERATOR_H
  20
  21 #include <memory>
  22
  23 #include "context/cdhashmap.h"
  24 #include "context/context.h"
  25 #include "proof/lazy_proof.h"
  26 #include "proof/proof_generator.h"
  27 #include "proof/proof_node_manager.h"
  28 #include "proof/trust_node.h"
  29
  30 namespace cvc5 {
  31
  32 /**
  33  * A simple proof generator class used by the theory engine. This class
  34  * stores proofs for TheoryEngine::getExplanation.
  35  *
  36  * Notice that this class could be made general purpose. Its main feature is
  37  * storing lazy proofs for facts in a context-dependent manner.
  38  */
  39 class TheoryEngineProofGenerator : public ProofGenerator
  40 {
  41   typedef context::CDHashMap<Node, std::shared_ptr<LazyCDProof>>
  42       NodeLazyCDProofMap;
  43
  44  public:
  45   TheoryEngineProofGenerator(ProofNodeManager* pnm, context::Context* c);
  46   ~TheoryEngineProofGenerator() {}
  47   /**
  48    * Make trust explanation. Called when lpf has a proof of lit from free
  49    * assumptions in exp.
  50    *
  51    * This stores lpf in the map d_proofs below and returns the trust node for
  52    * this propagation, which has TrustNodeKind TrustNodeKind::PROP_EXP. If this
  53    * explanation already exists, then the previous explanation is taken, which
  54    * also suffices for proving the implication.
  55    */
  56   TrustNode mkTrustExplain(TNode lit,
  57                            Node exp,
  58                            std::shared_ptr<LazyCDProof> lpf);
  59   /**
  60    * Get proof for, which expects implications corresponding to explained
  61    * propagations (=> exp lit) registered by the above method. This currently
  62    * involves calling the mkScope method of ProofNodeManager internally, which
  63    * returns a closed proof.
  64    */
  65   std::shared_ptr<ProofNode> getProofFor(Node f) override;
  66   /** Identify this generator (for debugging, etc..) */
  67   std::string identify() const override;
  68
  69  private:
  70   /** The proof manager, used for allocating new ProofNode objects */
  71   ProofNodeManager* d_pnm;
  72   /** Map from formulas to lazy CD proofs */
  73   NodeLazyCDProofMap d_proofs;
  74   /** The false node */
  75   Node d_false;
  76 };
  77
  78 }  // namespace cvc5
  79
  80 #endif /* CVC5__THEORY_ENGINE_PROOF_GENERATOR_H */