-
Notifications
You must be signed in to change notification settings - Fork 1
/
theories.mli
37 lines (31 loc) · 1.27 KB
/
theories.mli
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
open Formula
(**
* A theory works as follows: to solve a formula,
* first a premodel is constructed, then every construct must be solved,
* if they can be solved with this premodel, it means that the formula is
* satisfiable, and in this case, it produces an abstract_model, which can then be turned
* into a full model.
* If not, then it's up to the user to ask for another premodel and restart.
**)
module type T = sig
module Formula : F
open Formula
type premodel
type abstract_model
type model
type domain
(* for instance a cardinality constraints, or a forall, or a exists, or whatever *)
type construct
exception Unsat
val build_domain_for_construct: premodel -> construct -> domain
val ensure_domain: premodel -> string -> construct -> domain -> unit
val ensure_domain_fun: premodel -> (string -> string) -> construct -> domain -> unit
val ensure_domains_consistency: premodel -> domain list -> unit
val domain_to_string: domain -> string
val assert_formula: expr -> unit
val sort_for_construct: construct -> sort
val build_premodel: unit -> (((string -> string) * domain * construct) list) * premodel
val build_abstract_model: premodel -> abstract_model
val build_full_model: abstract_model -> model
val print_model: model -> unit
end