summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/compat/cvc3_compat.cpp96
-rw-r--r--src/compat/cvc3_compat.h3
-rw-r--r--src/parser/parser.h3
-rw-r--r--test/system/cvc3_main.cpp142
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, "<internal>").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, "<internal>").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<Type>& 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<std::string>& fields,
const std::vector<Type>& 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, "<internal>").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<Expr>& 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<std::string>& fields,
const std::vector<Expr>& 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<Expr>& 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<Expr>& 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<Expr>& 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<Expr>& 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<Expr>& vars, const Expr& body,
const std::vector<Expr>& triggers) {
- Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+ Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
}
Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body,
const std::vector<std::vector<Expr> >& 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<std::vector<Expr> > & 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<Expr>& 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<Expr>& multiTrigger) {
- Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+ Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)");
}
Expr ValidityChecker::existsExpr(const std::vector<Expr>& 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<Expr>& 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 <stdlib.h>
#include <map>
#include <utility>
@@ -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<Expr> 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<Expr> 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<std::vector<Expr> > trigsvv = s.getTriggers();
- DebugAssert( trigsvv.size() == 1,
+ FatalAssert( trigsvv.size() == 1,
"Expected s.getTriggers().size() == 1: " + trigsvv.size() );
std::vector<Expr> 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<vector<Expr> > 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<vector<Expr> > 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback