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
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);
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;
}
#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
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
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
}
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
#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;
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,
// 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()) {
* 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.
namespace CVC4 {
-inline Type TypeNode::toType() {
+inline Type TypeNode::toType() const
+{
return NodeManager::currentNM()->toType(*this);
}
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;
}
case kind::STORE_ALL: {
ArrayStoreAll asa = n.getConst<ArrayStoreAll>();
- out << "((as const " << asa.getType() << ") " << asa.getExpr() << ")";
+ out << "((as const " << asa.getType() << ") " << asa.getValue() << ")";
break;
}
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");
}
}
// 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 {
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);
}
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
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())) {
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);
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);
else {
Assert(n.getKind() == kind::STORE_ALL);
ArrayStoreAll storeAll = n.getConst<ArrayStoreAll>();
- ArrayType arrayType = storeAll.getType();
- return TypeNode::fromType(arrayType);
+ return storeAll.getType();
}
}
}
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;
}
{
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;
}
}
}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 );
}
}
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;
#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;
delete c_bool_and;
delete b_bool;
delete a_bool;
-
delete d_slv;
}
catch (Exception& e)
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() {
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);
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);
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);
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));
#-----------------------------------------------------------------------------#
# 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)
+++ /dev/null
-/********************* */
-/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
projects / cvc5.git / commitdiff