diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-25 06:56:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-25 06:56:14 +0000 |
commit | cb7363eef352200615e1a0d3729cea8b2c74d265 (patch) | |
tree | d57f6a9cfab879c1027e7282f63d0fae14fc0153 /src/expr | |
parent | e39882bd8a308711135a1ff644293fd9c46e6433 (diff) |
Weekend work. The main points:
* Type::getCardinality() returns the cardinality for for all types.
Theories give a cardinality in the their kinds file. For
cardinalities that depend on a type argument, a "cardinality
computer" function is named in the kinds file, which takes a
TypeNode and returns its cardinality.
* There's a bitmap for the set of "active theories" in the
TheoryEngine. Theories become "active" when a term that is owned by
them, or whose type is owned by them, is pre-registered (run CVC4
with --verbose to see theory activation). Non-active theories don't
get any calls for check() or propagate() or anything, and if we're
running in single-theory mode, the shared term manager doesn't have
to get involved. This is really important for get() performance
(which can only skimp on walking the entire sub-DAG only if the
theory doesn't require it AND the shared term manager doesn't
require it).
* TheoryEngine now does not call presolve(), registerTerm(),
notifyRestart(), etc., on a Theory if that theory doesn't declare
that property in its kinds file. To avoid coding errors,
mktheorytraits greps the theory header and gives warnings if:
+ the theory appears to declare one of the functions (check,
propagate, etc.) that isn't listed among its kinds file properties
(but probably should be)
+ the theory appears NOT to declare one of the functions listed in
its kinds file properties
* some bounded token stream work
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile.am | 11 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 1 | ||||
-rw-r--r-- | src/expr/expr_template.h | 2 | ||||
-rw-r--r-- | src/expr/kind_template.h | 2 | ||||
-rwxr-xr-x | src/expr/mkexpr | 30 | ||||
-rwxr-xr-x | src/expr/mkkind | 98 | ||||
-rwxr-xr-x | src/expr/mkmetakind | 31 | ||||
-rw-r--r-- | src/expr/type.cpp | 5 | ||||
-rw-r--r-- | src/expr/type.h | 6 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 5 | ||||
-rw-r--r-- | src/expr/type_node.h | 8 | ||||
-rw-r--r-- | src/expr/type_properties_template.h | 87 |
12 files changed, 267 insertions, 19 deletions
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 */ |