From 3d2e95c6049c38a0fbc03a824ce2fc08903517b4 Mon Sep 17 00:00:00 2001 From: oflatt Date: Tue, 6 Feb 2024 16:18:33 -0800 Subject: [PATCH 1/4] add assume test --- tree_assume/src/lib.rs | 1 + tree_assume/src/utility/assume.rs | 23 +++++++++++++++++++++++ tree_assume/src/utility/mod.rs | 1 + 3 files changed, 25 insertions(+) create mode 100644 tree_assume/src/utility/assume.rs create mode 100644 tree_assume/src/utility/mod.rs diff --git a/tree_assume/src/lib.rs b/tree_assume/src/lib.rs index 0d162e9ac..39d8e35b0 100644 --- a/tree_assume/src/lib.rs +++ b/tree_assume/src/lib.rs @@ -9,6 +9,7 @@ mod optimizations; pub mod schema; pub mod schema_helpers; mod to_egglog; +pub(crate) mod utility; pub type Result = std::result::Result<(), egglog::Error>; diff --git a/tree_assume/src/utility/assume.rs b/tree_assume/src/utility/assume.rs new file mode 100644 index 000000000..41471eee2 --- /dev/null +++ b/tree_assume/src/utility/assume.rs @@ -0,0 +1,23 @@ +#[cfg(test)] +use crate::{egglog_test, interpreter::Value, schema::Constant}; + +#[test] +fn test_assume_two_lets() -> crate::Result { + use crate::ast::*; + let expr = tlet(int(1), tlet(add(arg(), arg()), mul(arg(), int(2)))); + let arg1 = assume(inlet(int(1)), arg()); + let addarg1 = add(arg1.clone(), arg1.clone()); + let arg2 = assume(inlet(addarg1), arg()); + let expr2 = tlet(int(1), tlet(add(arg1.clone(), arg1), mul(arg2, int(2)))); + + egglog_test( + &format!("{expr}"), + &format!("(check (= {expr} {expr2}))"), + vec![ + expr.to_program(emptyt(), intt()), + expr2.to_program(emptyt(), intt()), + ], + Value::Tuple(vec![]), + Value::Const(Constant::Int(4)), + ) +} diff --git a/tree_assume/src/utility/mod.rs b/tree_assume/src/utility/mod.rs new file mode 100644 index 000000000..80d9441e9 --- /dev/null +++ b/tree_assume/src/utility/mod.rs @@ -0,0 +1 @@ +pub(crate) mod assume; From c297900e2dc552483320a1f2a2dfa7c8f008f17c Mon Sep 17 00:00:00 2001 From: oflatt Date: Wed, 7 Feb 2024 16:45:54 -0800 Subject: [PATCH 2/4] # This is a combination of 4 commits. # This is the 1st commit message: add assume test # This is the commit message #2: add assume depth notion # This is the commit message #3: top down assume list experiment # This is the commit message #4: finish writing crappy rules --- tree_assume/src/schedule.egg | 4 +- tree_assume/src/schema.egg | 6 ++ tree_assume/src/utility/assume.egg | 111 +++++++++++++++++++++++++++++ 3 files changed, 119 insertions(+), 2 deletions(-) create mode 100644 tree_assume/src/utility/assume.egg diff --git a/tree_assume/src/schedule.egg b/tree_assume/src/schedule.egg index 0e80b3024..1f5762716 100644 --- a/tree_assume/src/schedule.egg +++ b/tree_assume/src/schedule.egg @@ -1,6 +1,6 @@ (run-schedule (repeat 6 + (saturate assume) (saturate always-run) (saturate error-checking) - (run constant_fold) - )) \ No newline at end of file + (run constant_fold))) diff --git a/tree_assume/src/schema.egg b/tree_assume/src/schema.egg index 90b94a1c0..7b32a38d3 100644 --- a/tree_assume/src/schema.egg +++ b/tree_assume/src/schema.egg @@ -173,6 +173,11 @@ ; The term is in a loop with `input` and `pred_output`. ; input pred_output (InLoop Expr Expr) + (InFunc String Expr) + ; Branch of the switch and the predicate + (InSwitch i64 Expr) + ; If the predicate was true, and the predicate + (InIf bool Expr) ; Other assumptions are possible, but not supported yet. ; For example: ; A boolean predicate is true. @@ -183,6 +188,7 @@ ; Assume allows creating context-specific terms. ; e.g. (Assume (InLet (Const (Int 2))) (Arg)) is equal to (Const (Int 2)) (function Assume (Assumption Expr) Expr) +(function AssumeList (Assumption ListExpr) ListExpr) ; ================================= diff --git a/tree_assume/src/utility/assume.egg b/tree_assume/src/utility/assume.egg new file mode 100644 index 000000000..57afa51c7 --- /dev/null +++ b/tree_assume/src/utility/assume.egg @@ -0,0 +1,111 @@ +; This file propogates assume nodes top-down from functions. +; It gives each program path a unique equality relation. +; This can be quite expensive, so be careful running these rules. + +(ruleset assume) + +(sort AssumeList) +; We collect multiple assumes into one AssumeMulti. +; These happen when there are nested `If` or `Switch` statements. +; When it gets to the bottom, we flatten it back out to multiple `Assume` nodes +; for the convenience of other analyses. +(function AssumeMulti (AssumeList Expr) Expr :unextractable) + +(function AssumeCons (Assumption AssumeList) AssumeList :unextractable) +(function AssumeNil () AssumeList :unextractable) + +; ################### start top-down assumptions + +(rewrite + (Function name in_ty out_ty output) + (Function name in_ty out_ty + (AssumeMulti (AssumeCons (InFunction name) (AssumeNil)) + output)) + :ruleset assume) + + +; ################### operations +(rewrite (AssumeMulti asum (Bop op c1 c2)) + (Bop op (AssumeMulti asum c1) (AssumeMulti asum c2)) + :ruleset assume) +(rewrite (AssumeMulti assum (Uop op c1)) + (Uop op (AssumeMulti assum c1)) + :ruleset assume) +(rewrite (AssumeMulti assum (Get expr index)) + (Get (AssumeMulti assum expr) index) + :ruleset assume) +(rewrite (AssumeMulti assum (Alloc expr ty)) + (Alloc (AssumeMulti assum expr) ty) + :ruleset assume) +(rewrite (AssumeMulti assum (Call name expr)) + (Call name (AssumeMulti assum expr)) + :ruleset assume) + +; ################### tuple operations +(rewrite (AssumeMulti assum (Single expr)) + (Single (AssumeMulti assum expr)) + :ruleset assume) +(rewrite (AssumeMulti assum (Concat order e1 e2)) + (Concat order (AssumeMulti assum e1) (AssumeMulti assum e2)) + :ruleset assume) + +; #################### control flow + +; assumptions, predicate, cases, current case +(function SwitchAssume (AssumeList Expr ExprList i64) ExprList :unextractable) + +(rewrite (AssumeMulti assum (Switch pred cases)) + (Switch (AssumeMulti assum pred) + (SwitchAssume assum + (AssumeMulti assum pred) + cases + 0)) + :ruleset assume) + +(rewrite (SwitchAssume pred assum (Nil) current_case) + (AssumeMulti assum (Nil)) + :ruleset assume) + +(rewrite (SwitchAssume pred + assum + (Cons current rest) + current_case) + (Cons + (AssumeMulti + (AssumeCons (InSwitch current_case pred) assum) + current) + (SwitchAssume + pred + assum + rest + (+ current_case 1))) + :ruleset assume) + +(rewrite (AssumeMulti assum (If pred then else)) + (If (AssumeMulti assum pred) + (AssumeMulti + (Cons (InIf true (AssumeMulti assum pred)) assum) then) + (AssumeMulti + (Cons (InIf false (AssumeMulti assum pred)) assum) else)) + :ruleset assume) + +(rewrite (AssumeMulti assum (Let inputs body)) + (Let + (AssumeMulti assum inputs) + (AssumeMulti + ; new context, make a list with one assumption in it + (Cons (InLet (AssumeMulti assum inputs)) (Nil)) + body)) + :ruleset assume) + + +(rewrite (AssumeMulti assum (DoWhile inputs pred_outputs)) + (DoWhile + (AssumeMulti assum inputs) + (AssumeMulti + (Cons (InLoop (AssumeMulti assum inputs) pred_outputs) + (Nil)) + pred_outputs)) + :ruleset assume) + + From 70d259c2a7765e22322533484fa8c92aec37761b Mon Sep 17 00:00:00 2001 From: oflatt Date: Wed, 7 Feb 2024 16:46:51 -0800 Subject: [PATCH 3/4] add assume test add assume depth notion top down assume list experiment finish writing crappy rules base case passing nested let test passing greatly simplify because we don't need assumelist add comment about nestings --- tree_assume/src/ast.rs | 8 +++ tree_assume/src/lib.rs | 3 +- tree_assume/src/schema.egg | 4 +- tree_assume/src/schema.rs | 2 + tree_assume/src/schema_helpers.rs | 22 +++--- tree_assume/src/to_egglog.rs | 9 +++ tree_assume/src/utility/assume.egg | 110 +++++++++++------------------ tree_assume/src/utility/assume.rs | 70 ++++++++++++++++-- 8 files changed, 143 insertions(+), 85 deletions(-) diff --git a/tree_assume/src/ast.rs b/tree_assume/src/ast.rs index cb15c8db9..b1667cdf2 100644 --- a/tree_assume/src/ast.rs +++ b/tree_assume/src/ast.rs @@ -210,6 +210,14 @@ pub fn inloop(e1: RcExpr, e2: RcExpr) -> Assumption { Assumption::InLoop(e1, e2) } +pub fn inif(is_then: bool, pred: RcExpr) -> Assumption { + Assumption::InIf(is_then, pred) +} + +pub fn infunc(name: &str) -> Assumption { + Assumption::InFunc(name.to_string()) +} + pub fn assume(assumption: Assumption, body: RcExpr) -> RcExpr { RcExpr::new(Expr::Assume(assumption, body)) } diff --git a/tree_assume/src/lib.rs b/tree_assume/src/lib.rs index 39d8e35b0..ebc08c8af 100644 --- a/tree_assume/src/lib.rs +++ b/tree_assume/src/lib.rs @@ -39,7 +39,8 @@ pub fn egglog_test( "{}\n{build}\n{}\n{check}\n", [ include_str!("schema.egg"), - include_str!("optimizations/constant_fold.egg") + include_str!("optimizations/constant_fold.egg"), + include_str!("utility/assume.egg"), ] .join("\n"), include_str!("schedule.egg"), diff --git a/tree_assume/src/schema.egg b/tree_assume/src/schema.egg index 7b32a38d3..133bfc00d 100644 --- a/tree_assume/src/schema.egg +++ b/tree_assume/src/schema.egg @@ -173,7 +173,8 @@ ; The term is in a loop with `input` and `pred_output`. ; input pred_output (InLoop Expr Expr) - (InFunc String Expr) + ; name of the function + (InFunc String) ; Branch of the switch and the predicate (InSwitch i64 Expr) ; If the predicate was true, and the predicate @@ -188,7 +189,6 @@ ; Assume allows creating context-specific terms. ; e.g. (Assume (InLet (Const (Int 2))) (Arg)) is equal to (Const (Int 2)) (function Assume (Assumption Expr) Expr) -(function AssumeList (Assumption ListExpr) ListExpr) ; ================================= diff --git a/tree_assume/src/schema.rs b/tree_assume/src/schema.rs index dad1d01d0..e4e99468c 100644 --- a/tree_assume/src/schema.rs +++ b/tree_assume/src/schema.rs @@ -59,6 +59,8 @@ pub type RcExpr = Rc; pub enum Assumption { InLet(RcExpr), InLoop(RcExpr, RcExpr), + InFunc(String), + InIf(bool, RcExpr), } #[derive(Debug, Clone, PartialEq, Eq)] diff --git a/tree_assume/src/schema_helpers.rs b/tree_assume/src/schema_helpers.rs index 68a33f0d7..c35be6a62 100644 --- a/tree_assume/src/schema_helpers.rs +++ b/tree_assume/src/schema_helpers.rs @@ -35,14 +35,20 @@ impl Expr { } pub fn to_program(self: &RcExpr, input_ty: Type, output_ty: Type) -> TreeProgram { - TreeProgram { - entry: RcExpr::new(Expr::Function( - "main".to_string(), - input_ty, - output_ty, - self.clone(), - )), - functions: vec![], + match self.as_ref() { + Expr::Function(..) => TreeProgram { + entry: self.clone(), + functions: vec![], + }, + _ => TreeProgram { + entry: RcExpr::new(Expr::Function( + "main".to_string(), + input_ty, + output_ty, + self.clone(), + )), + functions: vec![], + }, } } } diff --git a/tree_assume/src/to_egglog.rs b/tree_assume/src/to_egglog.rs index 25d458b9a..0f78bb04e 100644 --- a/tree_assume/src/to_egglog.rs +++ b/tree_assume/src/to_egglog.rs @@ -66,6 +66,15 @@ impl Assumption { let rhs = rhs.to_egglog_internal(term_dag); term_dag.app("InLoop".into(), vec![lhs, rhs]) } + Assumption::InFunc(name) => { + let name_lit = term_dag.lit(Literal::String(name.into())); + term_dag.app("InFunc".into(), vec![name_lit]) + } + Assumption::InIf(is_then, pred) => { + let pred = pred.to_egglog_internal(term_dag); + let is_then = term_dag.lit(Literal::Bool(*is_then)); + term_dag.app("InIf".into(), vec![is_then, pred]) + } } } } diff --git a/tree_assume/src/utility/assume.egg b/tree_assume/src/utility/assume.egg index 57afa51c7..56553a7c4 100644 --- a/tree_assume/src/utility/assume.egg +++ b/tree_assume/src/utility/assume.egg @@ -5,107 +5,77 @@ (ruleset assume) (sort AssumeList) -; We collect multiple assumes into one AssumeMulti. -; These happen when there are nested `If` or `Switch` statements. -; When it gets to the bottom, we flatten it back out to multiple `Assume` nodes -; for the convenience of other analyses. -(function AssumeMulti (AssumeList Expr) Expr :unextractable) -(function AssumeCons (Assumption AssumeList) AssumeList :unextractable) -(function AssumeNil () AssumeList :unextractable) +; In order to saturate and not create unecessary contexts, we need to collapse +; duplicate assumptions. +; For example, the rewrite over `Function` could create many +; `(Assume (InFunc name) (Assume (InFunc name) ...))` nestings +(rewrite (Assume assumption (Assume assumption rest)) + (Assume assumption rest) + :ruleset assume) ; ################### start top-down assumptions (rewrite - (Function name in_ty out_ty output) + (Function name in_ty out_ty out) (Function name in_ty out_ty - (AssumeMulti (AssumeCons (InFunction name) (AssumeNil)) - output)) + (Assume (InFunc name) + out)) :ruleset assume) ; ################### operations -(rewrite (AssumeMulti asum (Bop op c1 c2)) - (Bop op (AssumeMulti asum c1) (AssumeMulti asum c2)) +(rewrite (Assume asum (Bop op c1 c2)) + (Bop op (Assume asum c1) (Assume asum c2)) :ruleset assume) -(rewrite (AssumeMulti assum (Uop op c1)) - (Uop op (AssumeMulti assum c1)) +(rewrite (Assume assum (Uop op c1)) + (Uop op (Assume assum c1)) :ruleset assume) -(rewrite (AssumeMulti assum (Get expr index)) - (Get (AssumeMulti assum expr) index) +(rewrite (Assume assum (Get expr index)) + (Get (Assume assum expr) index) :ruleset assume) -(rewrite (AssumeMulti assum (Alloc expr ty)) - (Alloc (AssumeMulti assum expr) ty) +(rewrite (Assume assum (Alloc expr ty)) + (Alloc (Assume assum expr) ty) :ruleset assume) -(rewrite (AssumeMulti assum (Call name expr)) - (Call name (AssumeMulti assum expr)) +(rewrite (Assume assum (Call name expr)) + (Call name (Assume assum expr)) :ruleset assume) ; ################### tuple operations -(rewrite (AssumeMulti assum (Single expr)) - (Single (AssumeMulti assum expr)) +(rewrite (Assume assum (Single expr)) + (Single (Assume assum expr)) :ruleset assume) -(rewrite (AssumeMulti assum (Concat order e1 e2)) - (Concat order (AssumeMulti assum e1) (AssumeMulti assum e2)) +(rewrite (Assume assum (Concat order e1 e2)) + (Concat order (Assume assum e1) (Assume assum e2)) :ruleset assume) ; #################### control flow ; assumptions, predicate, cases, current case -(function SwitchAssume (AssumeList Expr ExprList i64) ExprList :unextractable) - -(rewrite (AssumeMulti assum (Switch pred cases)) - (Switch (AssumeMulti assum pred) - (SwitchAssume assum - (AssumeMulti assum pred) - cases - 0)) +(function SwitchAssume (AssumeList Expr ListExpr i64) ListExpr :unextractable) + +(rewrite (Assume assum (If pred then else)) + (If (Assume assum pred) + (Assume + (InIf true (Assume assum pred)) then) + (Assume + (InIf false (Assume assum pred)) else)) :ruleset assume) -(rewrite (SwitchAssume pred assum (Nil) current_case) - (AssumeMulti assum (Nil)) - :ruleset assume) - -(rewrite (SwitchAssume pred - assum - (Cons current rest) - current_case) - (Cons - (AssumeMulti - (AssumeCons (InSwitch current_case pred) assum) - current) - (SwitchAssume - pred - assum - rest - (+ current_case 1))) - :ruleset assume) - -(rewrite (AssumeMulti assum (If pred then else)) - (If (AssumeMulti assum pred) - (AssumeMulti - (Cons (InIf true (AssumeMulti assum pred)) assum) then) - (AssumeMulti - (Cons (InIf false (AssumeMulti assum pred)) assum) else)) - :ruleset assume) - -(rewrite (AssumeMulti assum (Let inputs body)) +(rewrite (Assume assum (Let inputs body)) (Let - (AssumeMulti assum inputs) - (AssumeMulti - ; new context, make a list with one assumption in it - (Cons (InLet (AssumeMulti assum inputs)) (Nil)) + (Assume assum inputs) + (Assume + (InLet (Assume assum inputs)) body)) :ruleset assume) -(rewrite (AssumeMulti assum (DoWhile inputs pred_outputs)) +(rewrite (Assume assum (DoWhile inputs pred_outputs)) (DoWhile - (AssumeMulti assum inputs) - (AssumeMulti - (Cons (InLoop (AssumeMulti assum inputs) pred_outputs) - (Nil)) + (Assume assum inputs) + (Assume + (InLoop (Assume assum inputs) pred_outputs) pred_outputs)) :ruleset assume) - diff --git a/tree_assume/src/utility/assume.rs b/tree_assume/src/utility/assume.rs index 41471eee2..9e13a9db3 100644 --- a/tree_assume/src/utility/assume.rs +++ b/tree_assume/src/utility/assume.rs @@ -1,14 +1,49 @@ #[cfg(test)] use crate::{egglog_test, interpreter::Value, schema::Constant}; +#[test] +fn test_assume_in_func() -> crate::Result { + use crate::ast::*; + let expr = function("main", intt(), intt(), int(2)); + let expected = function("main", intt(), intt(), assume(infunc("main"), int(2))); + egglog_test( + &format!("{expr}"), + &format!("(check (= {expr} {expected}))"), + vec![ + expr.to_program(emptyt(), intt()), + expected.to_program(emptyt(), intt()), + ], + Value::Tuple(vec![]), + Value::Const(Constant::Int(2)), + ) +} + #[test] fn test_assume_two_lets() -> crate::Result { use crate::ast::*; - let expr = tlet(int(1), tlet(add(arg(), arg()), mul(arg(), int(2)))); - let arg1 = assume(inlet(int(1)), arg()); + let expr = function( + "main", + intt(), + intt(), + tlet(int(1), tlet(add(arg(), arg()), mul(arg(), int(2)))), + ); + let int1 = assume(infunc("main"), int(1)); + let arg1 = assume(inlet(int1.clone()), arg()); let addarg1 = add(arg1.clone(), arg1.clone()); - let arg2 = assume(inlet(addarg1), arg()); - let expr2 = tlet(int(1), tlet(add(arg1.clone(), arg1), mul(arg2, int(2)))); + let int2 = assume(inlet(addarg1.clone()), int(2)); + let arg2 = assume(inlet(addarg1.clone()), arg()); + let expr2 = function( + "main", + intt(), + intt(), + tlet( + int1, + tlet( + add(arg1.clone(), arg1.clone()), + mul(arg2.clone(), int2.clone()), + ), + ), + ); egglog_test( &format!("{expr}"), @@ -21,3 +56,30 @@ fn test_assume_two_lets() -> crate::Result { Value::Const(Constant::Int(4)), ) } + +#[test] +fn test_switch_contexts() -> crate::Result { + use crate::ast::*; + let expr = function("main", intt(), intt(), tif(ttrue(), int(1), int(2))); + let pred = assume(infunc("main"), ttrue()); + let expr2 = function( + "main", + intt(), + intt(), + tif( + pred.clone(), + assume(inif(true, pred.clone()), int(1)), + assume(inif(false, pred.clone()), int(2)), + ), + ); + egglog_test( + &format!("{expr}"), + &format!("(check (= {expr} {expr2}))"), + vec![ + expr.to_program(emptyt(), intt()), + expr2.to_program(emptyt(), intt()), + ], + Value::Tuple(vec![]), + Value::Const(Constant::Int(1)), + ) +} From 7cfe5280d8f5f74311602793c6bed06a5cc7ae7e Mon Sep 17 00:00:00 2001 From: oflatt Date: Thu, 8 Feb 2024 14:38:16 -0800 Subject: [PATCH 4/4] add cycle test and don't saturate --- tree_assume/src/ast.rs | 7 +++++- tree_assume/src/lib.rs | 2 +- tree_assume/src/schedule.egg | 4 ++-- tree_assume/src/utility/assume.egg | 5 ++-- tree_assume/src/utility/assume.rs | 38 ++++++++++++++++++++++++++++++ 5 files changed, 50 insertions(+), 6 deletions(-) diff --git a/tree_assume/src/ast.rs b/tree_assume/src/ast.rs index b1667cdf2..fb938b96b 100644 --- a/tree_assume/src/ast.rs +++ b/tree_assume/src/ast.rs @@ -163,7 +163,12 @@ macro_rules! parallel { pub use parallel; pub fn parallel_vec(es: impl IntoIterator) -> RcExpr { - es.into_iter().fold(empty(), |acc, x| push_par(x, acc)) + let mut iter = es.into_iter(); + if let Some(e) = iter.next() { + iter.fold(single(e), |acc, x| push_par(x, acc)) + } else { + empty() + } } pub fn tlet(lhs: RcExpr, rhs: RcExpr) -> RcExpr { diff --git a/tree_assume/src/lib.rs b/tree_assume/src/lib.rs index ebc08c8af..91ae82d1e 100644 --- a/tree_assume/src/lib.rs +++ b/tree_assume/src/lib.rs @@ -30,7 +30,7 @@ pub fn egglog_test( let result = interpret(&prog, input.clone()); assert_eq!( result, expected, - "Program {:?} produced {} instead of expected {}", + "Program {:?}\nproduced:\n{}\ninstead of expected:\n{}", prog, result, expected ); } diff --git a/tree_assume/src/schedule.egg b/tree_assume/src/schedule.egg index 1f5762716..bb825ab83 100644 --- a/tree_assume/src/schedule.egg +++ b/tree_assume/src/schedule.egg @@ -1,6 +1,6 @@ (run-schedule (repeat 6 - (saturate assume) + (repeat 100 assume) (saturate always-run) (saturate error-checking) - (run constant_fold))) + (saturate constant_fold))) diff --git a/tree_assume/src/utility/assume.egg b/tree_assume/src/utility/assume.egg index 56553a7c4..2904fa637 100644 --- a/tree_assume/src/utility/assume.egg +++ b/tree_assume/src/utility/assume.egg @@ -71,11 +71,12 @@ :ruleset assume) -(rewrite (Assume assum (DoWhile inputs pred_outputs)) +(rule ((= lhs (Assume assum (DoWhile inputs pred_outputs)))) + ((union lhs (DoWhile (Assume assum inputs) (Assume (InLoop (Assume assum inputs) pred_outputs) - pred_outputs)) + pred_outputs)))) :ruleset assume) diff --git a/tree_assume/src/utility/assume.rs b/tree_assume/src/utility/assume.rs index 9e13a9db3..576999e8b 100644 --- a/tree_assume/src/utility/assume.rs +++ b/tree_assume/src/utility/assume.rs @@ -83,3 +83,41 @@ fn test_switch_contexts() -> crate::Result { Value::Const(Constant::Int(1)), ) } + +#[test] +fn test_dowhile_cycle_assume() -> crate::Result { + use crate::ast::*; + // loop runs one iteration and returns 3 + let myloop = dowhile(single(int(2)), parallel!(tfalse(), int(3))); + let expr = function("main", intt(), intt(), myloop); + + let int2 = single(assume(infunc("main"), int(2))); + let inner_assume = inloop(int2.clone(), parallel!(tfalse(), int(3))); + let expr2 = function( + "main", + intt(), + intt(), + dowhile( + int2.clone(), + parallel!( + assume(inner_assume.clone(), tfalse()), + assume(inner_assume.clone(), int(3)), + ), + ), + ); + + egglog_test( + &format!( + "{expr} +(union {} {expr})", + single(int(3)) + ), + &format!("(check (= {expr} {expr2}))"), + vec![ + expr.to_program(emptyt(), intt()), + expr2.to_program(emptyt(), intt()), + ], + Value::Tuple(vec![]), + Value::Tuple(vec![Value::Const(Constant::Int(3))]), + ) +}