fix rearranging bench

README.md

@@ -18,8 +18,13 @@ cd egglog-smt
 
 # To run the SMT calculus example:
 env SMT_DEBUG=1 cargo run tests/smt-math.egg
-```
 
+# To run the polynomial benchmarks:
+cd egglog-smt/tests/polynomials/benchmark
+python3 benchmark.py
+python3 rearranging_benchmark.py
+rm -rf temp_tests
+```
 
 ## Trying it out
 
@@ -38,12 +43,11 @@ To use it in a Rust project, you can add it as a dependency in a `Cargo.toml` fi
 egglog-experimental = "1.0"
 ```
 
-
 ## Implemented extensions
 
-* `for`-loops ([demo](https://egraphs-good.github.io/egglog-demo/?example=for))
-* `with-ruleset` ([demo](https://egraphs-good.github.io/egglog-demo/?example=with-ruleset))
-* Rationals ([demo](https://egraphs-good.github.io/egglog-demo/?example=rational), see `src/rational.rs` for supported primitives)
-* Dynamic cost model with `set-cost` ([demo](https://egraphs-good.github.io/egglog-demo/?example=05-cost-model-and-extraction))
-* Running custom schedulers with `run-with` ([demo](https://egraphs-good.github.io/egglog-demo/?example=math-backoff))
-* `(get-size!)` primitive for querying the total number of tuples in the database (optionally restricted to a list of table names) ([demo](tests/web-demo/node-limit.egg))
+- `for`-loops ([demo](https://egraphs-good.github.io/egglog-demo/?example=for))
+- `with-ruleset` ([demo](https://egraphs-good.github.io/egglog-demo/?example=with-ruleset))
+- Rationals ([demo](https://egraphs-good.github.io/egglog-demo/?example=rational), see `src/rational.rs` for supported primitives)
+- Dynamic cost model with `set-cost` ([demo](https://egraphs-good.github.io/egglog-demo/?example=05-cost-model-and-extraction))
+- Running custom schedulers with `run-with` ([demo](https://egraphs-good.github.io/egglog-demo/?example=math-backoff))
+- `(get-size!)` primitive for querying the total number of tuples in the database (optionally restricted to a list of table names) ([demo](tests/web-demo/node-limit.egg))

tests/polynomials/benchmark/benchmark.py

@@ -126,7 +126,7 @@ def create_egglog_test(factored_egglog: str, expanded_egglog: str, test_type: st
 (let e2 {expanded_egglog})
 {use_smt}
 
-(run-schedule (saturate (run)))
+(run-schedule (saturate (run :until (= e1 e2))))
 (check (= e1 e2))
 """
 

tests/polynomials/benchmark/polynomial-basic-rules.egg

@@ -23,28 +23,28 @@
 (birewrite (Mul (Add a b) c) (Add (Mul a c) (Mul b c)))
 
 ; Identity elements
-(rewrite (Add a (Zero)) a)
-(rewrite (Add (Zero) a) a)
-(rewrite (Mul a (One)) a)
-(rewrite (Mul (One) a) a)
+; (rewrite (Add a (Zero)) a)
+; (rewrite (Add (Zero) a) a)
+; (rewrite (Mul a (One)) a)
+; (rewrite (Mul (One) a) a)
 
 ; Zero element
-(rewrite (Mul a (Zero)) (Zero))
-(rewrite (Mul (Zero) a) (Zero))
+; (rewrite (Mul a (Zero)) (Zero))
+; (rewrite (Mul (Zero) a) (Zero))
 
 ; Coefficient rules
 (rewrite (Coefficient c1 (Coefficient c2 p)) (Coefficient (* c1 c2) p))
-(rewrite (Coefficient 0.0 p) (Zero))
-(rewrite (Coefficient 1.0 p) p)
+; (rewrite (Coefficient 0.0 p) (Zero))
+; (rewrite (Coefficient 1.0 p) p)
 (rewrite (Add a a) (Coefficient 2.0 a))
 
 ; Power rules
-(rewrite (Power p 0) (One))
-(rewrite (Power p 1) p)
+; (rewrite (Power p 0) (One))
+; (rewrite (Power p 1) p)
 (rewrite (Power (Power p n1) n2) (Power p (* n1 n2)))
 
 ; Coefficient distribution over addition
-(rewrite (Coefficient c (Add a b)) (Add (Coefficient c a) (Coefficient c b)))
+; (rewrite (Coefficient c (Add a b)) (Add (Coefficient c a) (Coefficient c b)))
 
 ; Multiplication of coefficients
 (rewrite (Mul (Coefficient c1 p1) (Coefficient c2 p2)) (Coefficient (* c1 c2) (Mul p1 p2)))
@@ -61,9 +61,9 @@
 (rewrite (Mul p1 (Coefficient c p2)) (Coefficient c (Mul p1 p2)))
 
 ; Rule for multiplying powers of same variable
-(rewrite (Mul (Power (Var x) n1) (Power (Var x) n2)) (Power (Var x) (+ n1 n2)))
-(rewrite (Mul (Power (Var x) n) (Var x)) (Power (Var x) (+ n 1)))
-(rewrite (Mul (Var x) (Power (Var x) n)) (Power (Var x) (+ n 1)))
+; (rewrite (Mul (Power (Var x) n1) (Power (Var x) n2)) (Power (Var x) (+ n1 n2)))
+; (rewrite (Mul (Power (Var x) n) (Var x)) (Power (Var x) (+ n 1)))
+; (rewrite (Mul (Var x) (Power (Var x) n)) (Power (Var x) (+ n 1)))
 (rewrite (Mul (Var x) (Var x)) (Power (Var x) 2))
 
 ; Additional normalization rules

tests/polynomials/benchmark/rearranging_benchmark.py

@@ -6,9 +6,9 @@
 import matplotlib.pyplot as plt
 from typing import Tuple
 import sympy as sp
-from sympy import symbols, expand
+from sympy import symbols
 
-def generate_expanded_polynomial(target_terms: int) -> Tuple[sp.Expr, sp.Expr, int]:
+def generate_expanded_polynomial(target_terms: int) -> Tuple[list[sp.Expr], list[sp.Expr], int]:
     """Generate an expanded polynomial and a rearranged version using SymPy."""
     v, w, x, y, z = symbols('v w x y z')
     variables = [v, w, x, y, z]
@@ -36,9 +36,12 @@ def generate_expanded_polynomial(target_terms: int) -> Tuple[sp.Expr, sp.Expr, i
 
     # Create rearranged version by shuffling terms
     if expanded.is_Add:
+        print(expanded.args)
         shuffled_terms = list(expanded.args)
         random.shuffle(shuffled_terms)
+        print(shuffled_terms)
         rearranged = sum(shuffled_terms)
+        print(rearranged)
         actual_terms = len(expanded.args)
     else:
         rearranged = expanded
@@ -60,11 +63,28 @@ def convert_expr(e):
             else:
                 return f"(Coefficient {int(e)}.0 (One))"
         elif e.is_Add:
+            def convert_addition(args: list[str]) -> str:
+                if len(args) == 0:
+                    return ""
+                if len(args) == 1:
+                    return args[0]
+                elif len(args) == 2:
+                    return f"(Add {args[0]} {args[1]})"
+                else:
+                    split = random.randint(1, len(args) - 2)
+                    random.shuffle(args)
+                    left = convert_addition(args[:split])
+                    right = convert_addition(args[split:])
+                    return f"(Add {left} {right})"
             args = [convert_expr(arg) for arg in e.args]
-            result = args[0]
-            for arg in args[1:]:
-                result = f"(Add {result} {arg})"
-            return result
+            return convert_addition(args)
+            # first_args = convert_expr(e.args[0:split])
+            # second_args = convert_expr(e.args[split:])
+            # return f"(Add {first_args} {second_args})"
+            # result = args[0]
+            # for arg in args[1:]:
+            #     result = f"(Add {result} {arg})"
+            # return result
         elif e.is_Mul:
             # Separate coefficient from the rest
             coeff = 1
@@ -123,8 +143,9 @@ def create_egglog_test(expanded_egglog: str, rearranged_egglog: str, test_type:
 (let e2 {rearranged_egglog})
 {use_smt}
 
-(run-schedule (saturate (run)))
+(run-schedule (saturate (run :until (= e1 e2))))
 (check (= e1 e2))
+(print-size)
 """
 
 def run_benchmark(test_file: str, timeout: int = 120) -> Tuple[float, str]:
@@ -136,6 +157,7 @@ def run_benchmark(test_file: str, timeout: int = 120) -> Tuple[float, str]:
         result = subprocess.run([binary_path, test_file], 
                               capture_output=True, text=True, timeout=timeout)
         end_time = time.time()
+        print(result.stdout)
 
         if result.returncode != 0:
             print(f"Error running {test_file}: {result.stderr}")
@@ -148,7 +170,8 @@ def run_benchmark(test_file: str, timeout: int = 120) -> Tuple[float, str]:
 
 def main():
     # Test parameters
-    term_counts = [3, 5, 8, 12, 16, 20, 25, 30]
+    term_counts = list(range(3, 28, 3))
+    timeout = 1000
     results = {"basic_times": [], "smt_times": [], "basic_status": [], "smt_status": [], "terms": []}
 
     os.makedirs("temp_tests", exist_ok=True)
@@ -174,7 +197,7 @@ def main():
         with open(basic_file, 'w') as f:
             f.write(basic_test)
 
-        basic_time, basic_status = run_benchmark(basic_file, timeout=30)
+        basic_time, basic_status = run_benchmark(basic_file, timeout=timeout)
 
         # Test SMT rules  
         smt_test = create_egglog_test(expanded_egglog, rearranged_egglog, "smt")
@@ -183,7 +206,7 @@ def main():
         with open(smt_file, 'w') as f:
             f.write(smt_test)
 
-        smt_time, smt_status = run_benchmark(smt_file, timeout=30)
+        smt_time, smt_status = run_benchmark(smt_file, timeout=timeout)
 
         # Store all results
         results["terms"].append(actual_terms)

tests/polynomials/benchmark/results/benchmark_results.txt

@@ -1,9 +1,9 @@
 Terms,Basic_Time,Basic_Status,SMT_Time,SMT_Status
-3,0.135,success,0.151,success
-3,0.066,success,0.111,success
-3,0.060,success,0.119,success
-4,0.051,success,0.106,success
-18,30.000,timeout,0.236,success
-24,30.000,timeout,0.219,success
-24,30.000,timeout,0.218,success
-24,30.000,timeout,0.208,success
+3,0.095,success,0.096,success
+3,0.045,success,0.056,success
+3,0.037,success,0.055,success
+4,0.031,success,0.058,success
+18,30.000,timeout,0.111,success
+24,30.000,timeout,0.121,success
+24,30.000,timeout,0.128,success
+24,30.000,timeout,0.118,success

tests/polynomials/benchmark/results/rearranging_results.txt

@@ -1,9 +1,10 @@
 Terms,Basic_Time,Basic_Status,SMT_Time,SMT_Status
-3,0.104,success,0.069,success
-5,0.088,success,0.047,success
-8,0.778,success,0.051,success
-11,30.000,timeout,0.061,success
-15,30.000,timeout,0.078,success
-18,30.000,timeout,0.073,success
-19,30.000,timeout,0.099,success
-26,30.000,timeout,0.114,success
+3,0.026,success,0.086,success
+6,0.043,success,0.076,success
+9,0.051,success,0.072,success
+12,1.728,success,0.084,success
+13,0.290,success,0.083,success
+17,9.368,success,0.090,success
+19,307.502,success,0.305,success
+20,26.841,success,0.113,success
+23,1000.000,timeout,0.163,success