namespace CVC4 {
+std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol)
+{
+ switch (tcpol)
+ {
+ case TConvPolicy::FIXPOINT: out << "FIXPOINT"; break;
+ case TConvPolicy::ONCE: out << "ONCE"; break;
+ default: out << "TConvPolicy:unknown"; break;
+ }
+ return out;
+}
+
TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm,
- context::Context* c)
- : d_proof(pnm, nullptr, c), d_rewriteMap(c ? c : &d_context)
+ context::Context* c,
+ TConvPolicy tpol)
+ : d_proof(pnm, nullptr, c), d_rewriteMap(c ? c : &d_context), d_policy(tpol)
{
}
void TConvProofGenerator::addRewriteStep(Node t, Node s, ProofGenerator* pg)
{
- // should not rewrite term more than once
- Assert(!hasRewriteStep(t));
- Node eq = t.eqNode(s);
- d_proof.addLazyStep(eq, pg);
- d_rewriteMap[t] = s;
+ Node eq = registerRewriteStep(t, s);
+ if (!eq.isNull())
+ {
+ d_proof.addLazyStep(eq, pg);
+ }
}
void TConvProofGenerator::addRewriteStep(Node t, Node s, ProofStep ps)
{
- // should not rewrite term more than once
- Assert(!hasRewriteStep(t));
- Node eq = t.eqNode(s);
- d_proof.addStep(eq, ps);
- d_rewriteMap[t] = s;
+ Node eq = registerRewriteStep(t, s);
+ if (!eq.isNull())
+ {
+ d_proof.addStep(eq, ps);
+ }
}
void TConvProofGenerator::addRewriteStep(Node t,
const std::vector<Node>& children,
const std::vector<Node>& args)
{
- // should not rewrite term more than once
- Assert(!hasRewriteStep(t));
- Node eq = t.eqNode(s);
- d_proof.addStep(eq, id, children, args);
- d_rewriteMap[t] = s;
+ Node eq = registerRewriteStep(t, s);
+ if (!eq.isNull())
+ {
+ d_proof.addStep(eq, id, children, args);
+ }
}
bool TConvProofGenerator::hasRewriteStep(Node t) const
return !getRewriteStep(t).isNull();
}
+Node TConvProofGenerator::registerRewriteStep(Node t, Node s)
+{
+ if (t == s)
+ {
+ return Node::null();
+ }
+ // should not rewrite term to two different things
+ if (!getRewriteStep(t).isNull())
+ {
+ Assert(getRewriteStep(t) == s);
+ return Node::null();
+ }
+ d_rewriteMap[t] = s;
+ return t.eqNode(s);
+}
+
std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
{
Trace("tconv-pf-gen") << "TConvProofGenerator::getProofFor: " << f
Assert(false);
return nullptr;
}
- std::shared_ptr<ProofNode> pf = getProofForRewriting(f[0]);
- if (pf == nullptr)
- {
- // failed to generate proof
- Trace("tconv-pf-gen") << "...failed to get proof" << std::endl;
- Assert(false);
- return pf;
- }
- if (pf->getResult() != f)
+ // we use the existing proofs
+ LazyCDProof lpf(d_proof.getManager(), &d_proof);
+ Node conc = getProofForRewriting(f[0], lpf);
+ if (conc != f)
{
Trace("tconv-pf-gen") << "...failed, mismatch: returned proof concludes "
- << pf->getResult() << std::endl;
+ << conc << ", expected " << f << std::endl;
Assert(false);
return nullptr;
}
Trace("tconv-pf-gen") << "... success" << std::endl;
- return pf;
+ return lpf.getProofFor(f);
}
-std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node t)
+Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf)
{
- // we use the existing proofs
- LazyCDProof pf(d_proof.getManager(), &d_proof);
NodeManager* nm = NodeManager::currentNM();
// Invariant: if visited[t] = s or rewritten[t] = s and t,s are distinct,
// then pf is able to generate a proof of t=s.
Node rcur = getRewriteStep(cur);
if (!rcur.isNull())
{
- // d_proof should have a proof of cur = rcur. Hence there is nothing
- // to do here, as pf will reference prg to get the proof from d_proof.
- // It may be the case that rcur also rewrites, thus we cannot assign
- // the final rewritten form for cur yet. Instead we revisit cur after
- // finishing visiting rcur.
- rewritten[cur] = rcur;
- visit.push_back(cur);
- visit.push_back(rcur);
+ // d_proof has a proof of cur = rcur. Hence there is nothing
+ // to do here, as pf will reference d_proof to get its proof.
+ if (d_policy == TConvPolicy::FIXPOINT)
+ {
+ // It may be the case that rcur also rewrites, thus we cannot assign
+ // the final rewritten form for cur yet. Instead we revisit cur after
+ // finishing visiting rcur.
+ rewritten[cur] = rcur;
+ visit.push_back(cur);
+ visit.push_back(rcur);
+ }
+ else
+ {
+ Assert(d_policy == TConvPolicy::ONCE);
+ // not rewriting again, rcur is final
+ visited[cur] = rcur;
+ }
}
else
{
itr = rewritten.find(cur);
if (itr != rewritten.end())
{
+ // only can generate partially rewritten nodes when rewrite again is
+ // true.
+ Assert(d_policy != TConvPolicy::ONCE);
// if it was rewritten, check the status of the rewritten node,
// which should be finished now
Node rcur = itr->second;
pf.addStep(result, PfRule::CONG, pfChildren, pfArgs);
}
// did we rewrite ret (at post-rewrite)?
- Node rret = getRewriteStep(ret);
+ Node rret;
+ // only if not ONCE policy, which only does pre-rewrite
+ if (d_policy != TConvPolicy::ONCE)
+ {
+ rret = getRewriteStep(ret);
+ }
if (!rret.isNull())
{
if (cur != ret)
} while (!visit.empty());
Assert(visited.find(t) != visited.end());
Assert(!visited.find(t)->second.isNull());
- // make the overall proof
- Node teq = t.eqNode(visited[t]);
- return pf.getProofFor(teq);
+ // return the conclusion of the overall proof
+ return t.eqNode(visited[t]);
}
Node TConvProofGenerator::getRewriteStep(Node t) const
namespace CVC4 {
+/** A policy for how rewrite steps are applied in TConvProofGenerator */
+enum class TConvPolicy : uint32_t
+{
+ // steps are applied to fix-point, common use case is PfRule::REWRITE
+ FIXPOINT,
+ // steps are applied once at pre-rewrite, common use case is PfRule::SUBS
+ ONCE,
+};
+/** Writes a term conversion policy name to a stream. */
+std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol);
+
/**
* The term conversion proof generator.
*
* @param pnm The proof node manager for constructing ProofNode objects.
* @param c The context that this class depends on. If none is provided,
* this class is context-independent.
+ * @param tpol The policy for applying rewrite steps of this class. For
+ * details, see d_policy.
*/
- TConvProofGenerator(ProofNodeManager* pnm, context::Context* c = nullptr);
+ TConvProofGenerator(ProofNodeManager* pnm,
+ context::Context* c = nullptr,
+ TConvPolicy pol = TConvPolicy::FIXPOINT);
~TConvProofGenerator();
/**
* Add rewrite step t --> s based on proof generator.
* t = t', where t' is the result of rewriting t based on the rewrite steps
* registered to this class.
*
- * @param f The fact to get the proof for.
+ * @param f The equality fact to get the proof for.
* @return The proof for f.
*/
std::shared_ptr<ProofNode> getProofFor(Node f) override;
/** map to rewritten forms */
NodeNodeMap d_rewriteMap;
/**
- * Get the proof for term t. Returns a proof of t = t' where t' is the
- * result of rewriting t based on the rewrite steps registered to this class.
+ * Policy for how rewrites are applied to terms. As a simple example, say we
+ * have registered the rewrite steps:
+ * addRewriteStep( a, f(c), p1 )
+ * addRewriteStep( c, d, p2 )
+ * Then getProofForRewriting(f(a,c),pf) returns a proof of:
+ * f(a,c) = f(f(d),d) if d_policy is FIXPOINT,
+ * f(a,c) = f(f(c),d) if d_policy is ONCE.
+ */
+ TConvPolicy d_policy;
+ /**
+ * Adds a proof of t = t' to the proof pf where t' is the result of rewriting
+ * t based on the rewrite steps registered to this class. This method then
+ * returns the proved equality t = t'.
+ */
+ Node getProofForRewriting(Node t, LazyCDProof& pf);
+ /**
+ * Register rewrite step, returns the equality t=s if t is distinct from s
+ * and a rewrite step has not already been registered for t.
*/
- std::shared_ptr<ProofNode> getProofForRewriting(Node t);
+ Node registerRewriteStep(Node t, Node s);
};
} // namespace CVC4
projects / cvc5.git / commitdiff