1 /******************************************************************************
2 * Top contributors (to current version):
5 * This file is part of the cvc5 project.
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 * ****************************************************************************
13 * The theory engine proof generator.
16 #include "cvc5_private.h"
18 #ifndef CVC5__THEORY_ENGINE_PROOF_GENERATOR_H
19 #define CVC5__THEORY_ENGINE_PROOF_GENERATOR_H
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"
33 * A simple proof generator class used by the theory engine. This class
34 * stores proofs for TheoryEngine::getExplanation.
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.
39 class TheoryEngineProofGenerator
: public ProofGenerator
41 typedef context::CDHashMap
<Node
, std::shared_ptr
<LazyCDProof
>>
45 TheoryEngineProofGenerator(ProofNodeManager
* pnm
, context::Context
* c
);
46 ~TheoryEngineProofGenerator() {}
48 * Make trust explanation. Called when lpf has a proof of lit from free
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.
56 TrustNode
mkTrustExplain(TNode lit
,
58 std::shared_ptr
<LazyCDProof
> lpf
);
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.
65 std::shared_ptr
<ProofNode
> getProofFor(Node f
) override
;
66 /** Identify this generator (for debugging, etc..) */
67 std::string
identify() const override
;
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
;
80 #endif /* CVC5__THEORY_ENGINE_PROOF_GENERATOR_H */