std::vector<Node>& newSkolems,
bool reportDeps)
{
- Node itesRemoved = run(assertion, newAsserts, newSkolems, false, false);
+ TCtxStack ctx(&d_rtfc);
+ ctx.pushInitial(assertion);
+ Node itesRemoved = run(ctx, newAsserts, newSkolems);
// In some calling contexts, not necessary to report dependence information.
if (reportDeps && options::unsatCores())
{
return theory::TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get());
}
-Node RemoveTermFormulas::run(TNode node,
+Node RemoveTermFormulas::run(TCtxStack& ctx,
std::vector<theory::TrustNode>& output,
- std::vector<Node>& newSkolems,
- bool inQuant,
- bool inTerm)
+ std::vector<Node>& newSkolems)
{
- // Current node
- Debug("ite") << "removeITEs(" << node << ")" << " " << inQuant << " " << inTerm << endl;
-
- if( node.getKind()==kind::INST_PATTERN_LIST ){
+ Assert(!ctx.empty());
+ std::pair<Node, uint32_t> curr = ctx.getCurrent();
+ ctx.pop();
+ TNode node = curr.first;
+ if (node.getKind() == kind::INST_PATTERN_LIST)
+ {
return Node(node);
}
+ uint32_t cval = curr.second;
+ bool inQuant, inTerm;
+ RtfTermContext::getFlags(curr.second, inQuant, inTerm);
+ Debug("ite") << "removeITEs(" << node << ")"
+ << " " << inQuant << " " << inTerm << std::endl;
// The result may be cached already
- int cv = cacheVal( inQuant, inTerm );
- std::pair<Node, int> cacheKey(node, cv);
NodeManager *nodeManager = NodeManager::currentNM();
- TermFormulaCache::const_iterator i = d_tfCache.find(cacheKey);
- if (i != d_tfCache.end())
+ TermFormulaCache::const_iterator itc = d_tfCache.find(curr);
+ if (itc != d_tfCache.end())
{
- Node cached = (*i).second;
+ Node cached = (*itc).second;
Debug("ite") << "removeITEs: in-cache: " << cached << endl;
- return cached.isNull() ? Node(node) : cached;
+ return cached.isNull() ? Node(curr.first) : cached;
}
-
TypeNode nodeType = node.getType();
Node skolem;
Node newAssertion;
skolem = getSkolemForNode(node);
if (skolem.isNull())
{
+ Trace("rtf-proof-debug")
+ << "RemoveTermFormulas::run: make ITE skolem" << std::endl;
// Make the skolem to represent the ITE
SkolemManager* sm = nodeManager->getSkolemManager();
skolem = sm->mkPurifySkolem(
// we justify it internally
if (isProofEnabled())
{
+ Trace("rtf-proof-debug")
+ << "RemoveTermFormulas::run: justify " << newAssertion
+ << " with ITE axiom" << std::endl;
// ---------------------- REMOVE_TERM_FORMULA_AXIOM
// (ite node[0]
// (= node node[1]) ------------- MACRO_SR_PRED_INTRO
skolem = getSkolemForNode(node);
if (skolem.isNull())
{
+ Trace("rtf-proof-debug")
+ << "RemoveTermFormulas::run: make LAMBDA skolem" << std::endl;
// Make the skolem to represent the lambda
SkolemManager* sm = nodeManager->getSkolemManager();
skolem = sm->mkPurifySkolem(
// http://planetmath.org/hilbertsvarepsilonoperator.
if (!inQuant || !expr::hasFreeVar(node))
{
+ // NOTE: we can replace by t if body is of the form (and (= z t) ...)
skolem = getSkolemForNode(node);
if (skolem.isNull())
{
+ Trace("rtf-proof-debug")
+ << "RemoveTermFormulas::run: make WITNESS skolem" << std::endl;
// Make the skolem to witness the choice, which notice is handled
// as a special case within SkolemManager::mkPurifySkolem.
SkolemManager* sm = nodeManager->getSkolemManager();
// -------------------- SKOLEMIZE
// node[1] * { x -> skolem }
ProofGenerator* expg = sm->getProofGenerator(existsAssertion);
- if (expg != nullptr)
- {
- d_lp->addLazyStep(existsAssertion, expg);
- }
+ d_lp->addLazyStep(existsAssertion,
+ expg,
+ true,
+ "RemoveTermFormulas::run:skolem_pf",
+ false,
+ PfRule::WITNESS_AXIOM);
d_lp->addStep(newAssertion, PfRule::SKOLEMIZE, {existsAssertion}, {});
newAssertionPg = d_lp.get();
}
skolem = getSkolemForNode(node);
if (skolem.isNull())
{
+ Trace("rtf-proof-debug")
+ << "RemoveTermFormulas::run: make BOOLEAN_TERM_VARIABLE skolem"
+ << std::endl;
// Make the skolem to represent the Boolean term
// Skolems introduced for Boolean formulas appearing in terms have a
// special kind (BOOLEAN_TERM_VARIABLE) that ensures they are handled
// if the term should be replaced by a skolem
if( !skolem.isNull() ){
// Attach the skolem
- d_tfCache.insert(cacheKey, skolem);
+ d_tfCache.insert(curr, skolem);
+ // this must be done regardless of whether the assertion was new below,
+ // since a formula-term may rewrite to the same skolem in multiple contexts.
+ if (isProofEnabled())
+ {
+ // justify the introduction of the skolem
+ // ------------------- MACRO_SR_PRED_INTRO
+ // t = witness x. x=t
+ // The above step is trivial, since the skolems introduced above are
+ // all purification skolems. We record this equality in the term
+ // conversion proof generator.
+ d_tpg->addRewriteStep(node,
+ skolem,
+ PfRule::MACRO_SR_PRED_INTRO,
+ {},
+ {node.eqNode(skolem)},
+ cval);
+ }
// if the skolem was introduced in this call
if (!newAssertion.isNull())
{
+ Trace("rtf-proof-debug")
+ << "RemoveTermFormulas::run: setup proof for new assertion "
+ << newAssertion << std::endl;
// if proofs are enabled
if (isProofEnabled())
{
- // justify the introduction of the skolem
- // ------------------- MACRO_SR_PRED_INTRO
- // t = witness x. x=t
- // The above step is trivial, since the skolems introduced above are
- // all purification skolems. We record this equality in the term
- // conversion proof generator.
- d_tpg->addRewriteStep(node,
- skolem,
- PfRule::MACRO_SR_PRED_INTRO,
- {},
- {node.eqNode(skolem)});
// justify the axiom that defines the skolem, if not already done so
if (newAssertionPg == nullptr)
{
newAssertion, PfRule::MACRO_SR_PRED_INTRO, {}, {newAssertion});
}
}
- Debug("ite") << "*** term formula removal introduced " << skolem
- << " for " << node << std::endl;
+ Trace("rtf-debug") << "*** term formula removal introduced " << skolem
+ << " for " << node << std::endl;
// Remove ITEs from the new assertion, rewrite it and push it to the
// output
- newAssertion = run(newAssertion, output, newSkolems, false, false);
+ Node newAssertionPre = newAssertion;
+ TCtxStack cctx(&d_rtfc);
+ cctx.pushInitial(newAssertion);
+ newAssertion = run(cctx, output, newSkolems);
+
+ if (isProofEnabled())
+ {
+ if (newAssertionPre != newAssertion)
+ {
+ Trace("rtf-proof-debug")
+ << "RemoveTermFormulas::run: setup proof for processed new lemma"
+ << std::endl;
+ // for new assertions that rewrite recursively
+ Node naEq = newAssertionPre.eqNode(newAssertion);
+ d_lp->addLazyStep(naEq, d_tpg.get());
+ // ---------------- from lp ------------------------------- from tpg
+ // newAssertionPre newAssertionPre = newAssertion
+ // ------------------------------------------------------- EQ_RESOLVE
+ // newAssertion
+ d_lp->addStep(
+ newAssertion, PfRule::EQ_RESOLVE, {newAssertionPre, naEq}, {});
+ }
+ }
theory::TrustNode trna =
theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
+ Trace("rtf-proof-debug") << "Checking closed..." << std::endl;
+ trna.debugCheckClosed("rtf-proof-debug",
+ "RemoveTermFormulas::run:new_assert");
+
output.push_back(trna);
newSkolems.push_back(skolem);
}
return skolem;
}
- if (node.isClosure())
- {
- // Remember if we're inside a quantifier
- inQuant = true;
- }else if( !inTerm && hasNestedTermChildren( node ) ){
- // Remember if we're inside a term
- Debug("ite") << "In term because of " << node << " " << node.getKind() << std::endl;
- inTerm = true;
- }
-
// If not an ITE, go deep
- vector<Node> newChildren;
+ std::vector<Node> newChildren;
bool somethingChanged = false;
if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
newChildren.push_back(node.getOperator());
}
// Remove the ITEs from the children
- for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
- Node newChild = run(*it, output, newSkolems, inQuant, inTerm);
- somethingChanged |= (newChild != *it);
+ for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; i++)
+ {
+ ctx.pushChild(node, cval, i);
+ Node newChild = run(ctx, output, newSkolems);
+ somethingChanged |= (newChild != node[i]);
newChildren.push_back(newChild);
}
// If changes, we rewrite
if(somethingChanged) {
Node cached = nodeManager->mkNode(node.getKind(), newChildren);
- d_tfCache.insert(cacheKey, cached);
+ d_tfCache.insert(curr, cached);
return cached;
- } else {
- d_tfCache.insert(cacheKey, Node::null());
- return node;
}
+ d_tfCache.insert(curr, Node::null());
+ return node;
}
Node RemoveTermFormulas::getSkolemForNode(Node node) const
return Node::null();
}
-Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const {
+Node RemoveTermFormulas::replace(TNode node) const
+{
+ TCtxStack ctx(&d_rtfc);
+ ctx.pushInitial(node);
+ return replaceInternal(ctx);
+}
+
+Node RemoveTermFormulas::replaceInternal(TCtxStack& ctx) const
+{
+ // get the current node, tagged with a term context identifier
+ Assert(!ctx.empty());
+ std::pair<Node, uint32_t> curr = ctx.getCurrent();
+ ctx.pop();
+ TNode node = curr.first;
+
if( node.getKind()==kind::INST_PATTERN_LIST ){
return Node(node);
}
// Check the cache
- NodeManager *nodeManager = NodeManager::currentNM();
- int cv = cacheVal( inQuant, inTerm );
- TermFormulaCache::const_iterator i = d_tfCache.find(make_pair(node, cv));
- if (i != d_tfCache.end())
+ TermFormulaCache::const_iterator itc = d_tfCache.find(curr);
+ if (itc != d_tfCache.end())
{
- Node cached = (*i).second;
+ Node cached = (*itc).second;
return cached.isNull() ? Node(node) : cached;
}
- if (node.isClosure())
- {
- // Remember if we're inside a quantifier
- inQuant = true;
- }else if( !inTerm && hasNestedTermChildren( node ) ){
- // Remember if we're inside a term
- inTerm = true;
- }
-
vector<Node> newChildren;
bool somethingChanged = false;
if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
newChildren.push_back(node.getOperator());
}
// Replace in children
- for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
- Node newChild = replace(*it, inQuant, inTerm);
- somethingChanged |= (newChild != *it);
+ uint32_t cval = curr.second;
+ for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; i++)
+ {
+ ctx.pushChild(node, cval, i);
+ Node newChild = replaceInternal(ctx);
+ somethingChanged |= (newChild != node[i]);
newChildren.push_back(newChild);
}
// If changes, we rewrite
if(somethingChanged) {
- return nodeManager->mkNode(node.getKind(), newChildren);
- } else {
- return node;
+ return NodeManager::currentNM()->mkNode(node.getKind(), newChildren);
}
-}
-
-// returns true if the children of node should be considered nested terms
-bool RemoveTermFormulas::hasNestedTermChildren( TNode node ) {
- return theory::kindToTheoryId(node.getKind()) != theory::THEORY_BOOL
- && node.getKind() != kind::EQUAL && node.getKind() != kind::SEP_STAR
- && node.getKind() != kind::SEP_WAND
- && node.getKind() != kind::SEP_LABEL
- && node.getKind() != kind::BITVECTOR_EAGER_ATOM;
- // dont' worry about FORALL or EXISTS (handled separately)
+ return node;
}
Node RemoveTermFormulas::getAxiomFor(Node n)
nullptr,
TConvPolicy::FIXPOINT,
TConvCachePolicy::NEVER,
- "RemoveTermFormulas::TConvProofGenerator"));
+ "RemoveTermFormulas::TConvProofGenerator",
+ &d_rtfc));
d_lp.reset(new LazyCDProof(
d_pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof"));
}
#include "context/context.h"
#include "expr/lazy_proof.h"
#include "expr/node.h"
+#include "expr/term_context_stack.h"
#include "expr/term_conversion_proof_generator.h"
#include "smt/dump.h"
#include "theory/eager_proof_generator.h"
* Substitute under node using pre-existing cache. Do not remove
* any ITEs not seen during previous runs.
*/
- Node replace(TNode node, bool inQuant = false, bool inTerm = false) const;
+ Node replace(TNode node) const;
/** Returns true if e contains a term ite. */
bool containsTermITE(TNode e) const;
static Node getAxiomFor(Node n);
private:
- typedef context::
- CDInsertHashMap<std::pair<Node, int>,
- Node,
- PairHashFunction<Node, int, NodeHashFunction> >
- TermFormulaCache;
+ typedef context::CDInsertHashMap<
+ std::pair<Node, int32_t>,
+ Node,
+ PairHashFunction<Node, int32_t, NodeHashFunction> >
+ TermFormulaCache;
/** term formula removal cache
*
* This stores the results of term formula removal for inputs to the run(...)
*/
TermFormulaCache d_tfCache;
- /** return the integer cache value for the input flags to run(...) */
- static inline int cacheVal( bool inQuant, bool inTerm ) { return (inQuant ? 1 : 0) + 2*(inTerm ? 1 : 0); }
-
/** skolem cache
*
* This is a cache that maps terms to the skolem we use to replace them.
*/
inline Node getSkolemForNode(Node node) const;
- static bool hasNestedTermChildren( TNode node );
-
- /** A proof node manager */
+ /** Pointer to a proof node manager */
ProofNodeManager* d_pnm;
/**
* A proof generator for the term conversion.
* this class is responsible for.
*/
std::unique_ptr<LazyCDProof> d_lp;
+ /**
+ * The remove term formula context, which computes hash values for term
+ * contexts.
+ */
+ RtfTermContext d_rtfc;
/**
* Removes terms of the form (1), (2), (3) described above from node.
* inTerm is whether we are are processing node in a "term" position, that is, it is a subterm
* of a parent term that is not a Boolean connective.
*/
- Node run(TNode node,
+ Node run(TCtxStack& cxt,
std::vector<theory::TrustNode>& newAsserts,
- std::vector<Node>& newSkolems,
- bool inQuant,
- bool inTerm);
+ std::vector<Node>& newSkolems);
+ /** Replace internal */
+ Node replaceInternal(TCtxStack& ctx) const;
/** Whether proofs are enabled */
bool isProofEnabled() const;
projects / cvc5.git / commitdiff