(*
  Formalization of SMT Arithmetic for FloVer. Original author: Joachim Bard.
*)

Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Flover.Expressions.

Open Scope R.

(* list of all expr that can occur in SMT queries *)
(* alternative for SMTArith
Inductive SMTExpr : expr Q -> Prop :=
| ConstQ r : SMTExpr (Const REAL r)
| VarQ x : SMTExpr (Var Q x)
| UMinusQ e : SMTExpr e -> SMTExpr (Unop Neg e)
| PlusQ e1 e2 : SMTExpr e1 -> SMTExpr e2 -> SMTExpr (Binop Plus e1 e2)
| MinusQ e1 e2 : SMTExpr e1 -> SMTExpr e2 -> SMTExpr (Binop Sub e1 e2)
| TimesQ e1 e2 : SMTExpr e1 -> SMTExpr e2 -> SMTExpr (Binop Mult e1 e2)
| DivQ e1 e2 : SMTExpr e1 -> SMTExpr e2 -> SMTExpr (Binop Div e1 e2).
*)

Inductive SMTArith :=
| ConstQ (r: Q) : SMTArith
| VarQ (x: nat) : SMTArith
| UMinusQ (e: SMTArith) : SMTArith
| PlusQ (e1 e2: SMTArith) : SMTArith
| MinusQ (e1 e2: SMTArith) : SMTArith
| TimesQ (e1 e2: SMTArith) : SMTArith
| DivQ (e1 e2: SMTArith) : SMTArith.


Inductive SMTLogic :=
| LessQ (e1 e2: SMTArith) : SMTLogic
| LessEqQ (e1 e2: SMTArith) : SMTLogic
| EqualsQ (e1 e2: SMTArith) : SMTLogic
| NotQ (q: SMTLogic) : SMTLogic
| AndQ (q1 q2: SMTLogic) : SMTLogic
| OrQ (q1 q2: SMTLogic) : SMTLogic.

(* TODO: broken (div by 0); remove it *)
Fixpoint evalArith (f: nat -> R) (e: SMTArith) : R :=
  match e with
  | ConstQ r => Q2R r
  | VarQ x => f x
  | UMinusQ e => - (evalArith f e)
  | PlusQ e1 e2 => (evalArith f e1) + (evalArith f e2)
  | MinusQ e1 e2 => (evalArith f e1) - (evalArith f e2)
  | TimesQ e1 e2 => (evalArith f e1) * (evalArith f e2)
  | DivQ e1 e2 => (evalArith f e1) / (evalArith f e2)
  end.

Fixpoint evalLogic (f: nat -> R) (q: SMTLogic) : Prop :=
  match q with
  | LessQ q1 q2 => (evalArith f q1) < (evalArith f q2)
  | LessEqQ q1 q2 => (evalArith f q1) <= (evalArith f q2)
  | EqualsQ q1 q2 => (evalArith f q1) = (evalArith f q2)
  | NotQ q => ~ (evalLogic f q)
  | AndQ q1 q2 => (evalLogic f q1) /\ (evalLogic f q2)
  | OrQ q1 q2 => (evalLogic f q1) \/ (evalLogic f q2)
  end.

Inductive eval_smt (E: env) : SMTArith -> R -> Prop :=
| VarQ_load x v : E x = Some v -> eval_smt E (VarQ x) v
| ConstQ_eval r : eval_smt E (ConstQ r) (Q2R r)
| UMinusQ_eval e v : eval_smt E e v -> eval_smt E (UMinusQ e) (- v)
| PlusQ_eval e1 e2 v1 v2 :
    eval_smt E e1 v1 -> eval_smt E e2 v2 -> eval_smt E (PlusQ e1 e2) (v1 + v2)
| MinusQ_eval e1 e2 v1 v2 :
    eval_smt E e1 v1 -> eval_smt E e2 v2 -> eval_smt E (MinusQ e1 e2) (v1 - v2)
| TimesQ_eval e1 e2 v1 v2 :
    eval_smt E e1 v1 -> eval_smt E e2 v2 -> eval_smt E (TimesQ e1 e2) (v1 * v2)
| DivQ_eval e1 e2 v1 v2 :
    v2 <> 0 -> eval_smt E e1 v1 -> eval_smt E e2 v2 -> eval_smt E (DivQ e1 e2) (v1 / v2).

Fixpoint eval_smt_logic (E: env) (q: SMTLogic) : Prop :=
  match q with
  | LessQ e1 e2 => exists v1 v2, eval_smt E e1 v1 /\ eval_smt E e2 v2 /\ v1 < v2
  | LessEqQ e1 e2 => exists v1 v2, eval_smt E e1 v1 /\ eval_smt E e2 v2 /\ v1 <= v2
  | EqualsQ e1 e2 => exists v, eval_smt E e1 v /\ eval_smt E e2 v
  | NotQ q => ~ (eval_smt_logic E q)
  | AndQ q1 q2 => eval_smt_logic E q1 /\ eval_smt_logic E q2
  | OrQ q1 q2 => eval_smt_logic E q1 \/ eval_smt_logic E q2
  end.

(*
(* Does not work for NotQ *)
Inductive eval_smt_logic (E: env) : SMTLogic -> Prop :=
| LessQ_eval e1 e2 v1 v2 :
    eval_smt E e1 v1 -> eval_smt E e2 v2 -> v1 < v2 -> eval_smt_logic E (LessQ e1 e2)
| LessEqQ_eval e1 e2 v1 v2 :
    eval_smt E e1 v1 -> eval_smt E e2 v2 -> v1 <= v2 -> eval_smt_logic E (LessEqQ e1 e2)
| EqualsQ_eval e1 e2 v1 v2 :
    eval_smt E e1 v1 -> eval_smt E e2 v2 -> v1 = v2 -> eval_smt_logic E (EqualsQ e1 e2)
(* | NotQ_eval q : ~ (eval_smt_logic E q) -> eval_smt_logic E (NotQ q) *)
| AndQ_eval q1 q2 :
    eval_smt_logic E q1 -> eval_smt_logic E q2 -> eval_smt_logic E (AndQ q1 q2)
| OrQ_eval_l q1 q2 : eval_smt_logic E q1 -> eval_smt_logic E (OrQ q1 q2)
| OrQ_eval_r q1 q2 : eval_smt_logic E q2 -> eval_smt_logic E (OrQ q1 q2).
*)

Fixpoint SMTArith2Expr (e: SMTArith) : expr Q :=
  match e with
  | ConstQ r => Const REAL r
  | VarQ x => Var Q x
  | UMinusQ e0 => Unop Neg (SMTArith2Expr e0)
  | PlusQ e1 e2 => Binop Plus (SMTArith2Expr e1) (SMTArith2Expr e2)
  | MinusQ e1 e2 => Binop Sub (SMTArith2Expr e1) (SMTArith2Expr e2)
  | TimesQ e1 e2 => Binop Mult (SMTArith2Expr e1) (SMTArith2Expr e2)
  | DivQ e1 e2 => Binop Div (SMTArith2Expr e1) (SMTArith2Expr e2)
  end.