Commit ed34d15e authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix checker rewrites list. Did not contain interval negation before which led...

Fix checker rewrites list. Did not contain interval negation before which led to computation getting stuck on subtraction benchmarks
parent 6633ae37
(* Define a list containing all defined functions, that need to be unfolded while evaluating *)
let Checker_Rewrites =
[CertificateChecker;validIntervalbounds; validErrorbound;
maxAbsFun; isSupersetInterval; multInterval; subtractInterval; widenInterval; mkInterval;
maxAbsFun; isSupersetInterval; multInterval; subtractInterval; widenInterval; negateInterval; mkInterval;
addInterval; absIntvUpd; min4; max4; machineEpsilon; IVlo; IVhi];;
(* Define a list containing only the distincness and injectivity properties, for simplifying conditionals *)
......@@ -38,35 +38,7 @@ let rec DEPTH_PAT_CONV pattern conv term :thm =
|Abs (x,t) -> ABS_CONV (DEPTH_PAT_CONV pattern conv) term
|_ -> REFL term;;
(** OLD DAISY CONVERSION, NOT USED ANYMORE
let DAISY_CONV theRewrites term =
let allRewrites = List.concat [Checker_Rewrites; theRewrites; DistinctnessAndInjectivity] in
let unfolded_defs = REWRITE_CONV allRewrites term in
let no_conditionals = CONV_RULE CONDS_ELIM_CONV unfolded_defs in
let evaluated_conditions =
CONV_RULE
(REPEATC
(CHANGED_CONV
(ONCE_DEPTH_CONV
(CHANGED_CONV
(TRY_CONV NUM_REDUCE_CONV THENC TRY_CONV REAL_RAT_RED_CONV))))) no_conditionals in
let no_lets = CONV_RULE ((REPEATC (CHANGED_CONV (ONCE_DEPTH_CONV let_CONV))) THENC SIMP_CONV[FST;SND]) evaluated_conditions in
CONV_RULE
(REPEATC
(CHANGED_CONV
(ONCE_DEPTH_CONV
(CHANGED_CONV
(TRY_CONV REAL_RAT_ABS_CONV
THENC TRY_CONV REAL_RAT_MAX_CONV
THENC TRY_CONV REAL_RAT_MIN_CONV
THENC TRY_CONV REAL_RAT_RED_CONV
)
)
)
)
) no_lets;; **)
(** Benchmarking function, aply conversion to thm using CONV_RULE and compute time **)
(** Benchmarking function, apply conversion to thm using CONV_RULE and compute time **)
let step conv t = time (CONV_RULE conv) t;;
(** Simplifing conversions **)
......
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