* 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.
doc/cvc4.1_template.in \
doc/cvc4.5.in \
doc/libcvc4.3_template.in \
+ doc/SmtEngine.3cvc4_template.in \
+ doc/options.3cvc4_template.in \
doc/libcvc4parser.3.in \
doc/libcvc4compat.3.in
man_MANS = \
doc/pcvc4.1 \
doc/cvc4.5 \
doc/libcvc4.3 \
+ doc/SmtEngine.3cvc4 \
+ doc/options.3cvc4 \
doc/libcvc4parser.3 \
doc/libcvc4compat.3
CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc4_template])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc4_template])
CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
--- /dev/null
+.\" Process this file with
+.\" groff -man -Tascii SmtEngine.3cvc4
+.\"
+.TH SMTENGINE 3cvc4 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Library Interfaces"
+.SH NAME
+SmtEngine \- the primary interface to CVC4's theorem-proving capabilities
+.SH DESCRIPTION
+.B SmtEngine
+is the main entry point into the CVC4 theorem prover API.
+
+.SH SMTENGINE OPTIONS
+
+The SmtEngine is in charge of setting and getting information and options.
+Numerous options are available via the
+.I SmtEngine::setOption()
+call.
+.I SmtEngine::setOption()
+and
+.I SmtEngine::getOption()
+use the following option keys.
+
+.RS
+.TP 10
+.I "COMMON OPTIONS"
+${common_manpage_smt_documentation}
+
+${remaining_manpage_smt_documentation}
+.PD
+.RE
+
+.SH VERSION
+This manual page refers to
+.B CVC4
+version @VERSION@.
+.SH BUGS
+A Bugzilla for the CVC4 project is maintained at
+.BR http://church.cims.nyu.edu/bugzilla3/ .
+.SH AUTHORS
+.B CVC4
+is developed by a team of researchers at New York University
+and the University of Iowa.
+See the AUTHORS file in the distribution for a full list of
+contributors.
+.SH "SEE ALSO"
+.BR libcvc4 (3),
+.BR libcvc4parser (3),
+.BR libcvc4compat (3)
+
+Additionally, the CVC4 wiki contains useful information about the
+design and internals of CVC4. It is maintained at
+.BR http://church.cims.nyu.edu/wiki/ .
version @VERSION@.
.SH BUGS
A Bugzilla for the CVC4 project is maintained at
-.BR http://goedel.cs.nyu.edu/bugzilla3/ .
+.BR http://church.cims.nyu.edu/bugzilla3/ .
.SH AUTHORS
.B CVC4
is developed by a team of researchers at New York University
Additionally, the CVC4 wiki contains useful information about the
design and internals of CVC4. It is maintained at
-.BR http://goedel.cs.nyu.edu/wiki/ .
+.BR http://church.cims.nyu.edu/wiki/ .
Additionally, the CVC4 wiki contains useful information about the
design and internals of CVC4. It is maintained at
-.BR http://goedel.cs.nyu.edu/wiki/ .
+.BR http://church.cims.nyu.edu/wiki/ .
.I SmtEngine
is used primarily to make assertions, check satisfiability/validity, and extract models and proofs.
-The SmtEngine is also in charge of setting and getting information and options.
-.I SmtEngine::setOption()
-and
-.I SmtEngine::getOption()
-use the following option keys.
-
-.RS
-.TP 10
-.I "COMMON OPTIONS"
-${common_manpage_smt_documentation}
-
-${remaining_manpage_smt_documentation}
-.PD
-.RE
-
.SH "SEE ALSO"
.BR cvc4 (1),
.BR libcvc4parser (3),
Additionally, the CVC4 wiki contains useful information about the
design and internals of CVC4. It is maintained at
-.BR http://goedel.cs.nyu.edu/wiki/ .
+.BR http://church.cims.nyu.edu/wiki/ .
Additionally, the CVC4 wiki contains useful information about the
design and internals of CVC4. It is maintained at
-.BR http://goedel.cs.nyu.edu/wiki/ .
+.BR http://church.cims.nyu.edu/wiki/ .
--- /dev/null
+.\" Process this file with
+.\" groff -man -Tascii options.3cvc4
+.\"
+.TH OPTIONS 3cvc4 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Internals Documentation"
+.SH NAME
+options \- the options infrastructure
+
+.SH AVAILABLE INTERNAL OPTIONS
+
+.RS
+.TP 10
+.I "COMMON OPTIONS"
+${common_manpage_internals_documentation}
+
+${remaining_manpage_internals_documentation}
+.PD
+.RE
+
+.SH VERSION
+This manual page refers to
+.B CVC4
+version @VERSION@.
+.SH BUGS
+A Bugzilla for the CVC4 project is maintained at
+.BR http://church.cims.nyu.edu/bugzilla3/ .
+.SH AUTHORS
+.B CVC4
+is developed by a team of researchers at New York University
+and the University of Iowa.
+See the AUTHORS file in the distribution for a full list of
+contributors.
+.SH "SEE ALSO"
+.BR libcvc4 (3),
+.BR libcvc4parser (3),
+.BR libcvc4compat (3)
+
+Additionally, the CVC4 wiki contains useful information about the
+design and internals of CVC4. It is maintained at
+.BR http://church.cims.nyu.edu/wiki/ .
#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
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;
}
return c.isUnknown();
}
- Unhandled(d);
+ throw Exception("internal error: CVC3 cardinality kind unhandled");
}
bool operator==(CVC3CardinalityKind d, const Cardinality& c) {
}
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> >();
}
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;
}
}
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;
}
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;
}
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;
}
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));
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;
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;
tv.push_back(types);
vector<Type> dtts;
dataType(nv, cv, sv, tv, dtts);
- AlwaysAssert(dtts.size() == 1);
+ assert(dtts.size() == 1);
return dtts[0];
}
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>()));
}
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());
}
}
}
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);
}
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);
}
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();
}
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)));
}
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)));
}
}
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);
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());
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));
}
}
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)));
}
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));
}
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);
}
}
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()) {
}
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()) {
}
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()) {
}
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()) {
}
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();
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.
}
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);
}
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];
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);
}
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));
}
}
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) {
}
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));
}
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();
}
}
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();
}
#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 {
#include <iostream>
#include <sstream>
-#include "util/Assert.h"
+#include "util/exception.h"
namespace CVC4 {
namespace kind {
*/
enum TypeConstant {
${type_constant_list}
+#line 104 "${template}"
LAST_TYPE
};/* enum TypeConstant */
inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
switch(typeConstant) {
${type_constant_descriptions}
+#line 120 "${template}"
default:
out << "UNKNOWN_TYPE_CONSTANT";
break;
enum TheoryId {
${theory_enum}
+#line 132 "${template}"
THEORY_LAST
-};
+};/* enum TheoryId */
const TheoryId THEORY_FIRST = static_cast<TheoryId>(0);
const TheoryId THEORY_SAT_SOLVER = THEORY_LAST;
inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) {
switch(theoryId) {
${theory_descriptions}
+#line 146 "${template}"
default:
out << "UNKNOWN_THEORY";
break;
inline TheoryId kindToTheoryId(::CVC4::Kind k) {
switch(k) {
+ case kind::UNDEFINED_KIND:
+ case kind::NULL_EXPR:
+ break;
${kind_to_theory_id}
- default:
- Unhandled(k);
+#line 160 "${template}"
+ case kind::LAST_KIND:
+ break;
}
+ throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
}
inline TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) {
switch(typeConstant) {
${type_constant_to_theory_id}
- default:
- Unhandled(typeConstant);
+#line 170 "${template}"
+ case LAST_TYPE:
+ break;
}
+ throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant");
}
-}/* theory namespace */
-
-
+}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__KIND_H */
}
void SymbolTable::bind(const std::string& name, Expr obj,
- bool levelZero) throw(AssertionException) {
+ bool levelZero) throw() {
CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
ExprManagerScope ems(obj);
if(levelZero) d_exprMap->insertAtContextLevelZero(name, obj);
}
void SymbolTable::bindDefinedFunction(const std::string& name, Expr obj,
- bool levelZero) throw(AssertionException) {
+ bool levelZero) throw() {
CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
ExprManagerScope ems(obj);
if(levelZero){
return d_functions->contains(func);
}
-Expr SymbolTable::lookup(const std::string& name) const throw(AssertionException) {
+Expr SymbolTable::lookup(const std::string& name) const throw() {
return (*d_exprMap->find(name)).second;
}
return d_typeMap->find(name) != d_typeMap->end();
}
-Type SymbolTable::lookupType(const std::string& name) const throw(AssertionException) {
+Type SymbolTable::lookupType(const std::string& name) const throw() {
pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
Assert(p.first.size() == 0,
"type constructor arity is wrong: "
}
Type SymbolTable::lookupType(const std::string& name,
- const std::vector<Type>& params) const throw(AssertionException) {
+ const std::vector<Type>& params) const throw() {
pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
Assert(p.first.size() == params.size(),
"type constructor arity is wrong: "
* @param obj the expression to bind to <code>name</code>
* @param levelZero set if the binding must be done at level 0
*/
- void bind(const std::string& name, Expr obj, bool levelZero = false) throw(AssertionException);
+ void bind(const std::string& name, Expr obj, bool levelZero = false) throw();
/**
* Bind a function body to a name in the current scope. If
* @param obj the expression to bind to <code>name</code>
* @param levelZero set if the binding must be done at level 0
*/
- void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) throw(AssertionException);
+ void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) throw();
/**
* Bind a type to a name in the current scope. If <code>name</code>
* @param name the identifier to lookup
* @returns the expression bound to <code>name</code> in the current scope.
*/
- Expr lookup(const std::string& name) const throw(AssertionException);
+ Expr lookup(const std::string& name) const throw();
/**
* Lookup a bound type.
* @param name the type identifier to lookup
* @returns the type bound to <code>name</code> in the current scope.
*/
- Type lookupType(const std::string& name) const throw(AssertionException);
+ Type lookupType(const std::string& name) const throw();
/**
* Lookup a bound parameterized type.
* the current scope.
*/
Type lookupType(const std::string& name,
- const std::vector<Type>& params) const throw(AssertionException);
+ const std::vector<Type>& params) const throw();
/**
* Lookup the arity of a bound parameterized type.
#include "expr/node_manager.h"
#include "expr/type.h"
#include "expr/type_node.h"
-#include "util/Assert.h"
+#include "util/exception.h"
using namespace std;
}
Type& Type::operator=(const Type& t) {
- Assert(d_typeNode != NULL, "Unexpected NULL typenode pointer!");
- Assert(t.d_typeNode != NULL, "Unexpected NULL typenode pointer!");
+ CheckArgument(d_typeNode != NULL, this, "Unexpected NULL typenode pointer!");
+ CheckArgument(t.d_typeNode != NULL, t, "Unexpected NULL typenode pointer!");
if(this != &t) {
if(d_nodeManager == t.d_nodeManager) {
}
/** Cast to a Boolean type */
-Type::operator BooleanType() const throw(AssertionException) {
+Type::operator BooleanType() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isBoolean());
+ CheckArgument(isNull() || isBoolean(), this);
return BooleanType(*this);
}
}
/** Cast to a integer type */
-Type::operator IntegerType() const throw(AssertionException) {
+Type::operator IntegerType() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isInteger());
+ CheckArgument(isNull() || isInteger(), this);
return IntegerType(*this);
}
}
/** Cast to a real type */
-Type::operator RealType() const throw(AssertionException) {
+Type::operator RealType() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isReal());
+ CheckArgument(isNull() || isReal(), this);
return RealType(*this);
}
}
/** Cast to a string type */
-Type::operator StringType() const throw(AssertionException) {
+Type::operator StringType() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isString());
+ CheckArgument(isNull() || isString(), this);
return StringType(*this);
}
}
/** Cast to a bit-vector type */
-Type::operator BitVectorType() const throw(AssertionException) {
+Type::operator BitVectorType() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isBitVector());
+ CheckArgument(isNull() || isBitVector(), this);
return BitVectorType(*this);
}
/** Cast to a Constructor type */
-Type::operator DatatypeType() const throw(AssertionException) {
+Type::operator DatatypeType() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isDatatype());
+ CheckArgument(isNull() || isDatatype(), this);
return DatatypeType(*this);
}
}
/** Cast to a Constructor type */
-Type::operator ConstructorType() const throw(AssertionException) {
+Type::operator ConstructorType() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isConstructor());
+ CheckArgument(isNull() || isConstructor(), this);
return ConstructorType(*this);
}
}
/** Cast to a Selector type */
-Type::operator SelectorType() const throw(AssertionException) {
+Type::operator SelectorType() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isSelector());
+ CheckArgument(isNull() || isSelector(), this);
return SelectorType(*this);
}
}
/** Cast to a Tester type */
-Type::operator TesterType() const throw(AssertionException) {
+Type::operator TesterType() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isTester());
+ CheckArgument(isNull() || isTester(), this);
return TesterType(*this);
}
}
/** Cast to a function type */
-Type::operator FunctionType() const throw(AssertionException) {
+Type::operator FunctionType() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isFunction());
+ CheckArgument(isNull() || isFunction(), this);
return FunctionType(*this);
}
}
/** Cast to a tuple type */
-Type::operator TupleType() const throw(AssertionException) {
+Type::operator TupleType() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isTuple());
+ CheckArgument(isNull() || isTuple(), this);
return TupleType(*this);
}
}
/** Cast to a symbolic expression type */
-Type::operator SExprType() const throw(AssertionException) {
+Type::operator SExprType() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isSExpr());
+ CheckArgument(isNull() || isSExpr(), this);
return SExprType(*this);
}
}
/** Cast to an array type */
-Type::operator ArrayType() const throw(AssertionException) {
+Type::operator ArrayType() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
return ArrayType(*this);
}
}
/** Cast to a sort type */
-Type::operator SortType() const throw(AssertionException) {
+Type::operator SortType() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isSort());
+ CheckArgument(isNull() || isSort(), this);
return SortType(*this);
}
}
/** Cast to a sort constructor type */
-Type::operator SortConstructorType() const throw(AssertionException) {
+Type::operator SortConstructorType() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isSortConstructor());
+ CheckArgument(isNull() || isSortConstructor(), this);
return SortConstructorType(*this);
}
}
/** Cast to a predicate subtype */
-Type::operator PredicateSubtype() const throw(AssertionException) {
+Type::operator PredicateSubtype() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isPredicateSubtype());
+ CheckArgument(isNull() || isPredicateSubtype(), this);
return PredicateSubtype(*this);
}
}
/** Cast to a predicate subtype */
-Type::operator SubrangeType() const throw(AssertionException) {
+Type::operator SubrangeType() const throw(IllegalArgumentException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isSubrange());
+ CheckArgument(isNull() || isSubrange(), this);
return SubrangeType(*this);
}
Type FunctionType::getRangeType() const {
NodeManagerScope nms(d_nodeManager);
- Assert(isNull() || isFunction());
+ CheckArgument(isNull() || isFunction(), this);
return makeType(d_typeNode->getRangeType());
}
return SortType(makeType(d_nodeManager->mkSort(*d_typeNode, paramsNodes)));
}
-BooleanType::BooleanType(const Type& t) throw(AssertionException) :
+BooleanType::BooleanType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isBoolean());
+ CheckArgument(isNull() || isBoolean(), this);
}
-IntegerType::IntegerType(const Type& t) throw(AssertionException) :
+IntegerType::IntegerType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isInteger());
+ CheckArgument(isNull() || isInteger(), this);
}
-RealType::RealType(const Type& t) throw(AssertionException) :
+RealType::RealType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isReal());
+ CheckArgument(isNull() || isReal(), this);
}
-StringType::StringType(const Type& t) throw(AssertionException) :
+StringType::StringType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isString());
+ CheckArgument(isNull() || isString(), this);
}
-BitVectorType::BitVectorType(const Type& t) throw(AssertionException) :
+BitVectorType::BitVectorType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isBitVector());
+ CheckArgument(isNull() || isBitVector(), this);
}
-DatatypeType::DatatypeType(const Type& t) throw(AssertionException) :
+DatatypeType::DatatypeType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isDatatype());
+ CheckArgument(isNull() || isDatatype(), this);
}
-ConstructorType::ConstructorType(const Type& t) throw(AssertionException) :
+ConstructorType::ConstructorType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isConstructor());
+ CheckArgument(isNull() || isConstructor(), this);
}
-SelectorType::SelectorType(const Type& t) throw(AssertionException) :
+SelectorType::SelectorType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isSelector());
+ CheckArgument(isNull() || isSelector(), this);
}
-TesterType::TesterType(const Type& t) throw(AssertionException) :
+TesterType::TesterType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isTester());
+ CheckArgument(isNull() || isTester(), this);
}
-FunctionType::FunctionType(const Type& t) throw(AssertionException) :
+FunctionType::FunctionType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isFunction());
+ CheckArgument(isNull() || isFunction(), this);
}
-TupleType::TupleType(const Type& t) throw(AssertionException) :
+TupleType::TupleType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isTuple());
+ CheckArgument(isNull() || isTuple(), this);
}
-SExprType::SExprType(const Type& t) throw(AssertionException) :
+SExprType::SExprType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isSExpr());
+ CheckArgument(isNull() || isSExpr(), this);
}
-ArrayType::ArrayType(const Type& t) throw(AssertionException) :
+ArrayType::ArrayType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isArray());
+ CheckArgument(isNull() || isArray(), this);
}
-SortType::SortType(const Type& t) throw(AssertionException) :
+SortType::SortType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isSort());
+ CheckArgument(isNull() || isSort(), this);
}
SortConstructorType::SortConstructorType(const Type& t)
- throw(AssertionException) :
+ throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isSortConstructor());
+ CheckArgument(isNull() || isSortConstructor(), this);
}
PredicateSubtype::PredicateSubtype(const Type& t)
- throw(AssertionException) :
+ throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isPredicateSubtype());
+ CheckArgument(isNull() || isPredicateSubtype(), this);
}
SubrangeType::SubrangeType(const Type& t)
- throw(AssertionException) :
+ throw(IllegalArgumentException) :
Type(t) {
- Assert(isNull() || isSubrange());
+ CheckArgument(isNull() || isSubrange(), this);
}
unsigned BitVectorType::getSize() const {
const Datatype& DatatypeType::getDatatype() const {
if( d_typeNode->isParametricDatatype() ) {
- Assert( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE );
+ CheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this);
const Datatype& dt = (*d_typeNode)[0].getConst<Datatype>();
return dt;
} else {
#include <limits.h>
#include <stdint.h>
-#include "util/Assert.h"
#include "util/cardinality.h"
#include "util/subrange_bound.h"
class SubrangeType;
class Type;
-/** Strategy for hashing Types */
+/** Hash function for Types */
struct CVC4_PUBLIC TypeHashFunction {
/** Return a hash code for type t */
size_t operator()(const CVC4::Type& t) const;
* Cast this type to a Boolean type
* @return the BooleanType
*/
- operator BooleanType() const throw(AssertionException);
+ operator BooleanType() const throw(IllegalArgumentException);
/**
* Is this the integer type?
* Cast this type to a integer type
* @return the IntegerType
*/
- operator IntegerType() const throw(AssertionException);
+ operator IntegerType() const throw(IllegalArgumentException);
/**
* Is this the real type?
* Cast this type to a real type
* @return the RealType
*/
- operator RealType() const throw(AssertionException);
+ operator RealType() const throw(IllegalArgumentException);
/**
* Is this the string type?
* Cast this type to a string type
* @return the StringType
*/
- operator StringType() const throw(AssertionException);
+ operator StringType() const throw(IllegalArgumentException);
/**
* Is this the bit-vector type?
* Cast this type to a bit-vector type
* @return the BitVectorType
*/
- operator BitVectorType() const throw(AssertionException);
+ operator BitVectorType() const throw(IllegalArgumentException);
/**
* Is this a function type?
* Cast this type to a function type
* @return the FunctionType
*/
- operator FunctionType() const throw(AssertionException);
+ operator FunctionType() const throw(IllegalArgumentException);
/**
* Is this a tuple type?
* Cast this type to a tuple type
* @return the TupleType
*/
- operator TupleType() const throw(AssertionException);
+ operator TupleType() const throw(IllegalArgumentException);
/**
* Is this a symbolic expression type?
* Cast this type to a symbolic expression type
* @return the SExprType
*/
- operator SExprType() const throw(AssertionException);
+ operator SExprType() const throw(IllegalArgumentException);
/**
* Is this an array type?
* Cast this type to an array type
* @return the ArrayType
*/
- operator ArrayType() const throw(AssertionException);
+ operator ArrayType() const throw(IllegalArgumentException);
/**
* Is this a datatype type?
* Cast this type to a datatype type
* @return the DatatypeType
*/
- operator DatatypeType() const throw(AssertionException);
+ operator DatatypeType() const throw(IllegalArgumentException);
/**
* Is this a constructor type?
* Cast this type to a constructor type
* @return the ConstructorType
*/
- operator ConstructorType() const throw(AssertionException);
+ operator ConstructorType() const throw(IllegalArgumentException);
/**
* Is this a selector type?
* Cast this type to a selector type
* @return the SelectorType
*/
- operator SelectorType() const throw(AssertionException);
+ operator SelectorType() const throw(IllegalArgumentException);
/**
* Is this a tester type?
* Cast this type to a tester type
* @return the TesterType
*/
- operator TesterType() const throw(AssertionException);
+ operator TesterType() const throw(IllegalArgumentException);
/**
* Is this a sort kind?
* Cast this type to a sort type
* @return the sort type
*/
- operator SortType() const throw(AssertionException);
+ operator SortType() const throw(IllegalArgumentException);
/**
* Is this a sort constructor kind?
* Cast this type to a sort constructor type
* @return the sort constructor type
*/
- operator SortConstructorType() const throw(AssertionException);
+ operator SortConstructorType() const throw(IllegalArgumentException);
/**
* Is this a predicate subtype?
* Cast this type to a predicate subtype
* @return the predicate subtype
*/
- operator PredicateSubtype() const throw(AssertionException);
+ operator PredicateSubtype() const throw(IllegalArgumentException);
/**
* Is this an integer subrange type?
* Cast this type to an integer subrange type
* @return the integer subrange type
*/
- operator SubrangeType() const throw(AssertionException);
+ operator SubrangeType() const throw(IllegalArgumentException);
/**
* Outputs a string representation of this type to the stream.
public:
/** Construct from the base type */
- BooleanType(const Type& type = Type()) throw(AssertionException);
+ BooleanType(const Type& type = Type()) throw(IllegalArgumentException);
};/* class BooleanType */
/**
public:
/** Construct from the base type */
- IntegerType(const Type& type = Type()) throw(AssertionException);
+ IntegerType(const Type& type = Type()) throw(IllegalArgumentException);
};/* class IntegerType */
/**
public:
/** Construct from the base type */
- RealType(const Type& type = Type()) throw(AssertionException);
+ RealType(const Type& type = Type()) throw(IllegalArgumentException);
};/* class RealType */
/**
public:
/** Construct from the base type */
- StringType(const Type& type) throw(AssertionException);
+ StringType(const Type& type) throw(IllegalArgumentException);
};/* class StringType */
/**
public:
/** Construct from the base type */
- FunctionType(const Type& type = Type()) throw(AssertionException);
+ FunctionType(const Type& type = Type()) throw(IllegalArgumentException);
/** Get the argument types */
std::vector<Type> getArgTypes() const;
public:
/** Construct from the base type */
- TupleType(const Type& type = Type()) throw(AssertionException);
+ TupleType(const Type& type = Type()) throw(IllegalArgumentException);
/** Get the constituent types */
std::vector<Type> getTypes() const;
public:
/** Construct from the base type */
- SExprType(const Type& type = Type()) throw(AssertionException);
+ SExprType(const Type& type = Type()) throw(IllegalArgumentException);
/** Get the constituent types */
std::vector<Type> getTypes() const;
public:
/** Construct from the base type */
- ArrayType(const Type& type = Type()) throw(AssertionException);
+ ArrayType(const Type& type = Type()) throw(IllegalArgumentException);
/** Get the index type */
Type getIndexType() const;
public:
/** Construct from the base type */
- SortType(const Type& type = Type()) throw(AssertionException);
+ SortType(const Type& type = Type()) throw(IllegalArgumentException);
/** Get the name of the sort */
std::string getName() const;
public:
/** Construct from the base type */
- SortConstructorType(const Type& type = Type()) throw(AssertionException);
+ SortConstructorType(const Type& type = Type()) throw(IllegalArgumentException);
/** Get the name of the sort constructor */
std::string getName() const;
public:
/** Construct from the base type */
- PredicateSubtype(const Type& type = Type()) throw(AssertionException);
+ PredicateSubtype(const Type& type = Type()) throw(IllegalArgumentException);
/** Get the LAMBDA defining this predicate subtype */
Expr getPredicate() const;
public:
/** Construct from the base type */
- SubrangeType(const Type& type = Type()) throw(AssertionException);
+ SubrangeType(const Type& type = Type()) throw(IllegalArgumentException);
/** Get the bounds defining this integer subrange */
SubrangeBounds getSubrangeBounds() const;
public:
/** Construct from the base type */
- BitVectorType(const Type& type = Type()) throw(AssertionException);
+ BitVectorType(const Type& type = Type()) throw(IllegalArgumentException);
/**
* Returns the size of the bit-vector type.
public:
/** Construct from the base type */
- DatatypeType(const Type& type = Type()) throw(AssertionException);
+ DatatypeType(const Type& type = Type()) throw(IllegalArgumentException);
/** Get the underlying datatype */
const Datatype& getDatatype() const;
public:
/** Construct from the base type */
- ConstructorType(const Type& type = Type()) throw(AssertionException);
+ ConstructorType(const Type& type = Type()) throw(IllegalArgumentException);
/** Get the range type */
DatatypeType getRangeType() const;
public:
/** Construct from the base type */
- SelectorType(const Type& type = Type()) throw(AssertionException);
+ SelectorType(const Type& type = Type()) throw(IllegalArgumentException);
/** Get the domain type for this selector (the datatype type) */
DatatypeType getDomain() const;
public:
/** Construct from the base type */
- TesterType(const Type& type = Type()) throw(AssertionException);
+ TesterType(const Type& type = Type()) throw(IllegalArgumentException);
/** Get the type that this tester tests (the datatype type) */
DatatypeType getDomain() const;
#include "parser/parser_exception.h"
#include "expr/expr_manager.h"
#include "expr/command.h"
-#include "util/Assert.h"
#include "util/configuration.h"
#include "options/options.h"
#include "main/command_executor.h"
#include "util/language.h"
#include <string.h>
+#include <cassert>
#if HAVE_LIBREADLINE
# include <readline/readline.h>
commandsEnd = tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands);
break;
default:
- Unhandled(lang);
+ std::stringstream ss;
+ ss << "internal error: unhandled language " << lang;
+ throw Exception(ss.str());
}
d_usingReadline = true;
int err = ::read_history(d_historyFilename.c_str());
while(true) {
Debug("interactive") << "Input now '" << input << line << "'" << endl << flush;
- Assert( !(d_in.fail() && !d_in.eof()) || line.empty() );
+ assert( !(d_in.fail() && !d_in.eof()) || line.empty() );
/* Check for failure. */
if(d_in.fail() && !d_in.eof()) {
/* This should only happen if the input line was empty. */
- Assert( line.empty() );
+ assert( line.empty() );
d_in.clear();
}
if(!d_usingReadline) {
/* Extract the newline delimiter from the stream too */
int c CVC4_UNUSED = d_in.get();
- Assert( c == '\n' );
+ assert( c == '\n' );
Debug("interactive") << "Next char is '" << (char)c << "'" << endl << flush;
}
#include "expr/expr_manager.h"
#include "smt/smt_engine.h"
#include "expr/command.h"
-#include "util/Assert.h"
#include "util/configuration.h"
#include "main/options.h"
#include "theory/uf/options.h"
#include <sys/resource.h>
#include <unistd.h>
-#include "util/Assert.h"
#include "util/exception.h"
#include "options/options.h"
#include "util/statistics.h"
+#include "util/tls.h"
#include "smt/smt_engine.h"
#include "cvc4autoconfig.h"
using namespace std;
namespace CVC4 {
+
+#ifdef CVC4_DEBUG
+ extern CVC4_THREADLOCAL(const char*) s_debugLastException;
+#endif /* CVC4_DEBUG */
+
namespace main {
size_t cvc4StackSize;
@srcdir@/../smt/smt_options_template.cpp @builddir@/../smt/smt_options.cpp \
@top_builddir@/doc/cvc4.1_template @top_builddir@/doc/cvc4.1 \
@top_builddir@/doc/libcvc4.3_template @top_builddir@/doc/libcvc4.3 \
+ @top_builddir@/doc/SmtEngine.3cvc4_template @top_builddir@/doc/SmtEngine.3cvc4 \
+ @top_builddir@/doc/options.3cvc4_template @top_builddir@/doc/options.3cvc4 \
-t \
@srcdir@/base_options_template.h @srcdir@/base_options_template.cpp \
$(foreach o,$(OPTIONS_FILES),"$(srcdir)/$(o)" "$(patsubst %/,%,$(dir $(o)))") \
remaining_manpage_documentation=
common_manpage_smt_documentation=
remaining_manpage_smt_documentation=
+common_manpage_internals_documentation=
+remaining_manpage_internals_documentation=
seen_module=false
seen_endmodule=false
expect_doc=false
expect_doc_alternate=false
+seen_doc=false
n_long=256
internal=
remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation}
.TP
.I \"`echo "$module_name" | tr a-z A-Z` OPTIONS\"
+"
+ remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
+.TP
+.I \"`echo "$module_name" | tr a-z A-Z` OPTIONS\"
"
}
expect_doc=true
fi
expect_doc_alternate=false
+ seen_doc=false
# scan ahead to see where the type is
type_pos=2
# doc text...
check_module_seen
expect_doc=false
+ seen_doc=true
if [ -z "$short_option" -a -z "$long_option" ]; then
if [ -n "$short_option_alternate" -o -n "$long_option_alternate" ]; then
fi
fi
- if [ "$category" = UNDOCUMENTED ]; then
- return
- fi
-
the_opt=
if [ "$long_option" ]; then
the_opt="--$long_option"
fi
elif [ "$short_option" ]; then
the_opt="-$short_option"
- elif [ -z "$smtname" ]; then
- # nothing to document
- return
fi
if ! $options_already_documented; then
common_manpage_documentation="${common_manpage_documentation}
.IP \"$the_opt\"
$mandoc"
- else
+ elif [ "$category" != UNDOCUMENTED ]; then
remaining_documentation="${remaining_documentation}\\n\"
#line $lineno \"$kf\"
\"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
fi
fi
- if [ "$smtname" ]; then
+ if [ "$smtname" -a "$category" != UNDOCUMENTED ]; then
if [ "$category" = COMMON ]; then
common_manpage_smt_documentation="${common_manpage_smt_documentation}
.TP
($type) $mansmtdoc"
fi
fi
+ if [ "$internal" != - ]; then
+ if [ -z "$default_value" ]; then
+ typedefault="($type)"
+ else
+ typedefault="($type, default = $default_value)"
+ fi
+ if [ "$category" = COMMON ]; then
+ common_manpage_internals_documentation="${common_manpage_internals_documentation}
+.TP
+.B \"$internal\"
+$typedefault
+.br
+$mansmtdoc"
+ else
+ remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
+.TP
+.B \"$internal\"
+$typedefault
+.br
+$mansmtdoc"
+ fi
+ fi
else
- if [ "$the_opt" ]; then
+ if [ "$the_opt" -a "$category" != UNDOCUMENTED ]; then
if [ "$category" = COMMON ]; then
common_manpage_documentation="${common_manpage_documentation}
$@"
fi
fi
- if [ "$smtname" ]; then
+ if [ "$smtname" -a "$category" != UNDOCUMENTED ]; then
+ if [ "$category" = COMMON ]; then
common_manpage_smt_documentation="${common_manpage_smt_documentation}
$@"
- else
+ else
remaining_manpage_smt_documentation="${remaining_manpage_smt_documentation}
$@"
+ fi
+ fi
+
+ if [ "$internal" != - ]; then
+ if [ "$category" = COMMON ]; then
+ common_manpage_internals_documentation="${common_manpage_internals_documentation}
+$@"
+ else
+ remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
+$@"
+ fi
fi
fi
}
echo "$kf:$lineno: warning: SMT option $smtname is lacking documentation" >&2
fi
expect_doc=false
+ elif ! $seen_doc; then
+ if [ -n "$internal" -a "$internal" != - ]; then
+ if [ -z "$default_value" ]; then
+ typedefault="($type)"
+ else
+ typedefault="($type, default = $default_value)"
+ fi
+ if [ "$category" = COMMON ]; then
+ common_manpage_internals_documentation="${common_manpage_internals_documentation}
+.TP
+.B \"$internal\"
+$typedefault
+.br
+[undocumented]"
+ else
+ remaining_manpage_internals_documentation="${remaining_manpage_internals_documentation}
+.TP
+.B \"$internal\"
+$typedefault
+.br
+[undocumented]"
+ fi
+ fi
fi
if $expect_doc_alternate; then
fi
}
-total=$(($#/2+19*${#templates[@]}))
+total=$(($#/2+21*${#templates[@]}))
count=0
while [ $# -gt 0 ]; do
kf="$1"; shift
remaining_manpage_documentation \
common_manpage_smt_documentation \
remaining_manpage_smt_documentation \
+ common_manpage_internals_documentation \
+ remaining_manpage_internals_documentation \
; do
let ++count
progress "$output" $count $total
#include "parser/smt2/smt2_input.h"
#include "parser/tptp/tptp_input.h"
#include "util/output.h"
-#include "util/Assert.h"
using namespace std;
using namespace CVC4;
bool fileIsTemporary) :
InputStream(name,fileIsTemporary),
d_input(input) {
- AlwaysAssert( input != NULL );
+ assert( input != NULL );
}
AntlrInputStream::~AntlrInputStream() {
AntlrInputStream*
AntlrInputStream::newFileInputStream(const std::string& name,
bool useMmap)
- throw (InputStreamException, AssertionException) {
+ throw (InputStreamException) {
pANTLR3_INPUT_STREAM input = NULL;
if( useMmap ) {
input = MemoryMappedInputBufferNew(name);
AntlrInputStream::newStreamInputStream(std::istream& input,
const std::string& name,
bool lineBuffered)
- throw (InputStreamException, AssertionException) {
+ throw (InputStreamException) {
pANTLR3_INPUT_STREAM inputStream = NULL;
AntlrInputStream*
AntlrInputStream::newStringInputStream(const std::string& input,
const std::string& name)
- throw (InputStreamException, AssertionException) {
+ throw (InputStreamException) {
char* inputStr = strdup(input.c_str());
char* nameStr = strdup(name.c_str());
- AlwaysAssert( inputStr!=NULL && nameStr!=NULL );
+ assert( inputStr!=NULL && nameStr!=NULL );
#ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
pANTLR3_INPUT_STREAM inputStream =
antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8) inputStr,
break;
default:
- Unhandled(lang);
+ std::stringstream ss;
+ ss << "internal error: unhandled language " << lang << " in AntlrInput::newInput";
+ throw ParserException(ss.str());
}
return input;
void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) {
pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super);
- AlwaysAssert(lexer!=NULL);
+ assert(lexer!=NULL);
Parser *parser = (Parser*)(lexer->super);
- AlwaysAssert(parser!=NULL);
+ assert(parser!=NULL);
AntlrInput *input = (AntlrInput*) parser->getInput();
- AlwaysAssert(input!=NULL);
+ assert(input!=NULL);
/* Call the error display routine *if* there's not already a
* parse error pending. If a parser error is pending, this
}
void AntlrInput::parseError(const std::string& message)
- throw (ParserException, AssertionException) {
+ throw (ParserException) {
Debug("parser") << "Throwing exception: "
<< getInputStream()->getName() << ":"
<< d_lexer->getLine(d_lexer) << "."
#include <stdexcept>
#include <string>
#include <vector>
+#include <cassert>
#include "parser/bounded_token_buffer.h"
#include "parser/parser_exception.h"
#include "parser/input.h"
-#include "util/Assert.h"
#include "util/bitvector.h"
#include "util/integer.h"
#include "util/rational.h"
*/
static AntlrInputStream* newFileInputStream(const std::string& name,
bool useMmap = false)
- throw (InputStreamException, AssertionException);
+ throw (InputStreamException);
/** Create an input from an istream. */
static AntlrInputStream* newStreamInputStream(std::istream& input,
const std::string& name,
bool lineBuffered = false)
- throw (InputStreamException, AssertionException);
+ throw (InputStreamException);
/** Create a string input.
*
*/
static AntlrInputStream* newStringInputStream(const std::string& input,
const std::string& name)
- throw (InputStreamException, AssertionException);
+ throw (InputStreamException);
};/* class AntlrInputStream */
class Parser;
* Throws a <code>ParserException</code> with the given message.
*/
void parseError(const std::string& msg)
- throw (ParserException, AssertionException);
+ throw (ParserException);
/** Set the ANTLR3 lexer for this input. */
void setAntlr3Lexer(pANTLR3_LEXER pLexer);
ANTLR3_MARKER start = token->getStartIndex(token);
// Its the last character of the token (not the one just after)
ANTLR3_MARKER end = token->getStopIndex(token);
- Assert( start < end );
+ assert( start < end );
if( index > (size_t) end - start ) {
std::stringstream ss;
ss << "Out-of-bounds substring index: " << index;
#include "parser/antlr_input.h"
#include "parser/parser.h"
#include "parser/parser_exception.h"
-#include "util/Assert.h"
using namespace std;
// Dig the CVC4 objects out of the ANTLR3 mess
pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super);
- AlwaysAssert(antlr3Parser!=NULL);
+ assert(antlr3Parser!=NULL);
Parser *parser = (Parser*)(antlr3Parser->super);
- AlwaysAssert(parser!=NULL);
+ assert(parser!=NULL);
AntlrInput *input = (AntlrInput*) parser->getInput() ;
- AlwaysAssert(input!=NULL);
+ assert(input!=NULL);
// Signal we are in error recovery now
recognizer->state->errorRecovery = ANTLR3_TRUE;
}
}
} else {
- Unreachable("Parse error with empty set of expected tokens.");
+ assert(false);//("Parse error with empty set of expected tokens.");
}
}
break;
// then we are just going to report what we know about the
// token.
//
- Unhandled("Unexpected exception in parser.");
+ assert(false);//("Unexpected exception in parser.");
break;
}
#include <antlr3.h>
#include <iostream>
#include <string>
+#include <cassert>
#include "util/output.h"
-#include "util/Assert.h"
namespace CVC4 {
namespace parser {
in.getline((((char*)input->data) + input->sizeBuf), 1024);
}
input->sizeBuf += strlen(((char*)input->data) + input->sizeBuf);
- Assert(*(((char*)input->data) + input->sizeBuf) == '\0');
+ assert(*(((char*)input->data) + input->sizeBuf) == '\0');
Debug("pipe") << "SIZEBUF now " << input->sizeBuf << std::endl;
*(((char*)input->data) + input->sizeBuf) = '\n';
++input->sizeBuf;
#include <antlr3tokenstream.h>
#include "parser/bounded_token_buffer.h"
-#include "util/Assert.h"
+#include <cassert>
namespace CVC4 {
namespace parser {
pANTLR3_COMMON_TOKEN_STREAM stream;
- AlwaysAssert( k > 0 );
+ assert( k > 0 );
/* Memory for the interface structure
*/
buffer = (pBOUNDED_TOKEN_BUFFER) cts->super;
/* k must be in the range [-buffer->k..buffer->k] */
- AlwaysAssert( k <= (ANTLR3_INT32)buffer->k
+ assert( k <= (ANTLR3_INT32)buffer->k
&& -k <= (ANTLR3_INT32)buffer->k );
if(k == 0) {
/* Initialize the buffer on our first call. */
if( EXPECT_FALSE(buffer->empty == ANTLR3_TRUE) ) {
- AlwaysAssert( buffer->tokenBuffer != NULL );
+ assert( buffer->tokenBuffer != NULL );
buffer->tokenBuffer[ 0 ] = nextToken(buffer);
buffer->maxIndex = 0;
buffer->currentIndex = 0;
kIndex = buffer->currentIndex + k - 1;
} else {
/* Can't look behind more tokens than we've consumed. */
- AlwaysAssert( -k <= (ANTLR3_INT32)buffer->currentIndex );
+ assert( -k <= (ANTLR3_INT32)buffer->currentIndex );
/* look-behind token k is at offset -k */
kIndex = buffer->currentIndex + k;
}
static pANTLR3_COMMON_TOKEN
get (pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 i)
{
- Unreachable();
+ assert(false);// unimplemented
+ return NULL;
}
static pANTLR3_TOKEN_SOURCE
static pANTLR3_STRING
toString (pANTLR3_TOKEN_STREAM ts)
{
- Unimplemented("toString(ts)");
+ assert(false);// unimplemented
+ return NULL;
}
static pANTLR3_STRING
toStringSS(pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 start, ANTLR3_UINT32 stop)
{
- Unimplemented("toStringSS(ts, %u, %u)", start, stop);
+ assert(false);// unimplemented
+ return NULL;
}
static pANTLR3_STRING
toStringTT (pANTLR3_TOKEN_STREAM ts, pANTLR3_COMMON_TOKEN start, pANTLR3_COMMON_TOKEN stop)
{
- Unimplemented("toStringTT(ts, %u, %u)", start, stop);
+ assert(false);// unimplemented
+ return NULL;
}
/** Move the input pointer to the next incoming token. The stream
static ANTLR3_UINT32
dbgLA (pANTLR3_INT_STREAM is, ANTLR3_INT32 i)
{
- Unreachable();
+ assert(false);
+ return 0;
}
static ANTLR3_MARKER
static ANTLR3_MARKER
dbgMark (pANTLR3_INT_STREAM is)
{
- Unreachable();
+ assert(false);
+ return 0;
}
static void
static ANTLR3_UINT32
size (pANTLR3_INT_STREAM is)
{
- Unreachable();
+ assert(false);
+ return 0;
}
static ANTLR3_MARKER
static void
dbgRewindLast (pANTLR3_INT_STREAM is)
{
- Unreachable();
+ assert(false);
}
static void
rewindLast (pANTLR3_INT_STREAM is)
{
- Unreachable();
+ assert(false);
}
static void
rewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker)
static void
dbgRewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker)
{
- Unreachable();
+ assert(false);
}
static void
static void
dbgSeek (pANTLR3_INT_STREAM is, ANTLR3_MARKER index)
{
- Unreachable();
+ assert(false);
}
static pANTLR3_COMMON_TOKEN nextToken(pBOUNDED_TOKEN_BUFFER buffer) {
case IN_TOK: return 33;
default:
- Unhandled(CvcParserTokenNames[type]);
+ std::stringstream ss;
+ ss << "internal error: no entry in precedence table for operator " << CvcParserTokenNames[type];
+ throw ParserException(ss.str());
}
}/* getOperatorPrecedence() */
case INTDIV_TOK: return kind::INTS_DIVISION;
case MOD_TOK: return kind::INTS_MODULUS;
case DIV_TOK: return kind::DIVISION;
- case EXP_TOK: Unhandled(CvcParserTokenNames[type]);
+ case EXP_TOK: break;
// bvBinop
case CONCAT_TOK: return kind::BITVECTOR_CONCAT;
case BAR: return kind::BITVECTOR_OR;
case BVAND_TOK: return kind::BITVECTOR_AND;
-
- default:
- Unhandled(CvcParserTokenNames[type]);
}
+
+ std::stringstream ss;
+ ss << "internal error: no entry in operator-kind table for operator " << CvcParserTokenNames[type];
+ throw ParserException(ss.str());
+
}/* getOperatorKind() */
unsigned findPivot(const std::vector<unsigned>& operators,
const std::vector<CVC4::Expr>& expressions,
const std::vector<unsigned>& operators,
unsigned startIndex, unsigned stopIndex) {
- Assert(expressions.size() == operators.size() + 1);
- Assert(startIndex < expressions.size());
- Assert(stopIndex < expressions.size());
- Assert(startIndex <= stopIndex);
+ assert(expressions.size() == operators.size() + 1);
+ assert(startIndex < expressions.size());
+ assert(stopIndex < expressions.size());
+ assert(startIndex <= stopIndex);
if(stopIndex == startIndex) {
return expressions[startIndex];
@parser::includes {
#include <stdint.h>
+#include <cassert>
#include "expr/command.h"
#include "parser/parser.h"
#include "util/subrange_bound.h"
/* a type, possibly a function */
: restrictedTypePossiblyFunctionLHS[t,check,lhs]
{ if(lhs) {
- Assert(t.isTuple());
+ assert(t.isTuple());
args = TupleType(t).getTypes();
} else {
args.push_back(t);
}
: ( LBRACKET formula[f2] { dims.push_back(f2); } RBRACKET )+
ASSIGN_TOK uminusTerm[f3]
- { Assert(dims.size() >= 1);
+ { assert(dims.size() >= 1);
// these loops are a bit complicated; they're only used for the
// multidimensional ...WITH [a][b] :=... syntax
for(unsigned i = 0; i < dims.size() - 1; ++i) {
} else if(t.isTester()) {
f = MK_EXPR(CVC4::kind::APPLY_TESTER, args);
} else {
- Unhandled(t);
+ PARSER_STATE->parseError("internal error: unhandled function application kind");
}
}
| INTEGER_LITERAL { f = MK_CONST(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
/* bitvector literals */
| HEX_LITERAL
- { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 );
+ { assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 );
std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4);
f = MK_CONST( BitVector(hexString, 16) ); }
| BINARY_LITERAL
- { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 );
+ { assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 );
std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4);
f = MK_CONST( BitVector(binString, 2) ); }
/* record literals */
| PARENHASH recordEntry[name,e] { names.push_back(name); args.push_back(e); }
( COMMA recordEntry[name,e] { names.push_back(name); args.push_back(e); } )* HASHPAREN
{ std::vector< std::pair<std::string, Type> > typeIds;
- Assert(names.size() == args.size());
+ assert(names.size() == args.size());
for(unsigned i = 0; i < names.size(); ++i) {
typeIds.push_back(std::make_pair(names[i], args[i].getType()));
}
CvcInput::CvcInput(AntlrInputStream& inputStream) :
AntlrInput(inputStream,6) {
pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
- AlwaysAssert( input != NULL );
+ assert( input != NULL );
d_pCvcLexer = CvcLexerNew(input);
if( d_pCvcLexer == NULL ) {
setAntlr3Lexer( d_pCvcLexer->pLexer );
pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
- AlwaysAssert( tokenStream != NULL );
+ assert( tokenStream != NULL );
d_pCvcParser = CvcParserNew(tokenStream);
if( d_pCvcParser == NULL ) {
}
Command* CvcInput::parseCommand()
- throw (ParserException, TypeCheckingException, AssertionException) {
+ throw (ParserException, TypeCheckingException) {
return d_pCvcParser->parseCommand(d_pCvcParser);
}
Expr CvcInput::parseExpr()
- throw (ParserException, TypeCheckingException, AssertionException) {
+ throw (ParserException, TypeCheckingException) {
return d_pCvcParser->parseExpr(d_pCvcParser);
}
* @throws ParserException if an error is encountered during parsing.
*/
Command* parseCommand()
- throw(ParserException, TypeCheckingException, AssertionException);
+ throw(ParserException, TypeCheckingException);
/** Parse an expression from the input. Returns a null <code>Expr</code>
* if there is no expression there to parse.
* @throws ParserException if an error is encountered during parsing.
*/
Expr parseExpr()
- throw(ParserException, TypeCheckingException, AssertionException);
+ throw(ParserException, TypeCheckingException);
private:
#include "expr/type.h"
#include "parser/antlr_input.h"
#include "util/output.h"
-#include "util/Assert.h"
using namespace std;
using namespace CVC4;
Input* Input::newFileInput(InputLanguage lang,
const std::string& filename,
bool useMmap)
- throw (InputStreamException, AssertionException) {
+ throw (InputStreamException) {
AntlrInputStream *inputStream =
AntlrInputStream::newFileInputStream(filename, useMmap);
return AntlrInput::newInput(lang, *inputStream);
std::istream& input,
const std::string& name,
bool lineBuffered)
- throw (InputStreamException, AssertionException) {
+ throw (InputStreamException) {
AntlrInputStream *inputStream =
AntlrInputStream::newStreamInputStream(input, name, lineBuffered);
return AntlrInput::newInput(lang, *inputStream);
Input* Input::newStringInput(InputLanguage lang,
const std::string& str,
const std::string& name)
- throw (InputStreamException, AssertionException) {
+ throw (InputStreamException) {
AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str, name);
return AntlrInput::newInput(lang, *inputStream);
}
#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "parser/parser_exception.h"
-#include "util/Assert.h"
#include "util/language.h"
namespace CVC4 {
static Input* newFileInput(InputLanguage lang,
const std::string& filename,
bool useMmap = false)
- throw (InputStreamException, AssertionException);
+ throw (InputStreamException);
/** Create an input for the given stream.
*
std::istream& input,
const std::string& name,
bool lineBuffered = false)
- throw (InputStreamException, AssertionException);
+ throw (InputStreamException);
/** Create an input for the given string
*
static Input* newStringInput(InputLanguage lang,
const std::string& input,
const std::string& name)
- throw (InputStreamException, AssertionException);
+ throw (InputStreamException);
/** Destructor. Frees the input stream and closes the input. */
* @throws ParserException if an error is encountered during parsing.
*/
virtual Command* parseCommand()
- throw (ParserException, TypeCheckingException, AssertionException) = 0;
+ throw (ParserException, TypeCheckingException) = 0;
/**
* Issue a warning to the user, with source file, line, and column info.
* Throws a <code>ParserException</code> with the given message.
*/
virtual void parseError(const std::string& msg)
- throw (ParserException, AssertionException) = 0;
+ throw (ParserException) = 0;
/** Parse an expression from the input by invoking the
* implementation-specific parsing method. Returns a null
* @throws ParserException if an error is encountered during parsing.
*/
virtual Expr parseExpr()
- throw (ParserException, TypeCheckingException, AssertionException) = 0;
+ throw (ParserException, TypeCheckingException) = 0;
/** Set the Parser object for this input. */
virtual void setParser(Parser& parser) = 0;
#include <antlr3input.h>
#include "parser/memory_mapped_input_buffer.h"
-#include "util/Assert.h"
#include "util/exception.h"
namespace CVC4 {
#include <fstream>
#include <iterator>
#include <stdint.h>
+#include <cassert>
#include "parser/input.h"
#include "parser/parser.h"
#include "expr/type.h"
#include "util/output.h"
#include "options/options.h"
-#include "util/Assert.h"
using namespace std;
using namespace CVC4::kind;
Expr Parser::getSymbol(const std::string& name, SymbolType type) {
checkDeclaration(name, CHECK_DECLARED, type);
- Assert( isDeclared(name, type) );
+ assert( isDeclared(name, type) );
- switch( type ) {
-
- case SYM_VARIABLE: // Functions share var namespace
+ if(type == SYM_VARIABLE) {
+ // Functions share var namespace
return d_symtab->lookup(name);
-
- default:
- Unhandled(type);
}
+
+ assert(false);//Unhandled(type);
+ return Expr();
}
Type Parser::getType(const std::string& var_name,
SymbolType type) {
checkDeclaration(var_name, CHECK_DECLARED, type);
- Assert( isDeclared(var_name, type) );
+ assert( isDeclared(var_name, type) );
Type t = getSymbol(var_name, type).getType();
return t;
}
Type Parser::getSort(const std::string& name) {
checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
- Assert( isDeclared(name, SYM_SORT) );
+ assert( isDeclared(name, SYM_SORT) );
Type t = d_symtab->lookupType(name);
return t;
}
Type Parser::getSort(const std::string& name,
const std::vector<Type>& params) {
checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
- Assert( isDeclared(name, SYM_SORT) );
+ assert( isDeclared(name, SYM_SORT) );
Type t = d_symtab->lookupType(name, params);
return t;
}
size_t Parser::getArity(const std::string& sort_name){
checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT);
- Assert( isDeclared(sort_name, SYM_SORT) );
+ assert( isDeclared(sort_name, SYM_SORT) );
return d_symtab->lookupArity(sort_name);
}
bool levelZero) {
Debug("parser") << "defineVar( " << name << " := " << val << " , " << levelZero << ")" << std::endl;;
d_symtab->bind(name, val, levelZero);
- Assert( isDeclared(name) );
+ assert( isDeclared(name) );
}
void
Parser::defineFunction(const std::string& name, const Expr& val,
bool levelZero) {
d_symtab->bindDefinedFunction(name, val, levelZero);
- Assert( isDeclared(name) );
+ assert( isDeclared(name) );
}
void
Parser::defineType(const std::string& name, const Type& type) {
d_symtab->bindType(name, type);
- Assert( isDeclared(name, SYM_SORT) );
+ assert( isDeclared(name, SYM_SORT) );
}
void
const std::vector<Type>& params,
const Type& type) {
d_symtab->bindType(name, params, type);
- Assert( isDeclared(name, SYM_SORT) );
+ assert( isDeclared(name, SYM_SORT) );
}
void
std::vector<DatatypeType> types =
d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
- Assert(datatypes.size() == types.size());
+ assert(datatypes.size() == types.size());
for(unsigned i = 0; i < datatypes.size(); ++i) {
DatatypeType t = types[i];
return d_symtab->isBound(name);
case SYM_SORT:
return d_symtab->isBoundType(name);
- default:
- Unhandled(type);
}
+ assert(false);//Unhandled(type);
+ return false;
}
void Parser::checkDeclaration(const std::string& varName,
break;
default:
- Unhandled(check);
+ assert(false);//Unhandled(check);
}
}
#include <string>
#include <set>
#include <list>
+#include <cassert>
#include "parser/input.h"
#include "parser/parser_exception.h"
}
Parser* ParserBuilder::build()
- throw (InputStreamException, AssertionException) {
+ throw (InputStreamException) {
Input* input = NULL;
switch( d_inputType ) {
case FILE_INPUT:
input = Input::newFileInput(d_lang, d_filename, d_mmap);
break;
case LINE_BUFFERED_STREAM_INPUT:
- AlwaysAssert( d_streamInput != NULL,
- "Uninitialized stream input in ParserBuilder::build()" );
+ assert( d_streamInput != NULL );
input = Input::newStreamInput(d_lang, *d_streamInput, d_filename, true);
break;
case STREAM_INPUT:
- AlwaysAssert( d_streamInput != NULL,
- "Uninitialized stream input in ParserBuilder::build()" );
+ assert( d_streamInput != NULL );
input = Input::newStreamInput(d_lang, *d_streamInput, d_filename);
break;
case STRING_INPUT:
input = Input::newStringInput(d_lang, d_stringInput, d_filename);
break;
- default:
- Unreachable();
}
+ assert(input != NULL);
+
Parser* parser = NULL;
switch(d_lang) {
case language::input::LANG_SMTLIB_V1:
const Options& options);
/** Build the parser, using the current settings. */
- Parser *build() throw (InputStreamException, AssertionException);
+ Parser *build() throw (InputStreamException);
/** Should semantic checks be enabled in the parser? (Default: yes) */
ParserBuilder& withChecks(bool flag = true);
{ if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
/* Unary AND/OR can be replaced with the argument.
It just so happens expr should already by the only argument. */
- Assert( expr == args[0] );
+ assert( expr == args[0] );
} else if( CVC4::kind::isAssociative(kind) &&
args.size() > EXPR_MANAGER->maxArity(kind) ) {
/* Special treatment for associative operators with lots of children */
{ sorts.push_back(t); }
sortList[sorts] RPAREN_TOK
{ if( sorts.size() == 1 ) {
- Assert( t == sorts[0] );
+ assert( t == sorts[0] );
} else {
t = EXPR_MANAGER->mkFunctionType(sorts);
}
: attribute[key]
( USER_VALUE
{ std::string value = AntlrInput::tokenText($USER_VALUE);
- Assert(*value.begin() == '{');
- Assert(*value.rbegin() == '}');
+ assert(*value.begin() == '{');
+ assert(*value.rbegin() == '}');
// trim whitespace
value.erase(value.begin(), value.begin() + 1);
value.erase(value.begin(), std::find_if(value.begin(), value.end(), std::not1(std::ptr_fun<int, int>(std::isspace))));
}
case THEORY_BITVECTOR_ARRAYS_EX: {
- Unimplemented("Cannot yet handle SMT-LIBv1 bitvector arrays (i.e., the BitVector_ArraysEx theory)");
- //addOperator(kind::SELECT);
- //addOperator(kind::STORE);
+ // We don't define the "Array" symbol in this case;
+ // the parser creates the Array[m:n] types on the fly.
+ addOperator(kind::SELECT);
+ addOperator(kind::STORE);
break;
}
case THEORY_INT_ARRAYS:
case THEORY_INT_ARRAYS_EX: {
defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType()));
-
addOperator(kind::SELECT);
addOperator(kind::STORE);
break;
break;
default:
- Unhandled(theory);
+ std::stringstream ss;
+ ss << "internal error: unsupported theory " << theory;
+ throw ParserException(ss.str());
}
}
addTheory(THEORY_BITVECTORS);
break;
- case QF_ABV:
- addTheory(THEORY_ARRAYS_EX);
+ case QF_ABV:// nonstandard logic
+ addTheory(THEORY_BITVECTOR_ARRAYS_EX);
addTheory(THEORY_BITVECTORS);
break;
case QF_AUFBV:
addOperator(kind::APPLY_UF);
- addTheory(THEORY_ARRAYS_EX);
+ addTheory(THEORY_BITVECTOR_ARRAYS_EX);
addTheory(THEORY_BITVECTORS);
break;
- case QF_AUFBVLIA:
+ case QF_AUFBVLIA:// nonstandard logic
addOperator(kind::APPLY_UF);
addTheory(THEORY_ARRAYS_EX);
addTheory(THEORY_BITVECTORS);
addTheory(THEORY_INTS);
break;
- case QF_AUFBVLRA:
+ case QF_AUFBVLRA:// nonstandard logic
addOperator(kind::APPLY_UF);
addTheory(THEORY_ARRAYS_EX);
addTheory(THEORY_BITVECTORS);
break;
case QF_AUFLIA:
- addTheory(THEORY_INT_ARRAYS_EX);
+ addTheory(THEORY_INT_ARRAYS_EX);// nonstandard logic
addOperator(kind::APPLY_UF);
addTheory(THEORY_INTS);
break;
- case QF_AUFLIRA:
+ case QF_AUFLIRA:// nonstandard logic
addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
addOperator(kind::APPLY_UF);
addTheory(THEORY_INTS);
addTheory(THEORY_REALS);
break;
- case ALL_SUPPORTED:
+ case ALL_SUPPORTED:// nonstandard logic
addTheory(THEORY_QUANTIFIERS);
/* fall through */
- case QF_ALL_SUPPORTED:
+ case QF_ALL_SUPPORTED:// nonstandard logic
addTheory(THEORY_ARRAYS_EX);
addOperator(kind::APPLY_UF);
addTheory(THEORY_INTS);
Smt1Input::Smt1Input(AntlrInputStream& inputStream) :
AntlrInput(inputStream, 2) {
pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
- AlwaysAssert( input != NULL );
+ assert( input != NULL );
d_pSmt1Lexer = Smt1LexerNew(input);
if( d_pSmt1Lexer == NULL ) {
setAntlr3Lexer( d_pSmt1Lexer->pLexer );
pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
- AlwaysAssert( tokenStream != NULL );
+ assert( tokenStream != NULL );
d_pSmt1Parser = Smt1ParserNew(tokenStream);
if( d_pSmt1Parser == NULL ) {
}
Command* Smt1Input::parseCommand()
- throw (ParserException, TypeCheckingException, AssertionException) {
+ throw (ParserException, TypeCheckingException) {
return d_pSmt1Parser->parseCommand(d_pSmt1Parser);
}
Expr Smt1Input::parseExpr()
- throw (ParserException, TypeCheckingException, AssertionException) {
+ throw (ParserException, TypeCheckingException) {
return d_pSmt1Parser->parseExpr(d_pSmt1Parser);
}
* @throws ParserException if an error is encountered during parsing.
*/
Command* parseCommand()
- throw(ParserException, TypeCheckingException, AssertionException);
+ throw(ParserException, TypeCheckingException);
/**
* Parse an expression from the input. Returns a null
* @throws ParserException if an error is encountered during parsing.
*/
Expr parseExpr()
- throw(ParserException, TypeCheckingException, AssertionException);
+ throw(ParserException, TypeCheckingException);
private:
args.size() == 1) {
/* Unary AND/OR can be replaced with the argument.
It just so happens expr should already by the only argument. */
- Assert( expr == args[0] );
+ assert( expr == args[0] );
} else if( CVC4::kind::isAssociative(kind) &&
args.size() > EXPR_MANAGER->maxArity(kind) ) {
/* Special treatment for associative operators with lots of children */
}
| HEX_LITERAL
- { Assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
+ { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
expr = MK_CONST( BitVector(hexString, 16) ); }
| BINARY_LITERAL
- { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
+ { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
expr = MK_CONST( BitVector(binString, 2) ); }
}
t = EXPR_MANAGER->mkBitVectorType(numerals.front());
} else {
- Unhandled(name);
+ std::stringstream ss;
+ ss << "unknown indexed symbol `" << name << "'";
+ PARSER_STATE->parseError(ss.str());
}
}
| LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK
break;
default:
- Unhandled(theory);
+ std::stringstream ss;
+ ss << "internal error: unsupported theory " << theory;
+ throw ParserException(ss.str());
}
}
Smt2Input::Smt2Input(AntlrInputStream& inputStream) :
AntlrInput(inputStream, 2) {
pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
- AlwaysAssert( input != NULL );
+ assert( input != NULL );
d_pSmt2Lexer = Smt2LexerNew(input);
if( d_pSmt2Lexer == NULL ) {
setAntlr3Lexer( d_pSmt2Lexer->pLexer );
pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
- AlwaysAssert( tokenStream != NULL );
+ assert( tokenStream != NULL );
d_pSmt2Parser = Smt2ParserNew(tokenStream);
if( d_pSmt2Parser == NULL ) {
}
Command* Smt2Input::parseCommand()
- throw (ParserException, TypeCheckingException, AssertionException) {
+ throw (ParserException, TypeCheckingException) {
return d_pSmt2Parser->parseCommand(d_pSmt2Parser);
}
Expr Smt2Input::parseExpr()
- throw (ParserException, TypeCheckingException, AssertionException) {
+ throw (ParserException, TypeCheckingException) {
return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
}
* @throws ParserException if an error is encountered during parsing.
*/
Command* parseCommand()
- throw(ParserException, TypeCheckingException, AssertionException);
+ throw(ParserException, TypeCheckingException);
/**
* Parse an expression from the input. Returns a null
* @throws ParserException if an error is encountered during parsing.
*/
Expr parseExpr()
- throw(ParserException, TypeCheckingException, AssertionException);
+ throw(ParserException, TypeCheckingException);
};/* class Smt2Input */
break;
default:
- Unhandled(theory);
+ std::stringstream ss;
+ ss << "internal error: Tptp::addTheory(): unhandled theory " << theory;
+ throw ParserException(ss.str());
}
}
#include "parser/parser.h"
#include "expr/command.h"
#include <ext/hash_set>
+#include <cassert>
namespace CVC4 {
public:
bool cnf; //in a cnf formula
- void addFreeVar(Expr var){Assert(cnf); d_freeVar.push_back(var); };
+ void addFreeVar(Expr var){assert(cnf); d_freeVar.push_back(var); };
std::vector< Expr > getFreeVar(){
- Assert(cnf);
+ assert(cnf);
std::vector< Expr > r;
r.swap(d_freeVar);
return r;
case FR_PLAIN:
// it's a usual assert
return new AssertCommand(expr);
- break;
case FR_CONJECTURE:
// something to prove
return new AssertCommand(getExprManager()->mkExpr(kind::NOT,expr));
- break;
case FR_UNKNOWN:
case FR_FI_DOMAIN:
case FR_FI_FUNCTORS:
case FR_FI_PREDICATES:
case FR_TYPE:
return new EmptyCommand("Untreated role");
- break;
- default:
- Unreachable("fr",fr);
- };
-};
+ }
+ assert(false);// unreachable
+ return NULL;
+}
namespace tptp {
/**
TptpInput::TptpInput(AntlrInputStream& inputStream) :
AntlrInput(inputStream, 1) {
pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
- AlwaysAssert( input != NULL );
+ assert( input != NULL );
d_pTptpLexer = TptpLexerNew(input);
if( d_pTptpLexer == NULL ) {
setAntlr3Lexer( d_pTptpLexer->pLexer );
pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
- AlwaysAssert( tokenStream != NULL );
+ assert( tokenStream != NULL );
d_pTptpParser = TptpParserNew(tokenStream);
if( d_pTptpParser == NULL ) {
}
Command* TptpInput::parseCommand()
- throw (ParserException, TypeCheckingException, AssertionException) {
+ throw (ParserException, TypeCheckingException) {
return d_pTptpParser->parseCommand(d_pTptpParser);
}
Expr TptpInput::parseExpr()
- throw (ParserException, TypeCheckingException, AssertionException) {
+ throw (ParserException, TypeCheckingException) {
return d_pTptpParser->parseExpr(d_pTptpParser);
}
* @throws ParserException if an error is encountered during parsing.
*/
Command* parseCommand()
- throw(ParserException, TypeCheckingException, AssertionException);
+ throw(ParserException, TypeCheckingException);
/**
* Parse an expression from the input. Returns a null
* @throws ParserException if an error is encountered during parsing.
*/
Expr parseExpr()
- throw(ParserException, TypeCheckingException, AssertionException);
+ throw(ParserException, TypeCheckingException);
};/* class TptpInput */
d_substNodes() {
// 0 doesn't make sense
- CheckArgument(threshold > 0, threshold);
+ AlwaysAssertArgument(threshold > 0, threshold);
}
DagificationVisitor::~DagificationVisitor() {
return;
}
- CheckArgument(n.getType().isBoolean(), n,
- "CnfStream::ensureLiteral() requires a node of Boolean type.\n"
- "got node: %s\n"
- "its type: %s\n",
- n.toString().c_str(),
- n.getType().toString().c_str());
+ AlwaysAssertArgument(n.getType().isBoolean(), n,
+ "CnfStream::ensureLiteral() requires a node of Boolean type.\n"
+ "got node: %s\n"
+ "its type: %s\n",
+ n.toString().c_str(),
+ n.getType().toString().c_str());
bool negated CVC4_UNUSED = false;
SatLiteral lit;
option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "util/lemma_output_channel.h"
The output channel to receive notfication events for new lemmas
+option optionWithOnlyAlternate /--optionWithOnlyAlternate bool
+ option with only an alternate
+
endmodule
* to be in that type.
*/
void constrainSubtypes(TNode n, std::vector<Node>& assertions)
- throw(AssertionException);
+ throw();
/**
* Perform non-clausal simplification of a Node. This involves
*
* Returns false if the formula simplifies to "false"
*/
- bool simplifyAssertions() throw(TypeCheckingException, AssertionException);
+ bool simplifyAssertions() throw(TypeCheckingException);
public:
* even be simplified.
*/
void addFormula(TNode n)
- throw(TypeCheckingException, AssertionException);
+ throw(TypeCheckingException);
/**
* Expand definitions in n.
*/
Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache)
- throw(TypeCheckingException, AssertionException);
+ throw(TypeCheckingException);
};/* class SmtEnginePrivate */
using namespace CVC4::smt;
-SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
+SmtEngine::SmtEngine(ExprManager* em) throw() :
d_context(em->getContext()),
d_userLevels(),
d_userContext(new UserContext()),
// tempt people in the code to use the (potentially unlocked)
// version that's passed in, leading to assert-fails in certain
// uses of the CVC4 library.
-void SmtEngine::setLogicInternal() throw(AssertionException) {
+void SmtEngine::setLogicInternal() throw() {
Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already finished initializing for this run");
d_logic.lock();
}
Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache)
- throw(TypeCheckingException, AssertionException) {
+ throw(TypeCheckingException) {
if(n.getKind() != kind::APPLY && n.getNumChildren() == 0) {
// don't bother putting in the cache
void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertions)
- throw(AssertionException) {
+ throw() {
Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl;
// returns false if simpflication led to "false"
bool SmtEnginePrivate::simplifyAssertions()
- throw(TypeCheckingException, AssertionException) {
+ throw(TypeCheckingException) {
Assert(d_smt.d_pendingPops == 0);
try {
}
void SmtEnginePrivate::addFormula(TNode n)
- throw(TypeCheckingException, AssertionException) {
+ throw(TypeCheckingException) {
Trace("smt") << "SmtEnginePrivate::addFormula(" << n << ")" << endl;
}
Expr SmtEngine::getValue(const Expr& e)
- throw(ModalException, AssertionException) {
+ throw(ModalException) {
Assert(e.getExprManager() == d_exprManager);
SmtScope smts(this);
return Expr(d_exprManager, new Node(resultNode));
}
-bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
+bool SmtEngine::addToAssignment(const Expr& e) throw() {
SmtScope smts(this);
finalOptionsAreSet();
doPendingPops();
return true;
}
-CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
+CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) {
Trace("smt") << "SMT getAssignment()" << endl;
SmtScope smts(this);
finalOptionsAreSet();
}
}
-Model* SmtEngine::getModel() throw(ModalException, AssertionException) {
+Model* SmtEngine::getModel() throw(ModalException) {
Trace("smt") << "SMT getModel()" << endl;
SmtScope smts(this);
return d_theoryEngine->getModel();
}
-void SmtEngine::checkModel() throw(InternalErrorException) {
+void SmtEngine::checkModel() {
// --check-model implies --interactive, which enables the assertion list,
// so we should be ok.
Assert(d_assertionList != NULL, "don't have an assertion list to check in SmtEngine::checkModel()");
Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
}
-Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
+Proof* SmtEngine::getProof() throw(ModalException) {
Trace("smt") << "SMT getProof()" << endl;
SmtScope smts(this);
finalOptionsAreSet();
}
vector<Expr> SmtEngine::getAssertions()
- throw(ModalException, AssertionException) {
+ throw(ModalException) {
SmtScope smts(this);
finalOptionsAreSet();
if(Dump.isOn("benchmark")) {
* Check that a generated Model (via getModel()) actually satisfies
* all user assertions.
*/
- void checkModel() throw(InternalErrorException);
+ void checkModel();
/**
* This is something of an "init" procedure, but is idempotent; call
* Internally handle the setting of a logic. This function should always
* be called when d_logic is updated.
*/
- void setLogicInternal() throw(AssertionException);
+ void setLogicInternal() throw();
friend class ::CVC4::smt::SmtEnginePrivate;
friend class ::CVC4::smt::SmtScope;
/**
* Construct an SmtEngine with the given expression manager.
*/
- SmtEngine(ExprManager* em) throw(AssertionException);
+ SmtEngine(ExprManager* em) throw();
/**
* Destruct the SMT engine.
* by a SAT or INVALID query). Only permitted if the SmtEngine is
* set to operate interactively and produce-models is on.
*/
- Expr getValue(const Expr& e) throw(ModalException, AssertionException);
+ Expr getValue(const Expr& e) throw(ModalException);
/**
* Add a function to the set of expressions whose value is to be
* this function returns true if the expression was added and false
* if this request was ignored.
*/
- bool addToAssignment(const Expr& e) throw(AssertionException);
+ bool addToAssignment(const Expr& e) throw();
/**
* Get the assignment (only if immediately preceded by a SAT or
* INVALID query). Only permitted if the SmtEngine is set to
* operate interactively and produce-assignments is on.
*/
- CVC4::SExpr getAssignment() throw(ModalException, AssertionException);
+ CVC4::SExpr getAssignment() throw(ModalException);
/**
* Get the model (only if immediately preceded by a SAT
* or INVALID query). Only permitted if CVC4 was built with model
* support and produce-models is on.
*/
- Model* getModel() throw(ModalException, AssertionException);
+ Model* getModel() throw(ModalException);
/**
* Get the last proof (only if immediately preceded by an UNSAT
* or VALID query). Only permitted if CVC4 was built with proof
* support and produce-proofs is on.
*/
- Proof* getProof() throw(ModalException, AssertionException);
+ Proof* getProof() throw(ModalException);
/**
* Get the current set of assertions. Only permitted if the
* SmtEngine is set to operate interactively.
*/
- std::vector<Expr> getAssertions() throw(ModalException, AssertionException);
+ std::vector<Expr> getAssertions() throw(ModalException);
/**
* Push a user-level context.
}
std::string LogicInfo::getLogicString() const {
- Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
if(d_logicString == "") {
size_t seen = 0; // make sure we support all the active theories
}
void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) {
- Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+ CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
d_theories[id] = false;// ensure it's cleared
}
}
void LogicInfo::enableEverything() {
- Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+ CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
*this = LogicInfo();
}
void LogicInfo::disableEverything() {
- Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+ CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
*this = LogicInfo("");
}
void LogicInfo::enableTheory(theory::TheoryId theory) {
- Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+ CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
if(!d_theories[theory]) {
if(isTrueTheory(theory)) {
++d_sharingTheories;
}
void LogicInfo::disableTheory(theory::TheoryId theory) {
- Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+ CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
if(d_theories[theory]) {
if(isTrueTheory(theory)) {
Assert(d_sharingTheories > 0);
}
void LogicInfo::enableIntegers() {
- Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+ CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
enableTheory(THEORY_ARITH);
d_integers = true;
}
void LogicInfo::disableIntegers() {
- Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+ CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
d_integers = false;
if(!d_reals) {
}
void LogicInfo::enableReals() {
- Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+ CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
enableTheory(THEORY_ARITH);
d_reals = true;
}
void LogicInfo::disableReals() {
- Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+ CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
d_reals = false;
if(!d_integers) {
}
void LogicInfo::arithOnlyDifference() {
- Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+ CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
d_linear = true;
d_differenceLogic = true;
}
void LogicInfo::arithOnlyLinear() {
- Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+ CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
d_linear = true;
d_differenceLogic = false;
}
void LogicInfo::arithNonLinear() {
- Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+ CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
d_linear = false;
d_differenceLogic = false;
/** Is sharing enabled for this logic? */
bool isSharingEnabled() const {
- Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
return d_sharingTheories > 1;
}
/** Is the given theory module active in this logic? */
bool isTheoryEnabled(theory::TheoryId theory) const {
- Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
return d_theories[theory];
}
/** Is this a quantified logic? */
bool isQuantified() const {
- Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES);
}
/** Is this the all-inclusive logic? */
bool hasEverything() const {
- Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
LogicInfo everything;
everything.lock();
return *this == everything;
/** Is this the all-exclusive logic? (Here, that means propositional logic) */
bool hasNothing() const {
- Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
LogicInfo nothing("");
nothing.lock();
return *this == nothing;
* use "isPure(theory) && !isQuantified()".
*/
bool isPure(theory::TheoryId theory) const {
- Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
// the third and fourth conjucts are really just to rule out the misleading
// case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
return isTheoryEnabled(theory) && !isSharingEnabled() &&
/** Are integers in this logic? */
bool areIntegersUsed() const {
- Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
return d_integers;
}
/** Are reals in this logic? */
bool areRealsUsed() const {
- Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
return d_reals;
}
/** Does this logic only linear arithmetic? */
bool isLinear() const {
- Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
return d_linear || d_differenceLogic;
}
/** Does this logic only permit difference reasoning? (implies linear) */
bool isDifferenceLogic() const {
- Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+ CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
return d_differenceLogic;
}
/** Are these two LogicInfos equal? */
bool operator==(const LogicInfo& other) const {
- Assert(isLocked() && other.isLocked(), "This LogicInfo isn't locked yet, and cannot be queried");
+ CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
if(d_theories[id] != other.d_theories[id]) {
return false;
}
}
- Assert(d_sharingTheories == other.d_sharingTheories, "LogicInfo internal inconsistency");
+ CheckArgument(d_sharingTheories == other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
if(isTheoryEnabled(theory::THEORY_ARITH)) {
return
d_integers == other.d_integers &&
}
/** Is this LogicInfo "less than or equal" the other? */
bool operator<=(const LogicInfo& other) const {
- Assert(isLocked() && other.isLocked(), "This LogicInfo isn't locked yet, and cannot be queried");
+ CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
if(d_theories[id] && !other.d_theories[id]) {
return false;
}
}
- Assert(d_sharingTheories <= other.d_sharingTheories, "LogicInfo internal inconsistency");
+ CheckArgument(d_sharingTheories <= other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
return
(!d_integers || other.d_integers) &&
}
/** Is this LogicInfo "greater than or equal" the other? */
bool operator>=(const LogicInfo& other) const {
- Assert(isLocked() && other.isLocked(), "This LogicInfo isn't locked yet, and cannot be queried");
+ CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
if(!d_theories[id] && other.d_theories[id]) {
return false;
}
}
- Assert(d_sharingTheories >= other.d_sharingTheories, "LogicInfo internal inconsistency");
+ CheckArgument(d_sharingTheories >= other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
return
(d_integers || !other.d_integers) &&
namespace CVC4 {
#ifdef CVC4_DEBUG
-CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException = NULL;
+CVC4_THREADLOCAL(const char*) s_debugLastException = NULL;
#endif /* CVC4_DEBUG */
void AssertionException::construct(const char* header, const char* extra,
** Assertion utility classes, functions, exceptions, and macros.
**/
-#include "cvc4_public.h"
+#include "cvc4_private.h"
#ifndef __CVC4__ASSERT_H
#define __CVC4__ASSERT_H
namespace CVC4 {
-class CVC4_PUBLIC AssertionException : public Exception {
+class AssertionException : public Exception {
protected:
void construct(const char* header, const char* extra,
const char* function, const char* file,
}
};/* class AssertionException */
-class CVC4_PUBLIC UnreachableCodeException : public AssertionException {
+class UnreachableCodeException : public AssertionException {
protected:
UnreachableCodeException() : AssertionException() {}
}
};/* class UnreachableCodeException */
-class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException {
+class UnhandledCaseException : public UnreachableCodeException {
protected:
UnhandledCaseException() : UnreachableCodeException() {}
}
};/* class UnhandledCaseException */
-class CVC4_PUBLIC UnimplementedOperationException : public AssertionException {
+class UnimplementedOperationException : public AssertionException {
protected:
UnimplementedOperationException() : AssertionException() {}
}
};/* class UnimplementedOperationException */
-class CVC4_PUBLIC IllegalArgumentException : public AssertionException {
+class AssertArgumentException : public AssertionException {
protected:
- IllegalArgumentException() : AssertionException() {}
+ AssertArgumentException() : AssertionException() {}
public:
- IllegalArgumentException(const char* argDesc, const char* function,
- const char* file, unsigned line,
- const char* fmt, ...) :
+ AssertArgumentException(const char* argDesc, const char* function,
+ const char* file, unsigned line,
+ const char* fmt, ...) :
AssertionException() {
va_list args;
va_start(args, fmt);
va_end(args);
}
- IllegalArgumentException(const char* argDesc, const char* function,
- const char* file, unsigned line) :
+ AssertArgumentException(const char* argDesc, const char* function,
+ const char* file, unsigned line) :
AssertionException() {
construct("Illegal argument detected",
( std::string("`") + argDesc + "' is a bad argument" ).c_str(),
function, file, line);
}
- IllegalArgumentException(const char* condStr, const char* argDesc,
- const char* function, const char* file,
- unsigned line, const char* fmt, ...) :
+ AssertArgumentException(const char* condStr, const char* argDesc,
+ const char* function, const char* file,
+ unsigned line, const char* fmt, ...) :
AssertionException() {
va_list args;
va_start(args, fmt);
va_end(args);
}
- IllegalArgumentException(const char* condStr, const char* argDesc,
- const char* function, const char* file,
- unsigned line) :
+ AssertArgumentException(const char* condStr, const char* argDesc,
+ const char* function, const char* file,
+ unsigned line) :
AssertionException() {
construct("Illegal argument detected",
( std::string("`") + argDesc + "' is a bad argument; expected " +
condStr + " to hold" ).c_str(),
function, file, line);
}
-};/* class IllegalArgumentException */
+};/* class AssertArgumentException */
-class CVC4_PUBLIC InternalErrorException : public AssertionException {
+class InternalErrorException : public AssertionException {
protected:
InternalErrorException() : AssertionException() {}
#ifdef CVC4_DEBUG
-extern CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException;
+extern CVC4_THREADLOCAL(const char*) s_debugLastException;
/**
* Special assertion failure handling in debug mode; in non-debug
* debug builds only; in debug builds, it handles all assertion
* failures (even those that exist in non-debug builds).
*/
-void debugAssertionFailed(const AssertionException& thisException,
- const char* lastException) CVC4_PUBLIC;
+void debugAssertionFailed(const AssertionException& thisException, const char* lastException);
// If we're currently handling an exception, print a warning instead;
// otherwise std::terminate() is called by the runtime and we lose
#define InternalError(msg...) \
throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
#define IllegalArgument(arg, msg...) \
- throw ::CVC4::IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+ throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, ## msg)
#define CheckArgument(cond, arg, msg...) \
- AlwaysAssertArgument(cond, arg, ## msg)
+ do { \
+ if(EXPECT_FALSE( ! (cond) )) { \
+ throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, ## msg); \
+ } \
+ } while(0)
#define AlwaysAssertArgument(cond, arg, msg...) \
do { \
if(EXPECT_FALSE( ! (cond) )) { \
- throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+ throw ::CVC4::AssertArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
} \
} while(0)
#ifdef CVC4_ASSERTIONS
# define Assert(cond, msg...) AlwaysAssert(cond, ## msg)
# define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg)
+# define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ## msg)
#else /* ! CVC4_ASSERTIONS */
# define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
# define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
+# define DebugCheckArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
#endif /* CVC4_ASSERTIONS */
}/* CVC4 namespace */
Makefile.in \
debug.h \
exception.h \
+ exception.cpp \
hash.h \
bool.h \
proof.h \
};/* class AscriptionType */
/**
- * A hash strategy for type ascription operators.
+ * A hash function for type ascription operators.
*/
struct CVC4_PUBLIC AscriptionTypeHashFunction {
inline size_t operator()(const AscriptionType& at) const {
#define __CVC4__BITVECTOR_H
#include <iostream>
-#include "util/Assert.h"
+#include "util/exception.h"
#include "util/integer.h"
namespace CVC4 {
return d_value != y.d_value;
}
- BitVector equals(const BitVector& y) const {
- Assert(d_size == y.d_size);
+ BitVector equals(const BitVector& y) const {
+ CheckArgument(d_size == y.d_size, y);
return d_value == y.d_value;
}
// xor
BitVector operator ^(const BitVector& y) const {
- Assert (d_size == y.d_size);
+ CheckArgument(d_size == y.d_size, y);
return BitVector(d_size, d_value.bitwiseXor(y.d_value));
}
// or
BitVector operator |(const BitVector& y) const {
- Assert (d_size == y.d_size);
+ CheckArgument(d_size == y.d_size, y);
return BitVector(d_size, d_value.bitwiseOr(y.d_value));
}
// and
BitVector operator &(const BitVector& y) const {
- Assert (d_size == y.d_size);
+ CheckArgument(d_size == y.d_size, y);
return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
}
BitVector operator +(const BitVector& y) const {
- Assert (d_size == y.d_size);
+ CheckArgument(d_size == y.d_size, y);
Integer sum = d_value + y.d_value;
return BitVector(d_size, sum);
}
BitVector operator -(const BitVector& y) const {
- Assert (d_size == y.d_size);
+ CheckArgument(d_size == y.d_size, y);
// to maintain the invariant that we are only adding BitVectors of the
// same size
BitVector one(d_size, Integer(1));
}
BitVector operator *(const BitVector& y) const {
- Assert (d_size == y.d_size);
+ CheckArgument(d_size == y.d_size, y);
Integer prod = d_value * y.d_value;
return BitVector(d_size, prod);
}
BitVector unsignedDiv (const BitVector& y) const {
- Assert (d_size == y.d_size);
+ CheckArgument(d_size == y.d_size, y);
// TODO: decide whether we really want these semantics
if (y.d_value == 0) {
return BitVector(d_size, Integer(0));
}
- Assert (d_value >= 0 && y.d_value > 0);
+ CheckArgument(d_value >= 0, this);
+ CheckArgument(y.d_value > 0, y);
return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
}
BitVector unsignedRem(const BitVector& y) const {
- Assert (d_size == y.d_size);
+ CheckArgument(d_size == y.d_size, y);
// TODO: decide whether we really want these semantics
if (y.d_value == 0) {
return BitVector(d_size, Integer(0));
}
- Assert (d_value >= 0 && y.d_value > 0);
+ CheckArgument(d_value >= 0, this);
+ CheckArgument(y.d_value > 0, y);
return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
}
bool signedLessThan(const BitVector& y) const {
- Assert(d_size == y.d_size);
- Assert(d_value >= 0 && y.d_value >= 0);
+ CheckArgument(d_size == y.d_size, y);
+ CheckArgument(d_value >= 0, this);
+ CheckArgument(y.d_value >= 0, y);
Integer a = (*this).toSignedInt();
Integer b = y.toSignedInt();
}
bool unsignedLessThan(const BitVector& y) const {
- Assert(d_size == y.d_size);
- Assert(d_value >= 0 && y.d_value >= 0);
+ CheckArgument(d_size == y.d_size, y);
+ CheckArgument(d_value >= 0, this);
+ CheckArgument(y.d_value >= 0, y);
return d_value < y.d_value;
}
bool signedLessThanEq(const BitVector& y) const {
- Assert(d_size == y.d_size);
- Assert(d_value >= 0 && y.d_value >= 0);
+ CheckArgument(d_size == y.d_size, y);
+ CheckArgument(d_value >= 0, this);
+ CheckArgument(y.d_value >= 0, y);
Integer a = (*this).toSignedInt();
Integer b = y.toSignedInt();
}
bool unsignedLessThanEq(const BitVector& y) const {
- Assert(d_size == y.d_size);
- Assert(d_value >= 0 && y.d_value >= 0);
+ CheckArgument(d_size == y.d_size, this);
+ CheckArgument(d_value >= 0, this);
+ CheckArgument(y.d_value >= 0, y);
return d_value <= y.d_value;
}
}
// making sure we don't lose information casting
- Assert(y.d_value < Integer(1).multiplyByPow2(32));
+ CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
uint32_t amount = y.d_value.toUnsignedInt();
Integer res = d_value.multiplyByPow2(amount);
return BitVector(d_size, res);
}
// making sure we don't lose information casting
- Assert(y.d_value < Integer(1).multiplyByPow2(32));
+ CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
uint32_t amount = y.d_value.toUnsignedInt();
Integer res = d_value.divByPow2(amount);
return BitVector(d_size, res);
}
// making sure we don't lose information casting
- Assert(y.d_value < Integer(1).multiplyByPow2(32));
+ CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
uint32_t amount = y.d_value.toUnsignedInt();
Integer rest = d_value.divByPow2(amount);
if(sign_bit == Integer(0)) {
return BitVector(d_size, rest);
}
- Integer res = rest.oneExtend(d_size - amount, amount);
+ Integer res = rest.oneExtend(d_size - amount, amount);
return BitVector(d_size, res);
}
inline BitVector::BitVector(const std::string& num, unsigned base) {
- AlwaysAssert( base == 2 || base == 16 );
+ CheckArgument(base == 2 || base == 16, base);
if( base == 2 ) {
d_size = num.size();
- } else if( base == 16 ) {
- d_size = num.size() * 4;
} else {
- Unreachable("Unsupported base in BitVector(std::string&, unsigned int).");
+ d_size = num.size() * 4;
}
- d_value = Integer(num,base);
+ d_value = Integer(num, base);
}/* BitVector::BitVector() */
#include <utility>
#include "util/integer.h"
-#include "util/Assert.h"
+#include "util/exception.h"
namespace CVC4 {
CheckArgument(card >= 0, card,
"Cardinality must be a nonnegative integer, not %ld.", card);
d_card += 1;
- Assert(isFinite());
}
/**
"Cardinality must be a nonnegative integer, not %s.",
card.toString().c_str());
d_card += 1;
- Assert(isFinite());
}
/**
* Construct an infinite cardinality equal to the given Beth number.
*/
Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) {
- Assert(!isFinite());
}
/**
#include "expr/node.h"
#include "util/recursion_breaker.h"
#include "util/matcher.h"
+#include "util/Assert.h"
using namespace std;
size_t Datatype::indexOf(Expr item) {
ExprManagerScope ems(item);
- AssertArgument(item.getType().isConstructor() ||
- item.getType().isTester() ||
- item.getType().isSelector(),
- item,
- "arg must be a datatype constructor, selector, or tester");
+ CheckArgument(item.getType().isConstructor() ||
+ item.getType().isTester() ||
+ item.getType().isSelector(),
+ item,
+ "arg must be a datatype constructor, selector, or tester");
TNode n = Node::fromExpr(item);
if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
return indexOf( item[0] );
const std::vector<Type>& replacements,
const std::vector< SortConstructorType >& paramTypes,
const std::vector< DatatypeType >& paramReplacements)
- throw(AssertionException, DatatypeResolutionException) {
+ throw(IllegalArgumentException, DatatypeResolutionException) {
- AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager");
- CheckArgument(!d_resolved, "cannot resolve a Datatype twice");
- AssertArgument(resolutions.find(d_name) != resolutions.end(),
+ CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
+ CheckArgument(!d_resolved, this, "cannot resolve a Datatype twice");
+ CheckArgument(resolutions.find(d_name) != resolutions.end(), resolutions,
"Datatype::resolve(): resolutions doesn't contain me!");
- AssertArgument(placeholders.size() == replacements.size(), placeholders,
+ CheckArgument(placeholders.size() == replacements.size(), placeholders,
"placeholders and replacements must be the same size");
- AssertArgument(paramTypes.size() == paramReplacements.size(), paramTypes,
+ CheckArgument(paramTypes.size() == paramReplacements.size(), paramTypes,
"paramTypes and paramReplacements must be the same size");
CheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors");
DatatypeType self = (*resolutions.find(d_name)).second;
- AssertArgument(&self.getDatatype() == this, "Datatype::resolve(): resolutions doesn't contain me!");
+ CheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!");
d_resolved = true;
size_t index = 0;
for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
(*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements);
- Assert((*i).isResolved());
Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index);
Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++);
}
d_self = self;
- Assert(index == getNumConstructors());
}
void Datatype::addConstructor(const DatatypeConstructor& c) {
d_constructors.push_back(c);
}
-Cardinality Datatype::getCardinality() const throw(AssertionException) {
+Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
CheckArgument(isResolved(), this, "this datatype is not yet resolved");
RecursionBreaker<const Datatype*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
if(breaker.isRecursion()) {
return c;
}
-bool Datatype::isFinite() const throw(AssertionException) {
+bool Datatype::isFinite() const throw(IllegalArgumentException) {
CheckArgument(isResolved(), this, "this datatype is not yet resolved");
// we're using some internals, so we have to set up this library context
return true;
}
-bool Datatype::isWellFounded() const throw(AssertionException) {
+bool Datatype::isWellFounded() const throw(IllegalArgumentException) {
CheckArgument(isResolved(), this, "this datatype is not yet resolved");
// we're using some internals, so we have to set up this library context
return false;
}
-Expr Datatype::mkGroundTerm( Type t ) const throw(AssertionException) {
+Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
CheckArgument(isResolved(), this, "this datatype is not yet resolved");
// we're using some internals, so we have to set up this library context
}
}
-DatatypeType Datatype::getDatatypeType() const throw(AssertionException) {
+DatatypeType Datatype::getDatatypeType() const throw(IllegalArgumentException) {
CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
- Assert(!d_self.isNull() && !DatatypeType(d_self).isParametric());
+ CheckArgument(!d_self.isNull() && !DatatypeType(d_self).isParametric(), this);
return DatatypeType(d_self);
}
DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params)
- const throw(AssertionException) {
+ const throw(IllegalArgumentException) {
CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
- Assert(!d_self.isNull() && DatatypeType(d_self).isParametric());
+ CheckArgument(!d_self.isNull() && DatatypeType(d_self).isParametric(), this);
return DatatypeType(d_self).instantiate(params);
}
const std::vector<Type>& replacements,
const std::vector< SortConstructorType >& paramTypes,
const std::vector< DatatypeType >& paramReplacements)
- throw(AssertionException, DatatypeResolutionException) {
+ throw(IllegalArgumentException, DatatypeResolutionException) {
- AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager");
+ CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
CheckArgument(!isResolved(),
"cannot resolve a Datatype constructor twice; "
"perhaps the same constructor was added twice, "
return d_tester;
}
-Cardinality DatatypeConstructor::getCardinality() const throw(AssertionException) {
+Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) {
CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
Cardinality c = 1;
return c;
}
-bool DatatypeConstructor::isFinite() const throw(AssertionException) {
+bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
// we're using some internals, so we have to set up this library context
return true;
}
-bool DatatypeConstructor::isWellFounded() const throw(AssertionException) {
+bool DatatypeConstructor::isWellFounded() const throw(IllegalArgumentException) {
CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
// we're using some internals, so we have to set up this library context
return true;
}
-Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(AssertionException) {
+Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
// we're using some internals, so we have to set up this library context
groundTerms.push_back(getConstructor());
// for each selector, get a ground term
- Assert( t.isDatatype() );
+ CheckArgument( t.isDatatype(), t );
std::vector< Type > instTypes;
std::vector< Type > paramTypes;
if( DatatypeType(t).isParametric() ){
#include "expr/expr.h"
#include "expr/type.h"
-#include "util/Assert.h"
#include "util/output.h"
#include "util/hash.h"
#include "util/exception.h"
const std::vector<Type>& replacements,
const std::vector< SortConstructorType >& paramTypes,
const std::vector< DatatypeType >& paramReplacements)
- throw(AssertionException, DatatypeResolutionException);
+ throw(IllegalArgumentException, DatatypeResolutionException);
friend class Datatype;
/** Helper function for resolving parametric datatypes.
* Return the cardinality of this constructor (the product of the
* cardinalities of its arguments).
*/
- Cardinality getCardinality() const throw(AssertionException);
+ Cardinality getCardinality() const throw(IllegalArgumentException);
/**
* Return true iff this constructor is finite (it is nullary or
* each of its argument types are finite). This function can
* only be called for resolved constructors.
*/
- bool isFinite() const throw(AssertionException);
+ bool isFinite() const throw(IllegalArgumentException);
/**
* Return true iff this constructor is well-founded (there exist
* ground terms). The constructor must be resolved or an
* exception is thrown.
*/
- bool isWellFounded() const throw(AssertionException);
+ bool isWellFounded() const throw(IllegalArgumentException);
/**
* Construct and return a ground term of this constructor. The
* constructor must be both resolved and well-founded, or else an
* exception is thrown.
*/
- Expr mkGroundTerm( Type t ) const throw(AssertionException);
+ Expr mkGroundTerm( Type t ) const throw(IllegalArgumentException);
/**
* Returns true iff this Datatype constructor has already been
const std::vector<Type>& replacements,
const std::vector< SortConstructorType >& paramTypes,
const std::vector< DatatypeType >& paramReplacements)
- throw(AssertionException, DatatypeResolutionException);
+ throw(IllegalArgumentException, DatatypeResolutionException);
friend class ExprManager;// for access to resolve()
public:
* cardinalities of its constructors). The Datatype must be
* resolved.
*/
- Cardinality getCardinality() const throw(AssertionException);
+ Cardinality getCardinality() const throw(IllegalArgumentException);
/**
* Return true iff this Datatype is finite (all constructors are
* datatype is not well-founded, this function returns false. The
* Datatype must be resolved or an exception is thrown.
*/
- bool isFinite() const throw(AssertionException);
+ bool isFinite() const throw(IllegalArgumentException);
/**
* Return true iff this datatype is well-founded (there exist ground
* terms). The Datatype must be resolved or an exception is thrown.
*/
- bool isWellFounded() const throw(AssertionException);
+ bool isWellFounded() const throw(IllegalArgumentException);
/**
* Construct and return a ground term of this Datatype. The
* Datatype must be both resolved and well-founded, or else an
* exception is thrown.
*/
- Expr mkGroundTerm( Type t ) const throw(AssertionException);
+ Expr mkGroundTerm( Type t ) const throw(IllegalArgumentException);
/**
* Get the DatatypeType associated to this Datatype. Can only be
* called post-resolution.
*/
- DatatypeType getDatatypeType() const throw(AssertionException);
+ DatatypeType getDatatypeType() const throw(IllegalArgumentException);
/**
* Get the DatatypeType associated to this (parameterized) Datatype. Can only be
* called post-resolution.
*/
- DatatypeType getDatatypeType(const std::vector<Type>& params) const throw(AssertionException);
+ DatatypeType getDatatypeType(const std::vector<Type>& params) const throw(IllegalArgumentException);
/**
* Return true iff the two Datatypes are the same.
--- /dev/null
+/********************* */
+/*! \file exception.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief CVC4's exception base class and some associated utilities
+ **
+ ** CVC4's exception base class and some associated utilities.
+ **/
+
+#include "util/exception.h"
+#include <string>
+#include <cstdio>
+#include <cstdlib>
+#include <cstdarg>
+
+using namespace std;
+using namespace CVC4;
+
+void IllegalArgumentException::construct(const char* header, const char* extra,
+ const char* function, const char* fmt,
+ va_list args) {
+ // try building the exception msg with a smallish buffer first,
+ // then with a larger one if sprintf tells us to.
+ int n = 512;
+ char* buf;
+
+ for(;;) {
+ buf = new char[n];
+
+ int size;
+ if(extra == NULL) {
+ size = snprintf(buf, n, "%s\n%s\n",
+ header, function);
+ } else {
+ size = snprintf(buf, n, "%s\n%s\n\n %s\n",
+ header, function, extra);
+ }
+
+ if(size < n) {
+ va_list args_copy;
+ va_copy(args_copy, args);
+ size += vsnprintf(buf + size, n - size, fmt, args_copy);
+ va_end(args_copy);
+
+ if(size < n) {
+ break;
+ }
+ }
+
+ if(size >= n) {
+ // try again with a buffer that's large enough
+ n = size + 1;
+ delete [] buf;
+ }
+ }
+
+ setMessage(string(buf));
+
+ delete [] buf;
+}
+
+void IllegalArgumentException::construct(const char* header, const char* extra,
+ const char* function) {
+ // try building the exception msg with a smallish buffer first,
+ // then with a larger one if sprintf tells us to.
+ int n = 256;
+ char* buf;
+
+ for(;;) {
+ buf = new char[n];
+
+ int size;
+ if(extra == NULL) {
+ size = snprintf(buf, n, "%s.\n%s\n",
+ header, function);
+ } else {
+ size = snprintf(buf, n, "%s.\n%s\n\n %s\n",
+ header, function, extra);
+ }
+
+ if(size < n) {
+ break;
+ } else {
+ // try again with a buffer that's large enough
+ n = size + 1;
+ delete [] buf;
+ }
+ }
+
+ setMessage(string(buf));
+
+ delete [] buf;
+}
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief CVC4's exception base class and some associated utilities.
+ ** \brief CVC4's exception base class and some associated utilities
**
** CVC4's exception base class and some associated utilities.
**/
#include <string>
#include <sstream>
#include <exception>
+#include <cstdlib>
+#include <cstdarg>
namespace CVC4 {
};/* class Exception */
+class CVC4_PUBLIC IllegalArgumentException : public Exception {
+protected:
+ IllegalArgumentException() : Exception() {}
+
+ void construct(const char* header, const char* extra,
+ const char* function, const char* fmt, ...) {
+ va_list args;
+ va_start(args, fmt);
+ construct(header, extra, function, fmt, args);
+ va_end(args);
+ }
+
+ void construct(const char* header, const char* extra,
+ const char* function, const char* fmt, va_list args);
+
+ void construct(const char* header, const char* extra,
+ const char* function);
+
+public:
+ IllegalArgumentException(const char* condStr, const char* argDesc,
+ const char* function, const char* fmt, ...) :
+ Exception() {
+ va_list args;
+ va_start(args, fmt);
+ construct("Illegal argument detected",
+ ( std::string("`") + argDesc + "' is a bad argument"
+ + (*condStr == '\0' ? std::string() :
+ ( std::string("; expected ") +
+ condStr + " to hold" )) ).c_str(),
+ function, fmt, args);
+ va_end(args);
+ }
+
+ IllegalArgumentException(const char* condStr, const char* argDesc,
+ const char* function) :
+ Exception() {
+ construct("Illegal argument detected",
+ ( std::string("`") + argDesc + "' is a bad argument"
+ + (*condStr == '\0' ? std::string() :
+ ( std::string("; expected ") +
+ condStr + " to hold" )) ).c_str(),
+ function);
+ }
+};/* class IllegalArgumentException */
+
inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() CVC4_PUBLIC;
inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() {
e.toStream(os);
}/* CVC4 namespace */
+#if defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)
+# include "util/Assert.h"
+#endif /* __BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST */
+
+namespace CVC4 {
+
+#ifndef CheckArgument
+template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC;
+template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) {
+ if(EXPECT_FALSE( !cond )) { \
+ throw ::CVC4::IllegalArgumentException("", "", ""); \
+ } \
+}
+template <class T> inline void CheckArgument(bool cond, const T& arg) CVC4_PUBLIC;
+template <class T> inline void CheckArgument(bool cond, const T& arg) {
+ if(EXPECT_FALSE( !cond )) { \
+ throw ::CVC4::IllegalArgumentException("", "", ""); \
+ } \
+}
+#endif /* CheckArgument */
+
+#ifndef DebugCheckArgument
+template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC;
+template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) {
+ if(EXPECT_FALSE( !cond )) { \
+ throw ::CVC4::IllegalArgumentException("", "", ""); \
+ } \
+}
+template <class T> inline void DebugCheckArgument(bool cond, const T& arg) CVC4_PUBLIC;
+template <class T> inline void DebugCheckArgument(bool cond, const T& arg) {
+ if(EXPECT_FALSE( !cond )) { \
+ throw ::CVC4::IllegalArgumentException("", "", ""); \
+ } \
+}
+#endif /* DebugCheckArgument */
+
+}/* CVC4 namespace */
+
#endif /* __CVC4__EXCEPTION_H */
#include <cln/integer_io.h>
#include <limits>
-#include "util/Assert.h"
+#include "util/exception.h"
namespace CVC4 {
}
Integer oneExtend(uint32_t size, uint32_t amount) const {
- Assert((*this) < Integer(1).multiplyByPow2(size));
+ DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
cln::cl_byte range(amount, size);
cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1; // 2^size - 1
Integer temp(allones);
* If y divides *this, then exactQuotient returns (this/y)
*/
Integer exactQuotient(const Integer& y) const {
- Assert(y.divides(*this));
+ DebugCheckArgument(y.divides(*this), y);
return Integer( cln::exquo(d_value, y.d_value) );
}
}else if(exp == 0){
return Integer( 1 );
}else{
- Unimplemented();
+ throw Exception("Negative exponent in Integer::pow()");
}
}
fprinthexadecimal(ss,d_value);
break;
default:
- Unhandled();
- break;
+ throw Exception("Unhandled base in Integer::toString()");
}
std::string output = ss.str();
for( unsigned i = 0; i <= output.length(); ++i){
int sgn() const {
cln::cl_I sgn = cln::signum(d_value);
- Assert(sgn == 0 || sgn == -1 || sgn == 1);
return cln::cl_I_to_int(sgn);
}
long getLong() const {
// ensure there isn't overflow
- AlwaysAssert(d_value <= std::numeric_limits<long>::max(),
- "Overflow detected in Integer::getLong()");
- AlwaysAssert(d_value >= std::numeric_limits<long>::min(),
- "Overflow detected in Integer::getLong()");
+ CheckArgument(d_value <= std::numeric_limits<long>::max(), this,
+ "Overflow detected in Integer::getLong()");
+ CheckArgument(d_value >= std::numeric_limits<long>::min(), this,
+ "Overflow detected in Integer::getLong()");
return cln::cl_I_to_long(d_value);
}
unsigned long getUnsignedLong() const {
// ensure there isn't overflow
- AlwaysAssert(d_value <= std::numeric_limits<unsigned long>::max(),
- "Overflow detected in Integer::getUnsignedLong()");
- AlwaysAssert(d_value >= std::numeric_limits<unsigned long>::min(),
- "Overflow detected in Integer::getUnsignedLong()");
+ CheckArgument(d_value <= std::numeric_limits<unsigned long>::max(), this,
+ "Overflow detected in Integer::getUnsignedLong()");
+ CheckArgument(d_value >= std::numeric_limits<unsigned long>::min(), this,
+ "Overflow detected in Integer::getUnsignedLong()");
return cln::cl_I_to_ulong(d_value);
}
#include <string>
#include <iostream>
-#include "util/Assert.h"
#include "util/gmp_util.h"
+#include "util/exception.h"
namespace CVC4 {
*/
Integer oneExtend(uint32_t size, uint32_t amount) const {
// check that the size is accurate
- Assert ((*this) < Integer(1).multiplyByPow2(size));
+ DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
mpz_class res = d_value;
for (unsigned i = size; i < size + amount; ++i) {
* If y divides *this, then exactQuotient returns (this/y)
*/
Integer exactQuotient(const Integer& y) const {
- Assert(y.divides(*this));
+ DebugCheckArgument(y.divides(*this), y);
mpz_class q;
mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
return Integer( q );
long getLong() const {
long si = d_value.get_si();
// ensure there wasn't overflow
- AlwaysAssert(mpz_cmp_si(d_value.get_mpz_t(), si) == 0,
+ CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, this,
"Overflow detected in Integer::getLong()");
return si;
}
unsigned long getUnsignedLong() const {
unsigned long ui = d_value.get_ui();
// ensure there wasn't overflow
- AlwaysAssert(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0,
- "Overflow detected in Integer::getUnsignedLong()");
+ CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, this,
+ "Overflow detected in Integer::getUnsignedLong()");
return ui;
}
#ifndef __CVC4__PREDICATE_H
#define __CVC4__PREDICATE_H
-#include "util/Assert.h"
+#include "util/exception.h"
namespace CVC4 {
#include <gmp.h>
#include <string>
#include <sstream>
+#include <cassert>
#include <cln/rational.h>
#include <cln/input.h>
#include <cln/io.h>
#include <cln/rational_io.h>
#include <cln/number_io.h>
-#include "util/Assert.h"
+#include "util/exception.h"
#include "util/integer.h"
namespace CVC4 {
}else if(cln::minusp(d_value)){
return -1;
}else{
- Assert(cln::plusp(d_value));
+ assert(cln::plusp(d_value));
return 1;
}
}
#include <string>
#include "util/integer.h"
+#include "util/exception.h"
namespace CVC4 {
#include <iostream>
#include <string>
-#include "util/Assert.h"
+#include "util/exception.h"
namespace CVC4 {
-// TODO: either templatize Result on its Kind (Sat/Validity) or subclass.
-// TODO: INVALID/SAT provide models, etc?---perhaps just by linking back
-// into the SmtEngine that produced the Result?
-// TODO: make unconstructible except by SmtEngine? That would ensure that
-// any Result in the system is bona fide.
-
class Result;
std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC;
return d_which == TYPE_NONE;
}
enum UnknownExplanation whyUnknown() const {
- AlwaysAssert( isUnknown(),
- "This result is not unknown, so the reason for "
- "being unknown cannot be inquired of it" );
+ CheckArgument( isUnknown(), this,
+ "This result is not unknown, so the reason for "
+ "being unknown cannot be inquired of it" );
return d_unknownExplanation;
}
#include "util/integer.h"
#include "util/rational.h"
-#include "util/Assert.h"
+#include "util/exception.h"
namespace CVC4 {
}
inline std::string SExpr::getValue() const {
- AlwaysAssert( isAtom() );
+ CheckArgument( isAtom(), this );
switch(d_sexprType) {
case SEXPR_INTEGER:
return d_integerValue.toString();
case SEXPR_STRING:
case SEXPR_KEYWORD:
return d_stringValue;
- default:
- Unhandled(d_sexprType);
+ case SEXPR_NOT_ATOM:
+ return std::string();
}
- return d_stringValue;
+ return std::string();
}
inline const CVC4::Integer& SExpr::getIntegerValue() const {
- AlwaysAssert( isInteger() );
+ CheckArgument( isInteger(), this );
return d_integerValue;
}
inline const CVC4::Rational& SExpr::getRationalValue() const {
- AlwaysAssert( isRational() );
+ CheckArgument( isRational(), this );
return d_rationalValue;
}
inline const std::vector<SExpr>& SExpr::getChildren() const {
- AlwaysAssert( !isAtom() );
+ CheckArgument( !isAtom(), this );
return d_children;
}
return stats::getStatisticsRegistry(smt::currentSmtEngine());
}
-void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) {
+void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) {
#ifdef CVC4_STATISTICS_ON
StatSet& stats = current()->d_stats;
- AlwaysAssert(stats.find(s) == stats.end(),
- "Statistic `%s' was already registered with this registry.", s->getName().c_str());
+ CheckArgument(stats.find(s) == stats.end(), s,
+ "Statistic `%s' was already registered with this registry.",
+ s->getName().c_str());
stats.insert(s);
#endif /* CVC4_STATISTICS_ON */
}/* StatisticsRegistry::registerStat() */
-void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) {
+void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) {
#ifdef CVC4_STATISTICS_ON
StatSet& stats = current()->d_stats;
- AlwaysAssert(stats.find(s) != stats.end(),
- "Statistic `%s' was not registered with this registry.", s->getName().c_str());
+ CheckArgument(stats.find(s) != stats.end(), s,
+ "Statistic `%s' was not registered with this registry.",
+ s->getName().c_str());
stats.erase(s);
#endif /* CVC4_STATISTICS_ON */
}/* StatisticsRegistry::unregisterStat() */
#endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */
-void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) {
+void StatisticsRegistry::registerStat_(Stat* s) throw(CVC4::IllegalArgumentException) {
#ifdef CVC4_STATISTICS_ON
- AlwaysAssert(d_stats.find(s) == d_stats.end());
+ CheckArgument(d_stats.find(s) == d_stats.end(), s);
d_stats.insert(s);
#endif /* CVC4_STATISTICS_ON */
}/* StatisticsRegistry::registerStat_() */
-void StatisticsRegistry::unregisterStat_(Stat* s) throw(AssertionException) {
+void StatisticsRegistry::unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException) {
#ifdef CVC4_STATISTICS_ON
- AlwaysAssert(d_stats.find(s) != d_stats.end());
+ CheckArgument(d_stats.find(s) != d_stats.end(), s);
d_stats.erase(s);
#endif /* CVC4_STATISTICS_ON */
}/* StatisticsRegistry::unregisterStat_() */
void TimerStat::start() {
if(__CVC4_USE_STATISTICS) {
- AlwaysAssert(!d_running);
+ CheckArgument(!d_running, *this, "timer already running");
clock_gettime(CLOCK_MONOTONIC, &d_start);
d_running = true;
}
void TimerStat::stop() {
if(__CVC4_USE_STATISTICS) {
- AlwaysAssert(d_running);
+ CheckArgument(d_running, *this, "timer not running");
::timespec end;
clock_gettime(CLOCK_MONOTONIC, &end);
d_data += end - d_start;
#include <ctime>
#include <vector>
#include <stdint.h>
-
-#include "util/Assert.h"
+#include <cassert>
namespace CVC4 {
* will throw an assertion exception if the given name contains the
* statistic delimiter string.
*/
- Stat(const std::string& name) throw(CVC4::AssertionException) :
+ Stat(const std::string& name) throw(CVC4::IllegalArgumentException) :
d_name(name) {
if(__CVC4_USE_STATISTICS) {
- AlwaysAssert(d_name.find(", ") == std::string::npos);
+ CheckArgument(d_name.find(", ") == std::string::npos, name,
+ "Statistics names cannot include a comma (',')");
}
}
/** Get the value of the referenced data cell. */
const T& getData() const {
- if(__CVC4_USE_STATISTICS) {
- return *d_data;
- } else {
- Unreachable();
- }
+ return *d_data;
}
};/* class ReferenceStat<T> */
/** Get the underlying data value. */
const T& getData() const {
- if(__CVC4_USE_STATISTICS) {
- return d_data;
- } else {
- Unreachable();
- }
+ return d_data;
}
};/* class BackedStat<T> */
/** Get the data of the underlying (wrapped) statistic. */
const T& getData() const {
- if(__CVC4_USE_STATISTICS) {
- return d_stat.getData();
- } else {
- Unreachable();
- }
+ return d_stat.getData();
}
SExpr getValue() const {
StatisticsRegistry() {}
/** Construct a statistics registry */
- StatisticsRegistry(const std::string& name) throw(CVC4::AssertionException) :
+ StatisticsRegistry(const std::string& name)
+ throw(CVC4::IllegalArgumentException) :
Stat(name) {
d_prefix = name;
if(__CVC4_USE_STATISTICS) {
- AlwaysAssert(d_name.find(s_regDelim) == std::string::npos);
+ CheckArgument(d_name.find(s_regDelim) == std::string::npos, name,
+ "StatisticsRegistry names cannot contain the string \"%s\"",
+ s_regDelim.c_str());
}
}
#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT)
/** Register a new statistic, making it active. */
- static void registerStat(Stat* s) throw(AssertionException);
+ static void registerStat(Stat* s) throw(CVC4::IllegalArgumentException);
/** Unregister an active statistic, making it inactive. */
- static void unregisterStat(Stat* s) throw(AssertionException);
+ static void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException);
#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB) && ! __BUILDING_STATISTICS_FOR_EXPORT */
/** Register a new statistic */
- void registerStat_(Stat* s) throw(AssertionException);
+ void registerStat_(Stat* s) throw(CVC4::IllegalArgumentException);
/** Unregister a new statistic */
- void unregisterStat_(Stat* s) throw(AssertionException);
+ void unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException);
};/* class StatisticsRegistry */
inline timespec& operator+=(timespec& a, const timespec& b) {
// assumes a.tv_nsec and b.tv_nsec are in range
const long nsec_per_sec = 1000000000L; // one thousand million
- Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec);
- Assert(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec);
+ CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
+ CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b);
a.tv_sec += b.tv_sec;
long nsec = a.tv_nsec + b.tv_nsec;
- Assert(nsec >= 0);
+ assert(nsec >= 0);
if(nsec < 0) {
nsec += nsec_per_sec;
--a.tv_sec;
nsec -= nsec_per_sec;
++a.tv_sec;
}
- Assert(nsec >= 0 && nsec < nsec_per_sec);
+ assert(nsec >= 0 && nsec < nsec_per_sec);
a.tv_nsec = nsec;
return a;
}
inline timespec& operator-=(timespec& a, const timespec& b) {
// assumes a.tv_nsec and b.tv_nsec are in range
const long nsec_per_sec = 1000000000L; // one thousand million
- Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec);
- Assert(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec);
+ CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a);
+ CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b);
a.tv_sec -= b.tv_sec;
long nsec = a.tv_nsec - b.tv_nsec;
if(nsec < 0) {
nsec -= nsec_per_sec;
++a.tv_sec;
}
- Assert(nsec >= 0 && nsec < nsec_per_sec);
+ assert(nsec >= 0 && nsec < nsec_per_sec);
a.tv_nsec = nsec;
return a;
}
RegisterStatistic(StatisticsRegistry* reg, Stat* stat) :
d_reg(reg),
d_stat(stat) {
- Assert(d_reg != NULL,
- "You need to specify a statistics registry"
- "on which to set the statistic");
+ CheckArgument(reg != NULL, reg,
+ "You need to specify a statistics registry"
+ "on which to set the statistic");
d_reg->registerStat_(d_stat);
}
#define __CVC4__SUBRANGE_BOUND_H
#include "util/integer.h"
-#include "util/Assert.h"
+#include "util/exception.h"
#include <limits>
* precondition: joinIsBounded(a,b) is true
*/
static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b){
- Assert(joinIsBounded(a,b));
+ DebugCheckArgument(joinIsBounded(a,b), a);
SubrangeBound newLower = SubrangeBound::min(a.lower, b.lower);
SubrangeBound newUpper = SubrangeBound::max(a.upper, b.upper);
return SubrangeBounds(newLower, newUpper);
Expr e = psr->nextExpression();
stringstream ss;
ss << Expr::setlanguage(outlang) << Expr::setdepth(-1) << e;
- AlwaysAssert(psr->nextExpression().isNull(), "next expr should be null");
- AlwaysAssert(psr->done(), "parser should be done");
+ assert(psr->nextExpression().isNull());// next expr should be null
+ assert(psr->done());// parser should be done
string s = ss.str();
cout << "got this:" << endl
<< s << endl
psr->setInput(Input::newStringInput(toInputLanguage(outlang), s, "internal-buffer"));
Expr f = psr->nextExpression();
- AlwaysAssert(e == f);
+ assert(e == f);
cout << "got same expressions " << e.getId() << " and " << f.getId() << endl
<< "==============================================" << endl;
string out = translate(cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2);
cout << "back to SMT2 : " << out << endl << endl;
- AlwaysAssert(out == smt2, "differences in output");
+ assert(out == smt2);// differences in output
}
delete c;
}
- AlwaysAssert(psr->done(), "parser should be done");
+ assert(psr->done());// parser should be done
cout << Expr::setdepth(-1);
#include "expr/expr_manager.h"
#include "expr/expr.h"
-#include "util/Assert.h"
#include "util/exception.h"
using namespace CVC4;
void testMkAssociativeTooFew() {
std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), 1);
- TS_ASSERT_THROWS( d_exprManager->mkAssociative(AND,vars), AssertionException);
+ TS_ASSERT_THROWS( d_exprManager->mkAssociative(AND,vars), IllegalArgumentException);
}
void testMkAssociativeBadKind() {
std::vector<Expr> vars = mkVars(d_exprManager->integerType(), 10);
- TS_ASSERT_THROWS( d_exprManager->mkAssociative(TUPLE,vars), AssertionException);
+ TS_ASSERT_THROWS( d_exprManager->mkAssociative(TUPLE,vars), IllegalArgumentException);
}
};
#include "expr/expr_manager.h"
#include "expr/expr.h"
-#include "util/Assert.h"
#include "util/exception.h"
using namespace CVC4;
TS_ASSERT(!(AND ^ AND ^ AND).isEmpty());
#ifdef CVC4_ASSERTIONS
- TS_ASSERT_THROWS(~LAST_KIND, IllegalArgumentException);
+ TS_ASSERT_THROWS(~LAST_KIND, AssertArgumentException);
#endif /* CVC4_ASSERTIONS */
}
TS_ASSERT( f == fa.getOperator() );
#ifdef CVC4_ASSERTIONS
- TS_ASSERT_THROWS( f.getOperator(), AssertionException );
- TS_ASSERT_THROWS( a.getOperator(), AssertionException );
+ TS_ASSERT_THROWS( f.getOperator(), IllegalArgumentException );
+ TS_ASSERT_THROWS( a.getOperator(), IllegalArgumentException );
#endif /* CVC4_ASSERTIONS */
}
#include "expr/type.h"
#include "expr/expr_manager.h"
#include "util/cardinality.h"
-#include "util/Assert.h"
using namespace CVC4;
using namespace CVC4::kind;
LogicInfo info;
TS_ASSERT( !info.isLocked() );
-#ifdef CVC4_ASSERTIONS
- TS_ASSERT_THROWS( info.getLogicString(), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BUILTIN ), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BOOL ), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_UF ), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARITH ), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAY ), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BV ), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_DATATYPES ), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_QUANTIFIERS ), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_REWRITERULES ), CVC4::AssertionException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_BUILTIN ), CVC4::AssertionException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_BOOL ), CVC4::AssertionException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_UF ), CVC4::AssertionException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_ARITH ), CVC4::AssertionException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAY ), CVC4::AssertionException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_BV ), CVC4::AssertionException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_DATATYPES ), CVC4::AssertionException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_QUANTIFIERS ), CVC4::AssertionException );
- TS_ASSERT_THROWS( ! info.isPure( THEORY_REWRITERULES ), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.isQuantified(), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.areIntegersUsed(), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.areRealsUsed(), CVC4::AssertionException );
- TS_ASSERT_THROWS( ! info.isLinear(), CVC4::AssertionException );
-#endif /* CVC4_ASSERTIONS */
+ TS_ASSERT_THROWS( info.getLogicString(), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BUILTIN ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BOOL ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_UF ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARITH ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAY ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BV ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_DATATYPES ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_REWRITERULES ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( ! info.isPure( THEORY_BUILTIN ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( ! info.isPure( THEORY_BOOL ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( ! info.isPure( THEORY_UF ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( ! info.isPure( THEORY_ARITH ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAY ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( ! info.isPure( THEORY_BV ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( ! info.isPure( THEORY_DATATYPES ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( ! info.isPure( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( ! info.isPure( THEORY_REWRITERULES ), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.isQuantified(), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.areIntegersUsed(), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.areRealsUsed(), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( ! info.isLinear(), CVC4::IllegalArgumentException );
info.lock();
TS_ASSERT( info.isLocked() );
TS_ASSERT( info.areRealsUsed() );
TS_ASSERT( ! info.isLinear() );
-#ifdef CVC4_ASSERTIONS
- TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.disableIntegers(), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.disableQuantifiers(), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.disableTheory(THEORY_BV), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.disableTheory(THEORY_DATATYPES), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.enableIntegers(), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.disableReals(), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.disableTheory(THEORY_ARITH), CVC4::AssertionException );
- TS_ASSERT_THROWS( info.disableTheory(THEORY_UF), CVC4::AssertionException );
-#endif /* CVC4_ASSERTIONS */
+ TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.disableIntegers(), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.disableQuantifiers(), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.disableTheory(THEORY_BV), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.disableTheory(THEORY_DATATYPES), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.enableIntegers(), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.disableReals(), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.disableTheory(THEORY_ARITH), CVC4::IllegalArgumentException );
+ TS_ASSERT_THROWS( info.disableTheory(THEORY_UF), CVC4::IllegalArgumentException );
info = info.getUnlockedCopy();
TS_ASSERT( !info.isLocked() );
void testAssert() {
#ifdef CVC4_ASSERTIONS
TS_ASSERT_THROWS( Assert(false), AssertionException );
- TS_ASSERT_THROWS( AssertArgument(false, "x"), IllegalArgumentException );
+ TS_ASSERT_THROWS( AssertArgument(false, "x"), AssertArgumentException );
#else /* CVC4_ASSERTIONS */
TS_ASSERT_THROWS_NOTHING( Assert(false) );
TS_ASSERT_THROWS_NOTHING( AssertArgument(false, "x") );
TS_ASSERT_THROWS( IllegalArgument("x"), IllegalArgumentException );
TS_ASSERT_THROWS( CheckArgument(false, "x"), IllegalArgumentException );
TS_ASSERT_THROWS( AlwaysAssertArgument(false, "x"),
- IllegalArgumentException );
+ AssertArgumentException );
TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") );
TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") );
}
#ifdef CVC4_ASSERTIONS
in = Node();
- TS_ASSERT_THROWS( BooleanSimplification::negate(in), IllegalArgumentException );
+ TS_ASSERT_THROWS( BooleanSimplification::negate(in), AssertArgumentException );
#endif /* CVC4_ASSERTIONS */
}
#ifdef CVC4_ASSERTIONS
in = d_nm->mkNode(kind::AND, a, b);
- TS_ASSERT_THROWS( BooleanSimplification::simplifyClause(in), IllegalArgumentException );
+ TS_ASSERT_THROWS( BooleanSimplification::simplifyClause(in), AssertArgumentException );
#endif /* CVC4_ASSERTIONS */
}
#ifdef CVC4_ASSERTIONS
in = d_nm->mkNode(kind::OR, a, b);
- TS_ASSERT_THROWS( BooleanSimplification::simplifyHornClause(in), IllegalArgumentException );
+ TS_ASSERT_THROWS( BooleanSimplification::simplifyHornClause(in), AssertArgumentException );
#endif /* CVC4_ASSERTIONS */
}
#ifdef CVC4_ASSERTIONS
in = d_nm->mkNode(kind::OR, a, b);
- TS_ASSERT_THROWS( BooleanSimplification::simplifyConflict(in), IllegalArgumentException );
+ TS_ASSERT_THROWS( BooleanSimplification::simplifyConflict(in), AssertArgumentException );
#endif /* CVC4_ASSERTIONS */
}
projects / cvc5.git / commitdiff