Home
last modified time | relevance | path

Searched refs:ProofManager (Results 1 – 25 of 34) sorted by relevance

12

/dports/math/cvc4/CVC4-1.7/src/proof/
H A Dproof_manager.cpp61 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 Dsimplify_boolean_node.cpp36 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 Dcnf_proof.cpp399 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 Dlfsc_proof_printer.cpp36 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 Darith_proof.cpp39 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 Dtheory_proof.cpp216 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 Duf_proof.cpp37 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 Darray_proof.cpp162 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 Dresolution_bitvector_proof.cpp281 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 Dproof_manager.h143 class ProofManager {
176 ProofManager(context::Context* context, ProofFormat format = LFSC);
177 ~ProofManager();
179 static ProofManager* currentPM();
H A Dbitvector_proof.cpp202 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 Dclausal_bitvector_proof.cpp55 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 DSolver.cc153 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 Dassertion_pipeline.cpp58 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 Dsmt_engine_scope.h27 class ProofManager; variable
37 ProofManager* currentProofManager();
H A Dsmt_engine.h62 class ProofManager; variable
95 ProofManager* currentProofManager();
147 ProofManager* d_proofManager;
396 friend ProofManager* ::CVC4::smt::currentProofManager();
H A Dsmt_engine_scope.cpp38 ProofManager* currentProofManager() { in currentProofManager()
H A Dterm_formula_removal.cpp47 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 Der_proof.cpp217 << 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 Dnon_clausal_simp.cpp106 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 Dtheory_proxy.cpp108 ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); in explainPropagation()
109 ProofManager::getCnfProof()->setProofRecipe(proofRecipe); in explainPropagation()
H A Dcryptominisat.cpp126 freshId = ClauseId(ProofManager::currentPM()->nextId()); in addClause()
/dports/math/cvc4/CVC4-1.7/src/proof/drat/
H A Ddrat_proof.cpp276 << ProofManager::getVarName(l.getSatVariable(), "bb") << ") "; in outputAsLfsc()
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dinstantiate.cpp565 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 Dfun_def_process.cpp87 PROOF( ProofManager::currentPM()->addDependence(new_q, assertions[i]); ); in simplify()
121 PROOF(ProofManager::currentPM()->addDependence(n, assertions[i]);); in simplify()

12