1 files changed, 14 insertions, 0 deletions
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 8b21814dc..28a47d84d 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -62,6 +62,9 @@ mkConst_instantiations=
 mkConst_implementations=
 exportConstant_cases=
 
+typerules=
+construles=
+
 seen_theory=false
 seen_theory_builtin=false
 
@@ -139,6 +142,16 @@ function typerule {
 "
 }
 
+function construle {
+  # isconst OPERATOR isconst-checking-class
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+  construles="${construles}
+  case kind::$1:
+    return $2::computeIsConst(nodeManager, n);
+"
+}
+
 function sort {
   # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
   lineno=${BASH_LINENO[0]}
@@ -262,6 +275,7 @@ for var in \
     exportConstant_cases \
     typechecker_includes \
     typerules \
+    construles \
     ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done