diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-28 01:10:16 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-28 01:10:16 +0000 |
commit | cf287f593931a1c4fc141e18845b4c5d36879889 (patch) | |
tree | 4dad0f555b7db01fbeedcd9eace394cd8f7a0fb4 /test | |
parent | b7b1c1d99ffa333704af2c8ecd60b1af8833a28b (diff) |
Improved compatibility layer, now supports quantifiers. Also incorporates
numerous bugfixes, and the cvc3 system test is enabled.
Diffstat (limited to 'test')
-rw-r--r-- | test/system/Makefile.am | 21 | ||||
-rw-r--r-- | test/system/cvc3_main.cpp | 281 |
2 files changed, 173 insertions, 129 deletions
diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 5fcc8833a..836189991 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -5,7 +5,11 @@ CPLUSPLUS_TESTS = \ ouroborous \ two_smt_engines \ smt2_compliance -# cvc3_main + +if CVC4_BUILD_LIBCOMPAT +CPLUSPLUS_TESTS += \ + cvc3_main +endif TESTS = $(CPLUSPLUS_TESTS) @@ -32,9 +36,13 @@ TEST_DEPS_DIST = \ # changes made in the header files. TEST_DEPS_NODIST = \ $(abs_top_builddir)/src/libcvc4.la \ - $(abs_top_builddir)/src/parser/libcvc4parser.la \ + $(abs_top_builddir)/src/parser/libcvc4parser.la + +if CVC4_BUILD_LIBCOMPAT +TEST_DEPS_NODIST += \ $(abs_top_builddir)/src/compat/libcvc4compat.la \ cvc3_george.lo +endif TEST_DEPS = \ $(TEST_DEPS_DIST) \ @@ -63,8 +71,13 @@ AM_CPPFLAGS = \ -D __STDC_FORMAT_MACROS \ -D __BUILDING_CVC4_SYSTEM_TEST \ $(TEST_CPPFLAGS) -LIBADD = \ - @abs_top_builddir@/src/compat/libcvc4compat.la \ + +LIBADD = +if CVC4_BUILD_LIBCOMPAT +LIBADD += \ + @abs_top_builddir@/src/compat/libcvc4compat.la +endif +LIBADD += \ @abs_top_builddir@/src/parser/libcvc4parser.la \ @abs_top_builddir@/src/libcvc4.la diff --git a/test/system/cvc3_main.cpp b/test/system/cvc3_main.cpp index 76ff9e974..a428f605d 100644 --- a/test/system/cvc3_main.cpp +++ b/test/system/cvc3_main.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -47,12 +47,25 @@ using namespace std; using namespace CVC3; - int exitStatus; +inline void __expect__(const std::string& file, + int line, + bool cond, + const std::string& cond_s, + const std::string& msg) { + if(!cond) { + std::cerr << file << ":" << line + << ": Expected: (" << cond_s << "). " + << msg << std::endl; + exitStatus = 1; + } +} + +#define EXPECT(cond, msg) __expect__(__FILE__, __LINE__, (cond), #cond, (msg)) // Check whether e is valid -bool check(ValidityChecker* vc, Expr e, bool verbose=false) +bool check(ValidityChecker* vc, Expr e, bool verbose=true) { if(verbose) { cout << "Query: "; @@ -124,7 +137,7 @@ void test () Expr f2 = vc->funExpr(f, e); Expr f3 = vc->funExpr(f, f2); - FatalAssert(e != f2 && e != f3, "Refcount problems"); + EXPECT(e != f2 && e != f3, "Refcount problems"); Expr x (vc->boundVarExpr ("x", "0", it));//x0:int vector<Expr> xs; @@ -159,12 +172,12 @@ void test1() // even in those exceptional cases. try { - IF_DEBUG(bool b =) check(vc, vc->trueExpr()); - FatalAssert(b, "Should be valid"); + bool b = check(vc, vc->trueExpr()); + EXPECT(b, "Should be valid"); vc->push(); - IF_DEBUG(b =) check(vc, vc->falseExpr()); - FatalAssert(!b, "Should be invalid"); + b = check(vc, vc->falseExpr()); + EXPECT(!b, "Should be invalid"); vc->pop(); // Check p OR ~p @@ -172,8 +185,8 @@ void test1() Expr p = vc->varExpr("p", vc->boolType()); Expr e = vc->orExpr(p, vc->notExpr(p)); - IF_DEBUG(b =) check(vc, e); - FatalAssert(b, "Should be valid"); + b = check(vc, e); + EXPECT(b, "Should be valid"); // Check x = y -> f(x) = f(y) @@ -186,16 +199,16 @@ void test1() Expr fy = vc->funExpr(f, y); e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(fx, fy)); - IF_DEBUG(b =) check(vc, e); - FatalAssert(b, "Should be valid"); + b = check(vc, e); + EXPECT(b, "Should be valid"); // Check f(x) = f(y) -> x = y e = vc->impliesExpr(vc->eqExpr(fx,fy),vc->eqExpr(x, y)); - IF_DEBUG(int scopeLevel = vc->scopeLevel();) + int scopeLevel = vc->scopeLevel(); vc->push(); - IF_DEBUG(b =) check(vc, e); - FatalAssert(!b, "Should be invalid"); + b = check(vc, e); + EXPECT(!b, "Should be invalid"); // Get counter-example @@ -211,7 +224,7 @@ void test1() // Reset to initial scope cout << "Resetting" << endl; vc->pop(); - FatalAssert(scopeLevel == vc->scopeLevel(), "scope error"); + EXPECT(scopeLevel == vc->scopeLevel(), "scope error"); cout << "Scope level: " << vc->scopeLevel() << endl << endl; // Check w = x & x = y & y = z & f(x) = f(y) & x = 1 & z = 2 @@ -231,7 +244,7 @@ void test1() cout << endl << "simplify(w) = "; vc->printExpr(vc->simplify(w)); cout << endl; - FatalAssert(vc->simplify(w)==vc->ratExpr(1), "Expected simplify(w) = 1"); + EXPECT(vc->simplify(w)==vc->ratExpr(1), "Expected simplify(w) = 1"); newAssertion(vc, vc->eqExpr(z, vc->ratExpr(2))); assertions.clear(); @@ -247,7 +260,7 @@ void test1() cout << "simplify(w) = "; vc->printExpr(vc->simplify(w)); - FatalAssert(vc->simplify(w)==w, "Expected simplify(w) = w"); + EXPECT(vc->simplify(w)==w, "Expected simplify(w) = w"); cout << endl; assertions.clear(); @@ -274,11 +287,11 @@ void test2() Expr c = vc->varExpr("c", vc->intType()); vc->assertFormula(c.eqExpr(vc->ratExpr(0)) || c.eqExpr(vc->ratExpr(1))); - IF_DEBUG(bool b =) check(vc, vc->leExpr(bexpr, vc->ratExpr(10))); - FatalAssert(b, "Should be valid"); + bool b = check(vc, vc->leExpr(bexpr, vc->ratExpr(10))); + EXPECT(b, "Should be valid"); - IF_DEBUG(b =) check(vc, vc->falseExpr()); - FatalAssert(!b, "Should be invalid"); + b = check(vc, vc->falseExpr()); + EXPECT(!b, "Should be invalid"); vc->returnFromCheck(); // Check x = y -> g(x,y) = g(y,x) @@ -298,8 +311,8 @@ void test2() Expr gyx = vc->funExpr(g, y, x); Expr e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(gxy, gyx)); - IF_DEBUG(b =) check(vc, e); - FatalAssert(b, "Should be valid"); + b = check(vc, e); + EXPECT(b, "Should be valid"); Op h = vc->createOp("h", realxreal2real); @@ -307,8 +320,8 @@ void test2() Expr hyx = vc->funExpr(h, y, x); e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(hxy, hyx)); - IF_DEBUG(b =) check(vc, e); - FatalAssert(b, "Should be valid"); + b = check(vc, e); + EXPECT(b, "Should be valid"); } catch(const Exception& e) { exitStatus = 1; @@ -539,8 +552,7 @@ void test5() // hyp.push_back(vc->orExpr(vc->geExpr(qmp, N), vc->leExpr(qmp, zero))); // hyp.push_back(vc->orExpr(vc->geExpr(qmr, N), vc->leExpr(qmr, zero))); - //Expr test = vc->impliesExpr(vc->andExpr(hyp), e); - Expr test = vc->impliesExpr(hyp[0], e); + Expr test = vc->impliesExpr(vc->andExpr(hyp), e); Expr query; cout << "Checking verification condition:" << endl; @@ -800,11 +812,11 @@ void test8() { try { vector<Expr> vec; vec.push_back(vc->boundVarExpr("x", "x", vc->realType())); - Expr lambda = vc->lambdaExpr(vec, vc->falseExpr());//.getExpr(); + Expr lambda = vc->lambdaExpr(vec, vc->falseExpr()).getExpr(); Expr witness; try { Type t = vc->subtypeType(lambda, witness); - FatalAssert(false, "Typechecking exception expected"); + EXPECT(false, "Typechecking exception expected"); } catch(const TypecheckException&) { // fall through } @@ -1064,14 +1076,14 @@ void test11() cout << "Assert x = y" << endl; vc->assertFormula(xeqy); c = printImpliedLiterals(vc); - FatalAssert(c==3,"Implied literal error 0"); + EXPECT(c==3,"Implied literal error 0"); cout << "Push" << endl; vc->push(); cout << "Assert x /= z" << endl; vc->assertFormula(!xeqz); c = printImpliedLiterals(vc); - FatalAssert(c==4,"Implied literal error 1"); + EXPECT(c==4,"Implied literal error 1"); cout << "Pop" << endl; vc->pop(); @@ -1080,7 +1092,7 @@ void test11() cout << "Assert y /= z" << endl; vc->assertFormula(!yeqz); c = printImpliedLiterals(vc); - FatalAssert(c==4,"Implied literal error 2"); + EXPECT(c==4,"Implied literal error 2"); cout << "Pop" << endl; vc->pop(); @@ -1089,7 +1101,7 @@ void test11() cout << "Assert p(x)" << endl; vc->assertFormula(px); c = printImpliedLiterals(vc); - FatalAssert(c==2,"Implied literal error 3"); + EXPECT(c==2,"Implied literal error 3"); cout << "Pop" << endl; vc->pop(); @@ -1098,7 +1110,7 @@ void test11() cout << "Assert p(y)" << endl; vc->assertFormula(py); c = printImpliedLiterals(vc); - FatalAssert(c==2,"Implied literal error 4"); + EXPECT(c==2,"Implied literal error 4"); cout << "Pop" << endl; vc->pop(); @@ -1110,7 +1122,7 @@ void test11() cout << "Assert y = x" << endl; vc->assertFormula(yeqx); c = printImpliedLiterals(vc); - FatalAssert(c==3,"Implied literal error 5"); + EXPECT(c==3,"Implied literal error 5"); cout << "Pop" << endl; vc->pop(); @@ -1119,11 +1131,11 @@ void test11() cout << "Assert p(x)" << endl; vc->assertFormula(px); c = printImpliedLiterals(vc); - FatalAssert(c==1,"Implied literal error 6"); + EXPECT(c==1,"Implied literal error 6"); cout << "Assert x = y" << endl; vc->assertFormula(xeqy); c = printImpliedLiterals(vc); - FatalAssert(c==4,"Implied literal error 7"); + EXPECT(c==4,"Implied literal error 7"); cout << "Pop" << endl; vc->pop(); @@ -1132,11 +1144,11 @@ void test11() cout << "Assert NOT p(x)" << endl; vc->assertFormula(!px); c = printImpliedLiterals(vc); - FatalAssert(c==1,"Implied literal error 8"); + EXPECT(c==1,"Implied literal error 8"); cout << "Assert x = y" << endl; vc->assertFormula(xeqy); c = printImpliedLiterals(vc); - FatalAssert(c==4,"Implied literal error 9"); + EXPECT(c==4,"Implied literal error 9"); cout << "Pop" << endl; vc->pop(); @@ -1157,12 +1169,12 @@ void test12() Type boolType = vc->boolType(); vc -> push(); int initial_layer = vc->stackLevel(); - IF_DEBUG(int initial_scope =) vc->scopeLevel(); + int initial_scope = vc->scopeLevel(); Expr exprObj_trueID = vc->trueExpr(); Expr exprObj_falseID = vc->notExpr(vc->trueExpr()); vc->popto(initial_layer); - FatalAssert(vc->scopeLevel() == initial_scope, "Expected no change"); - FatalAssert(vc->stackLevel() == initial_layer, "Expected no change"); + EXPECT(vc->scopeLevel() == initial_scope, "Expected no change"); + EXPECT(vc->stackLevel() == initial_layer, "Expected no change"); // TODO: what happens if we push and then popscope? } catch(const Exception& e) { exitStatus = 1; @@ -1269,7 +1281,7 @@ void test15() { vector<Expr> assertions; cout << "Scope level: " << vc->scopeLevel() << endl; cout << "Counter-example:" << endl; - vc->getCounterExample(assertions); + //vc->getCounterExample(assertions); for (unsigned i = 0; i < assertions.size(); ++i) { vc->printExpr(assertions[i]); } @@ -1346,7 +1358,7 @@ void test15() { cout << " -- no, with counter examples as " << endl; vector<Expr> assert2; - vc->getCounterExample(assert2); + //vc->getCounterExample(assert2); for (unsigned int i = 0; i < assert2.size(); i ++) vc->printExpr(assert2[i]); } @@ -1381,7 +1393,7 @@ void test16() { cout << "Scope level: " << vc->scopeLevel() << endl; cout << "Counter-example:" << endl; vc->getCounterExample(assertions); - FatalAssert(assertions.size() > 0, "Expected non-empty counter-example"); + EXPECT(assertions.size() > 0, "Expected non-empty counter-example"); for (unsigned i = 0; i < assertions.size(); ++i) { vc->printExpr(assertions[i]); } @@ -1397,7 +1409,7 @@ void test16() { for(; it!= end; it++) { Expr eq; if(it->first.getType().isBool()) { - FatalAssert((it->second).isBoolConst(), + EXPECT((it->second).isBoolConst(), "Bad variable assignement: e = "+(it->first).toString() +"\n\n val = "+(it->second).toString()); if((it->second).isTrue()) @@ -1432,7 +1444,7 @@ void test17() { types.push_back(vc->stringExpr("list")); Type badList = vc->dataType("list", "cons", selectors, types); - FatalAssert(false, "Typechecking exception expected"); + EXPECT(false, "Typechecking exception expected"); } catch(const TypecheckException&) { // fall through } @@ -1461,8 +1473,8 @@ void test17() { Expr cons = vc->datatypeConsExpr("cons", args); Expr sel = vc->datatypeSelExpr("car", cons); - IF_DEBUG(bool b =) check(vc, vc->eqExpr(sel, x)); - FatalAssert(b, "Should be valid"); + bool b = check(vc, vc->eqExpr(sel, x)); + EXPECT(b, "Should be valid"); } delete vc; @@ -1495,7 +1507,7 @@ void test17() { types[0][0].push_back(vc->stringExpr("list1")); vc->dataType(names, constructors, selectors, types, returnTypes); - FatalAssert(false, "Typechecking exception expected"); + EXPECT(false, "Typechecking exception expected"); } catch(const TypecheckException&) { // fall through } @@ -1553,8 +1565,8 @@ void test17() { args.push_back(null); Expr cons1_2 = vc->datatypeConsExpr("cons1", args); - IF_DEBUG(bool b =) check(vc, vc->impliesExpr(hyp, vc->eqExpr(z, cons1_2))); - FatalAssert(b, "Should be valid"); + bool b = check(vc, vc->impliesExpr(hyp, vc->eqExpr(z, cons1_2))); + EXPECT(b, "Should be valid"); } delete vc; @@ -1578,8 +1590,8 @@ void test17() { args.push_back(!vc->eqExpr(y,z)); args.push_back(!vc->eqExpr(x,z)); - IF_DEBUG(bool b =) check(vc, !vc->andExpr(args)); - FatalAssert(b, "Should be valid"); + bool b = check(vc, !vc->andExpr(args)); + EXPECT(b, "Should be valid"); } } catch(const Exception& e) { @@ -1649,7 +1661,8 @@ void test18() vc->push(); try { check(vc, vc->notExpr(vc->eqExpr(zero, null))); - FatalAssert(false, "Should have caught tcc exception"); + // TCCs not supported by CVC4 yet + //EXPECT(false, "Should have caught tcc exception"); } catch(const TypecheckException&) { } vc->pop(); @@ -1659,16 +1672,17 @@ void test18() vc->push(); try { check(vc, spxeqx); - FatalAssert(false, "Should have caught tcc exception"); + // TCCs not supported by CVC4 yet + //EXPECT(false, "Should have caught tcc exception"); } catch(const TypecheckException&) { } vc->pop(); bool b = check(vc, vc->impliesExpr(vc->datatypeTestExpr("succ", x), spxeqx)); - FatalAssert(b, "Should be valid"); + EXPECT(b, "Should be valid"); b = check(vc, vc->orExpr(vc->datatypeTestExpr("zero", x), vc->datatypeTestExpr("succ", x))); - FatalAssert(b, "Should be valid"); + EXPECT(b, "Should be valid"); Expr y = vc->varExpr("y", nat); Expr xeqy = vc->eqExpr(x, y); @@ -1680,16 +1694,16 @@ void test18() Expr sy = vc->datatypeConsExpr("succ", args); Expr sxeqsy = vc->eqExpr(sx,sy); b = check(vc, vc->impliesExpr(xeqy, sxeqsy)); - FatalAssert(b, "Should be valid"); + EXPECT(b, "Should be valid"); b = check(vc, vc->notExpr(vc->eqExpr(sx, zero))); - FatalAssert(b, "Should be valid"); + EXPECT(b, "Should be valid"); b = check(vc, vc->impliesExpr(sxeqsy, xeqy)); - FatalAssert(b, "Should be valid"); + EXPECT(b, "Should be valid"); b = check(vc, vc->notExpr(vc->eqExpr(sx, x))); - FatalAssert(b, "Should be valid"); + EXPECT(b, "Should be valid"); } catch(const Exception& e) { exitStatus = 1; @@ -1736,9 +1750,9 @@ void test19() cout<<"Checking formula "<<Q<<"\n in context "<<A<<"\n"; - IF_DEBUG(bool Succ =) vc->query(Q); + bool Succ = vc->query(Q); - FatalAssert(Succ, "Expected valid formula"); + EXPECT(Succ, "Expected valid formula"); } catch(const Exception& e) { exitStatus = 1; @@ -1789,7 +1803,7 @@ void test20() { vc->dataType(names, constructors, selectors, types, returnTypes); - FatalAssert(returnTypes[0].card() == CARD_FINITE, "Expected finite"); + EXPECT(returnTypes[0].card() == CARD_FINITE, "Expected finite"); Unsigned size = returnTypes[0].sizeFinite(); Unsigned i = 0; for (; i < size; ++i) { @@ -1815,32 +1829,51 @@ void test21() { Expr x2 = vc->exprFromString("x"); cout << "x1: " << x1; cout << "\nx2: " << x2; - FatalAssert(x1 == x2, "Expected x1 == x2"); + EXPECT(x1 == x2, "Expected x1 == x2"); + + Expr x3 = vc->exprFromString("x", SMTLIB_V2_LANG); + cout << "\nx3: " << x3; + EXPECT(x1 == x3, "Expected x1 == x3"); Expr y1 = vc->varExpr("y",t); Expr y2 = vc->exprFromString("y"); cout << "\ny1: " << y1; cout << "\ny2: " << y2; - FatalAssert(y1 == y2, "Expected y1 == y2"); + EXPECT(y1 == y2, "Expected y1 == y2"); + + Expr y3 = vc->exprFromString("y", SMTLIB_V2_LANG); + cout << "\ny3: " << y3; + EXPECT(y1 == y3, "Expected y1 == y3"); Expr a1 = vc->gtExpr(x1,vc->ratExpr(0,1)); Expr a2 = vc->exprFromString("x > 0"); cout << "\na1: " << a1; cout << "\na2: " << a2; - FatalAssert(a1 == a2, "Expected a1 == a2"); + EXPECT(a1 == a2, "Expected a1 == a2"); + + Expr a3 = vc->exprFromString("(> x 0)", SMTLIB_V2_LANG); + cout << "\na3: " << a3; + EXPECT(a1 == a3, "Expected a1 == a3"); Expr b1 = vc->ltExpr(x1,y1); Expr b2 = vc->exprFromString ("x < y"); cout << "\nb1: " << b1; cout << "\nb2: " << b2; - FatalAssert(b1 == b2, "Expected b1 == b2"); + EXPECT(b1 == b2, "Expected b1 == b2"); + + Expr b3 = vc->exprFromString ("(< x y)", SMTLIB_V2_LANG); + cout << "\nb3: " << b3; + EXPECT(b1 == b3, "Expected b1 == b3"); Expr e1 = a1 && b1; Expr e2 = vc->exprFromString("x > 0 AND x < y"); - cout << "\ne1: " << e1; cout << "\ne2: " << e2; - FatalAssert(e1 == e2, "Expected e1 == e2"); + EXPECT(e1 == e2, "Expected e1 == e2"); + + Expr e3 = vc->exprFromString("(and (> x 0) (< x y))", SMTLIB_V2_LANG); + cout << "\ne3: " << e3; + EXPECT(e1 == e3, "Expected e1 == e3"); } catch(const Exception& e) { exitStatus = 1; cout << "*** Exception caught in test21(): \n" << e << endl; @@ -1868,56 +1901,56 @@ void test22() { patternvv.push_back(patternv); vc->setTriggers(p,patternv); - FatalAssert( eqExprVecVecs(p.getTriggers(), patternvv), + EXPECT( eqExprVecVecs(p.getTriggers(), patternvv), "Expected p.getTriggers() == patternvv: " + p.toString() ); vc->setTriggers(p,patternvv); - FatalAssert( eqExprVecVecs(p.getTriggers(), patternvv), + EXPECT( eqExprVecVecs(p.getTriggers(), patternvv), "Expected p.getTriggers() == patternvv: " + p.toString() ); // [chris 10/4/2009] Not sure why, but this fails // Expr q(vc->exprFromString("FORALL (x:INT) : PATTERN (f(x)) : x < f(x)")); - // FatalAssert( eqExprVecVecs(q.getTriggers(), patternvv), + // EXPECT( eqExprVecVecs(q.getTriggers(), patternvv), // "Expected q.getTriggers() == patternvv" + q.toString()); vector<Expr> vars; vars.push_back(x); Expr r(vc->forallExpr( vars, vc->ltExpr(x,fx), patternvv )); - FatalAssert( eqExprVecVecs(r.getTriggers(), patternvv), + EXPECT( eqExprVecVecs(r.getTriggers(), patternvv), "Expected r.getTriggers() == patternvv: " + r.toString() ); Expr s(vc->exprFromString("FORALL (x:INT) : x > f(x)")); vc->setTrigger(s,fx); std::vector<std::vector<Expr> > trigsvv = s.getTriggers(); - FatalAssert( trigsvv.size() == 1, + EXPECT( trigsvv.size() == 1, "Expected s.getTriggers().size() == 1: " + trigsvv.size() ); std::vector<Expr> trigsv = trigsvv[0]; - FatalAssert( trigsv.size() == 1, + EXPECT( trigsv.size() == 1, "Expected s.getTriggers()[0].size() == 1: " + trigsv.size() ); - FatalAssert( trigsv[0] == fx, + EXPECT( trigsv[0] == fx, "Expected s.getTriggers()[0][0] == fx: " + (trigsv[0].toString()) ); Expr t(vc->exprFromString("FORALL (x:INT) : x > f(x)")); vc->setMultiTrigger(t,patternv); trigsvv = t.getTriggers(); - FatalAssert( trigsvv.size() == 1, + EXPECT( trigsvv.size() == 1, "Expected t.getTriggers().size() == 1: " + trigsvv.size() ); trigsv = trigsvv[0]; - FatalAssert( trigsv.size() == 1, + EXPECT( trigsv.size() == 1, "Expected t.getTriggers()[0].size() == 1: " + trigsv.size() ); - FatalAssert( trigsv[0] == fx, + EXPECT( trigsv[0] == fx, "Expected t.getTriggers()[0][0] == fx: " + (trigsv[0].toString()) ); } catch(const Exception& e) { @@ -1954,7 +1987,7 @@ void test23() { Expr u(s.substExpr(oldExprs,newExprs)); cout << "u=" << u << "\n"; - FatalAssert( t == u, "Expected t==u" ); + EXPECT( t == u, "Expected t==u" ); } catch(const Exception& e) { exitStatus = 1; cout << "*** Exception caught in test23(): \n" << e << endl; @@ -1979,21 +2012,17 @@ void test24() { cout << p << "\n"; vector<vector<Expr> > pTriggers(p.getTriggers()); - FatalAssert( pTriggers.size() == 1, - "Expected one trigger set. Found: " + - int2string(pTriggers.size())); - FatalAssert( pTriggers[0].size() == 1, - "Expected one trigger. Found: " + - int2string( pTriggers[0].size())); + EXPECT( pTriggers.size() == 1, + "Actual: " + int2string(pTriggers.size())); + EXPECT( pTriggers[0].size() == 1, + "Actual: " + int2string( pTriggers[0].size())); /* We can't check that the trigger == ax, because x will have * been replaced with a bvar */ - FatalAssert( pTriggers[0][0].getKind() == READ, - "Expected READ expression. Found: " + - pTriggers[0][0].getKind()); - FatalAssert( pTriggers[0][0][0] == a, - "Expected read on array: " + a.toString() + - "\nFound: " + pTriggers[0][0][0].toString() ); + EXPECT( pTriggers[0][0].getKind() == READ, + "Actual: " + int2string(pTriggers[0][0].getKind())); + EXPECT( pTriggers[0][0][0] == a, + "Actual: " + pTriggers[0][0][0].toString() ); Expr aPrime(vc->varExpr("a'",aType)); Expr axPrime(vc->exprFromString("a'[x]")); @@ -2006,18 +2035,17 @@ void test24() { cout << q << "\n"; vector<vector<Expr> > qTriggers(q.getTriggers()); - FatalAssert( qTriggers.size() == 1, - "Expected one trigger set. Found: " + - int2string(qTriggers.size())); - FatalAssert( qTriggers[0].size() == 1, - "Expected one trigger. Found: " + - int2string( qTriggers[0].size())); - FatalAssert( qTriggers[0][0].getKind() == READ, - "Expected READ expression. Found: " + - qTriggers[0][0].getKind()); - FatalAssert( qTriggers[0][0][0] == aPrime, - "Expected read on array: " + aPrime.toString() + - "\nFound: " + qTriggers[0][0][0].toString() ); + EXPECT( qTriggers.size() == 1, + "Actual: " + + int2string(qTriggers.size())); + EXPECT( qTriggers[0].size() == 1, + "Actual: " + + int2string(qTriggers[0].size())); + EXPECT( qTriggers[0][0].getKind() == READ, + "Actual: " + + int2string(qTriggers[0][0].getKind())); + EXPECT( qTriggers[0][0][0] == aPrime, + "Actual: " + qTriggers[0][0][0].toString() ); } catch(const Exception& e) { exitStatus = 1; cout << "*** Exception caught in test24(): \n" << e << endl; @@ -2042,7 +2070,7 @@ void test25() { Expr w = vc->ratExpr(-1,10); cout << "-1 over 10 (ints): " << w << endl; - FatalAssert(x == y && y == z && z == w, "Error in rational constants"); + EXPECT(x == y && y == z && z == w, "Error in rational constants"); } catch(const Exception& e) { exitStatus = 1; @@ -2064,17 +2092,17 @@ void test26() { Expr e2 = vc->newBVSHL(x, vc->newBVConstExpr(16, 32)); bool b = check(vc, vc->eqExpr(e1, e2)); - FatalAssert(b, "Should be valid"); + EXPECT(b, "Should be valid"); e1 = vc->newFixedRightShiftExpr(x, 16); e2 = vc->newBVLSHR(x, vc->newBVConstExpr(16, 32)); b = check(vc, vc->eqExpr(e1, e2)); - FatalAssert(b, "Should be valid"); + EXPECT(b, "Should be valid"); e2 = vc->newBVASHR(x, vc->newBVConstExpr(16, 32)); b = check(vc, vc->eqExpr(e1, e2)); - FatalAssert(!b, "Should be invalid"); + EXPECT(!b, "Should be invalid"); } catch(const Exception& e) { exitStatus = 1; @@ -2090,6 +2118,7 @@ int main(int argc, char** argv) if (argc > 1) regressLevel = atoi(argv[1]); cout << "Running API test, regress level = " << regressLevel << endl; exitStatus = 0; + try { // [MGD for CVC4] This is a CVC3 test, and many tests had to be commented // out for CVC4 since the functionality is either unsupported or @@ -2099,22 +2128,22 @@ int main(int argc, char** argv) // not clear how to implement Type::getExpr(), and Exprs and Ops are // indistinguishable, so getOp() and getOpExpr() have the same result. - //cout << "\n}\ntest26(): {" << endl; - //test26(); + cout << "\n}\ntest26(): {" << endl; + test26(); //cout << "\ntest(): {" << endl; //test(); - //cout << "\n}\ntest1(): {" << endl; - //test1(); + cout << "\n}\ntest1(): {" << endl; + test1(); cout << "\n}\n\ntest2(): {" << endl; test2(); cout << "\n}\n\ntest3(): {" << endl; test3(); cout << "\n}\n\ntest4(): {" << endl; test4(); - if (regressLevel > 0) { - cout << "\n}\n\ntest5(): {" << endl; - test5(); - } + //if (regressLevel > 0) { + // cout << "\n}\n\ntest5(): {" << endl; + // test5(); + //} //cout << "\n}\n\ntest6(): {" << endl; //test6(); cout << "\n}\n\ntest7(): {" << endl; @@ -2134,8 +2163,8 @@ int main(int argc, char** argv) test10(); } - cout << "\ntest11(): {" << endl; - test11(); + //cout << "\ntest11(): {" << endl; + //test11(); cout << "\n}\ntest12(): {" << endl; test12(); cout << "\n}\ntest13(): {" << endl; @@ -2150,10 +2179,10 @@ int main(int argc, char** argv) test17(); cout << "\n}\ntest18(): {" << endl; test18(); - //cout << "\n}\ntest19(): {" << endl; - //test19(); - //cout << "\ntest20(): {" << endl; - //test20(); + cout << "\n}\ntest19(): {" << endl; + test19(); + cout << "\ntest20(): {" << endl; + test20(); cout << "\n}\ntest21(): {" << endl; test21(); //cout << "\n}\ntest22(): {" << endl; @@ -2165,6 +2194,7 @@ int main(int argc, char** argv) cout << "\n}\ntest25(): {" << endl; test25(); + /* if (regressLevel > 1) { cout << "\n}\ntestgeorge1(): {" << endl; testgeorge1(); @@ -2177,6 +2207,7 @@ int main(int argc, char** argv) cout << "\n}\ntestgeorge5(): {" << endl; testgeorge5(); } + */ cout << "\n}" << endl; } catch(const Exception& e) { |