Searched refs:addRewriteFilter (Results 1 – 4 of 4) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/proof/ |
| H A D | simplify_boolean_node.cpp | 65 ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str()); in simplifyBooleanNode()
76 ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str()); in simplifyBooleanNode()
87 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 | proof_manager.h | 284 void addRewriteFilter(const std::string &original, const std::string &substitute);
|
| H A D | theory_proof.cpp | 690 pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str()); in printTheoryLemmas()
812 pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str()); in printTheoryLemmas()
|
| H A D | proof_manager.cpp | 927 void ProofManager::addRewriteFilter(const std::string &original, const std::string &substitute) { in addRewriteFilter() function in CVC4::ProofManager
|