summaryrefslogtreecommitdiff
path: root/src/expr/mkexpr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/mkexpr')
-rwxr-xr-xsrc/expr/mkexpr8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 8c94db3cc..9e7a2596f 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -65,6 +65,7 @@ exportConstant_cases=
typerules=
construles=
+neverconstrules=
seen_theory=false
seen_theory_builtin=false
@@ -168,6 +169,12 @@ function construle {
#line $lineno \"$kf\"
return $2::computeIsConst(nodeManager, n);
"
+ neverconstrules="${neverconstrules}
+#line $lineno \"$kf\"
+ case kind::$1:
+#line $lineno \"$kf\"
+ return false;
+"
}
function sort {
@@ -294,6 +301,7 @@ for var in \
typechecker_includes \
typerules \
construles \
+ neverconstrules \
; do
eval text="\${text//\\\$\\{$var\\}/\${$var}}"
done
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback