diff options
Diffstat (limited to 'src')
-rwxr-xr-x | src/expr/mkexpr | 20 | ||||
-rwxr-xr-x | src/expr/mkkind | 21 | ||||
-rwxr-xr-x | src/expr/mkmetakind | 8 | ||||
-rw-r--r-- | src/theory/Makefile.am | 2 | ||||
-rwxr-xr-x | src/theory/mkrewriter | 36 | ||||
-rwxr-xr-x | src/theory/mktheorytraits | 53 |
6 files changed, 77 insertions, 63 deletions
diff --git a/src/expr/mkexpr b/src/expr/mkexpr index 0b384d518..40bf9992c 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -2,7 +2,7 @@ # # mkexpr # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 -# Copyright (c) 2010 The CVC4 Project +# Copyright (c) 2010-2011 The CVC4 Project # # The purpose of this script is to create {expr,expr_manager}.{h,cpp} # from template files and a list of theory kinds. Basically it just @@ -15,7 +15,7 @@ # Output is to standard out. # -copyright=2010 +copyright=2010-2011 filename=`basename "$1" | sed 's,_template,,'` @@ -91,52 +91,48 @@ function theory { function rewriter { # rewriter class header lineno=${BASH_LINENO[0]} + check_theory_seen } function properties { - # properties prop* - lineno=${BASH_LINENO[0]} + # properties prop* + lineno=${BASH_LINENO[0]} + check_theory_seen } function endtheory { # endtheory lineno=${BASH_LINENO[0]} + check_theory_seen } function sort { # sort TYPE ["comment"] lineno=${BASH_LINENO[0]} + check_theory_seen } function variable { # variable K ["comment"] - lineno=${BASH_LINENO[0]} - check_theory_seen } function operator { # operator K #children ["comment"] - lineno=${BASH_LINENO[0]} - check_theory_seen } function parameterized { # parameterized K #children ["comment"] - lineno=${BASH_LINENO[0]} - check_theory_seen } function constant { # constant K T Hasher header ["comment"] - lineno=${BASH_LINENO[0]} - check_theory_seen includes="${includes} diff --git a/src/expr/mkkind b/src/expr/mkkind index d790a0195..631f73a89 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -2,7 +2,7 @@ # # mkkind # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 -# Copyright (c) 2010 The CVC4 Project +# 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. @@ -14,7 +14,7 @@ # Output is to standard out. # -copyright=2010 +copyright=2010-2011 cat <<EOF /********************* */ @@ -41,7 +41,7 @@ kind_to_theory_id= type_constant_descriptions= type_constant_list= -type_constant_to_theory_id= +type_constant_to_theory_id= seen_theory=false seen_theory_builtin=false @@ -71,10 +71,10 @@ 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_enum="$1, - ${theory_enum}" + theory_enum="$1, + ${theory_enum}" theory_descriptions="${theory_descriptions} case ${theory_id}: out << \"${theory_id}\"; break; " } @@ -82,23 +82,24 @@ function theory { function properties { # rewriter class header lineno=${BASH_LINENO[0]} + check_theory_seen } function endtheory { # endtheory lineno=${BASH_LINENO[0]} + check_theory_seen } function rewriter { # properties prop* lineno=${BASH_LINENO[0]} + check_theory_seen } function sort { # sort TYPE ["comment"] - lineno=${BASH_LINENO[0]} - check_theory_seen register_sort "$1" "$2" } @@ -142,13 +143,13 @@ function constant { function register_sort { id=$1 comment=$2 - + 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; -" +" } function register_kind { diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 0d0ff4475..7f9037c1c 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -2,7 +2,7 @@ # # mkmetakind # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 -# Copyright (c) 2010 The CVC4 Project +# Copyright (c) 2010-2011 The CVC4 Project # # The purpose of this script is to create metakind.h from a template # and a list of theory kinds. @@ -17,7 +17,7 @@ # Output is to standard out. # -copyright=2010 +copyright=2010-2011 cat <<EOF /********************* */ @@ -83,21 +83,25 @@ function theory { function properties { # properties prop* lineno=${BASH_LINENO[0]} + check_theory_seen } function endtheory { # endtheory lineno=${BASH_LINENO[0]} + check_theory_seen } function rewriter { # rewriter class header lineno=${BASH_LINENO[0]} + check_theory_seen } function sort { # sort TYPE ["comment"] lineno=${BASH_LINENO[0]} + check_theory_seen } function variable { diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 142aef004..a9ff5376d 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -65,7 +65,7 @@ rewriter_tables.h: rewriter_tables_template.h mkrewriter @top_builddir@/src/theo theory_traits.h: theory_traits_template.h mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mktheorytraits $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true - $(AM_V_GEN)(@srcdir@//mktheorytraits \ + $(AM_V_GEN)(@srcdir@/mktheorytraits \ $< \ `cat @top_builddir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter index 8eb29bb15..a53da2022 100755 --- a/src/theory/mkrewriter +++ b/src/theory/mkrewriter @@ -2,23 +2,23 @@ # # mkrewriter # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 -# Copyright (c) 2010 The CVC4 Project +# 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 rewriter_tables.h from a template +# and a list of theory kinds. # # Invocation: # -# mkkind template-file theory-kind-files... +# mkrewriter template-file theory-kind-files... # # Output is to standard out. # -copyright=2010 +copyright=2010-2011 cat <<EOF /********************* */ -/** kind.h +/** rewriter_tables.h ** ** Copyright $copyright The AcSys Group, New York University, and as below. ** @@ -79,18 +79,20 @@ function theory { function properties { # properties prop* lineno=${BASH_LINENO[0]} + check_theory_seen } function endtheory { # endtheory lineno=${BASH_LINENO[0]} + check_theory_seen } function rewriter { # rewriter class header class="$1" header="$2" - + rewriter_includes="${rewriter_includes}#include \"$header\" " rewrite_init="${rewrite_init} ${class}::init(); @@ -113,32 +115,50 @@ function rewriter { " lineno=${BASH_LINENO[0]} - + check_theory_seen } function sort { # sort TYPE ["comment"] lineno=${BASH_LINENO[0]} + check_theory_seen } function variable { # variable K ["comment"] lineno=${BASH_LINENO[0]} + check_theory_seen } function operator { # operator K #children ["comment"] lineno=${BASH_LINENO[0]} + check_theory_seen } function parameterized { # parameterized K1 K2 #children ["comment"] lineno=${BASH_LINENO[0]} + check_theory_seen } function constant { # constant K T Hasher header ["comment"] lineno=${BASH_LINENO[0]} + check_theory_seen +} + +function check_theory_seen { + if ! $seen_theory; then + echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2 + exit 1 + fi +} + +function check_builtin_theory_seen { + if ! $seen_theory_builtin; then + echo "$me: warning: no declaration for the builtin theory found" >&2 + fi } while [ $# -gt 0 ]; do diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 58e5e4381..c06770a51 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -2,19 +2,19 @@ # # mktheorytraits # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 -# Copyright (c) 2010 The CVC4 Project +# 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 theory_traits.h from a template +# and a list of theory kinds. # # Invocation: # -# mkkind template-file theory-kind-files... +# mktheorytraits template-file theory-kind-files... # # Output is to standard out. # -copyright=2010 +copyright=2010-2011 cat <<EOF /********************* */ @@ -51,7 +51,7 @@ theory_polite="false" rewriter_class= rewriter_header= - + theory_id= theory_class= @@ -80,10 +80,10 @@ 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_class="$2" - + theory_includes="${theory_includes}#include \"$3\" " theory_for_each_macro="${theory_for_each_macro} CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::${theory_id}) \\ @@ -93,28 +93,30 @@ function theory { function rewriter { # rewriter class header lineno=${BASH_LINENO[0]} - + check_theory_seen + rewriter_class="$1" rewriter_header="$2" - + theory_includes="${theory_includes}#include \"$2\" " - } function endtheory { # endtheory - + lineno=${BASH_LINENO[0]} + check_theory_seen + theory_traits="${theory_traits} template<> struct TheoryTraits<${theory_id}> { typedef ${theory_class} theory_class; typedef ${rewriter_class} rewriter_class; - + static const bool isStableInfinite = ${theory_stable_infinite}; static const bool isFinite = ${theory_finite}; static const bool isPolite = ${theory_polite}; - + static const bool hasCheck = ${theory_has_check}; static const bool hasPropagate = ${theory_has_propagate}; static const bool hasStaticLearning = ${theory_has_static_learning}; @@ -133,10 +135,10 @@ struct TheoryTraits<${theory_id}> { rewriter_class= rewriter_header= - + theory_id= theory_class= - + lineno=${BASH_LINENO[0]} } @@ -144,10 +146,11 @@ struct TheoryTraits<${theory_id}> { function properties { # properties property* lineno=${BASH_LINENO[0]} - while (( $# )); + check_theory_seen + while (( $# )); do property="$1" - case "$property" in + case "$property" in finite) theory_finite="true";; stable-infinite) theory_stable_infinite="true";; polite) theory_polite="true";; @@ -157,50 +160,40 @@ function properties { presolve) theory_has_presolve="true"; esac shift - done; + done } function sort { # sort TYPE ["comment"] - lineno=${BASH_LINENO[0]} - check_theory_seen register_sort "$1" "$2" } function variable { # variable K ["comment"] - lineno=${BASH_LINENO[0]} - check_theory_seen register_kind "$1" 0 "$2" } function operator { # operator K #children ["comment"] - lineno=${BASH_LINENO[0]} - check_theory_seen register_kind "$1" "$2" "$3" } function parameterized { # parameterized K1 K2 #children ["comment"] - lineno=${BASH_LINENO[0]} - check_theory_seen register_kind "$1" "$3" "$4" } function constant { # constant K T Hasher header ["comment"] - lineno=${BASH_LINENO[0]} - check_theory_seen register_kind "$1" 0 "$5" } @@ -209,7 +202,7 @@ function register_sort { id=$1 comment=$2 type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break; -" +" } function register_kind { |