diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 09076d29e..5c8be98b3 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1810,8 +1810,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, // Run theory preprocessing, maybe Node ppNode = preprocess ? this->preprocess(node) : Node(node); - - if (d_lazyProof!=nullptr) + + if (d_lazyProof != nullptr) { // FIXME } @@ -1823,8 +1823,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, d_tform_remover.run(additionalLemmas.ref(), additionalLemmas.getIteSkolemMap()); Debug("ite") << "..done " << additionalLemmas[0] << std::endl; - - if (d_lazyProof!=nullptr) + + if (d_lazyProof != nullptr) { // FIXME } @@ -1953,13 +1953,13 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { if (d_lazyProof != nullptr) { - if (fullConflict!=conflict) + if (fullConflict != conflict) { // store the explicit step processTrustNode(tncExp, THEORY_BUILTIN); } Node fullConflictNeg = fullConflict.notNode(); - // ------------------------- explained ---------- from theory + // ------------------------- explained ---------- from theory // fullConflict => conflict ~conflict // ----------------------------------------------- MACRO_SR_PRED_TRANSFORM // ~fullConflict @@ -1969,7 +1969,8 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { std::vector<Node> args; args.push_back(fullConflictNeg); args.push_back(mkMethodId(MethodId::SB_PREDICATE)); - d_lazyProof->addStep(fullConflictNeg, PfRule::MACRO_SR_PRED_TRANSFORM, children, args); + d_lazyProof->addStep( + fullConflictNeg, PfRule::MACRO_SR_PRED_TRANSFORM, children, args); } Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; |