diff options
author | Tim King <taking@google.com> | 2015-12-24 05:38:43 -0500 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-12-24 05:38:43 -0500 |
commit | a39ad6584c1d61e22e72b53c3838f4f675ed2e19 (patch) | |
tree | ed40cb371c41ac285ca2bf41a82254a36134e132 /src/compat | |
parent | 87b0fe9ce10d1e5e9ed5a3e7db77f46bf3f68922 (diff) |
Miscellaneous fixes
- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example.
- Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems.
- Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions.
- Changing some headers to use iosfwd when possible.
Diffstat (limited to 'src/compat')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 352 |
1 files changed, 215 insertions, 137 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index d44bae7ee..3fa790f3e 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -18,11 +18,12 @@ #include <algorithm> #include <cassert> -#include <iostream> +#include <iosfwd> #include <iterator> #include <sstream> #include <string> +#include "base/exception.h" #include "base/output.h" #include "expr/kind.h" #include "expr/predicate.h" @@ -43,6 +44,16 @@ using namespace std; +// Matches base/cvc4_assert.h's PrettyCheckArgument. +// base/cvc4_assert.h cannot be directly included. +#define CompatCheckArgument(cond, arg, msg...) \ + do { \ + if(__builtin_expect( ( ! (cond) ), false )) { \ + throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, \ + ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); \ + } \ + } while(0) + #define Unimplemented(str) throw Exception(str) namespace CVC3 { @@ -474,12 +485,12 @@ std::string Expr::getUid() const { } std::string Expr::getString() const { - CVC4::CheckArgument(getKind() == CVC4::kind::CONST_STRING, *this, "CVC3::Expr::getString(): not a string Expr: `%s'", toString().c_str()); + CompatCheckArgument(getKind() == CVC4::kind::CONST_STRING, *this, "CVC3::Expr::getString(): not a string Expr: `%s'", toString().c_str()); return getConst<CVC4::String>().toString(); } std::vector<Expr> Expr::getVars() const { - CVC4::CheckArgument(isClosure(), *this, "CVC3::Expr::getVars(): not a closure Expr: `%s'", toString().c_str()); + CompatCheckArgument(isClosure(), *this, "CVC3::Expr::getVars(): not a closure Expr: `%s'", toString().c_str()); const vector<CVC4::Expr>& kids = (*this)[0].getChildren(); vector<Expr> v; for(vector<CVC4::Expr>::const_iterator i = kids.begin(); i != kids.end(); ++i) { @@ -497,7 +508,7 @@ int Expr::getBoundIndex() const { } Expr Expr::getBody() const { - CVC4::CheckArgument(isClosure(), *this, "CVC3::Expr::getBody(): not a closure Expr: `%s'", toString().c_str()); + CompatCheckArgument(isClosure(), *this, "CVC3::Expr::getBody(): not a closure Expr: `%s'", toString().c_str()); return (*this)[1]; } @@ -546,7 +557,7 @@ bool Expr::isSkolem() const { } const Rational& Expr::getRational() const { - CVC4::CheckArgument(isRational(), *this, "CVC3::Expr::getRational(): not a rational Expr: `%s'", toString().c_str()); + CompatCheckArgument(isRational(), *this, "CVC3::Expr::getRational(): not a rational Expr: `%s'", toString().c_str()); return getConst<CVC4::Rational>(); } @@ -573,7 +584,8 @@ Expr Expr::getExpr() const { } std::vector< std::vector<Expr> > Expr::getTriggers() const { - CVC4::CheckArgument(isClosure(), *this, "getTriggers() called on non-closure expr"); + CompatCheckArgument(isClosure(), *this, + "getTriggers() called on non-closure expr"); if(getNumChildren() < 3) { // no triggers for this quantifier return vector< vector<Expr> >(); @@ -756,37 +768,37 @@ CLFlag& CLFlag::operator=(const CLFlag& f) { } CLFlag& CLFlag::operator=(bool b) { - CVC4::CheckArgument(d_tp == CLFLAG_BOOL, this); + CompatCheckArgument(d_tp == CLFLAG_BOOL, this); d_data.b = b; return *this; } CLFlag& CLFlag::operator=(int i) { - CVC4::CheckArgument(d_tp == CLFLAG_INT, this); + CompatCheckArgument(d_tp == CLFLAG_INT, this); d_data.i = i; return *this; } CLFlag& CLFlag::operator=(const std::string& s) { - CVC4::CheckArgument(d_tp == CLFLAG_STRING, this); + CompatCheckArgument(d_tp == CLFLAG_STRING, this); *d_data.s = s; return *this; } CLFlag& CLFlag::operator=(const char* s) { - CVC4::CheckArgument(d_tp == CLFLAG_STRING, this); + CompatCheckArgument(d_tp == CLFLAG_STRING, this); *d_data.s = s; return *this; } CLFlag& CLFlag::operator=(const std::pair<string, bool>& p) { - CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this); + CompatCheckArgument(d_tp == CLFLAG_STRVEC, this); d_data.sv->push_back(p); return *this; } CLFlag& CLFlag::operator=(const std::vector<std::pair<string, bool> >& sv) { - CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this); + CompatCheckArgument(d_tp == CLFLAG_STRVEC, this); *d_data.sv = sv; return *this; } @@ -804,22 +816,22 @@ bool CLFlag::display() const { } const bool& CLFlag::getBool() const { - CVC4::CheckArgument(d_tp == CLFLAG_BOOL, this); + CompatCheckArgument(d_tp == CLFLAG_BOOL, this); return d_data.b; } const int& CLFlag::getInt() const { - CVC4::CheckArgument(d_tp == CLFLAG_INT, this); + CompatCheckArgument(d_tp == CLFLAG_INT, this); return d_data.i; } const std::string& CLFlag::getString() const { - CVC4::CheckArgument(d_tp == CLFLAG_STRING, this); + CompatCheckArgument(d_tp == CLFLAG_STRING, this); return *d_data.s; } const std::vector<std::pair<string, bool> >& CLFlag::getStrVec() const { - CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this); + CompatCheckArgument(d_tp == CLFLAG_STRVEC, this); return *d_data.sv; } @@ -842,7 +854,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); - CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); return (*i).second; } @@ -852,8 +864,8 @@ 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); - 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, + CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CompatCheckArgument((*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(), @@ -863,38 +875,38 @@ void CLFlags::setFlag(const std::string& name, const CLFlag& f) { void CLFlags::setFlag(const std::string& name, bool b) { FlagMap::iterator i = d_map.find(name); - CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CompatCheckArgument(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); - CVC4::CheckArgument(it != d_map.end(), name, "No command-line flag by that name, or not supported."); + CompatCheckArgument(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); - CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CompatCheckArgument(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); - CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CompatCheckArgument(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); - CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CompatCheckArgument(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); - CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); + CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported."); (*i).second = sv; } @@ -1233,8 +1245,8 @@ Type ValidityChecker::intType() { Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) { bool noLowerBound = l.getType().isString() && l.getConst<CVC4::String>() == "_NEGINF"; bool noUpperBound = r.getType().isString() && r.getConst<CVC4::String>() == "_POSINF"; - 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); + CompatCheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l); + CompatCheckArgument(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)); @@ -1298,7 +1310,7 @@ Type ValidityChecker::recordType(const std::string& field0, const Type& type0, Type ValidityChecker::recordType(const std::vector<std::string>& fields, const std::vector<Type>& types) { - CVC4::CheckArgument(fields.size() == types.size() && fields.size() > 0, + CompatCheckArgument(fields.size() == types.size() && fields.size() > 0, "invalid vector length(s) in recordType()"); std::vector< std::pair<std::string, CVC4::Type> > fieldSpecs; for(unsigned i = 0; i < fields.size(); ++i) { @@ -1311,7 +1323,9 @@ Type ValidityChecker::dataType(const std::string& name, const std::string& constructor, const std::vector<std::string>& selectors, const std::vector<Expr>& types) { - CVC4::CheckArgument(selectors.size() == types.size(), types, "expected selectors and types vectors to be of equal length"); + CompatCheckArgument(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; @@ -1325,8 +1339,12 @@ 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) { - 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"); + CompatCheckArgument(constructors.size() == selectors.size(), selectors, + "Expected constructors and selectors vectors to be of " + "equal length."); + CompatCheckArgument(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; @@ -1347,22 +1365,36 @@ void ValidityChecker::dataType(const std::vector<std::string>& names, const std::vector<std::vector<std::vector<Expr> > >& types, std::vector<Type>& returnTypes) { - 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"); + CompatCheckArgument(names.size() == constructors.size(), constructors, + "Expected names and constructors vectors to be of equal " + "length."); + CompatCheckArgument(names.size() == selectors.size(), selectors, + "Expected names and selectors vectors to be of equal " + "length."); + CompatCheckArgument(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], false); - 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"); + CompatCheckArgument(constructors[i].size() == selectors[i].size(), + "Expected sub-vectors in constructors and selectors " + "vectors to match in size."); + CompatCheckArgument(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]); - CVC4::CheckArgument(selectors[i][j].size() == types[i][j].size(), types, "expected sub-vectors in selectors and types vectors to match in size"); + CompatCheckArgument(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<CVC4::String>().toString())); + CVC4::DatatypeUnresolvedType unresolvedName = + types[i][j][k].getConst<CVC4::String>().toString(); + ctor.addArg(selectors[i][j][k], unresolvedName); } else { ctor.addArg(selectors[i][j][k], exprToType(types[i][j][k])); } @@ -1388,10 +1420,17 @@ 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. - CVC4::CheckArgument(d_constructors.find((*j).getName()) == d_constructors.end(), constructors, "cannot have two constructors with the same name in a ValidityChecker"); + CompatCheckArgument( + 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) { - CVC4::CheckArgument(d_selectors.find((*k).getName()) == d_selectors.end(), selectors, "cannot have two selectors with the same name in a ValidityChecker"); + CompatCheckArgument( + 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()); } } @@ -1407,7 +1446,8 @@ Type ValidityChecker::arrayType(const Type& typeIndex, const Type& typeData) { } Type ValidityChecker::bitvecType(int n) { - CVC4::CheckArgument(n >= 0, n, "cannot construct a bitvector type of negative size"); + CompatCheckArgument(n >= 0, n, + "Cannot construct a bitvector type of negative size."); return d_em->mkBitVectorType(n); } @@ -1444,7 +1484,7 @@ Expr ValidityChecker::varExpr(const std::string& name, const Type& type) { Expr ValidityChecker::varExpr(const std::string& name, const Type& type, const Expr& def) { - CVC4::CheckArgument(def.getType() == type, def, "expected types to match"); + CompatCheckArgument(def.getType() == type, def, "expected types to match"); d_parserContext->defineVar(name, def); return def; } @@ -1595,7 +1635,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 - CVC4::CheckArgument(children.size() > 0, children); + CompatCheckArgument(children.size() > 0, children); return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::AND, *reinterpret_cast<const vector<CVC4::Expr>*>(&children))); } @@ -1605,7 +1645,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 - CVC4::CheckArgument(children.size() > 0, children); + CompatCheckArgument(children.size() > 0, children); return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::OR, *reinterpret_cast<const vector<CVC4::Expr>*>(&children))); } @@ -1627,7 +1667,7 @@ Expr ValidityChecker::iteExpr(const Expr& ifpart, const Expr& thenpart, } Expr ValidityChecker::distinctExpr(const std::vector<Expr>& children) { - CVC4::CheckArgument(children.size() > 1, children, "it makes no sense to create a `distinct' expression with only one child"); + CompatCheckArgument(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); @@ -1639,7 +1679,7 @@ Op ValidityChecker::createOp(const std::string& name, const Type& type) { Op ValidityChecker::createOp(const std::string& name, const Type& type, const Expr& def) { - CVC4::CheckArgument(def.getType() == type, type, + CompatCheckArgument(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()); @@ -1689,7 +1729,7 @@ Expr ValidityChecker::ratExpr(const std::string& n, int base) { if(n.find(".") == string::npos) { return d_em->mkConst(Rational(n, base)); } else { - CVC4::CheckArgument(base == 10, base, "unsupported base for decimal parsing"); + CompatCheckArgument(base == 10, base, "unsupported base for decimal parsing"); return d_em->mkConst(Rational::fromDecimal(n)); } } @@ -1704,7 +1744,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 - CVC4::CheckArgument(children.size() > 0, children); + CompatCheckArgument(children.size() > 0, children); return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::PLUS, *reinterpret_cast<const vector<CVC4::Expr>*>(&children))); } @@ -1806,10 +1846,11 @@ Expr ValidityChecker::newBVConstExpr(const std::vector<bool>& bits) { Expr ValidityChecker::newBVConstExpr(const Rational& r, int len) { // implementation based on CVC3's TheoryBitvector::newBVConstExpr() - CVC4::CheckArgument(r.getDenominator() == 1, r, "ValidityChecker::newBVConstExpr: " - "not an integer: `%s'", r.toString().c_str()); - CVC4::CheckArgument(len > 0, len, "ValidityChecker::newBVConstExpr: " - "len = %d", len); + CompatCheckArgument(r.getDenominator() == 1, r, + "ValidityChecker::newBVConstExpr: " + "not an integer: `%s'", r.toString().c_str()); + CompatCheckArgument(len > 0, len, "ValidityChecker::newBVConstExpr: " + "len = %d", len); string s(r.toString(2)); size_t strsize = s.size(); @@ -1831,8 +1872,8 @@ Expr ValidityChecker::newBVConstExpr(const Rational& r, int len) { } Expr ValidityChecker::newConcatExpr(const Expr& t1, const Expr& t2) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only concat a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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); } @@ -1843,29 +1884,43 @@ Expr ValidityChecker::newConcatExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVExtractExpr(const Expr& e, int hi, int 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); + CompatCheckArgument(e.getType().isBitVector(), e, + "can only bvextract from a bitvector, not a `%s'", + e.getType().toString().c_str()); + CompatCheckArgument(hi >= low, hi, + "extraction [%d:%d] is bad; possibly inverted?", hi, low); + CompatCheckArgument(low >= 0, low, + "extraction [%d:%d] is bad (negative)", hi, low); + CompatCheckArgument(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); + d_em->mkConst(CVC4::BitVectorExtract(hi, low)), e); } Expr ValidityChecker::newBVNegExpr(const Expr& t1) { // CVC3's BVNEG => SMT-LIBv2 bvnot - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvneg a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, + "can only bvand a bitvector, not a `%s'", + t1.getType().toString().c_str()); + CompatCheckArgument(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 - CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_AND must have at least 2 children"); + CompatCheckArgument(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()) { @@ -1875,14 +1930,19 @@ Expr ValidityChecker::newBVAndExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVOrExpr(const Expr& t1, const Expr& t2) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, + "can only bvor a bitvector, not a `%s'", + t1.getType().toString().c_str()); + CompatCheckArgument(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 - CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_OR must have at least 2 children"); + CompatCheckArgument(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()) { @@ -1892,14 +1952,19 @@ Expr ValidityChecker::newBVOrExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVXorExpr(const Expr& t1, const Expr& t2) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, + "can only bvxor a bitvector, not a `%s'", + t1.getType().toString().c_str()); + CompatCheckArgument(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 - CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_XOR must have at least 2 children"); + CompatCheckArgument(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()) { @@ -1909,14 +1974,19 @@ Expr ValidityChecker::newBVXorExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVXnorExpr(const Expr& t1, const Expr& t2) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, + "can only bvxnor a bitvector, not a `%s'", + t1.getType().toString().c_str()); + CompatCheckArgument(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 - CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_XNOR must have at least 2 children"); + CompatCheckArgument(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()) { @@ -1926,73 +1996,81 @@ Expr ValidityChecker::newBVXnorExpr(const std::vector<Expr>& kids) { } Expr ValidityChecker::newBVNandExpr(const Expr& t1, const Expr& t2) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, + "can only bvnand a bitvector, not a `%s'", + t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, + "can only bvnor a bitvector, not a `%s'", + t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvcomp a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvlt a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvle a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvslt a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsle a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only sx a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(len >= 0, len, "must sx by a positive integer"); + CompatCheckArgument(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 - CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvuminus a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsub a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - CVC4::CheckArgument(len >= 0, len, + CompatCheckArgument(len >= 0, len, "padding length must be a non-negative integer, not %d", len); - CVC4::CheckArgument(e.getType().isBitVector(), e, + CompatCheckArgument(e.getType().isBitVector(), e, "input to bitvector operation must be a bitvector"); unsigned size = CVC4::BitVectorType(e.getType()).getSize(); @@ -2011,89 +2089,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 - CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_PLUS must have at least 2 children"); + CompatCheckArgument(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(); - CVC4::CheckArgument(unsigned(numbits) == size, numbits, + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvplus a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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(); - CVC4::CheckArgument(unsigned(numbits) == size, numbits, + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvmult a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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(); - CVC4::CheckArgument(unsigned(numbits) == size, numbits, + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvudiv a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvurem a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsdiv a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsrem a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsmod a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only left-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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. @@ -2101,20 +2179,20 @@ Expr ValidityChecker::newFixedRightShiftExpr(const Expr& t1, int r) { } Expr ValidityChecker::newBVSHL(const Expr& t1, const Expr& t2) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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) { - 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()); + CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str()); + CompatCheckArgument(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); } @@ -2129,30 +2207,30 @@ Expr ValidityChecker::tupleExpr(const std::vector<Expr>& exprs) { } Expr ValidityChecker::tupleSelectExpr(const Expr& tuple, int index) { - CVC4::CheckArgument(index >= 0 && index < tuple.getNumChildren(), + CompatCheckArgument(index >= 0 && index < tuple.getNumChildren(), "invalid index in tuple select"); return d_em->mkExpr(d_em->mkConst(CVC4::TupleSelect(index)), tuple); } Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index, const Expr& newValue) { - CVC4::CheckArgument(index >= 0 && index < tuple.getNumChildren(), + CompatCheckArgument(index >= 0 && index < tuple.getNumChildren(), "invalid index in tuple update"); return d_em->mkExpr(d_em->mkConst(CVC4::TupleUpdate(index)), tuple, newValue); } Expr ValidityChecker::datatypeConsExpr(const std::string& constructor, const std::vector<Expr>& args) { ConstructorMap::const_iterator i = d_constructors.find(constructor); - CVC4::CheckArgument(i != d_constructors.end(), constructor, "no such constructor"); + CompatCheckArgument(i != d_constructors.end(), constructor, "no such constructor"); const CVC4::Datatype& dt = *(*i).second; const CVC4::DatatypeConstructor& ctor = dt[constructor]; - CVC4::CheckArgument(ctor.getNumArgs() == args.size(), args, "arity mismatch in constructor application"); + CompatCheckArgument(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); - CVC4::CheckArgument(i != d_selectors.end(), selector, "no such selector"); + CompatCheckArgument(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]; @@ -2161,7 +2239,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); - CVC4::CheckArgument(i != d_constructors.end(), constructor, "no such constructor"); + CompatCheckArgument(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); @@ -2314,7 +2392,7 @@ void ValidityChecker::returnFromCheck() { } void ValidityChecker::getUserAssumptions(std::vector<Expr>& assumptions) { - CVC4::CheckArgument(assumptions.empty(), assumptions, "assumptions arg must be empty"); + CompatCheckArgument(assumptions.empty(), assumptions, "assumptions arg must be empty"); vector<CVC4::Expr> v = d_smt->getAssertions(); assumptions.swap(*reinterpret_cast<vector<Expr>*>(&v)); } @@ -2349,7 +2427,7 @@ QueryResult ValidityChecker::tryModelGeneration() { } FormulaValue ValidityChecker::value(const Expr& e) { - CVC4::CheckArgument(e.getType() == d_em->booleanType(), e, "argument must be a formula"); + CompatCheckArgument(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) { @@ -2367,7 +2445,7 @@ Expr ValidityChecker::getValue(const Expr& e) { } bool ValidityChecker::inconsistent(std::vector<Expr>& assumptions) { - CVC4::CheckArgument(assumptions.empty(), assumptions, "assumptions vector should be empty on entry"); + CompatCheckArgument(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)); @@ -2427,9 +2505,9 @@ void ValidityChecker::pop() { } void ValidityChecker::popto(int stackLevel) { - CVC4::CheckArgument(stackLevel >= 0, stackLevel, + CompatCheckArgument(stackLevel >= 0, stackLevel, "Cannot pop to a negative stack level %d", stackLevel); - CVC4::CheckArgument(unsigned(stackLevel) <= d_stackLevel, stackLevel, + CompatCheckArgument(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); @@ -2451,9 +2529,9 @@ void ValidityChecker::popScope() { } void ValidityChecker::poptoScope(int scopeLevel) { - CVC4::CheckArgument(scopeLevel >= 0, scopeLevel, + CompatCheckArgument(scopeLevel >= 0, scopeLevel, "Cannot pop to a negative scope level %d", scopeLevel); - CVC4::CheckArgument(unsigned(scopeLevel) <= d_parserContext->scopeLevel(), + CompatCheckArgument(unsigned(scopeLevel) <= d_parserContext->scopeLevel(), scopeLevel, "Cannot pop to a scope level higher than the current one! " "At scope level %u, user requested scope level %d", |