(* CMSC 330 Project - Boolean Formulae & SAT *)

(* NAME: *)

(* To load this file into the OCaml interpreter, type

   #use "boolean.ml"

   at the OCaml prompt
*)

type formula =
    False
  | True
  | Var of char
  | And of formula * formula
  | Or of formula * formula
  | Not of formula
  | Forall of char * formula
  | Exists of char * formula

type assignment = (char * bool) list

type vec = formula list

(*----------------------------------------------------------
  function f_to_str : formula -> string. 

	converts formula into a string 
*)

let rec f_to_str f = match f with
    False -> "F"
  | True -> "T"
  | Var x -> Char.escaped x
  | And (f1,f2) -> "(" ^ (f_to_str f1) ^ " && " ^ (f_to_str f2) ^ ")"
  | Or (f1,f2) -> "(" ^ (f_to_str f1) ^ " || " ^ (f_to_str f2) ^ ")"
  | Not f1 -> "(! " ^ (f_to_str f1) ^ ")"
  | Forall (x,f1) -> "(forall " ^ (Char.escaped x) ^ " : " ^ (f_to_str f1) ^ ")"
  | Exists (x,f1) -> "(exists " ^ (Char.escaped x) ^ " : " ^ (f_to_str f1) ^ ")"
;;

(*  YOUR CODE PAST THIS POINT *)


(*----------------------------------------------------------
  function count_assoc : assignment char -> int. 

	Counts the number of times an association appears 
	for some symbol x in the assignment. 

	count_assoc [('a',true);('a',false)] 'a' returns 2.
*)

let count_assoc lst x = 
	0
;;

(*----------------------------------------------------------
  function remove_assoc_all: assignment char -> assignment. 

	Removes all associations for some symbol x in the assignment. 

	remove_assoc_all [('a',true);('b',true);('a',false)] 'a'
	returns [('b',true)].
*)

let remove_assoc_all lst x = 
	[]
;;

(*----------------------------------------------------------
  function change_assoc_all: assignment char bool -> assignment. 

	Changes all associations for some symbol x in the 
	assignment to the specified boolean value. 

	change_assoc_all [('a',true);('a',false)] 'a' true
	returns [('a',true);('a',true)].
*)

let change_assoc_all lst x y = 
	[]
;;

(*----------------------------------------------------------
  function assoc_last: assignment char -> bool. 

	Returns the value bound to the last association 
	for some symbol x in the assignment. 

	assoc_last [('a',true);('a',false)] 'a' returns false. 
*)

let assoc_last lst x = 
	false
;;

(*----------------------------------------------------------
  function eval : formula -> assignment -> bool. 

	evaluates the boolean formula on the given variable assignment 
	returns the result as an OCaml bool. 
*)

let rec eval f e = match f with 
    False -> false
  | True -> false
  | Var x -> false
  | And (f1,f2) -> false
  | Or (f1,f2) -> false
  | Not f1 -> false
  | Forall (x,f1) -> false
  | Exists (x,f1) -> false
;;

(*----------------------------------------------------------
  function vars_of : formula -> char list. 

	takes a formula and returns a list of the names of the 
	free variables of the formula. 
*)

let vars_of x = 
	[]
;;

(*----------------------------------------------------------
  function sat : formula -> assignment option. 

	function returns Some a, where a is a satisfying assignment, 
	if the formula is satisfiable, or None otherwise. 
*)

let sat x = 
	None
;;

(*----------------------------------------------------------
  function int_of_vec : vec -> int. 

	takes a vec composed solely of Trues and Falses 
	returns the integer equivalent. 
*)

let int_of_vec x = 
	0
;;

(*----------------------------------------------------------
  function vec_of_int : int -> vec. 

	takes a non-negative integer 
	returns the corresponding vec. 
*)

let vec_of_int x = 
	[]
;;

(*----------------------------------------------------------
  function subst : assignment -> vec -> vec. 

	reduces the vec argument to a vec of all Trues and Falses 
	by replacing the variables in the vec according to the 
	assignment and then evaluating each bit. 
*)

let subst x y = 
	[]
;;

(*----------------------------------------------------------
  function eq : vec -> vec -> formula. 

	returns a formula representing whether the two bit vectors are equal. 
*)

let eq x y =
	(True)
;;

(*----------------------------------------------------------
  function add : vec -> vec -> vec. 

	returns a new vec representing the sum of the two vectors. 
*)

let add x y =
	[]
;;

(*----------------------------------------------------------
  function pad : vec -> int -> vec. 

	pad v i returns a new vec that is equal to v 
	but whose length is the greater of i and the length of v. 
*)

let pad x y =
	[]
;;

(*----------------------------------------------------------
  function add_three : vec -> vec -> vec -> vec. 

	returns a new vector that represents the sum of 
	the three input vectors. 
*)

let add_three x y z =
	[]
;;

(*----------------------------------------------------------
  function is_digit : vec -> formula. 

	input is a vec of length 4 (i.e., exactly 4 boolean formulae). 

	returns a formula that is true if and only if the vec is 
	greater than or equal to 1 and less than or equal to 9.
*)

let is_digit x =
	True	
;;

(*----------------------------------------------------------
  function disjoint : vec list -> formula. 

	takes a list of vecs and returns a formula representing whether 
	all the vecs are different from each other.
*)

let disjoint x =
	True	
;;

(*----------------------------------------------------------
  function is_magic : vec list -> formula. 

	takes a list of exactly nine vecs and returns a formula 
	representing whether the list is a magic square. 
*)

let is_magic x =
	True	
;;