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