summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/array_store_all.cpp57
-rw-r--r--src/expr/array_store_all.h21
-rw-r--r--src/expr/expr_template.cpp5
-rw-r--r--src/expr/type_node.h5
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback