(**************************************************************************)
(*                                                                        *)
(*     SMTCoq                                                             *)
(*     Copyright (C) 2011 - 2015                                          *)
(*                                                                        *)
(*     Michaël Armand                                                     *)
(*     Benjamin Grégoire                                                  *)
(*     Chantal Keller                                                     *)
(*                                                                        *)
(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
(*                                                                        *)
(*   This file is distributed under the terms of the CeCILL-C licence     *)
(*                                                                        *)
(**************************************************************************)

Require Import List.
Require Import Bool.
Require Import Int63.
Require Import PArray.

(* Require Import AxiomesInt. *)

Local Open Scope int63_scope.
Local Open Scope array_scope.

Coercion is_true (x: bool) := x = true.

Set Vm Optimize.

Notation var := int (only parsing).

(* Variables interpretation *)
Module Valuation.
(* TODO : Should be var -> Prop *)
  Definition t := var -> bool.
  Definition wf (rho : t) : Prop := rho 0 /\ ~ rho 1.

End Valuation.


Module Var.

  Definition _true : var := 0. (* true *)
  Register _true as PrimInline.

  Definition _false : var := 1. (* false *)

  Definition interp (rho:Valuation.t) (x:var) : bool := rho x.

  Lemma interp_true : forall rho, Valuation.wf rho -> interp rho _true.
  Proof. intros rho [H _];exact H. Qed.

  Lemma interp_false : forall rho, Valuation.wf rho -> ~ interp rho _false.
  Proof. intros rho [_ H];exact H. Qed.

End Var.

Notation _lit := int (only parsing).

Module Lit.

  Definition is_pos (l:_lit) := is_even l.
  Register is_pos as PrimInline.

  Definition blit (l:_lit) : var := l >> 1.
  Register blit as PrimInline.

  Definition lit (x:var) : _lit := x << 1.
  Register lit as PrimInline.

  Definition neg (l:_lit) : _lit := l lxor 1.
  Register neg as PrimInline.

  Definition nlit (x:var) : _lit := neg (lit x).
  Register nlit as PrimInline.

  Definition _true : _lit := Eval compute in lit Var._true.
  Register _true as PrimInline.

  Lemma lit_true : _true = lit Var._true.
  Proof. reflexivity. Qed.

  Definition _false : _lit := Eval compute in lit Var._false.
  Register _false as PrimInline.

  Lemma lit_false : _false = lit Var._false.
  Proof. reflexivity. Qed.

  Definition eqb (l l' : _lit) := l == l'.
  Register eqb as PrimInline.

  Lemma eqb_spec : forall l l', eqb l l' = true <-> l = l'.
  Proof eqb_spec.

  Lemma neg_involutive : forall l,  neg (neg l) = l.
  Proof.
    unfold neg;intros; rewrite <- lxor_assoc;change (1 lxor 1) with 0;rewrite lxor_0_r;trivial.
  Qed.

  Lemma blit_neg : forall l, blit (neg l) = blit l.
  Proof.
    unfold blit, neg;intros l.
    rewrite lxor_lsr, lxor_0_r;trivial.
  Qed.

  Lemma lit_blit: forall l,
    is_pos l = true -> lit (blit l) = l.
  Proof.
    unfold is_pos, lit, blit;intros.
    rewrite (bit_xor_split l) at 2.
    rewrite is_even_bit, negb_true_iff in H;rewrite H.
    symmetry;apply lxor_0_r.
  Qed.

  Lemma lit_blit_neg: forall l,
    is_pos l = false -> lit (blit l) = neg l.
  Proof.
    unfold is_pos, lit, blit;intros.
    rewrite (bit_xor_split l) at 2.
    rewrite is_even_bit, negb_false_iff in H;rewrite H.
    rewrite <- (neg_involutive ((l >> 1) << 1)) at 1;trivial.
  Qed.

  Lemma nlit_blit: forall l,
    is_pos l = false -> nlit (blit l) = l.
  Proof.
    unfold nlit;intros;rewrite lit_blit_neg;auto using neg_involutive.
  Qed.

  Lemma nlit_blit_neg: forall l,
    is_pos l = true -> nlit (blit l) = neg l.
  Proof.
    unfold nlit;intros;rewrite lit_blit;auto using neg_involutive.
  Qed.

  Lemma is_pos_lit : forall l,
    is_pos (lit l) = true.
  Proof.
    unfold is_pos, lit;apply is_even_lsl_1.
  Qed.

  Lemma is_pos_neg : forall l,
    is_pos (neg l) = negb (is_pos l).
  Proof.
    unfold neg, is_pos;intros l.
    rewrite is_even_xor, xorb_false_r;trivial.
  Qed.

  Lemma is_pos_nlit : forall l,
    is_pos (nlit l) = false.
  Proof.
    unfold nlit;intros l;rewrite is_pos_neg, is_pos_lit;trivial.
  Qed.

  Lemma is_pos_true : is_pos _true.
  Proof. reflexivity. Qed.

  Lemma is_pos_false : is_pos _false.
  Proof. reflexivity. Qed.

  Lemma blit_pos :forall a b,
    Lit.blit a = Lit.blit b -> Lit.is_pos a = Lit.is_pos b ->
    a = b.
  Proof lsr_is_even_eq.

  Lemma blit_lit : forall l, blit (lit (blit l)) = blit l.
  Proof.
    intros l;case_eq (is_pos l);intros.
    rewrite lit_blit;trivial.
    rewrite lit_blit_neg, blit_neg;trivial.
  Qed.

  Lemma blit_nlit : forall l, blit (nlit (blit l)) = blit l.
  Proof.
    intros l;case_eq (is_pos l);intros.
    rewrite nlit_blit_neg, blit_neg;trivial.
    rewrite nlit_blit;trivial.
  Qed.

  Lemma blit_true : blit _true = Var._true.
  Proof. reflexivity. Qed.

  Lemma blit_false : blit _false = Var._false.
  Proof. reflexivity. Qed.

                        (* Interpretation of a literal *)
  Definition interp rho (l:_lit) :=
    if is_pos l then Var.interp rho (blit l)
      else negb (Var.interp rho (blit l)).

  Lemma interp_true : forall rho, Valuation.wf rho -> interp rho _true.
  Proof.
    intros rho Hwf;unfold interp;rewrite is_pos_true, blit_true.
    apply Var.interp_true;trivial.
  Qed.

  Lemma interp_false : forall rho, Valuation.wf rho -> ~interp rho _false.
  Proof.
    intros rho Hwf;unfold interp;rewrite is_pos_false, blit_false.
    apply Var.interp_false;trivial.
  Qed.

  Lemma interp_neg : forall rho l, interp rho (neg l) = negb (interp rho l).
  Proof.
    intros rho l;unfold interp;rewrite is_pos_neg, blit_neg.
    destruct (is_pos l);simpl;auto using negb_involutive.
  Qed.

  Lemma interp_lit : forall rho l, interp rho (lit (blit l)) = Var.interp rho (blit l).
  Proof.
    intros;unfold interp;rewrite is_pos_lit, blit_lit;trivial.
  Qed.

  Lemma interp_nlit : forall rho l, interp rho (nlit (blit l)) = negb (Var.interp rho (blit l)).
  Proof.
    unfold nlit;intros rho l;rewrite interp_neg, interp_lit;trivial.
  Qed.

  Lemma interp_eq_compat : forall rho1 rho2 l,
    rho1 (blit l) = rho2 (blit l) ->
    interp rho1 l = interp rho2 l.
  Proof.
    unfold interp, Var.interp;intros rho1 rho2 l Heq;rewrite Heq;trivial.
  Qed.

  Lemma lxor_neg : forall l1 l2, (l1 lxor l2 == 1) = true -> l1 = Lit.neg l2.
  Proof.
    unfold Lit.neg; intros l1 l2;rewrite eqb_spec;intros Heq;rewrite <- Heq.
    rewrite lxor_comm, <- lxor_assoc, lxor_nilpotent, lxor_0_r;trivial.
  Qed.

End Lit.


Lemma compare_spec' : forall x y,
    match x ?= y with
    | Lt => x < y
    | Eq => x = y
    | Gt => y < x
    end.
Proof.
  intros x y;rewrite compare_def_spec;unfold compare_def.
  case_eq (x < y);intros;[reflexivity | ].
  case_eq (x == y);intros.
  rewrite <- eqb_spec;trivial.
  rewrite <- not_true_iff_false in H, H0.
  unfold is_true in *;rewrite ltb_spec in H |- *;rewrite eqb_spec in H0.
  assert ([|x|] <> [|y|]) by (intros Heq;apply H0, to_Z_inj;trivial);omega.
Qed.


Module C.

  Definition t := list _lit.

  Definition interp (rho:Valuation.t) (l:t) :=
    List.existsb (Lit.interp rho) l.

  Definition valid rho c :=
    interp rho c = true.

  Definition _true : t := Lit._true :: nil.

  Definition is_false (c:t) :=
    match c with
      | nil => true
      | _ => false
    end.

  Section OR.

    Variable or : t -> t -> t.
    Variable l1 : _lit.
    Variable c1 : t.

    Fixpoint or_aux (c2:t) :=
      match c2 with
      | nil => l1 :: c1
      | l2::c2' =>
        match l1 ?= l2 with
        | Eq => l1 :: or c1 c2'
        | Lt => l1 :: or c1 c2
        | Gt => l2 :: or_aux c2'
        end
      end.

    Variable rho : Valuation.t.
    Hypothesis or_correct : forall c2,
        interp rho (or c1 c2) = interp rho c1 || interp rho c2.

    Lemma or_aux_correct : forall c2,
      interp rho (or_aux c2) = interp rho (l1::c1) || interp rho c2.
    Proof.
      induction c2;simpl.
      rewrite orb_false_r;trivial.
      generalize (compare_spec' l1 a);destruct (l1 ?= a);intros H;simpl.
      rewrite H;destruct (Lit.interp rho a);trivial.
      rewrite !orb_false_l, or_correct;trivial.
      rewrite or_correct;simpl;rewrite orb_assoc;trivial.
      rewrite IHc2;simpl.
      destruct (Lit.interp rho a);simpl;trivial.
      rewrite orb_true_r;trivial.
    Qed.

  End OR.

  Fixpoint or (c1 c2:t) {struct c1} : t :=
    match c1, c2 with
    | nil, _ => c2
    | _, nil => c1
    | l1::c1, l2::c2' =>
      match compare l1 l2 with
      | Eq => l1 :: or c1 c2'
      | Lt => l1 :: or c1 c2
      | Gt => l2 :: or_aux or l1 c1 c2'
      end
    end.

  Lemma or_correct : forall rho c1 c2,
    interp rho (or c1 c2) = interp rho c1 || interp rho c2.
  Proof.
    induction c1;simpl;trivial.
    destruct c2;simpl.
    rewrite orb_false_r;trivial.
    generalize (compare_spec' a i);destruct (a ?= i);intros H;simpl.
    rewrite H, IHc1;simpl;destruct (Lit.interp rho i);simpl;trivial.
    rewrite IHc1, orb_assoc;trivial.
    rewrite or_aux_correct;simpl;trivial.
    destruct (Lit.interp rho i);trivial.
    simpl;rewrite !orb_true_r;trivial.
  Qed.

  Section RESOLVE.

    Variable resolve : t -> t -> t.
    Variable l1 : _lit.
    Variable c1 : t.

    Fixpoint resolve_aux (c2:t) : t :=
      match c2 with
      | nil => _true
      | l2::c2' =>
        match compare l1 l2 with
        | Eq => l1 :: resolve c1 c2'
        | Lt => if l1 lxor l2 == 1 then or c1 c2' else l1 :: resolve c1 c2
        | Gt =>
          if l1 lxor l2 == 1 then or c1 c2' else l2 :: resolve_aux c2'
        end
      end.

    Lemma resolve_aux_correct : forall rho,
      (forall c2, interp rho c1 -> interp rho c2 -> interp rho (resolve c1 c2)) ->
      interp rho (l1 :: c1) ->
      forall c2, interp rho c2 ->
      interp rho (resolve_aux c2).
    Proof.
      intros rho resolve_correct Hc1;simpl in Hc1.
      induction c2;simpl;try discriminate.
      generalize (compare_spec' l1 a);destruct (l1 ?= a);intros;subst;simpl.
      simpl in Hc1;destruct (Lit.interp rho a);simpl in *;auto.
      generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros.
      rewrite or_correct.
      rewrite H1, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho a).
      simpl in Hc1;rewrite Hc1;trivial.
      simpl in H0;rewrite H0, orb_true_r;trivial.
      simpl;destruct (Lit.interp rho l1);simpl;auto.
      generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros.
      rewrite or_correct.
      rewrite H1, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho a).
      simpl in Hc1;rewrite Hc1;trivial.
      simpl in H0;rewrite H0, orb_true_r;trivial.
      simpl;destruct (Lit.interp rho a);simpl;auto.
    Qed.

  End RESOLVE.

  Fixpoint resolve (c1 c2:t) {struct c1} : t :=
    match c1, c2 with
    | nil, _ => _true
    | _, nil => _true
    | l1::c1, l2::c2' =>
      match compare l1 l2 with
      | Eq => l1 :: resolve c1 c2'
      | Lt => if l1 lxor l2 == 1 then or c1 c2' else l1 :: resolve c1 c2
      | Gt =>
        if l1 lxor l2 == 1 then or c1 c2' else l2 :: resolve_aux resolve l1 c1 c2'
      end
    end.

  Lemma resolve_correct : forall rho c1 c2,
    interp rho c1 -> interp rho c2 ->
    interp rho (resolve c1 c2).
  Proof.
    induction c1;simpl;try discriminate.
    destruct c2;simpl;try discriminate.
    intros Hc1 Hc2.
    generalize (compare_spec' a i);destruct (a ?= i);intros;subst;simpl.
    destruct (Lit.interp rho i);simpl in *;auto.
    generalize (Lit.lxor_neg a i);destruct (a lxor i == 1);intros.
    rewrite or_correct.
    rewrite H0, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho i).
    simpl in Hc1;rewrite Hc1;trivial.
    simpl in Hc2;rewrite Hc2, orb_true_r;trivial.
    simpl;destruct (Lit.interp rho a);simpl;auto.
    generalize (Lit.lxor_neg a i);destruct (a lxor i == 1);intros.
    rewrite or_correct.
    rewrite H0, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho i).
    simpl in Hc1;rewrite Hc1;trivial.
    simpl in Hc2;rewrite Hc2, orb_true_r;trivial.
    simpl;destruct (Lit.interp rho i);simpl;auto using resolve_aux_correct.
  Qed.

  Lemma interp_true : forall rho, Valuation.wf rho -> interp rho _true = true.
  Proof.
    unfold _true, interp;intros rho Hwf;simpl.
    rewrite Lit.interp_true;trivial.
  Qed.

  Lemma is_false_correct :
    forall c, is_false c = true ->
      forall rho, ~valid rho c.
  Proof.
    unfold valid, interp;destruct c;simpl; auto;discriminate.
  Qed.

End C.


Notation clause_id := int (only parsing).

Notation resolution := (array clause_id) (only parsing).

Module S.

  Definition t := array C.t.

  Definition get (s:t) (cid:clause_id) := s.[cid].
  Register get as PrimInline.

  (* Do not use this function outside this module *)
  (* expect if you are sure that [c = sort_uniq c] *)
  Definition internal_set (s:t) (cid:clause_id) (c:C.t) : t := s.[cid <- c].
  Register internal_set as PrimInline.

  Definition make (nclauses : int) : t :=
    PArray.make nclauses C._true.

  Definition valid rho s :=
    forall id, C.valid rho (get s id).


  (* Specification of make *)

  Lemma valid_make : forall rho nclauses,
    Valuation.wf rho ->
    valid rho (make nclauses).
  Proof.
    unfold valid, make, get;intros.
    rewrite PArray.get_make; apply C.interp_true;trivial.
  Qed.


  (* Specification of get *)

  Lemma valid_get : forall rho s, valid rho s ->
    forall id, C.valid rho (get s id).
  Proof. auto. Qed.


  (* Specification of internal_set *)

  Lemma valid_internal_set :
    forall rho s, valid rho s ->
      forall c, C.valid rho c ->
        forall id, valid rho (set s id c).
  Proof.
    unfold valid, get, set;simpl;intros.
    destruct (Int63Properties.reflect_eqb id id0);subst.
    case_eq (id0 < length s);intros.
    rewrite PArray.get_set_same;trivial.
    rewrite PArray.get_outofbound.
    rewrite PArray.default_set.
    rewrite <- (PArray.get_outofbound _ _ (length s)); trivial.
    rewrite <- not_true_iff_false, ltb_spec;auto with zarith.
    rewrite PArray.length_set;trivial.
    rewrite get_set_other;trivial.
  Qed.

  (* Building clause *)
  (* Same as set but without precondition *)

  (* TODO: It can be a good idea to change the insertion sort algorithm *)

  Fixpoint insert l1 c :=
   match c with
   | nil => l1:: nil
   | l2 :: c' =>
     match l1 ?= l2 with
     | Lt => if l1 lxor l2 == 1 then C._true else l1 :: c
     | Eq => c
     | Gt => if l1 lxor l2 == 1 then C._true else l2 :: insert l1 c'
     end
   end.

  Fixpoint sort_uniq c :=
    match c with
    | nil => nil
    | l1 :: c => insert l1 (sort_uniq c)
    end.

  Lemma insert_correct : forall rho (Hwf:Valuation.wf rho) l1 c,
    C.interp rho (insert l1 c) = C.interp rho (l1 :: c).
  Proof.
    intros rho Hwf l1;induction c;simpl;trivial.
    generalize (compare_spec' l1 a);destruct (l1 ?= a);intros;subst;simpl.
    destruct (Lit.interp rho a);simpl in *;auto.
    generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros;trivial.
    rewrite C.interp_true;trivial.
    rewrite H0, Lit.interp_neg;trivial;destruct (Lit.interp rho a);trivial.
    generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros.
    rewrite C.interp_true;trivial.
    rewrite H0, Lit.interp_neg;trivial;destruct (Lit.interp rho a);trivial.
    simpl;rewrite orb_assoc,(orb_comm (Lit.interp rho l1)),<-orb_assoc,IHc;trivial.
  Qed.

  Lemma sort_uniq_correct : forall rho (Hwf:Valuation.wf rho) c,
    C.interp rho (sort_uniq c) = C.interp rho c.
  Proof.
    intros rho Hwf;induction c;simpl;trivial.
    rewrite insert_correct;trivial;simpl;rewrite IHc;trivial.
  Qed.

  Definition set_clause (s:t) pos (c:C.t) : t :=
    set s pos (sort_uniq c).

  Lemma valid_set_clause :
    forall rho s, Valuation.wf rho -> valid rho s -> forall pos c,
      C.valid rho c -> valid rho (set_clause s pos c).
  Proof.
    unfold valid, get, set_clause. intros rho s Hrho Hs pos c Hc id.
    destruct (Int63Properties.reflect_eqb pos id);subst.
    case_eq (id < length s); intro H.
    unfold get;rewrite PArray.get_set_same; trivial.
    unfold C.valid;rewrite sort_uniq_correct;trivial.
    generalize (Hs id);rewrite !PArray.get_outofbound, PArray.default_set;trivial.
    rewrite length_set;trivial.
    rewrite get_set_other;trivial.
  Qed.


  (* Resolution *)

  Definition set_resolve (s:t) pos (r:resolution) : t :=
    let len := PArray.length r in
    if len == 0 then s
    else
      let c := foldi (fun i c => C.resolve (get s (r.[i])) c) 1 (len - 1)
         (get s (r.[0])) in
      internal_set s pos c.

  Lemma valid_set_resolve :
    forall rho s, Valuation.wf rho -> valid rho s ->
      forall pos r, valid rho (set_resolve s pos r).
  Proof.
    unfold set_resolve; intros rho s Hrho Hv pos r.
    destruct (Int63Properties.reflect_eqb (length r) 0);[trivial | ].
    apply valid_internal_set;trivial.
    apply foldi_ind;auto.
    intros i c _ _ Hc;apply C.resolve_correct;auto;apply Hv.
  Qed.

End S.