Searched refs:getSatProof (Results 1 – 12 of 12) sorted by relevance
278 if(d_bvp){ d_bvp->getSatProof()->finalizeProof(cr); } in addClause_()297 d_bvp->getSatProof()->finalizeProof(confl); in addClause_()317 if(d_bvp){ d_bvp->getSatProof()->markDeleted(cr); } in detachClause()428 if(d_bvp){ d_bvp->getSatProof()->startResChain(confl); } in analyze()619 if(d_bvp){d_bvp->getSatProof()->resolveOutUnit(~p);} in analyzeFinal2()630 d_bvp->getSatProof()->resolveOutUnit(c[j]); in analyzeFinal2()701 d_bvp->getSatProof()->resolveOutUnit(c[j]); in analyzeFinal()781 if(d_bvp){d_bvp->getSatProof()->registerAssumption(var);} in addMarkerLiteral()1007 d_bvp->getSatProof()->endResChain(id); in search()1325 d_bvp->getSatProof()->registerTrueLit(mkLit(varTrue, false)); in setProofLog()[all …]
325 PROOF(ClauseId id = ProofManager::getSatProof()->registerClause( in reason()451 PROOF( ProofManager::getSatProof()->finalizeProof(cr); ) in addClause_()474 id = ProofManager::getSatProof()->storeUnitConflict( in addClause_()476 ProofManager::getSatProof()->finalizeProof( in addClause_()481 ProofManager::getSatProof()->finalizeProof(confl); in addClause_()510 PROOF( ProofManager::getSatProof()->markDeleted(cr); ); in detachClause()710 PROOF( ProofManager::getSatProof()->startResChain(confl); ) in analyze()753 PROOF(ProofManager::getSatProof()->resolveOutUnit(q);) in analyze()1304 } ProofManager::getSatProof() in search()1306 ProofManager::getSatProof() in search()[all …]
104 CVC3::Proof getSatProof(CNF_Manager*, CVC3::TheoryCore*) ;
172 virtual CVC3::Proof getSatProof(CNF_Manager*, CVC3::TheoryCore*) = 0 ;
87 CVC3::Proof getSatProof(CNF_Manager*, CVC3::TheoryCore*);
61 BVSatProof* getSatProof();
189 static CoreSatProof* getSatProof();
76 BVSatProof* ResolutionBitVectorProof::getSatProof() in getSatProof() function in CVC4::proof::ResolutionBitVectorProof
92 static_cast<CoreSatProof*>(getSatProof()), in getProof()99 CoreSatProof* ProofManager::getSatProof() { in getSatProof() function in CVC4::ProofManager
378 CVC3::Proof DPLLTMiniSat::getSatProof(CNF_Manager* cnfManager, CVC3::TheoryCore* core){ in getSatProof() function in DPLLTMiniSat
522 CVC3::Proof DPLLTBasic::getSatProof(CNF_Manager* cnfManager, CVC3::TheoryCore* core){ in getSatProof() function in DPLLTBasic
719 Proof pf = d_dpllt->getSatProof(d_cnfManager, d_core); in check()