Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.

1 files changed, 58 insertions, 6 deletions

diff --git a/src/expr/mkkind b/src/expr/mkkind
index ab80224eb..d790a0195 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -37,10 +37,18 @@ template=$1; shift
 
 kind_decls=
 kind_printers=
+kind_to_theory_id=
+
+type_constant_descriptions=
+type_constant_list=
+type_constant_to_theory_id= 
 
 seen_theory=false
 seen_theory_builtin=false
 
+theory_enum=
+theory_descriptions=
+
 function theory {
   # theory T header
 
@@ -49,20 +57,50 @@ function theory {
   # this script doesn't care about the theory class information, but
   # makes does make sure it's there
   seen_theory=true
-  if [ "$1" = builtin ]; then
+  if [ "$1" = THEORY_BUILTIN ]; then
     if $seen_theory_builtin; then
       echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
       exit 1
     fi
     seen_theory_builtin=true
-  elif [ -z "$1" -o -z "$2" ]; then
+  elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then
     echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
     exit 1
-  elif ! expr "$1" : '\(::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
-  elif ! expr "$1" : '\(::CVC4::theory::*\)' >/dev/null; then
+  elif ! expr "$2" : '\(::*\)' >/dev/null; then
+    echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
+  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_descriptions="${theory_descriptions}    case ${theory_id}: out << \"${theory_id}\"; break;
+"
+}
+
+function properties {
+  # rewriter class header
+  lineno=${BASH_LINENO[0]}
+}
+
+function endtheory {
+  # endtheory
+  lineno=${BASH_LINENO[0]}
+}
+
+function rewriter {
+  # properties prop*
+  lineno=${BASH_LINENO[0]}
+}
+
+function sort {
+  # sort TYPE ["comment"]
+  
+  lineno=${BASH_LINENO[0]}
+  
+  check_theory_seen
+  register_sort "$1" "$2"
 }
 
 function variable {
@@ -101,6 +139,18 @@ function constant {
   register_kind "$1" 0 "$5"
 }
 
+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 {
   r=$1
   nc=$2
@@ -110,6 +160,8 @@ 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;
+"
 }
 
 function check_theory_seen {
@@ -144,7 +196,7 @@ check_builtin_theory_seen
 ## output
 
 text=$(cat "$template")
-for var in kind_decls kind_printers; 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 theory_descriptions; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
 error=`expr "$text" : '.*\${\([^}]*\)}.*'`