src/theory/theory_engine_proof_generator.h

   1 /*********************                                                        */
   2 /*! \file theory_engine.h
   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 "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY_ENGINE_PROOF_GENERATOR_H
  18 #define CVC4__THEORY_ENGINE_PROOF_GENERATOR_H
  19
  20 #include <memory>
  21
  22 #include "context/cdhashmap.h"
  23 #include "context/context.h"
  24 #include "expr/lazy_proof.h"
  25 #include "expr/proof_generator.h"
  26 #include "expr/proof_node_manager.h"
  27 #include "theory/trust_node.h"
  28
  29 namespace CVC4 {
  30
  31 /**
  32  * A simple proof generator class used by the theory engine. This class
  33  * stores proofs for TheoryEngine::getExplanation.
  34  *
  35  * Notice that this class could be made general purpose. Its main feature is
  36  * storing lazy proofs for facts in a context-dependent manner.
  37  */
  38 class TheoryEngineProofGenerator : public ProofGenerator
  39 {
  40   typedef context::
  41       CDHashMap<Node, std::shared_ptr<LazyCDProof>, NodeHashFunction>
  42           NodeLazyCDProofMap;
  43
  44  public:
  45   TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u);
  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   theory::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 };
  75
  76 }  // namespace CVC4
  77
  78 #endif /* CVC4__THEORY_ENGINE_PROOF_GENERATOR_H */