From a39ad6584c1d61e22e72b53c3838f4f675ed2e19 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 24 Dec 2015 05:38:43 -0500 Subject: Miscellaneous fixes - Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example. - Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems. - Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions. - Changing some headers to use iosfwd when possible. --- src/expr/array_store_all.cpp | 73 +++++++++ src/expr/array_store_all.h | 59 +++---- src/expr/datatype.cpp | 111 +++++++------- src/expr/datatype.h | 9 +- src/expr/expr_manager_template.cpp | 296 ++++++++++++++++++++---------------- src/expr/expr_template.cpp | 45 +++--- src/expr/kind_map.h | 1 + src/expr/kind_template.h | 2 +- src/expr/matcher.h | 2 +- src/expr/mkexpr | 2 +- src/expr/node_manager.cpp | 4 +- src/expr/node_manager.h | 3 +- src/expr/predicate.cpp | 16 +- src/expr/record.cpp | 8 +- src/expr/result.cpp | 63 ++++++++ src/expr/result.h | 69 +++------ src/expr/sexpr.cpp | 8 +- src/expr/statistics_registry.cpp | 30 +++- src/expr/statistics_registry.h | 10 +- src/expr/symbol_table.cpp | 25 +-- src/expr/type.cpp | 86 +++++------ src/expr/uninterpreted_constant.cpp | 10 ++ src/expr/uninterpreted_constant.h | 19 +-- 23 files changed, 554 insertions(+), 397 deletions(-) (limited to 'src/expr') 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 +#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 + +#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 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::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& 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 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& 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& children) { Expr ExprManager::mkExpr(Kind kind, Expr child1, const std::vector& 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& 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& 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& datatypes, } std::map::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& 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 +#include +#include #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 -#include -#include - ${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 #include +#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 +#include #include #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 +#include #include #include #include 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& 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::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 +#include + #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 -#include -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, 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& params) const throw() { pair, 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 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& 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 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(); 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 #include +#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 + #include "expr/type.h" -#include 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; -- cgit v1.2.3