Home
last modified time | relevance | path

Searched refs:LemmaProofRecipe (Results 1 – 9 of 9) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/proof/
H A Dlemma_proof.cpp154 LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteBegin() const { in rewriteBegin()
158 LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteEnd() const { in rewriteEnd()
162 LemmaProofRecipe::iterator LemmaProofRecipe::begin() { in begin()
166 LemmaProofRecipe::iterator LemmaProofRecipe::end() { in end()
170 LemmaProofRecipe::const_iterator LemmaProofRecipe::begin() const { in begin()
174 LemmaProofRecipe::const_iterator LemmaProofRecipe::end() const { in end()
178 bool LemmaProofRecipe::operator<(const LemmaProofRecipe& other) const { in operator <()
182 bool LemmaProofRecipe::simpleLemma() const { in simpleLemma()
186 bool LemmaProofRecipe::compositeLemma() const { in compositeLemma()
190 const LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) const { in getStep()
[all …]
H A Dlemma_proof.h30 class LemmaProofRecipe {
92 bool operator<(const LemmaProofRecipe& other) const;
109 std::ostream& operator<<(std::ostream & out, const LemmaProofRecipe::ProofStep & step);
111 std::ostream& operator<<(std::ostream & out, const LemmaProofRecipe & recipe);
H A Dcnf_proof.h48 typedef std::map<std::set<Node>, LemmaProofRecipe> LemmaToRecipe;
149 void setProofRecipe(LemmaProofRecipe* proofRecipe);
150 LemmaProofRecipe getProofRecipe(const std::set<Node> &lemma);
H A Dcnf_proof.cpp169 LemmaProofRecipe CnfProof::getProofRecipe(const std::set<Node> &lemma) { in getProofRecipe()
216 void CnfProof::setProofRecipe(LemmaProofRecipe* proofRecipe) { in setProofRecipe()
304 LemmaProofRecipe recipe = getProofRecipe(clause_expr_nodes); in collectAtomsAndRewritesForLemmas()
307 const LemmaProofRecipe::ProofStep* proofStep = recipe.getStep(i); in collectAtomsAndRewritesForLemmas()
322 LemmaProofRecipe::RewriteIterator rewriteIt; in collectAtomsAndRewritesForLemmas()
H A Dtheory_proof.cpp471 LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(nodes); in dumpTheoryLemmas()
506 … LemmaProofRecipe recipe = ProofManager::currentPM()->getCnfProof()->getProofRecipe(conflictNodes); in finalizeBvConflicts()
514 const LemmaProofRecipe::ProofStep* currentStep = recipe.getStep(i); in finalizeBvConflicts()
617 LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(clause_expr_nodes); in printTheoryLemmas()
712 const LemmaProofRecipe::ProofStep* currentStep = recipe.getStep(i); in printTheoryLemmas()
H A Dproof_manager.cpp398 LemmaProofRecipe recipe; in getLemmasInUnsatCore()
453 LemmaProofRecipe recipe; in getWeakestImplicantInUnsatCore()
482 LemmaProofRecipe recipe; in getWeakestImplicantInUnsatCore()
/dports/math/cvc4/CVC4-1.7/src/prop/
H A Dtheory_proxy.cpp102 LemmaProofRecipe* proofRecipe = NULL; in explainPropagation()
103 PROOF(proofRecipe = new LemmaProofRecipe;); in explainPropagation()
/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dtheory_engine.cpp154 LemmaProofRecipe proofRecipe; in registerLemmaRecipe()
156 LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode); in registerLemmaRecipe()
1450 LemmaProofRecipe proofRecipe; in propagate()
1454 LemmaProofRecipe::ProofStep proofStep(theory, emptyNode); in propagate()
1620 LemmaProofRecipe::ProofStep proofStep(theoryOf(atom)->getId(), emptyNode); in getExplanationAndRecipe()
1678 LemmaProofRecipe::ProofStep proofStep(explainer, emptyNode); in getExplanationAndRecipe()
1693 LemmaProofRecipe *dontCareRecipe = NULL; in getExplanation()
1889 LemmaProofRecipe* proofRecipe = NULL; in conflict()
1891 proofRecipe = new LemmaProofRecipe; in conflict()
1893 LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode); in conflict()
[all …]
H A Dtheory_engine.h55 class LemmaProofRecipe; variable
608 …void getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* lemmaProofRe…
735 Node getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe);