diff options
Diffstat (limited to 'src/constraint.mli')
| -rw-r--r-- | src/constraint.mli | 34 |
1 files changed, 4 insertions, 30 deletions
diff --git a/src/constraint.mli b/src/constraint.mli index df9c8b3a..51088245 100644 --- a/src/constraint.mli +++ b/src/constraint.mli @@ -49,40 +49,14 @@ (**************************************************************************) module Big_int = Nat_big_num - -type nexp -type t +open Ast +open Ast_util type smt_result = Unknown | Sat | Unsat val load_digests : unit -> unit val save_digests : unit -> unit -val call_z3 : t -> smt_result - -val solve_z3 : t -> int -> Big_int.num option - -val string_of : t -> string - -val implies : t -> t -> t -val conj : t -> t -> t -val disj : t -> t -> t -val negate : t -> t -val literal : bool -> t -val forall : int list -> t -> t - -val lt : nexp -> nexp -> t -val lteq : nexp -> nexp -> t -val gt : nexp -> nexp -> t -val gteq : nexp -> nexp -> t -val eq : nexp -> nexp -> t -val neq : nexp -> nexp -> t - -val pow2 : nexp -> nexp -val add : nexp -> nexp -> nexp -val sub : nexp -> nexp -> nexp -val mult : nexp -> nexp -> nexp -val app : string -> nexp list -> nexp +val call_z3 : l -> kind_aux KBindings.t -> n_constraint -> smt_result -val constant : Big_int.num -> nexp -val variable : int -> nexp +val solve_z3 : l -> kind_aux KBindings.t -> n_constraint -> kid -> Big_int.num option |