solver.ml 2.04 KB
 Erwan Jahier committed Mar 17, 2010 1 2 3 4 5 6 7 8 9 10 11 12 13 ``````(*----------------------------------------------------------------------- ** 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 `````` Erwan Jahier committed Mar 17, 2010 14 15 ``````(****************************************************************************) (****************************************************************************) `````` Erwan Jahier committed Mar 17, 2010 16 17 18 19 20 21 22 23 24 25 26 27 `````` 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 `````` Erwan Jahier committed Mar 17, 2010 28 `````` ** in `f'. `````` Erwan Jahier committed Mar 17, 2010 29 30 `````` *) fun f -> `````` Erwan Jahier committed Mar 17, 2010 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 `````` ( match f with Bvar(var_name) -> ([(var_name, Lurette_stub.Bool(true))], []) | Not(Bvar(var_name)) -> ([(var_name, Lurette_stub.Bool(false))], []) | 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)) | True -> ([], []) | False -> ([], []) | Or(f1, f2) -> assert false | Eq(e1, e2) -> assert false | Ge(e1, e2) -> assert false | G(e1, e2) -> assert false ) `````` Erwan Jahier committed Mar 17, 2010 47 48 `````` (* ** XXX `````` Erwan Jahier committed Mar 17, 2010 49 `````` ** XXX FIX US !!! `````` Erwan Jahier committed Mar 17, 2010 50 51 52 53 54 55 `````` ** 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 56 `````` ** in the conjunction of formula appearing in `fl'. `````` Erwan Jahier committed Mar 17, 2010 57 58 59 60 61 62 63 64 65 66 67 68 69 70 `````` *) 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) `````` Erwan Jahier committed Mar 17, 2010 71 72 73 `````` (* XXX FIX ME !!! *) ``````