diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/uf/proof_equality_engine.cpp | 54 | ||||
| -rw-r--r-- | src/theory/uf/proof_equality_engine.h | 10 |
2 files changed, 0 insertions, 64 deletions
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 323f8c6a2..00e4662f9 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -40,60 +40,6 @@ ProofEqEngine::ProofEqEngine(context::Context* c, d_false = nm->mkConst(false); } -bool ProofEqEngine::assertAssume(TNode lit) -{ - Trace("pfee") << "pfee::assertAssume " << lit << std::endl; - // don't need to explicitly add anything to the proof here, since ASSUME - // nodes are constructed lazily - TNode atom = lit.getKind() == NOT ? lit[0] : lit; - bool polarity = lit.getKind() != NOT; - - // Second, assert it directly to the equality engine, where it is its own - // explanation. Notice we do not reference count atom/lit. - if (atom.getKind() == EQUAL) - { - if (d_pfEnabled) - { - // If proofs are enabled, we check if lit is an assertion of the form - // (= P true), (= P false), (= false P) or (= true P). - // Such literals must be handled as a special case here, since equality - // with Boolean constants have a special status internally within equality - // engine. In particular, the proofs constructed by EqProof conversion - // always produce proofs involving equalities with Boolean constants, and - // whose assumptions are only of the form P or (not P). However, in the - // case that (= P true) (resp (= P false)) is itself an input to the - // equality engine, we will explain in terms of P (resp. (not P)), which - // leads to a bogus proof, typically encountered in - // ProofNodeManager::mkScope. - // - // To correct this, we add an explicit *fact* that P holds by (= P true) - // here. This means that EqProof conversion may generate a proof where - // the internal equality (= P true) is justified by assumption P, and that - // afterwards, P is explained in terms of the original (external) equality - // (= P true) by the step provided here. This means that the proof may end - // up using (= P true) in a roundabout way (through two redundant steps), - // but regardless this allows the core proof utilities (EqProof - // conversion, proof equality engine, lazy proof, etc.) to be unconcerned - // with this case. Multiple users of the proof equality engine - // (SharedTermDatabase and TheoryArrays) require this special case. - if (atom[0].getKind() == kind::CONST_BOOLEAN - || atom[1].getKind() == kind::CONST_BOOLEAN) - { - Node nlit = Rewriter::rewrite(lit); - if (!CDProof::isSame(lit, nlit)) - { - // use a rewrite step as a fact - std::vector<Node> pfChildren; - pfChildren.push_back(lit); - return assertFact(nlit, PfRule::MACRO_SR_PRED_ELIM, pfChildren, {}); - } - } - } - return d_ee.assertEquality(atom, polarity, lit); - } - return d_ee.assertPredicate(atom, polarity, lit); -} - bool ProofEqEngine::assertFact(Node lit, PfRule id, const std::vector<Node>& exp, diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index e1105623a..d80c1e7bc 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -87,16 +87,6 @@ class ProofEqEngine : public EagerProofGenerator EqualityEngine& ee, ProofNodeManager* pnm); ~ProofEqEngine() {} - //-------------------------- assert assumption - /** - * Assert literal lit by assumption to the underlying equality engine. It is - * its own explanation. - * - * @param lit The literal to assert to the equality engine - * @return true if this fact was processed by this method. If lit already - * holds in the equality engine, this method returns false. - */ - bool assertAssume(TNode lit); //-------------------------- assert fact /** * Assert the literal lit by proof step id, given explanation exp and |