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/constraint.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/constraint.ml')
| -rw-r--r-- | src/constraint.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/constraint.ml b/src/constraint.ml index 7ead0cc8..b00c0a4e 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -53,6 +53,8 @@ open Ast open Ast_util open Util +let opt_smt_verbose = ref false + (* SMTLIB v2.0 format is based on S-expressions so we have a lightweight representation of those here. *) type sexpr = List of (sexpr list) | Atom of string @@ -185,7 +187,9 @@ let call_z3' l vars constraints : smt_result = let problems = [constraints] in let z3_file = smtlib_of_constraints l vars constraints in - (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *) + if !opt_smt_verbose then + prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file) + else (); let rec input_lines chan = function | 0 -> [] |