diff options
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 0f5d9ec8b..71e040ccc 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -2312,6 +2312,61 @@ std::string TheoryArrays::TheoryArraysDecisionStrategy::identify() const return std::string("th_arrays_dec"); } +Node 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); + return nm->mkNode(kind::FORALL, bvl, implies); + } + return node; +} + }/* CVC4::theory::arrays namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |