rewriter: log new top level vars to human rule trace

conjure_oxide/tests/integration/basic/div/04/input-expected-rule-trace-human.txt

@@ -43,6 +43,8 @@ Not((c != 0)),
 (a != SafeDiv(b, c)), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 (a != __0) 
+with new top level expressions:
+  __0 =aux SafeDiv(b, c)
 
 --
 

conjure_oxide/tests/integration/basic/div/05/div-05-expected-rule-trace-human.txt

@@ -25,6 +25,8 @@ And([(c != 0)]),
 (a != SafeDiv(b, c)), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 (a != __0) 
+with new top level expressions:
+  __0 =aux SafeDiv(b, c)
 
 --
 

conjure_oxide/tests/integration/basic/div/06/div-06-expected-rule-trace-human.txt

@@ -43,6 +43,8 @@ Not((c != 0)),
 (a != SafeDiv(b, c)), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 (a != __0) 
+with new top level expressions:
+  __0 =aux SafeDiv(b, c)
 
 --
 

conjure_oxide/tests/integration/basic/max/02/input-expected-rule-trace-human.txt

@@ -1,6 +1,10 @@
 Max([2, a]), 
    ~~> max_to_var ([("Base", 100)]) 
 __0 
+with new top level expressions:
+  (__0 >= 2)
+  (__0 >= a)
+  Or([(__0 = 2), (__0 = a)])
 
 --
 

conjure_oxide/tests/integration/basic/min/01/input-expected-rule-trace-human.txt

@@ -1,6 +1,10 @@
 Min([a, b]), 
    ~~> min_to_var ([("Base", 2000)]) 
 __0 
+with new top level expressions:
+  (__0 <= a)
+  (__0 <= b)
+  Or([(__0 = a), (__0 = b)])
 
 --
 

conjure_oxide/tests/integration/basic/min/02/input-expected-rule-trace-human.txt

@@ -1,6 +1,10 @@
 Min([a, b]), 
    ~~> min_to_var ([("Base", 2000)]) 
 __0 
+with new top level expressions:
+  (__0 <= a)
+  (__0 <= b)
+  Or([(__0 = a), (__0 = b)])
 
 --
 

conjure_oxide/tests/integration/basic/min/03/input-expected-rule-trace-human.txt

@@ -1,6 +1,10 @@
 Min([a, b]), 
    ~~> min_to_var ([("Base", 2000)]) 
 __0 
+with new top level expressions:
+  (__0 <= a)
+  (__0 <= b)
+  Or([(__0 = a), (__0 = b)])
 
 --
 

conjure_oxide/tests/integration/basic/min/04/input-expected-rule-trace-human.txt

@@ -1,6 +1,10 @@
 Min([a, b]), 
    ~~> min_to_var ([("Base", 2000)]) 
 __0 
+with new top level expressions:
+  (__0 <= a)
+  (__0 <= b)
+  Or([(__0 = a), (__0 = b)])
 
 --
 

conjure_oxide/tests/integration/basic/min/05/input-expected-rule-trace-human.txt

@@ -1,6 +1,10 @@
 Min([a, b]), 
    ~~> min_to_var ([("Base", 2000)]) 
 __0 
+with new top level expressions:
+  (__0 <= a)
+  (__0 <= b)
+  Or([(__0 = a), (__0 = b)])
 
 --
 

conjure_oxide/tests/integration/basic/mod/04/input-expected-rule-trace-human.txt

@@ -43,6 +43,8 @@ Not((c != 0)),
 (a != SafeMod(b,c)), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 (a != __0) 
+with new top level expressions:
+  __0 =aux SafeMod(b,c)
 
 --
 

conjure_oxide/tests/integration/basic/mod/05/mod-05-expected-rule-trace-human.txt

@@ -25,6 +25,8 @@ And([(c != 0)]),
 (a != SafeMod(b,c)), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 (a != __0) 
+with new top level expressions:
+  __0 =aux SafeMod(b,c)
 
 --
 

conjure_oxide/tests/integration/basic/mod/06/mod-06-expected-rule-trace-human.txt

@@ -43,6 +43,8 @@ Not((c != 0)),
 (a != SafeMod(b,c)), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 (a != __0) 
+with new top level expressions:
+  __0 =aux SafeMod(b,c)
 
 --
 

conjure_oxide/tests/integration/basic/neg/02-nested-neg/input-expected-rule-trace-human.txt

@@ -25,6 +25,8 @@ And([(z != 0)]),
 SafeDiv(-(y), z), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 SafeDiv(__0, z) 
+with new top level expressions:
+  __0 =aux -(y)
 
 --
 

conjure_oxide/tests/integration/basic/neg/03-negated-expression/input-expected-rule-trace-human.txt

@@ -37,6 +37,8 @@ And([(z != 0)]),
 (x = -(SafeDiv(y, z))), 
    ~~> flatten_minuseq ([("Minion", 4400)]) 
 MinusEq(x,__0) 
+with new top level expressions:
+  __0 =aux SafeDiv(y, z)
 
 --
 

conjure_oxide/tests/integration/basic/neg/04-negated-expression-nested/input-expected-rule-trace-human.txt

@@ -79,12 +79,16 @@ And([(x = SafeDiv(-(SafeDiv(y, z)), z)), (z != 0), (z != 0)])
 SafeDiv(-(SafeDiv(y, z)), z), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 SafeDiv(__0, z) 
+with new top level expressions:
+  __0 =aux -(SafeDiv(y, z))
 
 --
 
 __0 =aux -(SafeDiv(y, z)), 
    ~~> flatten_minuseq ([("Minion", 4400)]) 
 MinusEq(__0,__1) 
+with new top level expressions:
+  __1 =aux SafeDiv(y, z)
 
 --
 

conjure_oxide/tests/integration/basic/neg/05-sum/input-expected-rule-trace-human.txt

@@ -1,6 +1,8 @@
 Sum([-(y), z]), 
    ~~> flatten_vecop ([("Minion", 4400)]) 
 Sum([__0, z]) 
+with new top level expressions:
+  __0 =aux -(y)
 
 --
 

conjure_oxide/tests/integration/basic/neg/06-sum-nested/input-expected-rule-trace-human.txt

@@ -49,6 +49,9 @@ a
 Sum([-(y), -(z), -1, a, b]), 
    ~~> flatten_vecop ([("Minion", 4400)]) 
 Sum([__0, __1, -1, a, b]) 
+with new top level expressions:
+  __0 =aux -(y)
+  __1 =aux -(z)
 
 --
 

conjure_oxide/tests/integration/bugs/sm600-non-terminating-min/input-expected-rule-trace-human.txt

@@ -1,6 +1,8 @@
 Sum([Min([a, b]), 6]), 
    ~~> flatten_vecop ([("Minion", 4400)]) 
 Sum([__0, 6]) 
+with new top level expressions:
+  __0 =aux Min([a, b])
 
 --
 
@@ -13,6 +15,10 @@ SumLeq([__0, 6], 10)
 Min([a, b]), 
    ~~> min_to_var ([("Base", 2000)]) 
 __1 
+with new top level expressions:
+  (__1 <= a)
+  (__1 <= b)
+  Or([(__1 = a), (__1 = b)])
 
 --
 

conjure_oxide/tests/integration/experiment/works/max2/input-expected-rule-trace-human.txt

@@ -1,6 +1,8 @@
 Sum([Max([a, b]), 1]), 
    ~~> flatten_vecop ([("Minion", 4400)]) 
 Sum([__0, 1]) 
+with new top level expressions:
+  __0 =aux Max([a, b])
 
 --
 
@@ -19,6 +21,10 @@ And([SumLeq([__0, 1], x), SumGeq([__0, 1], x)])
 Max([a, b]), 
    ~~> max_to_var ([("Base", 100)]) 
 __1 
+with new top level expressions:
+  (__1 >= a)
+  (__1 >= b)
+  Or([(__1 = a), (__1 = b)])
 
 --
 
@@ -43,6 +49,10 @@ Ineq(b, __1, 0)
 Max([a, b]), 
    ~~> max_to_var ([("Base", 100)]) 
 __2 
+with new top level expressions:
+  (__2 >= a)
+  (__2 >= b)
+  Or([(__2 = a), (__2 = b)])
 
 --
 

conjure_oxide/tests/integration/minion_constraints/div_undefzero-03-nested/input-expected-rule-trace-human.txt

@@ -67,12 +67,16 @@ And([(SafeDiv(x, SafeDiv(y, z)) = 10), (SafeDiv(y, z) != 0), (z != 0)])
 SafeDiv(x, SafeDiv(y, z)), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 SafeDiv(x, __0) 
+with new top level expressions:
+  __0 =aux SafeDiv(y, z)
 
 --
 
 (SafeDiv(y, z) != 0), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 (__1 != 0) 
+with new top level expressions:
+  __1 =aux SafeDiv(y, z)
 
 --
 

conjure_oxide/tests/integration/minion_constraints/div_undefzero-04-nested-neq/input-expected-rule-trace-human.txt

@@ -67,18 +67,24 @@ And([(SafeDiv(x, SafeDiv(y, z)) != 10), (SafeDiv(y, z) != 0), (z != 0)])
 (SafeDiv(x, SafeDiv(y, z)) != 10), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 (__0 != 10) 
+with new top level expressions:
+  __0 =aux SafeDiv(x, SafeDiv(y, z))
 
 --
 
 (SafeDiv(y, z) != 0), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 (__1 != 0) 
+with new top level expressions:
+  __1 =aux SafeDiv(y, z)
 
 --
 
 SafeDiv(x, SafeDiv(y, z)), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 SafeDiv(x, __2) 
+with new top level expressions:
+  __2 =aux SafeDiv(y, z)
 
 --
 

conjure_oxide/tests/integration/minion_constraints/div_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt

@@ -97,12 +97,16 @@ Or([(SafeDiv(x, SafeDiv(y, z)) != 10), (SafeDiv(y, z) = 0), (z = 0)])
 (SafeDiv(x, SafeDiv(y, z)) != 10), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 (__0 != 10) 
+with new top level expressions:
+  __0 =aux SafeDiv(x, SafeDiv(y, z))
 
 --
 
 SafeDiv(x, SafeDiv(y, z)), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 SafeDiv(x, __1) 
+with new top level expressions:
+  __1 =aux SafeDiv(y, z)
 
 --
 

conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-03-nested/input-expected-rule-trace-human.txt

@@ -67,12 +67,16 @@ And([(SafeMod(x,SafeMod(y,z)) = 3), (SafeMod(y,z) != 0), (z != 0)])
 SafeMod(x,SafeMod(y,z)), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 SafeMod(x,__0) 
+with new top level expressions:
+  __0 =aux SafeMod(y,z)
 
 --
 
 (SafeMod(y,z) != 0), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 (__1 != 0) 
+with new top level expressions:
+  __1 =aux SafeMod(y,z)
 
 --
 

conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-04-nested-neq/input-expected-rule-trace-human.txt

@@ -67,18 +67,24 @@ And([(SafeMod(x,SafeMod(y,z)) != 3), (SafeMod(y,z) != 0), (z != 0)])
 (SafeMod(x,SafeMod(y,z)) != 3), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 (__0 != 3) 
+with new top level expressions:
+  __0 =aux SafeMod(x,SafeMod(y,z))
 
 --
 
 (SafeMod(y,z) != 0), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 (__1 != 0) 
+with new top level expressions:
+  __1 =aux SafeMod(y,z)
 
 --
 
 SafeMod(x,SafeMod(y,z)), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 SafeMod(x,__2) 
+with new top level expressions:
+  __2 =aux SafeMod(y,z)
 
 --
 

conjure_oxide/tests/integration/minion_constraints/modulo_undefzero-05-nested-noteq/input-expected-rule-trace-human.txt

@@ -97,12 +97,16 @@ Or([(SafeMod(x,SafeMod(y,z)) != 3), (SafeMod(y,z) = 0), (z = 0)])
 (SafeMod(x,SafeMod(y,z)) != 3), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 (__0 != 3) 
+with new top level expressions:
+  __0 =aux SafeMod(x,SafeMod(y,z))
 
 --
 
 SafeMod(x,SafeMod(y,z)), 
    ~~> flatten_binop ([("Minion", 4400)]) 
 SafeMod(x,__1) 
+with new top level expressions:
+  __1 =aux SafeMod(y,z)
 
 --
 

crates/conjure_core/src/rule_engine/rewriter_common.rs

@@ -3,6 +3,7 @@
 use super::{resolve_rules::ResolveRulesError, Reduction, Rule};
 use crate::ast::{pretty::pretty_vec, Expression};
 
+use itertools::Itertools;
 use thiserror::Error;
 use tracing::{info, trace};
 
@@ -28,13 +29,28 @@ pub fn log_rule_application(result: &RuleResult, initial_expression: &Expression
         red.new_expression
     );
 
+    let top_level_str = if !red.new_top.is_empty() {
+        let mut exprs: Vec<String> = vec![];
+
+        for expr in &red.new_top {
+            exprs.push(format!("  {}", expr));
+        }
+
+        let exprs = exprs.iter().join("\n");
+
+        format!("with new top level expressions:\n{}\n", exprs)
+    } else {
+        String::new()
+    };
+
     trace!(
         target: "rule_engine_human",
-        "{}, \n   ~~> {} ({:?}) \n{} \n\n--\n",
+        "{}, \n   ~~> {} ({:?}) \n{} \n{}\n--\n",
         initial_expression,
         rule.name,
         rule.rule_sets,
         red.new_expression,
+        top_level_str
     );
 }