#use "boolean.ml";;
#use "testUtils.ml";;

(* Helper functions *)

let print_assignment_pair (c,b) = print_string 
	( "(" ^ (Char.escaped c) ^ "," ^ (string_of_bool b) ^ ") " )
;;

let rec prt_assignment x = match x with
        [] -> print_endline ""
	| h::t -> (print_assignment_pair h) ; prt_assignment t
;;

let test_sat f = match (sat f) with
        None -> "None"
        | Some a -> print_string "% " ; prt_assignment a ; "SAT" 
;;

(* Test vars_of *)

let f1 = True ;;
let f2 = And (True, False) ;;
let f3 = Var 'x';;
let f4 = Exists('x', Or(Var 'x', Var 'y')) ;;

prt_char_list_sorted (vars_of f1) ;;
prt_char_list_sorted (vars_of f2) ;;
prt_char_list_sorted (vars_of f3) ;;
prt_char_list_sorted (vars_of f4) ;;

(* Test sat *)

let f1 = And (True, True) ;;
let f2 = And (True, False) ;;
let f3 = Var 'x' ;;
let f4 = Or(Var 'x', Var 'y') ;;
let f5 = And(Var 'x', Not (Var 'x')) ;;

print_endline (test_sat f1);;
print_endline (test_sat f2);;
print_endline (test_sat f3);;
print_endline (test_sat f4);;
print_endline (test_sat f5);;