std::vector<Node>& newSkolems,
bool reportDeps)
{
- TCtxStack ctx(&d_rtfc);
- ctx.pushInitial(assertion);
- Node itesRemoved = run(ctx, newAsserts, newSkolems);
+ Node itesRemoved = runInternal(assertion, 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(TCtxStack& ctx,
- std::vector<theory::TrustNode>& output,
- std::vector<Node>& newSkolems)
+Node RemoveTermFormulas::runInternal(Node assertion,
+ std::vector<theory::TrustNode>& output,
+ std::vector<Node>& newSkolems)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ TCtxStack ctx(&d_rtfc);
+ std::vector<bool> processedChildren;
+ ctx.pushInitial(assertion);
+ processedChildren.push_back(false);
+ std::pair<Node, uint32_t> initial = ctx.getCurrent();
+ std::pair<Node, uint32_t> curr;
+ Node node;
+ uint32_t nodeVal;
+ TermFormulaCache::const_iterator itc;
+ while (!ctx.empty())
+ {
+ curr = ctx.getCurrent();
+ itc = d_tfCache.find(curr);
+ node = curr.first;
+ nodeVal = curr.second;
+ Trace("rtf-debug") << "Visit " << node << ", " << nodeVal << std::endl;
+ if (itc != d_tfCache.end())
+ {
+ Trace("rtf-debug") << "...already computed" << std::endl;
+ ctx.pop();
+ processedChildren.pop_back();
+ // already computed
+ continue;
+ }
+ // if we have yet to process children
+ if (!processedChildren.back())
+ {
+ // check if we should replace the current node
+ Node currt = runCurrent(curr, output, newSkolems);
+ // if null, we need to recurse
+ if (!currt.isNull())
+ {
+ Trace("rtf-debug") << "...replace by skolem" << std::endl;
+ d_tfCache.insert(curr, currt);
+ ctx.pop();
+ processedChildren.pop_back();
+ }
+ else
+ {
+ size_t nchild = node.getNumChildren();
+ if (nchild > 0)
+ {
+ Trace("rtf-debug") << "...recurse to children" << std::endl;
+ // recurse if we have children
+ processedChildren[processedChildren.size() - 1] = true;
+ for (size_t i = 0; i < nchild; i++)
+ {
+ ctx.pushChild(node, nodeVal, i);
+ processedChildren.push_back(false);
+ }
+ }
+ else
+ {
+ Trace("rtf-debug") << "...base case" << std::endl;
+ d_tfCache.insert(curr, node);
+ ctx.pop();
+ processedChildren.pop_back();
+ }
+ }
+ continue;
+ }
+ Trace("rtf-debug") << "...reconstruct" << std::endl;
+ // otherwise, we are now finished processing children, pop the current node
+ // and compute the result
+ ctx.pop();
+ processedChildren.pop_back();
+ // if we have not already computed the result
+ std::vector<Node> newChildren;
+ bool childChanged = false;
+ if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ newChildren.push_back(node.getOperator());
+ }
+ // reconstruct from the children
+ std::pair<Node, uint32_t> currChild;
+ for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; i++)
+ {
+ // recompute the value of the child
+ uint32_t val = d_rtfc.computeValue(node, nodeVal, i);
+ currChild = std::pair<Node, uint32_t>(node[i], val);
+ itc = d_tfCache.find(currChild);
+ Assert(itc != d_tfCache.end());
+ Node newChild = (*itc).second;
+ Assert(!newChild.isNull());
+ childChanged |= (newChild != node[i]);
+ newChildren.push_back(newChild);
+ }
+ // If changes, we reconstruct the node
+ Node ret = node;
+ if (childChanged)
+ {
+ ret = nm->mkNode(node.getKind(), newChildren);
+ }
+ // cache
+ d_tfCache.insert(curr, ret);
+ }
+ itc = d_tfCache.find(initial);
+ Assert(itc != d_tfCache.end());
+ return (*itc).second;
+}
+
+Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
+ std::vector<theory::TrustNode>& output,
+ std::vector<Node>& newSkolems)
{
- Assert(!ctx.empty());
- std::pair<Node, uint32_t> curr = ctx.getCurrent();
- ctx.pop();
TNode node = curr.first;
if (node.getKind() == kind::INST_PATTERN_LIST)
{
Debug("ite") << "removeITEs(" << node << ")"
<< " " << inQuant << " " << inTerm << std::endl;
- // The result may be cached already
NodeManager *nodeManager = NodeManager::currentNM();
- TermFormulaCache::const_iterator itc = d_tfCache.find(curr);
- if (itc != d_tfCache.end())
- {
- Node cached = (*itc).second;
- Debug("ite") << "removeITEs: in-cache: " << cached << endl;
- return cached.isNull() ? Node(curr.first) : cached;
- }
TypeNode nodeType = node.getType();
Node skolem;
// if the term should be replaced by a skolem
if( !skolem.isNull() ){
- // Attach the 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())
// Remove ITEs from the new assertion, rewrite it and push it to the
// output
Node newAssertionPre = newAssertion;
- TCtxStack cctx(&d_rtfc);
- cctx.pushInitial(newAssertion);
- newAssertion = run(cctx, output, newSkolems);
+ newAssertion = runInternal(newAssertion, output, newSkolems);
if (isProofEnabled())
{
return skolem;
}
- // If not an ITE, go deep
- 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 (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(curr, cached);
- return cached;
- }
- d_tfCache.insert(curr, Node::null());
- return node;
+ // return null, indicating we will traverse children within runInternal
+ return Node::null();
}
Node RemoveTermFormulas::getSkolemForNode(Node node) const
TermFormulaCache::const_iterator itc = d_tfCache.find(curr);
if (itc != d_tfCache.end())
{
- Node cached = (*itc).second;
- return cached.isNull() ? Node(node) : cached;
+ return (*itc).second;
}
vector<Node> newChildren;
RtfTermContext d_rtfc;
/**
- * Removes terms of the form (1), (2), (3) described above from node.
- * All additional assertions are pushed into
- * assertions. iteSkolemMap contains a map from introduced skolem
- * variables to the index in assertions containing the new Boolean
- * ite created in conjunction with that skolem variable.
+ * Removes terms of the forms described above from formula assertion.
+ * All additional assertions and skolems are pushed into newAsserts and
+ * newSkolems, which are always of the same length.
*
- * inQuant is whether we are processing node in the body of quantified formula
- * 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.
+ * This uses a term-context-sensitive stack to process assertion. It returns
+ * the version of assertion with all term formulas removed.
*/
- Node run(TCtxStack& cxt,
- std::vector<theory::TrustNode>& newAsserts,
- std::vector<Node>& newSkolems);
+ Node runInternal(Node assertion,
+ std::vector<theory::TrustNode>& newAsserts,
+ std::vector<Node>& newSkolems);
+ /**
+ * This is called on curr of the form (t, val) where t is a term and val is
+ * a term context identifier computed by RtfTermContext. If curr should be
+ * replaced by a skolem, this method returns this skolem k, adds k to
+ * newSkolems and adds the axiom defining that skolem to newAsserts, where
+ * runInternal is called on that axiom. Otherwise, this method returns the
+ * null node.
+ */
+ Node runCurrent(std::pair<Node, uint32_t>& curr,
+ std::vector<theory::TrustNode>& newAsserts,
+ std::vector<Node>& newSkolems);
/** Replace internal */
Node replaceInternal(TCtxStack& ctx) const;
--- /dev/null
+/********************* */
+/*! \file issue4889.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Test for issue #4889
+ **/
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+
+int main()
+{
+#ifdef CVC4_USE_SYMFPU
+ Solver slv;
+ Sort sort_int = slv.getIntegerSort();
+ Sort sort_array = slv.mkArraySort(sort_int, sort_int);
+ Sort sort_fp128 = slv.mkFloatingPointSort(15, 113);
+ Sort sort_fp32 = slv.mkFloatingPointSort(8, 24);
+ Sort sort_bool = slv.getBooleanSort();
+ Term const0 = slv.mkConst(sort_fp32, "_c0");
+ Term const1 = slv.mkConst(sort_fp32, "_c2");
+ Term const2 = slv.mkConst(sort_bool, "_c4");
+ Term ite = slv.mkTerm(ITE, const2, const1, const0);
+ Term rem = slv.mkTerm(FLOATINGPOINT_REM, ite, const1);
+ Term isnan = slv.mkTerm(FLOATINGPOINT_ISNAN, rem);
+ slv.checkSatAssuming(isnan);
+#endif
+ return 0;
+}
projects / cvc5.git / commitdiff