summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/proof_node_manager.cpp75
-rw-r--r--src/theory/uf/proof_equality_engine.cpp54
-rw-r--r--src/theory/uf/proof_equality_engine.h10
3 files changed, 57 insertions, 82 deletions
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index 4875b7c46..0d13531a5 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -16,6 +16,7 @@
#include "expr/proof.h"
#include "expr/proof_node_algorithm.h"
+#include "theory/rewriter.h"
using namespace CVC4::kind;
@@ -65,6 +66,13 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
Trace("pnm-scope") << "ProofNodeManager::mkScope " << assumps << std::endl;
// we first ensure the assumptions are flattened
std::unordered_set<Node, NodeHashFunction> ac{assumps.begin(), assumps.end()};
+ // map from the rewritten form of assumptions to the original. This is only
+ // computed in the rare case when we need rewriting to match the
+ // assumptions. An example of this is for Boolean constant equalities in
+ // scoped proofs from the proof equality engine.
+ std::unordered_map<Node, Node, NodeHashFunction> acr;
+ // whether we have compute the map above
+ bool computedAcr = false;
// The free assumptions of the proof
std::map<Node, std::vector<ProofNode*>> famap;
@@ -83,30 +91,61 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
// otherwise it may be due to symmetry?
Node aeqSym = CDProof::getSymmFact(a);
Trace("pnm-scope") << " - try sym " << aeqSym << "\n";
- if (!aeqSym.isNull())
+ Node aMatch;
+ if (!aeqSym.isNull() && ac.count(aeqSym))
{
- if (ac.count(aeqSym))
+ Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a
+ << " for " << fa.second.size() << " proof nodes"
+ << std::endl;
+ aMatch = aeqSym;
+ }
+ else
+ {
+ // Otherwise, may be derivable by rewriting. Note this is used in
+ // ensuring that proofs from the proof equality engine that involve
+ // equality with Boolean constants are closed.
+ if (!computedAcr)
{
- Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a
- << " for " << fa.second.size() << " proof nodes"
- << std::endl;
- std::shared_ptr<ProofNode> pfaa = mkAssume(aeqSym);
- for (ProofNode* pfs : fa.second)
+ computedAcr = true;
+ for (const Node& acc : ac)
{
- Assert(pfs->getResult() == a);
- // must correct the orientation on this leaf
- std::vector<std::shared_ptr<ProofNode>> children;
- children.push_back(pfaa);
- std::vector<Node> args;
- args.push_back(a);
- updateNode(pfs, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
+ Node accr = theory::Rewriter::rewrite(acc);
+ if (accr != acc)
+ {
+ acr[accr] = acc;
+ }
}
- Trace("pnm-scope") << "...finished" << std::endl;
- acu.insert(aeqSym);
- continue;
}
+ Node ar = theory::Rewriter::rewrite(a);
+ std::unordered_map<Node, Node, NodeHashFunction>::iterator itr =
+ acr.find(ar);
+ if (itr != acr.end())
+ {
+ aMatch = itr->second;
+ }
+ }
+
+ // if we found a match either by symmetry or rewriting, then we connect
+ // the assumption here.
+ if (!aMatch.isNull())
+ {
+ std::shared_ptr<ProofNode> pfaa = mkAssume(aMatch);
+ // must correct the orientation on this leaf
+ std::vector<std::shared_ptr<ProofNode>> children;
+ children.push_back(pfaa);
+ std::vector<Node> args;
+ args.push_back(a);
+ for (ProofNode* pfs : fa.second)
+ {
+ Assert(pfs->getResult() == a);
+ updateNode(pfs, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
+ }
+ Trace("pnm-scope") << "...finished" << std::endl;
+ acu.insert(aMatch);
+ continue;
}
- // All free assumptions should be arguments to SCOPE.
+ // If we did not find a match, it is an error, since all free assumptions
+ // should be arguments to SCOPE.
std::stringstream ss;
bool dumpProofTraceOn = Trace.isOn("dump-proof-error");
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback