This is work towards eliminating global calls to getCurrentSmtEngine()->expandDefinition.
The next step will be to add Rewriter::expandDefinition.
// do not do any theory stuff if expandOnly is true
theory::Theory* t = d_smt.getTheoryEngine()->theoryOf(node);
+ theory::TheoryRewriter* tr = t->getTheoryRewriter();
Assert(t != NULL);
- TrustNode trn = t->expandDefinition(n);
+ TrustNode trn = tr->expandDefinition(n);
if (!trn.isNull())
{
node = trn.getNode();
ArithPreprocess::ArithPreprocess(ArithState& state,
InferenceManager& im,
ProofNodeManager* pnm,
- const LogicInfo& info)
- : d_im(im), d_opElim(pnm, info), d_reduced(state.getUserContext())
+ OperatorElim& oe)
+ : d_im(im), d_opElim(oe), d_reduced(state.getUserContext())
{
}
TrustNode ArithPreprocess::eliminate(TNode n,
class ArithState;
class InferenceManager;
+class OperatorElim;
/**
* This module can be used for (on demand) elimination of extended arithmetic
ArithPreprocess(ArithState& state,
InferenceManager& im,
ProofNodeManager* pnm,
- const LogicInfo& info);
+ OperatorElim& oe);
~ArithPreprocess() {}
/**
* Call eliminate operators on formula n, return the resulting trust node,
/** Reference to the inference manager */
InferenceManager& d_im;
/** The operator elimination utility */
- OperatorElim d_opElim;
+ OperatorElim& d_opElim;
/** The set of assertions that were reduced */
context::CDHashMap<Node, bool, NodeHashFunction> d_reduced;
};
#include "theory/arith/arith_rewriter.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/normal_form.h"
+#include "theory/arith/operator_elim.h"
#include "theory/theory.h"
#include "util/iand.h"
namespace theory {
namespace arith {
+ArithRewriter::ArithRewriter(OperatorElim& oe) : d_opElim(oe) {}
+
bool ArithRewriter::isAtom(TNode n) {
Kind k = n.getKind();
return arith::isRelationOperator(k) || k == kind::IS_INTEGER
return RewriteResponse(REWRITE_DONE, t);
}
+TrustNode ArithRewriter::expandDefinition(Node node)
+{
+ // call eliminate operators, to eliminate partial operators only
+ std::vector<SkolemLemma> lems;
+ TrustNode ret = d_opElim.eliminate(node, lems, true);
+ Assert(lems.empty());
+ return ret;
+}
+
RewriteResponse ArithRewriter::returnRewrite(TNode t, Node ret, Rewrite r)
{
Trace("arith-rewrite") << "ArithRewriter : " << t << " == " << ret << " by "
namespace theory {
namespace arith {
+class OperatorElim;
+
class ArithRewriter : public TheoryRewriter
{
public:
+ ArithRewriter(OperatorElim& oe);
RewriteResponse preRewrite(TNode n) override;
RewriteResponse postRewrite(TNode n) override;
+ /**
+ * Expand definition, which eliminates extended operators like div/mod in
+ * the given node.
+ */
+ TrustNode expandDefinition(Node node) override;
private:
static Node makeSubtractionNode(TNode l, TNode r);
}
/** return rewrite */
static RewriteResponse returnRewrite(TNode t, Node ret, Rewrite r);
+ /** The operator elimination utility */
+ OperatorElim& d_opElim;
}; /* class ArithRewriter */
} // namespace arith
d_astate(*d_internal, c, u, valuation),
d_im(*this, d_astate, pnm),
d_nonlinearExtension(nullptr),
- d_arithPreproc(d_astate, d_im, pnm, logicInfo)
+ d_opElim(pnm, logicInfo),
+ d_arithPreproc(d_astate, d_im, pnm, d_opElim),
+ d_rewriter(d_opElim)
{
// indicate we are using the theory state object and inference manager
d_theoryState = &d_astate;
d_internal->preRegisterTerm(n);
}
-TrustNode TheoryArith::expandDefinition(Node node)
-{
- // call eliminate operators, to eliminate partial operators only
- std::vector<SkolemLemma> lems;
- TrustNode ret = d_arithPreproc.eliminate(node, lems, true);
- Assert(lems.empty());
- return ret;
-}
-
void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
TrustNode TheoryArith::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
/** finish initialization */
void finishInit() override;
//--------------------------------- end initialization
- /**
- * Expand definition, which eliminates extended operators like div/mod in
- * the given node.
- */
- TrustNode expandDefinition(Node node) override;
/**
* Does non-context dependent setup for a node connected to a theory.
*/
* arithmetic.
*/
std::unique_ptr<nl::NonlinearExtension> d_nonlinearExtension;
+ /** The operator elimination utility */
+ OperatorElim d_opElim;
/** The preprocess utility */
ArithPreprocess d_arithPreproc;
/** The theory rewriter for this theory. */
TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems)
{
// first, see if we need to expand definitions
- TrustNode texp = expandDefinition(term);
+ TrustNode texp = d_rewriter.expandDefinition(term);
if (!texp.isNull())
{
return texp;
return std::string("th_arrays_dec");
}
-TrustNode TheoryArrays::expandDefinition(Node node)
-{
- NodeManager* nm = NodeManager::currentNM();
- Kind kind = node.getKind();
-
- /* Expand
- *
- * (eqrange a b i j)
- *
- * to
- *
- * forall k . i <= k <= j => a[k] = b[k]
- *
- */
- if (kind == kind::EQ_RANGE)
- {
- TNode a = node[0];
- TNode b = node[1];
- TNode i = node[2];
- TNode j = node[3];
- Node k = nm->mkBoundVar(i.getType());
- Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, k);
- TypeNode type = k.getType();
-
- Kind kle;
- Node range;
- if (type.isBitVector())
- {
- kle = kind::BITVECTOR_ULE;
- }
- else if (type.isFloatingPoint())
- {
- kle = kind::FLOATINGPOINT_LEQ;
- }
- else if (type.isInteger() || type.isReal())
- {
- kle = kind::LEQ;
- }
- else
- {
- Unimplemented() << "Type " << type << " is not supported for predicate "
- << kind;
- }
-
- range = nm->mkNode(kind::AND, nm->mkNode(kle, i, k), nm->mkNode(kle, k, j));
-
- Node eq = nm->mkNode(kind::EQUAL,
- nm->mkNode(kind::SELECT, a, k),
- nm->mkNode(kind::SELECT, b, k));
- Node implies = nm->mkNode(kind::IMPLIES, range, eq);
- Node ret = nm->mkNode(kind::FORALL, bvl, implies);
- return TrustNode::mkTrustRewrite(node, ret, nullptr);
- }
- return TrustNode::null();
-}
-
void TheoryArrays::computeRelevantTerms(std::set<Node>& termSet)
{
NodeManager* nm = NodeManager::currentNM();
std::string identify() const override { return std::string("TheoryArrays"); }
- TrustNode expandDefinition(Node node) override;
-
/////////////////////////////////////////////////////////////////////////////
// PREPROCESSING
/////////////////////////////////////////////////////////////////////////////
return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count);
}
+Node TheoryArraysRewriter::normalizeConstant(TNode node)
+{
+ return normalizeConstant(node, node[1].getType().getCardinality());
+}
+
+// this function is called by printers when using the option "--model-u-dt-enum"
+Node TheoryArraysRewriter::normalizeConstant(TNode node, Cardinality indexCard)
+{
+ TNode store = node[0];
+ TNode index = node[1];
+ TNode value = node[2];
+
+ std::vector<TNode> indices;
+ std::vector<TNode> elements;
+
+ // Normal form for nested stores is just ordering by index - but also need
+ // to check if we are writing to default value
+
+ // Go through nested stores looking for where to insert index
+ // Also check whether we are replacing an existing store
+ TNode replacedValue;
+ uint32_t depth = 1;
+ uint32_t valCount = 1;
+ while (store.getKind() == kind::STORE)
+ {
+ if (index == store[1])
+ {
+ replacedValue = store[2];
+ store = store[0];
+ break;
+ }
+ else if (index >= store[1])
+ {
+ break;
+ }
+ if (value == store[2])
+ {
+ valCount += 1;
+ }
+ depth += 1;
+ indices.push_back(store[1]);
+ elements.push_back(store[2]);
+ store = store[0];
+ }
+ Node n = store;
+
+ // Get the default value at the bottom of the nested stores
+ while (store.getKind() == kind::STORE)
+ {
+ if (value == store[2])
+ {
+ valCount += 1;
+ }
+ depth += 1;
+ store = store[0];
+ }
+ Assert(store.getKind() == kind::STORE_ALL);
+ ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
+ Node defaultValue = storeAll.getValue();
+ NodeManager* nm = NodeManager::currentNM();
+
+ // Check if we are writing to default value - if so the store
+ // to index can be ignored
+ if (value == defaultValue)
+ {
+ if (replacedValue.isNull())
+ {
+ // Quick exit - if writing to default value and nothing was
+ // replaced, we can just return node[0]
+ return node[0];
+ }
+ // else rebuild the store without the replaced write and then exit
+ }
+ else
+ {
+ n = nm->mkNode(kind::STORE, n, index, value);
+ }
+
+ // Build the rest of the store after inserting/deleting
+ while (!indices.empty())
+ {
+ n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
+ indices.pop_back();
+ elements.pop_back();
+ }
+
+ // Ready to exit if write was to the default value (see previous comment)
+ if (value == defaultValue)
+ {
+ return n;
+ }
+
+ if (indexCard.isInfinite())
+ {
+ return n;
+ }
+
+ // When index sort is finite, we have to check whether there is any value
+ // that is written to more than the default value. If so, it must become
+ // the new default value
+
+ TNode mostFrequentValue;
+ uint32_t mostFrequentValueCount = 0;
+ store = node[0];
+ if (store.getKind() == kind::STORE)
+ {
+ mostFrequentValue = getMostFrequentValue(store);
+ mostFrequentValueCount = getMostFrequentValueCount(store);
+ }
+
+ // Compute the most frequently written value for n
+ if (valCount > mostFrequentValueCount
+ || (valCount == mostFrequentValueCount && value < mostFrequentValue))
+ {
+ mostFrequentValue = value;
+ mostFrequentValueCount = valCount;
+ }
+
+ // Need to make sure the default value count is larger, or the same and the
+ // default value is expression-order-less-than nextValue
+ Cardinality::CardinalityComparison compare =
+ indexCard.compare(mostFrequentValueCount + depth);
+ Assert(compare != Cardinality::UNKNOWN);
+ if (compare == Cardinality::GREATER
+ || (compare == Cardinality::EQUAL && (defaultValue < mostFrequentValue)))
+ {
+ return n;
+ }
+
+ // Bad case: have to recompute value counts and/or possibly switch out
+ // default value
+ store = n;
+ std::unordered_set<TNode, TNodeHashFunction> indexSet;
+ std::unordered_map<TNode, uint32_t, TNodeHashFunction> elementsMap;
+ std::unordered_map<TNode, uint32_t, TNodeHashFunction>::iterator it;
+ uint32_t count;
+ uint32_t max = 0;
+ TNode maxValue;
+ while (store.getKind() == kind::STORE)
+ {
+ indices.push_back(store[1]);
+ indexSet.insert(store[1]);
+ elements.push_back(store[2]);
+ it = elementsMap.find(store[2]);
+ if (it != elementsMap.end())
+ {
+ (*it).second = (*it).second + 1;
+ count = (*it).second;
+ }
+ else
+ {
+ elementsMap[store[2]] = 1;
+ count = 1;
+ }
+ if (count > max || (count == max && store[2] < maxValue))
+ {
+ max = count;
+ maxValue = store[2];
+ }
+ store = store[0];
+ }
+
+ Assert(depth == indices.size());
+ compare = indexCard.compare(max + depth);
+ Assert(compare != Cardinality::UNKNOWN);
+ if (compare == Cardinality::GREATER
+ || (compare == Cardinality::EQUAL && (defaultValue < maxValue)))
+ {
+ Assert(!replacedValue.isNull() && mostFrequentValue == replacedValue);
+ return n;
+ }
+
+ // Out of luck: have to swap out default value
+
+ // Enumerate values from index type into newIndices and sort
+ std::vector<Node> newIndices;
+ TypeEnumerator te(index.getType());
+ bool needToSort = false;
+ uint32_t numTe = 0;
+ while (!te.isFinished()
+ && (!indexCard.isFinite()
+ || numTe < indexCard.getFiniteCardinality().toUnsignedInt()))
+ {
+ if (indexSet.find(*te) == indexSet.end())
+ {
+ if (!newIndices.empty() && (!(newIndices.back() < (*te))))
+ {
+ needToSort = true;
+ }
+ newIndices.push_back(*te);
+ }
+ ++numTe;
+ ++te;
+ }
+ Assert(indexCard.compare(newIndices.size() + depth) == Cardinality::EQUAL);
+ if (needToSort)
+ {
+ std::sort(newIndices.begin(), newIndices.end());
+ }
+
+ n = nm->mkConst(ArrayStoreAll(node.getType(), maxValue));
+ std::vector<Node>::iterator itNew = newIndices.begin(),
+ it_end = newIndices.end();
+ while (itNew != it_end || !indices.empty())
+ {
+ if (itNew != it_end && (indices.empty() || (*itNew) < indices.back()))
+ {
+ n = nm->mkNode(kind::STORE, n, (*itNew), defaultValue);
+ ++itNew;
+ }
+ else if (itNew == it_end || indices.back() < (*itNew))
+ {
+ if (elements.back() != maxValue)
+ {
+ n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
+ }
+ indices.pop_back();
+ elements.pop_back();
+ }
+ }
+ return n;
+}
+
+RewriteResponse TheoryArraysRewriter::postRewrite(TNode node)
+{
+ Trace("arrays-postrewrite")
+ << "Arrays::postRewrite start " << node << std::endl;
+ switch (node.getKind())
+ {
+ case kind::SELECT:
+ {
+ TNode store = node[0];
+ TNode index = node[1];
+ Node n;
+ bool val;
+ while (store.getKind() == kind::STORE)
+ {
+ if (index == store[1])
+ {
+ val = true;
+ }
+ else if (index.isConst() && store[1].isConst())
+ {
+ val = false;
+ }
+ else
+ {
+ n = Rewriter::rewrite(mkEqNode(store[1], index));
+ if (n.getKind() != kind::CONST_BOOLEAN)
+ {
+ break;
+ }
+ val = n.getConst<bool>();
+ }
+ if (val)
+ {
+ // select(store(a,i,v),j) = v if i = j
+ Trace("arrays-postrewrite")
+ << "Arrays::postRewrite returning " << store[2] << std::endl;
+ return RewriteResponse(REWRITE_DONE, store[2]);
+ }
+ // select(store(a,i,v),j) = select(a,j) if i /= j
+ store = store[0];
+ }
+ if (store.getKind() == kind::STORE_ALL)
+ {
+ // select(store_all(v),i) = v
+ ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
+ n = storeAll.getValue();
+ Trace("arrays-postrewrite")
+ << "Arrays::postRewrite returning " << n << std::endl;
+ Assert(n.isConst());
+ return RewriteResponse(REWRITE_DONE, n);
+ }
+ else if (store != node[0])
+ {
+ n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
+ Trace("arrays-postrewrite")
+ << "Arrays::postRewrite returning " << n << std::endl;
+ return RewriteResponse(REWRITE_DONE, n);
+ }
+ break;
+ }
+ case kind::STORE:
+ {
+ TNode store = node[0];
+ TNode value = node[2];
+ // store(a,i,select(a,i)) = a
+ if (value.getKind() == kind::SELECT && value[0] == store
+ && value[1] == node[1])
+ {
+ Trace("arrays-postrewrite")
+ << "Arrays::postRewrite returning " << store << std::endl;
+ return RewriteResponse(REWRITE_DONE, store);
+ }
+ TNode index = node[1];
+ if (store.isConst() && index.isConst() && value.isConst())
+ {
+ // normalize constant
+ Node n = normalizeConstant(node);
+ Assert(n.isConst());
+ Trace("arrays-postrewrite")
+ << "Arrays::postRewrite returning " << n << std::endl;
+ return RewriteResponse(REWRITE_DONE, n);
+ }
+ if (store.getKind() == kind::STORE)
+ {
+ // store(store(a,i,v),j,w)
+ bool val;
+ if (index == store[1])
+ {
+ val = true;
+ }
+ else if (index.isConst() && store[1].isConst())
+ {
+ val = false;
+ }
+ else
+ {
+ Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
+ if (eqRewritten.getKind() != kind::CONST_BOOLEAN)
+ {
+ Trace("arrays-postrewrite")
+ << "Arrays::postRewrite returning " << node << std::endl;
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+ val = eqRewritten.getConst<bool>();
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ if (val)
+ {
+ // store(store(a,i,v),i,w) = store(a,i,w)
+ Node result = nm->mkNode(kind::STORE, store[0], index, value);
+ Trace("arrays-postrewrite")
+ << "Arrays::postRewrite returning " << result << std::endl;
+ return RewriteResponse(REWRITE_AGAIN, result);
+ }
+ else if (index < store[1])
+ {
+ // store(store(a,i,v),j,w) = store(store(a,j,w),i,v)
+ // IF i != j and j comes before i in the ordering
+ std::vector<TNode> indices;
+ std::vector<TNode> elements;
+ indices.push_back(store[1]);
+ elements.push_back(store[2]);
+ store = store[0];
+ Node n;
+ while (store.getKind() == kind::STORE)
+ {
+ if (index == store[1])
+ {
+ val = true;
+ }
+ else if (index.isConst() && store[1].isConst())
+ {
+ val = false;
+ }
+ else
+ {
+ n = Rewriter::rewrite(mkEqNode(store[1], index));
+ if (n.getKind() != kind::CONST_BOOLEAN)
+ {
+ break;
+ }
+ val = n.getConst<bool>();
+ }
+ if (val)
+ {
+ store = store[0];
+ break;
+ }
+ else if (!(index < store[1]))
+ {
+ break;
+ }
+ indices.push_back(store[1]);
+ elements.push_back(store[2]);
+ store = store[0];
+ }
+ if (value.getKind() == kind::SELECT && value[0] == store
+ && value[1] == index)
+ {
+ n = store;
+ }
+ else
+ {
+ n = nm->mkNode(kind::STORE, store, index, value);
+ }
+ while (!indices.empty())
+ {
+ n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
+ indices.pop_back();
+ elements.pop_back();
+ }
+ Assert(n != node);
+ Trace("arrays-postrewrite")
+ << "Arrays::postRewrite returning " << n << std::endl;
+ return RewriteResponse(REWRITE_AGAIN, n);
+ }
+ }
+ break;
+ }
+ case kind::EQUAL:
+ {
+ if (node[0] == node[1])
+ {
+ Trace("arrays-postrewrite")
+ << "Arrays::postRewrite returning true" << std::endl;
+ return RewriteResponse(REWRITE_DONE,
+ NodeManager::currentNM()->mkConst(true));
+ }
+ else if (node[0].isConst() && node[1].isConst())
+ {
+ Trace("arrays-postrewrite")
+ << "Arrays::postRewrite returning false" << std::endl;
+ return RewriteResponse(REWRITE_DONE,
+ NodeManager::currentNM()->mkConst(false));
+ }
+ if (node[0] > node[1])
+ {
+ Node newNode =
+ NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
+ Trace("arrays-postrewrite")
+ << "Arrays::postRewrite returning " << newNode << std::endl;
+ return RewriteResponse(REWRITE_DONE, newNode);
+ }
+ break;
+ }
+ default: break;
+ }
+ Trace("arrays-postrewrite")
+ << "Arrays::postRewrite returning " << node << std::endl;
+ return RewriteResponse(REWRITE_DONE, node);
+}
+
+RewriteResponse TheoryArraysRewriter::preRewrite(TNode node)
+{
+ Trace("arrays-prerewrite")
+ << "Arrays::preRewrite start " << node << std::endl;
+ switch (node.getKind())
+ {
+ case kind::SELECT:
+ {
+ TNode store = node[0];
+ TNode index = node[1];
+ Node n;
+ bool val;
+ while (store.getKind() == kind::STORE)
+ {
+ if (index == store[1])
+ {
+ val = true;
+ }
+ else if (index.isConst() && store[1].isConst())
+ {
+ val = false;
+ }
+ else
+ {
+ n = Rewriter::rewrite(mkEqNode(store[1], index));
+ if (n.getKind() != kind::CONST_BOOLEAN)
+ {
+ break;
+ }
+ val = n.getConst<bool>();
+ }
+ if (val)
+ {
+ // select(store(a,i,v),j) = v if i = j
+ Trace("arrays-prerewrite")
+ << "Arrays::preRewrite returning " << store[2] << std::endl;
+ return RewriteResponse(REWRITE_AGAIN, store[2]);
+ }
+ // select(store(a,i,v),j) = select(a,j) if i /= j
+ store = store[0];
+ }
+ if (store.getKind() == kind::STORE_ALL)
+ {
+ // select(store_all(v),i) = v
+ ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
+ n = storeAll.getValue();
+ Trace("arrays-prerewrite")
+ << "Arrays::preRewrite returning " << n << std::endl;
+ Assert(n.isConst());
+ return RewriteResponse(REWRITE_DONE, n);
+ }
+ else if (store != node[0])
+ {
+ n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
+ Trace("arrays-prerewrite")
+ << "Arrays::preRewrite returning " << n << std::endl;
+ return RewriteResponse(REWRITE_DONE, n);
+ }
+ break;
+ }
+ case kind::STORE:
+ {
+ TNode store = node[0];
+ TNode value = node[2];
+ // store(a,i,select(a,i)) = a
+ if (value.getKind() == kind::SELECT && value[0] == store
+ && value[1] == node[1])
+ {
+ Trace("arrays-prerewrite")
+ << "Arrays::preRewrite returning " << store << std::endl;
+ return RewriteResponse(REWRITE_AGAIN, store);
+ }
+ if (store.getKind() == kind::STORE)
+ {
+ // store(store(a,i,v),j,w)
+ TNode index = node[1];
+ bool val;
+ if (index == store[1])
+ {
+ val = true;
+ }
+ else if (index.isConst() && store[1].isConst())
+ {
+ val = false;
+ }
+ else
+ {
+ Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
+ if (eqRewritten.getKind() != kind::CONST_BOOLEAN)
+ {
+ break;
+ }
+ val = eqRewritten.getConst<bool>();
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ if (val)
+ {
+ // store(store(a,i,v),i,w) = store(a,i,w)
+ Node newNode = nm->mkNode(kind::STORE, store[0], index, value);
+ Trace("arrays-prerewrite")
+ << "Arrays::preRewrite returning " << newNode << std::endl;
+ return RewriteResponse(REWRITE_DONE, newNode);
+ }
+ }
+ break;
+ }
+ case kind::EQUAL:
+ {
+ if (node[0] == node[1])
+ {
+ Trace("arrays-prerewrite")
+ << "Arrays::preRewrite returning true" << std::endl;
+ return RewriteResponse(REWRITE_DONE,
+ NodeManager::currentNM()->mkConst(true));
+ }
+ break;
+ }
+ default: break;
+ }
+
+ Trace("arrays-prerewrite")
+ << "Arrays::preRewrite returning " << node << std::endl;
+ return RewriteResponse(REWRITE_DONE, node);
+}
+
+TrustNode TheoryArraysRewriter::expandDefinition(Node node)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Kind kind = node.getKind();
+
+ /* Expand
+ *
+ * (eqrange a b i j)
+ *
+ * to
+ *
+ * forall k . i <= k <= j => a[k] = b[k]
+ *
+ */
+ if (kind == kind::EQ_RANGE)
+ {
+ TNode a = node[0];
+ TNode b = node[1];
+ TNode i = node[2];
+ TNode j = node[3];
+ Node k = nm->mkBoundVar(i.getType());
+ Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, k);
+ TypeNode type = k.getType();
+
+ Kind kle;
+ Node range;
+ if (type.isBitVector())
+ {
+ kle = kind::BITVECTOR_ULE;
+ }
+ else if (type.isFloatingPoint())
+ {
+ kle = kind::FLOATINGPOINT_LEQ;
+ }
+ else if (type.isInteger() || type.isReal())
+ {
+ kle = kind::LEQ;
+ }
+ else
+ {
+ Unimplemented() << "Type " << type << " is not supported for predicate "
+ << kind;
+ }
+
+ range = nm->mkNode(kind::AND, nm->mkNode(kle, i, k), nm->mkNode(kle, k, j));
+
+ Node eq = nm->mkNode(kind::EQUAL,
+ nm->mkNode(kind::SELECT, a, k),
+ nm->mkNode(kind::SELECT, b, k));
+ Node implies = nm->mkNode(kind::IMPLIES, range, eq);
+ Node ret = nm->mkNode(kind::FORALL, bvl, implies);
+ return TrustNode::mkTrustRewrite(node, ret, nullptr);
+ }
+ return TrustNode::null();
+}
+
} // namespace arrays
} // namespace theory
} // namespace cvc5
class TheoryArraysRewriter : public TheoryRewriter
{
- static Node normalizeConstant(TNode node) {
- return normalizeConstant(node, node[1].getType().getCardinality());
- }
+ /**
+ * Puts array constant node into normal form. This is so that array constants
+ * that are distinct nodes are semantically disequal.
+ */
+ static Node normalizeConstant(TNode node);
public:
- //this function is called by printers when using the option "--model-u-dt-enum"
- static Node normalizeConstant(TNode node, Cardinality indexCard) {
- TNode store = node[0];
- TNode index = node[1];
- TNode value = node[2];
+ /** Normalize a constant whose index type has cardinality indexCard */
+ static Node normalizeConstant(TNode node, Cardinality indexCard);
- std::vector<TNode> indices;
- std::vector<TNode> elements;
+ RewriteResponse postRewrite(TNode node) override;
- // Normal form for nested stores is just ordering by index - but also need
- // to check if we are writing to default value
+ RewriteResponse preRewrite(TNode node) override;
- // Go through nested stores looking for where to insert index
- // Also check whether we are replacing an existing store
- TNode replacedValue;
- unsigned depth = 1;
- unsigned valCount = 1;
- while (store.getKind() == kind::STORE) {
- if (index == store[1]) {
- replacedValue = store[2];
- store = store[0];
- break;
- }
- else if (!(index < store[1])) {
- break;
- }
- if (value == store[2]) {
- valCount += 1;
- }
- depth += 1;
- indices.push_back(store[1]);
- elements.push_back(store[2]);
- store = store[0];
- }
- Node n = store;
-
- // Get the default value at the bottom of the nested stores
- while (store.getKind() == kind::STORE) {
- if (value == store[2]) {
- valCount += 1;
- }
- depth += 1;
- store = store[0];
- }
- Assert(store.getKind() == kind::STORE_ALL);
- ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
- Node defaultValue = storeAll.getValue();
- NodeManager* nm = NodeManager::currentNM();
-
- // Check if we are writing to default value - if so the store
- // to index can be ignored
- if (value == defaultValue) {
- if (replacedValue.isNull()) {
- // Quick exit - if writing to default value and nothing was
- // replaced, we can just return node[0]
- return node[0];
- }
- // else rebuild the store without the replaced write and then exit
- }
- else {
- n = nm->mkNode(kind::STORE, n, index, value);
- }
-
- // Build the rest of the store after inserting/deleting
- while (!indices.empty()) {
- n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
- indices.pop_back();
- elements.pop_back();
- }
-
- // Ready to exit if write was to the default value (see previous comment)
- if (value == defaultValue) {
- return n;
- }
-
- if (indexCard.isInfinite()) {
- return n;
- }
-
- // When index sort is finite, we have to check whether there is any value
- // that is written to more than the default value. If so, it must become
- // the new default value
-
- TNode mostFrequentValue;
- unsigned mostFrequentValueCount = 0;
- store = node[0];
- if (store.getKind() == kind::STORE) {
- mostFrequentValue = getMostFrequentValue(store);
- mostFrequentValueCount = getMostFrequentValueCount(store);
- }
-
- // Compute the most frequently written value for n
- if (valCount > mostFrequentValueCount ||
- (valCount == mostFrequentValueCount && value < mostFrequentValue)) {
- mostFrequentValue = value;
- mostFrequentValueCount = valCount;
- }
-
- // Need to make sure the default value count is larger, or the same and the default value is expression-order-less-than nextValue
- Cardinality::CardinalityComparison compare = indexCard.compare(mostFrequentValueCount + depth);
- Assert(compare != Cardinality::UNKNOWN);
- if (compare == Cardinality::GREATER ||
- (compare == Cardinality::EQUAL && (defaultValue < mostFrequentValue))) {
- return n;
- }
-
- // Bad case: have to recompute value counts and/or possibly switch out
- // default value
- store = n;
- std::unordered_set<TNode, TNodeHashFunction> indexSet;
- std::unordered_map<TNode, unsigned, TNodeHashFunction> elementsMap;
- std::unordered_map<TNode, unsigned, TNodeHashFunction>::iterator it;
- unsigned count;
- unsigned max = 0;
- TNode maxValue;
- while (store.getKind() == kind::STORE) {
- indices.push_back(store[1]);
- indexSet.insert(store[1]);
- elements.push_back(store[2]);
- it = elementsMap.find(store[2]);
- if (it != elementsMap.end()) {
- (*it).second = (*it).second + 1;
- count = (*it).second;
- }
- else {
- elementsMap[store[2]] = 1;
- count = 1;
- }
- if (count > max ||
- (count == max && store[2] < maxValue)) {
- max = count;
- maxValue = store[2];
- }
- store = store[0];
- }
-
- Assert(depth == indices.size());
- compare = indexCard.compare(max + depth);
- Assert(compare != Cardinality::UNKNOWN);
- if (compare == Cardinality::GREATER ||
- (compare == Cardinality::EQUAL && (defaultValue < maxValue))) {
- Assert(!replacedValue.isNull() && mostFrequentValue == replacedValue);
- return n;
- }
-
- // Out of luck: have to swap out default value
-
- // Enumerate values from index type into newIndices and sort
- std::vector<Node> newIndices;
- TypeEnumerator te(index.getType());
- bool needToSort = false;
- unsigned numTe = 0;
- while (!te.isFinished() && (!indexCard.isFinite() || numTe<indexCard.getFiniteCardinality().toUnsignedInt())) {
- if (indexSet.find(*te) == indexSet.end()) {
- if (!newIndices.empty() && (!(newIndices.back() < (*te)))) {
- needToSort = true;
- }
- newIndices.push_back(*te);
- }
- ++numTe;
- ++te;
- }
- Assert(indexCard.compare(newIndices.size() + depth) == Cardinality::EQUAL);
- if (needToSort) {
- std::sort(newIndices.begin(), newIndices.end());
- }
-
- n = nm->mkConst(ArrayStoreAll(node.getType(), maxValue));
- std::vector<Node>::iterator itNew = newIndices.begin(), it_end = newIndices.end();
- while (itNew != it_end || !indices.empty()) {
- if (itNew != it_end && (indices.empty() || (*itNew) < indices.back())) {
- n = nm->mkNode(kind::STORE, n, (*itNew), defaultValue);
- ++itNew;
- }
- else if (itNew == it_end || indices.back() < (*itNew)) {
- if (elements.back() != maxValue) {
- n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
- }
- indices.pop_back();
- elements.pop_back();
- }
- }
- return n;
- }
-
- public:
- RewriteResponse postRewrite(TNode node) override
- {
- Trace("arrays-postrewrite") << "Arrays::postRewrite start " << node << std::endl;
- switch (node.getKind()) {
- case kind::SELECT: {
- TNode store = node[0];
- TNode index = node[1];
- Node n;
- bool val;
- while (store.getKind() == kind::STORE) {
- if (index == store[1]) {
- val = true;
- }
- else if (index.isConst() && store[1].isConst()) {
- val = false;
- }
- else {
- n = Rewriter::rewrite(mkEqNode(store[1], index));
- if (n.getKind() != kind::CONST_BOOLEAN) {
- break;
- }
- val = n.getConst<bool>();
- }
- if (val) {
- // select(store(a,i,v),j) = v if i = j
- Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << store[2] << std::endl;
- return RewriteResponse(REWRITE_DONE, store[2]);
- }
- // select(store(a,i,v),j) = select(a,j) if i /= j
- store = store[0];
- }
- if (store.getKind() == kind::STORE_ALL) {
- // select(store_all(v),i) = v
- ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
- n = storeAll.getValue();
- Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
- Assert(n.isConst());
- return RewriteResponse(REWRITE_DONE, n);
- }
- else if (store != node[0]) {
- n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
- Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
- return RewriteResponse(REWRITE_DONE, n);
- }
- break;
- }
- case kind::STORE: {
- TNode store = node[0];
- TNode value = node[2];
- // store(a,i,select(a,i)) = a
- if (value.getKind() == kind::SELECT &&
- value[0] == store &&
- value[1] == node[1]) {
- Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << store << std::endl;
- return RewriteResponse(REWRITE_DONE, store);
- }
- TNode index = node[1];
- if (store.isConst() && index.isConst() && value.isConst()) {
- // normalize constant
- Node n = normalizeConstant(node);
- Assert(n.isConst());
- Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
- return RewriteResponse(REWRITE_DONE, n);
- }
- if (store.getKind() == kind::STORE) {
- // store(store(a,i,v),j,w)
- bool val;
- if (index == store[1]) {
- val = true;
- }
- else if (index.isConst() && store[1].isConst()) {
- val = false;
- }
- else {
- Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
- if (eqRewritten.getKind() != kind::CONST_BOOLEAN) {
- Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << node << std::endl;
- return RewriteResponse(REWRITE_DONE, node);
- }
- val = eqRewritten.getConst<bool>();
- }
- NodeManager* nm = NodeManager::currentNM();
- if (val) {
- // store(store(a,i,v),i,w) = store(a,i,w)
- Node result = nm->mkNode(kind::STORE, store[0], index, value);
- Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << result << std::endl;
- return RewriteResponse(REWRITE_AGAIN, result);
- }
- else if (index < store[1]) {
- // store(store(a,i,v),j,w) = store(store(a,j,w),i,v)
- // IF i != j and j comes before i in the ordering
- std::vector<TNode> indices;
- std::vector<TNode> elements;
- indices.push_back(store[1]);
- elements.push_back(store[2]);
- store = store[0];
- Node n;
- while (store.getKind() == kind::STORE) {
- if (index == store[1]) {
- val = true;
- }
- else if (index.isConst() && store[1].isConst()) {
- val = false;
- }
- else {
- n = Rewriter::rewrite(mkEqNode(store[1], index));
- if (n.getKind() != kind::CONST_BOOLEAN) {
- break;
- }
- val = n.getConst<bool>();
- }
- if (val) {
- store = store[0];
- break;
- }
- else if (!(index < store[1])) {
- break;
- }
- indices.push_back(store[1]);
- elements.push_back(store[2]);
- store = store[0];
- }
- if (value.getKind() == kind::SELECT &&
- value[0] == store &&
- value[1] == index) {
- n = store;
- }
- else {
- n = nm->mkNode(kind::STORE, store, index, value);
- }
- while (!indices.empty()) {
- n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
- indices.pop_back();
- elements.pop_back();
- }
- Assert(n != node);
- Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
- return RewriteResponse(REWRITE_AGAIN, n);
- }
- }
- break;
- }
- case kind::EQUAL:{
- if(node[0] == node[1]) {
- Trace("arrays-postrewrite") << "Arrays::postRewrite returning true" << std::endl;
- return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
- }
- else if (node[0].isConst() && node[1].isConst()) {
- Trace("arrays-postrewrite") << "Arrays::postRewrite returning false" << std::endl;
- return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
- }
- if (node[0] > node[1]) {
- Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
- Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << newNode << std::endl;
- return RewriteResponse(REWRITE_DONE, newNode);
- }
- break;
- }
- default:
- break;
- }
- Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << node << std::endl;
- return RewriteResponse(REWRITE_DONE, node);
- }
-
- RewriteResponse preRewrite(TNode node) override
- {
- Trace("arrays-prerewrite") << "Arrays::preRewrite start " << node << std::endl;
- switch (node.getKind()) {
- case kind::SELECT: {
- TNode store = node[0];
- TNode index = node[1];
- Node n;
- bool val;
- while (store.getKind() == kind::STORE) {
- if (index == store[1]) {
- val = true;
- }
- else if (index.isConst() && store[1].isConst()) {
- val = false;
- }
- else {
- n = Rewriter::rewrite(mkEqNode(store[1], index));
- if (n.getKind() != kind::CONST_BOOLEAN) {
- break;
- }
- val = n.getConst<bool>();
- }
- if (val) {
- // select(store(a,i,v),j) = v if i = j
- Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << store[2] << std::endl;
- return RewriteResponse(REWRITE_AGAIN, store[2]);
- }
- // select(store(a,i,v),j) = select(a,j) if i /= j
- store = store[0];
- }
- if (store.getKind() == kind::STORE_ALL) {
- // select(store_all(v),i) = v
- ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
- n = storeAll.getValue();
- Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << n << std::endl;
- Assert(n.isConst());
- return RewriteResponse(REWRITE_DONE, n);
- }
- else if (store != node[0]) {
- n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
- Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << n << std::endl;
- return RewriteResponse(REWRITE_DONE, n);
- }
- break;
- }
- case kind::STORE: {
- TNode store = node[0];
- TNode value = node[2];
- // store(a,i,select(a,i)) = a
- if (value.getKind() == kind::SELECT &&
- value[0] == store &&
- value[1] == node[1]) {
- Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << store << std::endl;
- return RewriteResponse(REWRITE_AGAIN, store);
- }
- if (store.getKind() == kind::STORE) {
- // store(store(a,i,v),j,w)
- TNode index = node[1];
- bool val;
- if (index == store[1]) {
- val = true;
- }
- else if (index.isConst() && store[1].isConst()) {
- val = false;
- }
- else {
- Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
- if (eqRewritten.getKind() != kind::CONST_BOOLEAN) {
- break;
- }
- val = eqRewritten.getConst<bool>();
- }
- NodeManager* nm = NodeManager::currentNM();
- if (val) {
- // store(store(a,i,v),i,w) = store(a,i,w)
- Node newNode = nm->mkNode(kind::STORE, store[0], index, value);
- Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << newNode << std::endl;
- return RewriteResponse(REWRITE_DONE, newNode);
- }
- }
- break;
- }
- case kind::EQUAL:{
- if(node[0] == node[1]) {
- Trace("arrays-prerewrite") << "Arrays::preRewrite returning true" << std::endl;
- return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
- }
- break;
- }
- default:
- break;
- }
-
- Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << node << std::endl;
- return RewriteResponse(REWRITE_DONE, node);
- }
+ TrustNode expandDefinition(Node node) override;
static inline void init() {}
static inline void shutdown() {}
* See the rewrite rules for these kinds below.
*/
RewriteResponse preRewrite(TNode n) override;
-
private:
/**
* rewrites for n include:
}
}
-TrustNode TheoryBags::expandDefinition(Node n)
-{
- // TODO(projects#224): add choose and is_singleton here
- return TrustNode::null();
-}
-
void TheoryBags::presolve() {}
/**************************** eq::NotifyClass *****************************/
Node getModelValue(TNode) override;
std::string identify() const override { return "THEORY_BAGS"; }
void preRegisterTerm(TNode n) override;
- TrustNode expandDefinition(Node n) override;
void presolve() override;
private:
}
}
-TrustNode TheoryBV::expandDefinition(Node node)
-{
- Debug("bitvector-expandDefinition")
- << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
-
- Node ret;
- switch (node.getKind())
- {
- case kind::BITVECTOR_SDIV:
- case kind::BITVECTOR_SREM:
- case kind::BITVECTOR_SMOD:
- ret = TheoryBVRewriter::eliminateBVSDiv(node);
- break;
-
- default: break;
- }
- if (!ret.isNull() && node != ret)
- {
- return TrustNode::mkTrustRewrite(node, ret, nullptr);
- }
- return TrustNode::null();
-}
-
void TheoryBV::preRegisterTerm(TNode node)
{
d_internal->preRegisterTerm(node);
TrustNode TheoryBV::ppRewrite(TNode t, std::vector<SkolemLemma>& lems)
{
// first, see if we need to expand definitions
- TrustNode texp = expandDefinition(t);
+ TrustNode texp = d_rewriter.expandDefinition(t);
if (!texp.isNull())
{
return texp;
void finishInit() override;
- TrustNode expandDefinition(Node node) override;
-
void preRegisterTerm(TNode n) override;
bool preCheck(Effort e) override;
return res;
}
+TrustNode TheoryBVRewriter::expandDefinition(Node node)
+{
+ Debug("bitvector-expandDefinition")
+ << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
+ Node ret;
+ switch (node.getKind())
+ {
+ case kind::BITVECTOR_SDIV:
+ case kind::BITVECTOR_SREM:
+ case kind::BITVECTOR_SMOD: ret = eliminateBVSDiv(node); break;
+
+ default: break;
+ }
+ if (!ret.isNull() && node != ret)
+ {
+ return TrustNode::mkTrustRewrite(node, ret, nullptr);
+ }
+ return TrustNode::null();
+}
+
RewriteResponse TheoryBVRewriter::RewriteBitOf(TNode node, bool prerewrite)
{
Node resultNode = LinearRewriteStrategy<RewriteRule<BitOfConst>>::apply(node);
RewriteResponse postRewrite(TNode node) override;
RewriteResponse preRewrite(TNode node) override;
+ TrustNode expandDefinition(Node node) override;
+
private:
static RewriteResponse IdentityRewrite(TNode node, bool prerewrite = false);
static RewriteResponse UndefinedRewrite(TNode node, bool prerewrite = false);
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "expr/sygus_datatype.h"
#include "options/datatypes_options.h"
#include "theory/datatypes/sygus_datatype_utils.h"
return n;
}
+TrustNode DatatypesRewriter::expandDefinition(Node n)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ TypeNode tn = n.getType();
+ Node ret;
+ switch (n.getKind())
+ {
+ case kind::APPLY_SELECTOR:
+ {
+ Node selector = n.getOperator();
+ // APPLY_SELECTOR always applies to an external selector, cindexOf is
+ // legal here
+ size_t cindex = utils::cindexOf(selector);
+ const DType& dt = utils::datatypeOf(selector);
+ const DTypeConstructor& c = dt[cindex];
+ Node selector_use;
+ TypeNode ndt = n[0].getType();
+ if (options::dtSharedSelectors())
+ {
+ size_t selectorIndex = utils::indexOf(selector);
+ Trace("dt-expand") << "...selector index = " << selectorIndex
+ << std::endl;
+ Assert(selectorIndex < c.getNumArgs());
+ selector_use = c.getSelectorInternal(ndt, selectorIndex);
+ }
+ else
+ {
+ selector_use = selector;
+ }
+ Node sel = nm->mkNode(kind::APPLY_SELECTOR_TOTAL, selector_use, n[0]);
+ if (options::dtRewriteErrorSel())
+ {
+ ret = sel;
+ }
+ else
+ {
+ Node tester = c.getTester();
+ Node tst = nm->mkNode(APPLY_TESTER, tester, n[0]);
+ SkolemManager* sm = nm->getSkolemManager();
+ TypeNode tnw = nm->mkFunctionType(ndt, n.getType());
+ Node f =
+ sm->mkSkolemFunction(SkolemFunId::SELECTOR_WRONG, tnw, selector);
+ Node sk = nm->mkNode(kind::APPLY_UF, f, n[0]);
+ ret = nm->mkNode(kind::ITE, tst, sel, sk);
+ Trace("dt-expand") << "Expand def : " << n << " to " << ret
+ << std::endl;
+ }
+ }
+ break;
+ case TUPLE_UPDATE:
+ case RECORD_UPDATE:
+ {
+ Assert(tn.isDatatype());
+ const DType& dt = tn.getDType();
+ NodeBuilder b(APPLY_CONSTRUCTOR);
+ b << dt[0].getConstructor();
+ size_t size, updateIndex;
+ if (n.getKind() == TUPLE_UPDATE)
+ {
+ Assert(tn.isTuple());
+ size = tn.getTupleLength();
+ updateIndex = n.getOperator().getConst<TupleUpdate>().getIndex();
+ }
+ else
+ {
+ Assert(tn.isRecord());
+ const DTypeConstructor& recCons = dt[0];
+ size = recCons.getNumArgs();
+ // get the index for the name
+ updateIndex = recCons.getSelectorIndexForName(
+ n.getOperator().getConst<RecordUpdate>().getField());
+ }
+ Debug("tuprec") << "expr is " << n << std::endl;
+ Debug("tuprec") << "updateIndex is " << updateIndex << std::endl;
+ Debug("tuprec") << "t is " << tn << std::endl;
+ Debug("tuprec") << "t has arity " << size << std::endl;
+ for (size_t i = 0; i < size; ++i)
+ {
+ if (i == updateIndex)
+ {
+ b << n[1];
+ Debug("tuprec") << "arg " << i << " gets updated to " << n[1]
+ << std::endl;
+ }
+ else
+ {
+ b << nm->mkNode(
+ APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, i), n[0]);
+ Debug("tuprec") << "arg " << i << " copies "
+ << b[b.getNumChildren() - 1] << std::endl;
+ }
+ }
+ ret = b;
+ Debug("tuprec") << "return " << ret << std::endl;
+ }
+ break;
+ default: break;
+ }
+ if (!ret.isNull() && n != ret)
+ {
+ return TrustNode::mkTrustRewrite(n, ret, nullptr);
+ }
+ return TrustNode::null();
+}
+
} // namespace datatypes
} // namespace theory
} // namespace cvc5
* on all top-level codatatype subterms of n.
*/
static Node normalizeConstant(Node n);
+ /** expand defintions */
+ TrustNode expandDefinition(Node n) override;
private:
/** rewrite constructor term in */
d_im.process();
}
-TrustNode TheoryDatatypes::expandDefinition(Node n)
-{
- NodeManager* nm = NodeManager::currentNM();
- TypeNode tn = n.getType();
- Node ret;
- switch (n.getKind())
- {
- case kind::APPLY_SELECTOR:
- {
- Node selector = n.getOperator();
- // APPLY_SELECTOR always applies to an external selector, cindexOf is
- // legal here
- size_t cindex = utils::cindexOf(selector);
- const DType& dt = utils::datatypeOf(selector);
- const DTypeConstructor& c = dt[cindex];
- Node selector_use;
- TypeNode ndt = n[0].getType();
- if (options::dtSharedSelectors())
- {
- size_t selectorIndex = utils::indexOf(selector);
- Trace("dt-expand") << "...selector index = " << selectorIndex
- << std::endl;
- Assert(selectorIndex < c.getNumArgs());
- selector_use = c.getSelectorInternal(ndt, selectorIndex);
- }else{
- selector_use = selector;
- }
- Node sel = nm->mkNode(kind::APPLY_SELECTOR_TOTAL, selector_use, n[0]);
- if (options::dtRewriteErrorSel())
- {
- ret = sel;
- }
- else
- {
- Node tester = c.getTester();
- Node tst = nm->mkNode(APPLY_TESTER, tester, n[0]);
- tst = Rewriter::rewrite(tst);
- if (tst == d_true)
- {
- ret = sel;
- }else{
- SkolemManager* sm = nm->getSkolemManager();
- TypeNode tnw = nm->mkFunctionType(ndt, n.getType());
- Node f =
- sm->mkSkolemFunction(SkolemFunId::SELECTOR_WRONG, tnw, selector);
- Node sk = nm->mkNode(kind::APPLY_UF, f, n[0]);
- if (tst == nm->mkConst(false))
- {
- ret = sk;
- }
- else
- {
- ret = nm->mkNode(kind::ITE, tst, sel, sk);
- }
- }
- Trace("dt-expand") << "Expand def : " << n << " to " << ret
- << std::endl;
- }
- }
- break;
- case TUPLE_UPDATE:
- case RECORD_UPDATE:
- {
- Assert(tn.isDatatype());
- const DType& dt = tn.getDType();
- NodeBuilder b(APPLY_CONSTRUCTOR);
- b << dt[0].getConstructor();
- size_t size, updateIndex;
- if (n.getKind() == TUPLE_UPDATE)
- {
- Assert(tn.isTuple());
- size = tn.getTupleLength();
- updateIndex = n.getOperator().getConst<TupleUpdate>().getIndex();
- }
- else
- {
- Assert(tn.isRecord());
- const DTypeConstructor& recCons = dt[0];
- size = recCons.getNumArgs();
- // get the index for the name
- updateIndex = recCons.getSelectorIndexForName(
- n.getOperator().getConst<RecordUpdate>().getField());
- }
- Debug("tuprec") << "expr is " << n << std::endl;
- Debug("tuprec") << "updateIndex is " << updateIndex << std::endl;
- Debug("tuprec") << "t is " << tn << std::endl;
- Debug("tuprec") << "t has arity " << size << std::endl;
- for (size_t i = 0; i < size; ++i)
- {
- if (i == updateIndex)
- {
- b << n[1];
- Debug("tuprec") << "arg " << i << " gets updated to " << n[1]
- << std::endl;
- }
- else
- {
- b << nm->mkNode(
- APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, i), n[0]);
- Debug("tuprec") << "arg " << i << " copies "
- << b[b.getNumChildren() - 1] << std::endl;
- }
- }
- ret = b;
- Debug("tuprec") << "return " << ret << std::endl;
- }
- break;
- default: break;
- }
- if (!ret.isNull() && n != ret)
- {
- return TrustNode::mkTrustRewrite(n, ret, nullptr);
- }
- return TrustNode::null();
-}
-
TrustNode TheoryDatatypes::ppRewrite(TNode in, std::vector<SkolemLemma>& lems)
{
Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
// first, see if we need to expand definitions
- TrustNode texp = expandDefinition(in);
+ TrustNode texp = d_rewriter.expandDefinition(in);
if (!texp.isNull())
{
return texp;
void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
//--------------------------------- end standard check
void preRegisterTerm(TNode n) override;
- TrustNode expandDefinition(Node n) override;
TrustNode ppRewrite(TNode n, std::vector<SkolemLemma>& lems) override;
EqualityStatus getEqualityStatus(TNode a, TNode b) override;
std::string identify() const override
return;
}
-TrustNode TheoryFp::expandDefinition(Node node)
-{
- return d_rewriter.expandDefinition(node);
-}
-
void TheoryFp::handleLemma(Node node, InferenceId id)
{
Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl;
//--------------------------------- end initialization
void preRegisterTerm(TNode node) override;
- TrustNode expandDefinition(Node node) override;
TrustNode ppRewrite(TNode node, std::vector<SkolemLemma>& lems) override;
//--------------------------------- standard check
// often this will suffice
return postRewrite(equality).d_node;
}
- /** Expand definitions in node. */
- TrustNode expandDefinition(Node node);
+ /** Expand definitions in node */
+ TrustNode expandDefinition(Node node) override;
protected:
/** TODO: document (projects issue #265) */
d_internal->preRegisterTerm(node);
}
-TrustNode TheorySets::expandDefinition(Node n)
-{
- // we currently do not expand any set operators
- return TrustNode::null();
-}
-
TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
{
Kind nk = n.getKind();
Node getModelValue(TNode) override;
std::string identify() const override { return "THEORY_SETS"; }
void preRegisterTerm(TNode node) override;
- /** Expand partial operators (choose) from n. */
- TrustNode expandDefinition(Node n) override;
/**
* If the sets-ext option is not set and we have an extended operator,
* we throw an exception. Additionally, we expand operators like choose
#include "theory/rewriter.h"
#include "theory/strings/arith_entail.h"
#include "theory/strings/regexp_entail.h"
+#include "theory/strings/skolem_cache.h"
#include "theory/strings/strings_rewriter.h"
#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/word.h"
return RewriteResponse(REWRITE_DONE, node);
}
+TrustNode SequencesRewriter::expandDefinition(Node node)
+{
+ Trace("strings-exp-def") << "SequencesRewriter::expandDefinition : " << node
+ << std::endl;
+
+ if (node.getKind() == kind::SEQ_NTH)
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ Node s = node[0];
+ Node n = node[1];
+ // seq.nth(s, n) --> ite(0 <= n < len(s), seq.nth_total(s,n), Uf(s, n))
+ Node cond = nm->mkNode(AND,
+ nm->mkNode(LEQ, nm->mkConst(Rational(0)), n),
+ nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s)));
+ Node ss = nm->mkNode(SEQ_NTH_TOTAL, s, n);
+ Node uf = SkolemCache::mkSkolemSeqNth(s.getType(), "Uf");
+ Node u = nm->mkNode(APPLY_UF, uf, s, n);
+ Node ret = nm->mkNode(ITE, cond, ss, u);
+ Trace("strings-exp-def") << "...return " << ret << std::endl;
+ return TrustNode::mkTrustRewrite(node, ret, nullptr);
+ }
+ return TrustNode::null();
+}
+
Node SequencesRewriter::rewriteSeqNth(Node node)
{
Assert(node.getKind() == SEQ_NTH || node.getKind() == SEQ_NTH_TOTAL);
public:
RewriteResponse postRewrite(TNode node) override;
RewriteResponse preRewrite(TNode node) override;
+ /** Expand definition */
+ TrustNode expandDefinition(Node n) override;
/** rewrite equality
*
d_extTheory.registerTerm(n);
}
-TrustNode TheoryStrings::expandDefinition(Node node)
-{
- Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl;
-
- if (node.getKind() == kind::SEQ_NTH)
- {
- NodeManager* nm = NodeManager::currentNM();
- Node s = node[0];
- Node n = node[1];
- // seq.nth(s, n) --> ite(0 <= n < len(s), seq.nth_total(s,n), Uf(s, n))
- Node cond = nm->mkNode(AND,
- nm->mkNode(LEQ, d_zero, n),
- nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s)));
- Node ss = nm->mkNode(SEQ_NTH_TOTAL, s, n);
- Node uf = SkolemCache::mkSkolemSeqNth(s.getType(), "Uf");
- Node u = nm->mkNode(APPLY_UF, uf, s, n);
- Node ret = nm->mkNode(ITE, cond, ss, u);
- Trace("strings-exp-def") << "...return " << ret << std::endl;
- return TrustNode::mkTrustRewrite(node, ret, nullptr);
- }
- return TrustNode::null();
-}
-
bool TheoryStrings::preNotifyFact(
TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
{
void shutdown() override {}
/** preregister term */
void preRegisterTerm(TNode n) override;
- /** Expand definition */
- TrustNode expandDefinition(Node n) override;
//--------------------------------- standard check
/** Do we need a check call at last call effort? */
bool needsCheckLastEffort() override;
*/
TheoryInferenceManager* getInferenceManager() { return d_inferManager; }
- /**
- * Expand definitions in the term node. This returns a term that is
- * equivalent to node. It wraps this term in a TrustNode of kind
- * TrustNodeKind::REWRITE. If node is unchanged by this method, the
- * null TrustNode may be returned. This is an optimization to avoid
- * constructing the trivial equality (= node node) internally within
- * TrustNode.
- *
- * The purpose of this method is typically to eliminate the operators in node
- * that are syntax sugar that cannot otherwise be eliminated during rewriting.
- * For example, division relies on the introduction of an uninterpreted
- * function for the divide-by-zero case, which we do not introduce with
- * the rewriter, since this function may be cached in a non-global fashion.
- *
- * Some theories have kinds that are effectively definitions and should be
- * expanded before they are handled. Definitions allow a much wider range of
- * actions than the normal forms given by the rewriter. However no
- * assumptions can be made about subterms having been expanded or rewritten.
- * Where possible rewrite rules should be used, definitions should only be
- * used when rewrites are not possible, for example in handling
- * under-specified operations using partially defined functions.
- *
- * Some theories like sets use expandDefinition as a "context
- * independent preRegisterTerm". This is required for cases where
- * a theory wants to be notified about a term before preprocessing
- * and simplification but doesn't necessarily want to rewrite it.
- */
- virtual TrustNode expandDefinition(Node node)
- {
- // by default, do nothing
- return TrustNode::null();
- }
-
/**
* Pre-register a term. Done one time for a Node per SAT context level.
*/
return TrustNode::null();
}
+TrustNode TheoryRewriter::expandDefinition(Node node)
+{
+ // no expansion
+ return TrustNode::null();
+}
+
} // namespace theory
} // namespace cvc5
* node if no rewrites are applied.
*/
virtual TrustNode rewriteEqualityExtWithProof(Node node);
+
+ /**
+ * Expand definitions in the term node. This returns a term that is
+ * equivalent to node. It wraps this term in a TrustNode of kind
+ * TrustNodeKind::REWRITE. If node is unchanged by this method, the
+ * null TrustNode may be returned. This is an optimization to avoid
+ * constructing the trivial equality (= node node) internally within
+ * TrustNode.
+ *
+ * The purpose of this method is typically to eliminate the operators in node
+ * that are syntax sugar that cannot otherwise be eliminated during rewriting.
+ * For example, division relies on the introduction of an uninterpreted
+ * function for the divide-by-zero case, which we do not introduce with
+ * the standard rewrite methods.
+ *
+ * Some theories have kinds that are effectively definitions and should be
+ * expanded before they are handled. Definitions allow a much wider range of
+ * actions than the normal forms given by the rewriter. However no
+ * assumptions can be made about subterms having been expanded or rewritten.
+ * Where possible rewrite rules should be used, definitions should only be
+ * used when rewrites are not possible, for example in handling
+ * under-specified operations using partially defined functions.
+ */
+ virtual TrustNode expandDefinition(Node node);
};
} // namespace theory
projects / cvc5.git / commitdiff