diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/array_store_all.cpp | 57 | ||||
-rw-r--r-- | src/expr/array_store_all.h | 21 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 5 | ||||
-rw-r--r-- | src/expr/type_node.h | 5 |
4 files changed, 47 insertions, 41 deletions
diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp index 6655c7b61..0777bc1cf 100644 --- a/src/expr/array_store_all.cpp +++ b/src/expr/array_store_all.cpp @@ -21,15 +21,16 @@ #include <iostream> #include "base/check.h" -#include "expr/expr.h" -#include "expr/type.h" +#include "expr/node.h" +#include "expr/type_node.h" using namespace std; namespace CVC4 { -ArrayStoreAll::ArrayStoreAll(const ArrayType& type, const Expr& expr) - : d_type(), d_expr() { +ArrayStoreAll::ArrayStoreAll(const TypeNode& type, const Node& value) + : d_type(), d_value() +{ // this check is stronger than the assertion check in the expr manager that // ArrayTypes are actually array types // because this check is done in production builds too @@ -39,38 +40,41 @@ ArrayStoreAll::ArrayStoreAll(const ArrayType& type, const Expr& expr) type.toString().c_str()); PrettyCheckArgument( - expr.getType().isComparableTo(type.getConstituentType()), expr, + value.getType().isComparableTo(type.getArrayConstituentType()), + value, "expr type `%s' does not match constituent type of array type `%s'", - expr.getType().toString().c_str(), type.toString().c_str()); + value.getType().toString().c_str(), + type.toString().c_str()); - PrettyCheckArgument(expr.isConst(), expr, - "ArrayStoreAll requires a constant expression"); + PrettyCheckArgument( + value.isConst(), value, "ArrayStoreAll requires a constant expression"); - // Delay allocation until the checks above have been performed. If these fail, - // the memory for d_type and d_expr should not leak. The alternative is catch, - // delete and re-throw. - d_type.reset(new ArrayType(type)); - d_expr.reset(new Expr(expr)); + // Delay allocation until the checks above have been performed. If these + // fail, the memory for d_type and d_value should not leak. The alternative + // is catch, delete and re-throw. + d_type.reset(new TypeNode(type)); + d_value.reset(new Node(value)); } ArrayStoreAll::ArrayStoreAll(const ArrayStoreAll& other) - : d_type(new ArrayType(other.getType())), - d_expr(new Expr(other.getExpr())) {} + : d_type(new TypeNode(other.getType())), d_value(new Node(other.getValue())) +{ +} ArrayStoreAll::~ArrayStoreAll() {} ArrayStoreAll& ArrayStoreAll::operator=(const ArrayStoreAll& other) { (*d_type) = other.getType(); - (*d_expr) = other.getExpr(); + (*d_value) = other.getValue(); return *this; } -const ArrayType& ArrayStoreAll::getType() const { return *d_type; } +const TypeNode& ArrayStoreAll::getType() const { return *d_type; } -const Expr& ArrayStoreAll::getExpr() const { return *d_expr; } +const Node& ArrayStoreAll::getValue() const { return *d_value; } bool ArrayStoreAll::operator==(const ArrayStoreAll& asa) const { - return getType() == asa.getType() && getExpr() == asa.getExpr(); + return getType() == asa.getType() && getValue() == asa.getValue(); } bool ArrayStoreAll::operator!=(const ArrayStoreAll& asa) const @@ -80,14 +84,14 @@ bool ArrayStoreAll::operator!=(const ArrayStoreAll& asa) const bool ArrayStoreAll::operator<(const ArrayStoreAll& asa) const { - return (getType() < asa.getType()) || - (getType() == asa.getType() && getExpr() < asa.getExpr()); + return (getType() < asa.getType()) + || (getType() == asa.getType() && getValue() < asa.getValue()); } bool ArrayStoreAll::operator<=(const ArrayStoreAll& asa) const { - return (getType() < asa.getType()) || - (getType() == asa.getType() && getExpr() <= asa.getExpr()); + return (getType() < asa.getType()) + || (getType() == asa.getType() && getValue() <= asa.getValue()); } bool ArrayStoreAll::operator>(const ArrayStoreAll& asa) const @@ -101,12 +105,13 @@ bool ArrayStoreAll::operator>=(const ArrayStoreAll& asa) const } std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) { - return out << "__array_store_all__(" << asa.getType() << ", " << asa.getExpr() - << ')'; + return out << "__array_store_all__(" << asa.getType() << ", " + << asa.getValue() << ')'; } size_t ArrayStoreAllHashFunction::operator()(const ArrayStoreAll& asa) const { - return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr()); + return TypeNodeHashFunction()(asa.getType()) + * NodeHashFunction()(asa.getValue()); } } // namespace CVC4 diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h index 2d251257c..7fa25516c 100644 --- a/src/expr/array_store_all.h +++ b/src/expr/array_store_all.h @@ -24,29 +24,28 @@ #include <iosfwd> #include <memory> -namespace CVC4 { -// messy; Expr needs ArrayStoreAll (because it's the payload of a -// CONSTANT-kinded expression), and ArrayStoreAll needs Expr. -class Expr; -class ArrayType; -} // namespace CVC4 namespace CVC4 { +template <bool ref_count> +class NodeTemplate; +typedef NodeTemplate<true> Node; +class TypeNode; + class CVC4_PUBLIC ArrayStoreAll { public: /** * @throws IllegalArgumentException if `type` is not an array or if `expr` is * not a constant of type `type`. */ - ArrayStoreAll(const ArrayType& type, const Expr& expr); + ArrayStoreAll(const TypeNode& type, const Node& value); ~ArrayStoreAll(); ArrayStoreAll(const ArrayStoreAll& other); ArrayStoreAll& operator=(const ArrayStoreAll& other); - const ArrayType& getType() const; - const Expr& getExpr() const; + const TypeNode& getType() const; + const Node& getValue() const; bool operator==(const ArrayStoreAll& asa) const; bool operator!=(const ArrayStoreAll& asa) const; @@ -56,8 +55,8 @@ class CVC4_PUBLIC ArrayStoreAll { bool operator>=(const ArrayStoreAll& asa) const; private: - std::unique_ptr<ArrayType> d_type; - std::unique_ptr<Expr> d_expr; + std::unique_ptr<TypeNode> d_type; + std::unique_ptr<Node> d_value; }; /* class ArrayStoreAll */ std::ostream& operator<<(std::ostream& out, diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 50884f715..132d4bfaa 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -694,8 +694,9 @@ static Node exportConstant(TNode n, NodeManager* to, ExprManagerMapCollection& v // for export so those don't matter. ExprManager* toEm = to->toExprManager(); const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>(); - return to->mkConst(ArrayStoreAll(asa.getType().exportTo(toEm, vmap), - asa.getExpr().exportTo(toEm, vmap))); + return to->mkConst(ArrayStoreAll( + TypeNode::fromType(asa.getType().toType().exportTo(toEm, vmap)), + Node::fromExpr(asa.getValue().toExpr().exportTo(toEm, vmap)))); } switch(n.getKind()) { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 5082fe1d3..12c96d307 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -409,7 +409,7 @@ public: * Convert this TypeNode into a Type using the currently-in-scope * manager. */ - inline Type toType(); + inline Type toType() const; /** * Convert a Type into a TypeNode. @@ -754,7 +754,8 @@ typedef TypeNode::HashFunction TypeNodeHashFunction; namespace CVC4 { -inline Type TypeNode::toType() { +inline Type TypeNode::toType() const +{ return NodeManager::currentNM()->toType(*this); } |