Searched refs:getBitVectorProof (Results 1 – 3 of 3) sorted by relevance
120 proof::ResolutionBitVectorProof* ProofManager::getBitVectorProof() in getBitVectorProof() function in CVC4::ProofManager702 ProofManager::getBitVectorProof()->calculateAtomsInBitblastingProof(); in toStream()736 …if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof(… in toStream()737 ProofManager::getBitVectorProof()->printEmptyClauseProof(out, paren); in toStream()1044 …const std::set<Node>* additionalAtoms = ProofManager::getBitVectorProof()->getAtomsInBitblastingPr… in printGlobalLetMap()
194 static proof::ResolutionBitVectorProof* getBitVectorProof();
568 proof::BitVectorProof* bv = ProofManager::getBitVectorProof(); in finalizeBvConflicts()584 ProofManager::getBitVectorProof()->printBBDeclarationAndCnf(os, paren, map); in printTheoryLemmas()