From 070b3f89d4bc9940fb87e86108152144b187c891 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 4 Oct 2011 06:25:36 +0000 Subject: [PATCH] compat layer cleanup --- src/compat/cvc3_compat.cpp | 96 +++++++++++++------------ src/compat/cvc3_compat.h | 3 + src/parser/parser.h | 3 +- test/system/cvc3_main.cpp | 142 ++++++++++++++++++------------------- 4 files changed, 127 insertions(+), 117 deletions(-) diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 6db6b440e..7b748a2d3 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -680,6 +680,7 @@ ValidityChecker::ValidityChecker() : setUpOptions(d_options, *d_clflags); d_em = new CVC4::ExprManager(d_options); d_smt = new CVC4::SmtEngine(d_em); + d_parserContext = CVC4::parser::ParserBuilder(d_em, "").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build(); } ValidityChecker::ValidityChecker(const CLFlags& clflags) : @@ -688,9 +689,11 @@ ValidityChecker::ValidityChecker(const CLFlags& clflags) : setUpOptions(d_options, *d_clflags); d_em = new CVC4::ExprManager(d_options); d_smt = new CVC4::SmtEngine(d_em); + d_parserContext = CVC4::parser::ParserBuilder(d_em, "").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build(); } ValidityChecker::~ValidityChecker() { + delete d_parserContext; delete d_clflags; } @@ -948,11 +951,11 @@ Type ValidityChecker::intType() { } Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Subranges not supported by CVC4 yet (sorry!)"); } Type ValidityChecker::subtypeType(const Expr& pred, const Expr& witness) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Predicate subtyping not supported by CVC4 yet (sorry!)"); } Type ValidityChecker::tupleType(const Type& type0, const Type& type1) { @@ -977,23 +980,23 @@ Type ValidityChecker::tupleType(const std::vector& types) { } Type ValidityChecker::recordType(const std::string& field, const Type& type) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Type ValidityChecker::recordType(const std::string& field0, const Type& type0, const std::string& field1, const Type& type1) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Type ValidityChecker::recordType(const std::string& field0, const Type& type0, const std::string& field1, const Type& type1, const std::string& field2, const Type& type2) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Type ValidityChecker::recordType(const std::vector& fields, const std::vector& types) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Type ValidityChecker::dataType(const std::string& name, @@ -1042,11 +1045,11 @@ Type ValidityChecker::createType(const std::string& typeName) { } Type ValidityChecker::createType(const std::string& typeName, const Type& def) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + d_parserContext->defineType(typeName, def); } Type ValidityChecker::lookupType(const std::string& typeName) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + return d_parserContext->getSort(typeName); } ExprManager* ValidityChecker::getEM() { @@ -1054,16 +1057,17 @@ ExprManager* ValidityChecker::getEM() { } Expr ValidityChecker::varExpr(const std::string& name, const Type& type) { - return d_em->mkVar(name, type); + return d_parserContext->mkVar(name, type); } Expr ValidityChecker::varExpr(const std::string& name, const Type& type, const Expr& def) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + FatalAssert(def.getType() == type, "expected types to match"); + d_parserContext->defineVar(name, def); } Expr ValidityChecker::lookupVar(const std::string& name, Type* type) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + return d_parserContext->getVariable(name); } Type ValidityChecker::getType(const Expr& e) { @@ -1138,7 +1142,7 @@ void ValidityChecker::printExpr(const Expr& e, std::ostream& os) { } Expr ValidityChecker::parseExpr(const Expr& e) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + return e; } Type ValidityChecker::parseType(const Expr& e) { @@ -1167,14 +1171,11 @@ Expr ValidityChecker::exprFromString(const std::string& s, InputLanguage lang) { } CVC4::parser::Parser* p = CVC4::parser::ParserBuilder(d_em, "").withStringInput(s).withInputLanguage(lang).build(); - Expr dummy = p->nextExpression(); - if( dummy.isNull() ) { + p->useDeclarationsFrom(d_parserContext); + Expr e = p->nextExpression(); + if( e.isNull() ) { throw CVC4::parser::ParserException("Parser result is null: '" + s + "'"); } - //DebugAssert(dummy.getKind() == RAW_LIST, "Expected list expression"); - //DebugAssert(dummy.arity() == 2, "Expected two children"); - - Expr e = parseExpr(dummy[1]); delete p; @@ -1237,7 +1238,7 @@ Expr ValidityChecker::distinctExpr(const std::vector& children) { } Op ValidityChecker::createOp(const std::string& name, const Type& type) { - return d_em->mkVar(name, type); + return d_parserContext->mkVar(name, type); } Op ValidityChecker::createOp(const std::string& name, const Type& type, @@ -1246,7 +1247,9 @@ Op ValidityChecker::createOp(const std::string& name, const Type& type, } Op ValidityChecker::lookupOp(const std::string& name, Type* type) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Op op = d_parserContext->getFunction(name); + *type = op.getType(); + return op; } Expr ValidityChecker::funExpr(const Op& op, const Expr& child) { @@ -1333,32 +1336,32 @@ Expr ValidityChecker::geExpr(const Expr& left, const Expr& right) { } Expr ValidityChecker::recordExpr(const std::string& field, const Expr& expr) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0, const std::string& field1, const Expr& expr1) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0, const std::string& field1, const Expr& expr1, const std::string& field2, const Expr& expr2) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::recordExpr(const std::vector& fields, const std::vector& exprs) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::recSelectExpr(const Expr& record, const std::string& field) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::recUpdateExpr(const Expr& record, const std::string& field, const Expr& newValue) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Records not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::readExpr(const Expr& array, const Expr& index) { @@ -1657,12 +1660,12 @@ Expr ValidityChecker::tupleExpr(const std::vector& exprs) { } Expr ValidityChecker::tupleSelectExpr(const Expr& tuple, int index) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Tuples not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index, const Expr& newValue) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Tuples not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::datatypeConsExpr(const std::string& constructor, const std::vector& args) { @@ -1679,50 +1682,50 @@ Expr ValidityChecker::datatypeTestExpr(const std::string& constructor, const Exp Expr ValidityChecker::boundVarExpr(const std::string& name, const std::string& uid, const Type& type) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::forallExpr(const std::vector& vars, const Expr& body) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::forallExpr(const std::vector& vars, const Expr& body, const Expr& trigger) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::forallExpr(const std::vector& vars, const Expr& body, const std::vector& triggers) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::forallExpr(const std::vector& vars, const Expr& body, const std::vector >& triggers) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } void ValidityChecker::setTriggers(const Expr& e, const std::vector > & triggers) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } void ValidityChecker::setTriggers(const Expr& e, const std::vector& triggers) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } void ValidityChecker::setTrigger(const Expr& e, const Expr& trigger) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } void ValidityChecker::setMultiTrigger(const Expr& e, const std::vector& multiTrigger) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } Expr ValidityChecker::existsExpr(const std::vector& vars, const Expr& body) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); } Op ValidityChecker::lambdaExpr(const std::vector& vars, const Expr& body) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + Unimplemented("Lambda expressions not supported by CVC4 yet (sorry!)"); } Op ValidityChecker::transClosure(const Op& op) { @@ -1951,9 +1954,10 @@ void ValidityChecker::loadFile(const std::string& fileName, opts.interactive = interactive; opts.interactiveSetByUser = true; CVC4::parser::ParserBuilder parserBuilder(d_em, fileName, opts); - CVC4::parser::Parser* parser = parserBuilder.build(); - doCommands(parser, d_smt, opts); - delete parser; + CVC4::parser::Parser* p = parserBuilder.build(); + p->useDeclarationsFrom(d_parserContext); + doCommands(p, d_smt, opts); + delete p; } void ValidityChecker::loadFile(std::istream& is, @@ -1964,9 +1968,11 @@ void ValidityChecker::loadFile(std::istream& is, opts.interactive = interactive; opts.interactiveSetByUser = true; CVC4::parser::ParserBuilder parserBuilder(d_em, "[stream]", opts); - CVC4::parser::Parser* parser = parserBuilder.withStreamInput(is).build(); - doCommands(parser, d_smt, opts); - delete parser; + CVC4::parser::Parser* p = parserBuilder.withStreamInput(is).build(); + d_parserContext = p; + p->useDeclarationsFrom(d_parserContext); + doCommands(p, d_smt, opts); + delete p; } Statistics& ValidityChecker::getStatistics() { diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h index b4c9cba3e..1e4511ba5 100644 --- a/src/compat/cvc3_compat.h +++ b/src/compat/cvc3_compat.h @@ -60,6 +60,8 @@ #include "util/exception.h" #include "util/hash.h" +#include "parser/parser.h" + #include #include #include @@ -462,6 +464,7 @@ class CVC4_PUBLIC ValidityChecker { CVC4::Options d_options; CVC4::ExprManager* d_em; CVC4::SmtEngine* d_smt; + CVC4::parser::Parser* d_parserContext; ValidityChecker(const CLFlags& clflags); diff --git a/src/parser/parser.h b/src/parser/parser.h index 46544559a..70bd45c31 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -473,7 +473,8 @@ public: * This feature is useful when e.g. reading out-of-band expression data: * 1. Parsing --replay log files produced with --replay-log. * 2. Perhaps a multi-query benchmark file is being single-stepped - * with intervening queries on stdin that must reference + * with intervening queries on stdin that must reference the same + * declaration scope(s). * * However, the feature must be used carefully. Pushes and pops * should be performed with the correct current declaration scope. diff --git a/test/system/cvc3_main.cpp b/test/system/cvc3_main.cpp index ecf664923..d86526da8 100644 --- a/test/system/cvc3_main.cpp +++ b/test/system/cvc3_main.cpp @@ -124,7 +124,7 @@ void test () Expr f2 = vc->funExpr(f, e); Expr f3 = vc->funExpr(f, f2); - DebugAssert(e != f2 && e != f3, "Refcount problems"); + FatalAssert(e != f2 && e != f3, "Refcount problems"); Expr x (vc->boundVarExpr ("x", "0", it));//x0:int vector xs; @@ -160,11 +160,11 @@ void test1() try { IF_DEBUG(bool b =) check(vc, vc->trueExpr()); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); vc->push(); IF_DEBUG(b =) check(vc, vc->falseExpr()); - DebugAssert(!b, "Should be invalid"); + FatalAssert(!b, "Should be invalid"); vc->pop(); // Check p OR ~p @@ -173,7 +173,7 @@ void test1() Expr e = vc->orExpr(p, vc->notExpr(p)); IF_DEBUG(b =) check(vc, e); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); // Check x = y -> f(x) = f(y) @@ -187,7 +187,7 @@ void test1() e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(fx, fy)); IF_DEBUG(b =) check(vc, e); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); // Check f(x) = f(y) -> x = y @@ -195,7 +195,7 @@ void test1() IF_DEBUG(int scopeLevel = vc->scopeLevel();) vc->push(); IF_DEBUG(b =) check(vc, e); - DebugAssert(!b, "Should be invalid"); + FatalAssert(!b, "Should be invalid"); // Get counter-example @@ -211,7 +211,7 @@ void test1() // Reset to initial scope cout << "Resetting" << endl; vc->pop(); - DebugAssert(scopeLevel == vc->scopeLevel(), "scope error"); + FatalAssert(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 +231,7 @@ void test1() cout << endl << "simplify(w) = "; vc->printExpr(vc->simplify(w)); cout << endl; - DebugAssert(vc->simplify(w)==vc->ratExpr(1), "Expected simplify(w) = 1"); + FatalAssert(vc->simplify(w)==vc->ratExpr(1), "Expected simplify(w) = 1"); newAssertion(vc, vc->eqExpr(z, vc->ratExpr(2))); assertions.clear(); @@ -247,7 +247,7 @@ void test1() cout << "simplify(w) = "; vc->printExpr(vc->simplify(w)); - DebugAssert(vc->simplify(w)==w, "Expected simplify(w) = w"); + FatalAssert(vc->simplify(w)==w, "Expected simplify(w) = w"); cout << endl; assertions.clear(); @@ -275,10 +275,10 @@ void test2() vc->assertFormula(c.eqExpr(vc->ratExpr(0)) || c.eqExpr(vc->ratExpr(1))); IF_DEBUG(bool b =) check(vc, vc->leExpr(bexpr, vc->ratExpr(10))); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); IF_DEBUG(b =) check(vc, vc->falseExpr()); - DebugAssert(!b, "Should be invalid"); + FatalAssert(!b, "Should be invalid"); vc->returnFromCheck(); // Check x = y -> g(x,y) = g(y,x) @@ -299,7 +299,7 @@ void test2() Expr e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(gxy, gyx)); IF_DEBUG(b =) check(vc, e); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); Op h = vc->createOp("h", realxreal2real); @@ -308,7 +308,7 @@ void test2() e = vc->impliesExpr(vc->eqExpr(x,y),vc->eqExpr(hxy, hyx)); IF_DEBUG(b =) check(vc, e); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); } catch(const Exception& e) { exitStatus = 1; @@ -803,7 +803,7 @@ void test8() { Expr witness; try { Type t = vc->subtypeType(lambda, witness); - DebugAssert(false, "Typechecking exception expected"); + FatalAssert(false, "Typechecking exception expected"); } catch(const TypecheckException&) { // fall through } @@ -1063,14 +1063,14 @@ void test11() cout << "Assert x = y" << endl; vc->assertFormula(xeqy); c = printImpliedLiterals(vc); - DebugAssert(c==3,"Implied literal error 0"); + FatalAssert(c==3,"Implied literal error 0"); cout << "Push" << endl; vc->push(); cout << "Assert x /= z" << endl; vc->assertFormula(!xeqz); c = printImpliedLiterals(vc); - DebugAssert(c==4,"Implied literal error 1"); + FatalAssert(c==4,"Implied literal error 1"); cout << "Pop" << endl; vc->pop(); @@ -1079,7 +1079,7 @@ void test11() cout << "Assert y /= z" << endl; vc->assertFormula(!yeqz); c = printImpliedLiterals(vc); - DebugAssert(c==4,"Implied literal error 2"); + FatalAssert(c==4,"Implied literal error 2"); cout << "Pop" << endl; vc->pop(); @@ -1088,7 +1088,7 @@ void test11() cout << "Assert p(x)" << endl; vc->assertFormula(px); c = printImpliedLiterals(vc); - DebugAssert(c==2,"Implied literal error 3"); + FatalAssert(c==2,"Implied literal error 3"); cout << "Pop" << endl; vc->pop(); @@ -1097,7 +1097,7 @@ void test11() cout << "Assert p(y)" << endl; vc->assertFormula(py); c = printImpliedLiterals(vc); - DebugAssert(c==2,"Implied literal error 4"); + FatalAssert(c==2,"Implied literal error 4"); cout << "Pop" << endl; vc->pop(); @@ -1109,7 +1109,7 @@ void test11() cout << "Assert y = x" << endl; vc->assertFormula(yeqx); c = printImpliedLiterals(vc); - DebugAssert(c==3,"Implied literal error 5"); + FatalAssert(c==3,"Implied literal error 5"); cout << "Pop" << endl; vc->pop(); @@ -1118,11 +1118,11 @@ void test11() cout << "Assert p(x)" << endl; vc->assertFormula(px); c = printImpliedLiterals(vc); - DebugAssert(c==1,"Implied literal error 6"); + FatalAssert(c==1,"Implied literal error 6"); cout << "Assert x = y" << endl; vc->assertFormula(xeqy); c = printImpliedLiterals(vc); - DebugAssert(c==4,"Implied literal error 7"); + FatalAssert(c==4,"Implied literal error 7"); cout << "Pop" << endl; vc->pop(); @@ -1131,11 +1131,11 @@ void test11() cout << "Assert NOT p(x)" << endl; vc->assertFormula(!px); c = printImpliedLiterals(vc); - DebugAssert(c==1,"Implied literal error 8"); + FatalAssert(c==1,"Implied literal error 8"); cout << "Assert x = y" << endl; vc->assertFormula(xeqy); c = printImpliedLiterals(vc); - DebugAssert(c==4,"Implied literal error 9"); + FatalAssert(c==4,"Implied literal error 9"); cout << "Pop" << endl; vc->pop(); @@ -1160,8 +1160,8 @@ void test12() Expr exprObj_trueID = vc->trueExpr(); Expr exprObj_falseID = vc->notExpr(vc->trueExpr()); vc->popto(initial_layer); - DebugAssert(vc->scopeLevel() == initial_scope, "Expected no change"); - DebugAssert(vc->stackLevel() == initial_layer, "Expected no change"); + FatalAssert(vc->scopeLevel() == initial_scope, "Expected no change"); + FatalAssert(vc->stackLevel() == initial_layer, "Expected no change"); // TODO: what happens if we push and then popscope? } catch(const Exception& e) { exitStatus = 1; @@ -1380,7 +1380,7 @@ void test16() { cout << "Scope level: " << vc->scopeLevel() << endl; cout << "Counter-example:" << endl; vc->getCounterExample(assertions); - DebugAssert(assertions.size() > 0, "Expected non-empty counter-example"); + FatalAssert(assertions.size() > 0, "Expected non-empty counter-example"); for (unsigned i = 0; i < assertions.size(); ++i) { vc->printExpr(assertions[i]); } @@ -1396,7 +1396,7 @@ void test16() { for(; it!= end; it++) { Expr eq; if(it->first.getType().isBool()) { - DebugAssert((it->second).isBoolConst(), + FatalAssert((it->second).isBoolConst(), "Bad variable assignement: e = "+(it->first).toString() +"\n\n val = "+(it->second).toString()); if((it->second).isTrue()) @@ -1431,7 +1431,7 @@ void test17() { types.push_back(vc->stringExpr("list")); Type badList = vc->dataType("list", "cons", selectors, types); - DebugAssert(false, "Typechecking exception expected"); + FatalAssert(false, "Typechecking exception expected"); } catch(const TypecheckException&) { // fall through } @@ -1461,7 +1461,7 @@ void test17() { Expr sel = vc->datatypeSelExpr("car", cons); IF_DEBUG(bool b =) check(vc, vc->eqExpr(sel, x)); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); } delete vc; @@ -1494,7 +1494,7 @@ void test17() { types[0][0].push_back(vc->stringExpr("list1")); vc->dataType(names, constructors, selectors, types, returnTypes); - DebugAssert(false, "Typechecking exception expected"); + FatalAssert(false, "Typechecking exception expected"); } catch(const TypecheckException&) { // fall through } @@ -1553,7 +1553,7 @@ void test17() { Expr cons1_2 = vc->datatypeConsExpr("cons1", args); IF_DEBUG(bool b =) check(vc, vc->impliesExpr(hyp, vc->eqExpr(z, cons1_2))); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); } delete vc; @@ -1578,7 +1578,7 @@ void test17() { args.push_back(!vc->eqExpr(x,z)); IF_DEBUG(bool b =) check(vc, !vc->andExpr(args)); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); } } catch(const Exception& e) { @@ -1648,7 +1648,7 @@ void test18() vc->push(); try { check(vc, vc->notExpr(vc->eqExpr(zero, null))); - DebugAssert(false, "Should have caught tcc exception"); + FatalAssert(false, "Should have caught tcc exception"); } catch(const TypecheckException&) { } vc->pop(); @@ -1658,16 +1658,16 @@ void test18() vc->push(); try { check(vc, spxeqx); - DebugAssert(false, "Should have caught tcc exception"); + FatalAssert(false, "Should have caught tcc exception"); } catch(const TypecheckException&) { } vc->pop(); bool b = check(vc, vc->impliesExpr(vc->datatypeTestExpr("succ", x), spxeqx)); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); b = check(vc, vc->orExpr(vc->datatypeTestExpr("zero", x), vc->datatypeTestExpr("succ", x))); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); Expr y = vc->varExpr("y", nat); Expr xeqy = vc->eqExpr(x, y); @@ -1679,16 +1679,16 @@ void test18() Expr sy = vc->datatypeConsExpr("succ", args); Expr sxeqsy = vc->eqExpr(sx,sy); b = check(vc, vc->impliesExpr(xeqy, sxeqsy)); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); b = check(vc, vc->notExpr(vc->eqExpr(sx, zero))); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); b = check(vc, vc->impliesExpr(sxeqsy, xeqy)); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); b = check(vc, vc->notExpr(vc->eqExpr(sx, x))); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); } catch(const Exception& e) { exitStatus = 1; @@ -1737,7 +1737,7 @@ void test19() IF_DEBUG(bool Succ =) vc->query(Q); - DebugAssert(Succ, "Expected valid formula"); + FatalAssert(Succ, "Expected valid formula"); } catch(const Exception& e) { exitStatus = 1; @@ -1788,7 +1788,7 @@ void test20() { vc->dataType(names, constructors, selectors, types, returnTypes); - DebugAssert(returnTypes[0].card() == CARD_FINITE, "Expected finite"); + FatalAssert(returnTypes[0].card() == CARD_FINITE, "Expected finite"); Unsigned size = returnTypes[0].sizeFinite(); Unsigned i = 0; for (; i < size; ++i) { @@ -1814,32 +1814,32 @@ void test21() { Expr x2 = vc->exprFromString("x"); cout << "x1: " << x1; cout << "\nx2: " << x2; - DebugAssert(x1 == x2, "Expected x1 == x2"); + FatalAssert(x1 == x2, "Expected x1 == x2"); Expr y1 = vc->varExpr("y",t); Expr y2 = vc->exprFromString("y"); cout << "\ny1: " << y1; cout << "\ny2: " << y2; - DebugAssert(y1 == y2, "Expected y1 == y2"); + FatalAssert(y1 == y2, "Expected y1 == y2"); Expr a1 = vc->gtExpr(x1,vc->ratExpr(0,1)); Expr a2 = vc->exprFromString("x > 0"); cout << "\na1: " << a1; cout << "\na2: " << a2; - DebugAssert(a1 == a2, "Expected a1 == a2"); + FatalAssert(a1 == a2, "Expected a1 == a2"); Expr b1 = vc->ltExpr(x1,y1); Expr b2 = vc->exprFromString ("x < y"); cout << "\nb1: " << b1; cout << "\nb2: " << b2; - DebugAssert(b1 == b2, "Expected b1 == b2"); + FatalAssert(b1 == b2, "Expected b1 == b2"); Expr e1 = a1 && b1; Expr e2 = vc->exprFromString("x > 0 AND x < y"); cout << "\ne1: " << e1; cout << "\ne2: " << e2; - DebugAssert(e1 == e2, "Expected e1 == e2"); + FatalAssert(e1 == e2, "Expected e1 == e2"); } catch(const Exception& e) { exitStatus = 1; cout << "*** Exception caught in test21(): \n" << e << endl; @@ -1867,56 +1867,56 @@ void test22() { patternvv.push_back(patternv); vc->setTriggers(p,patternv); - DebugAssert( eqExprVecVecs(p.getTriggers(), patternvv), + FatalAssert( eqExprVecVecs(p.getTriggers(), patternvv), "Expected p.getTriggers() == patternvv: " + p.toString() ); vc->setTriggers(p,patternvv); - DebugAssert( eqExprVecVecs(p.getTriggers(), patternvv), + FatalAssert( 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)")); - // DebugAssert( eqExprVecVecs(q.getTriggers(), patternvv), + // FatalAssert( eqExprVecVecs(q.getTriggers(), patternvv), // "Expected q.getTriggers() == patternvv" + q.toString()); vector vars; vars.push_back(x); Expr r(vc->forallExpr( vars, vc->ltExpr(x,fx), patternvv )); - DebugAssert( eqExprVecVecs(r.getTriggers(), patternvv), + FatalAssert( 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 > trigsvv = s.getTriggers(); - DebugAssert( trigsvv.size() == 1, + FatalAssert( trigsvv.size() == 1, "Expected s.getTriggers().size() == 1: " + trigsvv.size() ); std::vector trigsv = trigsvv[0]; - DebugAssert( trigsv.size() == 1, + FatalAssert( trigsv.size() == 1, "Expected s.getTriggers()[0].size() == 1: " + trigsv.size() ); - DebugAssert( trigsv[0] == fx, + FatalAssert( 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(); - DebugAssert( trigsvv.size() == 1, + FatalAssert( trigsvv.size() == 1, "Expected t.getTriggers().size() == 1: " + trigsvv.size() ); trigsv = trigsvv[0]; - DebugAssert( trigsv.size() == 1, + FatalAssert( trigsv.size() == 1, "Expected t.getTriggers()[0].size() == 1: " + trigsv.size() ); - DebugAssert( trigsv[0] == fx, + FatalAssert( trigsv[0] == fx, "Expected t.getTriggers()[0][0] == fx: " + (trigsv[0].toString()) ); } catch(const Exception& e) { @@ -1953,7 +1953,7 @@ void test23() { Expr u(s.substExpr(oldExprs,newExprs)); cout << "u=" << u << "\n"; - DebugAssert( t == u, "Expected t==u" ); + FatalAssert( t == u, "Expected t==u" ); } catch(const Exception& e) { exitStatus = 1; cout << "*** Exception caught in test23(): \n" << e << endl; @@ -1978,19 +1978,19 @@ void test24() { cout << p << "\n"; vector > pTriggers(p.getTriggers()); - DebugAssert( pTriggers.size() == 1, + FatalAssert( pTriggers.size() == 1, "Expected one trigger set. Found: " + int2string(pTriggers.size())); - DebugAssert( pTriggers[0].size() == 1, + FatalAssert( pTriggers[0].size() == 1, "Expected one trigger. Found: " + int2string( pTriggers[0].size())); /* We can't check that the trigger == ax, because x will have * been replaced with a bvar */ - DebugAssert( pTriggers[0][0].getKind() == READ, + FatalAssert( pTriggers[0][0].getKind() == READ, "Expected READ expression. Found: " + pTriggers[0][0].getKind()); - DebugAssert( pTriggers[0][0][0] == a, + FatalAssert( pTriggers[0][0][0] == a, "Expected read on array: " + a.toString() + "\nFound: " + pTriggers[0][0][0].toString() ); @@ -2005,16 +2005,16 @@ void test24() { cout << q << "\n"; vector > qTriggers(q.getTriggers()); - DebugAssert( qTriggers.size() == 1, + FatalAssert( qTriggers.size() == 1, "Expected one trigger set. Found: " + int2string(qTriggers.size())); - DebugAssert( qTriggers[0].size() == 1, + FatalAssert( qTriggers[0].size() == 1, "Expected one trigger. Found: " + int2string( qTriggers[0].size())); - DebugAssert( qTriggers[0][0].getKind() == READ, + FatalAssert( qTriggers[0][0].getKind() == READ, "Expected READ expression. Found: " + qTriggers[0][0].getKind()); - DebugAssert( qTriggers[0][0][0] == aPrime, + FatalAssert( qTriggers[0][0][0] == aPrime, "Expected read on array: " + aPrime.toString() + "\nFound: " + qTriggers[0][0][0].toString() ); } catch(const Exception& e) { @@ -2041,7 +2041,7 @@ void test25() { Expr w = vc->ratExpr(-1,10); cout << "-1 over 10 (ints): " << w << endl; - DebugAssert(x == y && y == z && z == w, "Error in rational constants"); + FatalAssert(x == y && y == z && z == w, "Error in rational constants"); } catch(const Exception& e) { exitStatus = 1; @@ -2063,17 +2063,17 @@ void test26() { Expr e2 = vc->newBVSHL(x, vc->newBVConstExpr(16, 32)); bool b = check(vc, vc->eqExpr(e1, e2)); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); e1 = vc->newFixedRightShiftExpr(x, 16); e2 = vc->newBVLSHR(x, vc->newBVConstExpr(16, 32)); b = check(vc, vc->eqExpr(e1, e2)); - DebugAssert(b, "Should be valid"); + FatalAssert(b, "Should be valid"); e2 = vc->newBVASHR(x, vc->newBVConstExpr(16, 32)); b = check(vc, vc->eqExpr(e1, e2)); - DebugAssert(!b, "Should be invalid"); + FatalAssert(!b, "Should be invalid"); } catch(const Exception& e) { exitStatus = 1; -- 2.30.2