summaryrefslogtreecommitdiff
path: root/src/theory/mktheoryof
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/mktheoryof')
-rwxr-xr-xsrc/theory/mktheoryof14
1 files changed, 11 insertions, 3 deletions
diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof
index ef967342b..842e02a07 100755
--- a/src/theory/mktheoryof
+++ b/src/theory/mktheoryof
@@ -5,11 +5,11 @@
# Copyright (c) 2010 The CVC4 Project
#
# The purpose of this script is to create theoryof_table.h from a
-# prologue, epilogue, and a list of theory kinds.
+# template and a list of theory kinds.
#
# Invocation:
#
-# mktheoryof prologue-file epilogue-file theory-kind-files...
+# mktheoryof template-file theory-kind-files...
#
# Output is to standard out.
#
@@ -17,7 +17,7 @@
copyright=2010
cat <<EOF
-/********************* -*- C++ -*- */
+/********************* */
/** theoryof_table.h
**
** Copyright $copyright The AcSys Group, New York University, and as below.
@@ -84,6 +84,14 @@ function operator {
do_theoryof "$1"
}
+function nonatomic_operator {
+ # nonatomic_operator K #children ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ do_theoryof "$1"
+}
+
function parameterized {
# parameterized K #children ["comment"]
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback