Commit 829c6eb5 authored by Joachim Bard's avatar Joachim Bard

defining evaluation of smt queries as predicates

parent fbef6bd9
......@@ -37,6 +37,7 @@ Inductive 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
......@@ -58,6 +59,32 @@ Fixpoint evalLogic (f: nat -> R) (q: SMTLogic) : Prop :=
| 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).
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
......
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