SMTArith.v 2.41 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 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
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.

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.
60

61 62 63 64 65 66 67 68 69 70
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.
71

72
Definition unsat q := forall f, ~ evalLogic f q.