solver.ml 1.79 KB
Newer Older
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
32 33
	Bvar(var_name) -> ([(var_name, Bool(true))], [])
      | Not(Bvar(var_name)) -> ([(var_name, Bool(false))], [])
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
49
   ** in the conjunction of formula appearing in `fl'. 
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 *)