diff options
Diffstat (limited to 'src/proof/proof_manager.h')
-rw-r--r-- | src/proof/proof_manager.h | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 0342288fe..82efbab0f 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -69,7 +69,10 @@ class TheoryProof; class UFProof; class ArithProof; class ArrayProof; -class BitVectorProof; + +namespace proof { +class ResolutionBitVectorProof; +} template <class Solver> class LFSCSatProof; typedef TSatProof<CVC4::Minisat::Solver> CoreSatProof; @@ -77,7 +80,6 @@ typedef TSatProof<CVC4::Minisat::Solver> CoreSatProof; class LFSCCnfProof; class LFSCTheoryProofEngine; class LFSCUFProof; -class LFSCBitVectorProof; class LFSCRewriterProof; namespace prop { @@ -189,7 +191,7 @@ public: static TheoryProofEngine* getTheoryProofEngine(); static TheoryProof* getTheoryProof( theory::TheoryId id ); static UFProof* getUfProof(); - static BitVectorProof* getBitVectorProof(); + static proof::ResolutionBitVectorProof* getBitVectorProof(); static ArrayProof* getArrayProof(); static ArithProof* getArithProof(); |