(*
 * lablai - An ML Artificial Inteligence library
 * Copyright (C) 2006  Till Crueger
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 *)

(* File $RCSfile$ *)
(* last edited by $Author: till_crueger $ *)
(* $Date: 2007-12-15 19:53:03 +0100 (Sa, 15 Dez 2007) $, $Revision: 29 $ *)

type formula = True
   | False
   | Not of formula
   | Var of string
   | And of formula * formula
   | Or   of formula * formula
   | Implicates of formula * formula
   | Equals  of formula * formula
   ;;

(* all the assignments are kept in a simple association table*)
type model = (string * bool) list;;

type assignment = model -> model;;

exception Var_unbound;;
   
let empty : model = [];;   

let rec lookup ~var model =
   (*just try to look up the variable directely*)
   try 
      List.assoc var model
   with 
      Not_found -> raise Var_unbound
   ;;

let assign ~var value model =
   let rec loop vars =
      match vars with
         (* see if the variable was bound before *)
         ((var2,assig) :: vars) ->
            if var2 =var then
               (* then bind it to the new value *)
               (var2,value) :: vars
            else
               (var2,assig) :: (loop vars)
      |  [] ->
         (* else introduce a new binding*)
         (var,value) :: []
   in
   loop model
   ;;
   
let combine assig1 assig2 =
   fun model -> assig1 (assig2 model)
   ;;

let create assigs =
   let folder model assig = assig model in
   List.fold_left folder empty assigs
   ;;
   
let rec solve formula model =
   (* straightforward translation of the formula *)
   match formula with
      True   -> true
   |  False -> false
   | Not alpha -> not (solve alpha model)
   | Var var    -> lookup ~var model
   | And (alpha, beta) -> (solve alpha model ) && (solve beta model)
   | Or  (alpha, beta) -> (solve alpha model) || (solve beta model)
   | Implicates  (alpha, beta) -> (not (solve alpha model) ) || (solve beta model)
   | Equals (alpha, beta)  -> (solve alpha model) = (solve beta model)
   ;;

let find_vars formula= 
   (* get a list of all variables *)
   let rec find formula =
      match formula with
         Var alpha -> [alpha]
      | Not alpha -> find alpha
      | And (alpha,beta) -> (find alpha)  @ (find beta)
      | Or (alpha,beta) -> (find alpha) @ (find beta)
      | Implicates (alpha,beta) -> (find alpha) @ (find beta)
      | Equals (alpha,beta) -> (find alpha) @ (find beta)
      | True  -> []
      | False  -> []
   in
   let vars = find formula in
   (* eliminate duplicates *)
   let rec eliminate vars = 
         match vars with
            var :: vars ->
                  if List.exists (fun a -> a=var) vars then
                     eliminate vars
                  else
                     var :: (eliminate vars)
         |  [] -> []
   in 
   eliminate vars
   ;;

let print_bool b = if b then print_string "true" else print_string "false";;

let print_model m = 
   print_string "[\n";
   let rec printer m =
      match m with 
         (a,assig) :: rest ->
               print_string "    ";
               print_string a;
               print_string "=";
               print_bool assig;
               print_string "\n";
               printer rest
         |  [] -> ()
   in
   printer m;
   print_endline "]"
   ;;

let is_solvable formula =
   (* get all the variables*)
   let vars = find_vars formula in
   (* functions for the search using the uninf_search part of this lib *)
   (* Nodes of the search space are represented as a tuple of the unbound variables
   and a model containing the bindings for the bound ones*)
   let childgen incomplete =
      (* see if we can bind a variable *)
      match incomplete with
         (*bind it to true and false and remove it from the list of unbound vars *)
         (var :: vars , model) -> [(vars, assign ~var true model);
                                               (vars, assign ~var false model)]
      | ([], _) -> [];
   and
      goaltest incomplete =
         (* as long as there are unbound variables we cannot have a solution *)
         match incomplete with
            ([], model) -> solve formula model
         | _ -> false
   and 
      combinator a b c = 
         (*just see if we have a solution and return the bindings in that case *)
         if b then 
         (
            let (_,res) = a in
            Some res
          )
         else
            c
   in
   let  res = Uninf_search.dfsearch ~start:(vars,empty) ~childgen ~goaltest ~combinator in 
   res
   ;;
   
let find_models formula =
   (* get all the variables*)
   let vars = find_vars formula in
   (* functions for the search using the uninf_search part of this lib *)
   (* Nodes of the search space are represented as a tuple of the unbound variables
   and a model containing the bindings for the bound ones*)
   let childgen incomplete =
      (* see if we can bind a variable *)
      match incomplete with
         (*bind it to true and false and remove it from the list of unbound vars *)
         (var :: vars , model) -> [(vars, assign ~var true model);
                                               (vars, assign ~var false model)]
      | ([], _) -> [];
   and
      goaltest incomplete =
         (* as long as there are unbound variables we cannot have a solution *)
         match incomplete with
            ([], model) -> solve formula model
         | _ -> false
   and 
      combinator a b c = 
         (*just see if we have a solution and return the bindings in that case *)
         if b then 
         (
            let (_,res) = a in
            Some res
          )
         else
            c
   in
   let  res = Uninf_search.exhaustive_search ~start:(vars,empty) ~childgen ~goaltest ~combinator in 
   res
   ;;   
   
(* 
 * $Log$
 * Revision 1.8  2007/12/15 18:52:58  till_crueger
 * - Updated documentation
 * - Moved Log-Tags to a better position in the sources
 *
 * Revision 1.7  2006/03/26 17:58:24  till_crueger
 * Major code cleanup and improvment of the documentation.
 *
 * Revision 1.6  2006/02/22 18:13:27  till
 * Changed several filenames
 *
 * Revision 1.5  2006/02/20 20:21:46  till
 * Added LGPL to all files
 * Added LGPL to package
 *
 * Revision 1.4  2006/02/20 17:36:01  till
 * Improved Makefile
 *
 * Fixed some minor problems so they won't cause warnings
 *
 * Revision 1.3  2006/02/11 11:17:33  till
 * removed example to seperate file
 *
 * Revision 1.2  2006/02/11 11:11:12  till
 * Added CVS Tags
 *
 *)