Merge pull request #620 from egraphs-good/yihozhang-fix-top

Fix ternary operator rules

dag_in_context/src/type_analysis.egg

@@ -73,6 +73,18 @@
        (HasArgType b ty))
       ((HasArgType lhs ty))
       :ruleset type-analysis)
+(rule ((= lhs (Top _ a b c))
+       (HasArgType a ty))
+      ((HasArgType lhs ty))
+      :ruleset type-analysis)
+(rule ((= lhs (Top _ a b c))
+       (HasArgType b ty))
+      ((HasArgType lhs ty))
+      :ruleset type-analysis)
+(rule ((= lhs (Top _ a b c))
+       (HasArgType c ty))
+      ((HasArgType lhs ty))
+      :ruleset type-analysis)
 (rule ((= lhs (Get e _))
        (HasArgType e ty))
       ((HasArgType lhs ty))
@@ -285,7 +297,7 @@
 (rule (
         (= lhs (Top (Write) ptr val state))
         (HasType ptr (Base (PointerT ty)))
-        (HasType val (Base t)) ; TODO need to support pointers to pointers
+        (HasType val (Base ty)) ; TODO need to support pointers to pointers
       )
       ((HasType lhs (Base (StateT)))) ; Write returns ()
       :ruleset type-analysis)

dag_in_context/src/utility/add_context.egg

@@ -36,6 +36,12 @@
 
 
 ;; ######################################### Operators
+(rewrite (AddContext ctx (Top op c1 c2 c3))
+         (Top op
+           (AddContext ctx c1)
+           (AddContext ctx c2)
+           (AddContext ctx c3))
+               :ruleset context)
 (rewrite (AddContext ctx (Bop op c1 c2))
          (Bop op
            (AddContext ctx c1)

dag_in_context/src/utility/drop_at.egg

@@ -38,6 +38,14 @@
       :ruleset drop)
 
 ;; Operators
+(rule ((= lhs (DropAtInternal newty newctx idx (Top op c1 c2 c3)))
+       (ExprIsResolved (Top op c1 c2 c3)))
+      ((DelayedDropUnion lhs (Top op
+            (DropAtInternal newty newctx idx c1)
+            (DropAtInternal newty newctx idx c2)
+            (DropAtInternal newty newctx idx c3))))
+      :ruleset drop)
+
 (rule ((= lhs (DropAtInternal newty newctx idx (Bop op c1 c2)))
        (ExprIsResolved (Bop op c1 c2)))
       ((DelayedDropUnion lhs (Bop op

dag_in_context/src/utility/expr_size.egg

@@ -9,6 +9,10 @@
 (rule ((= expr (Const n ty assum))) 
       ((set (Expr-size expr) 1))  :ruleset always-run)
 
+(rule ((= expr (Top op x y z))
+       (= sum (+ (Expr-size z) (+ (Expr-size y) (Expr-size x)))))
+      ((set (Expr-size expr) (+ sum 1))) :ruleset always-run)
+
 (rule ((= expr (Bop op x y)) 
        (= sum (+ (Expr-size y) (Expr-size x)))) 
       ((set (Expr-size expr) (+ sum 1))) :ruleset always-run)
@@ -59,4 +63,4 @@
 
 (rule ((= expr (Alloc id e state ty)) ;; do state edge's expr should be counted?
         (= sum (Expr-size e))) 
-        ((set (Expr-size expr) (+ sum 1))) :ruleset always-run)
+        ((set (Expr-size expr) (+ sum 1))) :ruleset always-run)

dag_in_context/src/utility/subst.egg

@@ -44,6 +44,14 @@
       :ruleset subst)
 
 ;; Operators
+(rule ((= lhs (Subst assum to (Top op c1 c2 c3)))
+       (ExprIsResolved (Top op c1 c2 c3)))
+      ((DelayedSubstUnion lhs
+         (Top op (Subst assum to c1)
+                 (Subst assum to c2)
+                 (Subst assum to c3))))
+         :ruleset subst)
+
 (rule ((= lhs (Subst assum to (Bop op c1 c2)))
        (ExprIsResolved (Bop op c1 c2)))
       ((DelayedSubstUnion lhs

tests/snapshots/files__gamma_condition_and-optimize.snap

@@ -6,7 +6,7 @@ expression: visualization.result
 .b1_:
   c2_: int = const 0;
   v3_: bool = lt v0 c2_;
-  v4_: bool = gt v0 c2_;
+  v4_: bool = lt c2_ v0;
   c5_: int = const 1;
   c6_: int = const 3;
   v7_: int = id c6_;