| /dports/math/cvc4/CVC4-1.7/src/proof/ |
| H A D | proof_manager.cpp | 87 if (!currentPM()->d_fullProof) in getProof()
96 return *(currentPM()->d_fullProof); in getProof()
100 Assert (currentPM()->d_satProof); in getSatProof()
101 return currentPM()->d_satProof; in getSatProof()
105 Assert (currentPM()->d_cnfProof); in getCnfProof()
106 return currentPM()->d_cnfProof; in getCnfProof()
111 return currentPM()->d_theoryProof; in getTheoryProofEngine()
152 ProofManager* pm = currentPM(); in initCnfProof()
216 if (currentPM()->d_assertionFilters.find(node) != currentPM()->d_assertionFilters.end()) { in getPreprocessedAssertionName()
241 if (currentPM()->d_rewriteFilters.find(litName) != currentPM()->d_rewriteFilters.end()) { in getLitName()
[all …]
|
| H A D | simplify_boolean_node.cpp | 40 if (ProofManager::currentPM()->haveRewriteFilter(n.negate())) in simplifyBooleanNode()
65 ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str()); in simplifyBooleanNode()
76 ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str()); 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()
150 ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str()); in simplifyBooleanNode()
158 ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str()); in simplifyBooleanNode()
166 ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str()); in simplifyBooleanNode()
[all …]
|
| 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()
51 return n1 == ProofManager::currentPM()->lookupOp(n2.getOperator()); in match()
57 if(ProofManager::currentPM()->hasOp(n1.getOperator())) { in match()
58 return n2 == ProofManager::currentPM()->lookupOp(n1.getOperator()); in match()
299 b1 << ProofManager::currentPM()->mkOp(n1[side].getOperator()); in toStreamRecLFSC()
366 if(ProofManager::currentPM()->hasOp(n1.getOperator())) { 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()
357 ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); in printAssertions()
455 ProofManager* pm = ProofManager::currentPM(); in dumpTheoryLemmas()
558 ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode); in finalizeBvConflicts()
592 ProofManager* pm = ProofManager::currentPM(); in printTheoryLemmas()
732 ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode); in printTheoryLemmas()
1024 ProofManager::currentPM()->getLogicInfo(), in printTheoryLemmaProof()
1028 ProofManager::currentPM()->getLogicInfo(), in printTheoryLemmaProof()
[all …]
|
| H A D | uf_proof.cpp | 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()
276 b1.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>()); in toStreamRecLFSC()
289 if(ProofManager::currentPM()->hasOp(n2.getOperator())) { in toStreamRecLFSC()
290 b2.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>()); 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()
|
| 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()
|
| H A D | array_proof.cpp | 273 b1 << ProofManager::currentPM()->mkOp(n1[side].getOperator()); in toStreamRecLFSC()
297 b2 << ProofManager::currentPM()->mkOp(n1[1-side].getOperator()); in toStreamRecLFSC()
394 if(ProofManager::currentPM()->hasOp(n1.getOperator())) { in toStreamRecLFSC()
395 b1.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>()); in toStreamRecLFSC()
421 if(ProofManager::currentPM()->hasOp(n2.getOperator())) { in toStreamRecLFSC()
422 b2.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>()); 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()
|
| 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()
|
| H A D | proof_manager.h | 179 static ProofManager* currentPM();
|
| H A D | sat_proof_implementation.h | 510 ClauseId newId = ProofManager::currentPM()->nextId(); in registerClause()
544 ClauseId newId = ProofManager::currentPM()->nextId(); in registerUnitClause()
613 ClauseId new_id = ProofManager::currentPM()->nextId(); in registerAssumptionConflict()
|
| H A D | cnf_proof.cpp | 396 …LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngin… in printAtomMapping()
417 …LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngin… in printAtomMapping()
|
| /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/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()
|
| H A D | miplib_trick.cpp | 527 PROOF(ProofManager::currentPM()->addDependence(n, Node::null())); in applyInternal()
596 PROOF(ProofManager::currentPM()->addDependence(newAssertion, in applyInternal()
|
| H A D | quantifier_macros.cpp | 104 PROOF(ProofManager::currentPM()->addDependence(curr, assertions[i]); in simplify()
108 ProofManager::currentPM()->addDependence( in simplify()
|
| /dports/math/cvc4/CVC4-1.7/src/smt/ |
| 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()
|
| H A D | smt_engine.cpp | 938 ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id)); in finishInit()
1000 PROOF( ProofManager::currentPM()->setLogic(d_logic); ); in finishInit()
1003 ProofManager::currentPM()->getTheoryProofEngine()-> in finishInit()
3192 ProofManager::currentPM()->addAssertion(d_assertions[i].toExpr()); in processAssertions()
3552 ProofManager::currentPM()->addCoreAssertion(n.toExpr()); in addFormula()
3556 ProofManager::currentPM()->addDependence(n, Node::null()); in addFormula()
3562 ProofManager::currentPM()->addUnsatCore(n.toExpr()); in addFormula()
|
| /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()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/ |
| H A D | cryptominisat.cpp | 126 freshId = ClauseId(ProofManager::currentPM()->nextId()); in addClause()
|
| H A D | prop_engine.cpp | 113 ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext); in PropEngine()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/strings/ |
| H A D | theory_strings_preprocess.cpp | 635 PROOF( ProofManager::currentPM()->addDependence( res, vec_node[i] ); ); in processAssertions()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | equality_engine.cpp | 1057 eqp->d_node = ProofManager::currentPM()->mkOp(d_nodes[t1Id]); in getExplanation()
1167 … ProofManager::currentPM()->mkOp(d_nodes[f1.a]), in getExplanation()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/minisat/core/ |
| H A D | Solver.cc | 153 PROOF(ProofManager::currentPM()->initSatProof(this);) in Solver()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | theory_engine.cpp | 340 ProofManager::currentPM()->initTheoryProofEngine(); in TheoryEngine()
|