diff options
| author | Jon French | 2019-04-15 16:18:18 +0100 |
|---|---|---|
| committer | Jon French | 2019-04-15 16:18:18 +0100 |
| commit | a9f0b829507e9882efdb59cce4d83ea7e87f5f71 (patch) | |
| tree | 11cde6c1918bc15f4dda9a8e40afd4a1fe912a0a /src/constraint.mli | |
| parent | 0f6fd188ca232cb539592801fcbb873d59611d81 (diff) | |
| parent | 57443173923e87f33713c99dbab9eba7e3db0660 (diff) | |
Merge branch 'sail2' into rmem_interpreter
Diffstat (limited to 'src/constraint.mli')
| -rw-r--r-- | src/constraint.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/constraint.mli b/src/constraint.mli index b5d6ff6b..34e83964 100644 --- a/src/constraint.mli +++ b/src/constraint.mli @@ -61,10 +61,10 @@ type smt_result = Unknown | Sat | Unsat val load_digests : unit -> unit val save_digests : unit -> unit -val call_smt : l -> kind_aux KBindings.t -> n_constraint -> smt_result +val call_smt : l -> n_constraint -> smt_result -val solve_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option +val solve_smt : l -> n_constraint -> kid -> Big_int.num option -val solve_all_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num list option +val solve_all_smt : l -> n_constraint -> kid -> Big_int.num list option -val solve_unique_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option +val solve_unique_smt : l -> n_constraint -> kid -> Big_int.num option |