+Node TheoryArraysRewriter::expandEqRange(TNode node)
+{
+ Assert(node.getKind() == kind::EQ_RANGE);
+
+ NodeManager* nm = NodeManager::currentNM();
+ TNode a = node[0];
+ TNode b = node[1];
+ TNode i = node[2];
+ TNode j = node[3];
+ Node k = SkolemCache::getEqRangeVar(node);
+ 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 "
+ << node.getKind();
+ }
+
+ 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);
+ return nm->mkNode(kind::FORALL, bvl, implies);
+}
+