summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/array_store_all.cpp73
-rw-r--r--src/expr/array_store_all.h59
-rw-r--r--src/expr/datatype.cpp111
-rw-r--r--src/expr/datatype.h9
-rw-r--r--src/expr/expr_manager_template.cpp296
-rw-r--r--src/expr/expr_template.cpp45
-rw-r--r--src/expr/kind_map.h1
-rw-r--r--src/expr/kind_template.h2
-rw-r--r--src/expr/matcher.h2
-rwxr-xr-xsrc/expr/mkexpr2
-rw-r--r--src/expr/node_manager.cpp4
-rw-r--r--src/expr/node_manager.h3
-rw-r--r--src/expr/predicate.cpp16
-rw-r--r--src/expr/record.cpp8
-rw-r--r--src/expr/result.cpp63
-rw-r--r--src/expr/result.h69
-rw-r--r--src/expr/sexpr.cpp8
-rw-r--r--src/expr/statistics_registry.cpp30
-rw-r--r--src/expr/statistics_registry.h10
-rw-r--r--src/expr/symbol_table.cpp25
-rw-r--r--src/expr/type.cpp86
-rw-r--r--src/expr/uninterpreted_constant.cpp10
-rw-r--r--src/expr/uninterpreted_constant.h19
23 files changed, 554 insertions, 397 deletions
diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index 62c8ec978..d9d0a5f8d 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -20,12 +20,85 @@
#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 */
diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h
index b1d624266..293b785a9 100644
--- a/src/expr/array_store_all.h
+++ b/src/expr/array_store_all.h
@@ -20,61 +20,43 @@
#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);
}
@@ -82,6 +64,9 @@ public:
return !(*this < asa);
}
+private:
+ ArrayType* d_type;
+ Expr* d_expr;
};/* class ArrayStoreAll */
std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) CVC4_PUBLIC;
@@ -90,9 +75,7 @@ std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) CVC4_PUBLI
* 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 */
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 4ebc5071f..b9870afb4 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -67,7 +67,7 @@ const Datatype& Datatype::datatypeOf(Expr item) {
size_t Datatype::indexOf(Expr item) {
ExprManagerScope ems(item);
- CheckArgument(item.getType().isConstructor() ||
+ PrettyCheckArgument(item.getType().isConstructor() ||
item.getType().isTester() ||
item.getType().isSelector(),
item,
@@ -83,7 +83,7 @@ size_t Datatype::indexOf(Expr 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);
@@ -103,17 +103,17 @@ void Datatype::resolve(ExprManager* em,
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) {
@@ -136,14 +136,14 @@ void Datatype::resolve(ExprManager* em,
}
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;
@@ -153,14 +153,14 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
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{
@@ -176,7 +176,7 @@ Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) cons
}
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;
@@ -251,7 +251,8 @@ bool Datatype::computeCardinalityRecSingleton( 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);
@@ -272,7 +273,7 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) {
}
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);
@@ -293,7 +294,7 @@ bool Datatype::isUFinite() const throw(IllegalArgumentException) {
}
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);
@@ -308,7 +309,7 @@ bool Datatype::isWellFounded() const throw(IllegalArgumentException) {
}
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{
@@ -328,7 +329,7 @@ bool Datatype::computeWellFounded( std::vector< Type >& processing ) const throw
}
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);
@@ -348,7 +349,7 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
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;
}
@@ -404,15 +405,15 @@ Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) cons
}
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);
}
@@ -491,7 +492,7 @@ bool Datatype::operator==(const Datatype& other) const throw() {
}
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];
}
@@ -501,7 +502,7 @@ const DatatypeConstructor& Datatype::operator[](std::string name) const {
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 {
@@ -540,8 +541,8 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
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?");
@@ -640,7 +641,7 @@ DatatypeConstructor::DatatypeConstructor(std::string name) :
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) :
@@ -651,8 +652,8 @@ 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 ){
@@ -668,8 +669,8 @@ void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
// 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);
@@ -684,8 +685,8 @@ void DatatypeConstructor::addArg(std::string selectorName, DatatypeUnresolvedTyp
// 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()));
}
@@ -695,7 +696,7 @@ void DatatypeConstructor::addArg(std::string selectorName, DatatypeSelfType) {
// 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()));
}
@@ -708,15 +709,15 @@ std::string DatatypeConstructor::getTesterName() const throw() {
}
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) );
@@ -727,42 +728,42 @@ Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
}
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;
@@ -803,7 +804,8 @@ bool DatatypeConstructor::computeWellFounded( std::vector< Type >& processing )
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);
@@ -822,8 +824,9 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
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);
@@ -899,7 +902,7 @@ Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& proces
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];
}
@@ -909,7 +912,7 @@ const DatatypeConstructorArg& DatatypeConstructor::operator[](std::string name)
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 {
@@ -938,7 +941,7 @@ DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector)
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() {
@@ -951,12 +954,12 @@ 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;
}
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 1ea9fd6be..5f80c54f7 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -798,13 +798,16 @@ inline size_t Datatype::getNumParameters() const throw() {
}
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;
}
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index e7088a395..59f423e3c 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -29,7 +29,7 @@ ${includes}
// 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) \
@@ -164,16 +164,18 @@ RoundingModeType ExprManager::roundingModeType() const {
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);
@@ -186,16 +188,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1) {
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);
@@ -210,16 +214,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) {
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);
@@ -236,16 +242,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3,
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);
@@ -263,16 +271,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3,
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);
@@ -290,16 +300,18 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3,
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);
@@ -321,17 +333,20 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
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);
@@ -355,13 +370,16 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1,
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);
@@ -374,13 +392,16 @@ Expr ExprManager::mkExpr(Expr opExpr) {
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);
@@ -393,13 +414,16 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1) {
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);
@@ -414,9 +438,11 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) {
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(),
@@ -437,13 +463,18 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
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);
@@ -461,13 +492,16 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
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);
@@ -485,13 +519,16 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
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);
@@ -652,11 +689,12 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
}
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);
}
@@ -687,10 +725,11 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
}
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
@@ -902,9 +941,10 @@ Expr ExprManager::mkBoundVar(Type type) {
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);
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index dbd7c049b..dfbe179be 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -13,18 +13,18 @@
**
** 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
@@ -326,15 +326,16 @@ bool Expr::hasOperator() const {
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);
}
@@ -509,40 +510,40 @@ Expr Expr::notExpr() const {
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);
}
@@ -550,10 +551,10 @@ Expr Expr::iteExpr(const Expr& then_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);
}
diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h
index d3ed43e1c..02e9728f0 100644
--- a/src/expr/kind_map.h
+++ b/src/expr/kind_map.h
@@ -23,6 +23,7 @@
#include <stdint.h>
#include <iterator>
+#include "base/cvc4_assert.h"
#include "expr/kind.h"
namespace CVC4 {
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index c2ccb6b5e..799d1ac33 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -19,7 +19,7 @@
#ifndef __CVC4__KIND_H
#define __CVC4__KIND_H
-#include <iostream>
+#include <iosfwd>
#include <sstream>
#include "base/exception.h"
diff --git a/src/expr/matcher.h b/src/expr/matcher.h
index 92b1ce109..8cb092a64 100644
--- a/src/expr/matcher.h
+++ b/src/expr/matcher.h
@@ -19,7 +19,7 @@
#ifndef __CVC4__MATCHER_H
#define __CVC4__MATCHER_H
-#include <iostream>
+#include <iosfwd>
#include <string>
#include <vector>
#include <map>
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 068063c05..4717b611d 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -239,7 +239,7 @@ template <> $2 const & Expr::getConst< $2 >() const;
#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 >();
}
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 17524a3c0..c9e6866d4 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -393,8 +393,8 @@ TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor,
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);
}
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 390af8967..870408939 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1098,7 +1098,8 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
"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);
}
diff --git a/src/expr/predicate.cpp b/src/expr/predicate.cpp
index a4dd29592..5ccc3484a 100644
--- a/src/expr/predicate.cpp
+++ b/src/expr/predicate.cpp
@@ -34,9 +34,11 @@ Predicate::Predicate(const Expr& e) throw(IllegalArgumentException)
: 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)
@@ -44,9 +46,11 @@ 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() {
diff --git a/src/expr/record.cpp b/src/expr/record.cpp
index 2dee03dbf..ec5ef96f1 100644
--- a/src/expr/record.cpp
+++ b/src/expr/record.cpp
@@ -68,8 +68,9 @@ bool Record::contains(const std::string& name) const {
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();
}
@@ -115,7 +116,8 @@ std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) {
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];
}
diff --git a/src/expr/result.cpp b/src/expr/result.cpp
index 95e382b98..aeb62b0c3 100644
--- a/src/expr/result.cpp
+++ b/src/expr/result.cpp
@@ -29,6 +29,62 @@ using namespace std;
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),
@@ -78,6 +134,13 @@ Result::Result(const std::string& instr, std::string inputName) :
}
}
+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;
diff --git a/src/expr/result.h b/src/expr/result.h
index 74697eba6..8069f7ef9 100644
--- a/src/expr/result.h
+++ b/src/expr/result.h
@@ -75,49 +75,20 @@ private:
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) {
@@ -128,24 +99,24 @@ public:
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();
diff --git a/src/expr/sexpr.cpp b/src/expr/sexpr.cpp
index 0c0828616..69741859f 100644
--- a/src/expr/sexpr.cpp
+++ b/src/expr/sexpr.cpp
@@ -311,7 +311,7 @@ bool SExpr::languageQuotesKeywords(OutputLanguage language) {
std::string SExpr::getValue() const {
- CheckArgument( isAtom(), this );
+ PrettyCheckArgument( isAtom(), this );
switch(d_sexprType) {
case SEXPR_INTEGER:
return d_integerValue.toString();
@@ -335,17 +335,17 @@ std::string SExpr::getValue() const {
}
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;
}
diff --git a/src/expr/statistics_registry.cpp b/src/expr/statistics_registry.cpp
index c1db992c5..bf36236f7 100644
--- a/src/expr/statistics_registry.cpp
+++ b/src/expr/statistics_registry.cpp
@@ -17,6 +17,7 @@
#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"
@@ -36,6 +37,19 @@
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.
@@ -60,9 +74,9 @@ StatisticsRegistry* StatisticsRegistry::current() {
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() */
@@ -70,7 +84,7 @@ void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentExcept
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);
@@ -81,14 +95,14 @@ void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentExce
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_() */
@@ -107,7 +121,7 @@ void StatisticsRegistry::flushInformation(std::ostream &out) const {
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;
}
@@ -115,7 +129,7 @@ void TimerStat::start() {
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;
diff --git a/src/expr/statistics_registry.h b/src/expr/statistics_registry.h
index 89efe4021..4793f1301 100644
--- a/src/expr/statistics_registry.h
+++ b/src/expr/statistics_registry.h
@@ -607,15 +607,7 @@ public:
/** 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
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 3d53f2e44..c0a80b7ce 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -17,17 +17,18 @@
**/
#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;
@@ -49,7 +50,7 @@ SymbolTable::~SymbolTable() {
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);
@@ -57,7 +58,7 @@ void SymbolTable::bind(const std::string& name, Expr 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);
@@ -121,7 +122,7 @@ bool SymbolTable::isBoundType(const std::string& name) const throw() {
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());
@@ -131,12 +132,12 @@ Type SymbolTable::lookupType(const std::string& name) const throw() {
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()) {
@@ -161,7 +162,7 @@ Type SymbolTable::lookupType(const std::string& name,
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")) {
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 327be72eb..99d04d658 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -92,8 +92,8 @@ Type Type::getBaseType() const {
}
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) {
@@ -354,7 +354,7 @@ vector<Type> FunctionType::getArgTypes() const {
Type FunctionType::getRangeType() const {
NodeManagerScope nms(d_nodeManager);
- CheckArgument(isNull() || isFunction(), this);
+ PrettyCheckArgument(isNull() || isFunction(), this);
return makeType(d_typeNode->getRangeType());
}
@@ -430,112 +430,112 @@ SortType SortConstructorType::instantiate(const std::vector<Type>& params) const
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 {
@@ -585,7 +585,7 @@ std::vector<Type> ConstructorType::getArgTypes() 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 {
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp
index d41ab1045..97bc3ae4b 100644
--- a/src/expr/uninterpreted_constant.cpp
+++ b/src/expr/uninterpreted_constant.cpp
@@ -20,10 +20,20 @@
#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();
diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h
index 13a80a19d..5b2293df6 100644
--- a/src/expr/uninterpreted_constant.h
+++ b/src/expr/uninterpreted_constant.h
@@ -18,26 +18,18 @@
#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;
@@ -68,6 +60,9 @@ public:
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback