diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-12-11 18:58:13 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-11 18:58:13 -0300 |
commit | 8d0de294c259e789a149bc5ceb5d6501868e83d0 (patch) | |
tree | d714a7b920fc369bbbe3d37730fc4a6edeedde0e /src/prop/prop_engine.h | |
parent | 49215e6948aba1d6b762e28a7293581e25c2df8c (diff) |
[proof-new] Updating theory proxy to new proof infrastructure (#5653)
Diffstat (limited to 'src/prop/prop_engine.h')
-rw-r--r-- | src/prop/prop_engine.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 061324947..b36b9d22a 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -28,6 +28,7 @@ #include "options/options.h" #include "preprocessing/assertion_pipeline.h" #include "proof/proof_manager.h" +#include "prop/proof_cnf_stream.h" #include "util/resource_manager.h" #include "util/result.h" #include "util/unsafe_interrupt_exception.h" @@ -235,6 +236,9 @@ class PropEngine */ bool properExplanation(TNode node, TNode expl) const; + /** Retrieve this modules proof CNF stream. */ + ProofCnfStream* getProofCnfStream(); + /** * Return the prop engine proof. This should be called only when proofs are * enabled. Returns a proof of false whose free assumptions are the @@ -274,6 +278,8 @@ class PropEngine /** The CNF converter in use */ CnfStream* d_cnfStream; + /** Proof-producing CNF converter */ + std::unique_ptr<ProofCnfStream> d_pfCnfStream; /** Whether we were just interrupted (or not) */ bool d_interrupted; |