diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/hls/Scheduleoracle.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/hls/Scheduleoracle.v b/src/hls/Scheduleoracle.v index 2c60e96..1625238 100644 --- a/src/hls/Scheduleoracle.v +++ b/src/hls/Scheduleoracle.v @@ -362,6 +362,16 @@ Proof. congruence. Qed. +Definition empty : forest := Rtree.empty _. + +Lemma get_empty: + forall r, empty#r = Ebase r. +Proof. + intros r. unfold get_forest. + destruct (Rtree.get r empty) eqn:Heq; auto. + rewrite Rtree.gempty in Heq. discriminate. +Qed. + (*| We define the top-level oracle that will check if two basic blocks are equivalent after a scheduling transformation. |