SMTArith.v 4.25 KB
Newer Older
1 2 3 4 5
(*
  Formalization of SMT Arithmetic for FloVer. Original author: Joachim Bard.
*)

Require Import Coq.Reals.Reals Coq.QArith.Qreals.
6
Require Import Flover.Expressions.
7 8 9

Open Scope R.

10 11 12 13 14 15 16 17 18 19 20 21
(* 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).
*)

22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
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.

40
(* TODO: broken (div by 0); remove it *)
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
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.
61

62 63 64 65 66 67 68 69 70 71 72 73 74
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).

75 76 77 78 79 80 81 82 83 84 85 86
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 *)
87 88 89 90 91 92 93 94 95 96 97 98
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).
99
*)
100

101 102 103 104 105 106 107 108 109 110
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.