/dports/math/cvc4/CVC4-1.7/src/proof/ |
H A D | proof_manager.cpp | 61 ProofManager::ProofManager(context::Context* context, ProofFormat format) in ProofManager() function in CVC4::ProofManager 76 ProofManager::~ProofManager() { in ~ProofManager() 82 ProofManager* ProofManager::currentPM() { in currentPM() 99 CoreSatProof* ProofManager::getSatProof() { in getSatProof() 104 CnfProof* ProofManager::getCnfProof() { in getCnfProof() 114 UFProof* ProofManager::getUfProof() { in getUfProof() 152 ProofManager* pm = currentPM(); in initCnfProof() 329 void ProofManager::traceUnsatCore() { in traceUnsatCore() 371 void ProofManager::constructSatProof() { in constructSatProof() 883 Node ProofManager::mkOp(TNode n) { in mkOp() [all …]
|
H A D | simplify_boolean_node.cpp | 36 if (!ProofManager::hasLitName(n)) in simplifyBooleanNode() 40 if (ProofManager::currentPM()->haveRewriteFilter(n.negate())) in simplifyBooleanNode() 44 std::string litName = ProofManager::getLitName(n.negate()); in simplifyBooleanNode() 62 std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); in simplifyBooleanNode() 73 std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); in simplifyBooleanNode() 113 ProofManager::currentPM()->addRewriteFilter(litName, newLitName.str()); in simplifyBooleanNode() 122 ProofManager::currentPM()->addRewriteFilter(litName, newLitName.str()); in simplifyBooleanNode() 131 ProofManager::currentPM()->addRewriteFilter(litName, newLitName.str()); in simplifyBooleanNode() 141 ProofManager::currentPM()->addRewriteFilter(litName, newLitName.str()); in simplifyBooleanNode() 147 std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); in simplifyBooleanNode() [all …]
|
H A D | cnf_proof.cpp | 399 os << " (\\ " << ProofManager::getVarName(var, d_name); in printAtomMapping() 400 os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; in printAtomMapping() 422 os << " (\\ " << ProofManager::getVarName(var, d_name); in printAtomMapping() 423 os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; in printAtomMapping() 533 os_base << ProofManager::getLitName(blit, d_name); in printCnfProofForClause() 594 os_main << ProofManager::getLitName(lit, d_name) << " "; in printCnfProofForClause() 774 os << ProofManager::getLitName(lit2, d_name); in printCnfProofForClause() 814 os_main << ProofManager::getLitName(lit1, d_name) << " "; in printCnfProofForClause() 864 …os << "(ast _ _ _ " << ProofManager::getAtomName(var, d_name) <<" (\\ " << ProofManager::getLitNam… in printClause() 867 …os << "(asf _ _ _ " << ProofManager::getAtomName(var, d_name) <<" (\\ " << ProofManager::getLitNam… in printClause() [all …]
|
H A D | lfsc_proof_printer.cpp | 36 os << ProofManager::getInputClauseName(id, satProof->getName()); in clauseName() 40 os << ProofManager::getLemmaClauseName(id, satProof->getName()); in clauseName() 44 os << ProofManager::getLearntClauseName(id, satProof->getName()); in clauseName() 75 << ProofManager::getVarName(v, satProof->getName()) << ")"; in printResolution() 117 out << ProofManager::getVarName(v, satProof->getName()) << ")"; in printAssumptionsResolution() 156 << ProofManager::getInputClauseName(*i, namingPrefix) << " "; in printSatInputProof() 169 << ProofManager::getInputClauseName(clauses[i], namingPrefix) << " "; in printCMapProof() 182 << ProofManager::getVarName(i->getSatVariable(), namingPrefix) << ") "; in printSatClause()
|
H A D | arith_proof.cpp | 39 if(ProofManager::currentPM()->hasOp(n1)) { in match() 40 n1 = ProofManager::currentPM()->lookupOp(n1); in match() 42 if(ProofManager::currentPM()->hasOp(n2)) { in match() 43 n2 = ProofManager::currentPM()->lookupOp(n2); in match() 50 if(ProofManager::currentPM()->hasOp(n2.getOperator())) { in match() 57 if(ProofManager::currentPM()->hasOp(n1.getOperator())) { in match() 79 toStreamLFSC(out, ProofManager::getArithProof(), *d_proof, map); in toStream() 366 if(ProofManager::currentPM()->hasOp(n1.getOperator())) { in toStreamRecLFSC() 380 if(ProofManager::currentPM()->hasOp(n2.getOperator())) { in toStreamRecLFSC() 407 out << ProofManager::getLitName(pf.d_node.negate()); in toStreamRecLFSC() [all …]
|
H A D | theory_proof.cpp | 216 ProofManager* pm = ProofManager::currentPM(); in getTheoryForLemma() 343 ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); in registerTermsFromAssertions() 344 ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); in registerTermsFromAssertions() 356 ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); in printAssertions() 357 ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); in printAssertions() 455 ProofManager* pm = ProofManager::currentPM(); in dumpTheoryLemmas() 592 ProofManager* pm = ProofManager::currentPM(); in printTheoryLemmas() 874 os << ProofManager::sanitize(term); in printCoreTerm() 1154 os << ProofManager::sanitize(term); in printOwnedTerm() 1246 os << "(% " << ProofManager::sanitize(term) << " (term "; in printTermDeclarations() [all …]
|
H A D | uf_proof.cpp | 37 toStreamLFSC(out, ProofManager::getUfProof(), *d_proof, map); in toStream() 206 b1 << ProofManager::currentPM()->mkOp(n1[side].getOperator()); in toStreamRecLFSC() 218 b2 << ProofManager::currentPM()->mkOp(n1[1-side].getOperator()); in toStreamRecLFSC() 275 if(ProofManager::currentPM()->hasOp(n1.getOperator())) { in toStreamRecLFSC() 289 if(ProofManager::currentPM()->hasOp(n2.getOperator())) { in toStreamRecLFSC() 317 out << ProofManager::getLitName(pf.d_node.negate()); in toStreamRecLFSC() 604 ProofManager::currentPM()->ensureLiteral( in registerTerm() 606 ProofManager::currentPM()->ensureLiteral( in registerTerm() 672 if (!ProofManager::currentPM()->wasPrinted(*it)) { in printSortDeclarations() 675 ProofManager::currentPM()->markPrinted(*it); in printSortDeclarations() [all …]
|
H A D | array_proof.cpp | 162 ProofManager::getLitName(n2[0]) << std::endl; in toStreamRecLFSC() 164 out << " " << ProofManager::getLitName(n2[0]); in toStreamRecLFSC() 450 out << ProofManager::getLitName(pf.d_node.negate()); in toStreamRecLFSC() 1051 out << ProofManager::getLitName(child_proof->d_node[0]); in toStreamRecLFSC() 1098 ProofManager::currentPM()->ensureLiteral( in registerTerm() 1100 ProofManager::currentPM()->ensureLiteral( in registerTerm() 1230 if (!ProofManager::currentPM()->wasPrinted(*it)) { in printSortDeclarations() 1233 ProofManager::currentPM()->markPrinted(*it); in printSortDeclarations() 1257 os << "(% " << ProofManager::sanitize(term) << " "; in printTermDeclarations() 1273 os << "(% " << ProofManager::sanitize(term) << " "; in printTermDeclarations() [all …]
|
H A D | resolution_bitvector_proof.cpp | 281 ProofManager* pm = ProofManager::currentPM(); in printTheoryLemmaProof() 383 ProofManager* pm = ProofManager::currentPM(); in printTheoryLemmaProof() 411 ProofManager* pm = ProofManager::currentPM(); in printTheoryLemmaProof() 443 os << ProofManager::getLitName(lemma[i]); in printTheoryLemmaProof()
|
H A D | proof_manager.h | 143 class ProofManager { 176 ProofManager(context::Context* context, ProofFormat format = LFSC); 177 ~ProofManager(); 179 static ProofManager* currentPM();
|
H A D | bitvector_proof.cpp | 202 os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")"; in printOwnedTerm() 211 if (ProofManager::getSkolemizationManager()->isSkolem(term)) { in printOwnedTerm() 212 os << ProofManager::sanitize(term); in printOwnedTerm() 214 os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")"; in printOwnedTerm() 366 …if ((it->isVariable() || it->isConst()) && !ProofManager::getSkolemizationManager()->isSkolem(*it)… in printTermDeclarations() 367 d_exprToVariableName[*it] = ProofManager::sanitize(*it); in printTermDeclarations() 711 os <<"(\\ " << ProofManager::getPreprocessedAssertionName(ait->second) <<"\n"; in printBitblasting()
|
H A D | clausal_bitvector_proof.cpp | 55 int trueClauseId = ClauseId(ProofManager::currentPM()->nextId()); in initCnfProof() 63 int falseClauseId = ClauseId(ProofManager::currentPM()->nextId()); in initCnfProof()
|
/dports/math/cvc4/CVC4-1.7/src/prop/minisat/core/ |
H A D | Solver.cc | 153 PROOF(ProofManager::currentPM()->initSatProof(this);) in Solver() 325 PROOF(ClauseId id = ProofManager::getSatProof()->registerClause( in reason() 333 ProofManager::getCnfProof()->popCurrentAssertion();); in reason() 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() 1038 PROOF(ProofManager::getCnfProof()->popCurrentAssertion();) in propagateTheory() 1304 } ProofManager::getSatProof() in search() 1306 ProofManager::getSatProof() in search() [all …]
|
/dports/math/cvc4/CVC4-1.7/src/preprocessing/ |
H A D | assertion_pipeline.cpp | 58 PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]);); in replace() 66 PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]); in replace() 69 ProofManager::currentPM()->addDependence(n, addnDep); in replace() 78 : ns) { ProofManager::currentPM()->addDependence(n, d_nodes[i]); }); in replace()
|
/dports/math/cvc4/CVC4-1.7/src/smt/ |
H A D | smt_engine_scope.h | 27 class ProofManager; variable 37 ProofManager* currentProofManager();
|
H A D | smt_engine.h | 62 class ProofManager; variable 95 ProofManager* currentProofManager(); 147 ProofManager* d_proofManager; 396 friend ProofManager* ::CVC4::smt::currentProofManager();
|
H A D | smt_engine_scope.cpp | 38 ProofManager* currentProofManager() { in currentProofManager()
|
H A D | term_formula_removal.cpp | 47 PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); ) in run() 49 PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); ) in run()
|
/dports/math/cvc4/CVC4-1.7/src/proof/er/ |
H A D | er_proof.cpp | 217 << ProofManager::getVarName(def.d_oldLiteral.getSatVariable(), "bb") in outputAsLfsc() 301 os << ProofManager::getVarName(pivotVar, "bb"); in outputAsLfsc() 380 o << ProofManager::getInputClauseName(d_inputClauseIds[i - 1], "bb"); in writeIdForClauseProof()
|
/dports/math/cvc4/CVC4-1.7/src/preprocessing/passes/ |
H A D | non_clausal_simp.cpp | 106 PROOF(ProofManager::currentPM()->addDependence(n, Node::null())); in applyInternal() 168 PROOF(ProofManager::currentPM()->addDependence(n, Node::null())); in applyInternal() 211 PROOF(ProofManager::currentPM()->addDependence(n, Node::null())); in applyInternal()
|
/dports/math/cvc4/CVC4-1.7/src/prop/ |
H A D | theory_proxy.cpp | 108 ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); in explainPropagation() 109 ProofManager::getCnfProof()->setProofRecipe(proofRecipe); in explainPropagation()
|
H A D | cryptominisat.cpp | 126 freshId = ClauseId(ProofManager::currentPM()->nextId()); in addClause()
|
/dports/math/cvc4/CVC4-1.7/src/proof/drat/ |
H A D | drat_proof.cpp | 276 << ProofManager::getVarName(l.getSatVariable(), "bb") << ") "; in outputAsLfsc()
|
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
H A D | instantiate.cpp | 565 if (!ProofManager::currentPM()->unsatCoreAvailable()) in getUnsatCoreLemmas() 573 ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS, in getUnsatCoreLemmas() 595 Node n = ProofManager::currentPM()->getWeakestImplicantInUnsatCore( in getUnsatCoreLemmas()
|
H A D | fun_def_process.cpp | 87 PROOF( ProofManager::currentPM()->addDependence(new_q, assertions[i]); ); in simplify() 121 PROOF(ProofManager::currentPM()->addDependence(n, assertions[i]);); in simplify()
|