(* **************************************************
    Manipulation of first-order formulas
    in the language of boolean algebras. 
   ************************************************** *)

let optimize_formulas = ref true
let no_mona = ref false

exception Internal of string

type ident = string
type bVarDecl = ident * Types.value_type 
               (* (var,type) *)

type sets_and_bools = {
    s : ident list;
    b : ident list;
  }

type form = 
  | Atom of atomForm
  | Not of form
  | And of form list
  | Or of form list
  | Impl of form * form
  | Iff of form * form
  | ExistsOne of (bVarDecl list) * form
  | ForallOne of (bVarDecl list) * form
  | ExistsSet of (bVarDecl list) * form
  | ForallSet of (bVarDecl list) * form
  | ExistsProp of (ident list) * form
  | ForallProp of (ident list) * form

and atomForm = 
    Eq of setExp * setExp
  | Neq of setExp * setExp
  | Sub of setExp * setExp
  | True
  | False
  | Cardeq of setExp * int
  | Cardleq of setExp * int
  | Cardgeq of setExp * int
  | Disjoint of setExp list
  | Propvar of ident

and setExp =
    Var of ident
  | Emptyset
  | Union of setExp list
  | Inter of setExp list
  | Diff of setExp * setExp

let toString (f:form) : string = "<baformula>"

let rec count_size (f:form) =
  let rec count_atom_size (af:atomForm) =
    let rec count_setexp_size (se:setExp) =
      match se with
      | Var _ | Emptyset -> 1
      | Union sel | Inter sel -> 
          List.fold_right (fun x y -> (count_setexp_size x) + y) sel 1
      | Diff (l, r) -> 1 + count_setexp_size l + count_setexp_size r in
    match af with
    | Eq (l, r) | Neq (l, r) | Sub (l, r) -> 
        1 + count_setexp_size l + count_setexp_size r
    | True | False | Propvar _ -> 1
    | Cardeq (se, _) | Cardleq (se, _) | Cardgeq (se, _) -> 1 + count_setexp_size se
    | Disjoint sel -> List.fold_right (fun x y -> (count_setexp_size x) + y) sel 1 in
  match f with
  | Atom af -> 1 + count_atom_size af
  | Not nf -> 1 + count_size nf
  | And cs | Or cs -> List.fold_right (fun x y -> (count_size x) + y) cs 1
  | Impl (f1, f2) | Iff (f1, f2) -> 1 + count_size f1 + count_size f2
  | ExistsOne (vs, f') | ForallOne (vs, f') 
  | ExistsSet (vs, f') | ForallSet (vs, f') -> 
      1 + List.length vs + count_size f'
  | ExistsProp (vs, f') | ForallProp (vs, f') -> 
      1 + List.length vs + count_size f'

(*************************************)
(* Printing formulas to Mona strings *)
(*************************************)

let wrap (s:string) : string =
  let margin = 60 in
  let eol = '\n' in
  let isBreakable ch = (ch=' ') in
  let res = String.copy s in
  let rec rpl pos =
    if pos < String.length res then
      if isBreakable res.[pos] then
        (String.set res pos eol;
         rpl (pos + margin))
      else rpl (pos+1)
    else res
  in rpl 0

  let strNot   = "~ "
  let strAnd   = " & "
  let strOr    = " | "
  let strImpl  = " => "
  let strIff   = " <=> "
  let strForallOne = "all1 "
  let strForallSet = "all2 "
  let strExistsOne = "ex1 "
  let strExistsSet = "ex2 "
  let strExistsProp = "ex0 "
  let strForallProp = "all0 "
  let qbody = ": "
  let strEq = " = "
  let strNeq = " ~= "
  let strSub = " sub "
  let strTrue = "true"
  let strFalse = "false"
  let strEmptyset = "empty"
  let strUnion = " union "
  let strInter = " inter "
  let strDiff = " \\ "
  let strCardgeq = "cardGeq"
  let strCardeq = "cardEq"
  let strCardleq = "cardLeq"
  let strDisjoint = "disjoint"
  let strComma = ", "

  let mkCardgeq k = strCardgeq ^ (Format.sprintf "%d" k)
  let mkCardeq k = strCardeq ^ (Format.sprintf "%d" k)
  let mkCardleq k = strCardleq ^ (Format.sprintf "%d" k)
  let mkDisjoint k = strDisjoint ^ (Format.sprintf "%d" k)

  (* Print BA Formula *)
  let rec 
    p_form f = match f with  
      Atom af -> p_atomForm af
    | Not f1  -> strNot ^ pp_form f1
    | And fl  -> (match fl with
      | [] -> strTrue
      | _ -> p_form_list strAnd fl)
    | Or fl   -> (match fl with
      | [] -> strFalse
      | _ -> p_form_list strOr fl)
    | Impl (f1,f2) -> pp_form f1 ^ strImpl ^ pp_form f2
    | Iff (f1,f2)  -> pp_form f1 ^ strIff ^ pp_form f2
    | ForallOne (xts, f') -> p_quant (pp_quant strForallOne) xts f'
    | ForallSet (xts, f') -> p_quant (pp_quant strForallSet) xts f'
    | ExistsOne (xts, f') -> p_quant (pp_quant strExistsOne) xts f'
    | ExistsSet (xts, f') -> p_quant (pp_quant strExistsSet) xts f'
    | ExistsProp (vs, f') -> p_quantp (pp_quantp strExistsProp) vs f'
    | ForallProp (vs, f') -> p_quantp (pp_quantp strForallProp) vs f'
  and p_quant q xts f = 
    (match f with
    | ForallOne _ | ForallSet _ | ExistsOne _ 
    | ExistsSet _ -> 
        String.concat "" (List.map q xts) ^ p_form f
    | _ -> 
        String.concat "" (List.map q xts) ^ pp_form f)
  and p_quantp q vs f = 
    (match f with
    | ExistsProp _ | ForallProp _ -> 
        String.concat "" (List.map q vs) ^ p_form f
    | _ -> 
        String.concat "" (List.map q vs) ^ pp_form f)
  and
    pp_quant s (x,t) = s ^ x ^ qbody
  and
    pp_quantp s x = s ^ x ^ qbody
  and
    pp_form f = "(" ^ p_form f ^ ")"
  and
    p_form_list op fl = match fl with
      []    -> raise (Internal "empty list in p_form_list")
    | [f]   -> pp_form f
    | f::fs -> pp_form f ^ op ^ p_form_list op fs   
  and
    p_atomForm af = match af with
      Eq (s1,s2) -> p_setExp s1 ^ strEq ^ p_setExp s2
    | Neq (s1,s2) -> p_setExp s1 ^ strNeq ^ p_setExp s2
    | Sub (s1,s2) -> p_setExp s1 ^ strSub ^ p_setExp s2
    | True -> strTrue
    | False -> strFalse
    | Cardgeq (s,k) -> mkCardgeq k ^ pp_setExp s
    | Cardeq (s,k) -> mkCardeq k ^ pp_setExp s
    | Cardleq (s,k) -> mkCardleq k ^ pp_setExp s
    | Disjoint ss -> mkDisjoint (List.length ss) ^ "(" ^ p_setExp_list strComma ss ^ ")"
    | Propvar v -> v
  and
    p_setExp s = match s with
      Var id -> id
    | Emptyset -> strEmptyset
    | Union ss -> p_setExp_list strUnion ss
    | Inter ss -> p_setExp_list strInter ss
    | Diff (s1,s2) -> pp_setExp s1 ^ strDiff ^ pp_setExp s2
  and
    pp_setExp s = "(" ^ p_setExp s ^ ")"
  and
    p_setExp_list op ss = match ss with
      [] -> raise (Internal "empty list in p_setExp_list")
    | [s] -> pp_setExp s
    | s::ss -> pp_setExp s ^ op ^ p_setExp_list op ss

(* **************************************************
           Free variables of a formula
   ************************************************** *)

let rec remove_vars bvs vs = match vs with
| [] -> []
| v::vs1 -> 
    if (List.mem v bvs) then remove_vars bvs vs1
    else v :: remove_vars bvs vs1

let rec fv f : sets_and_bools = 
  fv1 f { s = []; b = [] } { s = []; b = [] }
and add_bool v bv0 acc = 
  if (List.mem v bv0.b) || (List.mem v acc.b) 
  then acc 
  else { s = acc.s; b = v::acc.b }
and add_set v bv0 acc = 
  if (List.mem v bv0.s) || (List.mem v acc.s) 
  then acc 
  else { s = v::acc.s; b = acc.b; }
and fv1 (f:form) (bv0:sets_and_bools) (acc:sets_and_bools) 
    : sets_and_bools = 
  match f with
  | Atom af -> atom_fv af bv0 acc
  | Not f1 -> fv1 f1 bv0 acc
  | And fs -> fv_list fs bv0 acc
  | Or fs -> fv_list fs bv0 acc
  | Impl (f1,f2) -> fv1 f1 bv0 (fv1 f2 bv0 acc)
  | Iff (f1,f2) -> fv1 f1 bv0 (fv1 f2 bv0 acc)
  | ExistsOne (bvts,f1)
  | ForallOne (bvts,f1)
  | ExistsSet (bvts,f1)
  | ForallSet (bvts,f1) -> 
      fv1 f1 { s = (List.rev_append (List.map fst bvts) bv0.s); b = bv0.b } acc
  | ExistsProp (bvs,f1) 
  | ForallProp (bvs,f1) -> 
      fv1 f1 { s = bv0.s; b = (List.rev_append bvs bv0.b) } acc
and fv_list fs bv0 acc = 
  match fs with
  | [] -> acc
  | f::fs1 -> fv_list fs1 bv0 (fv1 f bv0 acc)
and atom_fv af bv0 acc = 
  match af with
  | Eq (s1,s2) -> exp_fv s1 bv0 (exp_fv s2 bv0 acc)
  | Neq (s1,s2) -> exp_fv s1 bv0 (exp_fv s2 bv0 acc)
  | Sub (s1,s2) -> exp_fv s1 bv0 (exp_fv s2 bv0 acc)
  | True -> acc
  | False -> acc
  | Cardeq (s,_) -> exp_fv s bv0 acc
  | Cardleq (s,_) -> exp_fv s bv0 acc
  | Cardgeq (s,_) -> exp_fv s bv0 acc
  | Disjoint ss -> exp_fv_list ss bv0 acc
  | Propvar id -> add_bool id bv0 acc
and exp_fv s bv0 acc =
  match s with
  | Var s -> add_set s bv0 acc
  | Emptyset -> acc
  | Union ss -> exp_fv_list ss bv0 acc
  | Inter ss -> exp_fv_list ss bv0 acc
  | Diff (s1,s2) -> exp_fv s1 bv0 (exp_fv s2 bv0 acc)
and exp_fv_list ss bv0 acc = 
  match ss with
  | [] -> acc
  | s::ss1 -> exp_fv_list ss1 bv0 (exp_fv s bv0 acc)

(* **************************************************
   Smart Constructors
 ************************************************** *)

let mk_eq(s1,s2) = if (s1=s2) then Atom True else Atom (Eq(s1,s2))
let mk_neq(s1,s2) = if (s1=s2) then Atom False else Atom (Neq(s1,s2))

let mk_not f = match f with
| Atom False -> Atom True
| Atom True -> Atom False
| Atom (Eq(s1,s2)) -> Atom (Neq(s1,s2))
| Atom (Neq(s1,s2)) -> Atom (Eq(s1,s2))
| Not f1 -> f1
| f1 -> Not f1

let mk_iff(f1,f2) = if f1=f2 then Atom True else Iff(f1,f2)

let mk_impl(f1,f2) = match (f1,f2) with
| (Atom True,f2) -> f2
| (Atom False,f2) -> Atom True
| (f1,Atom False) -> mk_not f1
| (f1,Atom True) -> Atom True
| _ -> Impl(f1,f2)

let mk_sub(s1,s2) = Atom (Sub(s1,s2))

let mk_and fs = 
  let set_insert x xs = if List.mem x xs then xs else x::xs in
  let rec mkand1 fs acc = match fs with
  | [] -> (match acc with
    | [] -> Atom True
    | [f] -> f
    | _ -> And acc)
  | And fs0 :: fs1 -> mkand1 (List.rev_append fs0 fs1) acc
  | Atom True::fs1 -> mkand1 fs1 acc
  | Atom False::fs1 -> Atom False
  | fs::fs1 -> mkand1 fs1 (set_insert fs acc)
in mkand1 fs []
        
let mk_or fs = 
  let set_insert x xs = if List.mem x xs then xs else x::xs in
  let rec mkor1 fs acc = match fs with
  | [] -> (match acc with
    | [] -> Atom False
    | [f] -> f
    | _ -> Or acc)
  | Or fs0 :: fs1 -> mkor1 (List.rev_append fs0 fs1) acc
  | Atom False::fs1 -> mkor1 fs1 acc
  | Atom True::fs1 -> Atom True
  | fs::fs1 -> mkor1 fs1 (set_insert fs acc)
in mkor1 fs []

let mk_optimized_or (fs : form list) =
  match fs with
  | [And ll; And rl] ->
      let i = Util.intersect ll rl in
      mk_and ((mk_or [mk_and (Util.difference ll i); 
                      mk_and (Util.difference rl i)])::i)
  | _ -> mk_or fs

(*****************************************)
(* Does a variable occur in a formula    *)
(*****************************************)

let rec occurs v f = match f with  
| Atom a -> a_occurs v a
| Not f' -> occurs v f'
| And fs -> list_occurs v fs
| Or fs -> list_occurs v fs
| Impl (f1,f2) -> occurs v f1 || occurs v f2
| Iff (f1,f2) -> occurs v f1 || occurs v f2      
| ExistsOne (vts,f') -> 
    not (List.mem v (List.map fst vts)) &&
    occurs v f'
| ForallOne (vts,f') ->
    not (List.mem v (List.map fst vts)) &&
    occurs v f'
| ExistsSet (vts,f') ->
    not (List.mem v (List.map fst vts)) &&
    occurs v f'
| ForallSet (vts,f') ->
    not (List.mem v (List.map fst vts)) &&
    occurs v f'
| ExistsProp (vs,f') ->
    not (List.mem v vs) &&
    occurs v f'
| ForallProp (vs,f') ->
    not (List.mem v vs) &&
    occurs v f'
and
    list_occurs v fs = match fs with
    | [] -> false
    | f::fs' -> (occurs v f) || (list_occurs v fs')
and
    a_occurs v f = match f with
    | Eq (s1,s2) -> s_occurs v s1 || s_occurs v s2
    | Neq (s1,s2) -> s_occurs v s1 || s_occurs v s2
    | Sub (s1,s2) -> s_occurs v s1 || s_occurs v s2
    | True -> false
    | False -> false
    | Cardeq (s,i) -> s_occurs v s
    | Cardleq (s,i) -> s_occurs v s
    | Cardgeq (s,i) -> s_occurs v s
    | Disjoint ss -> list_s_occurs v ss
    | Propvar v' -> (v=v')
and
    list_s_occurs v ss = match ss with
    | [] -> false
    | s::ss' -> s_occurs v s || list_s_occurs v ss'
and
    s_occurs v s = match s with
    | Var v' -> (v=v')
    | Emptyset -> false
    | Union ss -> list_s_occurs v ss
    | Inter ss -> list_s_occurs v ss
    | Diff (s1,s2) -> s_occurs v s1 || s_occurs v s2

let mk_existsProp ((ids,f) : ident list * form) : form =
  let fvs = (fv f).b in
  let useful_vars = Util.intersect fvs ids in
  if (useful_vars = []) then f else ExistsProp(useful_vars,f)

let mk_forallProp ((ids,f) : ident list * form) : form =
  let fvs = (fv f).b in
  let useful_vars = Util.intersect fvs ids in
  if (useful_vars = []) then f else ForallProp(useful_vars,f)

let mk_existsSet((vts,f) : bVarDecl list * form) : form =
  let fvs = (fv f).s in
  let useful_vars = List.filter (fun (v,t) -> List.mem v fvs) vts in
  if (useful_vars = []) then f else ExistsSet(useful_vars,f)

let mk_forallSet((vts,f) : bVarDecl list * form) : form =
  let fvs = (fv f).s in
  let useful_vars = List.filter (fun (v,t) -> List.mem v fvs) vts in
  if (useful_vars = []) then f else ForallSet(useful_vars,f)

let mk_forallSetId((vs,f) : string list * form) : form =
  mk_forallSet(List.map (fun v -> (v,Types.TObj "")) vs,f)

(* **************************************************
           Set variable substitution
   ************************************************** *)
(* replace `Var x' by `y' in form *)
let rec subst (tbl:(Id.var_t * setExp) list) form =
  let remove_from_tbl vs = 
    List.filter (fun (x,y) -> not (List.mem x vs)) tbl in
  let remove_from_tbl_t vts = 
    remove_from_tbl (List.map fst vts) in
  let rec subst_setexp s =
    match s with
    | Var i when List.mem_assoc i tbl -> List.assoc i tbl
    | Union sel -> Union (List.map subst_setexp sel)
    | Inter sel -> Inter (List.map subst_setexp sel)
    | Diff (l, r) -> Diff (subst_setexp l, subst_setexp r)
    | _ -> s in
  let subst_atom a =
    match a with
    | Eq (l, r) -> Eq (subst_setexp l, subst_setexp r)
    | Neq (l, r) -> Neq (subst_setexp l, subst_setexp r)
    | Sub (l, r) -> Sub (subst_setexp l, subst_setexp r)
    | Cardeq (se, i) -> Cardeq (subst_setexp se, i)
    | Cardleq (se, i) -> Cardleq (subst_setexp se, i)
    | Cardgeq (se, i) -> Cardgeq (subst_setexp se, i)
    | Disjoint sel -> Disjoint (List.map subst_setexp sel) 
    | True | False | Propvar _ -> a in
  let rec subst_form f =
    match f with
    | Atom af -> Atom (subst_atom af)
    | Not nf -> Not (subst_form nf)
    | And fl -> mk_and (List.map subst_form fl)
    | Or fl -> Or (List.map subst_form fl)
    | Impl (p, c) -> Impl (subst_form p, subst_form c)
    | Iff (p, c) -> Iff (subst_form p, subst_form c)
    | ExistsOne (vts, f) -> 
        ExistsOne (vts, subst (remove_from_tbl_t vts) f)
    | ForallOne (vts, f) -> 
        ForallOne (vts, subst (remove_from_tbl_t vts) f)
    | ExistsSet (vts, f) -> 
        mk_existsSet (vts, subst (remove_from_tbl_t vts) f)
    | ForallSet (vts, f) -> 
        ForallSet (vts, subst (remove_from_tbl_t vts) f)
    | ExistsProp (vs, f) -> 
        mk_existsProp (vs, subst (remove_from_tbl vs) f)
    | ForallProp (vs, f) -> 
        ForallProp (vs, subst (remove_from_tbl vs) f)
  in
  subst_form form

(* **************************************************
           Propositional variable substitution
   ************************************************** *)

(* replace `Propvar x' by `y' in form *)
let rec subst_propvar (tbl:(Id.var_t * atomForm) list) form =
  let remove_from_tbl vs = 
    List.filter (fun (x,y) -> not (List.mem x vs)) tbl in
  let remove_from_tbl_t vts = 
    remove_from_tbl (List.map fst vts) in
  let subst_pv_atom a =
    match a with
    | Propvar v when List.mem_assoc v tbl -> List.assoc v tbl
    | _ -> a in
  let rec subst_pv_form f =
    match f with
    | Atom af -> Atom (subst_pv_atom af)
    | Not nf -> Not (subst_pv_form nf)
    | And fl -> mk_and (List.map subst_pv_form fl)
    | Or fl -> Or (List.map subst_pv_form fl)
    | Impl (p, c) -> Impl (subst_pv_form p, subst_pv_form c)
    | Iff (p, c) -> Iff (subst_pv_form p, subst_pv_form c)
    | ExistsOne (vts, f) -> 
        ExistsOne (vts, subst_propvar (remove_from_tbl_t vts) f)
    | ForallOne (vts, f) -> 
        ForallOne (vts, subst_propvar (remove_from_tbl_t vts) f)
    | ExistsSet (vts, f) -> 
        mk_existsSet (vts, subst_propvar (remove_from_tbl_t vts) f)
    | ForallSet (vts, f) -> 
        ForallSet (vts, subst_propvar (remove_from_tbl_t vts) f)
    | ExistsProp (vs, f) -> 
        mk_existsProp (vs, subst_propvar (remove_from_tbl vs) f)
    | ForallProp (vs, f) -> 
        ForallProp (vs, subst_propvar (remove_from_tbl vs) f)
  in
  subst_pv_form form

(* **************************************************
     Nesting quantifiers to reduce their scope
   ************************************************** *)

let dummy_type = Types.TObj "T" (* we currently ignore types *)

let it_all_be v f = ForallSet ([(v,dummy_type)],f)
let it_exist_be v f = ExistsSet ([(v,dummy_type)],f)

let it_all_prop_be v f = ForallProp ([v],f)
let it_exist_prop_be v f = ExistsProp ([v],f)

let rec exist_quant (v : ident) f = 
  match f with
  | Atom _ -> it_exist_be v f
  | Not f' -> Not (all_quant v f')
  | And fs -> 
      let (ins,outs) = List.partition (fun f0 -> occurs v f0) fs in
      let qins = (match ins with
      | [] -> Atom True
      | [f0] -> exist_quant v f0
      | _ -> it_exist_be v (mk_and ins)) in
      mk_and [qins; mk_and outs]
  | Or fs -> 
      let (ins,outs) = List.partition (fun f0 -> occurs v f0) fs in
      let qins = (match ins with
      | [] -> Atom False
      | [f0] -> exist_quant v f0
      | _ -> it_exist_be v (Or ins)) in
      mk_or [qins; mk_or outs]
  | Impl (f1,f2) -> 
      if (occurs v f1) then
        (if (occurs v f2) then it_exist_be v f
        else Impl (all_quant v f1, f2))
      else
        Impl (f1, exist_quant v f2)
  | Iff _ -> it_exist_be v f
  | ExistsOne (vts,f') -> ExistsOne (vts,exist_quant v f')
  | ForallOne _ -> it_exist_be v f
  | ExistsSet (vts,f') -> mk_existsSet (vts,exist_quant v f')
  | ForallSet _ -> it_exist_be v f  
  | ExistsProp (vs,f') -> mk_existsProp (vs,exist_quant v f')
  | ForallProp _ -> it_exist_be v f  
and all_quant v f = 
  match f with
  | Atom _ -> it_all_be v f
  | Not f' -> Not (exist_quant v f')
  | And fs -> 
      let (ins,outs) = List.partition (fun f0 -> occurs v f0) fs in
      let qins = (match ins with
      | [] -> Atom True
      | [f0] -> all_quant v f0
      | _ -> it_all_be v (mk_and ins)) in
      mk_and [qins; mk_and outs]
  | Or fs -> 
      let (ins,outs) = List.partition (fun f0 -> occurs v f0) fs in
      let qins = (match ins with
      | [] -> Atom False
      | [f0] -> all_quant v f0
      | _ -> it_all_be v (Or ins)) in
      mk_or [qins; mk_or outs]
  | Impl (f1,f2) -> 
      if (occurs v f1) then
        (if (occurs v f2) then it_all_be v f
        else Impl (exist_quant v f1, f2))
      else
        Impl (f1, all_quant v f2)
  | Iff _ -> it_all_be v f
  | ExistsOne _ -> it_all_be v f
  | ForallOne (vts,f') -> ForallOne (vts,all_quant v f')
  | ExistsSet _ -> it_all_be v f
  | ForallSet (vts,f') -> ForallSet (vts,all_quant v f')
  | ExistsProp _ -> it_all_be v f
  | ForallProp (vs,f') -> ForallProp (vs,all_quant v f')

let rec exist_prop_quant (v : ident) f = 
  match f with
  | Atom _ -> it_exist_prop_be v f
  | Not f' -> Not (all_prop_quant v f')
  | And fs -> 
      let (ins,outs) = List.partition (fun f0 -> occurs v f0) fs in
      let qins = (match ins with
      | [] -> Atom True
      | [f0] -> exist_prop_quant v f0
      | _ -> it_exist_prop_be v (mk_and ins)) in
      mk_and [qins; mk_and outs]
  | Or fs -> 
      let (ins,outs) = List.partition (fun f0 -> occurs v f0) fs in
      let qins = (match ins with
      | [] -> Atom False
      | [f0] -> exist_prop_quant v f0
      | _ -> it_exist_prop_be v (Or ins)) in
      mk_or [qins; mk_or outs]
  | Impl (f1,f2) -> 
      if (occurs v f1) then
        (if (occurs v f2) then it_exist_prop_be v f
        else Impl (all_prop_quant v f1, f2))
      else
        Impl (f1, exist_prop_quant v f2)
  | Iff _ -> it_exist_prop_be v f
  | ExistsOne (vts,f') -> ExistsOne (vts,exist_prop_quant v f')
  | ForallOne _ -> it_exist_prop_be v f
  | ExistsSet (vts,f') -> mk_existsSet (vts,exist_prop_quant v f')
  | ForallSet _ -> it_exist_prop_be v f 
  | ExistsProp (vs,f') -> mk_existsProp (vs,exist_prop_quant v f')
  | ForallProp _ -> it_exist_prop_be v f
and all_prop_quant v f = 
  match f with
  | Atom _ -> it_all_prop_be v f
  | Not f' -> Not (exist_prop_quant v f')
  | And fs -> 
      let (ins,outs) = List.partition (fun f0 -> occurs v f0) fs in
      let qins = (match ins with
      | [] -> Atom True
      | [f0] -> all_prop_quant v f0
      | _ -> it_all_prop_be v (mk_and ins)) in
      mk_and [qins; mk_and outs]
  | Or fs -> 
      let (ins,outs) = List.partition (fun f0 -> occurs v f0) fs in
      let qins = (match ins with
      | [] -> Atom False
      | [f0] -> all_prop_quant v f0
      | _ -> it_all_prop_be v (Or ins)) in
      mk_or [qins; mk_or outs]
  | Impl (f1,f2) -> 
      if (occurs v f1) then
        (if (occurs v f2) then it_all_prop_be v f
        else Impl (exist_prop_quant v f1, f2))
      else
        Impl (f1, all_prop_quant v f2)
  | Iff _ -> it_all_prop_be v f
  | ExistsOne _ -> it_all_prop_be v f
  | ForallOne (vts,f') -> ForallOne (vts,all_prop_quant v f')
  | ExistsSet _ -> it_all_prop_be v f
  | ForallSet (vts,f') -> ForallSet (vts,all_prop_quant v f')
  | ExistsProp _ -> it_all_prop_be v f
  | ForallProp (vs,f') -> ForallProp (vs,all_prop_quant v f')

and exist_quant' v f =
  if (occurs v f) then exist_quant v f else f
and all_quant' v f =
  if (occurs v f) then all_quant v f else f
and exist_prop_quant' v f =
  if (occurs v f) then exist_prop_quant v f else f
and all_prop_quant' v f =
  if (occurs v f) then all_prop_quant v f else f

let rec nest_quants (f : form) : form = 
  if (not !optimize_formulas) then 
    f
  else
    match f with
    | Atom f' -> Atom f'
    | Not f' -> Not (nest_quants f')
    | And fs -> mk_and (List.map nest_quants fs)
    | Or fs -> Or (List.map nest_quants fs)
    | Impl (f1,f2) -> Impl (nest_quants f1, nest_quants f2)
    | Iff (f1,f2) -> Iff (nest_quants f1, nest_quants f2)
    | ExistsOne (vts,f) -> ExistsOne (vts,nest_quants f)
    | ForallOne (vts,f) -> ForallOne (vts,nest_quants f)
    | ExistsProp (vs,f) ->
        let quant v f = exist_prop_quant' v f in
        List.fold_right quant vs (nest_quants f)
    | ForallProp (vs,f) ->
        let quant v f = all_prop_quant' v f in
        List.fold_right quant vs (nest_quants f)
    | ExistsSet (vts,f) -> 
        let quant (v,t) f = exist_quant' v f in
        List.fold_right quant vts (nest_quants f)
    | ForallSet (vts,f) -> 
        let quant (v,t) f = all_quant' v f in
        List.fold_right quant vts (nest_quants f)

(* Trivial Quantifier Elimination: exists x in S. x = E and F(x) => F(E) 
 * Also And/Or <singleton> => <singleton> 
 * Also tree-flattening of conjuncts And (And x y) z => And x y z *)

let rec flatten fs fs' = if not (!optimize_formulas) then 
  fs 
else
  match fs with
  | [] -> fs'
  | (Or [fs])::fsr -> flatten (fs::fsr) fs'
  | (And fs1)::fsr -> flatten (fs1 @ fsr) fs'
  | f::fsr -> 
      (*
         let _ = Util.msg ("\n CONJUNCT:" ^ MONA.form_to_mona f ^ "\n") in
       *)
   flatten fsr (f::fs')

(* **************************************************
        Primifier
   ************************************************** *)

let rec primify (f:form) = 
  let rec primify_setexp (fs:setExp) = 
    match fs with
    | Var id -> Var (id ^ (if not (Util.is_primed id) then "\'" else ""))
    | Emptyset -> fs
    | Union sel -> Union (List.map primify_setexp sel)
    | Inter sel -> Inter (List.map primify_setexp sel)
    | Diff (se1, se2) -> Diff (primify_setexp se1, primify_setexp se2) in
  let rec primify_atom (fa:atomForm) =
    match fa with
    | Eq (se1, se2) -> Eq (primify_setexp se1, primify_setexp se2)
    | Neq (se1, se2) -> Neq (primify_setexp se1, primify_setexp se2)
    | Sub (se1, se2) -> Sub (primify_setexp se1, primify_setexp se2)
    | True -> fa
    | False -> fa
    | Cardeq (se, i) -> Cardeq (primify_setexp se, i)
    | Cardleq (se, i) -> Cardleq (primify_setexp se, i)
    | Cardgeq (se, i) -> Cardgeq (primify_setexp se, i)
    | Disjoint sel -> Disjoint (List.map primify_setexp sel)
    | Propvar id -> 
        Propvar (id ^ (if not (Util.is_primed id) then "\'" else "")) in
  match f with
  | Atom af -> Atom (primify_atom af)
  | Not nf -> Not (primify nf)
  | And cs -> And (List.map primify cs)
  | Or ds -> Or (List.map primify ds)
  | Impl (a, p) -> Impl (primify a, primify p)
  | Iff (p1, p2) -> Iff (primify p1, primify p2)
  | ExistsOne (vts, f) -> ExistsOne (vts, primify f)
  | ForallOne (vts, f) -> ForallOne (vts, primify f)
  | ExistsSet (vts, f) -> ExistsSet (vts, primify f)
  | ForallSet (vts, f) -> ForallSet (vts, primify f)
  | ExistsProp (vts, f) -> ExistsProp (vts, primify f)
  | ForallProp (vts, f) -> ForallProp (vts, primify f)
  
(* **************************************************
        Simplifier
   ************************************************** *)

let rec simplify (f:form) = if not (!optimize_formulas) then
  f 
else 
  rebuild (rebuild f)
and rebuild f = match f with
| Atom a -> a_rebuild a
| Not f' -> Not (rebuild f')
| And fs -> mk_and (List.map rebuild fs)
| Or fs -> mk_optimized_or (List.map rebuild fs)
| Impl (f1,f2) -> mk_impl(rebuild f1, rebuild f2)
| Iff (f1,f2) -> mk_iff(rebuild f1, rebuild f2)
| ExistsOne (vts,f') -> ExistsOne (vts,rebuild f')
| ForallOne (vts,f') -> ForallOne (vts,rebuild f')
| ExistsSet (vts,f') -> simple_qe_exists_set (vts,rebuild f')
| ForallSet (vts,f') -> mk_forallSet (vts,rebuild f')
| ExistsProp (vs,f') -> simple_qe_exists_prop (vs,rebuild f')
| ForallProp (vs,f') -> mk_forallProp(vs,rebuild f')
and
    a_rebuild f = match f with
    | Eq (s1,s2) -> mk_eq(s_rebuild s1,s_rebuild s2)
    | Neq (s1,s2) -> mk_neq(s_rebuild s1,s_rebuild s2)
    | Sub (s1,s2) -> mk_sub(s_rebuild s1,s_rebuild s2)
    | True -> Atom True
    | False -> Atom False
    | Cardeq (s,i) -> Atom (Cardeq(s_rebuild s,i))
    | Cardleq (s,i) -> Atom (Cardleq(s_rebuild s,i))
    | Cardgeq (s,i) -> Atom (Cardgeq(s_rebuild s,i))
    | Disjoint ss -> Atom (Disjoint (List.map s_rebuild ss))
    | Propvar v' -> Atom f
and
    s_rebuild s = match s with
    | Var v' -> s
    | Emptyset -> s
    | Union ss -> Union (List.map s_rebuild ss)
    | Inter ss -> Inter (List.map s_rebuild ss)
    | Diff (s1,s2) -> Diff(s_rebuild s1, s_rebuild s2)
and    
    c_simple_qe_exists_set f = 
    (match f with
    | ExistsSet(vts,f1) -> simple_qe_exists_set(vts,f1)
    | ExistsProp(vs,f1) -> mk_existsProp(vs,c_simple_qe_exists_set f1)
    | _ -> f)
and 
    simple_qe_exists_set (vts,f) = match f with
    | And conjs -> 
        let (vts', conjs') = eliminate vts [] conjs in
        let (conjs'_with_vts, conjs'_without_vts) = 
          List.partition (fun f -> List.exists (fun (x, _) -> occurs x f) vts') conjs' in
        mk_and (mk_existsSet(vts', mk_and conjs'_with_vts) :: conjs'_without_vts)
    | ExistsProp(vs,f1) -> mk_existsProp(vs,simple_qe_exists_set(vts,f1))
    | _ -> mk_existsSet(vts,f)
and 
    c_simple_qe_exists_prop f =
    (match f with
    | ExistsProp(vs,f1) -> simple_qe_exists_prop(vs,f1)
    | ExistsSet(vts,f1) -> mk_existsSet(vts,c_simple_qe_exists_prop f1)
    | _ -> f)
and 
    simple_qe_exists_prop (vs,f) = match f with
    | And conjs -> 
        let (vs', conjs') = eliminate_bools vs [] conjs in
        let (conjs'_with_vs, conjs'_without_vs) = 
          List.partition (fun f -> List.exists (fun x -> occurs x f) vs') conjs' in
        mk_and (mk_existsProp(vs', mk_and conjs'_with_vs) :: 
                conjs'_without_vs)
    | ExistsSet(vts,f1) -> mk_existsSet(vts,simple_qe_exists_prop(vs,f1))
    | _ -> mk_existsProp(vs,f)
and
    eliminate 
    (bvars : bVarDecl list) 
    (bvars' : bVarDecl list) 
    (conjs : form list) = match bvars with
    | [] -> (bvars',conjs)
    | (x,t)::bvrest ->
        if (list_occurs x conjs) then
          (let (repl_conj,conjs') = find_repl x conjs [] in
          match repl_conj with
          | None -> eliminate bvrest ((x,t)::bvars') conjs
          | Some e -> 
              let sb conj = subst [(x, e)] conj in
              let conjs'' = List.map sb conjs' in
              eliminate bvrest bvars' conjs'')
        else
          eliminate bvrest bvars' conjs
and
    find_repl x conjs conjs' = match conjs with
    | [] -> (None,conjs')
    | Atom (Eq ((Var y),e))::cs when (y=x) & (not (s_occurs x e)) -> 
        (Some e, cs @ conjs')
    | Atom (Eq (e,(Var y)))::cs when (y=x) & (not (s_occurs x e)) ->
        (Some e, cs @ conjs')
    | c::cs -> find_repl x cs (c::conjs')
and
    eliminate_bools
    (bvars : ident list) 
    (bvars' : ident list) 
    (conjs : form list) : (ident list * form list) = match bvars with
    | [] -> (bvars',conjs)
    | x::bvrest ->
        begin
          (*
          if x=x then begin
            print_string ("Trying to eliminate" ^ x ^ "\n");
            print_string ("Conjuncts are:\n " ^ p_form (And conjs) ^ "\n\n")
          end;
           *)
        if (list_occurs x conjs) then
          (let (repl_conj,conjs') = find_repl_bools x conjs [] in
          match repl_conj with
          | None -> eliminate_bools bvrest (x::bvars') conjs
          | Some (Atom e) -> 
              let sb conj = subst_propvar [(x,e)] conj in
              let conjs'' = List.map sb conjs' in
              eliminate_bools bvrest bvars' conjs''
          | _ -> eliminate_bools bvrest (x::bvars') conjs)
        else
          eliminate_bools bvrest bvars' conjs
        end
and
    find_repl_bools x (conjs:form list) (conjs':form list) = match conjs with
    | [] -> (None,conjs')
    | Iff (f1,f2)::cs when f1=f2 -> find_repl_bools x cs conjs'
    | Iff (Atom (Propvar y),e)::cs when (y=x) & (not (occurs x e))
      -> (Some e, cs @ conjs')
    | Iff (e,Atom (Propvar y))::cs when (y=x) & (not (occurs x e))
      -> (Some e, cs @ conjs')
    | c::cs -> find_repl_bools x cs (c::conjs')

let sizes_and_times : (int * float) list ref = ref []
let print_stats () =
  print_string "BA statistics:\n";
  let n = List.length !sizes_and_times in
  if (n = 0) then
    print_string "[no cases run]\n"
  else begin
    let max_size = ref (0, 0.0) in
    List.iter (fun (x, y) -> 
      if (x > fst !max_size) then 
        max_size := (x, y)) !sizes_and_times;
    let total_size = List.fold_right 
        (fun (x, y) (x0, y0) -> ((x+x0), (y+.y0)))
        !sizes_and_times (0, 0.) in
    sizes_and_times := [];
    let s = Printf.sprintf "Number of cases run: %d\nMaximum formula size: %d [%.3fs]\nAverage formula size: %.1f [%.3fs]\nCumulative formula size: %d [%.3fs]\n"
        n (fst !max_size) (snd !max_size) 
        ((float_of_int (fst total_size)) /. (float_of_int n)) 
        ((snd total_size) /. (float_of_int n))
        (fst total_size) (snd total_size) in
    print_string s
  end

module type BADecisionProc = sig
  val valid : string -> form -> bool
  val getCounterexample : ident list -> form -> string
  val form_to_mona : form -> string
  val log : string -> unit
  exception BADecisionProcFailed
end

(* **************************************************
        MONA interface
   ************************************************** *)

module MONA : BADecisionProc = struct
  exception BADecisionProcFailed

(* BAD Idea, Pat, then I can't find the file later:
  let logChannel = open_out (Filename.temp_file "BA" ".log")
*)
  let logChannel = open_out "BA.log"
  let log str = begin
    output_string logChannel str; 
    output_string logChannel "\n";    
    flush logChannel
  end      

  (**************************************)
  (* Write file, invoke MONA, read file *)
  (**************************************)

  let inFileName  = "in.mona"
  let monaInclude = Util.qualify_helper_fn "cards.mona"
(*  let outFileName = Filename.temp_file "mona-out" ".txt" *)
  let outFileName = "mona-out.txt"
  let monaName = "mona"
  let validFormulaStr = "Formula is valid"
  let invalidFormulaStr = "Formula is unsatisfiable"

  let lineToFile (str:string) (fn:string) : unit = 
    begin
      let chn = open_out fn in
      output_string chn "ws1s;\n";
      output_string chn ("include \"" ^ monaInclude ^ "\";\n\n");
      output_string chn str;
      output_string chn ";\n";
      close_out chn
    end

  let runMona (inF:string) (mona:string) (outF:string) : float =
    let startTime = Unix.gettimeofday () in
    begin
      ignore (Sys.command (mona ^ " -q " ^ inF ^ "> " ^ outF));
      (Unix.gettimeofday () -. startTime)
    end

  let fileToLine (fn:string) : string =
    begin
      let chn = open_in fn in
      let str = input_line chn in
      close_in chn;
      str
    end

  type lineParseResult = Nothing | ParsedLine of string      

  let parse_line s = 
    if String.contains s '=' then ParsedLine s
    else Nothing

  let parseCounterexample (fn : string) : string = begin
    let chn = open_in fn in
    let firstLine = input_line chn in
    let expectedStr = "A counter-example of least length" in
    let leftContains str substr = 
      try (String.sub str 0 (String.length substr) = substr) with
        Invalid_argument _ -> false in
    let res = ref "" (*"\nFailed to retrieve a counterexample.\n"*) in
    let line = ref "" in
    if leftContains firstLine expectedStr then begin
      try begin        
        while (parse_line !line = Nothing) do
          line := input_line chn
        done;
        res := !line ^ "\n";
        while (parse_line !line <> Nothing) do
          (match (parse_line !line) with
            ParsedLine s -> res := !res ^ s ^ ", "
          | Nothing -> failwith "BA.parseCounterexample: BUG");
          line := input_line chn
        done;
        res := !res ^ "\n"
      end with End_of_file -> ()
    end else ();
    close_in chn;
    !res
  end

  let parseOutput str =
    if (str = validFormulaStr) then true
    else if (str = invalidFormulaStr) then false
    else raise (Internal ("Mona returned " ^ str))

  let form_to_mona f = Util.replace_dot_with_uscore (p_form f)

  let valid msg (f0:form) : bool = 
    let vs = fv f0 in
    let f = if vs.b = [] && vs.s = [] then f0
    else (let msg = "Pat, you goofed again: you don't know thy sets ["^
      (Util.spacify " " vs.s) ^ "] / bools [" ^ (Util.spacify " " vs.b) ^
      "] (BA.valid closed your formula).\n" in
    (Util.amsg msg; log msg; mk_forallProp(vs.b,mk_forallSetId(vs.s,f0)))) in
    begin
      log "FORMULA PURPOSE:\n"; log msg; log "\n";
(*
      log "ORIGINAL:\n"; log (wrap (form_to_mona f)); log "\n";
*)
      let sf = simplify f in
(*
      log "SIMPLIFIED:\n"; log (wrap (form_to_mona sf)); log "\n";
*)
      let final_form = simplify (nest_quants sf) in
      let str = wrap (form_to_mona final_form) in
      log "UNNESTED FINAL:\n"; log str; log "\n";
      lineToFile str inFileName;
      if (!no_mona) then
        begin
          sizes_and_times := (count_size final_form, 0.) :: !sizes_and_times;
          true
        end
      else
        let time = runMona inFileName monaName outFileName in 
        let res = parseOutput (fileToLine outFileName) in begin
          log (Printf.sprintf "Previous formula is: %B" res);
          log (Printf.sprintf "as computed in seconds %.3f" time); log "";
          sizes_and_times := (count_size final_form, time) :: !sizes_and_times;
          res
        end
    end

  let getCounterexample (all_sets:ident list) (f:form) : string =
    begin
      let fvs = String.concat "\n"
          (List.map (fun x -> 
            ("var2 "^(Util.replace_dot_with_uscore x)^";")) 
             (Util.remove_dups all_sets)) in
      let str = form_to_mona (nest_quants f) in
      lineToFile (fvs^str) inFileName;
      let time = runMona inFileName monaName outFileName in 
      let res = parseCounterexample outFileName in
      log res;
      res
    end
end

(* Decide if an invariant is initially true *)
let is_initially_true f =
  let fvs = fv f in
  (* e.g. assign empty set to all free set variables, false to all booleans,
     and decide *)
  let make_bools_false = 
    List.map (fun x -> Not (Atom (Propvar x))) fvs.b in
  let make_sets_empty =
    List.map (fun x -> Atom (Eq (Var x, Emptyset))) fvs.s in
  MONA.valid "initial value of invariant" 
   (mk_and (f :: (make_bools_false @ make_sets_empty)))

(* Test *)

let dotest () = 
  let f1 = Not (ForallSet ([("X",Types.TObj "A")],(Atom (Sub ((Var "X"),(Var "X")))))) in
  let ok1 = MONA.valid "" f1 in
  let f2 = ExistsSet ([("X",Types.TObj "A")],(Atom (Cardgeq ((Var "X"),1)))) in
  let ok2 = MONA.valid "" f2 in
  let s1 = Union [Var "X";Var "Y"] in
  let f31 = mk_and [Atom (Cardgeq ((Var "X"),1));
                 Atom (Cardleq ((Var "Y"),1));
                 Atom (Cardeq (s1,1));
                 Atom (Disjoint [(Var "X");(Var "Y")])] in
  let f3 = ExistsSet ([("X", Types.TObj "A")], ExistsSet ([("Y", Types.TObj "A")],f31)) in
  let ok3 = MONA.valid "" f3 in
  ok3


(* **************************************************
           Converting Sabsyn to BA
   ************************************************** *)
let rec ba_of_sabsyn (f:Sabsyn.form) : form = 
  let rec convert_setexp (se:Sabsyn.setExp) =
    match se with
    | Sabsyn.Prevar id -> Var id
    | Sabsyn.Postvar id -> Var (id ^ "'")
    | Sabsyn.Emptyset -> Emptyset
    | Sabsyn.Union us -> Union (List.map convert_setexp us)
    | Sabsyn.Inter is -> Inter (List.map convert_setexp is)
    | Sabsyn.Diff (d1, d2) -> Diff (convert_setexp d1, convert_setexp d2) in
  let rec convert_atom_form (af:Sabsyn.atomForm) : atomForm =
    match af with
    | Sabsyn.Eq (l,r) -> Eq (convert_setexp l, convert_setexp r)
    | Sabsyn.Neq (l,r) -> Neq (convert_setexp l, convert_setexp r)
    | Sabsyn.Sub (l,r) -> Sub (convert_setexp l, convert_setexp r)
    | Sabsyn.True -> True
    | Sabsyn.False -> False
    | Sabsyn.Cardeq (se, i)  -> Cardeq ((convert_setexp se), i)
    | Sabsyn.Cardleq (se, i) -> Cardleq ((convert_setexp se), i)
    | Sabsyn.Cardgeq (se, i) -> Cardgeq ((convert_setexp se), i)
    | Sabsyn.Disjoint ss -> Disjoint (List.map convert_setexp ss)
    | Sabsyn.Propvar id -> Propvar id
    | Sabsyn.Propvarpost id -> Propvar (id ^ "'") in
  let rec convert_form (f:Sabsyn.form) = 
    match f with
    | Sabsyn.Atom af -> Atom (convert_atom_form af)
    | Sabsyn.Not n -> Not (ba_of_sabsyn n)
    | Sabsyn.And cs -> mk_and (List.map ba_of_sabsyn cs)
    | Sabsyn.Or ds -> Or (List.map ba_of_sabsyn ds)
    | Sabsyn.Impl (ante, conseq) -> 
        Impl ((ba_of_sabsyn ante), (ba_of_sabsyn conseq))
    | Sabsyn.Iff (p, q) -> Iff ((ba_of_sabsyn p), (ba_of_sabsyn q))
    | Sabsyn.ExistsOne ((vdn, _) as vd, f) -> ExistsSet 
          ([vd], mk_and [Atom (Cardeq (Var vdn, 1)); ba_of_sabsyn f])
    | Sabsyn.ForallOne ((vdn, _) as vd, f) -> ForallSet 
          ([vd], mk_and [Atom (Cardeq (Var vdn, 1)); ba_of_sabsyn f])
    | Sabsyn.ExistsSet (vd, f) -> ExistsSet ([vd], ba_of_sabsyn f)
    | Sabsyn.ForallSet (vd, f) -> ForallSet ([vd], ba_of_sabsyn f)
    | Sabsyn.ExistsProp (vd, f) -> ExistsProp ([vd], ba_of_sabsyn f) 
    | Sabsyn.ForallProp (vd, f) -> ForallProp ([vd], ba_of_sabsyn f)
    | Sabsyn.UninterpretedString s -> 
        failwith "can't make BA forms from uninterpreted strings" in
  convert_form f

let show_form f = 
  let rec show_form0 ind (f0:form) : unit =
    Util.msg ind;
    (match f0 with
    | And (h::[]) ->
        Util.msg ind;
        Util.msg (MONA.form_to_mona h)
    | And (h::cs) ->
        let ind' = ind ^ "  " in
        show_form0 ind' h;
        List.iter (fun c -> Util.msg " & \n"; show_form0 ind' c) cs
    | _ -> Util.msg (MONA.form_to_mona f0)) in
  show_form0 "" f