diff options
Diffstat (limited to 'test/unit/expr/node_black.h')
| -rw-r--r-- | test/unit/expr/node_black.h | 78 |
1 files changed, 77 insertions, 1 deletions
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 91242322a..182f742b0 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -23,13 +23,15 @@ #include <vector> #include "api/cvc4cpp.h" -#include "smt/smt_engine.h" +#include "expr/dtype.h" #include "expr/expr_manager.h" #include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_manager.h" #include "expr/node_value.h" +#include "smt/smt_engine.h" #include "test_utils.h" +#include "theory/rewriter.h" using namespace CVC4; using namespace CVC4::kind; @@ -706,6 +708,80 @@ class NodeBlack : public CxxTest::TestSuite { std::equal(children.begin(), children.end(), skolems.begin())); } + void testIsConst() + { + // more complicated "constants" exist in datatypes and arrays theories + DType list("list"); + std::shared_ptr<DTypeConstructor> consC = + std::make_shared<DTypeConstructor>("cons"); + consC->addArg("car", d_nodeManager->integerType()); + consC->addArgSelf("cdr"); + list.addConstructor(consC); + list.addConstructor(std::make_shared<DTypeConstructor>("nil")); + TypeNode listType = d_nodeManager->mkDatatypeType(list); + const std::vector<std::shared_ptr<DTypeConstructor> >& lcons = + listType.getDType().getConstructors(); + Node cons = lcons[0]->getConstructor(); + Node nil = lcons[1]->getConstructor(); + Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType()); + Node cons_x_nil = + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, + cons, + x, + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)); + Node cons_1_nil = + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, + cons, + d_nodeManager->mkConst(Rational(1)), + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)); + Node cons_1_cons_2_nil = d_nodeManager->mkNode( + APPLY_CONSTRUCTOR, + cons, + d_nodeManager->mkConst(Rational(1)), + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, + cons, + d_nodeManager->mkConst(Rational(2)), + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil))); + TS_ASSERT(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst()); + TS_ASSERT(!cons_x_nil.isConst()); + TS_ASSERT(cons_1_nil.isConst()); + TS_ASSERT(cons_1_cons_2_nil.isConst()); + + TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), + d_nodeManager->integerType()); + Node zero = d_nodeManager->mkConst(Rational(0)); + Node one = d_nodeManager->mkConst(Rational(1)); + Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); + TS_ASSERT(storeAll.isConst()); + + Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); + TS_ASSERT(!arr.isConst()); + arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); + TS_ASSERT(arr.isConst()); + Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); + TS_ASSERT(!arr2.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); + TS_ASSERT(!arr2.isConst()); + + arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1), + d_nodeManager->mkBitVectorType(1)); + zero = d_nodeManager->mkConst(BitVector(1, unsigned(0))); + one = d_nodeManager->mkConst(BitVector(1, unsigned(1))); + storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); + TS_ASSERT(storeAll.isConst()); + + arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); + TS_ASSERT(!arr.isConst()); + arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); + TS_ASSERT(arr.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); + TS_ASSERT(!arr2.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, one, one); + TS_ASSERT(!arr2.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); + TS_ASSERT(!arr2.isConst()); + } + // This Test is designed to fail in a way that will cause a segfault, // so it is commented out. // This is for demonstrating what a certain type of user error looks like. |