From 9e164f1af5d2bd6f13eb894c8d395c7155590877 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 28 Feb 2011 07:03:33 +0000 Subject: Review of mktheorytraits, mkrewriter, and recent changes to other mk* scripts. Minor changes only, correcting some documentation and fixing some warnings that were being issued about functions not existing. --- src/expr/mkexpr | 20 +++++++----------- src/expr/mkkind | 21 ++++++++++--------- src/expr/mkmetakind | 8 +++++-- src/theory/Makefile.am | 2 +- src/theory/mkrewriter | 36 +++++++++++++++++++++++++------- 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 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 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 </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 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 </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 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 <&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 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 </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 { -- cgit v1.2.3