Aritmetica di Presburger

(* Espressioni *)
type exp =
    Num of int
  (* notazione deBruijn: le variabili sono numeri interi *)
  | Var of int
  | Plus of exp * exp

(* Formule *)
type form =
    Forall of form
  | Exists of form
  | Imp of form * form
  | Neg of form
  | True
  | False
  | Eq of exp * exp

(* Modifica l'indice delle variabile (Var n) in una espressione e
  Se n < th allora abbiamo (Var (n+i))
  Altrimenti abbiamo (Var (n+o)) *)
let rec shiftExp th i o e = match f with
  Num n -> Num n
| Var n -> if (n < th) then Var (n+i) else Var (n+o)
| Plus (e1, e2) -> Plus ((shiftExp th i o e1), (shiftExp th i o e2))

(* Modifica l'indice delle variabile (Var n) in una formula f
  Se n < th allora abbiamo (Var (n+i))
  Altrimenti abbiamo (Var (n+o)) *)
let rec shiftForm th i o f = match f with 
  Forall f1 -> Forall f1
| Exists f1 -> Exists f1
| Imp (f1, f2) -> Imp ((shiftForm th i o f1), (shiftForm th i o f2))
| Neg f1 -> Neg (shiftForm th i o f1)
| True -> True
| False -> False
| Eq (e1, e2) -> Eq ((shiftExp th i o e1), (shiftExp th i o e2))

(* Regole per la negazione *)
let rec lift_neg f = match f with
  Forall f1 -> Exists (lift_neg f1)
| Exists f1 -> Forall (lift_neg f1)
| Neg f1 -> f1
| True -> False
| False -> True
| _ -> Neg f

(* Regole per l'implicazione *)
let lift_if f1 f2 =
  let rec lift_if1 n m f1 f2 = match f2 with
    Forall b -> Forall (lift_if1 n (S m) f1 b)
  | Exists b -> Exists (lift_if1 n (S m) f1 b)
  | _ -> Imp ((shiftForm n m m f1), (shiftForm m O n f2))
  in
  let rec lift_if2 n f1 f2 =  match f1 with
    Forall b -> Exists (lift_if2 (S n) b f2)
  | Exists b -> Forall (lift_if2 (S n) b f2)
  | _ -> lift_if1 n O f1 f2
  in 
  lift_if2 O f1 f2

(* Funzione principale *)
let rec lift_quant f = match f with
  Forall f1 -> Forall (lift_quant f1)
| Exists f1 -> Exists (lift_quant f1)
| Imp (f1, f2) -> lift_if (lift_quant f1) (lift_quant f2)
| Neg f1 -> lift_neg (lift_quant f1)
| _ -> f

type form1 =
  FOR of form1
| EX of form1
| AND of form1 * form1
| OR of form1 * form1
| NEG of form1
| TRUE
| FALSE
| EQ of exp * exp
| CONG of int * exp * exp


(* Da form a form1 *)
let rec form_to_form1 f = match f with
  Forall f1 -> FOR (form_to_form1 f1)
| Exists f1 -> EX (form_to_form1 f1)
| Neg f1 -> NEG (form_to_form1 f1)
| Imp (f1, f2) -> OR (NEG (form_to_form1 f1), form_to_form1 f2)
| True -> TRUE
| False -> FALSE
| Eq (e1,e2) -> EQ (e1,e2)

(* Distributività destra *)
let rec push_and_rules1 f1 f2 = match f1 with
  OR (f3, f4) -> OR (push_and_rules1 f3 f2, push_and_rules1 f4 f2)
| _ -> AND (f1, f2)

(* Distributività sinistra *)
let rec push_and_rules f1 f2 = match f2 with
  OR (f3, f4) -> OR (push_and_rules f1 f3, push_and_rules f1 f4)
| _ -> push_and_rules1 f1 f2

(* Distributività *)
let rec push_and f = match f with
  AND (f1, f2) -> push_and_rules (push_and f1) (push_and f2)
| OR (f1, f2) -> OR (push_and f1, push_and f2)
| _ -> f

(* Trasforma una negazione di modulo in una disgiunzione di moduli *)
let rec expand_NEG_CONG i a b n = match n with 
  0 -> FALSE
| 1 -> CONG (i, a, Plus (b, Num n))
| _ -> OR (CONG (i, a, Plus (b, Num n)),
           expand_NEG_CONG i a b (n-1))

(* Spinge in basso le negazioni *)
let rec push_neg b f = match b,f with
  true, AND (f1, f2) -> AND ((push_neg true f1), (push_neg true f2))
| true, OR (f1, f2) -> OR ((push_neg true f1), (push_neg true f2))
| true, NEG f1 -> push_neg false f1
| true, _ -> f
| false, AND (f1, f2) -> OR ((push_neg false f1), (push_neg false f2))
| false, OR (f1, f2) -> AND ((push_neg false f1), (push_neg false f2))
| false, NEG f1 -> push_neg true f1
| false, TRUE -> FALSE
| false, FALSE -> TRUE
| false, CONG (0, e1, e2) -> NEG (EQ (e1, e2))
| false, CONG (1, e1, e2) -> FALSE
| false, CONG (i, e1, e2) -> expand_NEG_CONG i e1 e2 (i-1)
| false, _ -> NEG f

(* Mette sotto forma dnf *)
let dnf f = push_and (push_neg true f)

(* Espande i forall *)
let rec expand_forall b f = match (b,f) with
  true, FOR f1 -> NEG (EX (expand_forall false f1))
| true, EX f1 -> EX (expand_forall true f1)
| true, _ -> dnf f
| false, FOR f1 -> EX (expand_forall false f1)
| false, EX f1 -> NEG (EX (expand_forall true f1))
| false, _ -> dnf (NEG f)

(* Mette una formula form sotto forma prenex DNF per form1 *)
let normal_form f = expand_forall true (form_to_form1 (lift_quant f))

(x ∧¬z) ∨ (¬y ∧ ¬z)

*H6

∃x.∃y.((P x) ∧¬(Q x))

*H7

∃x.∀y.∃z. ¬(P x y) ∨(P z z)

H8

(* Decide se un modulo e' vero *)
let cong_dec i a b =
  match i with
   0 -> a=b
  | _ -> (a-b) mod i =0

(* Valuta una espressione in un ambiente *)
let rec exp_to_int l e = match e with
  Num n -> n
| Var n -> List.nth l n
| Plus (e1, e2) -> (exp_to_int l e1)+(exp_to_int l e2)

(* Decide una formula senza variabili *)
let rec decide_ground f = match f with
  FOR b -> false
| EX b -> false
| AND (f1, f2) -> if decide_ground f1 then decide_ground f2 else false
| OR (f1, f2) -> if decide_ground f1 then true else decide_ground f2 
| NEG f1 -> not (decide_ground f1)
| TRUE -> true
| FALSE -> false
| EQ (e1, e2) -> (exp_to_int [] e1) = (exp_to_int [] e2)
| CONG (i, e1, e2) -> cong_dec i (exp_to_int [] e1) (exp_to_int [] e2) 

(* Fattorizza una espressione rispetto a Var 0 *)
let rec factor_var e = match e with
  Num i -> 0, e
| Var 0 -> 1, Num 0
| Var n -> 0, Var (n-1)
| Plus (e1, e2) -> 
    let m1,e3 = factor_var e1 in
    let m2,e4 = factor_var e2 in
     (m1+m2), Plus (e3, e4)

(* Fattorizza una formula rispetto a Var 0 *)
let factor_exp f = match f with
  EQ (e1, e2) ->
    let m1,e3 = factor_var e1 in
    let m2,e4 = factor_var e2 in
    if (m1
    let m1,e3 = factor_var e1 in
    let m2,e4 = factor_var e2 in
    if (m1
    let m1,e3 = factor_var e1 in
    let m2,e4 = factor_var e2 in
    if (m1 0,f

(* Riduce un modulo con un modulo *)
let rec reduce_CONG_CONG1 i m1 m2 a1 a2 b1 b2 =
  if (m1=m2) then (m1,a1,b1, CONG (i, Plus (a2, b1), Plus (b2, a1)))
  else if m1 < m2 then
    reduce_CONG_CONG1 i m1 (m2-m1) a1 (Plus (a2, b1)) b1 (Plus (b2, a1))
  else
    reduce_CONG_CONG1 i m2 (m1-m2) a2 (Plus (a1, b2)) b2 (Plus (b1, a2))

(* Una simulazione del prodotto scalare *)
let rec scal n e = match n with
  0 -> Num 0
| 1 -> e
| _ -> Plus (e, (scal (n-1) e))

(* Riduce una lista di moduli con un modulo *)
let rec reduce_CONG_CONG i1 m1 a1 b1 l = match l with
  (m2,CONG (i2, a2, b2))::l1 -> 
    let (i4, a4,b4,f4) =
      reduce_CONG_CONG1 (lcm i1 i2) (((lcm i1 i2)/i1)*m1)
                        (((lcm i1 i2)/ i2) * m2)
                        (scal ((lcm i1 i2)/i1) a1)
                        (scal ((lcm i1 i2)/i2) a2)
                        (scal ((lcm i1 i2)/i1) b1)
                        (scal ((lcm i1 i2)/i2) b2) in
    let (i5, m5, a5, b5, l5) =
      reduce_CONG_CONG (lcm i1 i2) i4 a4 b4 l1 in
    (i5, m5, a5, b5, f4::l5)
| _ -> (i1,m1,a1,b1,[])


(* Riduce una lista di equazioni con un'equazione *)
let rec reduce_EQ_EQ m1 a1 b1 l = match l with
  (m2,EQ (a2, b2))::l1 ->
    (EQ (Plus (scal ((lcm m1 m2)/m1) b1, scal ((lcm m1 m2)/m2) a2), 
         Plus (scal ((lcm m1 m2)/m1) a1, scal ((lcm m1 m2)/m2) b2)))
    ::reduce_EQ_EQ m1 a1 b1 l1
| _                    -> []

(* Riduce una lista di negazioni di equazioni con un'equazione *)
let rec reduce_EQ_NEQ m1 a1 b1 l = match l with
  (m2,NEG (EQ (a2, b2)))::l1 ->
    (NEG (EQ (Plus (scal ((lcm m1 m2)/m1) b1, scal ((lcm m1 m2)/m2) a2), 
              Plus (scal ((lcm m1 m2)/m1) a1, scal ((lcm m1 m2)/m2) b2))))
    ::reduce_EQ_NEQ m1 a1 b1 l1
| _                          -> []


(* Riduce una lista di moduli con un'equazione *)
let rec reduce_EQ_CONG m1 a1 b1 l = match l with
  (m2,CONG (n, a2, b2))::l1 -> 
    (CONG (((lcm m1 m2)/m2)* n,
           Plus (scal ((lcm m1 m2)/m1) b1, scal ((lcm m1 m2)/m2) a2), 
           Plus (scal ((lcm m1 m2)/m1) a1, scal ((lcm m1 m2)/m2) b2)))
    ::reduce_EQ_CONG m1 a1 b1 l1
| _                         -> []

(* Chiama le riduzioni *)
let process_list l = match l with
  (l1,[],(m1,CONG (i1,a1,b1))::l3,l4) ->
   let (i2,m2,a2,b2,l5) = reduce_CONG_CONG i1 m1 a1 b1 l3 in
      (CONG (gcd i2 m2, a2, b2))::(List.append l1 l5)
| (l1,(m1,(EQ (a1, b1)))::l2,l3,l4) ->
  (CONG (m1, a1, b1))::
    (List.append l1
      (List.append (reduce_EQ_EQ m1 a1 b1 l2)
        (List.append (reduce_EQ_CONG m1 a1 b1 l3)
         (reduce_EQ_NEQ m1 a1 b1 l4))))
| (l1,_,_,_) -> l1

(* Tratta la lista di congiunzioni per produrre 4 liste:
     -la prima contiene tutte le formule che non contengono Var 0
     -la seconda contiene tutte le equazioni
     -la terza contiene tutti i moduli
     -la quarta contiene tutte le negazioni di equazione
*)
let rec sort_and f = match f with
| EQ (e1, e2) ->
    let n, f1 = factorExp f in
      if (n=0) then [f1],[],[],[]
      else [],[n,f1],[],[]
| NEG (EQ (e1, e2)) ->
    let n, f1 = factorExp f in
      if (n=0) then [f1],[],[],[]
      else [],[],[],[n,f1]
| CONG (n, e1, e2) ->
   if n=0 then
     begin
       let n1, f1 = factorExp (EQ (e1, e2)) in
         if n1=0 then [f1],[],[],[] else [],[n,f1],[],[]
     end
   else
     begin
       let n1, f1 = factorExp f in
         if n1=0 then [f1],[],[],[] else [],[],[n,f1],[]
     end
| AND (f1, f2) ->
    let (l1,l2,l3,l4) = sort_and f1 in
    let (l'1,l'2,l'3,l'4) = sort_and f2 in
      (List.append l1 l'1, List.append l2 l'2, List.append l3 l'3, List.append l4 l'4)
| f -> [f],[],[],[]

(* Trasforma una lista di formule in una congiunzione *)
let rec build_conj = function
  []      -> TRUE
| [e]     -> e
| e :: l1 -> AND (e, (build_conj l1))

(* Elimina la variabile 0 *)
let rec elim_quant f = match f with
  OR (f1, f2) -> OR ((elim_quant f1), (elim_quant f2))
| _  -> build_conj (process_list (sort_and f))

(* Elimina tutte le variabili *)
let rec elim_quants f = match f with
  EX f1 -> elim_quant (elim_quants f1)
| NEG (EX f1) -> dnf (NEG (elim_quant (elim_quants f1)))
| _ -> f