1(* ========================================================================= *)
2(* THE MESON PROOF PROCEDURE                                                 *)
3(* Copyright (c) 2001-2004 Joe Hurd.                                         *)
4(* ========================================================================= *)
5
6signature mlibMeson =
7sig
8
9type solver_node = mlibSolver.solver_node
10
11(* Tuning parameters *)
12type parameters =
13  {ancestor_pruning : bool,
14   ancestor_cutting : bool,
15   state_simplify   : bool,
16   cache_cutting    : bool,
17   divide_conquer   : bool,
18   unit_lemmaizing  : bool,
19   sort_literals    : int,                        (* In the range [0..2] *)
20   sort_rules       : bool}
21
22type 'a Parmupdate = ('a -> 'a) -> parameters -> parameters
23val defaults                : parameters
24val update_ancestor_pruning : bool Parmupdate
25val update_ancestor_cutting : bool Parmupdate
26val update_state_simplify   : bool Parmupdate
27val update_cache_cutting    : bool Parmupdate
28val update_divide_conquer   : bool Parmupdate
29val update_unit_lemmaizing  : bool Parmupdate
30val update_sort_literals    : int Parmupdate
31val update_sort_rules       : bool Parmupdate
32
33(* The meson solver *)
34val meson' : string * parameters -> solver_node
35val meson  : solver_node                          (* Uses defaults *)
36
37(* The delta preprocessor as a solver *)
38val delta' : string * parameters -> solver_node
39val delta  : solver_node                          (* Uses defaults *)
40
41(* The prolog solver *)
42val prolog' : string * parameters -> solver_node
43val prolog  : solver_node                         (* Uses defaults *)
44
45end
46