solver.mli 707 Bytes
Newer Older
1 2 3 4 5 6 7 8 9
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License 
**-----------------------------------------------------------------------
**
** File: solver.mli
** Main author: jahier@imag.fr
**
10
** Formula solver.
11 12 13 14 15
*)

open Formula

val is_satisfiable : formula list -> bool
16 17 18 19
(*
** succeeds if the list of formula (interpreted as a conjunct) is 
** satisfiable.
*)
20 21

val solve_formula: int -> formula list -> (subst list * subst list) list
22 23 24 25
(* 
** [solve_formula p fl] randomly assigns p values to free variables occuring
** in the conjunction of the formula of `fl'. 
*)
26 27