blob: a5959357a6a9b40d4720ebcdbf0ec39887a9d35a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2021 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
type t
type result = Sat | Unsat
val create : string array -> t
val send_command : t -> string -> (t -> 'a) -> 'a
val set_option : t -> string -> bool -> unit
val set_logic : t -> string -> unit
val declare_sort : t -> string -> int -> unit
val declare_fun : t -> string -> string list -> string -> unit
val assume : t -> string -> unit
val check_sat : t -> result
val get_proof : t -> (Lexing.lexbuf -> 'a) -> 'a
val get_model : t -> SExpr.t
val quit : t -> unit
|
