Home
last modified time | relevance | path

Searched refs:getTheoryProofEngine (Results 1 – 6 of 6) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/proof/
H A Dproof_manager.cpp94 static_cast<LFSCTheoryProofEngine*>(getTheoryProofEngine()))); in getProof()
109 TheoryProofEngine* ProofManager::getTheoryProofEngine() { in getTheoryProofEngine() function in CVC4::ProofManager
116 TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_UF); in getUfProof()
123 TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_BV); in getBitVectorProof()
129 TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARRAYS); in getArrayProof()
135 TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARITH); in getArithProof()
812 …ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm(inputAssertion, os, globalLetMa… in printPreprocessedAssertions()
1070 TheoryProofEngine* tpe = ProofManager::currentPM()->getTheoryProofEngine(); in printTrustedTerm()
H A Dproof_manager.h191 static TheoryProofEngine* getTheoryProofEngine();
H A Dcnf_proof.cpp396 …CTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); in printAtomMapping()
417 …CTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); in printAtomMapping()
H A Darray_proof.cpp173 ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, in toStreamRecLFSC()
736 ProofManager::getTheoryProofEngine()->printConstantDisequalityProof( in toStreamRecLFSC()
H A Duf_proof.cpp137 ProofManager::getTheoryProofEngine()->printConstantDisequalityProof( in toStreamRecLFSC()
/dports/math/cvc4/CVC4-1.7/src/smt/
H A Dsmt_engine.cpp938 ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id)); in finishInit()
1003 ProofManager::currentPM()->getTheoryProofEngine()-> in finishInit()