finite-model.ml

type variable = string

type formula =
   Equal of variable * variable
 | Epsilon of variable * variable
 | Imply of formula * formula
 | Not of formula
 | And of formula * formula
 | Or of formula * formula
 | Forall of variable * formula
 | Exists of variable * formula

type model = int * ((int list) list)

type assignment = (string, int) Hashtbl.t

let rec formula_to_str = function
   Equal (var1, var2) -> "(" ^ var1 ^ " = " ^ var2 ^ ")"
 | Epsilon (var1, var2) -> "(" ^ var1 ^ " in " ^ var2 ^ ")"
 | Imply (fml1, fml2) -> "(" ^ (formula_to_str fml1) ^ " -> " ^ (formula_to_str fml2) ^ ")"
 | Not fml -> "~(" ^ (formula_to_str fml) ^ ")"
 | And (fml1, fml2) -> "(" ^ (formula_to_str fml1) ^ " & " ^ (formula_to_str fml2) ^ ")"
 | Or (fml1, fml2) -> "(" ^ (formula_to_str fml1) ^ " | " ^ (formula_to_str fml2) ^ ")"
 | Forall (var, fml) -> "(forall " ^ var ^ ")" ^ (formula_to_str fml)
 | Exists (var, fml) -> "(exists " ^ var ^ ")" ^ (formula_to_str fml);;

let subst asgn var value =
  (let asgn' = Hashtbl.copy asgn in
    Hashtbl.add asgn' var value; asgn');;

let rec forall n fn = 
  if n == 0 then true
  else (fn (n-1)) && (forall (n-1) fn);;

let rec satisfies mdl fml asgn =
  let (numelems, graph) = mdl in
  match fml with
   Equal (var1, var2) -> (Hashtbl.find asgn var1) == (Hashtbl.find asgn var2)
 | Epsilon (var1, var2) ->
      let a = (Hashtbl.find asgn var1) in
      let b = (Hashtbl.find asgn var2) in
      List.nth (List.nth graph b) a
 | Imply (fml1, fml2) -> (not (satisfies mdl fml1 asgn)) || (satisfies mdl fml2 asgn)
 | Not fml -> not (satisfies mdl fml asgn)
 | And (fml1, fml2) -> (satisfies mdl fml1 asgn) && (satisfies mdl fml2 asgn)
 | Or (fml1, fml2) -> (satisfies mdl fml1 asgn) || (satisfies mdl fml2 asgn)
 | Forall (var, fml) -> 
      forall numelems (fun x -> satisfies mdl fml (subst asgn var x))
 | Exists (var, fml) -> 
      not (forall numelems (fun x -> not (satisfies mdl fml (subst asgn var x))));;

let fml = (Epsilon ("y", "x")) in
let mdl = (2, [[false; false]; [true; false]]) in
let asgn = Hashtbl.create 0 in
Hashtbl.add asgn "x" 0;
Hashtbl.add asgn "y" 1;
print_string (if (satisfies mdl fml asgn) then "true" else "false");
print_newline ()