Merge pull request #732 from egraphs-good/oflatt-more-query-opt

Upgrade egglog version

Cargo.toml

@@ -9,7 +9,7 @@ name = "files"
 
 
 [dependencies]
-egglog = { git = "https://github.com/egraphs-good/egglog", rev = "246b195" }
+egglog = { git = "https://github.com/egraphs-good/egglog", rev = "161a36f" }
 egraph-serialize = "0.2.0"
 log = "0.4.19"
 thiserror = "1"

dag_in_context/Cargo.toml

@@ -6,7 +6,7 @@ edition = "2021"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-egglog = { git = "https://github.com/egraphs-good/egglog", rev = "246b195" }
+egglog = { git = "https://github.com/egraphs-good/egglog", rev = "161a36f" }
 smallvec = "1.11.1"
 strum = "0.25"
 strum_macros = "0.25"

dag_in_context/src/from_egglog.rs

@@ -50,7 +50,7 @@ impl<'a> FromEgglog<'a> {
             Constant::Bool(*boolean)
           }
           ("Float", [lit]) => {
-            let Term::Lit(Literal::F64(f)) = self.termdag.get(*lit) else {
+            let Term::Lit(Literal::Float(f)) = self.termdag.get(*lit) else {
               panic!("Invalid float: {:?}", lit)
             };
             Constant::Float(*f)

dag_in_context/src/greedy_dag_extractor.rs

@@ -433,7 +433,7 @@ impl<'a> Extractor<'a> {
             } else if let Ok(n) = op.parse::<i64>() {
                 self.termdag.lit(ast::Literal::Int(n))
             } else if let Ok(f) = op.parse::<f64>() {
-                self.termdag.lit(ast::Literal::F64(OrderedFloat::from(f)))
+                self.termdag.lit(ast::Literal::Float(OrderedFloat::from(f)))
             } else if op == "true" {
                 self.termdag.lit(ast::Literal::Bool(true))
             } else if op == "false" {

dag_in_context/src/interval_analysis.egg

@@ -9,8 +9,8 @@
   (bound-min Bound Bound))
 
 ; bound tables
-(function lo-bound (Expr) Bound :unextractable :merge (bound-max old new))
-(function hi-bound (Expr) Bound :unextractable :merge (bound-min old new))
+(function lo-bound (Expr) Bound :merge (bound-max old new))
+(function hi-bound (Expr) Bound :merge (bound-min old new))
 
 ; if lo > hi, we have proven that this code is dead (as long as all our rules are sound)
 ; In this case, interval analysis might start going crazy and fail to saturate

dag_in_context/src/optimizations/conditional_invariant_code_motion.egg

@@ -1,4 +1,18 @@
 (ruleset cicm)
+(ruleset cicm-index)
+
+(relation InvCodeMotionCandidate (Expr Expr))
+
+(rule (
+        (= (TCPair t1 c1) (ExtractedExpr e1))
+        (= (TCPair t1 c2) (ExtractedExpr e2))
+        (ContextOf e1 (InIf true pred1 orig_ins3))
+        (ContextOf e2 (InIf false pred2 orig_ins4))
+        (!= e1 e2)
+     )
+     ((InvCodeMotionCandidate e1 e2))
+     :ruleset cicm-index)
+
 
 (rule (
         (= if_e (If pred orig_ins thn els))
@@ -21,6 +35,7 @@
         (ContextOf e2 (InIf false pred orig_ins))
 
         (= t1 t2)
+        (= orig_ins_len (TypeList-length tylist))
       )
       (
         ; pull the term out to the outer context
@@ -29,7 +44,6 @@
         ; Add it as an input to the new if
         (let new_ins (Concat orig_ins (Single new_term)))
         (let new_ins_ty (TupleT (TLConcat tylist (TCons ty (TNil)))))
-        (let orig_ins_len (TypeList-length tylist))
 
         ; New contexts
         (let if_tr (InIf true  pred new_ins))
@@ -67,27 +81,35 @@
       )
     :ruleset cicm)
 
+
+
 (rule (
+        (InvCodeMotionCandidate e1 e2)
         (= if_e (If pred orig_ins thn els))
         (HasArgType thn (TupleT tylist))
         (HasArgType els (TupleT tylist))
         (ContextOf if_e outer_ctx)
 
+        (ContextOf e1 (InIf true pred orig_ins))
+        (ContextOf e2 (InIf false pred orig_ins))
         (= e1 (Bop o x1 y1))
-        (HasType e1 (Base ty))
+
+        (= e2 (Bop o x2 y2))
+
         (= (TCPair t1 c1) (ExtractedExpr e1))
         (> 10 (Expr-size e1))
         (ExprIsPure e1)
-        (ContextOf e1 (InIf true pred orig_ins))
+        (HasType e1 (Base ty))
+
 
-        (= e2 (Bop o x2 y2))
+
         (HasType e2 (Base ty))
         (= (TCPair t2 c2) (ExtractedExpr e2))
         (> 10 (Expr-size e2))
         (ExprIsPure e2)
-        (ContextOf e2 (InIf false pred orig_ins))
 
         (= t1 t2)
+        (= orig_ins_len (TypeList-length tylist))
       )
       (
         ; pull the term out to the outer context
@@ -96,7 +118,6 @@
         ; Add it as an input to the new if
         (let new_ins (Concat orig_ins (Single new_term)))
         (let new_ins_ty (TupleT (TLConcat tylist (TCons ty (TNil)))))
-        (let orig_ins_len (TypeList-length tylist))
 
         ; New contexts
         (let if_tr (InIf true  pred new_ins))

dag_in_context/src/optimizations/conditional_push_in.egg

@@ -8,6 +8,7 @@
         (HasArgType thn (TupleT tylist))
         (HasArgType els (TupleT tylist))
         (HasType x (Base x_ty))
+        (= orig_ins_len (TypeList-length tylist))
       )
       (
         ; New inputs
@@ -23,7 +24,6 @@
         (let arg_fa (Arg new_ins_ty if_fa))
 
         ; SubTuple
-        (let orig_ins_len (TypeList-length tylist))
         (let st_tr (SubTuple arg_tr 0 orig_ins_len))
         (let st_fa (SubTuple arg_fa 0 orig_ins_len))
 
@@ -47,6 +47,7 @@
         (HasArgType thn (TupleT tylist))
         (HasArgType els (TupleT tylist))
         (HasType x (Base x_ty))
+        (= orig_ins_len (TypeList-length tylist))
       )
       (
         ; New inputs
@@ -62,7 +63,6 @@
         (let arg_fa (Arg new_ins_ty if_fa))
 
         ; SubTuple
-        (let orig_ins_len (TypeList-length tylist))
         (let st_tr (SubTuple arg_tr 0 orig_ins_len))
         (let st_fa (SubTuple arg_fa 0 orig_ins_len))
 
@@ -86,6 +86,7 @@
         (HasArgType thn (TupleT tylist))
         (HasArgType els (TupleT tylist))
         (HasType x (Base x_ty))
+        (= orig_ins_len (TypeList-length tylist))
       )
       (
         ; New inputs
@@ -101,7 +102,6 @@
         (let arg_fa (Arg new_ins_ty if_fa))
 
         ; SubTuple
-        (let orig_ins_len (TypeList-length tylist))
         (let st_tr (SubTuple arg_tr 0 orig_ins_len))
         (let st_fa (SubTuple arg_fa 0 orig_ins_len))
 

dag_in_context/src/optimizations/ivt.egg

@@ -4,8 +4,8 @@
 
 (sort IVTRes)
 ;;                              perm passthrough-perm passthrough-type passthrough-type-len
-(function IVTAnalysisRes (Expr Expr             TypeList         i64) IVTRes)
-(function IVTMin (IVTRes IVTRes) IVTRes)
+(constructor IVTAnalysisRes (Expr Expr             TypeList         i64) IVTRes)
+(constructor IVTMin (IVTRes IVTRes) IVTRes)
 
 (rule ((= lhs (IVTMin (IVTAnalysisRes _a _b _c len1) (IVTAnalysisRes _d _e _f len2)))
        (<= len1 len2))

dag_in_context/src/optimizations/loop_invariant.egg

@@ -1,8 +1,8 @@
 ;; Loop Invariant
 
 ;; bool: whether the term in the Expr is an invariant.
-(function is-inv-Expr (Expr Expr) bool :unextractable :merge (or old new))
-(function is-inv-ListExpr (Expr ListExpr) bool :unextractable :merge (or old new))
+(function is-inv-Expr (Expr Expr) bool :merge (or old new))
+(function is-inv-ListExpr (Expr ListExpr) bool :merge (or old new))
 
 ;; in default, when there is a find, set is-inv to false
 (rule ((BodyContainsExpr loop term)
@@ -45,11 +45,11 @@
       ((boundary-Expr loop expr)) :ruleset boundary-analysis)
 
 
-(function hoisted-loop (Expr Expr) bool :unextractable :merge (or old new) )
+(function hoisted-loop (Expr Expr) bool :merge (or old new) )
 (rule ((= loop (DoWhile in pred_out)))
       ((set (hoisted-loop in pred_out) false)) :ruleset always-run)
 
-(function InExtendedLoop (Expr Expr Expr) Assumption)
+(constructor InExtendedLoop (Expr Expr Expr) Assumption)
 
 ;; mock function
 (ruleset loop-inv-motion)

dag_in_context/src/optimizations/loop_strength_reduction.egg

@@ -53,14 +53,13 @@
         (ContextOf old-mul loop-ctx)
 
         (= arg-type (TupleT ty-list))
+        ; n is index of our new, temporary variable d
+        (= n (tuple-length inputs))
     )
     (
         ; Each time we need to update d by the product of the multiplied constant and the loop increment
         (let addend (Bop (Mul) c-out loop-incr-out))
 
-        ; n is index of our new, temporary variable d
-        (let n (tuple-length inputs))
-
         ; Initial value of d is i * c
         (let d-init (Bop (Mul) c-in (Get inputs i)))
 

dag_in_context/src/optimizations/loop_unroll.egg

@@ -72,7 +72,7 @@
 
 ;; loop peeling rule
 ;; Only peel loops that we know iterate < 3 times
-(function LoopPeeledPlaceholder (Expr) Assumption :unextractable)
+(constructor LoopPeeledPlaceholder (Expr) Assumption :unextractable)
 (rule
  ((= lhs (DoWhile inputs outputs))
   (ContextOf lhs ctx)