Commit 48e148e6 authored by Joachim Bard's avatar Joachim Bard

defining new format for SMT queries

parent 2c96eaf4
(*
Formalization of SMT Arithmetic for FloVer. Original author: Joachim Bard.
*)
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Open Scope R.
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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment