summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/api/cvc4cpp.cpp8
-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
-rw-r--r--src/printer/cvc/cvc_printer.cpp5
-rw-r--r--src/printer/smt2/smt2_printer.cpp2
-rw-r--r--src/theory/arrays/theory_arrays.cpp6
-rw-r--r--src/theory/arrays/theory_arrays_rewriter.h8
-rw-r--r--src/theory/arrays/theory_arrays_type_rules.h5
-rw-r--r--src/theory/arrays/type_enumerator.h3
-rw-r--r--src/theory/builtin/theory_builtin_rewriter.cpp5
-rw-r--r--test/unit/expr/expr_public.h78
-rw-r--r--test/unit/theory/theory_black.h6
-rw-r--r--test/unit/theory/type_enumerator_white.h21
-rw-r--r--test/unit/util/CMakeLists.txt2
-rw-r--r--test/unit/util/array_store_all_black.h83
-rw-r--r--test/unit/util/array_store_all_white.h94
18 files changed, 224 insertions, 190 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 550dd760b..3cca1a071 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1564,11 +1564,12 @@ bool Term::isConst() const
Term Term::getConstArrayBase() const
{
+ CVC4::ExprManagerScope exmgrs(*(d_solver->getExprManager()));
CVC4_API_CHECK_NOT_NULL;
// CONST_ARRAY kind maps to STORE_ALL internal kind
CVC4_API_CHECK(d_expr->getKind() == CVC4::Kind::STORE_ALL)
<< "Expecting a CONST_ARRAY Term when calling getConstArrayBase()";
- return Term(d_solver, d_expr->getConst<ArrayStoreAll>().getExpr());
+ return Term(d_solver, d_expr->getConst<ArrayStoreAll>().getValue().toExpr());
}
std::vector<Term> Term::getConstSequenceElements() const
@@ -3511,6 +3512,7 @@ Term Solver::mkBitVector(uint32_t size, std::string& s, uint32_t base) const
Term Solver::mkConstArray(Sort sort, Term val) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
CVC4_API_ARG_CHECK_NOT_NULL(sort);
CVC4_API_ARG_CHECK_NOT_NULL(val);
CVC4_API_SOLVER_CHECK_SORT(sort);
@@ -3518,8 +3520,8 @@ Term Solver::mkConstArray(Sort sort, Term val) const
CVC4_API_CHECK(sort.isArray()) << "Not an array sort.";
CVC4_API_CHECK(sort.getArrayElementSort().isComparableTo(val.getSort()))
<< "Value does not match element sort.";
- Term res = mkValHelper<CVC4::ArrayStoreAll>(
- CVC4::ArrayStoreAll(*sort.d_type, *val.d_expr));
+ Term res = mkValHelper<CVC4::ArrayStoreAll>(CVC4::ArrayStoreAll(
+ TypeNode::fromType(*sort.d_type), Node::fromExpr(*val.d_expr)));
return res;
CVC4_API_SOLVER_TRY_CATCH_END;
}
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);
}
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 216fb0517..900651e1d 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -246,8 +246,9 @@ void CvcPrinter::toStream(
case kind::STORE_ALL: {
const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>();
- out << "ARRAY(" << asa.getType().getIndexType() << " OF "
- << asa.getType().getConstituentType() << ") : " << asa.getExpr();
+ out << "ARRAY(" << asa.getType().getArrayIndexType() << " OF "
+ << asa.getType().getArrayConstituentType()
+ << ") : " << asa.getValue();
break;
}
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 3eedee600..49f786f78 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -237,7 +237,7 @@ void Smt2Printer::toStream(std::ostream& out,
case kind::STORE_ALL: {
ArrayStoreAll asa = n.getConst<ArrayStoreAll>();
- out << "((as const " << asa.getType() << ") " << asa.getExpr() << ")";
+ out << "((as const " << asa.getType() << ") " << asa.getValue() << ")";
break;
}
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 49f93286e..37443c070 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -808,7 +808,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
break;
}
ArrayStoreAll storeAll = node.getConst<ArrayStoreAll>();
- Node defaultValue = Node::fromExpr(storeAll.getExpr());
+ Node defaultValue = storeAll.getValue();
if (!defaultValue.isConst()) {
throw LogicException("Array theory solver does not yet support non-constant default values for arrays");
}
@@ -1230,7 +1230,7 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m)
}
// Build the STORE_ALL term with the default value
- rep = nm->mkConst(ArrayStoreAll(nrep.getType().toType(), rep.toExpr()));
+ rep = nm->mkConst(ArrayStoreAll(nrep.getType(), rep));
/*
}
else {
@@ -1904,7 +1904,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
TNode constArr = d_infoMap.getConstArr(a);
if (!constArr.isNull()) {
ArrayStoreAll storeAll = constArr.getConst<ArrayStoreAll>();
- Node defValue = Node::fromExpr(storeAll.getExpr());
+ Node defValue = storeAll.getValue();
Node selConst = NodeManager::currentNM()->mkNode(kind::SELECT, constArr, i);
if (!d_equalityEngine.hasTerm(selConst)) {
preRegisterTermInternal(selConst);
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index e81b7d7c0..e8f03c1d0 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -93,7 +93,7 @@ class TheoryArraysRewriter : public TheoryRewriter
}
Assert(store.getKind() == kind::STORE_ALL);
ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
- Node defaultValue = Node::fromExpr(storeAll.getExpr());
+ Node defaultValue = storeAll.getValue();
NodeManager* nm = NodeManager::currentNM();
// Check if we are writing to default value - if so the store
@@ -214,7 +214,7 @@ class TheoryArraysRewriter : public TheoryRewriter
std::sort(newIndices.begin(), newIndices.end());
}
- n = nm->mkConst(ArrayStoreAll(node.getType().toType(), maxValue.toExpr()));
+ 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())) {
@@ -267,7 +267,7 @@ class TheoryArraysRewriter : public TheoryRewriter
if (store.getKind() == kind::STORE_ALL) {
// select(store_all(v),i) = v
ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
- n = Node::fromExpr(storeAll.getExpr());
+ n = storeAll.getValue();
Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
Assert(n.isConst());
return RewriteResponse(REWRITE_DONE, n);
@@ -432,7 +432,7 @@ class TheoryArraysRewriter : public TheoryRewriter
if (store.getKind() == kind::STORE_ALL) {
// select(store_all(v),i) = v
ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
- n = Node::fromExpr(storeAll.getExpr());
+ n = storeAll.getValue();
Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << n << std::endl;
Assert(n.isConst());
return RewriteResponse(REWRITE_DONE, n);
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index e5681d50f..56c51d9bf 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -69,8 +69,7 @@ struct ArrayStoreTypeRule {
else {
Assert(n.getKind() == kind::STORE_ALL);
ArrayStoreAll storeAll = n.getConst<ArrayStoreAll>();
- ArrayType arrayType = storeAll.getType();
- return TypeNode::fromType(arrayType);
+ return storeAll.getType();
}
}
@@ -106,7 +105,7 @@ struct ArrayStoreTypeRule {
}
Assert(store.getKind() == kind::STORE_ALL);
ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
- Node defaultValue = Node::fromExpr(storeAll.getExpr());
+ Node defaultValue = storeAll.getValue();
if (value == defaultValue) {
return false;
}
diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index 3da793617..5894501b2 100644
--- a/src/theory/arrays/type_enumerator.h
+++ b/src/theory/arrays/type_enumerator.h
@@ -53,7 +53,8 @@ class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
{
d_indexVec.push_back(*d_index);
d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
- d_arrayConst = d_nm->mkConst(ArrayStoreAll(type.toType(), (*(*d_constituentVec.back())).toExpr()));
+ d_arrayConst =
+ d_nm->mkConst(ArrayStoreAll(type, (*(*d_constituentVec.back()))));
Trace("array-type-enum") << "Array const : " << d_arrayConst << std::endl;
}
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index 245e7cb8a..456b0cbca 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -185,7 +185,7 @@ Node TheoryBuiltinRewriter::getLambdaForArrayRepresentationRec( TNode a, TNode b
}
}else if( a.getKind()==kind::STORE_ALL ){
ArrayStoreAll storeAll = a.getConst<ArrayStoreAll>();
- Node sa = Node::fromExpr(storeAll.getExpr());
+ Node sa = storeAll.getValue();
// convert the default value recursively (bounded by the number of arguments in bvl)
ret = getLambdaForArrayRepresentationRec( sa, bvl, bvlIndex+1, visited );
}
@@ -448,8 +448,7 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambdaRec(TNode n,
}
Trace("builtin-rewrite-debug2") << " make array store all " << curr.getType() << " annotated : " << array_type << std::endl;
Assert(curr.getType().isSubtypeOf(array_type.getArrayConstituentType()));
- curr = nm->mkConst(
- ArrayStoreAll((ArrayType(array_type.toType())), curr.toExpr()));
+ curr = nm->mkConst(ArrayStoreAll(array_type, curr));
Trace("builtin-rewrite-debug2") << " build array..." << std::endl;
// can only build if default value is constant (since array store all must be constant)
Trace("builtin-rewrite-debug2") << " got constant base " << curr << std::endl;
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 86de45fe9..f8ccd23d4 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -23,6 +23,9 @@
#include "base/exception.h"
#include "expr/expr.h"
#include "expr/expr_manager.h"
+#include "expr/expr_manager_scope.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
#include "options/options.h"
using namespace CVC4;
@@ -85,7 +88,6 @@ class ExprPublic : public CxxTest::TestSuite {
delete c_bool_and;
delete b_bool;
delete a_bool;
-
delete d_slv;
}
catch (Exception& e)
@@ -369,40 +371,46 @@ class ExprPublic : public CxxTest::TestSuite {
TS_ASSERT(cons_1_nil.isConst());
TS_ASSERT(cons_1_cons_2_nil.isConst());
- ArrayType arrType = d_em->mkArrayType(d_em->integerType(), d_em->integerType());
- Expr zero = d_em->mkConst(Rational(0));
- Expr one = d_em->mkConst(Rational(1));
- Expr storeAll = d_em->mkConst(ArrayStoreAll(arrType, zero));
- TS_ASSERT(storeAll.isConst());
-
- Expr arr = d_em->mkExpr(STORE, storeAll, zero, zero);
- TS_ASSERT(!arr.isConst());
- arr = d_em->mkExpr(STORE, storeAll, zero, one);
- TS_ASSERT(arr.isConst());
- Expr arr2 = d_em->mkExpr(STORE, arr, one, zero);
- TS_ASSERT(!arr2.isConst());
- arr2 = d_em->mkExpr(STORE, arr, one, one);
- TS_ASSERT(arr2.isConst());
- arr2 = d_em->mkExpr(STORE, arr, zero, one);
- TS_ASSERT(!arr2.isConst());
-
- arrType = d_em->mkArrayType(d_em->mkBitVectorType(1), d_em->mkBitVectorType(1));
- zero = d_em->mkConst(BitVector(1,unsigned(0)));
- one = d_em->mkConst(BitVector(1,unsigned(1)));
- storeAll = d_em->mkConst(ArrayStoreAll(arrType, zero));
- TS_ASSERT(storeAll.isConst());
-
- arr = d_em->mkExpr(STORE, storeAll, zero, zero);
- TS_ASSERT(!arr.isConst());
- arr = d_em->mkExpr(STORE, storeAll, zero, one);
- TS_ASSERT(arr.isConst());
- arr2 = d_em->mkExpr(STORE, arr, one, zero);
- TS_ASSERT(!arr2.isConst());
- arr2 = d_em->mkExpr(STORE, arr, one, one);
- TS_ASSERT(!arr2.isConst());
- arr2 = d_em->mkExpr(STORE, arr, zero, one);
- TS_ASSERT(!arr2.isConst());
-
+ {
+ ExprManagerScope ems(*d_em);
+ ArrayType arrType =
+ d_em->mkArrayType(d_em->integerType(), d_em->integerType());
+ Expr zero = d_em->mkConst(Rational(0));
+ Expr one = d_em->mkConst(Rational(1));
+ Expr storeAll = d_em->mkConst(
+ ArrayStoreAll(TypeNode::fromType(arrType), Node::fromExpr(zero)));
+ TS_ASSERT(storeAll.isConst());
+
+ Expr arr = d_em->mkExpr(STORE, storeAll, zero, zero);
+ TS_ASSERT(!arr.isConst());
+ arr = d_em->mkExpr(STORE, storeAll, zero, one);
+ TS_ASSERT(arr.isConst());
+ Expr arr2 = d_em->mkExpr(STORE, arr, one, zero);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = d_em->mkExpr(STORE, arr, one, one);
+ TS_ASSERT(arr2.isConst());
+ arr2 = d_em->mkExpr(STORE, arr, zero, one);
+ TS_ASSERT(!arr2.isConst());
+
+ arrType =
+ d_em->mkArrayType(d_em->mkBitVectorType(1), d_em->mkBitVectorType(1));
+ zero = d_em->mkConst(BitVector(1, unsigned(0)));
+ one = d_em->mkConst(BitVector(1, unsigned(1)));
+ storeAll = d_em->mkConst(
+ ArrayStoreAll(TypeNode::fromType(arrType), Node::fromExpr(zero)));
+ TS_ASSERT(storeAll.isConst());
+
+ arr = d_em->mkExpr(STORE, storeAll, zero, zero);
+ TS_ASSERT(!arr.isConst());
+ arr = d_em->mkExpr(STORE, storeAll, zero, one);
+ TS_ASSERT(arr.isConst());
+ arr2 = d_em->mkExpr(STORE, arr, one, zero);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = d_em->mkExpr(STORE, arr, one, one);
+ TS_ASSERT(!arr2.isConst());
+ arr2 = d_em->mkExpr(STORE, arr, zero, one);
+ TS_ASSERT(!arr2.isConst());
+ }
}
void testGetConst() {
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 45d13d416..b1b79ec07 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -62,7 +62,7 @@ class TheoryBlack : public CxxTest::TestSuite {
TypeNode arrType = d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType());
Node zero = d_nm->mkConst(Rational(0));
Node one = d_nm->mkConst(Rational(1));
- Node storeAll = d_nm->mkConst(ArrayStoreAll(arrType.toType(), zero.toExpr()));
+ Node storeAll = d_nm->mkConst(ArrayStoreAll(arrType, zero));
TS_ASSERT(storeAll.isConst());
Node arr = d_nm->mkNode(STORE, storeAll, zero, zero);
@@ -85,7 +85,7 @@ class TheoryBlack : public CxxTest::TestSuite {
arrType = d_nm->mkArrayType(d_nm->mkBitVectorType(1), d_nm->mkBitVectorType(1));
zero = d_nm->mkConst(BitVector(1,unsigned(0)));
one = d_nm->mkConst(BitVector(1,unsigned(1)));
- storeAll = d_nm->mkConst(ArrayStoreAll(arrType.toType(), zero.toExpr()));
+ storeAll = d_nm->mkConst(ArrayStoreAll(arrType, zero));
TS_ASSERT(storeAll.isConst());
arr = d_nm->mkNode(STORE, storeAll, zero, zero);
@@ -113,7 +113,7 @@ class TheoryBlack : public CxxTest::TestSuite {
one = d_nm->mkConst(BitVector(2,unsigned(1)));
Node two = d_nm->mkConst(BitVector(2,unsigned(2)));
Node three = d_nm->mkConst(BitVector(2,unsigned(3)));
- storeAll = d_nm->mkConst(ArrayStoreAll(arrType.toType(), one.toExpr()));
+ storeAll = d_nm->mkConst(ArrayStoreAll(arrType, one));
TS_ASSERT(storeAll.isConst());
arr = d_nm->mkNode(STORE, storeAll, zero, zero);
diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h
index f8ce734ec..b996919ee 100644
--- a/test/unit/theory/type_enumerator_white.h
+++ b/test/unit/theory/type_enumerator_white.h
@@ -234,13 +234,20 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite {
TS_ASSERT( ! te.isFinished() );
// ensure that certain items were found
- ArrayType arrayType(d_em->mkArrayType(d_em->integerType(), d_em->integerType()));
- Node zeroes = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(0))));
- Node ones = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(1))));
- Node twos = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(2))));
- Node threes = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(3))));
- Node fours = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(4))));
- Node tens = d_nm->mkConst(ArrayStoreAll(arrayType, d_em->mkConst(Rational(10))));
+ TypeNode arrayType =
+ d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType());
+ Node zeroes =
+ d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(0))));
+ Node ones =
+ d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(1))));
+ Node twos =
+ d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(2))));
+ Node threes =
+ d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(3))));
+ Node fours =
+ d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(4))));
+ Node tens =
+ d_nm->mkConst(ArrayStoreAll(arrayType, d_nm->mkConst(Rational(10))));
Node zero = d_nm->mkConst(Rational(0));
Node one = d_nm->mkConst(Rational(1));
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index 0748e1059..5bccc9137 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -1,7 +1,7 @@
#-----------------------------------------------------------------------------#
# Add unit tests
-cvc4_add_unit_test_black(array_store_all_black util)
+cvc4_add_unit_test_white(array_store_all_white util)
cvc4_add_unit_test_white(assert_white util)
cvc4_add_unit_test_black(binary_heap_black util)
cvc4_add_unit_test_black(bitvector_black util)
diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h
deleted file mode 100644
index bf0163317..000000000
--- a/test/unit/util/array_store_all_black.h
+++ /dev/null
@@ -1,83 +0,0 @@
-/********************* */
-/*! \file array_store_all_black.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Tim King, Morgan Deters, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4::ArrayStoreAll
- **
- ** Black box testing of CVC4::ArrayStoreAll.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "api/cvc4cpp.h"
-#include "expr/array_store_all.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
-#include "expr/expr_manager_scope.h"
-#include "expr/type.h"
-#include "test_utils.h"
-
-using namespace CVC4;
-using namespace std;
-
-class ArrayStoreAllBlack : public CxxTest::TestSuite {
- public:
- void setUp() override
- {
- d_slv = new api::Solver();
- d_em = d_slv->getExprManager();
- }
-
- void tearDown() override { delete d_slv; }
-
- void testStoreAll() {
- Type usort = d_em->mkSort("U");
- ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->realType()),
- d_em->mkConst(Rational(9, 2)));
- ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort),
- d_em->mkConst(UninterpretedConstant(usort, 0)));
- ArrayStoreAll(d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->realType()),
- d_em->mkConst(Rational(0)));
- ArrayStoreAll(
- d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->integerType()),
- d_em->mkConst(Rational(0)));
- }
-
- void testTypeErrors()
- {
- TS_ASSERT_THROWS(ArrayStoreAll(d_em->integerType(),
- d_em->mkConst(UninterpretedConstant(
- d_em->mkSort("U"), 0))),
- IllegalArgumentException&);
- TS_ASSERT_THROWS(
- ArrayStoreAll(d_em->integerType(), d_em->mkConst(Rational(9, 2))),
- IllegalArgumentException&);
- TS_ASSERT_THROWS(
- ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->mkSort("U")),
- d_em->mkConst(Rational(9, 2))),
- IllegalArgumentException&);
- }
-
- void testConstError() {
- Type usort = d_em->mkSort("U");
- TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll(
- d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkVar(usort)));
- TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll(
- d_em->integerType(), d_em->mkVar("x", d_em->integerType())));
- TS_ASSERT_THROWS_ANYTHING(
- ArrayStoreAll(d_em->integerType(),
- d_em->mkExpr(kind::PLUS, d_em->mkConst(Rational(1)),
- d_em->mkConst(Rational(0)))));
- }
-
- private:
- api::Solver* d_slv;
- ExprManager* d_em;
-}; /* class ArrayStoreAllBlack */
diff --git a/test/unit/util/array_store_all_white.h b/test/unit/util/array_store_all_white.h
new file mode 100644
index 000000000..fb7857003
--- /dev/null
+++ b/test/unit/util/array_store_all_white.h
@@ -0,0 +1,94 @@
+/********************* */
+/*! \file array_store_all_white.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Tim King, Morgan Deters, Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::ArrayStoreAll
+ **
+ ** Black box testing of CVC4::ArrayStoreAll.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "api/cvc4cpp.h"
+#include "expr/array_store_all.h"
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
+#include "expr/type.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "test_utils.h"
+
+using namespace CVC4;
+using namespace std;
+
+class ArrayStoreAllWhite : public CxxTest::TestSuite
+{
+ public:
+ void setUp() override
+ {
+ d_slv = new api::Solver();
+ d_scope = new smt::SmtScope(d_slv->getSmtEngine());
+ d_nm = d_slv->getSmtEngine()->d_nodeManager;
+ }
+
+ void tearDown() override
+ {
+ delete d_scope;
+ delete d_slv;
+ }
+
+ void testStoreAll()
+ {
+ TypeNode usort = d_nm->mkSort("U");
+ ArrayStoreAll(d_nm->mkArrayType(d_nm->integerType(), d_nm->realType()),
+ d_nm->mkConst(Rational(9, 2)));
+ ArrayStoreAll(d_nm->mkArrayType(d_nm->mkSort("U"), usort),
+ d_nm->mkConst(UninterpretedConstant(usort.toType(), 0)));
+ ArrayStoreAll(d_nm->mkArrayType(d_nm->mkBitVectorType(8), d_nm->realType()),
+ d_nm->mkConst(Rational(0)));
+ ArrayStoreAll(
+ d_nm->mkArrayType(d_nm->mkBitVectorType(8), d_nm->integerType()),
+ d_nm->mkConst(Rational(0)));
+ }
+
+ void testTypeErrors()
+ {
+ TS_ASSERT_THROWS(ArrayStoreAll(d_nm->integerType(),
+ d_nm->mkConst(UninterpretedConstant(
+ d_nm->mkSort("U").toType(), 0))),
+ IllegalArgumentException&);
+ TS_ASSERT_THROWS(
+ ArrayStoreAll(d_nm->integerType(), d_nm->mkConst(Rational(9, 2))),
+ IllegalArgumentException&);
+ TS_ASSERT_THROWS(
+ ArrayStoreAll(d_nm->mkArrayType(d_nm->integerType(), d_nm->mkSort("U")),
+ d_nm->mkConst(Rational(9, 2))),
+ IllegalArgumentException&);
+ }
+
+ void testConstError()
+ {
+ TypeNode usort = d_nm->mkSort("U");
+ TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll(
+ d_nm->mkArrayType(d_nm->mkSort("U"), usort), d_nm->mkVar(usort)));
+ TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll(
+ d_nm->integerType(), d_nm->mkVar("x", d_nm->integerType())));
+ TS_ASSERT_THROWS_ANYTHING(
+ ArrayStoreAll(d_nm->integerType(),
+ d_nm->mkNode(kind::PLUS,
+ d_nm->mkConst(Rational(1)),
+ d_nm->mkConst(Rational(0)))));
+ }
+
+ private:
+ api::Solver* d_slv;
+ smt::SmtScope* d_scope;
+ NodeManager* d_nm;
+}; /* class ArrayStoreAllBlack */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback