summaryrefslogtreecommitdiff
path: root/src/initial_check.mli
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-12-19 20:18:04 +0000
committerAlasdair Armstrong2018-12-19 20:18:04 +0000
commit40f7f5d00a9afff27f1d2329ab525705e57c6d6f (patch)
treeb5e5315d0854e0bcac5a75c3f6cf9f3e0a4ed686 /src/initial_check.mli
parent52c604b1f8f70bf5ad1ce6a5495b926b1372faa0 (diff)
Improve sizeof rewriting performance
Simply constraints further before calling Z3 to improve performance of sizeof re-writing.
Diffstat (limited to 'src/initial_check.mli')
-rw-r--r--src/initial_check.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/initial_check.mli b/src/initial_check.mli
index 25187e4c..9d2beab2 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -92,3 +92,4 @@ val val_spec_of_string : id -> string -> unit def
val exp_of_string : string -> unit exp
val typ_of_string : string -> typ
+val constraint_of_string : string -> n_constraint