- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example.
- Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems.
- Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions.
- Changing some headers to use iosfwd when possible.
#define InternalError(msg...) \
throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
#define IllegalArgument(arg, msg...) \
- throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, ## msg)
-#define CheckArgument(cond, arg, msg...) \
+ throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, \
+ ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str());
+// This cannot use check argument directly as this forces
+// CheckArgument to use a va_list. This is unsupported in Swig.
+#define PrettyCheckArgument(cond, arg, msg...) \
do { \
if(__builtin_expect( ( ! (cond) ), false )) { \
- throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, ## msg); \
+ throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, \
+ ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); \
} \
} while(0)
#define AlwaysAssertArgument(cond, arg, msg...) \
**/
#include "base/exception.h"
+
#include <string>
#include <cstdio>
#include <cstdlib>
using namespace std;
-#warning "TODO: Remove the second definition of CheckArgument and DebugCheckArgument."
-
namespace CVC4 {
+
+char* IllegalArgumentException::s_header = "Illegal argument detected";
+
+std::string IllegalArgumentException::formatVariadic() {
+ return std::string();
+}
+
+std::string IllegalArgumentException::formatVariadic(const char* format, ...) {
+ va_list args;
+ va_start(args, format);
+
+ int n = 512;
+ char* buf = NULL;
+
+ for (int i = 0; i < 2; ++i){
+ Assert(n > 0);
+ if(buf != NULL){
+ delete [] buf;
+ }
+ buf = new char[n];
+
+ va_list args_copy;
+ va_copy(args_copy, args);
+ int size = vsnprintf(buf, n, format, args);
+ va_end(args_copy);
+
+ if(size >= n){
+ buf[n-1] = '\0';
+ n = size + 1;
+ } else {
+ break;
+ }
+ }
+ // buf is not NULL is an invariant.
+ // buf is also 0 terminated.
+ Assert(buf != NULL);
+ std::string result(buf);
+ delete [] buf;
+ va_end(args);
+ return result;
+}
+
+std::string IllegalArgumentException::format_extra(const char* condStr, const char* argDesc){
+ return ( std::string("`") + argDesc + "' is a bad argument"
+ + (*condStr == '\0' ? std::string() :
+ ( std::string("; expected ") +
+ condStr + " to hold" )) );
+}
+
void IllegalArgumentException::construct(const char* header, const char* extra,
- const char* function, const char* fmt,
- va_list args) {
+ const char* function, const char* tail) {
// try building the exception msg with a smallish buffer first,
// then with a larger one if sprintf tells us to.
int n = 512;
int size;
if(extra == NULL) {
- size = snprintf(buf, n, "%s\n%s\n",
- header, function);
+ size = snprintf(buf, n, "%s\n%s\n%s",
+ header, function, tail);
} else {
- size = snprintf(buf, n, "%s\n%s\n\n %s\n",
- header, function, extra);
+ size = snprintf(buf, n, "%s\n%s\n\n %s\n%s",
+ header, function, extra, tail);
}
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) {
+ break;
+ } else {
+ // size >= n
// try again with a buffer that's large enough
n = size + 1;
delete [] buf;
#ifndef __CVC4__EXCEPTION_H
#define __CVC4__EXCEPTION_H
-#include <iostream>
-#include <string>
+#include <cstdarg>
+#include <cstdlib>
+#include <exception>
+#include <iosfwd>
#include <sstream>
#include <stdexcept>
-#include <exception>
-#include <cstdlib>
-#include <cstdarg>
+#include <string>
namespace CVC4 {
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);
+ const char* function, const char* tail);
void construct(const char* header, const char* extra,
const char* function);
+ static std::string format_extra(const char* condStr, const char* argDesc);
+
+ static char* s_header;
+
public:
+
IllegalArgumentException(const char* condStr, const char* argDesc,
- const char* function, const char* fmt, ...) :
+ const char* function, const char* tail) :
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);
+ construct(s_header, format_extra(condStr, argDesc).c_str(), function, tail);
}
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);
+ construct(s_header, format_extra(condStr, argDesc).c_str(), function);
}
+
+ /**
+ * This is a convenience function for building usages that are variadic.
+ *
+ * Having IllegalArgumentException itself be variadic is problematic for
+ * making sure calls to IllegalArgumentException clean up memory.
+ */
+ static std::string formatVariadic();
+ static std::string formatVariadic(const char* format, ...);
};/* class IllegalArgumentException */
inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() CVC4_PUBLIC;
return os;
}
-}/* CVC4 namespace */
-
-#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT)
-# include "base/cvc4_assert.h"
-#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && !__BUILDING_STATISTICS_FOR_EXPORT */
-
-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, ...) {
+template <class T> inline void CheckArgument(bool cond, const T& arg,
+ const char* tail) CVC4_PUBLIC;
+template <class T> inline void CheckArgument(bool cond, const T& arg,
+ const char* tail) {
if(__builtin_expect( ( !cond ), false )) { \
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)
+ CVC4_PUBLIC;
template <class T> inline void CheckArgument(bool cond, const T& arg) {
if(__builtin_expect( ( !cond ), false )) { \
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(__builtin_expect( ( !cond ), false )) { \
- 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(__builtin_expect( ( !cond ), false )) { \
- throw ::CVC4::IllegalArgumentException("", "", ""); \
- } \
-}
-#endif /* DebugCheckArgument */
}/* CVC4 namespace */
#include <sstream>
#include <set>
#include <cassert>
-#include <iostream>
+#include <iosfwd>
#include <string>
#include <jni.h>
#include <algorithm>
#include <cassert>
-#include <iostream>
+#include <iosfwd>
#include <iterator>
#include <sstream>
#include <string>
+#include "base/exception.h"
#include "base/output.h"
#include "expr/kind.h"
#include "expr/predicate.h"
using namespace std;
+// Matches base/cvc4_assert.h's PrettyCheckArgument.
+// base/cvc4_assert.h cannot be directly included.
+#define CompatCheckArgument(cond, arg, msg...) \
+ do { \
+ if(__builtin_expect( ( ! (cond) ), false )) { \
+ throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, \
+ ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); \
+ } \
+ } while(0)
+
#define Unimplemented(str) throw Exception(str)
namespace CVC3 {
}
std::string Expr::getString() const {
- CVC4::CheckArgument(getKind() == CVC4::kind::CONST_STRING, *this, "CVC3::Expr::getString(): not a string Expr: `%s'", toString().c_str());
+ CompatCheckArgument(getKind() == CVC4::kind::CONST_STRING, *this, "CVC3::Expr::getString(): not a string Expr: `%s'", toString().c_str());
return getConst<CVC4::String>().toString();
}
std::vector<Expr> Expr::getVars() const {
- CVC4::CheckArgument(isClosure(), *this, "CVC3::Expr::getVars(): not a closure Expr: `%s'", toString().c_str());
+ CompatCheckArgument(isClosure(), *this, "CVC3::Expr::getVars(): not a closure Expr: `%s'", toString().c_str());
const vector<CVC4::Expr>& kids = (*this)[0].getChildren();
vector<Expr> v;
for(vector<CVC4::Expr>::const_iterator i = kids.begin(); i != kids.end(); ++i) {
}
Expr Expr::getBody() const {
- CVC4::CheckArgument(isClosure(), *this, "CVC3::Expr::getBody(): not a closure Expr: `%s'", toString().c_str());
+ CompatCheckArgument(isClosure(), *this, "CVC3::Expr::getBody(): not a closure Expr: `%s'", toString().c_str());
return (*this)[1];
}
}
const Rational& Expr::getRational() const {
- CVC4::CheckArgument(isRational(), *this, "CVC3::Expr::getRational(): not a rational Expr: `%s'", toString().c_str());
+ CompatCheckArgument(isRational(), *this, "CVC3::Expr::getRational(): not a rational Expr: `%s'", toString().c_str());
return getConst<CVC4::Rational>();
}
}
std::vector< std::vector<Expr> > Expr::getTriggers() const {
- CVC4::CheckArgument(isClosure(), *this, "getTriggers() called on non-closure expr");
+ CompatCheckArgument(isClosure(), *this,
+ "getTriggers() called on non-closure expr");
if(getNumChildren() < 3) {
// no triggers for this quantifier
return vector< vector<Expr> >();
}
CLFlag& CLFlag::operator=(bool b) {
- CVC4::CheckArgument(d_tp == CLFLAG_BOOL, this);
+ CompatCheckArgument(d_tp == CLFLAG_BOOL, this);
d_data.b = b;
return *this;
}
CLFlag& CLFlag::operator=(int i) {
- CVC4::CheckArgument(d_tp == CLFLAG_INT, this);
+ CompatCheckArgument(d_tp == CLFLAG_INT, this);
d_data.i = i;
return *this;
}
CLFlag& CLFlag::operator=(const std::string& s) {
- CVC4::CheckArgument(d_tp == CLFLAG_STRING, this);
+ CompatCheckArgument(d_tp == CLFLAG_STRING, this);
*d_data.s = s;
return *this;
}
CLFlag& CLFlag::operator=(const char* s) {
- CVC4::CheckArgument(d_tp == CLFLAG_STRING, this);
+ CompatCheckArgument(d_tp == CLFLAG_STRING, this);
*d_data.s = s;
return *this;
}
CLFlag& CLFlag::operator=(const std::pair<string, bool>& p) {
- CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this);
+ CompatCheckArgument(d_tp == CLFLAG_STRVEC, this);
d_data.sv->push_back(p);
return *this;
}
CLFlag& CLFlag::operator=(const std::vector<std::pair<string, bool> >& sv) {
- CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this);
+ CompatCheckArgument(d_tp == CLFLAG_STRVEC, this);
*d_data.sv = sv;
return *this;
}
}
const bool& CLFlag::getBool() const {
- CVC4::CheckArgument(d_tp == CLFLAG_BOOL, this);
+ CompatCheckArgument(d_tp == CLFLAG_BOOL, this);
return d_data.b;
}
const int& CLFlag::getInt() const {
- CVC4::CheckArgument(d_tp == CLFLAG_INT, this);
+ CompatCheckArgument(d_tp == CLFLAG_INT, this);
return d_data.i;
}
const std::string& CLFlag::getString() const {
- CVC4::CheckArgument(d_tp == CLFLAG_STRING, this);
+ CompatCheckArgument(d_tp == CLFLAG_STRING, this);
return *d_data.s;
}
const std::vector<std::pair<string, bool> >& CLFlag::getStrVec() const {
- CVC4::CheckArgument(d_tp == CLFLAG_STRVEC, this);
+ CompatCheckArgument(d_tp == CLFLAG_STRVEC, this);
return *d_data.sv;
}
const CLFlag& CLFlags::getFlag(const std::string& name) const {
FlagMap::const_iterator i = d_map.find(name);
- CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+ CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
return (*i).second;
}
void CLFlags::setFlag(const std::string& name, const CLFlag& f) {
FlagMap::iterator i = d_map.find(name);
- CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
- CVC4::CheckArgument((*i).second.getType() == f.getType(), f,
+ CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+ CompatCheckArgument((*i).second.getType() == f.getType(), f,
"Command-line flag `%s' has type %s, but caller tried to set to a %s.",
name.c_str(),
toString((*i).second.getType()).c_str(),
void CLFlags::setFlag(const std::string& name, bool b) {
FlagMap::iterator i = d_map.find(name);
- CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+ CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
(*i).second = b;
}
void CLFlags::setFlag(const std::string& name, int i) {
FlagMap::iterator it = d_map.find(name);
- CVC4::CheckArgument(it != d_map.end(), name, "No command-line flag by that name, or not supported.");
+ CompatCheckArgument(it != d_map.end(), name, "No command-line flag by that name, or not supported.");
(*it).second = i;
}
void CLFlags::setFlag(const std::string& name, const std::string& s) {
FlagMap::iterator i = d_map.find(name);
- CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+ CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
(*i).second = s;
}
void CLFlags::setFlag(const std::string& name, const char* s) {
FlagMap::iterator i = d_map.find(name);
- CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+ CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
(*i).second = s;
}
void CLFlags::setFlag(const std::string& name, const std::pair<string, bool>& p) {
FlagMap::iterator i = d_map.find(name);
- CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+ CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
(*i).second = p;
}
void CLFlags::setFlag(const std::string& name,
const std::vector<std::pair<string, bool> >& sv) {
FlagMap::iterator i = d_map.find(name);
- CVC4::CheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
+ CompatCheckArgument(i != d_map.end(), name, "No command-line flag by that name, or not supported.");
(*i).second = sv;
}
Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) {
bool noLowerBound = l.getType().isString() && l.getConst<CVC4::String>() == "_NEGINF";
bool noUpperBound = r.getType().isString() && r.getConst<CVC4::String>() == "_POSINF";
- CVC4::CheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l);
- CVC4::CheckArgument(noUpperBound || (r.getKind() == CVC4::kind::CONST_RATIONAL && r.getConst<Rational>().isIntegral()), r);
+ CompatCheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l);
+ CompatCheckArgument(noUpperBound || (r.getKind() == CVC4::kind::CONST_RATIONAL && r.getConst<Rational>().isIntegral()), r);
CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst<Rational>().getNumerator());
CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst<Rational>().getNumerator());
return d_em->mkSubrangeType(CVC4::SubrangeBounds(bl, br));
Type ValidityChecker::recordType(const std::vector<std::string>& fields,
const std::vector<Type>& types) {
- CVC4::CheckArgument(fields.size() == types.size() && fields.size() > 0,
+ CompatCheckArgument(fields.size() == types.size() && fields.size() > 0,
"invalid vector length(s) in recordType()");
std::vector< std::pair<std::string, CVC4::Type> > fieldSpecs;
for(unsigned i = 0; i < fields.size(); ++i) {
const std::string& constructor,
const std::vector<std::string>& selectors,
const std::vector<Expr>& types) {
- CVC4::CheckArgument(selectors.size() == types.size(), types, "expected selectors and types vectors to be of equal length");
+ CompatCheckArgument(selectors.size() == types.size(), types,
+ "expected selectors and types vectors to be of equal"
+ "length");
vector<string> cv;
vector< vector<string> > sv;
vector< vector<Expr> > tv;
const std::vector<std::string>& constructors,
const std::vector<std::vector<std::string> >& selectors,
const std::vector<std::vector<Expr> >& types) {
- CVC4::CheckArgument(constructors.size() == selectors.size(), selectors, "expected constructors and selectors vectors to be of equal length");
- CVC4::CheckArgument(constructors.size() == types.size(), types, "expected constructors and types vectors to be of equal length");
+ CompatCheckArgument(constructors.size() == selectors.size(), selectors,
+ "Expected constructors and selectors vectors to be of "
+ "equal length.");
+ CompatCheckArgument(constructors.size() == types.size(), types,
+ "Expected constructors and types vectors to be of equal "
+ "length.");
vector<string> nv;
vector< vector<string> > cv;
vector< vector< vector<string> > > sv;
const std::vector<std::vector<std::vector<Expr> > >& types,
std::vector<Type>& returnTypes) {
- CVC4::CheckArgument(names.size() == constructors.size(), constructors, "expected names and constructors vectors to be of equal length");
- CVC4::CheckArgument(names.size() == selectors.size(), selectors, "expected names and selectors vectors to be of equal length");
- CVC4::CheckArgument(names.size() == types.size(), types, "expected names and types vectors to be of equal length");
+ CompatCheckArgument(names.size() == constructors.size(), constructors,
+ "Expected names and constructors vectors to be of equal "
+ "length.");
+ CompatCheckArgument(names.size() == selectors.size(), selectors,
+ "Expected names and selectors vectors to be of equal "
+ "length.");
+ CompatCheckArgument(names.size() == types.size(), types,
+ "Expected names and types vectors to be of equal "
+ "length.");
vector<CVC4::Datatype> dv;
// Set up the datatype specifications.
for(unsigned i = 0; i < names.size(); ++i) {
CVC4::Datatype dt(names[i], false);
- CVC4::CheckArgument(constructors[i].size() == selectors[i].size(), "expected sub-vectors in constructors and selectors vectors to match in size");
- CVC4::CheckArgument(constructors[i].size() == types[i].size(), "expected sub-vectors in constructors and types vectors to match in size");
+ CompatCheckArgument(constructors[i].size() == selectors[i].size(),
+ "Expected sub-vectors in constructors and selectors "
+ "vectors to match in size.");
+ CompatCheckArgument(constructors[i].size() == types[i].size(),
+ "Expected sub-vectors in constructors and types "
+ "vectors to match in size.");
for(unsigned j = 0; j < constructors[i].size(); ++j) {
CVC4::DatatypeConstructor ctor(constructors[i][j]);
- CVC4::CheckArgument(selectors[i][j].size() == types[i][j].size(), types, "expected sub-vectors in selectors and types vectors to match in size");
+ CompatCheckArgument(selectors[i][j].size() == types[i][j].size(), types,
+ "Expected sub-vectors in selectors and types vectors "
+ "to match in size.");
for(unsigned k = 0; k < selectors[i][j].size(); ++k) {
if(types[i][j][k].getType().isString()) {
- ctor.addArg(selectors[i][j][k], CVC4::DatatypeUnresolvedType(types[i][j][k].getConst<CVC4::String>().toString()));
+ CVC4::DatatypeUnresolvedType unresolvedName =
+ types[i][j][k].getConst<CVC4::String>().toString();
+ ctor.addArg(selectors[i][j][k], unresolvedName);
} else {
ctor.addArg(selectors[i][j][k], exprToType(types[i][j][k]));
}
}
for(CVC4::Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
// For each constructor, register its name and its selectors names.
- CVC4::CheckArgument(d_constructors.find((*j).getName()) == d_constructors.end(), constructors, "cannot have two constructors with the same name in a ValidityChecker");
+ CompatCheckArgument(
+ d_constructors.find((*j).getName()) == d_constructors.end(),
+ constructors,
+ "Cannot have two constructors with the same name in a "
+ "ValidityChecker.");
d_constructors[(*j).getName()] = &dt;
for(CVC4::DatatypeConstructor::const_iterator k = (*j).begin(); k != (*j).end(); ++k) {
- CVC4::CheckArgument(d_selectors.find((*k).getName()) == d_selectors.end(), selectors, "cannot have two selectors with the same name in a ValidityChecker");
+ CompatCheckArgument(
+ d_selectors.find((*k).getName()) == d_selectors.end(), selectors,
+ "Cannot have two selectors with the same name in a "
+ "ValidityChecker.");
d_selectors[(*k).getName()] = make_pair(&dt, (*j).getName());
}
}
}
Type ValidityChecker::bitvecType(int n) {
- CVC4::CheckArgument(n >= 0, n, "cannot construct a bitvector type of negative size");
+ CompatCheckArgument(n >= 0, n,
+ "Cannot construct a bitvector type of negative size.");
return d_em->mkBitVectorType(n);
}
Expr ValidityChecker::varExpr(const std::string& name, const Type& type,
const Expr& def) {
- CVC4::CheckArgument(def.getType() == type, def, "expected types to match");
+ CompatCheckArgument(def.getType() == type, def, "expected types to match");
d_parserContext->defineVar(name, def);
return def;
}
Expr ValidityChecker::andExpr(const std::vector<Expr>& children) {
// AND must have at least 2 children
- CVC4::CheckArgument(children.size() > 0, children);
+ CompatCheckArgument(children.size() > 0, children);
return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::AND, *reinterpret_cast<const vector<CVC4::Expr>*>(&children)));
}
Expr ValidityChecker::orExpr(const std::vector<Expr>& children) {
// OR must have at least 2 children
- CVC4::CheckArgument(children.size() > 0, children);
+ CompatCheckArgument(children.size() > 0, children);
return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::OR, *reinterpret_cast<const vector<CVC4::Expr>*>(&children)));
}
}
Expr ValidityChecker::distinctExpr(const std::vector<Expr>& children) {
- CVC4::CheckArgument(children.size() > 1, children, "it makes no sense to create a `distinct' expression with only one child");
+ CompatCheckArgument(children.size() > 1, children, "it makes no sense to create a `distinct' expression with only one child");
const vector<CVC4::Expr>& v =
*reinterpret_cast<const vector<CVC4::Expr>*>(&children);
return d_em->mkExpr(CVC4::kind::DISTINCT, v);
Op ValidityChecker::createOp(const std::string& name, const Type& type,
const Expr& def) {
- CVC4::CheckArgument(def.getType() == type, type,
+ CompatCheckArgument(def.getType() == type, type,
"Type mismatch in ValidityChecker::createOp(): `%s' defined to an "
"expression of type %s but ascribed as type %s", name.c_str(),
def.getType().toString().c_str(), type.toString().c_str());
if(n.find(".") == string::npos) {
return d_em->mkConst(Rational(n, base));
} else {
- CVC4::CheckArgument(base == 10, base, "unsupported base for decimal parsing");
+ CompatCheckArgument(base == 10, base, "unsupported base for decimal parsing");
return d_em->mkConst(Rational::fromDecimal(n));
}
}
Expr ValidityChecker::plusExpr(const std::vector<Expr>& children) {
// PLUS must have at least 2 children
- CVC4::CheckArgument(children.size() > 0, children);
+ CompatCheckArgument(children.size() > 0, children);
return (children.size() == 1) ? children[0] : Expr(d_em->mkExpr(CVC4::kind::PLUS, *reinterpret_cast<const vector<CVC4::Expr>*>(&children)));
}
Expr ValidityChecker::newBVConstExpr(const Rational& r, int len) {
// implementation based on CVC3's TheoryBitvector::newBVConstExpr()
- CVC4::CheckArgument(r.getDenominator() == 1, r, "ValidityChecker::newBVConstExpr: "
- "not an integer: `%s'", r.toString().c_str());
- CVC4::CheckArgument(len > 0, len, "ValidityChecker::newBVConstExpr: "
- "len = %d", len);
+ CompatCheckArgument(r.getDenominator() == 1, r,
+ "ValidityChecker::newBVConstExpr: "
+ "not an integer: `%s'", r.toString().c_str());
+ CompatCheckArgument(len > 0, len, "ValidityChecker::newBVConstExpr: "
+ "len = %d", len);
string s(r.toString(2));
size_t strsize = s.size();
}
Expr ValidityChecker::newConcatExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only concat a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only concat a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only concat a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only concat a bitvector, not a `%s'", t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_CONCAT, t1, t2);
}
}
Expr ValidityChecker::newBVExtractExpr(const Expr& e, int hi, int low) {
- CVC4::CheckArgument(e.getType().isBitVector(), e, "can only bvextract from a bitvector, not a `%s'", e.getType().toString().c_str());
- CVC4::CheckArgument(hi >= low, hi, "extraction [%d:%d] is bad; possibly inverted?", hi, low);
- CVC4::CheckArgument(low >= 0, low, "extraction [%d:%d] is bad (negative)", hi, low);
- CVC4::CheckArgument(CVC4::BitVectorType(e.getType()).getSize() > unsigned(hi), hi, "bitvector is of size %u, extraction [%d:%d] is off-the-end", CVC4::BitVectorType(e.getType()).getSize(), hi, low);
+ CompatCheckArgument(e.getType().isBitVector(), e,
+ "can only bvextract from a bitvector, not a `%s'",
+ e.getType().toString().c_str());
+ CompatCheckArgument(hi >= low, hi,
+ "extraction [%d:%d] is bad; possibly inverted?", hi, low);
+ CompatCheckArgument(low >= 0, low,
+ "extraction [%d:%d] is bad (negative)", hi, low);
+ CompatCheckArgument(CVC4::BitVectorType(e.getType()).getSize() > unsigned(hi),
+ hi,
+ "bitvector is of size %u, extraction [%d:%d] is off-the-end",
+ CVC4::BitVectorType(e.getType()).getSize(), hi, low);
return d_em->mkExpr(CVC4::kind::BITVECTOR_EXTRACT,
- d_em->mkConst(CVC4::BitVectorExtract(hi, low)), e);
+ d_em->mkConst(CVC4::BitVectorExtract(hi, low)), e);
}
Expr ValidityChecker::newBVNegExpr(const Expr& t1) {
// CVC3's BVNEG => SMT-LIBv2 bvnot
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvneg a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1,
+ "can only bvneg a bitvector, not a `%s'",
+ t1.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_NOT, t1);
}
Expr ValidityChecker::newBVAndExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvand a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvand a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1,
+ "can only bvand a bitvector, not a `%s'",
+ t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2,
+ "can only bvand a bitvector, not a `%s'",
+ t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_AND, t1, t2);
}
Expr ValidityChecker::newBVAndExpr(const std::vector<Expr>& kids) {
// BITVECTOR_AND is not N-ary in CVC4
- CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_AND must have at least 2 children");
+ CompatCheckArgument(kids.size() > 1, kids,
+ "BITVECTOR_AND must have at least 2 children");
std::vector<Expr>::const_reverse_iterator i = kids.rbegin();
Expr e = *i++;
while(i != kids.rend()) {
}
Expr ValidityChecker::newBVOrExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvor a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvor a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1,
+ "can only bvor a bitvector, not a `%s'",
+ t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2,
+ "can only bvor a bitvector, not a `%s'",
+ t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_OR, t1, t2);
}
Expr ValidityChecker::newBVOrExpr(const std::vector<Expr>& kids) {
// BITVECTOR_OR is not N-ary in CVC4
- CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_OR must have at least 2 children");
+ CompatCheckArgument(kids.size() > 1, kids,
+ "BITVECTOR_OR must have at least 2 children");
std::vector<Expr>::const_reverse_iterator i = kids.rbegin();
Expr e = *i++;
while(i != kids.rend()) {
}
Expr ValidityChecker::newBVXorExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvxor a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvxor a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1,
+ "can only bvxor a bitvector, not a `%s'",
+ t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2,
+ "can only bvxor a bitvector, not a `%s'",
+ t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_XOR, t1, t2);
}
Expr ValidityChecker::newBVXorExpr(const std::vector<Expr>& kids) {
// BITVECTOR_XOR is not N-ary in CVC4
- CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_XOR must have at least 2 children");
+ CompatCheckArgument(kids.size() > 1, kids,
+ "BITVECTOR_XOR must have at least 2 children");
std::vector<Expr>::const_reverse_iterator i = kids.rbegin();
Expr e = *i++;
while(i != kids.rend()) {
}
Expr ValidityChecker::newBVXnorExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvxnor a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvxnor a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1,
+ "can only bvxnor a bitvector, not a `%s'",
+ t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2,
+ "can only bvxnor a bitvector, not a `%s'",
+ t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_XNOR, t1, t2);
}
Expr ValidityChecker::newBVXnorExpr(const std::vector<Expr>& kids) {
// BITVECTOR_XNOR is not N-ary in CVC4
- CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_XNOR must have at least 2 children");
+ CompatCheckArgument(kids.size() > 1, kids,
+ "BITVECTOR_XNOR must have at least 2 children");
std::vector<Expr>::const_reverse_iterator i = kids.rbegin();
Expr e = *i++;
while(i != kids.rend()) {
}
Expr ValidityChecker::newBVNandExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvnand a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvnand a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1,
+ "can only bvnand a bitvector, not a `%s'",
+ t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2,
+ "can only bvnand a bitvector, not a `%s'",
+ t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_NAND, t1, t2);
}
Expr ValidityChecker::newBVNorExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvnor a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvnor a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1,
+ "can only bvnor a bitvector, not a `%s'",
+ t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2,
+ "can only bvnor a bitvector, not a `%s'",
+ t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_NOR, t1, t2);
}
Expr ValidityChecker::newBVCompExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvcomp a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvcomp a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvcomp a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvcomp a bitvector, not a `%s'", t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_COMP, t1, t2);
}
Expr ValidityChecker::newBVLTExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvlt a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvlt a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvlt a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvlt a bitvector, not a `%s'", t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_ULT, t1, t2);
}
Expr ValidityChecker::newBVLEExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvle a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvle a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvle a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvle a bitvector, not a `%s'", t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_ULE, t1, t2);
}
Expr ValidityChecker::newBVSLTExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvslt a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvslt a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvslt a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvslt a bitvector, not a `%s'", t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_SLT, t1, t2);
}
Expr ValidityChecker::newBVSLEExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsle a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsle a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsle a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvsle a bitvector, not a `%s'", t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_SLE, t1, t2);
}
Expr ValidityChecker::newSXExpr(const Expr& t1, int len) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only sx a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(len >= 0, len, "must sx by a positive integer");
- CVC4::CheckArgument(unsigned(len) >= CVC4::BitVectorType(t1.getType()).getSize(), len, "cannot sx by something smaller than the bitvector (%d < %u)", len, CVC4::BitVectorType(t1.getType()).getSize());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only sx a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(len >= 0, len, "must sx by a positive integer");
+ CompatCheckArgument(unsigned(len) >= CVC4::BitVectorType(t1.getType()).getSize(), len, "cannot sx by something smaller than the bitvector (%d < %u)", len, CVC4::BitVectorType(t1.getType()).getSize());
return d_em->mkExpr(CVC4::kind::BITVECTOR_SIGN_EXTEND,
d_em->mkConst(CVC4::BitVectorSignExtend(len)), t1);
}
Expr ValidityChecker::newBVUminusExpr(const Expr& t1) {
// CVC3's BVUMINUS => SMT-LIBv2 bvneg
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvuminus a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvuminus a bitvector, not a `%s'", t1.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_NEG, t1);
}
Expr ValidityChecker::newBVSubExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsub a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsub by a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsub a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvsub by a bitvector, not a `%s'", t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_SUB, t1, t2);
}
// Copied from CVC3's bitvector theory: makes bitvector expression "e"
// into "len" bits, by zero-padding, or extracting least-significant bits.
Expr ValidityChecker::bvpad(int len, const Expr& e) {
- CVC4::CheckArgument(len >= 0, len,
+ CompatCheckArgument(len >= 0, len,
"padding length must be a non-negative integer, not %d", len);
- CVC4::CheckArgument(e.getType().isBitVector(), e,
+ CompatCheckArgument(e.getType().isBitVector(), e,
"input to bitvector operation must be a bitvector");
unsigned size = CVC4::BitVectorType(e.getType()).getSize();
Expr ValidityChecker::newBVPlusExpr(int numbits, const std::vector<Expr>& kids) {
// BITVECTOR_PLUS is not N-ary in CVC4
- CVC4::CheckArgument(kids.size() > 1, kids, "BITVECTOR_PLUS must have at least 2 children");
+ CompatCheckArgument(kids.size() > 1, kids, "BITVECTOR_PLUS must have at least 2 children");
std::vector<Expr>::const_reverse_iterator i = kids.rbegin();
Expr e = *i++;
while(i != kids.rend()) {
e = d_em->mkExpr(CVC4::kind::BITVECTOR_PLUS, bvpad(numbits, *i++), e);
}
unsigned size = CVC4::BitVectorType(e.getType()).getSize();
- CVC4::CheckArgument(unsigned(numbits) == size, numbits,
+ CompatCheckArgument(unsigned(numbits) == size, numbits,
"argument must match computed size of bitvector sum: "
"passed size == %u, computed size == %u", numbits, size);
return e;
}
Expr ValidityChecker::newBVPlusExpr(int numbits, const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvplus a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvplus a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvplus a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvplus a bitvector, not a `%s'", t2.getType().toString().c_str());
Expr e = d_em->mkExpr(CVC4::kind::BITVECTOR_PLUS, bvpad(numbits, t1), bvpad(numbits, t2));
unsigned size = CVC4::BitVectorType(e.getType()).getSize();
- CVC4::CheckArgument(unsigned(numbits) == size, numbits,
+ CompatCheckArgument(unsigned(numbits) == size, numbits,
"argument must match computed size of bitvector sum: "
"passed size == %u, computed size == %u", numbits, size);
return e;
}
Expr ValidityChecker::newBVMultExpr(int numbits, const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvmult a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvmult by a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvmult a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvmult by a bitvector, not a `%s'", t2.getType().toString().c_str());
Expr e = d_em->mkExpr(CVC4::kind::BITVECTOR_MULT, bvpad(numbits, t1), bvpad(numbits, t2));
unsigned size = CVC4::BitVectorType(e.getType()).getSize();
- CVC4::CheckArgument(unsigned(numbits) == size, numbits,
+ CompatCheckArgument(unsigned(numbits) == size, numbits,
"argument must match computed size of bitvector product: "
"passed size == %u, computed size == %u", numbits, size);
return e;
}
Expr ValidityChecker::newBVUDivExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvudiv a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvudiv by a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvudiv a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvudiv by a bitvector, not a `%s'", t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_UDIV, t1, t2);
}
Expr ValidityChecker::newBVURemExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvurem a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvurem by a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvurem a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvurem by a bitvector, not a `%s'", t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_UREM, t1, t2);
}
Expr ValidityChecker::newBVSDivExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsdiv a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsdiv by a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsdiv a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvsdiv by a bitvector, not a `%s'", t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_SDIV, t1, t2);
}
Expr ValidityChecker::newBVSRemExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsrem a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsrem by a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsrem a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvsrem by a bitvector, not a `%s'", t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_SREM, t1, t2);
}
Expr ValidityChecker::newBVSModExpr(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only bvsmod a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only bvsmod by a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only bvsmod a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only bvsmod by a bitvector, not a `%s'", t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_SMOD, t1, t2);
}
Expr ValidityChecker::newFixedLeftShiftExpr(const Expr& t1, int r) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only left-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(r >= 0, r, "left shift amount must be >= 0 (you passed %d)", r);
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only left-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(r >= 0, r, "left shift amount must be >= 0 (you passed %d)", r);
// Defined in:
// http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit
return d_em->mkExpr(CVC4::kind::BITVECTOR_CONCAT, t1, d_em->mkConst(CVC4::BitVector(r)));
}
Expr ValidityChecker::newFixedConstWidthLeftShiftExpr(const Expr& t1, int r) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(r >= 0, r, "const-width left shift amount must be >= 0 (you passed %d)", r);
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(r >= 0, r, "const-width left shift amount must be >= 0 (you passed %d)", r);
// just turn it into a BVSHL
return d_em->mkExpr(CVC4::kind::BITVECTOR_SHL, t1, d_em->mkConst(CVC4::BitVector(CVC4::BitVectorType(t1.getType()).getSize(), unsigned(r))));
}
Expr ValidityChecker::newFixedRightShiftExpr(const Expr& t1, int r) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(r >= 0, r, "right shift amount must be >= 0 (you passed %d)", r);
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(r >= 0, r, "right shift amount must be >= 0 (you passed %d)", r);
// Defined in:
// http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit
// Should be equivalent to a BVLSHR; just turn it into that.
}
Expr ValidityChecker::newBVSHL(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_SHL, t1, t2);
}
Expr ValidityChecker::newBVLSHR(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_LSHR, t1, t2);
}
Expr ValidityChecker::newBVASHR(const Expr& t1, const Expr& t2) {
- CVC4::CheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
- CVC4::CheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str());
+ CompatCheckArgument(t1.getType().isBitVector(), t1, "can only right-shift a bitvector, not a `%s'", t1.getType().toString().c_str());
+ CompatCheckArgument(t2.getType().isBitVector(), t2, "can only right-shift by a bitvector, not a `%s'", t2.getType().toString().c_str());
return d_em->mkExpr(CVC4::kind::BITVECTOR_ASHR, t1, t2);
}
}
Expr ValidityChecker::tupleSelectExpr(const Expr& tuple, int index) {
- CVC4::CheckArgument(index >= 0 && index < tuple.getNumChildren(),
+ CompatCheckArgument(index >= 0 && index < tuple.getNumChildren(),
"invalid index in tuple select");
return d_em->mkExpr(d_em->mkConst(CVC4::TupleSelect(index)), tuple);
}
Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index,
const Expr& newValue) {
- CVC4::CheckArgument(index >= 0 && index < tuple.getNumChildren(),
+ CompatCheckArgument(index >= 0 && index < tuple.getNumChildren(),
"invalid index in tuple update");
return d_em->mkExpr(d_em->mkConst(CVC4::TupleUpdate(index)), tuple, newValue);
}
Expr ValidityChecker::datatypeConsExpr(const std::string& constructor, const std::vector<Expr>& args) {
ConstructorMap::const_iterator i = d_constructors.find(constructor);
- CVC4::CheckArgument(i != d_constructors.end(), constructor, "no such constructor");
+ CompatCheckArgument(i != d_constructors.end(), constructor, "no such constructor");
const CVC4::Datatype& dt = *(*i).second;
const CVC4::DatatypeConstructor& ctor = dt[constructor];
- CVC4::CheckArgument(ctor.getNumArgs() == args.size(), args, "arity mismatch in constructor application");
+ CompatCheckArgument(ctor.getNumArgs() == args.size(), args, "arity mismatch in constructor application");
return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, ctor.getConstructor(), vector<CVC4::Expr>(args.begin(), args.end()));
}
Expr ValidityChecker::datatypeSelExpr(const std::string& selector, const Expr& arg) {
SelectorMap::const_iterator i = d_selectors.find(selector);
- CVC4::CheckArgument(i != d_selectors.end(), selector, "no such selector");
+ CompatCheckArgument(i != d_selectors.end(), selector, "no such selector");
const CVC4::Datatype& dt = *(*i).second.first;
string constructor = (*i).second.second;
const CVC4::DatatypeConstructor& ctor = dt[constructor];
Expr ValidityChecker::datatypeTestExpr(const std::string& constructor, const Expr& arg) {
ConstructorMap::const_iterator i = d_constructors.find(constructor);
- CVC4::CheckArgument(i != d_constructors.end(), constructor, "no such constructor");
+ CompatCheckArgument(i != d_constructors.end(), constructor, "no such constructor");
const CVC4::Datatype& dt = *(*i).second;
const CVC4::DatatypeConstructor& ctor = dt[constructor];
return d_em->mkExpr(CVC4::kind::APPLY_TESTER, ctor.getTester(), arg);
}
void ValidityChecker::getUserAssumptions(std::vector<Expr>& assumptions) {
- CVC4::CheckArgument(assumptions.empty(), assumptions, "assumptions arg must be empty");
+ CompatCheckArgument(assumptions.empty(), assumptions, "assumptions arg must be empty");
vector<CVC4::Expr> v = d_smt->getAssertions();
assumptions.swap(*reinterpret_cast<vector<Expr>*>(&v));
}
}
FormulaValue ValidityChecker::value(const Expr& e) {
- CVC4::CheckArgument(e.getType() == d_em->booleanType(), e, "argument must be a formula");
+ CompatCheckArgument(e.getType() == d_em->booleanType(), e, "argument must be a formula");
try {
return d_smt->getValue(e).getConst<bool>() ? TRUE_VAL : FALSE_VAL;
} catch(CVC4::Exception& e) {
}
bool ValidityChecker::inconsistent(std::vector<Expr>& assumptions) {
- CVC4::CheckArgument(assumptions.empty(), assumptions, "assumptions vector should be empty on entry");
+ CompatCheckArgument(assumptions.empty(), assumptions, "assumptions vector should be empty on entry");
if(d_smt->checkSat() == CVC4::Result::UNSAT) {
// supposed to be a minimal set, but CVC4 doesn't support that
d_smt->getAssertions().swap(*reinterpret_cast<std::vector<CVC4::Expr>*>(&assumptions));
}
void ValidityChecker::popto(int stackLevel) {
- CVC4::CheckArgument(stackLevel >= 0, stackLevel,
+ CompatCheckArgument(stackLevel >= 0, stackLevel,
"Cannot pop to a negative stack level %d", stackLevel);
- CVC4::CheckArgument(unsigned(stackLevel) <= d_stackLevel, stackLevel,
+ CompatCheckArgument(unsigned(stackLevel) <= d_stackLevel, stackLevel,
"Cannot pop to a stack level higher than the current one! "
"At stack level %u, user requested stack level %d",
d_stackLevel, stackLevel);
}
void ValidityChecker::poptoScope(int scopeLevel) {
- CVC4::CheckArgument(scopeLevel >= 0, scopeLevel,
+ CompatCheckArgument(scopeLevel >= 0, scopeLevel,
"Cannot pop to a negative scope level %d", scopeLevel);
- CVC4::CheckArgument(unsigned(scopeLevel) <= d_parserContext->scopeLevel(),
+ CompatCheckArgument(unsigned(scopeLevel) <= d_parserContext->scopeLevel(),
scopeLevel,
"Cannot pop to a scope level higher than the current one! "
"At scope level %u, user requested scope level %d",
namespace CVC4 {}
using namespace CVC4;
-#include <iostream>
-#include <vector>
+#include <cassert>
+#include <ext/hash_map>
+#include <iosfwd>
#include <set>
#include <string>
-#include <ext/hash_map>
#include <typeinfo>
-#include <cassert>
+#include <vector>
#include "base/exception.h"
#include "base/modal_exception.h"
#include <iostream>
+#include "base/cvc4_assert.h"
+#include "expr/expr.h"
+#include "expr/type.h"
+
using namespace std;
namespace CVC4 {
+ArrayStoreAll::ArrayStoreAll(const ArrayStoreAll& other)
+ : d_type(new ArrayType(other.getType()))
+ , d_expr(new Expr(other.getExpr())) {}
+
+ArrayStoreAll::~ArrayStoreAll() throw() {
+ delete d_expr;
+ delete d_type;
+}
+
+ArrayStoreAll& ArrayStoreAll::operator=(const ArrayStoreAll& other){
+ (*d_type) = other.getType();
+ (*d_expr) = other.getExpr();
+}
+
+ArrayStoreAll::ArrayStoreAll(const ArrayType& type, const Expr& expr)
+ throw(IllegalArgumentException)
+ : d_type(new ArrayType(type))
+ , d_expr(new Expr(expr))
+{
+ // this check is stronger than the assertion check in the expr manager that ArrayTypes are actually array types
+ // because this check is done in production builds too
+ PrettyCheckArgument(
+ type.isArray(),
+ type,
+ "array store-all constants can only be created for array types, not `%s'",
+ type.toString().c_str());
+
+ PrettyCheckArgument(
+ expr.getType().isComparableTo(type.getConstituentType()),
+ expr,
+ "expr type `%s' does not match constituent type of array type `%s'",
+ expr.getType().toString().c_str(),
+ type.toString().c_str());
+
+ PrettyCheckArgument(
+ expr.isConst(),
+ expr,
+ "ArrayStoreAll requires a constant expression");
+}
+
+
+const ArrayType& ArrayStoreAll::getType() const throw() {
+ return *d_type;
+}
+
+const Expr& ArrayStoreAll::getExpr() const throw() {
+ return *d_expr;
+}
+
+bool ArrayStoreAll::operator==(const ArrayStoreAll& asa) const throw() {
+ return getType() == asa.getType() && getExpr() == asa.getExpr();
+}
+
+
+bool ArrayStoreAll::operator<(const ArrayStoreAll& asa) const throw() {
+ return (getType() < asa.getType()) ||
+ (getType() == asa.getType() && getExpr() < asa.getExpr());
+}
+
+bool ArrayStoreAll::operator<=(const ArrayStoreAll& asa) const throw() {
+ return (getType() < asa.getType()) ||
+ (getType() == asa.getType() && getExpr() <= asa.getExpr());
+}
+
std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) {
return out << "__array_store_all__(" << asa.getType() << ", " << asa.getExpr() << ')';
}
+size_t ArrayStoreAllHashFunction::operator()(const ArrayStoreAll& asa) const {
+ return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr());
+}
+
+
}/* CVC4 namespace */
#pragma once
+#include <iosfwd>
+
+#include "base/exception.h"
+
namespace CVC4 {
// messy; Expr needs ArrayStoreAll (because it's the payload of a
// CONSTANT-kinded expression), and ArrayStoreAll needs Expr.
- class CVC4_PUBLIC ArrayStoreAll;
+ class Expr;
+ class ArrayType;
}/* CVC4 namespace */
-#include "expr/expr.h"
-#include "expr/type.h"
-#include <iostream>
namespace CVC4 {
class CVC4_PUBLIC ArrayStoreAll {
- const ArrayType d_type;
- const Expr d_expr;
-
public:
+ ArrayStoreAll(const ArrayStoreAll& other);
- ArrayStoreAll(ArrayType type, Expr expr) throw(IllegalArgumentException) :
- d_type(type),
- d_expr(expr) {
+ ArrayStoreAll& operator=(const ArrayStoreAll& other);
- // this check is stronger than the assertion check in the expr manager that ArrayTypes are actually array types
- // because this check is done in production builds too
- CheckArgument(type.isArray(), type, "array store-all constants can only be created for array types, not `%s'", type.toString().c_str());
+ ArrayStoreAll(const ArrayType& type, const Expr& expr)
+ throw(IllegalArgumentException);
- CheckArgument(expr.getType().isComparableTo(type.getConstituentType()), expr, "expr type `%s' does not match constituent type of array type `%s'", expr.getType().toString().c_str(), type.toString().c_str());
- CheckArgument(expr.isConst(), expr, "ArrayStoreAll requires a constant expression");
- }
+ ~ArrayStoreAll() throw();
- ~ArrayStoreAll() throw() {
- }
+ const ArrayType& getType() const throw();
- ArrayType getType() const throw() {
- return d_type;
- }
- Expr getExpr() const throw() {
- return d_expr;
- }
+ const Expr& getExpr() const throw();
+
+ bool operator==(const ArrayStoreAll& asa) const throw();
- bool operator==(const ArrayStoreAll& asa) const throw() {
- return d_type == asa.d_type && d_expr == asa.d_expr;
- }
bool operator!=(const ArrayStoreAll& asa) const throw() {
return !(*this == asa);
}
- bool operator<(const ArrayStoreAll& asa) const throw() {
- return d_type < asa.d_type ||
- (d_type == asa.d_type && d_expr < asa.d_expr);
- }
- bool operator<=(const ArrayStoreAll& asa) const throw() {
- return d_type < asa.d_type ||
- (d_type == asa.d_type && d_expr <= asa.d_expr);
- }
+ bool operator<(const ArrayStoreAll& asa) const throw();
+ bool operator<=(const ArrayStoreAll& asa) const throw();
bool operator>(const ArrayStoreAll& asa) const throw() {
return !(*this <= asa);
}
return !(*this < asa);
}
+private:
+ ArrayType* d_type;
+ Expr* d_expr;
};/* class ArrayStoreAll */
std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) CVC4_PUBLIC;
* Hash function for the ArrayStoreAll constants.
*/
struct CVC4_PUBLIC ArrayStoreAllHashFunction {
- inline size_t operator()(const ArrayStoreAll& asa) const {
- return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr());
- }
+ size_t operator()(const ArrayStoreAll& asa) const;
};/* struct ArrayStoreAllHashFunction */
}/* CVC4 namespace */
size_t Datatype::indexOf(Expr item) {
ExprManagerScope ems(item);
- CheckArgument(item.getType().isConstructor() ||
+ PrettyCheckArgument(item.getType().isConstructor() ||
item.getType().isTester() ||
item.getType().isSelector(),
item,
size_t Datatype::cindexOf(Expr item) {
ExprManagerScope ems(item);
- CheckArgument(item.getType().isSelector(),
+ PrettyCheckArgument(item.getType().isSelector(),
item,
"arg must be a datatype selector");
TNode n = Node::fromExpr(item);
const std::vector< DatatypeType >& paramReplacements)
throw(IllegalArgumentException, DatatypeResolutionException) {
- 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,
+ PrettyCheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
+ PrettyCheckArgument(!d_resolved, this, "cannot resolve a Datatype twice");
+ PrettyCheckArgument(resolutions.find(d_name) != resolutions.end(), resolutions,
"Datatype::resolve(): resolutions doesn't contain me!");
- CheckArgument(placeholders.size() == replacements.size(), placeholders,
+ PrettyCheckArgument(placeholders.size() == replacements.size(), placeholders,
"placeholders and replacements must be the same size");
- CheckArgument(paramTypes.size() == paramReplacements.size(), paramTypes,
+ PrettyCheckArgument(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");
+ PrettyCheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors");
DatatypeType self = (*resolutions.find(d_name)).second;
- CheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!");
+ PrettyCheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!");
d_resolved = true;
size_t index = 0;
for(std::vector<DatatypeConstructor>::iterator i = d_constructors.begin(), i_end = d_constructors.end(); i != i_end; ++i) {
}
void Datatype::addConstructor(const DatatypeConstructor& c) {
- CheckArgument(!d_resolved, this,
+ PrettyCheckArgument(!d_resolved, this,
"cannot add a constructor to a finalized Datatype");
d_constructors.push_back(c);
}
void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
- CheckArgument(!d_resolved, this,
+ PrettyCheckArgument(!d_resolved, this,
"cannot set sygus type to a finalized Datatype");
d_sygus_type = st;
d_sygus_bvl = bvl;
Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
- CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
std::vector< Type > processing;
computeCardinality( processing );
return d_card;
}
Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){
- CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
d_card = Cardinality::INTEGERS;
}else{
}
bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) {
- CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
if( d_card_rec_singleton==0 ){
Assert( d_card_u_assume.empty() );
std::vector< Type > processing;
}
bool Datatype::isFinite() const throw(IllegalArgumentException) {
- CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
+
// we're using some internals, so we have to set up this library context
ExprManagerScope ems(d_self);
TypeNode self = TypeNode::fromType(d_self);
}
bool Datatype::isUFinite() const throw(IllegalArgumentException) {
- CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
// we're using some internals, so we have to set up this library context
ExprManagerScope ems(d_self);
TypeNode self = TypeNode::fromType(d_self);
}
bool Datatype::isWellFounded() const throw(IllegalArgumentException) {
- CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
if( d_well_founded==0 ){
// we're using some internals, so we have to set up this library context
ExprManagerScope ems(d_self);
}
bool Datatype::computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException) {
- CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
return d_isCo;
}else{
}
Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
- CheckArgument(isResolved(), this, "this datatype is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
ExprManagerScope ems(d_self);
if( groundTerm.isNull() ){
if( !d_isCo ){
// if we get all the way here, we aren't well-founded
- CheckArgument(false, *this, "datatype is not well-founded, cannot construct a ground term!");
+ IllegalArgument(*this, "datatype is not well-founded, cannot construct a ground term!");
}else{
return groundTerm;
}
}
DatatypeType Datatype::getDatatypeType() const throw(IllegalArgumentException) {
- CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
- CheckArgument(!d_self.isNull(), *this);
+ PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
+ PrettyCheckArgument(!d_self.isNull(), *this);
return DatatypeType(d_self);
}
DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params)
const throw(IllegalArgumentException) {
- CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
- CheckArgument(!d_self.isNull() && DatatypeType(d_self).isParametric(), this);
+ PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
+ PrettyCheckArgument(!d_self.isNull() && DatatypeType(d_self).isParametric(), this);
return DatatypeType(d_self).instantiate(params);
}
}
const DatatypeConstructor& Datatype::operator[](size_t index) const {
- CheckArgument(index < getNumConstructors(), index, "index out of bounds");
+ PrettyCheckArgument(index < getNumConstructors(), index, "index out of bounds");
return d_constructors[index];
}
return *i;
}
}
- CheckArgument(false, name, "No such constructor `%s' of datatype `%s'", name.c_str(), d_name.c_str());
+ IllegalArgument(name, "No such constructor `%s' of datatype `%s'", name.c_str(), d_name.c_str());
}
Expr Datatype::getConstructor(std::string name) const {
const std::vector< DatatypeType >& paramReplacements, size_t cindex)
throw(IllegalArgumentException, DatatypeResolutionException) {
- CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
- CheckArgument(!isResolved(),
+ PrettyCheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
+ PrettyCheckArgument(!isResolved(),
"cannot resolve a Datatype constructor twice; "
"perhaps the same constructor was added twice, "
"or to two datatypes?");
d_name(name + '\0' + "is_" + name), // default tester name is "is_FOO"
d_tester(),
d_args() {
- CheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
+ PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
}
DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) :
d_name(name + '\0' + tester),
d_tester(),
d_args() {
- CheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
- CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
+ PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
+ PrettyCheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
}
void DatatypeConstructor::setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_args ){
// we're going to be a constant stuffed inside a node. So we stow
// the selector type away inside a var until resolution (when we can
// create the proper selector type)
- CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
- CheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type");
+ PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
+ PrettyCheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type");
// we're using some internals, so we have to set up this library context
ExprManagerScope ems(selectorType);
// we're going to be a constant stuffed inside a node. So we stow
// the selector type away after a NUL in the name string until
// resolution (when we can create the proper selector type)
- CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
- CheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type");
+ PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
+ PrettyCheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type");
d_args.push_back(DatatypeConstructorArg(selectorName + '\0' + selectorType.getName(), Expr()));
}
// the name string with a NUL to indicate that we have a
// self-selecting selector until resolution (when we can create the
// proper selector type)
- CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
+ PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
d_args.push_back(DatatypeConstructorArg(selectorName + '\0', Expr()));
}
}
Expr DatatypeConstructor::getConstructor() const {
- CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
return d_constructor;
}
Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
- CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
ExprManagerScope ems(d_constructor);
const Datatype& dt = Datatype::datatypeOf(d_constructor);
- CheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric");
+ PrettyCheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric");
DatatypeType dtt = dt.getDatatypeType();
Matcher m(dtt);
m.doMatching( TypeNode::fromType(dtt), TypeNode::fromType(returnType) );
}
Expr DatatypeConstructor::getTester() const {
- CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
return d_tester;
}
Expr DatatypeConstructor::getSygusOp() const {
- CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
return d_sygus_op;
}
Expr DatatypeConstructor::getSygusLetBody() const {
- CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
return d_sygus_let_body;
}
unsigned DatatypeConstructor::getNumSygusLetArgs() const {
- CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
return d_sygus_let_args.size();
}
Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const {
- CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
return d_sygus_let_args[i];
}
unsigned DatatypeConstructor::getNumSygusLetInputArgs() const {
- CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
return d_sygus_num_let_input_args;
}
bool DatatypeConstructor::isSygusIdFunc() const {
- CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body;
}
Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) {
- CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
Cardinality c = 1;
bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
- CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+
// we're using some internals, so we have to set up this library context
ExprManagerScope ems(d_constructor);
TNode self = Node::fromExpr(d_constructor);
self.setAttribute(DatatypeFiniteAttr(), true);
return true;
}
+
bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) {
- CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
// we're using some internals, so we have to set up this library context
ExprManagerScope ems(d_constructor);
TNode self = Node::fromExpr(d_constructor);
const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const {
- CheckArgument(index < getNumArgs(), index, "index out of bounds");
+ PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
return d_args[index];
}
return *i;
}
}
- CheckArgument(false, name, "No such arg `%s' of constructor `%s'", name.c_str(), d_name.c_str());
+ IllegalArgument(name, "No such arg `%s' of constructor `%s'", name.c_str(), d_name.c_str());
}
Expr DatatypeConstructor::getSelector(std::string name) const {
d_name(name),
d_selector(selector),
d_resolved(false) {
- CheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name");
+ PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name");
}
std::string DatatypeConstructorArg::getName() const throw() {
}
Expr DatatypeConstructorArg::getSelector() const {
- CheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor");
+ PrettyCheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor");
return d_selector;
}
Expr DatatypeConstructorArg::getConstructor() const {
- CheckArgument(isResolved(), this,
+ PrettyCheckArgument(isResolved(), this,
"cannot get a associated constructor for argument of an unresolved datatype constructor");
return d_constructor;
}
}
inline Type Datatype::getParameter( unsigned int i ) const {
- CheckArgument(isParametric(), this, "cannot get type parameter of a non-parametric datatype");
- CheckArgument(i < d_params.size(), i, "type parameter index out of range for datatype");
+ CheckArgument(isParametric(), this,
+ "Cannot get type parameter of a non-parametric datatype.");
+ CheckArgument(i < d_params.size(), i,
+ "Type parameter index out of range for datatype.");
return d_params[i];
}
inline std::vector<Type> Datatype::getParameters() const {
- CheckArgument(isParametric(), this, "cannot get type parameters of a non-parametric datatype");
+ CheckArgument(isParametric(), this,
+ "Cannot get type parameters of a non-parametric datatype.");
return d_params;
}
// compiler directs the user to the template file instead of the
// generated one. We don't want the user to modify the generated one,
// since it'll get overwritten on a later build.
-#line 32 "${template}"
+#line 33 "${template}"
#ifdef CVC4_STATISTICS_ON
#define INC_STAT(kind) \
Expr ExprManager::mkExpr(Kind kind, Expr child1) {
const kind::MetaKind mk = kind::metaKindOf(kind);
const unsigned n = 1 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
- CheckArgument(mk == kind::metakind::PARAMETERIZED ||
- mk == kind::metakind::OPERATOR, kind,
- "Only operator-style expressions are made with mkExpr(); "
- "to make variables and constants, see mkVar(), mkBoundVar(), "
- "and mkConst().");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
+ PrettyCheckArgument(
+ mk == kind::metakind::PARAMETERIZED ||
+ mk == kind::metakind::OPERATOR, kind,
+ "Only operator-style expressions are made with mkExpr(); "
+ "to make variables and constants, see mkVar(), mkBoundVar(), "
+ "and mkConst().");
+ PrettyCheckArgument(
+ n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
try {
INC_STAT(kind);
Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) {
const kind::MetaKind mk = kind::metaKindOf(kind);
const unsigned n = 2 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
- CheckArgument(mk == kind::metakind::PARAMETERIZED ||
- mk == kind::metakind::OPERATOR, kind,
- "Only operator-style expressions are made with mkExpr(); "
- "to make variables and constants, see mkVar(), mkBoundVar(), "
- "and mkConst().");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
+ PrettyCheckArgument(
+ mk == kind::metakind::PARAMETERIZED ||
+ mk == kind::metakind::OPERATOR, kind,
+ "Only operator-style expressions are made with mkExpr(); "
+ "to make variables and constants, see mkVar(), mkBoundVar(), "
+ "and mkConst().");
+ PrettyCheckArgument(
+ n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
try {
INC_STAT(kind);
Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) {
const kind::MetaKind mk = kind::metaKindOf(kind);
const unsigned n = 3 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
- CheckArgument(mk == kind::metakind::PARAMETERIZED ||
- mk == kind::metakind::OPERATOR, kind,
- "Only operator-style expressions are made with mkExpr(); "
- "to make variables and constants, see mkVar(), mkBoundVar(), "
- "and mkConst().");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
+ PrettyCheckArgument(
+ mk == kind::metakind::PARAMETERIZED ||
+ mk == kind::metakind::OPERATOR, kind,
+ "Only operator-style expressions are made with mkExpr(); "
+ "to make variables and constants, see mkVar(), mkBoundVar(), "
+ "and mkConst().");
+ PrettyCheckArgument(
+ n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
try {
INC_STAT(kind);
Expr child4) {
const kind::MetaKind mk = kind::metaKindOf(kind);
const unsigned n = 4 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
- CheckArgument(mk == kind::metakind::PARAMETERIZED ||
- mk == kind::metakind::OPERATOR, kind,
- "Only operator-style expressions are made with mkExpr(); "
- "to make variables and constants, see mkVar(), mkBoundVar(), "
- "and mkConst().");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
+ PrettyCheckArgument(
+ mk == kind::metakind::PARAMETERIZED ||
+ mk == kind::metakind::OPERATOR, kind,
+ "Only operator-style expressions are made with mkExpr(); "
+ "to make variables and constants, see mkVar(), mkBoundVar(), "
+ "and mkConst().");
+ PrettyCheckArgument(
+ n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
try {
INC_STAT(kind);
Expr child4, Expr child5) {
const kind::MetaKind mk = kind::metaKindOf(kind);
const unsigned n = 5 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
- CheckArgument(mk == kind::metakind::PARAMETERIZED ||
- mk == kind::metakind::OPERATOR, kind,
- "Only operator-style expressions are made with mkExpr(); "
- "to make variables and constants, see mkVar(), mkBoundVar(), "
- "and mkConst().");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
+ PrettyCheckArgument(
+ mk == kind::metakind::PARAMETERIZED ||
+ mk == kind::metakind::OPERATOR, kind,
+ "Only operator-style expressions are made with mkExpr(); "
+ "to make variables and constants, see mkVar(), mkBoundVar(), "
+ "and mkConst().");
+ PrettyCheckArgument(
+ n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
try {
INC_STAT(kind);
Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
const kind::MetaKind mk = kind::metaKindOf(kind);
const unsigned n = children.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
- CheckArgument(mk == kind::metakind::PARAMETERIZED ||
- mk == kind::metakind::OPERATOR, kind,
- "Only operator-style expressions are made with mkExpr(); "
- "to make variables and constants, see mkVar(), mkBoundVar(), "
- "and mkConst().");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
+ PrettyCheckArgument(
+ mk == kind::metakind::PARAMETERIZED ||
+ mk == kind::metakind::OPERATOR, kind,
+ "Only operator-style expressions are made with mkExpr(); "
+ "to make variables and constants, see mkVar(), mkBoundVar(), "
+ "and mkConst().");
+ PrettyCheckArgument(
+ n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
Expr ExprManager::mkExpr(Kind kind, Expr child1,
const std::vector<Expr>& otherChildren) {
const kind::MetaKind mk = kind::metaKindOf(kind);
- const unsigned n = otherChildren.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0) + 1;
- CheckArgument(mk == kind::metakind::PARAMETERIZED ||
- mk == kind::metakind::OPERATOR, kind,
- "Only operator-style expressions are made with mkExpr(); "
- "to make variables and constants, see mkVar(), mkBoundVar(), "
- "and mkConst().");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
+ const unsigned n =
+ otherChildren.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0) + 1;
+ PrettyCheckArgument(
+ mk == kind::metakind::PARAMETERIZED ||
+ mk == kind::metakind::OPERATOR, kind,
+ "Only operator-style expressions are made with mkExpr(); "
+ "to make variables and constants, see mkVar(), mkBoundVar(), "
+ "and mkConst().");
+ PrettyCheckArgument(
+ n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
Expr ExprManager::mkExpr(Expr opExpr) {
const unsigned n = 0;
Kind kind = NodeManager::operatorToKind(opExpr.getNode());
- CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
- "This Expr constructor is for parameterized kinds only");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
+ PrettyCheckArgument(
+ opExpr.getKind() == kind::BUILTIN ||
+ kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+ "This Expr constructor is for parameterized kinds only");
+ PrettyCheckArgument(
+ n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
try {
INC_STAT(kind);
Expr ExprManager::mkExpr(Expr opExpr, Expr child1) {
const unsigned n = 1;
Kind kind = NodeManager::operatorToKind(opExpr.getNode());
- CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
- "This Expr constructor is for parameterized kinds only");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
+ PrettyCheckArgument(
+ (opExpr.getKind() == kind::BUILTIN ||
+ kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
+ "This Expr constructor is for parameterized kinds only");
+ PrettyCheckArgument(
+ n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
try {
INC_STAT(kind);
Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) {
const unsigned n = 2;
Kind kind = NodeManager::operatorToKind(opExpr.getNode());
- CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
- "This Expr constructor is for parameterized kinds only");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
+ PrettyCheckArgument(
+ (opExpr.getKind() == kind::BUILTIN ||
+ kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
+ "This Expr constructor is for parameterized kinds only");
+ PrettyCheckArgument(
+ n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
try {
INC_STAT(kind);
Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) {
const unsigned n = 3;
Kind kind = NodeManager::operatorToKind(opExpr.getNode());
- CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+ PrettyCheckArgument(
+ (opExpr.getKind() == kind::BUILTIN ||
+ kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
"This Expr constructor is for parameterized kinds only");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+ PrettyCheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
"Exprs with kind %s must have at least %u children and "
"at most %u children (the one under construction has %u)",
kind::kindToString(kind).c_str(),
Expr child4) {
const unsigned n = 4;
Kind kind = NodeManager::operatorToKind(opExpr.getNode());
- CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
- "This Expr constructor is for parameterized kinds only");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
+ PrettyCheckArgument(
+ (opExpr.getKind() == kind::BUILTIN ||
+ kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
+ "This Expr constructor is for parameterized kinds only");
+
+ PrettyCheckArgument(
+ n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
+
NodeManagerScope nms(d_nodeManager);
try {
INC_STAT(kind);
Expr child4, Expr child5) {
const unsigned n = 5;
Kind kind = NodeManager::operatorToKind(opExpr.getNode());
- CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
- "This Expr constructor is for parameterized kinds only");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
+ PrettyCheckArgument(
+ (opExpr.getKind() == kind::BUILTIN ||
+ kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
+ "This Expr constructor is for parameterized kinds only");
+ PrettyCheckArgument(
+ n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
try {
INC_STAT(kind);
Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
const unsigned n = children.size();
Kind kind = NodeManager::operatorToKind(opExpr.getNode());
- CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
- "This Expr constructor is for parameterized kinds only");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
+ PrettyCheckArgument(
+ (opExpr.getKind() == kind::BUILTIN ||
+ kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
+ "This Expr constructor is for parameterized kinds only");
+ PrettyCheckArgument(
+ n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
}
Type type(d_nodeManager, typeNode);
DatatypeType dtt(type);
- CheckArgument(nameResolutions.find((*i).getName()) == nameResolutions.end(),
- datatypes,
- "cannot construct two datatypes at the same time "
- "with the same name `%s'",
- (*i).getName().c_str());
+ PrettyCheckArgument(
+ nameResolutions.find((*i).getName()) == nameResolutions.end(),
+ datatypes,
+ "cannot construct two datatypes at the same time "
+ "with the same name `%s'",
+ (*i).getName().c_str());
nameResolutions.insert(std::make_pair((*i).getName(), dtt));
dtts.push_back(dtt);
}
}
std::map<std::string, DatatypeType>::const_iterator resolver =
nameResolutions.find(name);
- CheckArgument(resolver != nameResolutions.end(),
- unresolvedTypes,
- "cannot resolve type `%s'; it's not among "
- "the datatypes being defined", name.c_str());
+ PrettyCheckArgument(
+ resolver != nameResolutions.end(),
+ unresolvedTypes,
+ "cannot resolve type `%s'; it's not among "
+ "the datatypes being defined", name.c_str());
// We will instruct the Datatype to substitute "*i" (the
// unresolved SortType used as a placeholder in complex types)
// with "(*resolver).second" (the DatatypeType we created in the
Expr ExprManager::mkAssociative(Kind kind,
const std::vector<Expr>& children) {
- CheckArgument( kind::isAssociative(kind), kind,
- "Illegal kind in mkAssociative: %s",
- kind::kindToString(kind).c_str());
+ PrettyCheckArgument(
+ kind::isAssociative(kind), kind,
+ "Illegal kind in mkAssociative: %s",
+ kind::kindToString(kind).c_str());
NodeManagerScope nms(d_nodeManager);
const unsigned int max = maxArity(kind);
**
** Public-facing expression interface, implementation.
**/
+#include "expr/expr.h"
+
+#include <iterator>
+#include <utility>
+#include <vector>
#include "base/cvc4_assert.h"
-#include "expr/expr.h"
#include "expr/node.h"
#include "expr/expr_manager_scope.h"
#include "expr/variable_type_map.h"
#include "expr/node_manager_attributes.h"
-#include <vector>
-#include <iterator>
-#include <utility>
-
${includes}
// This is a hack, but an important one: if there's an error, the
Expr Expr::getOperator() const {
ExprManagerScope ems(*this);
Assert(d_node != NULL, "Unexpected NULL expression pointer!");
- CheckArgument(d_node->hasOperator(), *this,
- "Expr::getOperator() called on an Expr with no operator");
+ PrettyCheckArgument(d_node->hasOperator(), *this,
+ "Expr::getOperator() called on an Expr with no operator");
return Expr(d_exprManager, new Node(d_node->getOperator()));
}
Type Expr::getType(bool check) const throw (TypeCheckingException) {
ExprManagerScope ems(*this);
Assert(d_node != NULL, "Unexpected NULL expression pointer!");
- CheckArgument(!d_node->isNull(), this, "Can't get type of null expression!");
+ PrettyCheckArgument(!d_node->isNull(), this,
+ "Can't get type of null expression!");
return d_exprManager->getType(*this, check);
}
Expr Expr::andExpr(const Expr& e) const {
Assert(d_exprManager != NULL,
"Don't have an expression manager for this expression!");
- CheckArgument(d_exprManager == e.d_exprManager, e,
- "Different expression managers!");
+ PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
+ "Different expression managers!");
return d_exprManager->mkExpr(AND, *this, e);
}
Expr Expr::orExpr(const Expr& e) const {
Assert(d_exprManager != NULL,
"Don't have an expression manager for this expression!");
- CheckArgument(d_exprManager == e.d_exprManager, e,
- "Different expression managers!");
+ PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
+ "Different expression managers!");
return d_exprManager->mkExpr(OR, *this, e);
}
Expr Expr::xorExpr(const Expr& e) const {
Assert(d_exprManager != NULL,
"Don't have an expression manager for this expression!");
- CheckArgument(d_exprManager == e.d_exprManager, e,
- "Different expression managers!");
+ PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
+ "Different expression managers!");
return d_exprManager->mkExpr(XOR, *this, e);
}
Expr Expr::iffExpr(const Expr& e) const {
Assert(d_exprManager != NULL,
"Don't have an expression manager for this expression!");
- CheckArgument(d_exprManager == e.d_exprManager, e,
- "Different expression managers!");
+ PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
+ "Different expression managers!");
return d_exprManager->mkExpr(IFF, *this, e);
}
Expr Expr::impExpr(const Expr& e) const {
Assert(d_exprManager != NULL,
"Don't have an expression manager for this expression!");
- CheckArgument(d_exprManager == e.d_exprManager, e,
- "Different expression managers!");
+ PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
+ "Different expression managers!");
return d_exprManager->mkExpr(IMPLIES, *this, e);
}
const Expr& else_e) const {
Assert(d_exprManager != NULL,
"Don't have an expression manager for this expression!");
- CheckArgument(d_exprManager == then_e.d_exprManager, then_e,
- "Different expression managers!");
- CheckArgument(d_exprManager == else_e.d_exprManager, else_e,
- "Different expression managers!");
+ PrettyCheckArgument(d_exprManager == then_e.d_exprManager, then_e,
+ "Different expression managers!");
+ PrettyCheckArgument(d_exprManager == else_e.d_exprManager, else_e,
+ "Different expression managers!");
return d_exprManager->mkExpr(ITE, *this, then_e, else_e);
}
#include <stdint.h>
#include <iterator>
+#include "base/cvc4_assert.h"
#include "expr/kind.h"
namespace CVC4 {
#ifndef __CVC4__KIND_H
#define __CVC4__KIND_H
-#include <iostream>
+#include <iosfwd>
#include <sstream>
#include "base/exception.h"
#ifndef __CVC4__MATCHER_H
#define __CVC4__MATCHER_H
-#include <iostream>
+#include <iosfwd>
#include <string>
#include <vector>
#include <map>
#line $lineno \"$kf\"
template <> $2 const & Expr::getConst() const {
#line $lineno \"$kf\"
- CheckArgument(getKind() == ::CVC4::kind::$1, *this, \"Improper kind for getConst<$2>()\");
+ PrettyCheckArgument(getKind() == ::CVC4::kind::$1, *this, \"Improper kind for getConst<$2>()\");
#line $lineno \"$kf\"
return d_node->getConst< $2 >();
}
sorts.push_back(sort);
}
Debug("datatypes") << "ctor range: " << range << endl;
- CheckArgument(!range.isFunctionLike(), range,
- "cannot create higher-order function types");
+ PrettyCheckArgument(!range.isFunctionLike(), range,
+ "cannot create higher-order function types");
sorts.push_back(range);
return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts);
}
"cannot index arrays by a function-like type");
CheckArgument(!constituentType.isFunctionLike(), constituentType,
"cannot store function-like types in arrays");
- Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl;
+ Debug("arrays") << "making array type " << indexType << " "
+ << constituentType << std::endl;
return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
}
: d_predicate(new Expr(e))
, d_witness(new Expr())
{
- CheckArgument(! e.isNull(), e, "Predicate cannot be null");
- CheckArgument(e.getType().isPredicate(), e, "Expression given is not predicate");
- CheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, "Expression given is not predicate of a single argument");
+ PrettyCheckArgument(! e.isNull(), e, "Predicate cannot be null");
+ PrettyCheckArgument(e.getType().isPredicate(), e,
+ "Expression given is not predicate");
+ PrettyCheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e,
+ "Expression given is not predicate of a single argument");
}
Predicate::Predicate(const Expr& e, const Expr& w)
: d_predicate(new Expr(e))
, d_witness(new Expr(w))
{
- CheckArgument(! e.isNull(), e, "Predicate cannot be null");
- CheckArgument(e.getType().isPredicate(), e, "Expression given is not predicate");
- CheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, "Expression given is not predicate of a single argument");
+ PrettyCheckArgument(! e.isNull(), e, "Predicate cannot be null");
+ PrettyCheckArgument(e.getType().isPredicate(), e,
+ "Expression given is not predicate");
+ PrettyCheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e,
+ "Expression given is not predicate of a single argument");
}
Predicate::~Predicate() {
size_t Record::getIndex(std::string name) const {
FieldVector::const_iterator i = find(*d_fields, name);
- CheckArgument(i != d_fields->end(), name,
- "requested field `%s' does not exist in record", name.c_str());
+ PrettyCheckArgument(i != d_fields->end(), name,
+ "requested field `%s' does not exist in record",
+ name.c_str());
return i - d_fields->begin();
}
const std::pair<std::string, Type>& Record::operator[](size_t index) const {
- CheckArgument(index < d_fields->size(), index, "index out of bounds for record type");
+ PrettyCheckArgument(index < d_fields->size(), index,
+ "index out of bounds for record type");
return (*d_fields)[index];
}
namespace CVC4 {
+Result::Result()
+ : d_sat(SAT_UNKNOWN)
+ , d_validity(VALIDITY_UNKNOWN)
+ , d_which(TYPE_NONE)
+ , d_unknownExplanation(UNKNOWN_REASON)
+ , d_inputName("")
+{ }
+
+
+Result::Result(enum Sat s, std::string inputName)
+ : d_sat(s)
+ , d_validity(VALIDITY_UNKNOWN)
+ , d_which(TYPE_SAT)
+ , d_unknownExplanation(UNKNOWN_REASON)
+ , d_inputName(inputName)
+{
+ PrettyCheckArgument(s != SAT_UNKNOWN,
+ "Must provide a reason for satisfiability being unknown");
+}
+
+Result::Result(enum Validity v, std::string inputName)
+ : d_sat(SAT_UNKNOWN)
+ , d_validity(v)
+ , d_which(TYPE_VALIDITY)
+ , d_unknownExplanation(UNKNOWN_REASON)
+ , d_inputName(inputName)
+{
+ PrettyCheckArgument(v != VALIDITY_UNKNOWN,
+ "Must provide a reason for validity being unknown");
+}
+
+
+Result::Result(enum Sat s, enum UnknownExplanation unknownExplanation,
+ std::string inputName)
+ : d_sat(s)
+ , d_validity(VALIDITY_UNKNOWN)
+ , d_which(TYPE_SAT)
+ , d_unknownExplanation(unknownExplanation)
+ , d_inputName(inputName)
+{
+ PrettyCheckArgument(s == SAT_UNKNOWN,
+ "improper use of unknown-result constructor");
+}
+
+Result::Result(enum Validity v, enum UnknownExplanation unknownExplanation,
+ std::string inputName)
+ : d_sat(SAT_UNKNOWN)
+ , d_validity(v)
+ , d_which(TYPE_VALIDITY)
+ , d_unknownExplanation(unknownExplanation)
+ , d_inputName(inputName)
+{
+ PrettyCheckArgument(v == VALIDITY_UNKNOWN,
+ "improper use of unknown-result constructor");
+}
+
Result::Result(const std::string& instr, std::string inputName) :
d_sat(SAT_UNKNOWN),
d_validity(VALIDITY_UNKNOWN),
}
}
+Result::UnknownExplanation Result::whyUnknown() const {
+ PrettyCheckArgument( isUnknown(), this,
+ "This result is not unknown, so the reason for "
+ "being unknown cannot be inquired of it" );
+ return d_unknownExplanation;
+}
+
bool Result::operator==(const Result& r) const throw() {
if(d_which != r.d_which) {
return false;
std::string d_inputName;
public:
- Result() :
- d_sat(SAT_UNKNOWN),
- d_validity(VALIDITY_UNKNOWN),
- d_which(TYPE_NONE),
- d_unknownExplanation(UNKNOWN_REASON),
- d_inputName("") {
- }
- Result(enum Sat s, std::string inputName = "") :
- d_sat(s),
- d_validity(VALIDITY_UNKNOWN),
- d_which(TYPE_SAT),
- d_unknownExplanation(UNKNOWN_REASON),
- d_inputName(inputName) {
- CheckArgument(s != SAT_UNKNOWN,
- "Must provide a reason for satisfiability being unknown");
- }
- Result(enum Validity v, std::string inputName = "") :
- d_sat(SAT_UNKNOWN),
- d_validity(v),
- d_which(TYPE_VALIDITY),
- d_unknownExplanation(UNKNOWN_REASON),
- d_inputName(inputName) {
- CheckArgument(v != VALIDITY_UNKNOWN,
- "Must provide a reason for validity being unknown");
- }
- Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName = "") :
- d_sat(s),
- d_validity(VALIDITY_UNKNOWN),
- d_which(TYPE_SAT),
- d_unknownExplanation(unknownExplanation),
- d_inputName(inputName) {
- CheckArgument(s == SAT_UNKNOWN,
- "improper use of unknown-result constructor");
- }
- Result(enum Validity v, enum UnknownExplanation unknownExplanation, std::string inputName = "") :
- d_sat(SAT_UNKNOWN),
- d_validity(v),
- d_which(TYPE_VALIDITY),
- d_unknownExplanation(unknownExplanation),
- d_inputName(inputName) {
- CheckArgument(v == VALIDITY_UNKNOWN,
- "improper use of unknown-result constructor");
- }
+
+ Result();
+
+ Result(enum Sat s, std::string inputName = "");
+
+ Result(enum Validity v, std::string inputName = "");
+
+ Result(enum Sat s,
+ enum UnknownExplanation unknownExplanation,
+ std::string inputName = "");
+
+ Result(enum Validity v, enum UnknownExplanation unknownExplanation,
+ std::string inputName = "");
+
Result(const std::string& s, std::string inputName = "");
Result(const Result& r, std::string inputName) {
enum Sat isSat() const {
return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN;
}
+
enum Validity isValid() const {
return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN;
}
+
bool isUnknown() const {
return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN;
}
+
Type getType() const {
return d_which;
}
+
bool isNull() const {
return d_which == TYPE_NONE;
}
- enum UnknownExplanation whyUnknown() const {
- CheckArgument( isUnknown(), this,
- "This result is not unknown, so the reason for "
- "being unknown cannot be inquired of it" );
- return d_unknownExplanation;
- }
+
+ enum UnknownExplanation whyUnknown() const;
bool operator==(const Result& r) const throw();
inline bool operator!=(const Result& r) const throw();
std::string SExpr::getValue() const {
- CheckArgument( isAtom(), this );
+ PrettyCheckArgument( isAtom(), this );
switch(d_sexprType) {
case SEXPR_INTEGER:
return d_integerValue.toString();
}
const CVC4::Integer& SExpr::getIntegerValue() const {
- CheckArgument( isInteger(), this );
+ PrettyCheckArgument( isInteger(), this );
return d_integerValue;
}
const CVC4::Rational& SExpr::getRationalValue() const {
- CheckArgument( isRational(), this );
+ PrettyCheckArgument( isRational(), this );
return d_rationalValue;
}
const std::vector<SExpr>& SExpr::getChildren() const {
- CheckArgument( !isAtom(), this );
+ PrettyCheckArgument( !isAtom(), this );
Assert( d_children != NULL );
return *d_children;
}
#include "expr/statistics_registry.h"
+#include "base/cvc4_assert.h"
#include "expr/expr_manager.h"
#include "lib/clock_gettime.h"
#include "smt/smt_engine.h"
namespace CVC4 {
+/** Construct a statistics registry */
+StatisticsRegistry::StatisticsRegistry(const std::string& name)
+ throw(CVC4::IllegalArgumentException) :
+ Stat(name) {
+
+ d_prefix = name;
+ if(__CVC4_USE_STATISTICS) {
+ PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name,
+ "StatisticsRegistry names cannot contain the string \"%s\"",
+ s_regDelim.c_str());
+ }
+}
+
namespace stats {
// This is a friend of SmtEngine, just to reach in and get it.
void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) {
#ifdef CVC4_STATISTICS_ON
StatSet& stats = current()->d_stats;
- CheckArgument(stats.find(s) == stats.end(), s,
- "Statistic `%s' was already registered with this registry.",
- s->getName().c_str());
+ PrettyCheckArgument(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(CVC4::IllegalArgumentException) {
#ifdef CVC4_STATISTICS_ON
StatSet& stats = current()->d_stats;
- CheckArgument(stats.find(s) != stats.end(), s,
+ PrettyCheckArgument(stats.find(s) != stats.end(), s,
"Statistic `%s' was not registered with this registry.",
s->getName().c_str());
stats.erase(s);
void StatisticsRegistry::registerStat_(Stat* s) throw(CVC4::IllegalArgumentException) {
#ifdef CVC4_STATISTICS_ON
- CheckArgument(d_stats.find(s) == d_stats.end(), s);
+ PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s);
d_stats.insert(s);
#endif /* CVC4_STATISTICS_ON */
}/* StatisticsRegistry::registerStat_() */
void StatisticsRegistry::unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException) {
#ifdef CVC4_STATISTICS_ON
- CheckArgument(d_stats.find(s) != d_stats.end(), s);
+ PrettyCheckArgument(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) {
- CheckArgument(!d_running, *this, "timer already running");
+ PrettyCheckArgument(!d_running, *this, "timer already running");
clock_gettime(CLOCK_MONOTONIC, &d_start);
d_running = true;
}
void TimerStat::stop() {
if(__CVC4_USE_STATISTICS) {
- CheckArgument(d_running, *this, "timer not running");
+ PrettyCheckArgument(d_running, *this, "timer not running");
::timespec end;
clock_gettime(CLOCK_MONOTONIC, &end);
d_data += end - d_start;
/** Construct a statistics registry */
StatisticsRegistry(const std::string& name)
- throw(CVC4::IllegalArgumentException) :
- Stat(name) {
- d_prefix = name;
- if(__CVC4_USE_STATISTICS) {
- CheckArgument(d_name.find(s_regDelim) == std::string::npos, name,
- "StatisticsRegistry names cannot contain the string \"%s\"",
- s_regDelim.c_str());
- }
- }
+ throw(CVC4::IllegalArgumentException);
/**
* Set the name of this statistic registry, used as prefix during
**/
#include "expr/symbol_table.h"
-#include "expr/expr.h"
-#include "expr/type.h"
-#include "expr/expr_manager_scope.h"
+
+#include <string>
+#include <utility>
+
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
#include "context/context.h"
+#include "expr/expr.h"
+#include "expr/expr_manager_scope.h"
+#include "expr/type.h"
-#include <string>
-#include <utility>
-using namespace CVC4;
using namespace CVC4::context;
using namespace std;
void SymbolTable::bind(const std::string& name, Expr obj,
bool levelZero) throw() {
- CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
+ PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
ExprManagerScope ems(obj);
if(levelZero) d_exprMap->insertAtContextLevelZero(name, obj);
else d_exprMap->insert(name, obj);
void SymbolTable::bindDefinedFunction(const std::string& name, Expr obj,
bool levelZero) throw() {
- CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
+ PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
ExprManagerScope ems(obj);
if(levelZero){
d_exprMap->insertAtContextLevelZero(name, obj);
Type SymbolTable::lookupType(const std::string& name) const throw() {
pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
- CheckArgument(p.first.size() == 0, name,
+ PrettyCheckArgument(p.first.size() == 0, name,
"type constructor arity is wrong: "
"`%s' requires %u parameters but was provided 0",
name.c_str(), p.first.size());
Type SymbolTable::lookupType(const std::string& name,
const std::vector<Type>& params) const throw() {
pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
- CheckArgument(p.first.size() == params.size(), params,
+ PrettyCheckArgument(p.first.size() == params.size(), params,
"type constructor arity is wrong: "
"`%s' requires %u parameters but was provided %u",
name.c_str(), p.first.size(), params.size());
if(p.first.size() == 0) {
- CheckArgument(p.second.isSort(), name);
+ PrettyCheckArgument(p.second.isSort(), name.c_str());
return p.second;
}
if(p.second.isSortConstructor()) {
return instantiation;
} else if(p.second.isDatatype()) {
- CheckArgument(DatatypeType(p.second).isParametric(), name, "expected parametric datatype");
+ PrettyCheckArgument(DatatypeType(p.second).isParametric(), name, "expected parametric datatype");
return DatatypeType(p.second).instantiate(params);
} else {
if(Debug.isOn("sort")) {
}
Type& Type::operator=(const Type& t) {
- CheckArgument(d_typeNode != NULL, this, "Unexpected NULL typenode pointer!");
- CheckArgument(t.d_typeNode != NULL, t, "Unexpected NULL typenode pointer!");
+ PrettyCheckArgument(d_typeNode != NULL, this, "Unexpected NULL typenode pointer!");
+ PrettyCheckArgument(t.d_typeNode != NULL, t, "Unexpected NULL typenode pointer!");
if(this != &t) {
if(d_nodeManager == t.d_nodeManager) {
Type FunctionType::getRangeType() const {
NodeManagerScope nms(d_nodeManager);
- CheckArgument(isNull() || isFunction(), this);
+ PrettyCheckArgument(isNull() || isFunction(), this);
return makeType(d_typeNode->getRangeType());
}
BooleanType::BooleanType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- CheckArgument(isNull() || isBoolean(), this);
+ PrettyCheckArgument(isNull() || isBoolean(), this);
}
IntegerType::IntegerType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- CheckArgument(isNull() || isInteger(), this);
+ PrettyCheckArgument(isNull() || isInteger(), this);
}
RealType::RealType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- CheckArgument(isNull() || isReal(), this);
+ PrettyCheckArgument(isNull() || isReal(), this);
}
StringType::StringType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- CheckArgument(isNull() || isString(), this);
+ PrettyCheckArgument(isNull() || isString(), this);
}
RoundingModeType::RoundingModeType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- CheckArgument(isNull() || isRoundingMode(), this);
+ PrettyCheckArgument(isNull() || isRoundingMode(), this);
}
BitVectorType::BitVectorType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- CheckArgument(isNull() || isBitVector(), this);
+ PrettyCheckArgument(isNull() || isBitVector(), this);
}
FloatingPointType::FloatingPointType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- CheckArgument(isNull() || isFloatingPoint(), this);
+ PrettyCheckArgument(isNull() || isFloatingPoint(), this);
}
DatatypeType::DatatypeType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- CheckArgument(isNull() || isDatatype(), this);
+ PrettyCheckArgument(isNull() || isDatatype(), this);
}
ConstructorType::ConstructorType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- CheckArgument(isNull() || isConstructor(), this);
+ PrettyCheckArgument(isNull() || isConstructor(), this);
}
SelectorType::SelectorType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
- CheckArgument(isNull() || isSelector(), this);
+ PrettyCheckArgument(isNull() || isSelector(), this);
}
-TesterType::TesterType(const Type& t) throw(IllegalArgumentException) :
- Type(t) {
- CheckArgument(isNull() || isTester(), this);
+TesterType::TesterType(const Type& t) throw(IllegalArgumentException)
+ : Type(t) {
+ PrettyCheckArgument(isNull() || isTester(), this);
}
-FunctionType::FunctionType(const Type& t) throw(IllegalArgumentException) :
- Type(t) {
- CheckArgument(isNull() || isFunction(), this);
+FunctionType::FunctionType(const Type& t) throw(IllegalArgumentException)
+ : Type(t) {
+ PrettyCheckArgument(isNull() || isFunction(), this);
}
-TupleType::TupleType(const Type& t) throw(IllegalArgumentException) :
- Type(t) {
- CheckArgument(isNull() || isTuple(), this);
+TupleType::TupleType(const Type& t) throw(IllegalArgumentException)
+ : Type(t) {
+ PrettyCheckArgument(isNull() || isTuple(), this);
}
-RecordType::RecordType(const Type& t) throw(IllegalArgumentException) :
- Type(t) {
- CheckArgument(isNull() || isRecord(), this);
+RecordType::RecordType(const Type& t) throw(IllegalArgumentException)
+ : Type(t) {
+ PrettyCheckArgument(isNull() || isRecord(), this);
}
-SExprType::SExprType(const Type& t) throw(IllegalArgumentException) :
- Type(t) {
- CheckArgument(isNull() || isSExpr(), this);
+SExprType::SExprType(const Type& t) throw(IllegalArgumentException)
+ : Type(t) {
+ PrettyCheckArgument(isNull() || isSExpr(), this);
}
-ArrayType::ArrayType(const Type& t) throw(IllegalArgumentException) :
- Type(t) {
- CheckArgument(isNull() || isArray(), this);
+ArrayType::ArrayType(const Type& t) throw(IllegalArgumentException)
+ : Type(t) {
+ PrettyCheckArgument(isNull() || isArray(), this);
}
-SetType::SetType(const Type& t) throw(IllegalArgumentException) :
- Type(t) {
- CheckArgument(isNull() || isSet(), this);
+SetType::SetType(const Type& t) throw(IllegalArgumentException)
+ : Type(t) {
+ PrettyCheckArgument(isNull() || isSet(), this);
}
-SortType::SortType(const Type& t) throw(IllegalArgumentException) :
- Type(t) {
- CheckArgument(isNull() || isSort(), this);
+SortType::SortType(const Type& t) throw(IllegalArgumentException)
+ : Type(t) {
+ PrettyCheckArgument(isNull() || isSort(), this);
}
SortConstructorType::SortConstructorType(const Type& t)
- throw(IllegalArgumentException) :
- Type(t) {
- CheckArgument(isNull() || isSortConstructor(), this);
+ throw(IllegalArgumentException)
+ : Type(t) {
+ PrettyCheckArgument(isNull() || isSortConstructor(), this);
}
/* - not in release 1.0
PredicateSubtype::PredicateSubtype(const Type& t)
throw(IllegalArgumentException) :
Type(t) {
- CheckArgument(isNull() || isPredicateSubtype(), this);
+ PrettyCheckArgument(isNull() || isPredicateSubtype(), this);
}
*/
SubrangeType::SubrangeType(const Type& t)
throw(IllegalArgumentException) :
Type(t) {
- CheckArgument(isNull() || isSubrange(), this);
+ PrettyCheckArgument(isNull() || isSubrange(), this);
}
unsigned BitVectorType::getSize() const {
const Datatype& DatatypeType::getDatatype() const {
NodeManagerScope nms(d_nodeManager);
if( d_typeNode->isParametricDatatype() ) {
- CheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this);
+ PrettyCheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this);
const Datatype& dt = (*d_typeNode)[0].getConst<Datatype>();
return dt;
} else {
#include <sstream>
#include <string>
+#include "base/cvc4_assert.h"
+
using namespace std;
namespace CVC4 {
+UninterpretedConstant::UninterpretedConstant(Type type, Integer index) throw(IllegalArgumentException)
+ : d_type(type)
+ , d_index(index)
+{
+ //PrettyCheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str());
+ PrettyCheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str());
+}
+
std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) {
stringstream ss;
ss << uc.getType();
#pragma once
+#include <iosfwd>
+
#include "expr/type.h"
-#include <iostream>
namespace CVC4 {
class CVC4_PUBLIC UninterpretedConstant {
- const Type d_type;
- const Integer d_index;
-
public:
- UninterpretedConstant(Type type, Integer index) throw(IllegalArgumentException) :
- d_type(type),
- d_index(index) {
- //CheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str());
- CheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str());
- }
+ UninterpretedConstant(Type type, Integer index) throw(IllegalArgumentException);
- ~UninterpretedConstant() throw() {
- }
+ ~UninterpretedConstant() throw() { }
Type getType() const throw() {
return d_type;
return !(*this < uc);
}
+private:
+ const Type d_type;
+ const Integer d_index;
};/* class UninterpretedConstant */
std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) CVC4_PUBLIC;
#ifndef __CVC4__MAIN__COMMAND_EXECUTOR_H
#define __CVC4__MAIN__COMMAND_EXECUTOR_H
-#include <iostream>
+#include <iosfwd>
#include <string>
#include "expr/expr_manager.h"
#include "main/command_executor.h"
#include "main/portfolio_util.h"
-#include <vector>
-#include <string>
-#include <iostream>
+#include <iosfwd>
#include <sstream>
+#include <string>
+#include <vector>
namespace CVC4 {
#ifndef __CVC4__INTERACTIVE_SHELL_H
#define __CVC4__INTERACTIVE_SHELL_H
-#include <iostream>
+#include <iosfwd>
#include <string>
#include "options/language.h"
option binary_name std::string
-option in std::istream* :default &std::cin :include <iostream>
-option out std::ostream* :default &std::cout :include <iostream>
-option err std::ostream* :default &std::cerr :include <iostream>
+option in std::istream* :default &std::cin :include <iosfwd>
+option out std::ostream* :default &std::cout :include <iosfwd>
+option err std::ostream* :default &std::cerr :include <iosfwd>
common-option inputLanguage input-language -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "options/language.h" :default language::input::LANG_AUTO :read-write
force input language (default is "auto"; see --lang help)
#include <iostream>
-
namespace CVC4 {
std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) {
#ifndef __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H
#define __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H
-#include <iostream>
+#include <iosfwd>
namespace CVC4 {
namespace theory {
#include "options/bv_bitblast_mode.h"
+#include <iostream>
+
namespace CVC4 {
std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode) {
#ifndef __CVC4__THEORY__BV__BITBLAST_MODE_H
#define __CVC4__THEORY__BV__BITBLAST_MODE_H
-#include <iostream>
+#include <iosfwd>
namespace CVC4 {
namespace theory {
// theory/arith/options_handlers.h
ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToArithUnateLemmaMode(option, optarg);
}
ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToArithPropagationMode(option, optarg);
}
ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToErrorSelectionRule(option, optarg);
}
// theory/quantifiers/options_handlers.h
theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToInstWhenMode(option, optarg);
}
void checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->checkInstWhenMode(option, mode);
}
theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToLiteralMatchMode(option, optarg);
}
void checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->checkLiteralMatchMode(option, mode);
}
theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToMbqiMode(option, optarg);
}
void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->checkMbqiMode(option, mode);
}
theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToQcfWhenMode(option, optarg);
}
theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToQcfMode(option, optarg);
}
theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToUserPatMode(option, optarg);
}
theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToTriggerSelMode(option, optarg);
}
theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToPrenexQuantMode(option, optarg);
}
theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToCegqiFairMode(option, optarg);
}
theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler-> stringToTermDbMode(option, optarg);
}
theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToIteLiftQuantMode(option, optarg);
}
theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToSygusInvTemplMode(option, optarg);
}
theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToMacrosQuantMode(option, optarg);
}
// theory/bv/options_handlers.h
void abcEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->abcEnabledBuild(option, value);
}
void abcEnabledBuild(std::string option, std::string value, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->abcEnabledBuild(option, value);
}
theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToBitblastMode(option, optarg);
}
theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToBvSlicerMode(option, optarg);
}
void setBitblastAig(std::string option, bool arg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->setBitblastAig(option, arg);
}
// theory/booleans/options_handlers.h
theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToBooleanTermConversionMode( option, optarg);
}
// theory/uf/options_handlers.h
theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToUfssMode(option, optarg);
}
// theory/options_handlers.h
theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToTheoryOfMode(option, optarg);
}
void useTheory(std::string option, std::string optarg, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->useTheory(option, optarg);
}
// printer/options_handlers.h
ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToModelFormatMode(option, optarg);
}
InstFormatMode stringToInstFormatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToInstFormatMode(option, optarg);
}
// decision/options_handlers.h
decision::DecisionMode stringToDecisionMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToDecisionMode(option, optarg);
}
decision::DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToDecisionWeightInternal(option, optarg);
}
/* options/base_options_handlers.h */
void setVerbosity(std::string option, int value, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->setVerbosity(option, value);
}
void increaseVerbosity(std::string option, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->increaseVerbosity(option);
}
void decreaseVerbosity(std::string option, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->decreaseVerbosity(option);
}
OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToOutputLanguage(option, optarg);
}
InputLanguage stringToInputLanguage(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToInputLanguage(option, optarg);
}
void addTraceTag(std::string option, std::string optarg, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->addTraceTag(option, optarg);
}
void addDebugTag(std::string option, std::string optarg, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->addDebugTag(option, optarg);
}
void setPrintSuccess(std::string option, bool value, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->setPrintSuccess(option, value);
}
/* main/options_handlers.h */
void showConfiguration(std::string option, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->showConfiguration(option);
}
void showDebugTags(std::string option, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->showDebugTags(option);
}
void showTraceTags(std::string option, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->showTraceTags(option);
}
void threadN(std::string option, OptionsHandler* handler){
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->threadN(option);
}
/* expr/options_handlers.h */
void setDefaultExprDepth(std::string option, int depth, OptionsHandler* handler){
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->setDefaultExprDepth(option, depth);
}
void setDefaultDagThresh(std::string option, int dag, OptionsHandler* handler){
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->setDefaultDagThresh(option, dag);
}
void setPrintExprTypes(std::string option, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->setPrintExprTypes(option);
}
/* smt/options_handlers.h */
void dumpMode(std::string option, std::string optarg, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->dumpMode(option, optarg);
}
LogicInfo* stringToLogicInfo(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException){
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToLogicInfo(option, optarg);
}
SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException){
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->stringToSimplificationMode(option, optarg);
}
// ensure we haven't started search yet
void beforeSearch(std::string option, bool value, OptionsHandler* handler) throw(ModalException){
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->beforeSearch(option, value);
}
void setProduceAssertions(std::string option, bool value, OptionsHandler* handler) throw() {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->setProduceAssertions(option, value);
}
// ensure we are a proof-enabled build of CVC4
void proofEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->proofEnabledBuild(option, value);
}
void dumpToFile(std::string option, std::string optarg, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->dumpToFile(option, optarg);
}
void setRegularOutputChannel(std::string option, std::string optarg, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->setRegularOutputChannel(option, optarg);
}
void setDiagnosticOutputChannel(std::string option, std::string optarg, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
handler->setDiagnosticOutputChannel(option, optarg);
}
std::string checkReplayFilename(std::string option, std::string optarg, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->checkReplayFilename(option, optarg);
}
std::ostream* checkReplayLogFilename(std::string option, std::string optarg, OptionsHandler* handler) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->checkReplayLogFilename(option, optarg);
}
// ensure we are a stats-enabled build of CVC4
void statsEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->statsEnabledBuild(option, value);
}
unsigned long tlimitHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->tlimitHandler(option, optarg);
}
unsigned long tlimitPerHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler-> tlimitPerHandler(option, optarg);
}
unsigned long rlimitHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->rlimitHandler(option, optarg);
}
unsigned long rlimitPerHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) {
- CheckArgument(handler != NULL, handler, s_third_argument_warning);
+ PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning);
return handler->rlimitPerHandler(option, optarg);
}
#include "options/simplification_mode.h"
+#include <iostream>
+
namespace CVC4 {
std::ostream& operator<<(std::ostream& out, SimplificationMode mode) {
#ifndef __CVC4__SMT__SIMPLIFICATION_MODE_H
#define __CVC4__SMT__SIMPLIFICATION_MODE_H
-#include <iostream>
+#include <iosfwd>
namespace CVC4 {
**
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__CNF_PROOF_H
#define __CVC4__CNF_PROOF_H
-#include "cvc4_private.h"
-#include "util/proof.h"
-#include "proof/sat_proof.h"
-
-#include <ext/hash_set>
#include <ext/hash_map>
-#include <iostream>
+#include <ext/hash_set>
+#include <iosfwd>
+
+#include "proof/sat_proof.h"
+#include "util/proof.h"
namespace CVC4 {
namespace prop {
#ifndef __CVC4__PROOF_MANAGER_H
#define __CVC4__PROOF_MANAGER_H
-#include <iostream>
+#include <iosfwd>
#include <map>
-#include "proof/proof.h"
-#include "util/proof.h"
+
#include "expr/node.h"
+#include "proof/proof.h"
#include "theory/logic_info.h"
#include "theory/substitutions.h"
+#include "util/proof.h"
namespace CVC4 {
#ifndef __CVC4__SAT__PROOF_H
#define __CVC4__SAT__PROOF_H
-#include <iostream>
#include <stdint.h>
-#include <vector>
-#include <set>
+
#include <ext/hash_map>
#include <ext/hash_set>
+#include <iosfwd>
+#include <set>
#include <sstream>
+#include <vector>
+
#include "expr/expr.h"
#include "proof/proof_manager.h"
**
**/
+#include "cvc4_private.h"
#ifndef __CVC4__THEORY_PROOF_H
#define __CVC4__THEORY_PROOF_H
-#include "cvc4_private.h"
-#include "util/proof.h"
-#include "expr/expr.h"
#include <ext/hash_set>
-#include <iostream>
+#include <iosfwd>
+
+#include "expr/expr.h"
+#include "util/proof.h"
namespace CVC4 {
#ifndef __CVC4__UNSAT_CORE_H
#define __CVC4__UNSAT_CORE_H
-#include <iostream>
+#include <iosfwd>
#include <vector>
+
#include "expr/expr.h"
namespace CVC4 {
#include "cvc4_private.h"
-#include <iostream>
+#include <iosfwd>
#include "base/output.h"
#include "context/context.h"
Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
Type type = e.getType(options::typeChecking());
// must be Boolean
- CheckArgument( type.isBoolean(), e,
- "expected Boolean-typed variable or function application "
- "in addToAssignment()" );
+ PrettyCheckArgument(
+ type.isBoolean(), e,
+ "expected Boolean-typed variable or function application "
+ "in addToAssignment()" );
Node n = e.getNode();
// must be an APPLY of a zero-ary defined function, or a variable
- CheckArgument( ( ( n.getKind() == kind::APPLY &&
- ( d_definedFunctions->find(n.getOperator()) !=
- d_definedFunctions->end() ) &&
- n.getNumChildren() == 0 ) ||
- n.isVar() ), e,
- "expected variable or defined-function application "
- "in addToAssignment(),\ngot %s", e.toString().c_str() );
+ PrettyCheckArgument(
+ ( ( n.getKind() == kind::APPLY &&
+ ( d_definedFunctions->find(n.getOperator()) !=
+ d_definedFunctions->end() ) &&
+ n.getNumChildren() == 0 ) ||
+ n.isVar() ), e,
+ "expected variable or defined-function application "
+ "in addToAssignment(),\ngot %s", e.toString().c_str() );
if(!options::produceAssignments()) {
return false;
}
#include <utility>
#include <vector>
+#include "base/cvc4_assert.h"
#include "base/output.h"
#include "expr/node.h"
#include "expr/sexpr.h"
GetValueCommand::GetValueCommand(const std::vector<Expr>& terms) throw() :
d_terms(terms) {
- CheckArgument(terms.size() >= 1, terms, "cannot get-value of an empty set of terms");
+ PrettyCheckArgument(terms.size() >= 1, terms,
+ "cannot get-value of an empty set of terms");
}
const std::vector<Expr>& GetValueCommand::getTerms() const throw() {
#ifndef __CVC4__COMMAND_H
#define __CVC4__COMMAND_H
-#include <iostream>
+#include <iosfwd>
+#include <map>
#include <sstream>
#include <string>
#include <vector>
-#include <map>
#include "expr/datatype.h"
#include "expr/expr.h"
#ifndef __CVC4__MODEL_H
#define __CVC4__MODEL_H
-#include <iostream>
+#include <iosfwd>
#include <vector>
#include "expr/expr.h"
class ApproximateSimplex;
class TreeLog {
private:
- ApproximateSimplex* d_generator;
+ ApproximateSimplex* d_generator CVC4_UNUSED;
int next_exec_ord;
typedef std::map<int, NodeLog> ToNodeMap;
#include <ostream>
#include "base/exception.h"
+#include "base/cvc4_assert.h"
#include "util/integer.h"
#include "util/rational.h"
lock();
}
+/** Is sharing enabled for this logic? */
+bool LogicInfo::isSharingEnabled() const {
+ PrettyCheckArgument(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 LogicInfo::isTheoryEnabled(theory::TheoryId theory) const {
+ PrettyCheckArgument(d_locked, *this,
+ "This LogicInfo isn't locked yet, and cannot be queried");
+ return d_theories[theory];
+}
+
+/** Is this a quantified logic? */
+bool LogicInfo::isQuantified() const {
+ PrettyCheckArgument(d_locked, *this,
+ "This LogicInfo isn't locked yet, and cannot be queried");
+ return isTheoryEnabled(theory::THEORY_QUANTIFIERS);
+}
+
+/** Is this the all-inclusive logic? */
+bool LogicInfo::hasEverything() const {
+ PrettyCheckArgument(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 LogicInfo::hasNothing() const {
+ PrettyCheckArgument(d_locked, *this,
+ "This LogicInfo isn't locked yet, and cannot be queried");
+ LogicInfo nothing("");
+ nothing.lock();
+ return *this == nothing;
+}
+
+bool LogicInfo::isPure(theory::TheoryId theory) const {
+ PrettyCheckArgument(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() &&
+ ( !isTrueTheory(theory) || d_sharingTheories == 1 ) &&
+ ( isTrueTheory(theory) || d_sharingTheories == 0 );
+}
+
+bool LogicInfo::areIntegersUsed() const {
+ PrettyCheckArgument(d_locked, *this,
+ "This LogicInfo isn't locked yet, and cannot be queried");
+ PrettyCheckArgument(
+ isTheoryEnabled(theory::THEORY_ARITH), *this,
+ "Arithmetic not used in this LogicInfo; cannot ask whether integers are used");
+ return d_integers;
+}
+
+bool LogicInfo::areRealsUsed() const {
+ PrettyCheckArgument(d_locked, *this,
+ "This LogicInfo isn't locked yet, and cannot be queried");
+ PrettyCheckArgument(
+ isTheoryEnabled(theory::THEORY_ARITH), *this,
+ "Arithmetic not used in this LogicInfo; cannot ask whether reals are used");
+ return d_reals;
+}
+
+bool LogicInfo::isLinear() const {
+ PrettyCheckArgument(d_locked, *this,
+ "This LogicInfo isn't locked yet, and cannot be queried");
+ PrettyCheckArgument(
+ isTheoryEnabled(theory::THEORY_ARITH), *this,
+ "Arithmetic not used in this LogicInfo; cannot ask whether it's linear");
+ return d_linear || d_differenceLogic;
+}
+
+bool LogicInfo::isDifferenceLogic() const {
+ PrettyCheckArgument(d_locked, *this,
+ "This LogicInfo isn't locked yet, and cannot be queried");
+ PrettyCheckArgument(
+ isTheoryEnabled(theory::THEORY_ARITH), *this,
+ "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic");
+ return d_differenceLogic;
+}
+
+bool LogicInfo::hasCardinalityConstraints() const {
+ PrettyCheckArgument(d_locked, *this,
+ "This LogicInfo isn't locked yet, and cannot be queried");
+ return d_cardinalityConstraints;
+}
+
+
+bool LogicInfo::operator==(const LogicInfo& other) const {
+ PrettyCheckArgument(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;
+ }
+ }
+
+ PrettyCheckArgument(d_sharingTheories == other.d_sharingTheories, *this,
+ "LogicInfo internal inconsistency");
+ if(isTheoryEnabled(theory::THEORY_ARITH)) {
+ return
+ d_integers == other.d_integers &&
+ d_reals == other.d_reals &&
+ d_linear == other.d_linear &&
+ d_differenceLogic == other.d_differenceLogic;
+ } else {
+ return true;
+ }
+}
+
+bool LogicInfo::operator<=(const LogicInfo& other) const {
+ PrettyCheckArgument(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;
+ }
+ }
+ PrettyCheckArgument(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) &&
+ (!d_reals || other.d_reals) &&
+ (d_linear || !other.d_linear) &&
+ (d_differenceLogic || !other.d_differenceLogic);
+ } else {
+ return true;
+ }
+}
+
+bool LogicInfo::operator>=(const LogicInfo& other) const {
+ PrettyCheckArgument(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;
+ }
+ }
+ PrettyCheckArgument(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) &&
+ (d_reals || !other.d_reals) &&
+ (!d_linear || other.d_linear) &&
+ (!d_differenceLogic || other.d_differenceLogic);
+ } else {
+ return true;
+ }
+}
+
std::string LogicInfo::getLogicString() const {
- CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
+ PrettyCheckArgument(
+ d_locked, *this,
+ "This LogicInfo isn't locked yet, and cannot be queried");
if(d_logicString == "") {
LogicInfo qf_all_supported;
qf_all_supported.disableQuantifiers();
}
void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) {
- CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+ PrettyCheckArgument(!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() {
- CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+ PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
*this = LogicInfo();
}
void LogicInfo::disableEverything() {
- CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+ PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
*this = LogicInfo("");
}
void LogicInfo::enableTheory(theory::TheoryId theory) {
- CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+ PrettyCheckArgument(!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) {
- CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+ PrettyCheckArgument(!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() {
- CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+ PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
enableTheory(THEORY_ARITH);
d_integers = true;
}
void LogicInfo::disableIntegers() {
- CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+ PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
d_integers = false;
if(!d_reals) {
}
void LogicInfo::enableReals() {
- CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+ PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
enableTheory(THEORY_ARITH);
d_reals = true;
}
void LogicInfo::disableReals() {
- CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+ PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
d_reals = false;
if(!d_integers) {
}
void LogicInfo::arithOnlyDifference() {
- CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+ PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
d_linear = true;
d_differenceLogic = true;
}
void LogicInfo::arithOnlyLinear() {
- CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+ PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
d_linear = true;
d_differenceLogic = false;
}
void LogicInfo::arithNonLinear() {
- CheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
+ PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
d_linear = false;
d_differenceLogic = false;
std::string getLogicString() const;
/** Is sharing enabled for this logic? */
- bool isSharingEnabled() const {
- CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
- return d_sharingTheories > 1;
- }
+ bool isSharingEnabled() const;
/** Is the given theory module active in this logic? */
- bool isTheoryEnabled(theory::TheoryId theory) const {
- CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
- return d_theories[theory];
- }
+ bool isTheoryEnabled(theory::TheoryId theory) const;
/** Is this a quantified logic? */
- bool isQuantified() const {
- CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
- return isTheoryEnabled(theory::THEORY_QUANTIFIERS);
- }
+ bool isQuantified() const;
/** Is this the all-inclusive logic? */
- bool hasEverything() const {
- CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
- LogicInfo everything;
- everything.lock();
- return *this == everything;
- }
+ bool hasEverything() const;
/** Is this the all-exclusive logic? (Here, that means propositional logic) */
- bool hasNothing() const {
- CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
- LogicInfo nothing("");
- nothing.lock();
- return *this == nothing;
- }
+ bool hasNothing() const;
/**
* Is this a pure logic (only one "true" background theory). Quantifiers
* can exist in such logics though; to test for quantifier-free purity,
* use "isPure(theory) && !isQuantified()".
*/
- bool isPure(theory::TheoryId theory) const {
- 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() &&
- ( !isTrueTheory(theory) || d_sharingTheories == 1 ) &&
- ( isTrueTheory(theory) || d_sharingTheories == 0 );
- }
+ bool isPure(theory::TheoryId theory) const;
// these are for arithmetic
/** Are integers in this logic? */
- bool areIntegersUsed() const {
- CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
- CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether integers are used");
- return d_integers;
- }
+ bool areIntegersUsed() const;
+
/** Are reals in this logic? */
- bool areRealsUsed() const {
- CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
- CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether reals are used");
- return d_reals;
- }
+ bool areRealsUsed() const;
+
/** Does this logic only linear arithmetic? */
- bool isLinear() const {
- CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
- CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's linear");
- return d_linear || d_differenceLogic;
- }
+ bool isLinear() const;
+
/** Does this logic only permit difference reasoning? (implies linear) */
- bool isDifferenceLogic() const {
- CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
- CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic");
- return d_differenceLogic;
- }
+ bool isDifferenceLogic() const;
+
/** Does this logic allow cardinality constraints? */
- bool hasCardinalityConstraints() const {
- CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
- return d_cardinalityConstraints;
- }
+ bool hasCardinalityConstraints() const;
// MUTATORS
// COMPARISON
/** Are these two LogicInfos equal? */
- bool operator==(const LogicInfo& other) const {
- 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;
- }
- }
- CheckArgument(d_sharingTheories == other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
- if(isTheoryEnabled(theory::THEORY_ARITH)) {
- return
- d_integers == other.d_integers &&
- d_reals == other.d_reals &&
- d_linear == other.d_linear &&
- d_differenceLogic == other.d_differenceLogic;
- } else {
- return true;
- }
- }
+ bool operator==(const LogicInfo& other) const;
+
/** Are these two LogicInfos disequal? */
bool operator!=(const LogicInfo& other) const {
return !(*this == other);
}
+
/** Is this LogicInfo "greater than" (does it contain everything and more) the other? */
bool operator>(const LogicInfo& other) const {
return *this >= other && *this != other;
}
+
/** Is this LogicInfo "less than" (does it contain strictly less) the other? */
bool operator<(const LogicInfo& other) const {
return *this <= other && *this != other;
}
/** Is this LogicInfo "less than or equal" the other? */
- bool operator<=(const LogicInfo& other) const {
- 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;
- }
- }
- 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) &&
- (!d_reals || other.d_reals) &&
- (d_linear || !other.d_linear) &&
- (d_differenceLogic || !other.d_differenceLogic);
- } else {
- return true;
- }
- }
+ bool operator<=(const LogicInfo& other) const;
+
/** Is this LogicInfo "greater than or equal" the other? */
- bool operator>=(const LogicInfo& other) const {
- 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;
- }
- }
- 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) &&
- (d_reals || !other.d_reals) &&
- (!d_linear || other.d_linear) &&
- (!d_differenceLogic || other.d_differenceLogic);
- } else {
- return true;
- }
- }
+ bool operator>=(const LogicInfo& other) const;
/** Are two LogicInfos comparable? That is, is one of <= or > true? */
bool isComparableTo(const LogicInfo& other) const {
std::map< int, std::vector< Node > > disj;
std::map< int, std::vector< Node > > fvs;
for( unsigned i=0; i<body.getNumChildren(); i++ ){
- int pid = getPurifyIdLit( body[i] );
-
+ int pid CVC4_UNUSED = getPurifyIdLit( body[i] );
}
//mark as an attribute
//Node attr = NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, body );
-
}
}
#include "theory/uf/theory_uf_model.h"
using namespace std;
-using namespace CVC4;
using namespace CVC4::kind;
using namespace CVC4::context;
-using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace theory {
TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncModels) :
d_substitutions(c, false), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels)
}
}
}
+
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
regexp.h \
smt2_quote_string.cpp \
smt2_quote_string.h \
+ subrange_bound.cpp \
subrange_bound.h \
tuple.h \
unsafe_interrupt_exception.h \
**/
#include "util/abstract_value.h"
+
#include <iostream>
#include <sstream>
#include <string>
+#include "base/cvc4_assert.h"
+
using namespace std;
namespace CVC4 {
AbstractValue::AbstractValue(Integer index) throw(IllegalArgumentException) :
d_index(index) {
- CheckArgument(index >= 1, index, "index >= 1 required for abstract value, not `%s'", index.toString().c_str());
+ PrettyCheckArgument(index >= 1, index, "index >= 1 required for abstract value, not `%s'", index.toString().c_str());
}
}/* CVC4 namespace */
#pragma once
-#include <iostream>
+#include <iosfwd>
#include "util/integer.h"
#include <limits>
#include <functional>
+#include "base/cvc4_assert.h"
#include "base/exception.h"
namespace CVC4 {
#ifndef __CVC4__BITVECTOR_H
#define __CVC4__BITVECTOR_H
-#include <iostream>
+#include <iosfwd>
#include "base/exception.h"
#include "util/integer.h"
namespace CVC4 {
class CVC4_PUBLIC BitVector {
-
-private:
-
- /*
- Class invariants:
- * no overflows: 2^d_size < d_value
- * no negative numbers: d_value >= 0
- */
- unsigned d_size;
- Integer d_value;
-
- Integer toSignedInt() const {
- // returns Integer corresponding to two's complement interpretation of bv
- unsigned size = d_size;
- Integer sign_bit = d_value.extractBitRange(1,size-1);
- Integer val = d_value.extractBitRange(size-1, 0);
- Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
- return res;
- }
-
-
public:
BitVector(unsigned size, const Integer& val):
d_size(size),
d_value(val.modByPow2(size))
{}
-
+
BitVector(unsigned size = 0)
: d_size(size), d_value(0) {}
: d_size(size), d_value(z) {
d_value = d_value.modByPow2(size);
}
-
+
BitVector(unsigned size, unsigned long int z)
: d_size(size), d_value(z) {
d_value = d_value.modByPow2(size);
BitVector(unsigned size, const BitVector& q)
: d_size(size), d_value(q.d_value) {}
-
+
BitVector(const std::string& num, unsigned base = 2);
~BitVector() {}
Integer toInteger() const {
return d_value;
}
-
+
BitVector& operator =(const BitVector& x) {
if(this == &x)
return *this;
}
bool operator ==(const BitVector& y) const {
- if (d_size != y.d_size) return false;
+ if (d_size != y.d_size) return false;
return d_value == y.d_value;
}
bool operator !=(const BitVector& y) const {
- if (d_size != y.d_size) return true;
+ if (d_size != y.d_size) return true;
return d_value != y.d_value;
}
// xor
BitVector operator ^(const BitVector& y) const {
CheckArgument(d_size == y.d_size, y);
- return BitVector(d_size, d_value.bitwiseXor(y.d_value));
+ return BitVector(d_size, d_value.bitwiseXor(y.d_value));
}
-
+
// or
BitVector operator |(const BitVector& y) const {
CheckArgument(d_size == y.d_size, y);
- return BitVector(d_size, d_value.bitwiseOr(y.d_value));
+ return BitVector(d_size, d_value.bitwiseOr(y.d_value));
}
-
+
// and
BitVector operator &(const BitVector& y) const {
CheckArgument(d_size == y.d_size, y);
- return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
+ return BitVector(d_size, d_value.bitwiseAnd(y.d_value));
}
// not
BitVector operator ~() const {
- return BitVector(d_size, d_value.bitwiseNot());
+ return BitVector(d_size, d_value.bitwiseNot());
}
/*
bool operator <(const BitVector& y) const {
- return d_value < y.d_value;
+ return d_value < y.d_value;
}
bool operator >(const BitVector& y) const {
}
bool operator <=(const BitVector& y) const {
- return d_value <= y.d_value;
+ return d_value <= y.d_value;
}
-
+
bool operator >=(const BitVector& y) const {
return d_value >= y.d_value ;
}
-
+
BitVector operator +(const BitVector& y) const {
CheckArgument(d_size == y.d_size, y);
Integer sum = d_value + y.d_value;
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 one(d_size, Integer(1));
return *this + ~y + one;
}
BitVector operator -() const {
- BitVector one(d_size, Integer(1));
+ BitVector one(d_size, Integer(1));
return ~(*this) + one;
}
BitVector setBit(uint32_t i) const {
CheckArgument(i < d_size, i);
Integer res = d_value.setBit(i);
- return BitVector(d_size, res);
+ return BitVector(d_size, res);
}
bool isBitSet(uint32_t i) const {
- CheckArgument(i < d_size, i);
- return d_value.isBitSet(i);
+ CheckArgument(i < d_size, i);
+ return d_value.isBitSet(i);
}
-
- /**
- * Total division function that returns 0 when the denominator is 0.
+
+ /**
+ * Total division function that returns 0 when the denominator is 0.
*/
BitVector unsignedDivTotal (const BitVector& y) const {
}
CheckArgument(d_value >= 0, this);
CheckArgument(y.d_value > 0, y);
- return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
+ return BitVector(d_size, d_value.floorDivideQuotient(y.d_value));
}
-
- /**
- * Total division function that returns 0 when the denominator is 0.
+
+ /**
+ * Total division function that returns 0 when the denominator is 0.
*/
BitVector unsignedRemTotal(const BitVector& y) const {
CheckArgument(d_size == y.d_size, y);
}
CheckArgument(d_value >= 0, this);
CheckArgument(y.d_value > 0, y);
- return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
+ return BitVector(d_size, d_value.floorDivideRemainder(y.d_value));
}
-
-
+
+
bool signedLessThan(const BitVector& y) const {
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();
-
- return a < b;
+ Integer b = y.toSignedInt();
+
+ return a < b;
}
bool unsignedLessThan(const BitVector& y) const {
CheckArgument(d_size == y.d_size, y);
CheckArgument(d_value >= 0, this);
CheckArgument(y.d_value >= 0, y);
- return d_value < y.d_value;
+ return d_value < y.d_value;
}
bool signedLessThanEq(const BitVector& y) const {
CheckArgument(d_value >= 0, this);
CheckArgument(y.d_value >= 0, y);
Integer a = (*this).toSignedInt();
- Integer b = y.toSignedInt();
-
- return a <= b;
+ Integer b = y.toSignedInt();
+
+ return a <= b;
}
bool unsignedLessThanEq(const BitVector& y) const {
CheckArgument(d_size == y.d_size, this);
CheckArgument(d_value >= 0, this);
CheckArgument(y.d_value >= 0, y);
- return d_value <= y.d_value;
+ return d_value <= y.d_value;
}
-
+
/*
Extend operations
*/
-
BitVector zeroExtend(unsigned amount) const {
- return BitVector(d_size + amount, d_value);
+ return BitVector(d_size + amount, d_value);
}
BitVector signExtend(unsigned amount) const {
Integer sign_bit = d_value.extractBitRange(1, d_size -1);
if(sign_bit == Integer(0)) {
- return BitVector(d_size + amount, d_value);
+ return BitVector(d_size + amount, d_value);
} else {
Integer val = d_value.oneExtend(d_size, amount);
return BitVector(d_size+ amount, val);
}
}
-
+
/*
Shifts on BitVectors
*/
-
BitVector leftShift(const BitVector& y) const {
if (y.d_value > Integer(d_size)) {
- return BitVector(d_size, Integer(0));
+ return BitVector(d_size, Integer(0));
}
if (y.d_value == 0) {
- return *this;
+ return *this;
}
// making sure we don't lose information casting
CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
- uint32_t amount = y.d_value.toUnsignedInt();
+ uint32_t amount = y.d_value.toUnsignedInt();
Integer res = d_value.multiplyByPow2(amount);
return BitVector(d_size, res);
}
BitVector logicalRightShift(const BitVector& y) const {
if(y.d_value > Integer(d_size)) {
- return BitVector(d_size, Integer(0));
+ return BitVector(d_size, Integer(0));
}
// making sure we don't lose information casting
CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y);
- uint32_t amount = y.d_value.toUnsignedInt();
- Integer res = d_value.divByPow2(amount);
+ uint32_t amount = y.d_value.toUnsignedInt();
+ Integer res = d_value.divByPow2(amount);
return BitVector(d_size, res);
}
BitVector arithRightShift(const BitVector& y) const {
- Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
+ Integer sign_bit = d_value.extractBitRange(1, d_size - 1);
if(y.d_value > Integer(d_size)) {
if(sign_bit == Integer(0)) {
- return BitVector(d_size, Integer(0));
+ return BitVector(d_size, Integer(0));
} else {
- return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) -1 );
+ return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) -1 );
}
}
-
+
if (y.d_value == 0) {
- return *this;
+ return *this;
}
// making sure we don't lose information casting
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);
+ return BitVector(d_size, rest);
}
Integer res = rest.oneExtend(d_size - amount, amount);
return BitVector(d_size, res);
}
-
+
/*
Convenience functions
*/
-
+
size_t hash() const {
return d_value.hash() + d_size;
}
@return k if the integer is equal to 2^{k-1} and zero otherwise
*/
unsigned isPow2() {
- return d_value.isPow2();
+ return d_value.isPow2();
}
+private:
+ /*
+ Class invariants:
+ * no overflows: 2^d_size < d_value
+ * no negative numbers: d_value >= 0
+ */
+ unsigned d_size;
+ Integer d_value;
+
+ Integer toSignedInt() const {
+ // returns Integer corresponding to two's complement interpretation of bv
+ unsigned size = d_size;
+ Integer sign_bit = d_value.extractBitRange(1,size-1);
+ Integer val = d_value.extractBitRange(size-1, 0);
+ Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val;
+ return res;
+ }
};/* class BitVector */
/**
- * The structure representing the extraction of one Boolean bit.
+ * The structure representing the extraction of one Boolean bit.
*/
struct CVC4_PUBLIC BitVectorBitOf {
/** The index of the bit */
: bitIndex(i) {}
bool operator == (const BitVectorBitOf& other) const {
- return bitIndex == other.bitIndex;
+ return bitIndex == other.bitIndex;
}
};/* struct BitVectorBitOf */
#include "util/cardinality.h"
+#include "base/cvc4_assert.h"
+
+
namespace CVC4 {
const Integer Cardinality::s_unknownCard(0);
const Cardinality Cardinality::REALS(CardinalityBeth(1));
const Cardinality Cardinality::UNKNOWN_CARD((CardinalityUnknown()));
+CardinalityBeth::CardinalityBeth(const Integer& beth)
+ : d_index(beth)
+{
+ PrettyCheckArgument(beth >= 0, beth,
+ "Beth index must be a nonnegative integer, not %s.",
+ beth.toString().c_str());
+}
+
+Cardinality::Cardinality(long card)
+ : d_card(card)
+{
+ PrettyCheckArgument(card >= 0, card,
+ "Cardinality must be a nonnegative integer, not %ld.",
+ card);
+ d_card += 1;
+}
+
+Cardinality::Cardinality(const Integer& card)
+ : d_card(card)
+{
+ PrettyCheckArgument(card >= 0, card,
+ "Cardinality must be a nonnegative integer, not %s.",
+ card.toString().c_str());
+ d_card += 1;
+}
+
+
+Integer Cardinality::getFiniteCardinality() const throw(IllegalArgumentException) {
+ PrettyCheckArgument(isFinite(), *this, "This cardinality is not finite.");
+ PrettyCheckArgument(!isLargeFinite(), *this, "This cardinality is finite, but too large to represent.");
+ return d_card - 1;
+}
+
+Integer Cardinality::getBethNumber() const throw(IllegalArgumentException) {
+ PrettyCheckArgument(!isFinite() && !isUnknown(), *this,
+ "This cardinality is not infinite (or is unknown).");
+ return -d_card - 1;
+}
+
Cardinality& Cardinality::operator+=(const Cardinality& c) throw() {
if(isUnknown()) {
return *this;
Integer d_index;
public:
- CardinalityBeth(const Integer& beth) : d_index(beth) {
- CheckArgument(beth >= 0, beth,
- "Beth index must be a nonnegative integer, not %s.",
- beth.toString().c_str());
- }
+ CardinalityBeth(const Integer& beth);
const Integer& getNumber() const throw() {
return d_index;
* "unsigned" argument to enforce the restriction, we mask some
* errors that automatically convert, like "Cardinality(-1)".
*/
- Cardinality(long card) : d_card(card) {
- CheckArgument(card >= 0, card,
- "Cardinality must be a nonnegative integer, not %ld.", card);
- d_card += 1;
- }
+ Cardinality(long card);
/**
* Construct a finite cardinality equal to the integer argument.
* The argument must be nonnegative.
*/
- Cardinality(const Integer& card) : d_card(card) {
- CheckArgument(card >= 0, card,
- "Cardinality must be a nonnegative integer, not %s.",
- card.toString().c_str());
- d_card += 1;
- }
+ Cardinality(const Integer& card);
/**
* Construct an infinite cardinality equal to the given Beth number.
* cardinality. (If this cardinality is infinite, this function
* throws an IllegalArgumentException.)
*/
- Integer getFiniteCardinality() const throw(IllegalArgumentException) {
- CheckArgument(isFinite(), *this, "This cardinality is not finite.");
- CheckArgument(!isLargeFinite(), *this, "This cardinality is finite, but too large to represent.");
- return d_card - 1;
- }
+ Integer getFiniteCardinality() const throw(IllegalArgumentException);
/**
* In the case that this cardinality is infinite, return its Beth
* number. (If this cardinality is finite, this function throws an
* IllegalArgumentException.)
*/
- Integer getBethNumber() const throw(IllegalArgumentException) {
- CheckArgument(!isFinite() && !isUnknown(), *this,
- "This cardinality is not infinite (or is unknown).");
- return -d_card - 1;
- }
+ Integer getBethNumber() const throw(IllegalArgumentException);
/** Assigning addition of this cardinality with another. */
Cardinality& operator+=(const Cardinality& c) throw();
#include "util/divisible.h"
+#include "base/cvc4_assert.h"
#include "base/exception.h"
using namespace std;
namespace CVC4 {
Divisible::Divisible(const Integer& n) : k(n) {
- CheckArgument(n > 0, n, "Divisible predicate must be constructed over positive N");
+ PrettyCheckArgument(n > 0, n, "Divisible predicate must be constructed over positive N");
}
}/* CVC4 namespace */
#ifndef __CVC4__DIVISIBLE_H
#define __CVC4__DIVISIBLE_H
-#include <iostream>
+#include <iosfwd>
#include "base/exception.h"
#include "util/integer.h"
namespace CVC4 {
- FloatingPointSize::FloatingPointSize (unsigned _e, unsigned _s) : e(_e), s(_s)
- {
- CheckArgument(validExponentSize(_e),_e,"Invalid exponent size : %d",_e);
- CheckArgument(validSignificandSize(_s),_s,"Invalid significand size : %d",_s);
- }
+FloatingPointSize::FloatingPointSize (unsigned _e, unsigned _s) : e(_e), s(_s)
+{
+ PrettyCheckArgument(validExponentSize(_e),_e,"Invalid exponent size : %d",_e);
+ PrettyCheckArgument(validSignificandSize(_s),_s,"Invalid significand size : %d",_s);
+}
- FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), s(old.s)
- {
- CheckArgument(validExponentSize(e),e,"Invalid exponent size : %d",e);
- CheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s);
- }
+FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), s(old.s)
+{
+ PrettyCheckArgument(validExponentSize(e),e,"Invalid exponent size : %d",e);
+ PrettyCheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s);
+}
- void FloatingPointLiteral::unfinished (void) const {
- Unimplemented("Floating-point literals not yet implemented.");
- }
+void FloatingPointLiteral::unfinished (void) const {
+ Unimplemented("Floating-point literals not yet implemented.");
+}
}/* CVC4 namespace */
# error "This source should only ever be built if CVC4_CLN_IMP is on !"
#endif /* CVC4_CLN_IMP */
+#include "base/cvc4_assert.h"
+
using namespace std;
-using namespace CVC4;
+
+namespace CVC4 {
+
+signed int Integer::s_fastSignedIntMin = -(1<<29);
+signed int Integer::s_fastSignedIntMax = (1<<29)-1;
+signed long Integer::s_slowSignedIntMin = (signed long) std::numeric_limits<signed int>::min();
+signed long Integer::s_slowSignedIntMax = (signed long) std::numeric_limits<signed int>::max();
+
+unsigned int Integer::s_fastUnsignedIntMax = (1<<29)-1;
+unsigned long Integer::s_slowUnsignedIntMax = (unsigned long) std::numeric_limits<unsigned int>::max();
+
+Integer Integer::oneExtend(uint32_t size, uint32_t amount) const {
+ 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);
+
+ return Integer(cln::deposit_field(allones, d_value, range));
+}
+
+
+Integer Integer::exactQuotient(const Integer& y) const {
+ DebugCheckArgument(y.divides(*this), y);
+ return Integer( cln::exquo(d_value, y.d_value) );
+}
void Integer::parseInt(const std::string& s, unsigned base) throw(std::invalid_argument) {
}
bool Integer::fitsSignedInt() const {
+ // http://www.ginac.de/CLN/cln.html#Conversions
// TODO improve performance
- return d_value <= std::numeric_limits<signed int>::max() &&
- d_value >= std::numeric_limits<signed int>::min();
+ Assert(s_slowSignedIntMin <= s_fastSignedIntMin);
+ Assert(s_fastSignedIntMin <= s_fastSignedIntMax);
+ Assert(s_fastSignedIntMax <= s_slowSignedIntMax);
+
+ return (d_value <= s_fastSignedIntMax || d_value <= s_slowSignedIntMax) &&
+ (d_value >= s_fastSignedIntMin || d_value >= s_slowSignedIntMax);
}
bool Integer::fitsUnsignedInt() const {
// TODO improve performance
- return sgn() >= 0 && d_value <= std::numeric_limits<unsigned int>::max();
+ Assert(s_fastUnsignedIntMax <= s_slowUnsignedIntMax);
+ return sgn() >= 0 &&
+ (d_value <= s_fastUnsignedIntMax || d_value <= s_slowUnsignedIntMax);
}
signed int Integer::getSignedInt() const {
CheckArgument(fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
return cln::cl_I_to_uint(d_value);
}
+
+} /* namespace CVC4 */
#ifndef __CVC4__INTEGER_H
#define __CVC4__INTEGER_H
-#include <string>
-#include <sstream>
-#include <iostream>
-
-#include <cln/integer.h>
#include <cln/input.h>
+#include <cln/integer.h>
#include <cln/integer_io.h>
+#include <iostream>
#include <limits>
+#include <sstream>
+#include <string>
#include "base/exception.h"
void parseInt(const std::string& s, unsigned base) throw(std::invalid_argument);
+
+ // These constants are to help with CLN conversion in 32 bit.
+ // See http://www.ginac.de/CLN/cln.html#Conversions
+ static signed int s_fastSignedIntMax; /* 2^29 - 1 */
+ static signed int s_fastSignedIntMin; /* -2^29 */
+ static unsigned int s_fastUnsignedIntMax; /* 2^29 - 1 */
+
+ static signed long s_slowSignedIntMax; /* std::numeric_limits<signed int>::max() */
+ static signed long s_slowSignedIntMin; /* std::numeric_limits<signed int>::min() */
+ static unsigned long s_slowUnsignedIntMax; /* std::numeric_limits<unsigned int>::max() */
+
public:
/** Constructs a rational with the value 0. */
return Integer(cln::logior(d_value, mask));
}
- Integer oneExtend(uint32_t size, uint32_t amount) const {
- 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);
-
- return Integer(cln::deposit_field(allones, d_value, range));
- }
+ Integer oneExtend(uint32_t size, uint32_t amount) const;
uint32_t toUnsignedInt() const {
return cln::cl_I_to_uint(d_value);
/**
* If y divides *this, then exactQuotient returns (this/y)
*/
- Integer exactQuotient(const Integer& y) const {
- DebugCheckArgument(y.divides(*this), y);
- return Integer( cln::exquo(d_value, y.d_value) );
- }
+ Integer exactQuotient(const Integer& y) const;
Integer modByPow2(uint32_t exp) const {
cln::cl_byte range(exp, 0);
#include <string>
#include "cvc4autoconfig.h"
+
+#include "base/cvc4_assert.h"
#include "util/rational.h"
#ifndef CVC4_GMP_IMP
# error "This source should only ever be built if CVC4_GMP_IMP is on !"
#endif /* CVC4_GMP_IMP */
-using namespace std;
-using namespace CVC4;
+using namespace std;
+namespace CVC4 {
Integer::Integer(const char* s, unsigned base)
: d_value(s, base)
signed int Integer::getSignedInt() const {
// ensure there isn't overflow
CheckArgument(d_value <= std::numeric_limits<int>::max(), this,
- "Overflow detected in Integer::getSignedInt()");
+ "Overflow detected in Integer::getSignedInt().");
CheckArgument(d_value >= std::numeric_limits<int>::min(), this,
- "Overflow detected in Integer::getSignedInt()");
- CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()");
+ "Overflow detected in Integer::getSignedInt().");
+ CheckArgument(fitsSignedInt(), this,
+ "Overflow detected in Integer::getSignedInt().");
return (signed int) d_value.get_si();
}
"Overflow detected in Integer::getUnsignedInt()");
CheckArgument(d_value >= std::numeric_limits<unsigned int>::min(), this,
"Overflow detected in Integer::getUnsignedInt()");
- CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
+ CheckArgument(fitsSignedInt(), this,
+ "Overflow detected in Integer::getUnsignedInt()");
return (unsigned int) d_value.get_ui();
}
+
+Integer Integer::oneExtend(uint32_t size, uint32_t amount) const {
+ // check that the size is accurate
+ DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
+ mpz_class res = d_value;
+
+ for (unsigned i = size; i < size + amount; ++i) {
+ mpz_setbit(res.get_mpz_t(), i);
+ }
+
+ return Integer(res);
+}
+
+Integer Integer::exactQuotient(const Integer& y) const {
+ 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 );
+}
+
+} /* namespace CVC4 */
#define __CVC4__INTEGER_H
#include <string>
-#include <iostream>
+#include <iosfwd>
#include <limits>
#include "base/exception.h"
* Returns the integer with the binary representation of size bits
* extended with amount 1's
*/
- Integer oneExtend(uint32_t size, uint32_t amount) const {
- // check that the size is accurate
- DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
- mpz_class res = d_value;
-
- for (unsigned i = size; i < size + amount; ++i) {
- mpz_setbit(res.get_mpz_t(), i);
- }
-
- return Integer(res);
- }
+ Integer oneExtend(uint32_t size, uint32_t amount) const;
uint32_t toUnsignedInt() const {
return mpz_get_ui(d_value.get_mpz_t());
/**
* If y divides *this, then exactQuotient returns (this/y)
*/
- Integer exactQuotient(const Integer& y) const {
- 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 );
- }
+ Integer exactQuotient(const Integer& y) const;
/**
* Returns y mod 2^exp
long si = d_value.get_si();
// ensure there wasn't overflow
CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, this,
- "Overflow detected in Integer::getLong()");
+ "Overflow detected in Integer::getLong().");
return si;
}
+
unsigned long getUnsignedLong() const {
unsigned long ui = d_value.get_ui();
// ensure there wasn't overflow
CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, this,
- "Overflow detected in Integer::getUnsignedLong()");
+ "Overflow detected in Integer::getUnsignedLong().");
return ui;
}
#ifndef __CVC4__PROOF_H
#define __CVC4__PROOF_H
-#include <iostream>
+#include <iosfwd>
namespace CVC4 {
# error "This source should only ever be built if CVC4_CLN_IMP is on !"
#endif /* CVC4_CLN_IMP */
+#include "base/cvc4_assert.h"
+
using namespace std;
-using namespace CVC4;
+
+namespace CVC4 {
/* Computes a rational given a decimal string. The rational
* version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>.
}
}
-std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){
+std::ostream& operator<<(std::ostream& os, const Rational& q){
return os << q.toString();
}
ss << ")";
setMessage(ss.str());
}
+
+} /* namespace CVC4 */
#include "cvc4autoconfig.h"
-#ifndef CVC4_GMP_IMP
+#ifndef CVC4_GMP_IMP // Make sure this comes after cvc4autoconfig.h
# error "This source should only ever be built if CVC4_GMP_IMP is on !"
#endif /* CVC4_GMP_IMP */
-std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){
+#include "base/cvc4_assert.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& os, const Rational& q){
return os << q.toString();
}
-namespace CVC4 {
/* Computes a rational given a decimal string. The rational
* version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>.
--- /dev/null
+/********************* */
+/*! \file subrange_bound.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2015 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Representation of subrange bounds
+ **
+ ** Simple class to represent a subrange bound, either infinite
+ ** (no bound) or finite (an arbitrary precision integer).
+ **/
+
+#include "util/subrange_bound.h"
+
+#include <limits>
+
+#include "base/cvc4_assert.h"
+#include "base/exception.h"
+#include "util/integer.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds)
+throw() {
+ out << bounds.lower << ".." << bounds.upper;
+
+ return out;
+}
+
+/** Get the finite SubrangeBound, failing an assertion if infinite. */
+const Integer& SubrangeBound::getBound() const throw(IllegalArgumentException) {
+ PrettyCheckArgument(!d_nobound, this, "SubrangeBound is infinite");
+ return d_bound;
+}
+
+SubrangeBounds::SubrangeBounds(const SubrangeBound& l,
+ const SubrangeBound& u)
+ : lower(l)
+ , upper(u)
+{
+ PrettyCheckArgument(!l.hasBound() || !u.hasBound() ||
+ l.getBound() <= u.getBound(),
+ l, "Bad subrange bounds specified");
+}
+
+bool SubrangeBounds::joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b){
+ return (a.lower.hasBound() && b.lower.hasBound()) ||
+ (a.upper.hasBound() && b.upper.hasBound());
+}
+
+SubrangeBounds SubrangeBounds::join(const SubrangeBounds& a, const SubrangeBounds& 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);
+}
+
+} /* namespace CVC4 */
* has a lower bound of -5 and an infinite upper bound.
*/
class CVC4_PUBLIC SubrangeBound {
- bool d_nobound;
- Integer d_bound;
-
public:
/** Construct an infinite SubrangeBound. */
}
/** Get the finite SubrangeBound, failing an assertion if infinite. */
- const Integer& getBound() const throw(IllegalArgumentException) {
- CheckArgument(!d_nobound, this, "SubrangeBound is infinite");
- return d_bound;
- }
+ const Integer& getBound() const throw(IllegalArgumentException);
/** Returns true iff this is a finite SubrangeBound. */
bool hasBound() const throw() {
}
}
+private:
+ bool d_nobound;
+ Integer d_bound;
};/* class SubrangeBound */
class CVC4_PUBLIC SubrangeBounds {
SubrangeBound lower;
SubrangeBound upper;
- SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u) :
- lower(l),
- upper(u) {
- CheckArgument(!l.hasBound() || !u.hasBound() ||
- l.getBound() <= u.getBound(),
- l, "Bad subrange bounds specified");
- }
+ SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u);
bool operator==(const SubrangeBounds& bounds) const {
return lower == bounds.lower && upper == bounds.upper;
/**
* Returns true if the join of two subranges is not (- infinity, + infinity).
*/
- static bool joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b){
- return (a.lower.hasBound() && b.lower.hasBound()) ||
- (a.upper.hasBound() && b.upper.hasBound());
- }
+ static bool joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b);
/**
* Returns the join of two subranges, a and b.
* precondition: joinIsBounded(a,b) is true
*/
- static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& 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);
- }
+ static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b);
};/* class SubrangeBounds */
return out;
}
-inline std::ostream&
-operator<<(std::ostream& out, const SubrangeBounds& bounds) throw() CVC4_PUBLIC;
-
-inline std::ostream&
-operator<<(std::ostream& out, const SubrangeBounds& bounds) throw() {
- out << bounds.lower << ".." << bounds.upper;
-
- return out;
-}
+std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds)
+throw() CVC4_PUBLIC;
}/* CVC4 namespace */
}
class Foo {
- int blah;
+ int blah CVC4_UNUSED;
public:
Foo(int b) : blah(b) {}
};
projects / cvc5.git / commitdiff