solver.ml 1.79 KB
 Erwan Jahier committed Mar 17, 2010 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 ``````(*----------------------------------------------------------------------- ** Copyright (C) 2001 - Verimag. ** This file may only be copied under the terms of the GNU Library General ** Public License **----------------------------------------------------------------------- ** ** File: solver.ml ** Main author: jahier@imag.fr ** *) open Formula open Lurette_stub exception False_formula let formula_list_to_conj fl = match fl with [] -> assert false | f::[] -> f | f1::f2::tail -> List.fold_left (fun x y -> And(x, y)) (And(f1, f2)) tail let rec (solve_formula_one: formula -> subst list * env_loc) = (* ** [solve_formula f] randomly assigns values to free variables occuring ** in the formula `f'. *) fun f -> match f with `````` Erwan Jahier committed Mar 17, 2010 32 33 `````` Bvar(var_name) -> ([(var_name, Bool(true))], []) | Not(Bvar(var_name)) -> ([(var_name, Bool(false))], []) `````` Erwan Jahier committed Mar 17, 2010 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 `````` | And(f1, f2) -> let (out1, loc1) = solve_formula_one f1 in let (out2, loc2) = solve_formula_one f2 in ((List.append out1 out2), (List.append loc1 loc2)) | False -> assert false | _ -> assert false (* ** XXX ** XXX FIXME !!! ** XXX *) let (solve_formula: int -> formula list -> (subst list * subst list) list) = (* ** [solve_formula p fl] randomly assigns p values to free variables occuring `````` Erwan Jahier committed Mar 17, 2010 49 `````` ** in the conjunction of formula appearing in `fl'. `````` Erwan Jahier committed Mar 17, 2010 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 `````` *) fun p fl -> let f = formula_list_to_conj fl in Util.unfold (solve_formula_one) f p (****************************************************************************) (****************************************************************************) let rec (is_satisfiable : formula list -> bool) = fun fl -> (* ** returns true if the formula is satisfiable *) not (List.mem False fl) (* XXX *)``````