diff options
| author | Alasdair Armstrong | 2019-06-06 17:29:22 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-06-06 17:30:13 +0100 |
| commit | d225547fc49807961967181b8661a35fe4de8ed3 (patch) | |
| tree | 49e9ff8867271a6cff4f16bf056392a24f09540b /src/jib/jib_smt.mli | |
| parent | 9bdc4266ea3ba81ec3f05e44b1069a6752cdaf0a (diff) | |
Add an option to pre-compile the axiomatic model for SMT
Diffstat (limited to 'src/jib/jib_smt.mli')
| -rw-r--r-- | src/jib/jib_smt.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli index 2680f937..28d10fd3 100644 --- a/src/jib/jib_smt.mli +++ b/src/jib/jib_smt.mli @@ -139,6 +139,9 @@ module Make_optimizer(S : Sequence) : sig val optimize : smt_def Stack.t -> smt_def S.t end +val to_axiomatic_model : + string -> Type_check.Env.t -> Type_check.tannot defs -> unit + (** Generate SMT for all the $property and $counterexample pragmas in an AST, and write it to appropriately named files. *) val generate_smt : |