egglog 3.0.0

egglog is a language that combines the benefits of equality saturation and datalog. It can be used for analysis, optimization, and synthesis of programs. It is the successor to the popular rust library egg.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147

use egglog::CommandOutput;
use egglog::EGraph;
use egglog::prelude::*;

fn find_extract_best(outputs: &[CommandOutput]) -> String {
    outputs
        .iter()
        .find(|o| matches!(o, CommandOutput::ExtractBest(..)))
        .expect("No ExtractBest output found")
        .to_string()
}

#[test]
fn test_extraction_same_with_proof_mode() {
    // Test that extraction in normal mode produces the same result as extraction in proof mode
    let _ = env_logger::builder().is_test(true).try_init();

    let program = r#"
        (datatype Math
            (Num i64)
            (Add Math Math)
            (Mul Math Math))

        (rewrite (Add (Num a) (Num b)) (Num (+ a b)))
        (rewrite (Mul (Num a) (Num b)) (Num (* a b)))

        ; commutativity
        (rewrite (Add x y) (Add y x))
        (rewrite (Mul x y) (Mul y x))

        ; associativity
        (rewrite (Add (Add x y) z) (Add x (Add y z)))
        (rewrite (Mul (Mul x y) z) (Mul x (Mul y z)))

        ; distributivity
        (rewrite (Mul x (Add y z)) (Add (Mul x y) (Mul x z)))

        (let expr (Mul (Add (Num 1) (Num 2)) (Num 3)))
        (run 10)
    "#;

    // Run in normal mode and extract
    let mut egraph_normal = EGraph::default();
    egraph_normal.parse_and_run_program(None, program).unwrap();
    let normal_output = egraph_normal
        .parse_and_run_program(None, "(extract expr)")
        .unwrap();
    let normal_extracted = find_extract_best(&normal_output);

    // Run in proof mode and extract
    let mut egraph_proofs = EGraph::new_with_proofs();
    egraph_proofs.parse_and_run_program(None, program).unwrap();
    let proofs_output = egraph_proofs
        .parse_and_run_program(None, "(extract expr)")
        .unwrap();
    let proofs_extracted = find_extract_best(&proofs_output);

    // They should produce the same extraction result
    assert_eq!(
        normal_extracted, proofs_extracted,
        "Extraction differs between normal mode and proof mode:\nNormal: {normal_extracted}\nProofs: {proofs_extracted}"
    );

    // The result should be (Num 9) since (1+2)*3 = 9
    assert!(
        normal_extracted.contains("Num") && normal_extracted.contains("9"),
        "Expected (Num 9), got: {normal_extracted}"
    );
}

#[test]
fn test_extraction_same_with_proof_mode_using_rule_macro() {
    // Test using the rule! macro from prelude
    let _ = env_logger::builder().is_test(true).try_init();

    // Setup program with datatypes - use an expression that simplifies to a unique result
    let setup = r#"
        (datatype Expr
            (Var String)
            (Lit i64)
            (Add Expr Expr))

        ; Simplification rule that gives a unique result
        (rewrite (Add (Lit a) (Lit b)) (Lit (+ a b)))

        (let x (Add (Lit 1) (Lit 2)))
        (run 10)
    "#;

    // Run in normal mode
    let mut egraph_normal = EGraph::default();
    egraph_normal.parse_and_run_program(None, setup).unwrap();

    add_ruleset(&mut egraph_normal, "my_rules").unwrap();
    rule(
        &mut egraph_normal,
        "my_rules",
        facts![(= (Add a b) e)],
        actions![(union e (Add b a))],
    )
    .unwrap();

    for _ in 0..5 {
        run_ruleset(&mut egraph_normal, "my_rules").unwrap();
    }

    let normal_output = egraph_normal
        .parse_and_run_program(None, "(extract x)")
        .unwrap();
    let normal_extracted = find_extract_best(&normal_output);

    // Run in proof mode
    let mut egraph_proofs = EGraph::new_with_proofs();
    egraph_proofs.parse_and_run_program(None, setup).unwrap();

    // Add the same rule
    add_ruleset(&mut egraph_proofs, "my_rules").unwrap();
    rule(
        &mut egraph_proofs,
        "my_rules",
        facts![(= (Add a b) e)],
        actions![(union e (Add b a))],
    )
    .unwrap();

    for _ in 0..5 {
        run_ruleset(&mut egraph_proofs, "my_rules").unwrap();
    }

    // Extract
    let proofs_output = egraph_proofs
        .parse_and_run_program(None, "(extract x)")
        .unwrap();
    let proofs_extracted = find_extract_best(&proofs_output);

    // They should produce the same extraction result
    assert_eq!(
        normal_extracted, proofs_extracted,
        "Extraction differs between normal mode and proof mode:\nNormal: {normal_extracted}\nProofs: {proofs_extracted}"
    );

    // The result should be (Lit 3) since 1+2=3
    assert!(
        normal_extracted.contains("Lit") && normal_extracted.contains("3"),
        "Expected (Lit 3), got: {normal_extracted}"
    );
}