diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
commit | f9a4fe48a4ec2355f8fec93d3f47242577df2511 (patch) | |
tree | eb49b7760b16aa17666d59464c96979b445fbcc8 /src/expr/mkexpr | |
parent | eecc1e4f301711dbb2bf1508ea0ba6cd20acd593 (diff) |
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.
Diffstat (limited to 'src/expr/mkexpr')
-rwxr-xr-x | src/expr/mkexpr | 30 |
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"] |