Searched refs:getTheoryProofEngine (Results 1 – 6 of 6) sorted by relevance
94 static_cast<LFSCTheoryProofEngine*>(getTheoryProofEngine()))); in getProof()109 TheoryProofEngine* ProofManager::getTheoryProofEngine() { in getTheoryProofEngine() function in CVC4::ProofManager116 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()
191 static TheoryProofEngine* getTheoryProofEngine();
396 …CTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); in printAtomMapping()417 …CTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); in printAtomMapping()
173 ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, in toStreamRecLFSC()736 ProofManager::getTheoryProofEngine()->printConstantDisequalityProof( in toStreamRecLFSC()
137 ProofManager::getTheoryProofEngine()->printConstantDisequalityProof( in toStreamRecLFSC()
938 ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id)); in finishInit()1003 ProofManager::currentPM()->getTheoryProofEngine()-> in finishInit()