/********************* */
/*! \file type_enumerator_white.h
** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ ** Morgan Deters, Andres Noetzli, Clark Barrett
+ ** 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 White box testing of CVC4::theory::TypeEnumerator
**
#include <cxxtest/TestSuite.h>
-#include "expr/node_manager.h"
+#include <unordered_set>
+
+#include "expr/array_store_all.h"
+#include "expr/dtype.h"
#include "expr/expr_manager.h"
-#include "expr/type_node.h"
#include "expr/kind.h"
+#include "expr/node_manager.h"
+#include "expr/type_node.h"
+#include "options/language.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "theory/type_enumerator.h"
-#include "util/language.h"
-#include "util/array_store_all.h"
using namespace CVC4;
+using namespace CVC4::smt;
using namespace CVC4::theory;
using namespace CVC4::kind;
using namespace std;
class TypeEnumeratorWhite : public CxxTest::TestSuite {
- ExprManager* d_em;
- NodeManager* d_nm;
- NodeManagerScope* d_scope;
-
-public:
-
- void setUp() {
+ public:
+ void setUp() override
+ {
d_em = new ExprManager();
+ d_smt = new SmtEngine(d_em);
d_nm = NodeManager::fromExprManager(d_em);
- d_scope = new NodeManagerScope(d_nm);
+ d_scope = new SmtScope(d_smt);
+ d_smt->finishInit();
}
- void tearDown() {
+ void tearDown() override
+ {
delete d_scope;
+ delete d_smt;
delete d_em;
}
TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(true));
TS_ASSERT( ! te.isFinished() );
- TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
TS_ASSERT( te.isFinished() );
- TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
TS_ASSERT( te.isFinished() );
- TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
TS_ASSERT( te.isFinished() );
}
void testUF() {
- TypeNode sortn = d_nm->mkSort("T");
- Type sort = sortn.toType();
- TypeNode sortn2 = d_nm->mkSort("U");
- Type sort2 = sortn2.toType();
- TypeEnumerator te(sortn);
+ TypeNode sort = d_nm->mkSort("T");
+ TypeNode sort2 = d_nm->mkSort("U");
+ TypeEnumerator te(sort);
TS_ASSERT_EQUALS(*te, d_nm->mkConst(UninterpretedConstant(sort, 0)));
for(size_t i = 1; i < 100; ++i) {
TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort, i)));
TS_ASSERT( ! te.isFinished() );
}
- void testDatatypesFinite() {
- Datatype dt("Colors");
- dt.addConstructor(DatatypeConstructor("red"));
- dt.addConstructor(DatatypeConstructor("orange"));
- dt.addConstructor(DatatypeConstructor("yellow"));
- dt.addConstructor(DatatypeConstructor("green"));
- dt.addConstructor(DatatypeConstructor("blue"));
- dt.addConstructor(DatatypeConstructor("violet"));
- TypeNode datatype = TypeNode::fromType(d_em->mkDatatypeType(dt));
+ void testDTypesFinite()
+ {
+ DType dt("Colors");
+ dt.addConstructor(std::make_shared<DTypeConstructor>("red"));
+ dt.addConstructor(std::make_shared<DTypeConstructor>("orange"));
+ dt.addConstructor(std::make_shared<DTypeConstructor>("yellow"));
+ dt.addConstructor(std::make_shared<DTypeConstructor>("green"));
+ dt.addConstructor(std::make_shared<DTypeConstructor>("blue"));
+ dt.addConstructor(std::make_shared<DTypeConstructor>("violet"));
+ TypeNode datatype = d_nm->mkDatatypeType(dt);
+ const std::vector<std::shared_ptr<DTypeConstructor> >& dtcons =
+ datatype.getDType().getConstructors();
TypeEnumerator te(datatype);
- TS_ASSERT_EQUALS(*te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("red")));
- TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("orange")));
- TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("yellow")));
- TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("green")));
- TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("blue")));
- TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("violet")));
- TS_ASSERT_THROWS(*++te, NoMoreValuesException);
- TS_ASSERT_THROWS(*++te, NoMoreValuesException);
- TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT_EQUALS(
+ *te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor()));
+ TS_ASSERT_EQUALS(
+ *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor()));
+ TS_ASSERT_EQUALS(
+ *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor()));
+ TS_ASSERT_EQUALS(
+ *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[3]->getConstructor()));
+ TS_ASSERT_EQUALS(
+ *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[4]->getConstructor()));
+ TS_ASSERT_EQUALS(
+ *++te, d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[5]->getConstructor()));
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
}
- void testDatatypesInfinite1() {
- Datatype colors("Colors");
- colors.addConstructor(DatatypeConstructor("red"));
- colors.addConstructor(DatatypeConstructor("orange"));
- colors.addConstructor(DatatypeConstructor("yellow"));
- colors.addConstructor(DatatypeConstructor("green"));
- colors.addConstructor(DatatypeConstructor("blue"));
- colors.addConstructor(DatatypeConstructor("violet"));
- TypeNode colorsType = TypeNode::fromType(d_em->mkDatatypeType(colors));
- Datatype listColors("ListColors");
- DatatypeConstructor consC("cons");
- consC.addArg("car", colorsType.toType());
- consC.addArg("cdr", DatatypeSelfType());
+ void testDTypesInfinite1()
+ {
+ DType colors("Colors");
+ colors.addConstructor(std::make_shared<DTypeConstructor>("red"));
+ colors.addConstructor(std::make_shared<DTypeConstructor>("orange"));
+ colors.addConstructor(std::make_shared<DTypeConstructor>("yellow"));
+ colors.addConstructor(std::make_shared<DTypeConstructor>("green"));
+ colors.addConstructor(std::make_shared<DTypeConstructor>("blue"));
+ colors.addConstructor(std::make_shared<DTypeConstructor>("violet"));
+ TypeNode colorsType = d_nm->mkDatatypeType(colors);
+ const std::vector<std::shared_ptr<DTypeConstructor> >& ctCons =
+ colorsType.getDType().getConstructors();
+ DType listColors("ListColors");
+ std::shared_ptr<DTypeConstructor> consC =
+ std::make_shared<DTypeConstructor>("cons");
+ consC->addArg("car", colorsType);
+ consC->addArgSelf("cdr");
listColors.addConstructor(consC);
- listColors.addConstructor(DatatypeConstructor("nil"));
- TypeNode listColorsType = TypeNode::fromType(d_em->mkDatatypeType(listColors));
+ listColors.addConstructor(std::make_shared<DTypeConstructor>("nil"));
+ TypeNode listColorsType = d_nm->mkDatatypeType(listColors);
+ const std::vector<std::shared_ptr<DTypeConstructor> >& lctCons =
+ listColorsType.getDType().getConstructors();
TypeEnumerator te(listColorsType);
TS_ASSERT( ! te.isFinished() );
- Node cons = Node::fromExpr(DatatypeType(listColorsType.toType()).getDatatype().getConstructor("cons"));
- Node nil = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(listColorsType.toType()).getDatatype().getConstructor("nil"));
- Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("red"));
+ Node cons = lctCons[0]->getConstructor();
+ Node nil = d_nm->mkNode(APPLY_CONSTRUCTOR, lctCons[1]->getConstructor());
+ Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, ctCons[0]->getConstructor());
+ Node orange = d_nm->mkNode(APPLY_CONSTRUCTOR, ctCons[1]->getConstructor());
+ Node yellow = d_nm->mkNode(APPLY_CONSTRUCTOR, ctCons[2]->getConstructor());
TS_ASSERT_EQUALS(*te, nil);
TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil));
TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)));
TS_ASSERT( ! te.isFinished() );
+ TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil));
+ TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))));
TS_ASSERT( ! te.isFinished() );
- TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange,
+ d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)));
TS_ASSERT( ! te.isFinished() );
- TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))))));
+ TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, yellow, nil));
TS_ASSERT( ! te.isFinished() );
TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))))));
- TS_ASSERT( ! te.isFinished() );
- TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
- d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))))))));
+ d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil)));
TS_ASSERT( ! te.isFinished() );
}
- void NOTYETtestDatatypesInfinite2() {
+ void NOTYETtestDTypesInfinite2()
+ {
//TypeNode datatype;
//TypeEnumerator te(datatype);
//TS_ASSERT( ! te.isFinished() );
void testArraysInfinite() {
TypeEnumerator te(d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType()));
- hash_set<Node, NodeHashFunction> elts;
+ unordered_set<Node, NodeHashFunction> elts;
for(size_t i = 0; i < 1000; ++i) {
TS_ASSERT( ! te.isFinished() );
Node elt = *te++;
- std::cout << elt << std::endl;
// ensure no duplicates
TS_ASSERT( elts.find(elt) == elts.end() );
elts.insert(elt);
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));
//TS_ASSERT( elts.find( d_nm->mkNode(STORE, d_nm->mkNode(STORE, d_nm->mkNode(STORE, d_nm->mkNode(STORE, twos, three, zero), two, zero), one, zero), zero, zero) ) != elts.end() );
}
- void testArraysFinite() {
- ArrayType arrType(d_em->mkArrayType(d_em->mkBitVectorType(2), d_em->booleanType()));
- TypeEnumerator te(TypeNode::fromType(arrType));
- TS_ASSERT( ! te.isFinished() );
- TS_ASSERT_EQUALS(*te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(false))));
- TS_ASSERT( ! te.isFinished() );
- TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(true))));
- TS_ASSERT( ! te.isFinished() );
- TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(false))));
- TS_ASSERT( ! te.isFinished() );
- TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(true))));
- TS_ASSERT( ! te.isFinished() );
- TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(false))));
- TS_ASSERT( ! te.isFinished() );
- TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(true))));
- TS_ASSERT( ! te.isFinished() );
- TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(false))));
- TS_ASSERT( ! te.isFinished() );
- TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayStoreAll(arrType, d_em->mkConst(true))));
- TS_ASSERT( ! te.isFinished() );
- TS_ASSERT_THROWS(*++te, NoMoreValuesException);
- TS_ASSERT( te.isFinished() );
- TS_ASSERT_THROWS(*++te, NoMoreValuesException);
- TS_ASSERT( te.isFinished() );
- TS_ASSERT_THROWS(*++te, NoMoreValuesException);
- TS_ASSERT( te.isFinished() );
- }
-
void testBV() {
TypeEnumerator te(d_nm->mkBitVectorType(3));
TS_ASSERT_EQUALS(*te, d_nm->mkConst(BitVector(3u, 0u)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 5u)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 6u)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 7u)));
- TS_ASSERT_THROWS(*++te, NoMoreValuesException);
- TS_ASSERT_THROWS(*++te, NoMoreValuesException);
- TS_ASSERT_THROWS(*++te, NoMoreValuesException);
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
+ TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
}
+ private:
+ ExprManager* d_em;
+ SmtEngine* d_smt;
+ NodeManager* d_nm;
+ SmtScope* d_scope;
};/* class TypeEnumeratorWhite */
projects / cvc5.git / blobdiff