Commit 59aa2719 authored by Joachim Bard's avatar Joachim Bard

implementing splitting of query

parent b08371d2
......@@ -4,6 +4,7 @@
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Flover.Expressions.
Require Import Flover.Infra.ExpressionAbbrevs.
Open Scope R.
......@@ -82,6 +83,27 @@ Fixpoint eval_smt_logic (E: env) (q: SMTLogic) : Prop :=
| OrQ q1 q2 => eval_smt_logic E q1 \/ eval_smt_logic E q2
end.
Fixpoint varsSMT (e: SMTArith) :=
match e with
| VarQ x => {{x}}
| ConstQ _ => NatSet.empty
| UMinusQ e => varsSMT e
| PlusQ e1 e2 => varsSMT e1 varsSMT e2
| MinusQ e1 e2 => varsSMT e1 varsSMT e2
| TimesQ e1 e2 => varsSMT e1 varsSMT e2
| DivQ e1 e2 => varsSMT e1 varsSMT e2
end.
Fixpoint varsLogic (q: SMTLogic) :=
match q with
| LessQ e1 e2 => varsSMT e1 varsSMT e2
| LessEqQ e1 e2 => varsSMT e1 varsSMT e2
| EqualsQ e1 e2 => varsSMT e1 varsSMT e2
| NotQ q => varsLogic q
| AndQ q1 q2 => varsLogic q1 varsLogic q2
| OrQ q1 q2 => varsLogic q1 varsLogic q2
end.
(*
(* Does not work for NotQ *)
Inductive eval_smt_logic (E: env) : SMTLogic -> Prop :=
......@@ -100,7 +122,7 @@ Inductive eval_smt_logic (E: env) : SMTLogic -> Prop :=
Fixpoint SMTArith2Expr (e: SMTArith) : expr Q :=
match e with
| ConstQ r => Const REAL r
| ConstQ r => Expressions.Const REAL r
| VarQ x => Var Q x
| UMinusQ e0 => Unop Neg (SMTArith2Expr e0)
| PlusQ e1 e2 => Binop Plus (SMTArith2Expr e1) (SMTArith2Expr e2)
......@@ -108,3 +130,221 @@ Fixpoint SMTArith2Expr (e: SMTArith) : expr Q :=
| TimesQ e1 e2 => Binop Mult (SMTArith2Expr e1) (SMTArith2Expr e2)
| DivQ e1 e2 => Binop Div (SMTArith2Expr e1) (SMTArith2Expr e2)
end.
Definition optionBind2 (X: Type) (F: X -> X -> X) (x x': option X) : option X :=
match x with
| Some v => match x' with
| Some v' => Some (F v v')
| None => x
end
| None => x'
end.
Definition merge_split (F: SMTLogic -> SMTLogic -> SMTLogic) l r :=
match l, r with
| (P1, q1), (P2, q2) => (optionBind2 AndQ P1 P2, optionBind2 F q1 q2)
end.
(*
(* TODO: splits by syntax *)
(* if q looks like part of the precondition it appears left, otherwise right *)
Fixpoint splitPre (q: SMTLogic) : option SMTLogic * option SMTLogic :=
match q with
| LessEqQ (ConstQ r) (VarQ x) => (Some q, None)
| LessEqQ (VarQ x) (ConstQ r) => (Some q, None)
| LessQ (ConstQ r) (VarQ x) => (Some q, None)
| LessQ (VarQ x) (ConstQ r) => (Some q, None)
| AndQ q1 q2 => merge_split AndQ (splitPre q1) (splitPre q2)
| _ => (None, Some q)
end.
Lemma splitPre_LessEqQ e1 e2 :
splitPre (LessEqQ e1 e2) = (Some (LessEqQ e1 e2), None)
\/ splitPre (LessEqQ e1 e2) = (None, Some (LessEqQ e1 e2)).
Proof.
destruct e1, e2; auto.
Qed.
Lemma splitPre_LessQ e1 e2 :
splitPre (LessQ e1 e2) = (Some (LessQ e1 e2), None)
\/ splitPre (LessQ e1 e2) = (None, Some (LessQ e1 e2)).
Proof.
destruct e1, e2; auto.
Qed.
Lemma splitPre_correct_SN q q' :
splitPre q = (Some q', None) -> q = q'.
Proof.
induction q in q' |- *; cbn; intros eq; try congruence.
- destruct e1, e2; congruence.
- destruct e1, e2; congruence.
- destruct (splitPre q1) as [[?|] [?|]]; destruct (splitPre q2) as [[?|] [?|]]; cbn in eq; try congruence.
+ rewrite (IHq1 s), (IHq2 s0); auto.
congruence.
+ rewrite (IHq1 s); auto. admit.
+
Lemma splitPre_corr E (q p' q': SMTLogic) :
(eval_smt_logic E q)
-> (splitPre q = (Some p', Some q') -> eval_smt_logic E p' /\ eval_smt_logic E q')
/\ (splitPre q = (None, Some q') -> eval_smt_logic E q')
/\ (splitPre q = (Some p', None) -> eval_smt_logic E p').
Proof.
induction q in p', q' |- *; intros H.
- destruct (splitPre_LessQ e1 e2) as [-> | ->]; repeat split; congruence.
- destruct (splitPre_LessEqQ e1 e2) as [-> | ->]; repeat split; congruence.
- cbn. repeat split; congruence.
- cbn. repeat split; try congruence. intros H'. assert (q' = NotQ q) by congruence.
now subst.
- destruct H as [H1 H2]. cbn.
destruct (splitPre q1) as [[?|] [?|]]; destruct (splitPre q2) as [[?|] [?|]]; cbn; repeat split; try congruence.
+ assert (p' = AndQ s s1) by congruence.
rewrite H0. cbn. split.
* destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
* destruct (IHq2 s1 s2 H2) as [? [? ?]]. tauto.
+ assert (q' = AndQ s0 s2) by congruence.
rewrite H0. cbn. split.
* destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
* destruct (IHq2 s1 s2 H2) as [? [? ?]]. tauto.
+ assert (p' = AndQ s s1) by congruence.
rewrite H0. cbn. split.
* destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
* destruct (IHq2 s1 s1 H2) as [? [? ?]]. tauto.
+ assert (q' = s0) by congruence.
rewrite H0.
destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
+ assert (p' = s) by congruence.
rewrite H0.
destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
+ assert (q' = AndQ s0 s1) by congruence.
rewrite H0. cbn. split.
* destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
* destruct (IHq2 s1 s1 H2) as [? [? ?]]. tauto.
+ assert (p' = s) by congruence.
rewrite H0.
destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
+ assert (q' = s0) by congruence.
rewrite H0.
destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
+ admit.
+ admit.
+ intros H. assert (p' = AndQ s s0) by congruence.
rewrite H0. cbn. split.
* destruct (IHq1 s s0 H1) as [? [? ?]]. tauto.
* destruct (IHq2 s0 s0 H2) as [? [? ?]]. tauto.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
- cbn. repeat split; congruence.
Admitted.
Lemma splitPre_correct E (q p' q': SMTLogic) :
(splitPre q = (Some p', Some q') -> eval_smt_logic E p' /\ eval_smt_logic E q')
/\ (splitPre q = (None, Some q') -> eval_smt_logic E q')
/\ (splitPre q = (Some p', None) -> eval_smt_logic E p')
-> eval_smt_logic E q.
Proof.
induction q in p', q' |- *; intros [H1 [H2 H3]].
- destruct (splitPre_LessQ e1 e2) as [H|H]; rewrite H in *.
+ apply H3.
*)
(* TODO: Maybe introduce True as SMTLogic *)
Fixpoint findLow (q: SMTLogic) (x: nat) (lo: Q) : option SMTLogic * option SMTLogic :=
match q with
| LessEqQ (ConstQ c) (VarQ x) => if Qeq_bool c lo then (Some q, None) else (None, Some q)
| AndQ q1 q2 => match findLow q1 x lo with
| (Some q', None) => (Some q', Some q2)
| (Some q', Some q'') => (Some q', Some (AndQ q'' q2))
| (None, _) => match findLow q2 x lo with
| (Some q', None) => (Some q', Some q1)
| (Some q', Some q'') => (Some q', Some (AndQ q1 q''))
| (None , _) => (None, Some q)
end
end
| _ => (None, Some q)
end.
Lemma findLow_correct E v q q' x lo :
E x = Some v -> Q2R lo <= v -> fst (findLow q x lo) = Some q' -> eval_smt_logic E q'.
Proof.
intros H1 H2. induction q; try discriminate.
- cbn. destruct e1, e2; try discriminate.
(* cbn. intros H. assert (eq: q' = LessEqQ (ConstQ r) (VarQ x0)) by congruence.
rewrite eq. cbn. exists (Q2R r). exists v. repeat split; cbn; auto. *)
Abort.
Fixpoint findHi (q: SMTLogic) (x: nat) (hi: Q) : option SMTLogic * option SMTLogic :=
match q with
| LessEqQ (VarQ x) (ConstQ c) => if Qeq_bool c hi then (Some q, None) else (None, Some q)
| AndQ q1 q2 => match findHi q1 x hi with
| (Some q', None) => (Some q', Some q2)
| (Some q', Some q'') => (Some q', Some (AndQ q'' q2))
| (None, _) => match findHi q2 x hi with
| (Some q', None) => (Some q', Some q1)
| (Some q', Some q'') => (Some q', Some (AndQ q1 q''))
| (None , _) => (None, Some q)
end
end
| _ => (None, Some q)
end.
Lemma findHi_correct E v q q' x hi :
E x = Some v -> v <= Q2R hi -> fst (findHi q x hi) = Some q' -> eval_smt_logic E q'.
Admitted.
Definition findLowHi (q: SMTLogic) (x: nat) (iv: intv) :=
match findLow q x (fst iv) with
| (Some ql, Some q') => match findHi q' x (snd iv) with
| (Some qh, res) => (Some (AndQ ql qh), res)
| _ => (None, None) (* error occured *)
end
| _ => (None, None) (* error occured *)
end.
Definition foldFnc (el: expr Q * intv) (qs: option SMTLogic * option SMTLogic) :=
match el with
| (Var _ x, iv) =>
match qs with
| (None, Some q) => findLowHi q x iv
| (Some q', Some q) => match findLowHi q x iv with
| (Some q'', rest) => (Some (AndQ q'' q'), rest)
| _ => (None, None)
end
| _ => qs
end
| _ => qs
end.
Definition splitPre (P: FloverMap.t intv) q :=
List.fold_right foldFnc (None, Some q) (FloverMap.elements P).
Definition eval_precond E (P: FloverMap.t intv) :=
forall x lo hi, (List.In (Var Q x, (lo, hi)) (FloverMap.elements P)) -> exists vR: R,
E x = Some vR /\ FloverMap.find (Var Q x) P = Some (lo, hi)
/\ Q2R lo <= vR <= Q2R hi.
Lemma splitPre_correct E P q q' :
fst(splitPre P q) = Some q' -> eval_smt_logic E q' -> eval_precond E P.
Proof.
unfold splitPre, eval_precond.
induction (FloverMap.elements P) in q' |- *.
- cbn. tauto.
- cbn. intros H H' x lo hi [eq | tail].
+ admit.
+ destruct (List.fold_right foldFnc (None, Some q) l) as [[q''|] ?].
* apply (IHl q''); auto.
cbn in H. admit.
* destruct o, a, k; cbn in H; try discriminate.
Abort.
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