diff options
53 files changed, 1736 insertions, 174 deletions
diff --git a/Makefile.builds.in b/Makefile.builds.in index 5ef00509b..e6d6e7bcd 100644 --- a/Makefile.builds.in +++ b/Makefile.builds.in @@ -111,6 +111,8 @@ endif check test units regress: all (cd $(CURRENT_BUILD)/test && $(MAKE) $@) +units%: + (cd $(CURRENT_BUILD)/test && $(MAKE) units TEST_PREFIX=$(subst units:,,$@)) regress%: all (cd $(CURRENT_BUILD)/test && $(MAKE) $@) diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 1d7af717b..4ed5a3ac7 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -31,6 +31,7 @@ libexpr_la_SOURCES = \ nodist_libexpr_la_SOURCES = \ kind.h \ metakind.h \ + type_properties.h \ expr.h \ expr.cpp \ expr_manager.h \ @@ -39,6 +40,7 @@ nodist_libexpr_la_SOURCES = \ EXTRA_DIST = \ kind_template.h \ metakind_template.h \ + type_properties_template.h \ expr_manager_template.h \ expr_manager_template.cpp \ expr_template.h \ @@ -50,6 +52,7 @@ EXTRA_DIST = \ BUILT_SOURCES = \ kind.h \ metakind.h \ + type_properties.h \ expr.h \ expr.cpp \ expr_manager.h \ @@ -83,6 +86,14 @@ metakind.h: metakind_template.h mkmetakind @top_builddir@/src/theory/.subdirs @t `cat @top_builddir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) +type_properties.h: type_properties_template.h mkkind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds + $(AM_V_at)chmod +x @srcdir@/mkkind + $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true + $(AM_V_GEN)(@srcdir@/mkkind \ + $< \ + `cat @top_builddir@/src/theory/.subdirs` \ + > $@) || (rm -f $@ && exit 1) + expr.h: expr_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkexpr $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index b7f376811..f395d781c 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -278,7 +278,6 @@ public: */ Expr mkAssociative(Kind kind, const std::vector<Expr>& children); - /** Make a function type from domain to range. */ FunctionType mkFunctionType(Type domain, Type range); diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 24cb6dc5d..43d40105e 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -758,7 +758,7 @@ public: ${getConst_instantiations} -#line 758 "${template}" +#line 762 "${template}" namespace expr { diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 6b9787f6c..724f7413f 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Template for the Node kind header. + ** \brief Template for the Node kind header ** ** Template for the Node kind header. **/ diff --git a/src/expr/mkexpr b/src/expr/mkexpr index da2847d84..a7302da26 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -104,10 +104,17 @@ function endtheory { # endtheory lineno=${BASH_LINENO[0]} check_theory_seen + seen_endtheory=true } function sort { - # sort TYPE ["comment"] + # sort TYPE cardinality ["comment"] + lineno=${BASH_LINENO[0]} + check_theory_seen +} + +function cardinality { + # cardinality TYPE cardinality-computer [header] lineno=${BASH_LINENO[0]} check_theory_seen } @@ -164,6 +171,10 @@ template <> $2 const & Expr::getConst() const { } function check_theory_seen { + if $seen_endtheory; then + echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2 + exit 1 + fi if ! $seen_theory; then echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2 exit 1 @@ -179,15 +190,27 @@ function check_builtin_theory_seen { while [ $# -gt 0 ]; do kf=$1 seen_theory=false + seen_endtheory=false b=$(basename $(dirname "$kf")) source "$kf" - check_theory_seen + if ! $seen_theory; then + echo "$kf: error: no theory content found in file!" >&2 + exit 1 + fi + if ! $seen_endtheory; then + echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2 + exit 1 + fi shift done check_builtin_theory_seen ## output +# generate warnings about incorrect #line annotations in templates +nl -ba -s' ' "$template" | grep '^ *[0-9][0-9]* # *line' | + awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2 + text=$(cat "$template") for var in \ includes \ @@ -195,7 +218,8 @@ for var in \ getConst_instantiations \ getConst_implementations \ mkConst_instantiations \ - mkConst_implementations; do + mkConst_implementations \ + ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` diff --git a/src/expr/mkkind b/src/expr/mkkind index fa80894b2..08d874c79 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -4,8 +4,8 @@ # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 # Copyright (c) 2010-2011 The CVC4 Project # -# The purpose of this script is to create kind.h from a template and a -# list of theory kinds. +# The purpose of this script is to create kind.h (and also +# type_properties.h) from a template and a list of theory kinds. # # Invocation: # @@ -16,9 +16,11 @@ copyright=2010-2011 +filename=`basename "$1" | sed 's,_template,,'` + cat <<EOF /********************* */ -/** kind.h +/** $filename ** ** Copyright $copyright The AcSys Group, New York University, and as below. ** @@ -29,6 +31,23 @@ cat <<EOF ** for the CVC4 project. **/ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ + +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ + +/* Edit the template file instead: */ +/* $1 */ + EOF me=$(basename "$0") @@ -42,6 +61,9 @@ kind_to_theory_id= type_constant_descriptions= type_constant_list= type_constant_to_theory_id= +type_cardinalities= +type_constant_cardinalities= +type_cardinalities_includes= seen_theory=false seen_theory_builtin=false @@ -89,6 +111,7 @@ function endtheory { # endtheory lineno=${BASH_LINENO[0]} check_theory_seen + seen_endtheory=true } function rewriter { @@ -98,10 +121,17 @@ function rewriter { } function sort { - # sort TYPE ["comment"] + # sort TYPE cardinality ["comment"] lineno=${BASH_LINENO[0]} check_theory_seen - register_sort "$1" "$2" + register_sort "$1" "$2" "$3" +} + +function cardinality { + # cardinality TYPE cardinality-computer [header] + lineno=${BASH_LINENO[0]} + check_theory_seen + register_cardinality "$1" "$2" "$3" } function variable { @@ -142,14 +172,33 @@ function constant { function register_sort { id=$1 - comment=$2 + cardinality=$2 + comment=$3 type_constant_list="${type_constant_list} ${id}, /**< ${comment} */ " type_constant_descriptions="${type_constant_descriptions} case $id: out << \"${comment}\"; break; " - type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break; + type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; +" + type_constant_cardinalities="${type_constant_cardinalities}#line $lineno \"$kf\" + case $id: return Cardinality($cardinality); +" +} + +function register_cardinality { + id=$1 + cardinality_computer=$(sed 's,%TYPE%,typeNode,g' <<<"$2") + header=$3 + + type_cardinalities="${type_cardinalities}#line $lineno \"$kf\" + case $id: return $cardinality_computer; +" + if [ -n "$header" ]; then + type_cardinalities_includes="${type_cardinalities_includes}#line $lineno \"$kf\" +#include \"$header\" " + fi } function register_kind { @@ -161,11 +210,15 @@ function register_kind { " kind_printers="${kind_printers} case $r: out << \"$r\"; break; " - kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id; break; + kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id; " } function check_theory_seen { + if $seen_endtheory; then + echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2 + exit 1 + fi if ! $seen_theory; then echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2 exit 1 @@ -181,6 +234,7 @@ function check_builtin_theory_seen { while [ $# -gt 0 ]; do kf=$1 seen_theory=false + seen_endtheory=false b=$(basename $(dirname "$kf")) kind_decls="${kind_decls} /* from $b */ @@ -189,15 +243,39 @@ while [ $# -gt 0 ]; do /* from $b */ " source "$kf" - check_theory_seen + if ! $seen_theory; then + echo "$kf: error: no theory content found in file!" >&2 + exit 1 + fi + if ! $seen_endtheory; then + echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2 + exit 1 + fi shift done check_builtin_theory_seen ## output +# generate warnings about incorrect #line annotations in templates +nl -ba -s' ' "$template" | grep '^ *[0-9][0-9]* # *line' | + awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2 + text=$(cat "$template") -for var in kind_decls kind_printers kind_to_theory_id theory_enum type_constant_list type_constant_descriptions type_constant_to_theory_id theory_descriptions; do +for var in \ + kind_decls \ + kind_printers \ + kind_to_theory_id \ + theory_enum \ + type_constant_list \ + type_constant_descriptions \ + type_constant_to_theory_id \ + type_cardinalities \ + type_constant_cardinalities \ + type_cardinalities_includes \ + theory_descriptions \ + template \ + ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 7f9037c1c..00599c5a0 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -90,6 +90,7 @@ function endtheory { # endtheory lineno=${BASH_LINENO[0]} check_theory_seen + seen_endtheory=true } function rewriter { @@ -99,7 +100,13 @@ function rewriter { } function sort { - # sort TYPE ["comment"] + # sort TYPE cardinality ["comment"] + lineno=${BASH_LINENO[0]} + check_theory_seen +} + +function cardinality { + # cardinality TYPE cardinality-computer [header] lineno=${BASH_LINENO[0]} check_theory_seen } @@ -287,6 +294,10 @@ function primitive_type { } function check_theory_seen { + if $seen_endtheory; then + echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2 + exit 1 + fi if ! $seen_theory; then echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2 exit 1 @@ -302,6 +313,7 @@ function check_builtin_theory_seen { while [ $# -gt 0 ]; do kf=$1 seen_theory=false + seen_endtheory=false b=$(basename $(dirname "$kf")) metakind_kinds="${metakind_kinds} /* from $b */ @@ -310,13 +322,24 @@ while [ $# -gt 0 ]; do /* from $b */ " source "$kf" - check_theory_seen + if ! $seen_theory; then + echo "$kf: error: no theory content found in file!" >&2 + exit 1 + fi + if ! $seen_endtheory; then + echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2 + exit 1 + fi shift done check_builtin_theory_seen ## output +# generate warnings about incorrect #line annotations in templates +nl -ba -s' ' "$template" | grep '^ *[0-9][0-9]* # *line' | + awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2 + text=$(cat "$template") for var in \ metakind_includes \ @@ -328,7 +351,9 @@ for var in \ metakind_constDeleters \ metakind_ubchildren \ metakind_lbchildren \ - metakind_operatorKinds; do + metakind_operatorKinds \ + template \ + ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 4ea425aa7..27a3f9da7 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -68,6 +68,11 @@ bool Type::isNull() const { return d_typeNode->isNull(); } +Cardinality Type::getCardinality() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getCardinality(); +} + Type& Type::operator=(const Type& t) { Assert(d_typeNode != NULL, "Unexpected NULL typenode pointer!"); Assert(t.d_typeNode != NULL, "Unexpected NULL typenode pointer!"); diff --git a/src/expr/type.h b/src/expr/type.h index 290bb360a..89cb994e7 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -27,6 +27,7 @@ #include <stdint.h> #include "util/Assert.h" +#include "util/cardinality.h" namespace CVC4 { @@ -137,6 +138,11 @@ public: bool isNull() const; /** + * Return the cardinality of this type. + */ + Cardinality getCardinality() const; + + /** * Substitution of Types. */ Type substitute(const Type& type, const Type& replacement) const; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 0b22fdf0f..e48a92321 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -19,6 +19,7 @@ #include <vector> #include "expr/type_node.h" +#include "expr/type_properties.h" using namespace std; @@ -46,6 +47,10 @@ TypeNode TypeNode::substitute(const TypeNode& type, return nb.constructTypeNode(); } +Cardinality TypeNode::getCardinality() const { + return kind::getCardinality(*this); +} + bool TypeNode::isBoolean() const { return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE; diff --git a/src/expr/type_node.h b/src/expr/type_node.h index c04bef0c7..f51d7a9ba 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -32,6 +32,7 @@ #include "expr/kind.h" #include "expr/metakind.h" #include "util/Assert.h" +#include "util/cardinality.h" namespace CVC4 { @@ -342,6 +343,13 @@ public: return d_nv == &expr::NodeValue::s_null; } + /** + * Returns the cardinality of this type. + * + * @return a finite or infinite cardinality + */ + Cardinality getCardinality() const; + /** Is this the Boolean type? */ bool isBoolean() const; diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h new file mode 100644 index 000000000..b6fd644c8 --- /dev/null +++ b/src/expr/type_properties_template.h @@ -0,0 +1,87 @@ +/********************* */ +/*! \file type_properties_template.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Template for the Type properties header + ** + ** Template for the Type properties header. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__TYPE_PROPERTIES_H +#define __CVC4__TYPE_PROPERTIES_H + +#line 25 "${template}" + +#include "expr/type_node.h" +#include "util/Assert.h" +#include "expr/kind.h" +#include "expr/expr.h" +#include "util/language.h" + +#include <sstream> + +${type_cardinalities_includes} + +#line 37 "${template}" + +namespace CVC4 { +namespace kind { + +/** + * Return the cardinality of the type constant represented by the + * TypeConstant argument. This function is auto-generated from Theory + * "kinds" files, so includes contributions from each theory regarding + * that theory's types. + */ +inline Cardinality getCardinality(TypeConstant tc) { + switch(tc) { +${type_constant_cardinalities} +#line 51 "${template}" + default: { + std::stringstream ss; + ss << "No cardinality known for type constant " << tc; + InternalError(ss.str()); + } + } +}/* getCardinality(TypeConstant) */ + +/** + * Return the cardinality of the type represented by the TypeNode + * argument. This function is auto-generated from Theory "kinds" + * files, so includes contributions from each theory regarding that + * theory's types. + */ +inline Cardinality getCardinality(TypeNode typeNode) { + AssertArgument(!typeNode.isNull(), typeNode); + switch(Kind k = typeNode.getKind()) { + case TYPE_CONSTANT: + return getCardinality(typeNode.getConst<TypeConstant>()); +${type_cardinalities} +#line 72 "${template}" + default: { + std::stringstream ss; + ss << Expr::setlanguage(language::toOutputLanguage + ( Options::current()->inputLanguage )); + ss << "A theory kinds file did not provide a cardinality " + << "or cardinality computer for type:\n" << typeNode + << "\nof kind " << k; + InternalError(ss.str()); + } + } +}/* getCardinality(TypeNode) */ + +}/* CVC4::kind namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__TYPE_PROPERTIES_H */ diff --git a/src/lib/replacements.h b/src/lib/replacements.h index c930d2654..6e6f0d0f5 100644 --- a/src/lib/replacements.h +++ b/src/lib/replacements.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -16,6 +16,8 @@ ** Common header for replacement function sources. **/ +#include "cvc4_public.h" + #ifndef __CVC4__LIB__REPLACEMENTS_H #define __CVC4__LIB__REPLACEMENTS_H diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index d9291c903..8df9ea6a0 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1361,7 +1361,7 @@ bvNegTerm[CVC4::Expr& f] postfixTerm[CVC4::Expr& f] @init { Expr f2; - bool extract, left; + bool extract = false, left = false; std::vector<Expr> args; std::string id; } @@ -1718,7 +1718,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes] constructorDef[CVC4::Datatype& type] @init { std::string id; - CVC4::Datatype::Constructor* ctor; + CVC4::Datatype::Constructor* ctor = NULL; } : identifier[id,CHECK_UNDECLARED,SYM_SORT] { diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 0d680f4c9..eecf95875 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -71,3 +71,15 @@ theory_traits.h: theory_traits_template.h mktheorytraits @top_builddir@/src/theo $< \ `cat @top_builddir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) + +AM_V_CHECK = $(am__v_CHECK_$(V)) +am__v_CHECK_ = $(am__v_CHECK_$(AM_DEFAULT_VERBOSITY)) +am__v_CHECK_0 = @echo " CHECK " $@; + +.PHONY: theory-properties +theory-properties: + $(AM_V_CHECK)@srcdir@/mktheorytraits \ + theory_traits_template.h \ + `cat @top_builddir@/src/theory/.subdirs` \ + > /dev/null +all-local check-local: theory-properties diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 9e2e3a3a7..a0fc71ab4 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -6,7 +6,8 @@ theory THEORY_ARITH ::CVC4::theory::arith::TheoryArith "theory/arith/theory_arith.h" -properties stable-infinite check propagate staticLearning presolve +properties stable-infinite +properties check propagate staticLearning presolve notifyRestart rewriter ::CVC4::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h" @@ -17,8 +18,8 @@ operator MINUS 2 "arithmetic binary subtraction operator" operator UMINUS 1 "arithmetic unary negation" operator DIVISION 2 "arithmetic division" -sort REAL_TYPE "Real type" -sort INTEGER_TYPE "Integer type" +sort REAL_TYPE Cardinality::REALS "Real type" +sort INTEGER_TYPE Cardinality::INTEGERS "Integer type" constant CONST_RATIONAL \ ::CVC4::Rational \ @@ -37,4 +38,4 @@ operator LEQ 2 "less than or equal, x <= y" operator GT 2 "greater than, x > y" operator GEQ 2 "greater than or equal, x >= y" -endtheory
\ No newline at end of file +endtheory diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 7738f50ca..533145dc2 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -6,11 +6,15 @@ theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h" -properties polite stable-infinite +properties polite stable-infinite +properties check rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h" operator ARRAY_TYPE 2 "array type" +cardinality ARRAY_TYPE \ + "::CVC4::theory::arrays::CardinalityComputer::computeCardinality(%TYPE%)" \ + "theory/arrays/theory_arrays_type_rules.h" # select a i is a[i] operator SELECT 2 "array select" @@ -18,4 +22,4 @@ operator SELECT 2 "array select" # store a i e is a[i] <= e operator STORE 3 "array store" -endtheory
\ No newline at end of file +endtheory diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 64fdd8303..fbbda9e44 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -34,14 +34,14 @@ public: TheoryArrays(context::Context* c, OutputChannel& out, Valuation valuation); ~TheoryArrays(); void preRegisterTerm(TNode n) { } - void registerTerm(TNode n) { } + //void registerTerm(TNode n) { } - void presolve() { } + //void presolve() { } void addSharedTerm(TNode t); void notifyEq(TNode lhs, TNode rhs); void check(Effort e); - void propagate(Effort e) { } + //void propagate(Effort e) { } void explain(TNode n) { } Node getValue(TNode n); void shutdown() { } diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 11e8a8443..bd3c8ad67 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -11,9 +11,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Theory of arrays. + ** \brief Typing and cardinality rules for the theory of arrays ** - ** Theory of arrays. + ** Typing and cardinality rules for the theory of arrays. **/ #include "cvc4_private.h" @@ -65,6 +65,17 @@ struct ArrayStoreTypeRule { } };/* struct ArrayStoreTypeRule */ +struct CardinalityComputer { + inline static Cardinality computeCardinality(TypeNode type) { + Assert(type.getKind() == kind::ARRAY_TYPE); + + Cardinality indexCard = type[0].getCardinality(); + Cardinality valueCard = type[1].getCardinality(); + + return valueCard ^ indexCard; + } +};/* struct CardinalityComputer */ + }/* CVC4::theory::arrays namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index 25ca1cfe3..ce7c9111a 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -6,11 +6,11 @@ theory THEORY_BOOL ::CVC4::theory::booleans::TheoryBool "theory/booleans/theory_bool.h" -properties finite +properties finite rewriter ::CVC4::theory::booleans::TheoryBoolRewriter "theory/booleans/theory_bool_rewriter.h" -sort BOOLEAN_TYPE "Boolean type" +sort BOOLEAN_TYPE 2 "Boolean type" constant CONST_BOOLEAN \ bool \ diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index dfcdd22b8..fd6d20e03 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -34,15 +34,6 @@ public: Theory(THEORY_BOOL, c, out, valuation) { } - void preRegisterTerm(TNode n) { - Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl; - Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl; - } - void registerTerm(TNode n) { - Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl; - Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl; - } - Node getValue(TNode n); std::string identify() const { return std::string("TheoryBool"); } diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 2831161c3..a170ba145 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -6,12 +6,58 @@ # The first non-blank, non-comment line in this file must be a theory # declaration: # -# theory [builtin] T header +# theory ID T header # -# The special tag "builtin" declares that this is the builtin theory. -# There can be only one and it should be processed first. +# Thereafter, ID is bound to your theory. It becomes part of an +# enumeration that identifies all theories. If your theory has +# several, distinct implementations, they still all share a kinds +# file, a theory ID, all the defined kinds/operators/types for the +# theory, typechecker, etc. They should also share a base class +# (that's the T above). The header is the header for this base +# class. # -# There are four basic commands for declaring kinds: +# The very end of this file should end with: +# +# endtheory +# +# There are several basic commands: +# +# properties PROPERTIES... +# +# This command declares properties of the theory. It can occur +# more than once, in which case the effect is additive. +# +# The current set of properties and their meanings are: +# +# finite the theory is finite +# stable-infinite the theory is stably infinite +# polite the theory is polite +# +# check the theory supports the check() function +# propagate the theory supports propagate() (and explain()) +# staticLearning the theory supports staticLearning() +# registerTerm the theory supports registerTerm() +# notifyRestart the theory supports notifyRestart() +# presolve the theory supports presolve() +# +# In the case of the "theory-supports-function" properties, you +# need to declare these for your theory or the functions will not +# be called! This is used to speed up the core where functionality +# is not needed. +# +# rewriter T header +# +# This declares a rewriter class T for your theory, declared in +# header. Your rewriter class provides four functions: +# +# static void init(); +# static void shutdown(); +# static RewriteResponse preRewrite(TNode node); +# static RewriteResponse postRewrite(TNode node); +# +# ...BUT please note that init() and shutdown() may be removed in +# future, so if possible, do not rely on them being called (and +# implement them as a no-op). # # variable K ["comment"] # @@ -76,6 +122,54 @@ # For consistency, constants taking a non-void payload should # start with "CONST_", but this is not enforced. # +# sort K cardinality ["comment"] +# +# This creates a kind K that represents a sort (a "type constant"). +# These kinds of types are "atomic" types; if you need to describe +# a complex type that takes type arguments (like arrays), use +# "operator"; if you need to describe one that takes "constant" +# arguments (like bitvectors), use "constant", and if you invent +# one that takes both, you could try "parameterized". In those +# cases, you'll want to provide a cardinality separately for your +# type. +# +# The cardinality argument is a nonnegative number (if the sort is +# finite), or Cardinality::INTEGERS if the sort has the same +# cardinality as the integers, or Cardinality::REALS if the sort +# has the same cardinality as the reals. +# +# For consistency, sorts should end with "_TYPE", but this is not +# enforced. +# +# cardinality K cardinality-computer [header] +# +# This command does not define a kind; the kind K needs to be +# defined by one of the other commands above. This command just +# provides a cardinality for types of kind K. The +# "cardinality-computer" is a C++ expression that will yield a +# Cardinality for the type. In that expression, the sequence of +# characters "%TYPE%" will be rewritten with a variable containing +# a TypeNode of kind K. The optional "header" argument is an +# include file necessary to compile the cardinality-computer +# expression. +# +# If the cardinality need not be computed per-type (i.e., it's the +# same for all types of kind K, but the "sort" gesture above could +# not be used---in which case it doesn't already have a registered +# cardinality), you can simply construct a Cardinality temporary. +# For example: +# +# cardinality MY_TYPE Cardinality(Cardinality::INTEGERS) +# +# If not, you might opt to use a computer; a common place to put it +# is with your type checker: +# +# cardinality MY_TYPE \ +# ::CVC4::theory::foo::TheoryFoo::CardinalityComputer(%TYPE%) \ +# "theory/foo/theory_foo_type_rules.h" +# +# +# # Lines may be broken with a backslash between arguments; for example: # # constant CONST_INT \ @@ -108,12 +202,12 @@ theory THEORY_BUILTIN ::CVC4::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h" -properties stable-infinite +properties stable-infinite # Rewriter responisble for all the terms of the theory rewriter ::CVC4::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h" -sort BUILTIN_OPERATOR_TYPE "Built in type for built in operators" +sort BUILTIN_OPERATOR_TYPE Cardinality::INTEGERS "Built in type for built in operators" # A kind representing "inlined" operators defined with OPERATOR # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's @@ -140,6 +234,12 @@ constant TYPE_CONSTANT \ "expr/kind.h" \ "basic types" operator FUNCTION_TYPE 2: "function type" +cardinality FUNCTION_TYPE \ + "::CVC4::theory::builtin::FunctionCardinality::computeCardinality(%TYPE%)" \ + "theory/builtin/theory_builtin_type_rules.h" operator TUPLE_TYPE 2: "tuple type" +cardinality TUPLE_TYPE \ + "::CVC4::theory::builtin::TupleCardinality::computeCardinality(%TYPE%)" \ + "theory/builtin/theory_builtin_type_rules.h" -endtheory
\ No newline at end of file +endtheory diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 0d313594c..bebfca9ab 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -128,6 +128,39 @@ public: } };/* class TupleTypeRule */ +class FunctionCardinality { +public: + inline static Cardinality computeCardinality(TypeNode type) { + Assert(type.getKind() == kind::FUNCTION_TYPE); + + Cardinality argsCard(1); + // get the largest cardinality of function arguments/return type + for(unsigned i = 0, i_end = type.getNumChildren() - 1; i < i_end; ++i) { + argsCard *= type[i].getCardinality(); + } + + Cardinality valueCard = type[type.getNumChildren() - 1].getCardinality(); + + return valueCard ^ argsCard; + } +};/* class FuctionCardinality */ + +class TupleCardinality { +public: + inline static Cardinality computeCardinality(TypeNode type) { + Assert(type.getKind() == kind::TUPLE_TYPE); + + Cardinality card(1); + for(TypeNode::iterator i = type.begin(), + i_end = type.end(); + i != i_end; + ++i) { + card *= (*i).getCardinality(); + } + + return card; + } +};/* class TupleCardinality */ }/* CVC4::theory::builtin namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 381e90d47..d10e32ee0 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -6,7 +6,8 @@ theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h" -properties finite check propagate +properties finite +properties check propagate rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h" @@ -15,6 +16,9 @@ constant BITVECTOR_TYPE \ "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \ "util/bitvector.h" \ "bit-vector type" +cardinality BITVECTOR_TYPE \ + "::CVC4::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \ + "theory/bv/theory_bv_type_rules.h" constant CONST_BITVECTOR \ ::CVC4::BitVector \ @@ -95,4 +99,4 @@ parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign- parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left" parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right" -endtheory
\ No newline at end of file +endtheory diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index d65f0388b..748352321 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -113,11 +113,11 @@ public: void preRegisterTerm(TNode n); - void registerTerm(TNode n) { } + //void registerTerm(TNode n) { } void check(Effort e); - void presolve() { } + //void presolve() { } void propagate(Effort e) { } diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index a27fd351c..613df47f3 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -189,6 +189,20 @@ public: } }; +class CardinalityComputer { +public: + inline static Cardinality computeCardinality(TypeNode type) { + Assert(type.getKind() == kind::BITVECTOR_TYPE); + + unsigned size = type.getConst<BitVectorSize>(); + if(size == 0) { + return 0; + } + Integer i = Integer(2).pow(size); + return i; + } +};/* class CardinalityComputer */ + }/* CVC4::theory::bv namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index e7a559fc6..5e813b125 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -64,10 +64,12 @@ void TheoryDatatypes::checkFiniteWellFounded() { //check well-founded and finite, create distinguished ground terms map<TypeNode, vector<Node> >::iterator it; vector<Node>::iterator itc; + // for each datatype... for( it = d_cons.begin(); it != d_cons.end(); ++it ) { d_distinguishTerms[it->first] = Node::null(); d_finite[it->first] = false; d_wellFounded[it->first] = false; + // for each ctor of that datatype... for( itc = it->second.begin(); itc != it->second.end(); ++itc ) { d_cons_finite[*itc] = false; d_cons_wellFounded[*itc] = false; @@ -76,10 +78,12 @@ void TheoryDatatypes::checkFiniteWellFounded() { bool changed; do{ changed = false; + // for each datatype... for( it = d_cons.begin(); it != d_cons.end(); ++it ) { TypeNode t = it->first; Debug("datatypes-finite") << "Check type " << t << endl; bool typeFinite = true; + // for each ctor of that datatype... for( itc = it->second.begin(); itc != it->second.end(); ++itc ) { Node cn = *itc; TypeNode ct = cn.getType(); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 7b74bfece..36d1b3311 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -152,15 +152,11 @@ public: addDatatypeDefinitions(type); } } - void registerTerm(TNode n) { } - void presolve(); void addSharedTerm(TNode t); void notifyEq(TNode lhs, TNode rhs); void check(Effort e); - void propagate(Effort e) { } - void explain(TNode n, Effort e) { } Node getValue(TNode n); void shutdown() { } std::string identify() const { return std::string("TheoryDatatypes"); } diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter index a53da2022..78fc39984 100755 --- a/src/theory/mkrewriter +++ b/src/theory/mkrewriter @@ -35,16 +35,16 @@ me=$(basename "$0") template=$1; shift -rewriter_includes= +rewriter_includes= rewrite_init= rewrite_shutdown= -pre_rewrite_calls= -pre_rewrite_get_cache= +pre_rewrite_calls= +pre_rewrite_get_cache= pre_rewrite_set_cache= post_rewrite_calls= -post_rewrite_get_cache= +post_rewrite_get_cache= post_rewrite_set_cache= seen_theory=false @@ -55,6 +55,11 @@ function theory { lineno=${BASH_LINENO[0]} + if $seen_theory; then + echo "$kf:$lineno: theory declaration can only appear once" >&2 + exit 1; + fi + # this script doesn't care about the theory class information, but # makes does make sure it's there seen_theory=true @@ -72,8 +77,8 @@ function theory { elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2 fi - - theory_id="$1" + + theory_id="$1" } function properties { @@ -86,32 +91,33 @@ function endtheory { # endtheory lineno=${BASH_LINENO[0]} check_theory_seen + seen_endtheory=true } function rewriter { # rewriter class header - class="$1" + class="$1" header="$2" rewriter_includes="${rewriter_includes}#include \"$header\" " rewrite_init="${rewrite_init} ${class}::init(); " - rewrite_shutdown="${rewrite_shutdown} ${class}::shutdown(); + rewrite_shutdown="${rewrite_shutdown} ${class}::shutdown(); " pre_rewrite_calls="${pre_rewrite_calls} case ${theory_id}: return ${class}::preRewrite(node); " - pre_rewrite_get_cache="${pre_rewrite_get_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::getPreRewriteCache(node); + pre_rewrite_get_cache="${pre_rewrite_get_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::getPreRewriteCache(node); " - pre_rewrite_set_cache="${pre_rewrite_set_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::setPreRewriteCache(node, cache); + pre_rewrite_set_cache="${pre_rewrite_set_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::setPreRewriteCache(node, cache); " post_rewrite_calls="${post_rewrite_calls} case ${theory_id}: return ${class}::postRewrite(node); " - post_rewrite_get_cache="${post_rewrite_get_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::getPostRewriteCache(node); -" - post_rewrite_set_cache="${post_rewrite_set_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::setPostRewriteCache(node, cache); + post_rewrite_get_cache="${post_rewrite_get_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::getPostRewriteCache(node); +" + post_rewrite_set_cache="${post_rewrite_set_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::setPostRewriteCache(node, cache); " lineno=${BASH_LINENO[0]} @@ -119,7 +125,13 @@ function rewriter { } function sort { - # sort TYPE ["comment"] + # sort TYPE cardinality ["comment"] + lineno=${BASH_LINENO[0]} + check_theory_seen +} + +function cardinality { + # cardinality TYPE cardinality-computer [header] lineno=${BASH_LINENO[0]} check_theory_seen } @@ -149,6 +161,10 @@ function constant { } function check_theory_seen { + if $seen_endtheory; then + echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2 + exit 1 + fi if ! $seen_theory; then echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2 exit 1 @@ -164,17 +180,39 @@ function check_builtin_theory_seen { while [ $# -gt 0 ]; do kf=$1 seen_theory=false + seen_endtheory=false b=$(basename $(dirname "$kf")) source "$kf" - check_theory_seen + if ! $seen_theory; then + echo "$kf: error: no theory content found in file!" >&2 + exit 1 + fi + if ! $seen_endtheory; then + echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2 + exit 1 + fi shift done check_builtin_theory_seen ## output +# generate warnings about incorrect #line annotations in templates +nl -ba -s' ' "$template" | grep '^ *[0-9][0-9]* # *line' | + awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2 + text=$(cat "$template") -for var in rewriter_includes pre_rewrite_calls post_rewrite_calls pre_rewrite_get_cache post_rewrite_get_cache pre_rewrite_set_cache post_rewrite_set_cache rewrite_init rewrite_shutdown; do +for var in \ + rewriter_includes \ + pre_rewrite_calls \ + post_rewrite_calls \ + pre_rewrite_get_cache \ + post_rewrite_get_cache \ + pre_rewrite_set_cache \ + post_rewrite_set_cache \ + rewrite_init rewrite_shutdown \ + template \ + ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index c06770a51..9672fc871 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -42,7 +42,9 @@ theory_for_each_macro="#define CVC4_FOR_EACH_THEORY \\ theory_has_check="false" theory_has_propagate="false" -theory_has_static_learning="false" +theory_has_staticLearning="false" +theory_has_registerTerm="false" +theory_has_notifyRestart="false" theory_has_presolve="false" theory_stable_infinite="false" @@ -63,6 +65,11 @@ function theory { lineno=${BASH_LINENO[0]} + if $seen_theory; then + echo "$kf:$lineno: theory declaration can only appear once" >&2 + exit 1; + fi + # this script doesn't care about the theory class information, but # makes does make sure it's there seen_theory=true @@ -84,7 +91,8 @@ function theory { theory_id="$1" theory_class="$2" - theory_includes="${theory_includes}#include \"$3\" + theory_header="$3" + theory_includes="${theory_includes}#include \"$theory_header\" " theory_for_each_macro="${theory_for_each_macro} CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::${theory_id}) \\ " @@ -107,6 +115,8 @@ function endtheory { lineno=${BASH_LINENO[0]} check_theory_seen + seen_endtheory=true + theory_traits="${theory_traits} template<> struct TheoryTraits<${theory_id}> { @@ -119,14 +129,34 @@ struct TheoryTraits<${theory_id}> { static const bool hasCheck = ${theory_has_check}; static const bool hasPropagate = ${theory_has_propagate}; - static const bool hasStaticLearning = ${theory_has_static_learning}; + static const bool hasStaticLearning = ${theory_has_staticLearning}; + static const bool hasRegisterTerm = ${theory_has_registerTerm}; + static const bool hasNotifyRestart = ${theory_has_staticLearning}; static const bool hasPresolve = ${theory_has_presolve}; }; " + # warnings about theory content and properties + dir="$(dirname "$kf")/../../" + if [ -e "$dir/$theory_header" ]; then + for function in check propagate staticLearning registerTerm notifyRestart presolve; do + if eval "\$theory_has_$function"; then + grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' || + echo "$kf: warning: $theory_class has property \"$function\" in its kinds file but doesn't appear to declare the function" >&2 + else + grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' && + echo "$kf: warning: $theory_class does not have property \"$function\" in its kinds file but appears to declare the function" >&2 + fi + done + else + echo "$me: warning: theory header \"$theory_header\" does not exist or is unreadable" >&2 + fi + theory_has_check="false" theory_has_propagate="false" - theory_has_static_learning="false" + theory_has_staticLearning="false" + theory_has_registerTerm="false" + theory_has_notifyRestart="false" theory_has_presolve="false" theory_stable_infinite="false" @@ -156,18 +186,27 @@ function properties { polite) theory_polite="true";; check) theory_has_check="true";; propagate) theory_has_propagate="true";; - staticLearning) theory_has_static_learning="true";; - presolve) theory_has_presolve="true"; + staticLearning) theory_has_staticLearning="true";; + presolve) theory_has_presolve="true";; + registerTerm) theory_has_registerTerm="true";; + notifyRestart) theory_has_notifyRestart="true";; + *) echo "$kf:$lineno: error: unknown theory property \"$property\"" >&2; exit 1;; esac shift done } function sort { - # sort TYPE ["comment"] + # sort TYPE cardinality ["comment"] + lineno=${BASH_LINENO[0]} + check_theory_seen + register_sort "$1" "$2" "$3" +} + +function cardinality { + # cardinality TYPE cardinality-computer [header] lineno=${BASH_LINENO[0]} check_theory_seen - register_sort "$1" "$2" } function variable { @@ -200,7 +239,8 @@ function constant { function register_sort { id=$1 - comment=$2 + cardinality=$2 + comment=$3 type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break; " } @@ -214,6 +254,10 @@ function register_kind { } function check_theory_seen { + if $seen_endtheory; then + echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2 + exit 1 + fi if ! $seen_theory; then echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2 exit 1 @@ -229,23 +273,34 @@ function check_builtin_theory_seen { while [ $# -gt 0 ]; do kf=$1 seen_theory=false + seen_endtheory=false b=$(basename $(dirname "$kf")) - kind_decls="${kind_decls} - /* from $b */ -" - kind_printers="${kind_printers} - /* from $b */ -" source "$kf" - check_theory_seen + if ! $seen_theory; then + echo "$kf: error: no theory content found in file!" >&2 + exit 1 + fi + if ! $seen_endtheory; then + echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2 + exit 1 + fi shift done check_builtin_theory_seen ## output +# generate warnings about incorrect #line annotations in templates +nl -ba -s' ' "$template" | grep '^ *[0-9][0-9]* # *line' | + awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2 + text=$(cat "$template") -for var in theory_traits theory_for_each_macro theory_includes; do +for var in \ + theory_traits \ + theory_for_each_macro \ + theory_includes \ + template \ + ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d37916515..b4d6654b1 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -117,7 +117,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { * twice. */ // FIXME when ExprSets are online, use one of those to avoid // duplicates in the above? - // Actually, that doesn't work because you have to make sure + // Actually, that doesn't work because you have to make sure // that the *last* occurrence is the one that gets processed first @CB // This could be a big performance problem though because it requires // traversing a DAG as a tree and that can really blow up @CB @@ -132,6 +132,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { TheoryEngine::TheoryEngine(context::Context* ctxt) : d_propEngine(NULL), d_context(ctxt), + d_activeTheories(0), d_theoryOut(this, ctxt), d_hasShutDown(false), d_incomplete(ctxt, false), @@ -139,6 +140,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt) : for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { d_theoryTable[theoryId] = NULL; + d_theoryIsActive[theoryId] = false; } Rewriter::init(); @@ -150,7 +152,7 @@ TheoryEngine::~TheoryEngine() { Assert(d_hasShutDown); for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { - if(d_theoryTable[theoryId]) { + if(d_theoryTable[theoryId] != NULL) { delete d_theoryTable[theoryId]; } } @@ -163,7 +165,7 @@ struct preprocess_stack_element { bool children_added; preprocess_stack_element(TNode node) : node(node), children_added(false) {} -}; +};/* struct preprocess_stack_element */ Node TheoryEngine::preprocess(TNode node) { // Make sure the node is type-checked first (some rewrites depend on @@ -198,24 +200,29 @@ void TheoryEngine::preRegister(TNode preprocessed) { if (current.getKind() == kind::EQUAL) { TheoryId theoryLHS = Theory::theoryOf(current[0]); Debug("register") << "preregistering " << current << " with " << theoryLHS << std::endl; + markActive(theoryLHS); d_theoryTable[theoryLHS]->preRegisterTerm(current); // TheoryId theoryRHS = Theory::theoryOf(current[1]); // if (theoryLHS != theoryRHS) { +// markActive(theoryRHS); // d_theoryTable[theoryRHS]->preRegisterTerm(current); // Debug("register") << "preregistering " << current << " with " << theoryRHS << std::endl; // } // TheoryId typeTheory = Theory::theoryOf(current[0].getType()); // if (typeTheory != theoryLHS && typeTheory != theoryRHS) { +// markActive(typeTheory); // d_theoryTable[typeTheory]->preRegisterTerm(current); // Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl; // } } else { TheoryId theory = Theory::theoryOf(current); Debug("register") << "preregistering " << current << " with " << theory << std::endl; + markActive(theory); d_theoryTable[theory]->preRegisterTerm(current); TheoryId typeTheory = Theory::theoryOf(current.getType()); if (theory != typeTheory) { Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl; + markActive(typeTheory); d_theoryTable[typeTheory]->preRegisterTerm(current); } } @@ -248,7 +255,7 @@ bool TheoryEngine::check(theory::Theory::Effort effort) { #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasCheck) { \ + if (theory::TheoryTraits<THEORY>::hasCheck && d_theoryIsActive[THEORY]) { \ reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->check(effort); \ if (!d_theoryOut.d_conflictNode.get().isNull()) { \ return false; \ @@ -271,7 +278,7 @@ void TheoryEngine::propagate() { #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasPropagate) { \ + if (theory::TheoryTraits<THEORY>::hasPropagate && d_theoryIsActive[THEORY]) { \ reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \ } @@ -359,13 +366,22 @@ Node TheoryEngine::getValue(TNode node) { bool TheoryEngine::presolve() { d_theoryOut.d_conflictNode = Node::null(); d_theoryOut.d_propagatedLiterals.clear(); + try { - for(unsigned i = 0; i < THEORY_LAST; ++ i) { - d_theoryTable[i]->presolve(); - if(!d_theoryOut.d_conflictNode.get().isNull()) { - return true; - } - } + // Definition of the statement that is to be run by every theory +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasPresolve && d_theoryIsActive[THEORY]) { \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->presolve(); \ + if(!d_theoryOut.d_conflictNode.get().isNull()) { \ + return true; \ + } \ + } + + // Presolve for each theory using the statement above + CVC4_FOR_EACH_THEORY } catch(const theory::Interrupted&) { Debug("theory") << "TheoryEngine::presolve() => interrupted" << endl; } @@ -375,20 +391,37 @@ bool TheoryEngine::presolve() { void TheoryEngine::notifyRestart() { - for(unsigned i = 0; i < THEORY_LAST; ++ i) { - if (d_theoryTable[i]) { - d_theoryTable[i]->notifyRestart(); - } + // Definition of the statement that is to be run by every theory +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_theoryIsActive[THEORY]) { \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->notifyRestart(); \ } -} + // notify each theory using the statement above + CVC4_FOR_EACH_THEORY +} void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) { - for(unsigned i = 0; i < THEORY_LAST; ++ i) { - if (d_theoryTable[i]) { - d_theoryTable[i]->staticLearning(in, learned); - } + // NOTE that we don't look at d_theoryIsActive[] here. First of + // all, we haven't done any pre-registration yet, so we don't know + // which theories are active. Second, let's give each theory a shot + // at doing something with the input formula, even if it wouldn't + // otherwise be active. + + // Definition of the statement that is to be run by every theory +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasStaticLearning) { \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->staticLearning(in, learned); \ } + + // notify each theory using the statement above + CVC4_FOR_EACH_THEORY } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 85f26f012..19374d6db 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief The theory engine. + ** \brief The theory engine ** ** The theory engine. **/ @@ -51,10 +51,24 @@ class TheoryEngine { /** Our context */ context::Context* d_context; - /** A table of from theory ifs to theory pointers */ + /** A table of from theory IDs to theory pointers */ theory::Theory* d_theoryTable[theory::THEORY_LAST]; /** + * A bitmap of theories that are "active" for the current run. We + * mark a theory active when we firt see a term or type belonging to + * it. This is important because we can optimize for single-theory + * runs (no sharing), can reduce the cost of walking the DAG on + * registration, etc. + */ + bool d_theoryIsActive[theory::THEORY_LAST]; + + /** + * The count of active theories in the d_theoryIsActive bitmap. + */ + size_t d_activeTheories; + + /** * An output channel for Theory that passes messages * back to a TheoryEngine. */ @@ -159,6 +173,17 @@ class TheoryEngine { */ Node removeITEs(TNode t); + /** + * Mark a theory active if it's not already. + */ + void markActive(theory::TheoryId th) { + if(!d_theoryIsActive[th]) { + d_theoryIsActive[th] = true; + ++d_activeTheories; + Notice() << "Theory " << th << " has been activated." << std::endl; + } + } + public: /** @@ -249,7 +274,7 @@ public: /** * Preprocess a node. This involves theory-specific rewriting, then - * calling preRegisterTerm() on what's left over. + * calling preRegister() on what's left over. * @param n the node to preprocess */ Node preprocess(TNode n); diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 8c34370d7..0b377fb11 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -11,17 +11,13 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] + ** \brief Common utilities for testing theories ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** Common utilities for testing theories. **/ - - #include "cvc4_public.h" - #ifndef __CVC4__THEORY__THEORY_TEST_UTILS_H #define __CVC4__THEORY__ITHEORY_TEST_UTILS_H @@ -48,7 +44,7 @@ enum OutputChannelCallType { AUG_LEMMA, LEMMA, EXPLANATION -}; +};/* enum OutputChannelCallType */ }/* CVC4::theory namespace */ @@ -121,9 +117,11 @@ public: } private: + void push(OutputChannelCallType call, TNode n) { - d_callHistory.push_back(std::make_pair(call,n)); + d_callHistory.push_back(std::make_pair(call, n)); } + };/* class TestOutputChannel */ }/* CVC4::theory namespace */ diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h index c6541dbea..525c06b3c 100644 --- a/src/theory/theory_traits_template.h +++ b/src/theory/theory_traits_template.h @@ -11,10 +11,12 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] + ** \brief A template for the theory_traits.h header, defining various + ** (static) aspects of theories ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** This file is a template for the theory_traits.h header, defining + ** various (static) aspects of theories, combined with the theory + ** kinds files to produce the final header. **/ #pragma once diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index a1fcac1df..d7f542038 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -6,15 +6,22 @@ theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h" -properties stable-infinite check propagate staticLearning presolve +properties stable-infinite +properties check propagate staticLearning presolve notifyRestart rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" -sort KIND_TYPE "Uninterpreted Sort" +# Justified because we can have an unbounded-but-finite number of +# sorts. Assuming we have |Z| is probably ok for now.. +sort KIND_TYPE Cardinality::INTEGERS "Uninterpreted Sort" parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" variable SORT_TAG "sort tag" parameterized SORT_TYPE SORT_TAG 0: "sort type" +# This is really "unknown" cardinality, but maybe this will be good +# enough (for now) ? Once we support quantifiers, maybe reconsider +# this.. +cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)" -endtheory
\ No newline at end of file +endtheory diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 9746b38ab..34d6df881 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -40,6 +40,15 @@ public: TheoryUF(context::Context* ctxt, OutputChannel& out, Valuation valuation) : Theory(THEORY_UF, ctxt, out, valuation) { } + // We declare these here (even though it's not terribly useful) for + // documentation reasons, and to keep mktheorytraits from issuing a + // spurious warning. + virtual void check(Effort) = 0; + virtual void propagate(Effort) {} + virtual void staticLearning(TNode in, NodeBuilder<>& learned) {} + virtual void notifyRestart() {} + virtual void presolve() {} + };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ diff --git a/src/util/Assert.h b/src/util/Assert.h index 0ff89bedf..e38a3f9cf 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -221,6 +221,16 @@ public: va_end(args); } + InternalErrorException(const char* function, const char* file, unsigned line, + std::string fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Internal error detected", "", + function, file, line, fmt.c_str(), args); + va_end(args); + } + };/* class InternalErrorException */ #ifdef CVC4_DEBUG diff --git a/src/util/Makefile.am b/src/util/Makefile.am index e76858d80..a6ff0ea40 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -45,8 +45,11 @@ libutil_la_SOURCES = \ stats.cpp \ dynamic_array.h \ language.h \ + language.cpp \ triple.h \ subrange_bound.h \ + cardinality.h \ + cardinality.cpp \ trans_closure.h \ trans_closure.cpp \ boolean_simplification.h \ diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp new file mode 100644 index 000000000..d38be1c92 --- /dev/null +++ b/src/util/cardinality.cpp @@ -0,0 +1,126 @@ +/********************* */ +/*! \file cardinality.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of cardinality + ** + ** Implementation of a simple class to represent a cardinality. + **/ + +#include "util/cardinality.h" + +namespace CVC4 { + +const Integer Cardinality::s_intCard(-1); +const Integer Cardinality::s_realCard(-2); + +const Cardinality Cardinality::INTEGERS(Cardinality::Beth(0)); +const Cardinality Cardinality::REALS(Cardinality::Beth(1)); + +Cardinality& Cardinality::operator+=(const Cardinality& c) throw() { + if(isFinite() && c.isFinite()) { + d_card += c.d_card; + return *this; + } + if(*this >= c) { + return *this; + } else { + return *this = c; + } +} + +/** Assigning multiplication of this cardinality with another. */ +Cardinality& Cardinality::operator*=(const Cardinality& c) throw() { + if(*this == 0 || c == 0) { + return *this = 0; + } else if(!isFinite() || !c.isFinite()) { + if(*this >= c) { + return *this; + } else { + return *this = c; + } + } else { + d_card *= c.d_card; + return *this; + } +} + +/** Assigning exponentiation of this cardinality with another. */ +Cardinality& Cardinality::operator^=(const Cardinality& c) + throw(IllegalArgumentException) { + if(c == 0) { + // (anything) ^ 0 == 1 + d_card = 1; + return *this; + } else if(*this == 0) { + // 0 ^ (>= 1) == 0 + return *this; + } else if(*this == 1) { + // 1 ^ (>= 1) == 1 + return *this; + } else if(c == 1) { + // (anything) ^ 1 == (that thing) + return *this; + } else if(isFinite() && c.isFinite()) { + // finite ^ finite == finite + // + // Note: can throw an assertion if c is too big for + // exponentiation + d_card = d_card.pow(c.d_card.getUnsignedLong()); + return *this; + } else if(!isFinite() && c.isFinite()) { + // inf ^ finite == inf + return *this; + } else { + Assert(*this >= 2 && !c.isFinite(), + "fall-through case not as expected:\n%s\n%s", + this->toString().c_str(), c.toString().c_str()); + // (>= 2) ^ beth_k == beth_(k+1) + // unless the base is already > the exponent + if(*this > c) { + return *this; + } + d_card = c.d_card - 1; + return *this; + } +} + + +std::string Cardinality::toString() const throw() { + std::stringstream ss; + ss << *this; + return ss.str(); +} + + +std::ostream& operator<<(std::ostream& out, + Cardinality::Beth b) + throw() { + out << "beth[" << b.getNumber() << ']'; + + return out; +} + + +std::ostream& operator<<(std::ostream& out, const Cardinality& c) + throw() { + if(c.isFinite()) { + out << c.getFiniteCardinality(); + } else { + out << Cardinality::Beth(c.getBethNumber()); + } + + return out; +} + + +}/* CVC4 namespace */ diff --git a/src/util/cardinality.h b/src/util/cardinality.h new file mode 100644 index 000000000..c520c2735 --- /dev/null +++ b/src/util/cardinality.h @@ -0,0 +1,234 @@ +/********************* */ +/*! \file cardinality.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of cardinality + ** + ** Simple class to represent a cardinality; used by the CVC4 type system + ** give the cardinality of sorts. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__CARDINALITY_H +#define __CVC4__CARDINALITY_H + +#include <iostream> +#include <utility> + +#include "util/integer.h" +#include "util/Assert.h" + +namespace CVC4 { + +/** + * A simple representation of a cardinality. We store an + * arbitrary-precision integer for finite cardinalities, and we + * distinguish infinite cardinalities represented as Beth numbers. + */ +class CVC4_PUBLIC Cardinality { + /** Cardinality of the integers */ + static const Integer s_intCard; + + /** Cardinality of the reals */ + static const Integer s_realCard; + + /** + * In the case of finite cardinality, this is >= 0, and is equal to + * the cardinality. If infinite, it is < 0, and is Beth[|card|-1]. + * That is, "-1" means Beth 0 == |Z|, "-2" means Beth 1 == |R|, etc. + */ + Integer d_card; + +public: + + /** The cardinality of the set of integers. */ + static const Cardinality INTEGERS; + + /** The cardinality of the set of real numbers. */ + static const Cardinality REALS; + + /** + * Representation for a Beth number, used only to construct + * Cardinality objects. + */ + class Beth { + Integer d_index; + + public: + Beth(const Integer& beth) : d_index(beth) { + CheckArgument(beth >= 0, beth, + "Beth index must be a nonnegative integer, not %s.", + beth.toString().c_str()); + } + + const Integer& getNumber() const throw() { + return d_index; + } + };/* class Cardinality::Beth */ + + /** + * Construct a finite cardinality equal to the integer argument. + * The argument must be nonnegative. If we change this to an + * "unsigned" argument to enforce the restriction, we mask some + * errors that automatically convert, like "Cardinality(-1)". + */ + Cardinality(long card) : d_card(card) { + CheckArgument(card >= 0, card, + "Cardinality must be a nonnegative integer, not %ld.", card); + Assert(isFinite()); + } + + /** + * Construct a finite cardinality equal to the integer argument. + * The argument must be nonnegative. + */ + Cardinality(const Integer& card) : d_card(card) { + CheckArgument(card >= 0, card, + "Cardinality must be a nonnegative integer, not %s.", + card.toString().c_str()); + Assert(isFinite()); + } + + /** + * Construct an infinite cardinality equal to the given Beth number. + */ + Cardinality(Beth beth) : d_card(-beth.getNumber() - 1) { + Assert(!isFinite()); + } + + /** Returns true iff this cardinality is finite. */ + bool isFinite() const throw() { + return d_card >= 0; + } + + /** + * Returns true iff this cardinality is finite or countably + * infinite. + */ + bool isCountable() const throw() { + return d_card >= s_intCard; + } + + /** + * In the case that this cardinality is finite, return its + * cardinality. (If this cardinality is infinite, this function + * throws an IllegalArgumentException.) + */ + const Integer& getFiniteCardinality() const throw(IllegalArgumentException) { + CheckArgument(isFinite(), *this, "This cardinality is not finite."); + return d_card; + } + + /** + * In the case that this cardinality is infinite, return its Beth + * number. (If this cardinality is finite, this function throws an + * IllegalArgumentException.) + */ + Integer getBethNumber() const throw(IllegalArgumentException) { + CheckArgument(!isFinite(), *this, "This cardinality is not infinite."); + return -d_card - 1; + } + + /** Assigning addition of this cardinality with another. */ + Cardinality& operator+=(const Cardinality& c) throw(); + + /** Assigning multiplication of this cardinality with another. */ + Cardinality& operator*=(const Cardinality& c) throw(); + + /** Assigning exponentiation of this cardinality with another. */ + Cardinality& operator^=(const Cardinality& c) throw(IllegalArgumentException); + + /** Add two cardinalities. */ + Cardinality operator+(const Cardinality& c) const throw() { + Cardinality card(*this); + card += c; + return card; + } + + /** Multiply two cardinalities. */ + Cardinality operator*(const Cardinality& c) const throw() { + Cardinality card(*this); + card *= c; + return card; + } + + /** + * Exponentiation of two cardinalities. Throws an exception if both + * are finite and the exponent is too large. + */ + Cardinality operator^(const Cardinality& c) const throw(IllegalArgumentException) { + Cardinality card(*this); + card ^= c; + return card; + } + + /** Test for equality between cardinalities. */ + bool operator==(const Cardinality& c) const throw() { + return d_card == c.d_card; + } + + /** Test for disequality between cardinalities. */ + bool operator!=(const Cardinality& c) const throw() { + return !(*this == c); + } + + /** Test whether this cardinality is less than another. */ + bool operator<(const Cardinality& c) const throw() { + return + ( isFinite() && !c.isFinite() ) || + ( isFinite() && c.isFinite() && d_card < c.d_card ) || + ( !isFinite() && !c.isFinite() && d_card > c.d_card ); + } + + /** + * Test whether this cardinality is less than or equal to + * another. + */ + bool operator<=(const Cardinality& c) const throw() { + return *this < c || *this == c; + } + + /** Test whether this cardinality is greater than another. */ + bool operator>(const Cardinality& c) const throw() { + return !(*this <= c); + } + + /** + * Test whether this cardinality is greater than or equal to + * another. + */ + bool operator>=(const Cardinality& c) const throw() { + return !(*this < c); + } + + /** + * Return a string representation of this cardinality. + */ + std::string toString() const throw(); + +};/* class Cardinality */ + + +/** Print an element of the InfiniteCardinality enumeration. */ +std::ostream& operator<<(std::ostream& out, Cardinality::Beth b) + throw() CVC4_PUBLIC; + + +/** Print a cardinality in a human-readable fashion. */ +std::ostream& operator<<(std::ostream& out, const Cardinality& c) + throw() CVC4_PUBLIC; + + +}/* CVC4 namespace */ + +#endif /* __CVC4__CARDINALITY_H */ diff --git a/src/util/datatype.h b/src/util/datatype.h index 26e58264a..74bff1843 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -150,6 +150,7 @@ public: /** Get the name of this constructor argument. */ std::string getName() const throw(); + /** * Get the selector for this constructor argument; this call is * only permitted after resolution. @@ -203,12 +204,14 @@ public: * to this Datatype constructor. */ void addArg(std::string selectorName, Type selectorType); + /** * Add an argument (i.e., a data field) of the given name to this * Datatype constructor that refers to an as-yet-unresolved * Datatype (which may be mutually-recursive). */ void addArg(std::string selectorName, Datatype::UnresolvedType selectorType); + /** * Add a self-referential (i.e., a data field) of the given name * to this Datatype constructor that refers to the enclosing diff --git a/src/util/debug.h b/src/util/debug.h index 4fc5d5caa..402c5bed4 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -20,6 +20,8 @@ ** util/Assert.h. **/ +#include "cvc4_private.h" + #ifndef __CVC4__DEBUG_H #define __CVC4__DEBUG_H diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index d13c946de..8c3fc14e5 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -142,25 +142,45 @@ public: } - Integer operator+(const Integer& y) const{ + Integer operator+(const Integer& y) const { return Integer( d_value + y.d_value ); } + Integer& operator+=(const Integer& y) { + d_value += y.d_value; + return *this; + } Integer operator-(const Integer& y) const { return Integer( d_value - y.d_value ); } + Integer& operator-=(const Integer& y) { + d_value -= y.d_value; + return *this; + } Integer operator*(const Integer& y) const { return Integer( d_value * y.d_value ); } + Integer& operator*=(const Integer& y) { + d_value *= y.d_value; + return *this; + } Integer operator/(const Integer& y) const { return Integer( cln::floor1(d_value, y.d_value) ); } + Integer& operator/=(const Integer& y) { + d_value = cln::floor1(d_value, y.d_value); + return *this; + } Integer operator%(const Integer& y) const { return Integer( cln::floor2(d_value, y.d_value).remainder ); } + Integer& operator%=(const Integer& y) { + d_value = cln::floor2(d_value, y.d_value).remainder; + return *this; + } /** Raise this Integer to the power <code>exp</code>. * @@ -208,8 +228,15 @@ public: //friend std::ostream& operator<<(std::ostream& os, const Integer& n); - long getLong() const { return cln::cl_I_to_long(d_value); } - unsigned long getUnsignedLong() const {return cln::cl_I_to_ulong(d_value); } + long getLong() const { + // supposed to throw if not representable in type "long" + return cln::cl_I_to_long(d_value); + } + + unsigned long getUnsignedLong() const { + // supposed to throw if not representable in type "unsigned long" + return cln::cl_I_to_ulong(d_value); + } /** * Computes the hash of the node from the first word of the diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 13bed50b3..c1d46ca65 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -25,6 +25,7 @@ #include <string> #include <iostream> +#include "util/Assert.h" #include "util/gmp_util.h" namespace CVC4 { @@ -84,7 +85,7 @@ public: return d_value == y.d_value; } - Integer operator-() const{ + Integer operator-() const { return Integer(-(d_value)); } @@ -110,23 +111,45 @@ public: } - Integer operator+(const Integer& y) const{ + Integer operator+(const Integer& y) const { return Integer( d_value + y.d_value ); } + Integer& operator+=(const Integer& y) { + d_value += y.d_value; + return *this; + } Integer operator-(const Integer& y) const { return Integer( d_value - y.d_value ); } + Integer& operator-=(const Integer& y) { + d_value -= y.d_value; + return *this; + } Integer operator*(const Integer& y) const { return Integer( d_value * y.d_value ); } + Integer& operator*=(const Integer& y) { + d_value *= y.d_value; + return *this; + } + Integer operator/(const Integer& y) const { return Integer( d_value / y.d_value ); } + Integer& operator/=(const Integer& y) { + d_value /= y.d_value; + return *this; + } + Integer operator%(const Integer& y) const { return Integer( d_value % y.d_value ); } + Integer& operator%=(const Integer& y) { + d_value %= y.d_value; + return *this; + } /** Raise this Integer to the power <code>exp</code>. * @@ -144,8 +167,22 @@ public: //friend std::ostream& operator<<(std::ostream& os, const Integer& n); - long getLong() const { return d_value.get_si(); } - unsigned long getUnsignedLong() const {return d_value.get_ui(); } + long getLong() const { + long si = d_value.get_si(); +#ifdef CVC4_ASSERTIONS + // ensure there wasn't overflow + Assert(mpz_cmp_si(d_value.get_mpz_t(), si) == 0); +#endif /* CVC4_ASSERTIONS */ + return si; + } + unsigned long getUnsignedLong() const { + unsigned long ui = d_value.get_ui(); +#ifdef CVC4_ASSERTIONS + // ensure there wasn't overflow + Assert(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0); +#endif /* CVC4_ASSERTIONS */ + return ui; + } /** * Computes the hash of the node from the first word of the diff --git a/src/util/language.cpp b/src/util/language.cpp new file mode 100644 index 000000000..da54a4783 --- /dev/null +++ b/src/util/language.cpp @@ -0,0 +1,65 @@ +/********************* */ +/*! \file language.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Definition of input and output languages + ** + ** Definition of input and output languages. + **/ + +#include "util/language.h" + +namespace CVC4 { +namespace language { + +InputLanguage toInputLanguage(OutputLanguage language) { + switch(language) { + case output::LANG_SMTLIB: + case output::LANG_SMTLIB_V2: + case output::LANG_CVC4: + // these entries directly correspond (by design) + return InputLanguage(int(language)); + + default: { + std::stringstream ss; + ss << "Cannot map output language `" << language + << "' to an input language."; + throw CVC4::Exception(ss.str()); + } + }/* switch(language) */ +}/* toInputLanguage() */ + +OutputLanguage toOutputLanguage(InputLanguage language) { + switch(language) { + case input::LANG_SMTLIB: + case input::LANG_SMTLIB_V2: + case input::LANG_CVC4: + // these entries directly correspond (by design) + return OutputLanguage(int(language)); + + default: + // Revert to the default (AST) language. + // + // We used to throw an exception here, but that's not quite right. + // We often call this while constructing exceptions, for one, and + // it's better to output SOMETHING related to the original + // exception rather than mask it with another exception. Also, + // the input language isn't always defined---e.g. during the + // initial phase of the main CVC4 driver while it determines which + // language is appropriate, and during unit tests. Also, when + // users are writing their own code against the library. + return output::LANG_AST; + }/* switch(language) */ +}/* toOutputLanguage() */ + +}/* CVC4::language namespace */ +}/* CVC4 namespace */ diff --git a/src/util/language.h b/src/util/language.h index 814f8dcd1..dbda6a315 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -31,7 +31,7 @@ namespace language { namespace input { -enum Language { +enum CVC4_PUBLIC Language { // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 /** Auto-detect the language */ @@ -58,6 +58,7 @@ enum Language { LANG_MAX };/* enum Language */ +inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC; inline std::ostream& operator<<(std::ostream& out, Language lang) { switch(lang) { case LANG_AUTO: @@ -82,7 +83,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { namespace output { -enum Language { +enum CVC4_PUBLIC Language { // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9] @@ -109,6 +110,7 @@ enum Language { LANG_MAX };/* enum Language */ +inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC; inline std::ostream& operator<<(std::ostream& out, Language lang) { switch(lang) { case LANG_SMTLIB: @@ -138,39 +140,8 @@ typedef language::output::Language OutputLanguage; namespace language { -inline InputLanguage toInputLanguage(OutputLanguage language) { - switch(language) { - case output::LANG_SMTLIB: - case output::LANG_SMTLIB_V2: - case output::LANG_CVC4: - // these entries directly correspond (by design) - return InputLanguage(int(language)); - - default: { - std::stringstream ss; - ss << "Cannot map output language `" << language - << "' to an input language."; - throw CVC4::Exception(ss.str()); - } - }/* switch(language) */ -}/* toInputLanguage() */ - -inline OutputLanguage toOutputLanguage(InputLanguage language) { - switch(language) { - case input::LANG_SMTLIB: - case input::LANG_SMTLIB_V2: - case input::LANG_CVC4: - // these entries directly correspond (by design) - return OutputLanguage(int(language)); - - default: { - std::stringstream ss; - ss << "Cannot map input language `" << language - << "' to an output language."; - throw CVC4::Exception(ss.str()); - } - }/* switch(language) */ -}/* toOutputLanguage() */ +InputLanguage toInputLanguage(OutputLanguage language) CVC4_PUBLIC; +OutputLanguage toOutputLanguage(InputLanguage language) CVC4_PUBLIC; }/* CVC4::language namespace */ }/* CVC4 namespace */ diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h index fc6a259b4..0c84b214e 100644 --- a/src/util/subrange_bound.h +++ b/src/util/subrange_bound.h @@ -33,7 +33,7 @@ namespace CVC4 { * an infinite bound). For example, the CVC language subrange [-5.._] * has a lower bound of -5 and an infinite upper bound. */ -class SubrangeBound { +class CVC4_PUBLIC SubrangeBound { bool d_nobound; Integer d_bound; @@ -79,6 +79,9 @@ public: };/* class SubrangeBound */ inline std::ostream& +operator<<(std::ostream& out, const SubrangeBound& bound) throw() CVC4_PUBLIC; + +inline std::ostream& operator<<(std::ostream& out, const SubrangeBound& bound) throw() { if(bound.hasBound()) { out << bound.getBound(); diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 13d28f3bb..f50cc32db 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -19,6 +19,7 @@ UNIT_TESTS = \ expr/attribute_black \ expr/declaration_scope_black \ expr/node_self_iterator_black \ + expr/type_cardinality_public \ parser/parser_black \ parser/parser_builder_black \ prop/cnf_stream_black \ @@ -46,6 +47,7 @@ UNIT_TESTS = \ util/trans_closure_black \ util/boolean_simplification_black \ util/subrange_bound_white \ + util/cardinality_public \ main/interactive_shell_black export VERBOSE = 1 diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h new file mode 100644 index 000000000..381d5fdea --- /dev/null +++ b/test/unit/expr/type_cardinality_public.h @@ -0,0 +1,223 @@ +/********************* */ +/*! \file type_cardinality_public.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Public box testing of Type::getCardinality() for various Types + ** + ** Public box testing of Type::getCardinality() for various Types. + **/ + +#include <cxxtest/TestSuite.h> + +#include <iostream> +#include <string> +#include <sstream> + +#include "expr/kind.h" +#include "expr/type.h" +#include "expr/expr_manager.h" +#include "util/cardinality.h" +#include "util/Assert.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace std; + +class TypeCardinalityPublic : public CxxTest::TestSuite { + ExprManager* d_em; + +public: + + void setUp() { + d_em = new ExprManager(); + } + + void tearDown() { + delete d_em; + } + + void testTheBasics() { + TS_ASSERT( d_em->booleanType().getCardinality() == 2 ); + TS_ASSERT( d_em->integerType().getCardinality() == Cardinality::INTEGERS ); + TS_ASSERT( d_em->realType().getCardinality() == Cardinality::REALS ); + } + + void testArrays() { + Type intToInt = d_em->mkArrayType(d_em->integerType(), d_em->integerType()); + Type realToReal = d_em->mkArrayType(d_em->realType(), d_em->realType()); + Type realToInt = d_em->mkArrayType(d_em->realType(), d_em->integerType()); + Type intToReal = d_em->mkArrayType(d_em->integerType(), d_em->realType()); + Type intToBool = d_em->mkArrayType(d_em->integerType(), d_em->booleanType()); + Type realToBool = d_em->mkArrayType(d_em->realType(), d_em->booleanType()); + Type boolToReal = d_em->mkArrayType(d_em->booleanType(), d_em->realType()); + Type boolToInt = d_em->mkArrayType(d_em->booleanType(), d_em->integerType()); + Type boolToBool = d_em->mkArrayType(d_em->booleanType(), d_em->booleanType()); + + TS_ASSERT( intToInt.getCardinality() == Cardinality::REALS ); + TS_ASSERT( realToReal.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realToInt.getCardinality() > Cardinality::REALS ); + TS_ASSERT( intToReal.getCardinality() == Cardinality::REALS ); + TS_ASSERT( intToBool.getCardinality() == Cardinality::REALS ); + TS_ASSERT( realToBool.getCardinality() > Cardinality::REALS ); + TS_ASSERT( boolToReal.getCardinality() == Cardinality::REALS ); + TS_ASSERT( boolToInt.getCardinality() == Cardinality::INTEGERS ); + TS_ASSERT( boolToBool.getCardinality() == 4 ); + } + + void testUnaryFunctions() { + Type intToInt = d_em->mkFunctionType(d_em->integerType(), d_em->integerType()); + Type realToReal = d_em->mkFunctionType(d_em->realType(), d_em->realType()); + Type realToInt = d_em->mkFunctionType(d_em->realType(), d_em->integerType()); + Type intToReal = d_em->mkFunctionType(d_em->integerType(), d_em->realType()); + Type intToBool = d_em->mkFunctionType(d_em->integerType(), d_em->booleanType()); + Type realToBool = d_em->mkFunctionType(d_em->realType(), d_em->booleanType()); + Type boolToReal = d_em->mkFunctionType(d_em->booleanType(), d_em->realType()); + Type boolToInt = d_em->mkFunctionType(d_em->booleanType(), d_em->integerType()); + Type boolToBool = d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType()); + + TS_ASSERT( intToInt.getCardinality() == Cardinality::REALS ); + TS_ASSERT( realToReal.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realToInt.getCardinality() > Cardinality::REALS ); + TS_ASSERT( intToReal.getCardinality() == Cardinality::REALS ); + TS_ASSERT( intToBool.getCardinality() == Cardinality::REALS ); + TS_ASSERT( realToBool.getCardinality() > Cardinality::REALS ); + TS_ASSERT( boolToReal.getCardinality() == Cardinality::REALS ); + TS_ASSERT( boolToInt.getCardinality() == Cardinality::INTEGERS ); + TS_ASSERT( boolToBool.getCardinality() == 4 ); + } + + void testBinaryFunctions() { + vector<Type> boolbool; boolbool.push_back(d_em->booleanType()); boolbool.push_back(d_em->booleanType()); + vector<Type> boolint; boolint.push_back(d_em->booleanType()); boolint.push_back(d_em->integerType()); + vector<Type> intbool; intbool.push_back(d_em->integerType()); intbool.push_back(d_em->booleanType()); + vector<Type> intint; intint.push_back(d_em->integerType()); intint.push_back(d_em->integerType()); + vector<Type> intreal; intreal.push_back(d_em->integerType()); intreal.push_back(d_em->realType()); + vector<Type> realint; realint.push_back(d_em->realType()); realint.push_back(d_em->integerType()); + vector<Type> realreal; realreal.push_back(d_em->realType()); realreal.push_back(d_em->realType()); + vector<Type> realbool; realbool.push_back(d_em->realType()); realbool.push_back(d_em->booleanType()); + vector<Type> boolreal; boolreal.push_back(d_em->booleanType()); boolreal.push_back(d_em->realType()); + + Type boolboolToBool = d_em->mkFunctionType(boolbool, d_em->booleanType()); + Type boolboolToInt = d_em->mkFunctionType(boolbool, d_em->integerType()); + Type boolboolToReal = d_em->mkFunctionType(boolbool, d_em->realType()); + + Type boolintToBool = d_em->mkFunctionType(boolint, d_em->booleanType()); + Type boolintToInt = d_em->mkFunctionType(boolint, d_em->integerType()); + Type boolintToReal = d_em->mkFunctionType(boolint, d_em->realType()); + + Type intboolToBool = d_em->mkFunctionType(intbool, d_em->booleanType()); + Type intboolToInt = d_em->mkFunctionType(intbool, d_em->integerType()); + Type intboolToReal = d_em->mkFunctionType(intbool, d_em->realType()); + + Type intintToBool = d_em->mkFunctionType(intint, d_em->booleanType()); + Type intintToInt = d_em->mkFunctionType(intint, d_em->integerType()); + Type intintToReal = d_em->mkFunctionType(intint, d_em->realType()); + + Type intrealToBool = d_em->mkFunctionType(intreal, d_em->booleanType()); + Type intrealToInt = d_em->mkFunctionType(intreal, d_em->integerType()); + Type intrealToReal = d_em->mkFunctionType(intreal, d_em->realType()); + + Type realintToBool = d_em->mkFunctionType(realint, d_em->booleanType()); + Type realintToInt = d_em->mkFunctionType(realint, d_em->integerType()); + Type realintToReal = d_em->mkFunctionType(realint, d_em->realType()); + + Type realrealToBool = d_em->mkFunctionType(realreal, d_em->booleanType()); + Type realrealToInt = d_em->mkFunctionType(realreal, d_em->integerType()); + Type realrealToReal = d_em->mkFunctionType(realreal, d_em->realType()); + + Type realboolToBool = d_em->mkFunctionType(realbool, d_em->booleanType()); + Type realboolToInt = d_em->mkFunctionType(realbool, d_em->integerType()); + Type realboolToReal = d_em->mkFunctionType(realbool, d_em->realType()); + + Type boolrealToBool = d_em->mkFunctionType(boolreal, d_em->booleanType()); + Type boolrealToInt = d_em->mkFunctionType(boolreal, d_em->integerType()); + Type boolrealToReal = d_em->mkFunctionType(boolreal, d_em->realType()); + + TS_ASSERT( boolboolToBool.getCardinality() == 16 ); + TS_ASSERT( boolboolToInt.getCardinality() == Cardinality::INTEGERS ); + TS_ASSERT( boolboolToReal.getCardinality() == Cardinality::REALS ); + + TS_ASSERT( boolintToBool.getCardinality() == Cardinality::REALS ); + TS_ASSERT( boolintToInt.getCardinality() == Cardinality::REALS ); + TS_ASSERT( boolintToReal.getCardinality() == Cardinality::REALS ); + + TS_ASSERT( intboolToBool.getCardinality() == Cardinality::REALS ); + TS_ASSERT( intboolToInt.getCardinality() == Cardinality::REALS ); + TS_ASSERT( intboolToReal.getCardinality() == Cardinality::REALS ); + + TS_ASSERT( intintToBool.getCardinality() == Cardinality::REALS ); + TS_ASSERT( intintToInt.getCardinality() == Cardinality::REALS ); + TS_ASSERT( intintToReal.getCardinality() == Cardinality::REALS ); + + TS_ASSERT( intrealToBool.getCardinality() > Cardinality::REALS ); + TS_ASSERT( intrealToInt.getCardinality() > Cardinality::REALS ); + TS_ASSERT( intrealToReal.getCardinality() > Cardinality::REALS ); + + TS_ASSERT( realintToBool.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realintToInt.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realintToReal.getCardinality() > Cardinality::REALS ); + + TS_ASSERT( realrealToBool.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realrealToInt.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realrealToReal.getCardinality() > Cardinality::REALS ); + + TS_ASSERT( realboolToBool.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realboolToInt.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realboolToReal.getCardinality() > Cardinality::REALS ); + + TS_ASSERT( boolrealToBool.getCardinality() > Cardinality::REALS ); + TS_ASSERT( boolrealToInt.getCardinality() > Cardinality::REALS ); + TS_ASSERT( boolrealToReal.getCardinality() > Cardinality::REALS ); + } + + void testTernaryFunctions() { + vector<Type> boolbool; boolbool.push_back(d_em->booleanType()); boolbool.push_back(d_em->booleanType()); + vector<Type> boolboolbool = boolbool; boolboolbool.push_back(d_em->booleanType()); + + Type boolboolTuple = d_em->mkTupleType(boolbool); + Type boolboolboolTuple = d_em->mkTupleType(boolboolbool); + + Type boolboolboolToBool = d_em->mkFunctionType(boolboolbool, d_em->booleanType()); + Type boolboolToBoolbool = d_em->mkFunctionType(boolbool, boolboolTuple); + Type boolToBoolboolbool = d_em->mkFunctionType(d_em->booleanType(), boolboolboolTuple); + + TS_ASSERT( boolboolboolToBool.getCardinality() == /* 2 ^ 8 */ 1 << 8 ); + TS_ASSERT( boolboolToBoolbool.getCardinality() == /* 4 ^ 4 */ 4 * 4 * 4 * 4 ); + TS_ASSERT( boolToBoolboolbool.getCardinality() == /* 8 ^ 2 */ 8 * 8 ); + } + + void testUndefinedSorts() { + Type foo = d_em->mkSort("foo"); + // We've currently assigned them a specific Beth number, which + // isn't really correct, but... + TS_ASSERT( !foo.getCardinality().isFinite() ); + } + + void testBitvectors() { + Debug.on("bvcard"); + TS_ASSERT( d_em->mkBitVectorType(0).getCardinality() == 0 ); + for(unsigned i = 1; i < 128; ++i) { + try { + Cardinality card = Cardinality(2) ^ i; + if( d_em->mkBitVectorType(i).getCardinality() != card ) { + stringstream ss; + ss << "test failed for bitvector(" << i << ")"; + TS_FAIL(ss.str().c_str()); + } + } catch(Exception& e) { + cout << endl << e << endl; + throw; + } + } + } + +};/* TypeCardinalityPublic */ diff --git a/test/unit/util/cardinality_public.h b/test/unit/util/cardinality_public.h new file mode 100644 index 000000000..5927e1bfa --- /dev/null +++ b/test/unit/util/cardinality_public.h @@ -0,0 +1,255 @@ +/********************* */ +/*! \file cardinality_public.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Public-box testing of CVC4::Cardinality + ** + ** Public-box testing of CVC4::Cardinality. + **/ + +#include "util/cardinality.h" +#include "util/integer.h" + +#include <string> +#include <sstream> + +using namespace CVC4; +using namespace std; + +class CardinalityPublic : public CxxTest::TestSuite { + stringstream ss; + +public: + + void testCardinalities() { + Cardinality zero(0); + Cardinality one(1); + Cardinality two(2); + + Cardinality invalid(0); + TS_ASSERT_THROWS( invalid = Cardinality(-1), IllegalArgumentException); + TS_ASSERT_THROWS( invalid = Cardinality(-2), IllegalArgumentException); + TS_ASSERT_THROWS( invalid = Cardinality(Integer("-3983982192391747295721957")), IllegalArgumentException); + invalid = one; // test assignment + invalid = Cardinality(5); // test assignment to temporary + + Cardinality copy(one); // test copy + Cardinality big(Integer("3983982192391747295721957")); + Cardinality r(Cardinality::REALS); + Cardinality i(Cardinality::INTEGERS); + + TS_ASSERT( zero < one ); + TS_ASSERT( one < two ); + TS_ASSERT( two < invalid ); + TS_ASSERT( invalid < big ); + TS_ASSERT( big < i ); + TS_ASSERT( i < r ); + + TS_ASSERT( zero <= one ); + TS_ASSERT( zero <= zero ); + TS_ASSERT( one <= two ); + TS_ASSERT( one <= one ); + TS_ASSERT( two <= invalid ); + TS_ASSERT( two <= two ); + TS_ASSERT( invalid <= big ); + TS_ASSERT( invalid <= invalid ); + TS_ASSERT( big <= i ); + TS_ASSERT( big <= big ); + TS_ASSERT( i <= r ); + TS_ASSERT( i <= i ); + TS_ASSERT( r <= r ); + + TS_ASSERT( zero == zero ); + TS_ASSERT( one == one ); + TS_ASSERT( two == two ); + TS_ASSERT( invalid == invalid ); + TS_ASSERT( copy == copy ); + TS_ASSERT( copy == one ); + TS_ASSERT( one == copy ); + TS_ASSERT( big == big ); + TS_ASSERT( i == i ); + TS_ASSERT( r == r ); + + TS_ASSERT( zero != one ); + TS_ASSERT( one != two ); + TS_ASSERT( two != invalid ); + TS_ASSERT( copy != r ); + TS_ASSERT( copy != i ); + TS_ASSERT( big != i ); + TS_ASSERT( i != big ); + TS_ASSERT( big != zero ); + TS_ASSERT( r != i ); + TS_ASSERT( i != r ); + + TS_ASSERT( r > zero ); + TS_ASSERT( r > one ); + TS_ASSERT( r > two ); + TS_ASSERT( r > copy ); + TS_ASSERT( r > invalid ); + TS_ASSERT( r > big ); + TS_ASSERT( r > i ); + TS_ASSERT( !( r > r ) ); + TS_ASSERT( r >= r ); + + TS_ASSERT( zero.isFinite() ); + TS_ASSERT( one.isFinite() ); + TS_ASSERT( two.isFinite() ); + TS_ASSERT( copy.isFinite() ); + TS_ASSERT( invalid.isFinite() ); + TS_ASSERT( big.isFinite() ); + TS_ASSERT( !i.isFinite() ); + TS_ASSERT( !r.isFinite() ); + + TS_ASSERT( zero.getFiniteCardinality() == 0 ); + TS_ASSERT( one.getFiniteCardinality() == 1 ); + TS_ASSERT( two.getFiniteCardinality() == 2 ); + TS_ASSERT( copy.getFiniteCardinality() == 1 ); + TS_ASSERT( invalid.getFiniteCardinality() == 5 ); + TS_ASSERT( big.getFiniteCardinality() == Integer("3983982192391747295721957") ); + TS_ASSERT_THROWS( i.getFiniteCardinality(), IllegalArgumentException ); + TS_ASSERT_THROWS( r.getFiniteCardinality(), IllegalArgumentException ); + + TS_ASSERT_THROWS( zero.getBethNumber(), IllegalArgumentException ); + TS_ASSERT_THROWS( one.getBethNumber(), IllegalArgumentException ); + TS_ASSERT_THROWS( two.getBethNumber(), IllegalArgumentException ); + TS_ASSERT_THROWS( copy.getBethNumber(), IllegalArgumentException ); + TS_ASSERT_THROWS( invalid.getBethNumber(), IllegalArgumentException ); + TS_ASSERT_THROWS( big.getBethNumber(), IllegalArgumentException ); + TS_ASSERT( i.getBethNumber() == 0 ); + TS_ASSERT( r.getBethNumber() == 1 ); + + TS_ASSERT( zero != Cardinality::INTEGERS ); + TS_ASSERT( one != Cardinality::INTEGERS ); + TS_ASSERT( two != Cardinality::INTEGERS ); + TS_ASSERT( copy != Cardinality::INTEGERS ); + TS_ASSERT( invalid != Cardinality::INTEGERS ); + TS_ASSERT( big != Cardinality::INTEGERS ); + TS_ASSERT( r != Cardinality::INTEGERS ); + TS_ASSERT( i == Cardinality::INTEGERS ); + + TS_ASSERT( zero != Cardinality::REALS ); + TS_ASSERT( one != Cardinality::REALS ); + TS_ASSERT( two != Cardinality::REALS ); + TS_ASSERT( copy != Cardinality::REALS ); + TS_ASSERT( invalid != Cardinality::REALS ); + TS_ASSERT( big != Cardinality::REALS ); + TS_ASSERT( i != Cardinality::REALS ); + TS_ASSERT( r == Cardinality::REALS ); + + // should work the other way too + + TS_ASSERT( Cardinality::INTEGERS != zero ); + TS_ASSERT( Cardinality::INTEGERS != one ); + TS_ASSERT( Cardinality::INTEGERS != two ); + TS_ASSERT( Cardinality::INTEGERS != copy ); + TS_ASSERT( Cardinality::INTEGERS != invalid ); + TS_ASSERT( Cardinality::INTEGERS != big ); + TS_ASSERT( Cardinality::INTEGERS != r ); + TS_ASSERT( Cardinality::INTEGERS == i ); + + TS_ASSERT( Cardinality::REALS != zero ); + TS_ASSERT( Cardinality::REALS != one ); + TS_ASSERT( Cardinality::REALS != two ); + TS_ASSERT( Cardinality::REALS != copy ); + TS_ASSERT( Cardinality::REALS != invalid ); + TS_ASSERT( Cardinality::REALS != big ); + TS_ASSERT( Cardinality::REALS != i ); + TS_ASSERT( Cardinality::REALS == r ); + + // finite cardinal arithmetic + + TS_ASSERT( zero + zero == zero ); + TS_ASSERT( zero * zero == zero ); + TS_ASSERT( (zero ^ zero) == one ); + TS_ASSERT( zero + one == one ); + TS_ASSERT( zero * one == zero ); + TS_ASSERT( (zero ^ one) == zero ); + TS_ASSERT( one + zero == one ); + TS_ASSERT( one * zero == zero ); + TS_ASSERT( (one ^ zero) == one ); + TS_ASSERT( two + two == 4 ); + TS_ASSERT( (two ^ two) == 4 ); + TS_ASSERT( two * two == 4 ); + TS_ASSERT( (two += two) == 4 ); + TS_ASSERT( two == 4 ); + TS_ASSERT( (two = 2) == 2 ); + TS_ASSERT( two == 2 ); + TS_ASSERT( (two *= 2) == 4 ); + TS_ASSERT( two == 4 ); + TS_ASSERT( ((two = 2) ^= 2) == 4 ); + TS_ASSERT( two == 4 ); + TS_ASSERT( (two = 2) == 2 ); + + // infinite cardinal arithmetic + + Cardinality x = i, y = Cardinality(2)^x, z = Cardinality(2)^y; + + TS_ASSERT( x == i && y == r ); + TS_ASSERT( x != r && y != i ); + TS_ASSERT( x != z && y != z ); + TS_ASSERT( x.isCountable() && !x.isFinite() ); + TS_ASSERT( !y.isCountable() && !y.isFinite() ); + TS_ASSERT( !z.isCountable() && !z.isFinite() ); + + TS_ASSERT( big < x ); + TS_ASSERT( x < y ); + TS_ASSERT( y < z ); + + TS_ASSERT_THROWS( big.getBethNumber(), IllegalArgumentException ); + TS_ASSERT( x.getBethNumber() == 0 ); + TS_ASSERT( y.getBethNumber() == 1 ); + TS_ASSERT( z.getBethNumber() == 2 ); + + TS_ASSERT( (zero ^ x) == zero ); + TS_ASSERT( (one ^ x) == one ); + TS_ASSERT( (two ^ x) == y && (two ^ x) != x ); + TS_ASSERT( (big ^ x) == y && (big ^ x) != x ); + TS_ASSERT( (two ^ x) == (big ^ x) ); + + TS_ASSERT( (x ^ zero) == one ); + TS_ASSERT( (x ^ one) == x ); + TS_ASSERT( (x ^ two) == x ); + TS_ASSERT( (x ^ big) == x ); + TS_ASSERT( (x ^ big) == (x ^ two) ); + + TS_ASSERT( (zero ^ y) == zero ); + TS_ASSERT( (one ^ y) == one ); + TS_ASSERT( (two ^ y) != x && (two ^ y) != y ); + TS_ASSERT( (big ^ y) != y && (big ^ y) != y ); + TS_ASSERT( (big ^ y).getBethNumber() == 2 ); + TS_ASSERT( (two ^ y) == (big ^ y) ); + + TS_ASSERT( (y ^ zero) == one ); + TS_ASSERT( (y ^ one) == y ); + TS_ASSERT( (y ^ two) == y ); + TS_ASSERT( (y ^ big) == y ); + TS_ASSERT( (y ^ big) == (y ^ two) ); + + TS_ASSERT( (x ^ x) == y ); + TS_ASSERT( (y ^ x) == y ); + TS_ASSERT( (x ^ y) == z ); + TS_ASSERT( (y ^ y) == z ); + TS_ASSERT( (z ^ x) == z ); + TS_ASSERT( (z ^ y) == z ); + TS_ASSERT( (zero ^ z) == 0 ); + TS_ASSERT( (z ^ zero) == 1 ); + TS_ASSERT( (z ^ 0) == 1 ); + TS_ASSERT( (two ^ z) > z ); + TS_ASSERT( (big ^ z) == (two ^ z) ); + TS_ASSERT( (x ^ z) == (two ^ z) ); + TS_ASSERT( (y ^ z) == (x ^ z) ); + TS_ASSERT( (z ^ z) == (x ^ z) ); + TS_ASSERT( (z ^ z).getBethNumber() == 3 ); + + }/* testCardinalities() */ + +};/* class CardinalityPublic */ diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h index f4bd1f8b8..66e29a01b 100644 --- a/test/unit/util/integer_black.h +++ b/test/unit/util/integer_black.h @@ -18,6 +18,7 @@ #include <cxxtest/TestSuite.h> #include <sstream> +#include <limits> #include "util/integer.h" @@ -295,6 +296,17 @@ public: TS_ASSERT_EQUALS( Integer(-1000), Integer(-10).pow(3) ); } + void testOverlyLong() { + unsigned long ul = numeric_limits<unsigned long>::max(); + Integer i(ul); + TS_ASSERT(i.getUnsignedLong() == ul); + TS_ASSERT_THROWS_ANYTHING(i.getLong()); + unsigned long ulplus1 = ul + 1; + TS_ASSERT(ulplus1 == 0); + i = i + 1; + TS_ASSERT_THROWS_ANYTHING(i.getUnsignedLong()); + } + void testTestBit() { TS_ASSERT( ! Integer(0).testBit(6) ); TS_ASSERT( ! Integer(0).testBit(5) ); diff --git a/test/unit/util/subrange_bound_white.h b/test/unit/util/subrange_bound_white.h index a41f75af9..d7587d679 100644 --- a/test/unit/util/subrange_bound_white.h +++ b/test/unit/util/subrange_bound_white.h @@ -11,9 +11,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief White box testing of CVC4::SubrangeBound + ** \brief White-box testing of CVC4::SubrangeBound ** - ** White box testing of CVC4::SubrangeBound. + ** White-box testing of CVC4::SubrangeBound. **/ #include "util/subrange_bound.h" |