Review of mktheorytraits, mkrewriter, and recent changes to other mk* scripts. Minor...

diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 0b384d518290178bde1791842f0c6cf1b554f2a6..40bf9992c75dd5fe88a3d188e71f21fd73cb61e1 100755 (executable)
--- 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 d790a0195de72583980007f31170049de9631190..631f73a8932009ef7c544af24251b12c85cd2273 100755 (executable)
--- 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 0d0ff44750983cff45a23b2de599c63759815e1a..7f9037c1c90f360f42691a7a950d1e906a9dd068 100755 (executable)
--- 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 142aef0048d6c362a8f5872500e397c3844bb1a1..a9ff5376d7f98209eb96029fc3cea72246c72623 100644 (file)
--- 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 8eb29bb1527a7325782b4c4bcf0e92126c8b9f0f..a53da20226dd79b222bd554844110e8f167afb60 100755 (executable)
--- 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 58e5e4381c5cc885db5b9d5e15138e1f2bae2e3f..c06770a517842ced9c6e713f860beccd0583de8b 100755 (executable)
--- 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 {