diff options
| author | Alasdair Armstrong | 2018-12-19 20:18:04 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-12-19 20:18:04 +0000 |
| commit | 40f7f5d00a9afff27f1d2329ab525705e57c6d6f (patch) | |
| tree | b5e5315d0854e0bcac5a75c3f6cf9f3e0a4ed686 /src/initial_check.ml | |
| parent | 52c604b1f8f70bf5ad1ce6a5495b926b1372faa0 (diff) | |
Improve sizeof rewriting performance
Simply constraints further before calling Z3 to improve performance of
sizeof re-writing.
Diffstat (limited to 'src/initial_check.ml')
| -rw-r--r-- | src/initial_check.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index 17b4b515..16597b3a 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -795,6 +795,10 @@ let typ_of_string str = let typ = to_ast_typ initial_ctx typ in typ +let constraint_of_string str = + let atyp = Parser.typ_eof Lexer.token (Lexing.from_string str) in + to_ast_constraint initial_ctx atyp + let extern_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, (fun _ -> Some (string_of_id id)), false)) let val_spec_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, (fun _ -> None), false)) |