diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-02-28 07:03:33 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-02-28 07:03:33 +0000 |
commit | 9e164f1af5d2bd6f13eb894c8d395c7155590877 (patch) | |
tree | f5e8658db62b50b447fbc18590570501e57129d5 /src/theory | |
parent | bda6ad1b93619a68006034d9a47e641ce5ab14a7 (diff) |
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.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/Makefile.am | 2 | ||||
-rwxr-xr-x | src/theory/mkrewriter | 36 | ||||
-rwxr-xr-x | src/theory/mktheorytraits | 53 |
3 files changed, 52 insertions, 39 deletions
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 { |