diff options
Diffstat (limited to 'test/system/cvc3_main.cpp')
-rw-r--r-- | test/system/cvc3_main.cpp | 30 |
1 files changed, 16 insertions, 14 deletions
diff --git a/test/system/cvc3_main.cpp b/test/system/cvc3_main.cpp index cee56757e..ff7448ded 100644 --- a/test/system/cvc3_main.cpp +++ b/test/system/cvc3_main.cpp @@ -1236,7 +1236,7 @@ void test15() { /***************************************************** * array declaration * *****************************************************/ - +/* // array: index type Type index_type = vc->subrangeType(vc->ratExpr(0), vc->ratExpr(3)); @@ -1252,13 +1252,13 @@ void test15() { arr = vc->writeExpr(arr, vc->ratExpr(1), vc->ratExpr(1)); arr = vc->writeExpr(arr, vc->ratExpr(2), vc->ratExpr(0)); arr = vc->writeExpr(arr, vc->ratExpr(3), vc->ratExpr(0)); - +*/ /***************************************************** * forall Expr * *****************************************************/ - +/* // for loop: index Expr id = vc->boundVarExpr("id", "0", vc->subrangeType(vc->ratExpr(0), vc->ratExpr(2))); @@ -1283,11 +1283,11 @@ void test15() { } cout << "End of counter-example" << endl << endl; vc->pop(); - + */ /***************************************************** * manual expansion * *****************************************************/ - +/* Expr e1 = vc->leExpr(vc->readExpr(arr, vc->ratExpr(0)), vc->readExpr(arr, vc->ratExpr(1))); Expr e2 = vc->leExpr(vc->readExpr(arr, vc->ratExpr(1)), @@ -1295,13 +1295,13 @@ void test15() { Expr e3 = vc->leExpr(vc->readExpr(arr, vc->ratExpr(2)), vc->readExpr(arr, vc->ratExpr(3))); Expr manual_expr = vc->andExpr(e1, vc->andExpr(e2, e3)); - +*/ /***************************************************** * exists Expr * *****************************************************/ - +/* // exists: index Expr id_ex = vc->varExpr("id_ex", vc->subrangeType(vc->ratExpr(0), vc->ratExpr(2))); @@ -1313,14 +1313,14 @@ void test15() { vc->readExpr(arr, vc->plusExpr(id_ex, vc->ratExpr(1)))); // exists expr Expr ex_expr = vc->existsExpr(vars_ex, ex_body); - +*/ /***************************************************** * ??? forall <==> manual expansion * *****************************************************/ - + /* cout << endl << "Checking forallExpr <==> manual expansion ..." << endl; if (vc->query(vc->iffExpr(forall_expr, manual_expr))) cout << " -- yes." << endl; @@ -1334,12 +1334,13 @@ void test15() { } cout << endl; - +*/ /***************************************************** * ??? !forall <==> existsExpr * *****************************************************/ + /* cout << endl << "Checking !forallExpr <==> existsExpr ..." << endl; if (vc->query(vc->iffExpr(vc->notExpr(forall_expr), ex_expr))) cout << " -- yes." << endl; @@ -1360,7 +1361,7 @@ void test15() { } cout << endl << "End of testcases." << endl << endl; - +*/ } catch(const Exception& e) { exitStatus = 1; @@ -1373,6 +1374,7 @@ void test15() { void test16() { ValidityChecker *vc = ValidityChecker::create(); try { + /* Type zto100 = vc->subrangeType(vc->ratExpr(0), vc->ratExpr(100)); Expr mem = vc->varExpr("mem", vc->arrayType(zto100, vc->intType())); Expr a = vc->varExpr("a", zto100); @@ -1418,7 +1420,7 @@ void test16() { //cout << Expr(ASSERT, eq) << "\n"; } } - +*/ } catch(const Exception& e) { exitStatus = 1; cout << "*** Exception caught in test16(): \n" << e << endl; @@ -1794,8 +1796,8 @@ void test20() { constructors[2].push_back("cons"); selectors[2][0].push_back("s0"); types[2][0].push_back(vc->bitvecType(2).getExpr()); - selectors[2][0].push_back("s1"); - types[2][0].push_back(vc->arrayType(vc->intType(), vc->subrangeType(vc->ratExpr(0), vc->ratExpr(0))).getExpr()); + //selectors[2][0].push_back("s1"); + //types[2][0].push_back(vc->arrayType(vc->intType(), vc->subrangeType(vc->ratExpr(0), vc->ratExpr(0))).getExpr()); vc->dataType(names, constructors, selectors, types, returnTypes); |