diff options
| author | Jon French | 2019-02-25 12:10:30 +0000 |
|---|---|---|
| committer | Jon French | 2019-02-25 12:10:30 +0000 |
| commit | 915d75f9c49fa2c2a9d47d189e4224cee16582c9 (patch) | |
| tree | 77a93e682796977898af0b56e0a61d7689db112e /src/constraint.mli | |
| parent | a8a5308e4981b3d09fb2bf0c59d592ef6ae4417e (diff) | |
| parent | 38656b50ad24df6a29f3a84e50adfcf409131fb0 (diff) | |
Merge branch 'sail2' into rmem_interpreter
Diffstat (limited to 'src/constraint.mli')
| -rw-r--r-- | src/constraint.mli | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/constraint.mli b/src/constraint.mli index fa318c35..b5d6ff6b 100644 --- a/src/constraint.mli +++ b/src/constraint.mli @@ -54,11 +54,17 @@ open Ast_util val opt_smt_verbose : bool ref +val set_solver : string -> unit + type smt_result = Unknown | Sat | Unsat val load_digests : unit -> unit val save_digests : unit -> unit -val call_z3 : l -> kind_aux KBindings.t -> n_constraint -> smt_result +val call_smt : l -> kind_aux KBindings.t -> n_constraint -> smt_result + +val solve_smt : l -> kind_aux KBindings.t -> 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_z3 : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option +val solve_unique_smt : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option |