summaryrefslogtreecommitdiff
path: root/src/theory/mkrewriter
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/mkrewriter')
-rwxr-xr-xsrc/theory/mkrewriter10
1 files changed, 8 insertions, 2 deletions
diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index b8fa51d77..780409d52 100755
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -2,7 +2,7 @@
#
# mkrewriter
# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2011 The CVC4 Project
+# Copyright (c) 2010-2012 The CVC4 Project
#
# The purpose of this script is to create rewriter_tables.h from a template
# and a list of theory kinds.
@@ -14,7 +14,7 @@
# Output is to standard out.
#
-copyright=2010-2011
+copyright=2010-2012
cat <<EOF
/********************* */
@@ -83,6 +83,12 @@ function theory {
theory_id="$1"
}
+function instantiator {
+ # instantiator class header
+ lineno=${BASH_LINENO[0]}
+ check_theory_seen
+}
+
function properties {
# properties prop*
lineno=${BASH_LINENO[0]}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback