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, 25 insertions, 5 deletions

diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 35a245a84..0b384d518 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -72,22 +72,42 @@ 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
 }
 
+function rewriter {
+  # rewriter class header
+  lineno=${BASH_LINENO[0]}
+}
+
+function properties {
+    # properties prop*
+    lineno=${BASH_LINENO[0]}
+}
+
+function endtheory {
+  # endtheory
+  lineno=${BASH_LINENO[0]}
+}
+
+function sort {
+  # sort TYPE ["comment"]
+  lineno=${BASH_LINENO[0]}
+}
+
 function variable {
   # variable K ["comment"]