solver.ml 2.04 KB
Newer Older
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

14 15
(****************************************************************************)
(****************************************************************************)
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
28
   ** in `f'. 
29 30
   *)
  fun f ->
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
    )
47 48
 	  (* 
	   ** XXX 
49
	   ** XXX FIX US !!!
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
56
   ** in the conjunction of formula appearing in `fl'. 
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)
71 72 73
      (* XXX  FIX ME !!! *)