Commit 935df721 authored by Heiko Becker's avatar Heiko Becker

Fix CertificateChecker such that it suffices to require import this file in Coq

parent 7162dd60
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.PreconditionValidation.
Require Export Coq.QArith.QArith.
Require Export Daisy.Infra.ExpressionAbbrevs.
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
andb (andb (validIntervalbounds e absenv P) (approximatesPrecond e absenv P)) (validErrorbound e absenv).
......
Require Import Coq.QArith.QArith.
Require Import Daisy.ErrorValidation Daisy.Infra.RationalConstruction Daisy.Infra.ExpressionAbbrevs.
Require Import Daisy.CertificateChecker.
(*Require Import Daisy.ErrorValidation Daisy.Infra.RationalConstruction Daisy.Infra.ExpressionAbbrevs. *)
(*
TODO: update according to:
[ Info ]
......@@ -72,6 +72,8 @@ Definition lowerBoundAddUCst:Q := 1157 # 5.
Definition upperBoundAddUCst:Q := 2157 # 5.
Definition errAddUCst := (7771411516990528329)#(81129638414606681695789005144064).
Definition precondition:precond := fun n:nat => (- 100#1, 100#1).
Definition absEnv : analysisResult :=
fun (e:exp Q) =>
match e with
......@@ -80,9 +82,9 @@ Definition absEnv : analysisResult :=
|Binop _ _ _ => (lowerBoundAddUCst,upperBoundAddUCst,errAddUCst)
| _ => (0,0,0) end.
Eval compute in validErrorbound valCst absEnv.
Eval compute in validErrorbound varU absEnv.
Eval compute in validErrorbound valCstAddVarU absEnv.
Eval compute in CertificateChecker valCst absEnv precondition.
Eval compute in CertificateChecker varU absEnv precondition.
Eval compute in CertificateChecker valCstAddVarU absEnv precondition.
(* UNUSED STUFF BEGINS HERE
(** The added assertion becomes the precondition for us **)
......
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