summaryrefslogtreecommitdiff
path: root/src/theory/mktheorytraits
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/mktheorytraits')
-rwxr-xr-xsrc/theory/mktheorytraits16
1 files changed, 0 insertions, 16 deletions
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index c8ef23a78..a44d8e9c3 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -61,9 +61,6 @@ theory_parametric="false"
rewriter_class=
rewriter_header=
-instantiator_class=void
-instantiator_header=
-
theory_id=
theory_class=
@@ -135,7 +132,6 @@ template<>
struct TheoryTraits<${theory_id}> {
typedef ${theory_class} theory_class;
typedef ${rewriter_class} rewriter_class;
- typedef ${instantiator_class} instantiator_class;
static const bool isStableInfinite = ${theory_stable_infinite};
static const bool isFinite = ${theory_finite};
@@ -240,18 +236,6 @@ function construle {
check_theory_seen
}
-function instantiator {
- # instantiator class header
- lineno=${BASH_LINENO[0]}
- check_theory_seen
-
- instantiator_class="$1"
- instantiator_header="$2"
-
- theory_includes="${theory_includes}#include \"$2\"
-"
-}
-
function properties {
# properties property*
lineno=${BASH_LINENO[0]}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback