Searched refs:getCnfProof (Results 1 – 8 of 8) sorted by relevance
221 Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); in getTheoryForLemma()232 Assert (pm->getCnfProof()->haveProofRecipe(nodes)); in getTheoryForLemma()233 return pm->getCnfProof()->getProofRecipe(nodes).getTheory(); in getTheoryForLemma()463 Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); in dumpTheoryLemmas()471 LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(nodes); in dumpTheoryLemmas()558 ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode); in finalizeBvConflicts()606 Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); in printTheoryLemmas()617 LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(clause_expr_nodes); in printTheoryLemmas()626 pm->getCnfProof()->printClause(*clause, os, clause_paren); in printTheoryLemmas()732 ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode); in printTheoryLemmas()[all …]
93 static_cast<LFSCCnfProof*>(getCnfProof()), in getProof()104 CnfProof* ProofManager::getCnfProof() { in getCnfProof() function in CVC4::ProofManager399 if (!getCnfProof()->haveProofRecipe(lemma)) { in getLemmasInUnsatCore()404 recipe = getCnfProof()->getProofRecipe(lemma); in getLemmasInUnsatCore()418 Node node = getCnfProof()->getAtom(lit.getSatVariable()); in satClauseToNodeSet()454 if (!getCnfProof()->haveProofRecipe(currentLemma)) in getWeakestImplicantInUnsatCore()457 recipe = getCnfProof()->getProofRecipe(currentLemma); in getWeakestImplicantInUnsatCore()483 if (!getCnfProof()->haveProofRecipe(currentLemma)) in getWeakestImplicantInUnsatCore()486 recipe = getCnfProof()->getProofRecipe(currentLemma); in getWeakestImplicantInUnsatCore()
282 CnfProof* cnf = pm->getCnfProof(); in printTheoryLemmaProof()384 CnfProof* cnf = pm->getCnfProof(); in printTheoryLemmaProof()412 CnfProof* cnf = pm->getCnfProof(); in printTheoryLemmaProof()
202 CnfProof* getCnfProof() { return d_cnfProof.get(); } in getCnfProof() function
190 static CnfProof* getCnfProof();
108 ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); in explainPropagation()109 ProofManager::getCnfProof()->setProofRecipe(proofRecipe); in explainPropagation()
327 ProofManager::getCnfProof()->registerConvertedClause(id, true); in reason()333 ProofManager::getCnfProof()->popCurrentAssertion();); in reason()405 Node assertion = ProofManager::getCnfProof()->getCurrentAssertion(); in addClause_()406 Node def = ProofManager::getCnfProof()->getCurrentDefinition(); in addClause_()1038 PROOF(ProofManager::getCnfProof()->popCurrentAssertion();) in propagateTheory()1799 ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); in updateLemmas()1800 ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); in updateLemmas()1816 ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); in updateLemmas()1817 ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); in updateLemmas()
181 ProofManager::getCnfProof()->setProofRecipe(&proofRecipe); in registerLemmaRecipe()1458 ProofManager::getCnfProof()->setProofRecipe(&proofRecipe); in propagate()1914 PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe)); in conflict()1945 ProofManager::getCnfProof()->setProofRecipe(proofRecipe); in conflict()