diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
commit | 65f720aac2d497c6e829d9c76638073a10060e7d (patch) | |
tree | 357035797e31f96a37dce30cb97ddb0aaf8f3bb7 /src/compat | |
parent | c0c351a89871e0a6881668fa1a8d87349ab8af8e (diff) |
Public interface review items:
* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
or a public exception type.
* auto-generated documentation for Smt options and internal options
Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
Diffstat (limited to 'src/compat')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 289 | ||||
-rw-r--r-- | src/compat/cvc3_compat.h | 10 |
2 files changed, 146 insertions, 153 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index b7c7013d2..95417845f 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -40,9 +40,12 @@ #include <sstream> #include <algorithm> #include <iterator> +#include <cassert> using namespace std; +#define Unimplemented(str) throw Exception(str) + namespace CVC3 { // Connects ExprManagers to ValidityCheckers. Needed to clean up the @@ -60,13 +63,13 @@ static bool typeHasExpr(const Type& t) { static Expr typeToExpr(const Type& t) { std::hash_map<Type, Expr, CVC4::TypeHashFunction>::const_iterator i = s_typeToExpr.find(t); - AlwaysAssert(i != s_typeToExpr.end()); + assert(i != s_typeToExpr.end()); return (*i).second; } static Type exprToType(const Expr& e) { std::hash_map<Expr, Type, CVC4::ExprHashFunction>::const_iterator i = s_exprToType.find(e); - AlwaysAssert(i != s_exprToType.end()); + assert(i != s_exprToType.end()); return (*i).second; } @@ -145,7 +148,7 @@ bool operator==(const Cardinality& c, CVC3CardinalityKind d) { return c.isUnknown(); } - Unhandled(d); + throw Exception("internal error: CVC3 cardinality kind unhandled"); } bool operator==(CVC3CardinalityKind d, const Cardinality& c) { @@ -431,7 +434,7 @@ Expr Expr::getExpr() const { } std::vector< std::vector<Expr> > Expr::getTriggers() const { - CheckArgument(isClosure(), *this, __PRETTY_FUNCTION__, "getTriggers() called on non-closure expr"); + CVC4::CheckArgument(isClosure(), *this, "getTriggers() called on non-closure expr"); if(getNumChildren() < 3) { // no triggers for this quantifier return vector< vector<Expr> >(); @@ -589,37 +592,37 @@ CLFlag& CLFlag::operator=(const CLFlag& f) { } CLFlag& CLFlag::operator=(bool b) { - CheckArgument(d_tp == CLFLAG_BOOL, this); + CVC4::CheckArgument(d_tp == CLFLAG_BOOL, this); d_data.b = b; return *this; } CLFlag& CLFlag::operator=(int i) { - CheckArgument(d_tp == CLFLAG_INT, this); + CVC4::CheckArgument(d_tp == CLFLAG_INT, this); d_data.i = i; return *this; } CLFlag& CLFlag::operator=(const std::string& s) { - CheckArgument(d_tp == CLFLAG_STRING, this); + CVC4::CheckArgument(d_tp == CLFLAG_STRING, this); *d_data.s = s; return *this; } CLFlag& CLFlag::operator=(const char* s) { - CheckArgument(d_tp == CLFLAG_STRING, this); + CVC4::CheckArgument(d_tp == CLFLAG_STRING, this); *d_data.s = s; return *this; } CLFlag& CLFlag::operator=(const std::pair<string, bool>& p) { - CheckArgument(d_tp == CLFLAG_STRVEC, this); + CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this); d_data.sv->push_back(p); return *this; } CLFlag& CLFlag::operator=(const std::vector<std::pair<string, bool> >& sv) { - CheckArgument(d_tp == CLFLAG_STRVEC, this); + CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this); *d_data.sv = sv; return *this; } @@ -637,22 +640,22 @@ bool CLFlag::display() const { } const bool& CLFlag::getBool() const { - CheckArgument(d_tp == CLFLAG_BOOL, this); + CVC4::CheckArgument(d_tp == CLFLAG_BOOL, this); return d_data.b; } const int& CLFlag::getInt() const { - CheckArgument(d_tp == CLFLAG_INT, this); + CVC4::CheckArgument(d_tp == CLFLAG_INT, this); return d_data.i; } const std::string& CLFlag::getString() const { - CheckArgument(d_tp == CLFLAG_STRING, this); + CVC4::CheckArgument(d_tp == CLFLAG_STRING, this); return *d_data.s; } const std::vector<std::pair<string, bool> >& CLFlag::getStrVec() const { - CheckArgument(d_tp == CLFLAG_STRVEC, this); + CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this); return *d_data.sv; } @@ -675,7 +678,7 @@ size_t CLFlags::countFlags(const std::string& name, const CLFlag& CLFlags::getFlag(const std::string& name) const { FlagMap::const_iterator i = d_map.find(name); - CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); return (*i).second; } @@ -685,49 +688,49 @@ const CLFlag& CLFlags::operator[](const std::string& name) const { void CLFlags::setFlag(const std::string& name, const CLFlag& f) { FlagMap::iterator i = d_map.find(name); - CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); - CheckArgument((*i).second.getType() == f.getType(), f, - "Command-line flag `%s' has type %s, but caller tried to set to a %s.", - name.c_str(), - toString((*i).second.getType()).c_str(), - toString(f.getType()).c_str()); + CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CVC4::CheckArgument((*i).second.getType() == f.getType(), f, + "Command-line flag `%s' has type %s, but caller tried to set to a %s.", + name.c_str(), + toString((*i).second.getType()).c_str(), + toString(f.getType()).c_str()); (*i).second = f; } void CLFlags::setFlag(const std::string& name, bool b) { FlagMap::iterator i = d_map.find(name); - CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); (*i).second = b; } void CLFlags::setFlag(const std::string& name, int i) { FlagMap::iterator it = d_map.find(name); - CheckArgument(it != d_map.end(), name, "No command-line flag by that name, or not supported."); + CVC4::CheckArgument(it != d_map.end(), name, "No command-line flag by that name, or not supported."); (*it).second = i; } void CLFlags::setFlag(const std::string& name, const std::string& s) { FlagMap::iterator i = d_map.find(name); - CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); (*i).second = s; } void CLFlags::setFlag(const std::string& name, const char* s) { FlagMap::iterator i = d_map.find(name); - CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); (*i).second = s; } void CLFlags::setFlag(const std::string& name, const std::pair<string, bool>& p) { FlagMap::iterator i = d_map.find(name); - CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); (*i).second = p; } void CLFlags::setFlag(const std::string& name, const std::vector<std::pair<string, bool> >& sv) { FlagMap::iterator i = d_map.find(name); - CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); (*i).second = sv; } @@ -1063,8 +1066,8 @@ Type ValidityChecker::intType() { Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) { bool noLowerBound = l.getType().isString() && l.getConst<string>() == "_NEGINF"; bool noUpperBound = r.getType().isString() && r.getConst<string>() == "_POSINF"; - CheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l); - CheckArgument(noUpperBound || (r.getKind() == CVC4::kind::CONST_RATIONAL && r.getConst<Rational>().isIntegral()), r); + CVC4::CheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l); + CVC4::CheckArgument(noUpperBound || (r.getKind() == CVC4::kind::CONST_RATIONAL && r.getConst<Rational>().isIntegral()), r); CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst<Rational>().getNumerator()); CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst<Rational>().getNumerator()); return d_em->mkSubrangeType(CVC4::SubrangeBounds(bl, br)); @@ -1123,7 +1126,7 @@ Type ValidityChecker::dataType(const std::string& name, const std::string& constructor, const std::vector<std::string>& selectors, const std::vector<Expr>& types) { - CheckArgument(selectors.size() == types.size(), types, "expected selectors and types vectors to be of equal length"); + CVC4::CheckArgument(selectors.size() == types.size(), types, "expected selectors and types vectors to be of equal length"); vector<string> cv; vector< vector<string> > sv; vector< vector<Expr> > tv; @@ -1137,8 +1140,8 @@ Type ValidityChecker::dataType(const std::string& name, const std::vector<std::string>& constructors, const std::vector<std::vector<std::string> >& selectors, const std::vector<std::vector<Expr> >& types) { - CheckArgument(constructors.size() == selectors.size(), selectors, "expected constructors and selectors vectors to be of equal length"); - CheckArgument(constructors.size() == types.size(), types, "expected constructors and types vectors to be of equal length"); + CVC4::CheckArgument(constructors.size() == selectors.size(), selectors, "expected constructors and selectors vectors to be of equal length"); + CVC4::CheckArgument(constructors.size() == types.size(), types, "expected constructors and types vectors to be of equal length"); vector<string> nv; vector< vector<string> > cv; vector< vector< vector<string> > > sv; @@ -1149,7 +1152,7 @@ Type ValidityChecker::dataType(const std::string& name, tv.push_back(types); vector<Type> dtts; dataType(nv, cv, sv, tv, dtts); - AlwaysAssert(dtts.size() == 1); + assert(dtts.size() == 1); return dtts[0]; } @@ -1159,19 +1162,19 @@ void ValidityChecker::dataType(const std::vector<std::string>& names, const std::vector<std::vector<std::vector<Expr> > >& types, std::vector<Type>& returnTypes) { - CheckArgument(names.size() == constructors.size(), constructors, "expected names and constructors vectors to be of equal length"); - CheckArgument(names.size() == selectors.size(), selectors, "expected names and selectors vectors to be of equal length"); - CheckArgument(names.size() == types.size(), types, "expected names and types vectors to be of equal length"); + CVC4::CheckArgument(names.size() == constructors.size(), constructors, "expected names and constructors vectors to be of equal length"); + CVC4::CheckArgument(names.size() == selectors.size(), selectors, "expected names and selectors vectors to be of equal length"); + CVC4::CheckArgument(names.size() == types.size(), types, "expected names and types vectors to be of equal length"); vector<CVC4::Datatype> dv; // Set up the datatype specifications. for(unsigned i = 0; i < names.size(); ++i) { CVC4::Datatype dt(names[i]); - CheckArgument(constructors[i].size() == selectors[i].size(), "expected sub-vectors in constructors and selectors vectors to match in size"); - CheckArgument(constructors[i].size() == types[i].size(), "expected sub-vectors in constructors and types vectors to match in size"); + CVC4::CheckArgument(constructors[i].size() == selectors[i].size(), "expected sub-vectors in constructors and selectors vectors to match in size"); + CVC4::CheckArgument(constructors[i].size() == types[i].size(), "expected sub-vectors in constructors and types vectors to match in size"); for(unsigned j = 0; j < constructors[i].size(); ++j) { CVC4::DatatypeConstructor ctor(constructors[i][j]); - CheckArgument(selectors[i][j].size() == types[i][j].size(), types, "expected sub-vectors in selectors and types vectors to match in size"); + CVC4::CheckArgument(selectors[i][j].size() == types[i][j].size(), types, "expected sub-vectors in selectors and types vectors to match in size"); for(unsigned k = 0; k < selectors[i][j].size(); ++k) { if(types[i][j][k].getType().isString()) { ctor.addArg(selectors[i][j][k], CVC4::DatatypeUnresolvedType(types[i][j][k].getConst<string>())); @@ -1200,10 +1203,10 @@ void ValidityChecker::dataType(const std::vector<std::string>& names, } for(CVC4::Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) { // For each constructor, register its name and its selectors names. - CheckArgument(d_constructors.find((*j).getName()) == d_constructors.end(), constructors, "cannot have two constructors with the same name in a ValidityChecker"); + CVC4::CheckArgument(d_constructors.find((*j).getName()) == d_constructors.end(), constructors, "cannot have two constructors with the same name in a ValidityChecker"); d_constructors[(*j).getName()] = &dt; for(CVC4::DatatypeConstructor::const_iterator k = (*j).begin(); k != (*j).end(); ++k) { - CheckArgument(d_selectors.find((*k).getName()) == d_selectors.end(), selectors, "cannot have two selectors with the same name in a ValidityChecker"); + CVC4::CheckArgument(d_selectors.find((*k).getName()) == d_selectors.end(), selectors, "cannot have two selectors with the same name in a ValidityChecker"); d_selectors[(*k).getName()] = make_pair(&dt, (*j).getName()); } } @@ -1219,7 +1222,7 @@ Type ValidityChecker::arrayType(const Type& typeIndex, const Type& typeData) { } Type ValidityChecker::bitvecType(int n) { - CheckArgument(n >= 0, n, "cannot construct a bitvector type of negative size"); + CVC4::CheckArgument(n >= 0, n, "cannot construct a bitvector type of negative size"); return d_em->mkBitVectorType(n); } @@ -1255,7 +1258,7 @@ Expr ValidityChecker::varExpr(const std::string& name, const Type& type) { Expr ValidityChecker::varExpr(const std::string& name, const Type& type, const Expr& def) { - FatalAssert(def.getType() == type, "expected types to match"); + CVC4::CheckArgument(def.getType() == type, def, "expected types to match"); d_parserContext->defineVar(name, def); } @@ -1281,7 +1284,7 @@ Type ValidityChecker::getBaseType(const Type& t) { if(type.isReal()) { return d_em->realType(); } - Assert(!type.isInteger());// should be handled by Real + assert(!type.isInteger());// should be handled by Real if(type.isBoolean()) { return d_em->booleanType(); } @@ -1418,7 +1421,7 @@ Expr ValidityChecker::andExpr(const Expr& left, const Expr& right) { Expr ValidityChecker::andExpr(const std::vector<Expr>& children) { // AND must have at least 2 children - CheckArgument(children.size() > 0, children); + CVC4::CheckArgument(children.size() > 0, children); return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::AND, *reinterpret_cast<const vector<CVC4::Expr>*>(&children))); } @@ -1428,7 +1431,7 @@ Expr ValidityChecker::orExpr(const Expr& left, const Expr& right) { Expr ValidityChecker::orExpr(const std::vector<Expr>& children) { // OR must have at least 2 children - CheckArgument(children.size() > 0, children); + CVC4::CheckArgument(children.size() > 0, children); return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::OR, *reinterpret_cast<const vector<CVC4::Expr>*>(&children))); } @@ -1450,7 +1453,7 @@ Expr ValidityChecker::iteExpr(const Expr& ifpart, const Expr& thenpart, } Expr ValidityChecker::distinctExpr(const std::vector<Expr>& children) { - CheckArgument(children.size() > 1, children, "it makes no sense to create a `distinct' expression with only one child"); + CVC4::CheckArgument(children.size() > 1, children, "it makes no sense to create a `distinct' expression with only one child"); const vector<CVC4::Expr>& v = *reinterpret_cast<const vector<CVC4::Expr>*>(&children); return d_em->mkExpr(CVC4::kind::DISTINCT, v); @@ -1462,7 +1465,7 @@ Op ValidityChecker::createOp(const std::string& name, const Type& type) { Op ValidityChecker::createOp(const std::string& name, const Type& type, const Expr& def) { - CheckArgument(def.getType() == type, type, + CVC4::CheckArgument(def.getType() == type, type, "Type mismatch in ValidityChecker::createOp(): `%s' defined to an " "expression of type %s but ascribed as type %s", name.c_str(), def.getType().toString().c_str(), type.toString().c_str()); @@ -1512,7 +1515,7 @@ Expr ValidityChecker::ratExpr(const std::string& n, int base) { if(n.find(".") == string::npos) { return d_em->mkConst(Rational(n, base)); } else { - CheckArgument(base == 10, base, "unsupported base for decimal parsing"); + CVC4::CheckArgument(base == 10, base, "unsupported base for decimal parsing"); return d_em->mkConst(Rational::fromDecimal(n)); } } @@ -1527,7 +1530,7 @@ Expr ValidityChecker::plusExpr(const Expr& left, const Expr& right) { Expr ValidityChecker::plusExpr(const std::vector<Expr>& children) { // PLUS must have at least 2 children - CheckArgument(children.size() > 0, children); + CVC4::CheckArgument(children.size() > 0, children); return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::PLUS, *reinterpret_cast<const vector<CVC4::Expr>*>(&children))); } @@ -1618,9 +1621,9 @@ Expr ValidityChecker::newBVConstExpr(const std::vector<bool>& bits) { Expr ValidityChecker::newBVConstExpr(const Rational& r, int len) { // implementation based on CVC3's TheoryBitvector::newBVConstExpr() - CheckArgument(r.getDenominator() == 1, r, "ValidityChecker::newBVConstExpr: " + CVC4::CheckArgument(r.getDenominator() == 1, r, "ValidityChecker::newBVConstExpr: " "not an integer: `%s'", r.toString().c_str()); - CheckArgument(len > 0, len, "ValidityChecker::newBVConstExpr: " + CVC4::CheckArgument(len > 0, len, "ValidityChecker::newBVConstExpr: " "len = %d", len); string s(r.toString(2)); @@ -1643,8 +1646,8 @@ Expr ValidityChecker::newBVConstExpr(const Rational& r, int len) { } Expr ValidityChecker::newConcatExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only concat a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only concat a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only concat a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only concat a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_CONCAT, t1, t2); } @@ -1655,29 +1658,29 @@ Expr ValidityChecker::newConcatExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVExtractExpr(const Expr& e, int hi, int low) { - CheckArgument(e.getType().isBitVector(), e, "can only bvextract from a bitvector, not a `%s'", e.getType().toString().c_str()); - CheckArgument(hi >= low, hi, "extraction [%d:%d] is bad; possibly inverted?", hi, low); - CheckArgument(low >= 0, low, "extraction [%d:%d] is bad (negative)", hi, low); - CheckArgument(CVC4::BitVectorType(e.getType()).getSize() > unsigned(hi), hi, "bitvector is of size %u, extraction [%d:%d] is off-the-end", CVC4::BitVectorType(e.getType()).getSize(), hi, low); + CVC4::CheckArgument(e.getType().isBitVector(), e, "can only bvextract from a bitvector, not a `%s'", e.getType().toString().c_str()); + CVC4::CheckArgument(hi >= low, hi, "extraction [%d:%d] is bad; possibly inverted?", hi, low); + CVC4::CheckArgument(low >= 0, low, "extraction [%d:%d] is bad (negative)", hi, low); + CVC4::CheckArgument(CVC4::BitVectorType(e.getType()).getSize() > unsigned(hi), hi, "bitvector is of size %u, extraction [%d:%d] is off-the-end", CVC4::BitVectorType(e.getType()).getSize(), hi, low); return d_em->mkExpr(CVC4::kind::BITVECTOR_EXTRACT, d_em->mkConst(CVC4::BitVectorExtract(hi, low)), e); } Expr ValidityChecker::newBVNegExpr(const Expr& t1) { // CVC3's BVNEG => SMT-LIBv2 bvnot - CheckArgument(t1.getType().isBitVector(), t1, "can only bvneg a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvneg a bitvector, not a `%s'", t1.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_NOT, t1); } Expr ValidityChecker::newBVAndExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvand a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvand a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvand a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvand a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_AND, t1, t2); } Expr ValidityChecker::newBVAndExpr(const std::vector<Expr>& kids) { // BITVECTOR_AND is not N-ary in CVC4 - CheckArgument(kids.size() > 1, kids, "BITVECTOR_AND must have at least 2 children"); + CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_AND must have at least 2 children"); std::vector<Expr>::const_reverse_iterator i = kids.rbegin(); Expr e = *i++; while(i != kids.rend()) { @@ -1687,14 +1690,14 @@ Expr ValidityChecker::newBVAndExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVOrExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvor a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvor a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvor a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvor a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_OR, t1, t2); } Expr ValidityChecker::newBVOrExpr(const std::vector<Expr>& kids) { // BITVECTOR_OR is not N-ary in CVC4 - CheckArgument(kids.size() > 1, kids, "BITVECTOR_OR must have at least 2 children"); + CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_OR must have at least 2 children"); std::vector<Expr>::const_reverse_iterator i = kids.rbegin(); Expr e = *i++; while(i != kids.rend()) { @@ -1704,14 +1707,14 @@ Expr ValidityChecker::newBVOrExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVXorExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvxor a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvxor a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvxor a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvxor a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_XOR, t1, t2); } Expr ValidityChecker::newBVXorExpr(const std::vector<Expr>& kids) { // BITVECTOR_XOR is not N-ary in CVC4 - CheckArgument(kids.size() > 1, kids, "BITVECTOR_XOR must have at least 2 children"); + CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_XOR must have at least 2 children"); std::vector<Expr>::const_reverse_iterator i = kids.rbegin(); Expr e = *i++; while(i != kids.rend()) { @@ -1721,14 +1724,14 @@ Expr ValidityChecker::newBVXorExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVXnorExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvxnor a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvxnor a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvxnor a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvxnor a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_XNOR, t1, t2); } Expr ValidityChecker::newBVXnorExpr(const std::vector<Expr>& kids) { // BITVECTOR_XNOR is not N-ary in CVC4 - CheckArgument(kids.size() > 1, kids, "BITVECTOR_XNOR must have at least 2 children"); + CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_XNOR must have at least 2 children"); std::vector<Expr>::const_reverse_iterator i = kids.rbegin(); Expr e = *i++; while(i != kids.rend()) { @@ -1738,73 +1741,73 @@ Expr ValidityChecker::newBVXnorExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVNandExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvnand a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvnand a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvnand a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvnand a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_NAND, t1, t2); } Expr ValidityChecker::newBVNorExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvnor a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvnor a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvnor a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvnor a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_NOR, t1, t2); } Expr ValidityChecker::newBVCompExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvcomp a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvcomp a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvcomp a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvcomp a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_COMP, t1, t2); } Expr ValidityChecker::newBVLTExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvlt a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvlt a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvlt a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvlt a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_ULT, t1, t2); } Expr ValidityChecker::newBVLEExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvle a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvle a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvle a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvle a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_ULE, t1, t2); } Expr ValidityChecker::newBVSLTExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvslt a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvslt a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvslt a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvslt a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SLT, t1, t2); } Expr ValidityChecker::newBVSLEExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvsle a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvsle a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsle a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsle a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SLE, t1, t2); } Expr ValidityChecker::newSXExpr(const Expr& t1, int len) { - CheckArgument(t1.getType().isBitVector(), t1, "can only sx a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(len >= 0, len, "must sx by a positive integer"); - CheckArgument(unsigned(len) >= CVC4::BitVectorType(t1.getType()).getSize(), len, "cannot sx by something smaller than the bitvector (%d < %u)", len, CVC4::BitVectorType(t1.getType()).getSize()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only sx a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(len >= 0, len, "must sx by a positive integer"); + CVC4::CheckArgument(unsigned(len) >= CVC4::BitVectorType(t1.getType()).getSize(), len, "cannot sx by something smaller than the bitvector (%d < %u)", len, CVC4::BitVectorType(t1.getType()).getSize()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SIGN_EXTEND, d_em->mkConst(CVC4::BitVectorSignExtend(len)), t1); } Expr ValidityChecker::newBVUminusExpr(const Expr& t1) { // CVC3's BVUMINUS => SMT-LIBv2 bvneg - CheckArgument(t1.getType().isBitVector(), t1, "can only bvuminus a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvuminus a bitvector, not a `%s'", t1.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_NEG, t1); } Expr ValidityChecker::newBVSubExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvsub a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvsub by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsub a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsub by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SUB, t1, t2); } // Copied from CVC3's bitvector theory: makes bitvector expression "e" // into "len" bits, by zero-padding, or extracting least-significant bits. Expr ValidityChecker::bvpad(int len, const Expr& e) { - CheckArgument(len >= 0, len, + CVC4::CheckArgument(len >= 0, len, "padding length must be a non-negative integer, not %d", len); - CheckArgument(e.getType().isBitVector(), e, + CVC4::CheckArgument(e.getType().isBitVector(), e, "input to bitvector operation must be a bitvector"); unsigned size = CVC4::BitVectorType(e.getType()).getSize(); @@ -1823,89 +1826,89 @@ Expr ValidityChecker::bvpad(int len, const Expr& e) { Expr ValidityChecker::newBVPlusExpr(int numbits, const std::vector<Expr>& kids) { // BITVECTOR_PLUS is not N-ary in CVC4 - CheckArgument(kids.size() > 1, kids, "BITVECTOR_PLUS must have at least 2 children"); + CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_PLUS must have at least 2 children"); std::vector<Expr>::const_reverse_iterator i = kids.rbegin(); Expr e = *i++; while(i != kids.rend()) { e = d_em->mkExpr(CVC4::kind::BITVECTOR_PLUS, bvpad(numbits, *i++), e); } unsigned size = CVC4::BitVectorType(e.getType()).getSize(); - CheckArgument(unsigned(numbits) == size, numbits, + CVC4::CheckArgument(unsigned(numbits) == size, numbits, "argument must match computed size of bitvector sum: " "passed size == %u, computed size == %u", numbits, size); return e; } Expr ValidityChecker::newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvplus a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvplus a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvplus a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvplus a bitvector, not a `%s'", t2.getType().toString().c_str()); Expr e = d_em->mkExpr(CVC4::kind::BITVECTOR_PLUS, bvpad(numbits, t1), bvpad(numbits, t2)); unsigned size = CVC4::BitVectorType(e.getType()).getSize(); - CheckArgument(unsigned(numbits) == size, numbits, + CVC4::CheckArgument(unsigned(numbits) == size, numbits, "argument must match computed size of bitvector sum: " "passed size == %u, computed size == %u", numbits, size); return e; } Expr ValidityChecker::newBVMultExpr(int numbits, const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvmult a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvmult by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvmult a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvmult by a bitvector, not a `%s'", t2.getType().toString().c_str()); Expr e = d_em->mkExpr(CVC4::kind::BITVECTOR_MULT, bvpad(numbits, t1), bvpad(numbits, t2)); unsigned size = CVC4::BitVectorType(e.getType()).getSize(); - CheckArgument(unsigned(numbits) == size, numbits, + CVC4::CheckArgument(unsigned(numbits) == size, numbits, "argument must match computed size of bitvector product: " "passed size == %u, computed size == %u", numbits, size); return e; } Expr ValidityChecker::newBVUDivExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvudiv a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvudiv by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvudiv a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvudiv by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_UDIV, t1, t2); } Expr ValidityChecker::newBVURemExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvurem a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvurem by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvurem a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvurem by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_UREM, t1, t2); } Expr ValidityChecker::newBVSDivExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvsdiv a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvsdiv by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsdiv a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsdiv by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SDIV, t1, t2); } Expr ValidityChecker::newBVSRemExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvsrem a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvsrem by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsrem a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsrem by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SREM, t1, t2); } Expr ValidityChecker::newBVSModExpr(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only bvsmod a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only bvsmod by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsmod a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsmod by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SMOD, t1, t2); } Expr ValidityChecker::newFixedLeftShiftExpr(const Expr& t1, int r) { - CheckArgument(t1.getType().isBitVector(), t1, "can only left-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(r >= 0, r, "left shift amount must be >= 0 (you passed %d)", r); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only left-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(r >= 0, r, "left shift amount must be >= 0 (you passed %d)", r); // Defined in: // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit return d_em->mkExpr(CVC4::kind::BITVECTOR_CONCAT, t1, d_em->mkConst(CVC4::BitVector(r))); } Expr ValidityChecker::newFixedConstWidthLeftShiftExpr(const Expr& t1, int r) { - CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(r >= 0, r, "const-width left shift amount must be >= 0 (you passed %d)", r); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(r >= 0, r, "const-width left shift amount must be >= 0 (you passed %d)", r); // just turn it into a BVSHL return d_em->mkExpr(CVC4::kind::BITVECTOR_SHL, t1, d_em->mkConst(CVC4::BitVector(CVC4::BitVectorType(t1.getType()).getSize(), unsigned(r)))); } Expr ValidityChecker::newFixedRightShiftExpr(const Expr& t1, int r) { - CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(r >= 0, r, "right shift amount must be >= 0 (you passed %d)", r); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(r >= 0, r, "right shift amount must be >= 0 (you passed %d)", r); // Defined in: // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit // Should be equivalent to a BVLSHR; just turn it into that. @@ -1913,20 +1916,20 @@ Expr ValidityChecker::newFixedRightShiftExpr(const Expr& t1, int r) { } Expr ValidityChecker::newBVSHL(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_SHL, t1, t2); } Expr ValidityChecker::newBVLSHR(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_LSHR, t1, t2); } Expr ValidityChecker::newBVASHR(const Expr& t1, const Expr& t2) { - CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); - CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); + CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str()); return d_em->mkExpr(CVC4::kind::BITVECTOR_ASHR, t1, t2); } @@ -1951,16 +1954,16 @@ Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index, Expr ValidityChecker::datatypeConsExpr(const std::string& constructor, const std::vector<Expr>& args) { ConstructorMap::const_iterator i = d_constructors.find(constructor); - AlwaysAssert(i != d_constructors.end(), "no such constructor"); + CVC4::CheckArgument(i != d_constructors.end(), constructor, "no such constructor"); const CVC4::Datatype& dt = *(*i).second; const CVC4::DatatypeConstructor& ctor = dt[constructor]; - AlwaysAssert(ctor.getNumArgs() == args.size(), "arity mismatch in constructor application"); + CVC4::CheckArgument(ctor.getNumArgs() == args.size(), args, "arity mismatch in constructor application"); return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, ctor.getConstructor(), vector<CVC4::Expr>(args.begin(), args.end())); } Expr ValidityChecker::datatypeSelExpr(const std::string& selector, const Expr& arg) { SelectorMap::const_iterator i = d_selectors.find(selector); - AlwaysAssert(i != d_selectors.end(), "no such selector"); + CVC4::CheckArgument(i != d_selectors.end(), selector, "no such selector"); const CVC4::Datatype& dt = *(*i).second.first; string constructor = (*i).second.second; const CVC4::DatatypeConstructor& ctor = dt[constructor]; @@ -1969,7 +1972,7 @@ Expr ValidityChecker::datatypeSelExpr(const std::string& selector, const Expr& a Expr ValidityChecker::datatypeTestExpr(const std::string& constructor, const Expr& arg) { ConstructorMap::const_iterator i = d_constructors.find(constructor); - AlwaysAssert(i != d_constructors.end(), "no such constructor"); + CVC4::CheckArgument(i != d_constructors.end(), constructor, "no such constructor"); const CVC4::Datatype& dt = *(*i).second; const CVC4::DatatypeConstructor& ctor = dt[constructor]; return d_em->mkExpr(CVC4::kind::APPLY_TESTER, ctor.getTester(), arg); @@ -2122,7 +2125,7 @@ void ValidityChecker::returnFromCheck() { } void ValidityChecker::getUserAssumptions(std::vector<Expr>& assumptions) { - CheckArgument(assumptions.empty(), assumptions, "assumptions arg must be empty"); + CVC4::CheckArgument(assumptions.empty(), assumptions, "assumptions arg must be empty"); vector<CVC4::Expr> v = d_smt->getAssertions(); assumptions.swap(*reinterpret_cast<vector<Expr>*>(&v)); } @@ -2157,7 +2160,7 @@ QueryResult ValidityChecker::tryModelGeneration() { } FormulaValue ValidityChecker::value(const Expr& e) { - CheckArgument(e.getType() == d_em->booleanType(), e, "argument must be a formula"); + CVC4::CheckArgument(e.getType() == d_em->booleanType(), e, "argument must be a formula"); try { return d_smt->getValue(e).getConst<bool>() ? TRUE_VAL : FALSE_VAL; } catch(CVC4::Exception& e) { @@ -2175,7 +2178,7 @@ Expr ValidityChecker::getValue(const Expr& e) { } bool ValidityChecker::inconsistent(std::vector<Expr>& assumptions) { - CheckArgument(assumptions.empty(), assumptions, "assumptions vector should be empty on entry"); + CVC4::CheckArgument(assumptions.empty(), assumptions, "assumptions vector should be empty on entry"); if(d_smt->checkSat() == CVC4::Result::UNSAT) { // supposed to be a minimal set, but CVC4 doesn't support that d_smt->getAssertions().swap(*reinterpret_cast<std::vector<CVC4::Expr>*>(&assumptions)); @@ -2235,12 +2238,12 @@ void ValidityChecker::pop() { } void ValidityChecker::popto(int stackLevel) { - CheckArgument(stackLevel >= 0, stackLevel, - "Cannot pop to a negative stack level %d", stackLevel); - CheckArgument(unsigned(stackLevel) <= d_stackLevel, stackLevel, - "Cannot pop to a stack level higher than the current one! " - "At stack level %u, user requested stack level %d", - d_stackLevel, stackLevel); + CVC4::CheckArgument(stackLevel >= 0, stackLevel, + "Cannot pop to a negative stack level %d", stackLevel); + CVC4::CheckArgument(unsigned(stackLevel) <= d_stackLevel, stackLevel, + "Cannot pop to a stack level higher than the current one! " + "At stack level %u, user requested stack level %d", + d_stackLevel, stackLevel); while(unsigned(stackLevel) < d_stackLevel) { pop(); } @@ -2259,13 +2262,13 @@ void ValidityChecker::popScope() { } void ValidityChecker::poptoScope(int scopeLevel) { - CheckArgument(scopeLevel >= 0, scopeLevel, - "Cannot pop to a negative scope level %d", scopeLevel); - CheckArgument(unsigned(scopeLevel) <= d_parserContext->getDeclarationLevel(), - scopeLevel, - "Cannot pop to a scope level higher than the current one! " - "At scope level %u, user requested scope level %d", - d_parserContext->getDeclarationLevel(), scopeLevel); + CVC4::CheckArgument(scopeLevel >= 0, scopeLevel, + "Cannot pop to a negative scope level %d", scopeLevel); + CVC4::CheckArgument(unsigned(scopeLevel) <= d_parserContext->getDeclarationLevel(), + scopeLevel, + "Cannot pop to a scope level higher than the current one! " + "At scope level %u, user requested scope level %d", + d_parserContext->getDeclarationLevel(), scopeLevel); while(unsigned(scopeLevel) < d_parserContext->getDeclarationLevel()) { popScope(); } diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h index 31d914b58..911e967ca 100644 --- a/src/compat/cvc3_compat.h +++ b/src/compat/cvc3_compat.h @@ -68,16 +68,6 @@ #include <map> #include <utility> -// some #defines that CVC3 exported to userspace :( -#ifdef CVC4_DEBUG -# define DebugAssert(cond, str) Assert((cond), "CVC3-style assertion failed: %s", std::string(str).c_str()); -# define IF_DEBUG(x) x -#else -# define DebugAssert(...) -# define IF_DEBUG(x) -#endif -#define FatalAssert(cond, str) AlwaysAssert((cond), "CVC3-style assertion failed: %s", std::string(str).c_str()); - //class CInterface; namespace CVC3 { |