egglog 3.0.0

use egglog::{
    ast::{ResolvedCommand, sanitize_internal_names},
    extract::DefaultCost,
    *,
};

#[test]
fn globals_missing_prefix_errors_when_opted_in() {
    let mut egraph = EGraph::default();
    egraph.set_strict_mode(true);
    let err = egraph
        .parse_and_run_program(None, "(let value 41)")
        .unwrap_err();
    match err {
        Error::TypeError(TypeError::GlobalMissingPrefix { ref name, .. }) => {
            assert_eq!(name, "value");
        }
        other => panic!("expected missing dollar error, got {other:?}"),
    }
}

#[test]
fn globals_missing_prefix_errors_for_prefixed_pattern_variable_when_opted_in() {
    let mut egraph = EGraph::default();
    egraph.set_strict_mode(true);
    let err = egraph
        .parse_and_run_program(None, "(rule ((= $x 1)) ())")
        .unwrap_err();

    match err {
        Error::TypeError(TypeError::NonGlobalPrefixed { ref name, .. }) => {
            assert_eq!(name, "$x");
        }
        other => panic!("expected non-global prefixed variable error, got {other:?}"),
    }
}

#[test]
fn globals_missing_prefix_errors_for_prefixed_rule_let_when_opted_in() {
    let mut egraph = EGraph::default();
    egraph.set_strict_mode(true);
    let err = egraph
        .parse_and_run_program(None, "(rule () ((let $y 1)))")
        .unwrap_err();

    match err {
        Error::TypeError(TypeError::NonGlobalPrefixed { ref name, .. }) => {
            assert_eq!(name, "$y");
        }
        other => panic!("expected non-global prefixed variable error, got {other:?}"),
    }
}

#[test]
fn globals_cannot_be_shadowed_by_pattern_variables() {
    let _ = env_logger::builder().is_test(true).try_init();

    let mut egraph = EGraph::default();
    let program = r#"
        (let $value 41)
        (rule ((= value $value)) ())
    "#;

    let err = egraph.parse_and_run_program(None, program).unwrap_err();
    match err {
        Error::Shadowing(message, _global_span, _shadow_span) => {
            assert!(message.contains("pattern variable `value`"));
            assert!(message.contains("global `$value`"));
        }
        other => panic!("expected shadowing error, got {other:?}"),
    }
}

#[test]
fn test_simple_extract1() {
    let _ = env_logger::builder().is_test(true).try_init();

    let mut egraph = EGraph::default();

    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
             (datatype Op (Add i64 i64))
             (let expr (Add 1 1))
             (extract expr)"#,
        )
        .unwrap();
    let CommandOutput::ExtractBest(_, cost, _) = outputs[0] else {
        panic!();
    };
    assert_eq!(cost, 3);
}

#[test]
fn primitive_error_in_extract_returns_error() {
    let _ = env_logger::builder().is_test(true).try_init();

    let mut egraph = EGraph::default();
    // Evaluating this primitive should surface a user-facing error instead of
    // panicking when the primitive fails.
    let err = egraph
        .parse_and_run_program(None, "(extract (<< 1 10000))")
        .unwrap_err();
    assert!(err.to_string().contains("call of primitive << failed"));
}

#[test]
fn primitive_error_in_run_schedule_returns_error() {
    let _ = env_logger::builder().is_test(true).try_init();

    let mut egraph = EGraph::default();
    let program = r#"
        (ruleset problematic)
        (rule ()
              ((let tmp (<< 1 10000)))
              :ruleset problematic)
        (run-schedule (run problematic))
    "#;

    let err = egraph.parse_and_run_program(None, program).unwrap_err();
    assert!(err.to_string().contains("call of primitive << failed"));
}

#[test]
fn check_facts_stops_safely_in_parallel_mode() {
    use std::fmt::Write;

    let mut program = String::from("(relation Candidate (i64))\n");
    for i in 0..20_000 {
        writeln!(&mut program, "(Candidate {i})").unwrap();
    }

    let mut egraph = EGraph::new(32);
    egraph.parse_and_run_program(None, &program).unwrap();
    egraph
        .parse_and_run_program(None, "(check (Candidate x))")
        .unwrap();
    egraph
        .parse_and_run_program(None, "(check (Candidate 19999))")
        .unwrap();
}

#[test]
fn prove_exists_reports_query_mismatch() {
    let _ = env_logger::builder().is_test(true).try_init();

    let mut egraph = EGraph::new_with_proofs();
    let program = r#"
        (relation R (i64))
    (prove (R x))
    "#;

    let err = egraph.parse_and_run_program(None, program).unwrap_err();
    let msg = err.to_string();
    assert!(
        msg.contains("Could not find a proof due to query not matching"),
        "expected helpful error message, got {msg}"
    );
}

#[test]
fn test_simple_extract2() {
    let _ = env_logger::builder().is_test(true).try_init();

    let mut egraph = EGraph::default();

    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
             (datatype Term
               (Origin :cost 0)
               (BigStep Term :cost 10)
               (SmallStep Term :cost 1)
             )
             (let t (Origin))
             (let tb (BigStep t))
             (let tbs (SmallStep tb))
             (let ts (SmallStep t))
             (let tss (SmallStep ts))
             (let tsss (SmallStep tss))
             (union tbs tsss)
             (let tssss (SmallStep tsss))
             (union tssss tb)
             (extract tb)
             "#,
        )
        .unwrap();
    assert!(matches!(outputs[0], CommandOutput::ExtractBest(_, 4, _)));
}

#[test]
fn test_simple_extract3() {
    let _ = env_logger::builder().is_test(true).try_init();

    let mut egraph = EGraph::default();

    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
             (datatype Fruit
               (Apple i64 :cost 1)
               (Orange f64 :cost 2)
             )
             (datatype Vegetable
               (Broccoli bool :cost 3)
               (Carrot Fruit :cost 4)
             )
             (let a (Apple 5))
             (let o (Orange 3.14))
             (let b (Broccoli true))
             (let c (Carrot a))
             (extract a)
             "#,
        )
        .unwrap();

    let CommandOutput::ExtractBest(_, cost, _) = outputs[0] else {
        panic!();
    };
    assert_eq!(cost, 2);
}

#[test]
fn test_simple_extract4() {
    let _ = env_logger::builder().is_test(true).try_init();

    let mut egraph = EGraph::default();

    egraph
        .parse_and_run_program(
            None,
            r#"
        (datatype Foo
            (Foobar)
        )
        (subsume (Foobar))
        (datatype Bar
            (Barbar Foo)
        )
        (let x (Barbar (Foobar)))
        (extract x)
        "#,
        )
        .unwrap_err();
}

#[test]
fn test_simple_extract5() {
    let _ = env_logger::builder().is_test(true).try_init();

    let mut egraph = EGraph::default();

    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
             (datatype Foo
                (Foobar i64)
             )
             (let foobar (Foobar 42))
             (datatype Bar
                (Barfoo i64)
             )
             (let barfoo (Barfoo 24))
             (sort QuaVec (Vec i64))
             (sort QuaMap (Map QuaVec Foo))
             (function Quaz () QuaMap :no-merge)
             (set (Quaz) (map-empty))
             (extract (Quaz))
             "#,
        )
        .unwrap();

    let CommandOutput::ExtractBest(_, cost, _) = outputs[0] else {
        panic!();
    };
    assert_eq!(cost, 0);
}

#[test]
fn test_simple_extract6() {
    let _ = env_logger::builder().is_test(true).try_init();

    let mut egraph = EGraph::default();

    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
             (datatype False)
             (sort QuaVec (Vec i64))
             (sort QuaMap (Map QuaVec False))
             (function Quaz () QuaMap :no-merge)
             (set (Quaz) (map-empty))
             (extract (Quaz))
             "#,
        )
        .unwrap();

    let CommandOutput::ExtractBest(_, cost, _) = outputs[0] else {
        panic!();
    };
    assert_eq!(cost, 0);
}

#[test]
fn test_simple_extract7() {
    let _ = env_logger::builder().is_test(true).try_init();

    let mut egraph = EGraph::default();

    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
            (datatype Foo
                (bar)
                (baz)
            )
            (sort Mapsrt1 (Map i64 Foo))
            (let map1 (map-insert (map-empty) 0 (bar)))

            (sort Mapsrt2 (Map bool Foo))
            (let map2 (map-insert (map-empty) false (baz)))
            ;(let map2b (map-insert (map-empty) false (bar)))
            ;(union map2 map2b)

            ;(extract map1)
            ;(extract map2)

            ;(function toerr (Mapsrt2) Foo :no-merge)

            ;(set (toerr map2) (bar))

            (union (bar) (baz))
            ; Also unions map1 and map2!?

            (extract map1)
            (extract map2)

            ;(extract (toerr map2))

             "#,
        )
        .unwrap();

    let CommandOutput::ExtractBest(_, cost, _) = outputs[0] else {
        panic!();
    };
    assert_eq!(cost, 2);
}

#[test]
fn test_simple_extract8() {
    let _ = env_logger::builder().is_test(true).try_init();

    let mut egraph = EGraph::default();

    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
            (datatype Foo
                (bar :cost 10)
            )
            (function func () Foo :no-merge)
            (set (func) (bar))

            (extract (bar))
            "#,
        )
        .unwrap();

    let CommandOutput::ExtractBest(_, cost, _) = outputs[0] else {
        panic!();
    };
    assert_eq!(cost, 10);
}

#[test]
fn test_simple_extract9() {
    let _ = env_logger::builder().is_test(true).try_init();

    let mut egraph = EGraph::default();

    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
            (datatype Foo)
            (datatype NodeA)
            (datatype NodeB)
            (datatype NodeC)
            (constructor ctoa (NodeC) NodeA)
            (constructor atob (NodeA) NodeB)
            (constructor btoc (NodeB) NodeC)

            (constructor bar () Foo :cost 9223372036854775807)
            (constructor barbar (Foo Foo) Foo :cost 2)

            (constructor groundedA (Foo) NodeA)
            (let a (groundedA (barbar (bar) (bar))))
            (let b (atob a))
            (let c (btoc b))
            (let a2 (ctoa c))
            (let b2 (atob a2))
            (let c2 (btoc b2))
            (union a a2)
            (union b b2)
            (union c c2)

            (extract a)
            "#,
        )
        .unwrap();

    let CommandOutput::ExtractBest(_, cost, _) = outputs[0] else {
        panic!();
    };
    assert_eq!(cost, DefaultCost::MAX);

    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
            (extract b)
            "#,
        )
        .unwrap();

    let CommandOutput::ExtractBest(_, cost, _) = outputs[0] else {
        panic!();
    };
    assert_eq!(cost, DefaultCost::MAX);

    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
            (extract c)
            "#,
        )
        .unwrap();

    let CommandOutput::ExtractBest(_, cost, _) = outputs[0] else {
        panic!();
    };
    assert_eq!(cost, DefaultCost::MAX);
}

#[test]
fn test_extract_variants1() {
    let _ = env_logger::builder().is_test(true).try_init();

    let mut egraph = EGraph::default();

    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
             (datatype Term
               (Origin :cost 0)
               (BigStep Term :cost 10)
               (SmallStep Term :cost 1)
             )
             (let t (Origin))
             (let tb (BigStep t))
             (let tbs (SmallStep tb))
             (let ts (SmallStep t))
             (let tss (SmallStep ts))
             (let tsss (SmallStep tss))
             (union tbs tsss)
             (let tssss (SmallStep tsss))
             (union tssss tb)
             (extract tb 3)
             "#,
        )
        .unwrap();
    assert_eq!(
        outputs[0].to_string(),
        "(\n   (SmallStep (SmallStep (SmallStep (SmallStep (Origin)))))\n   (BigStep (Origin))\n)\n"
    );
}

#[test]
fn test_subsumed_unextractable_action_extract() {
    // Test when an expression is subsumed, it isn't extracted, even if its the cheapest
    let mut egraph = EGraph::default();

    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
            (datatype Math)
            (constructor expensive () Math :cost 100)
            (constructor cheap () Math :cost 1)
            (union (expensive) (cheap))
            (extract (expensive))
            "#,
        )
        .unwrap();

    let CommandOutput::ExtractBest(_term_dag, _, _term_id) = &outputs[0] else {
        panic!("Should get extract best command output");
    };
    // Originally should give back numeric term
    assert!(match &outputs[0] {
        CommandOutput::ExtractBest(termdag, _, term_id) => {
            matches!(termdag.get(*term_id), Term::App(s, ..) if s == "cheap")
        }
        _ => false,
    });
    // Then if we make one as subsumed, it should give back the variable term
    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
            (subsume (cheap))
            (extract (expensive))
            "#,
        )
        .unwrap();
    assert!(match &outputs[0] {
        CommandOutput::ExtractBest(termdag, _, term_id) => {
            matches!(termdag.get(*term_id), Term::App(s, ..) if s == "expensive")
        }
        _ => false,
    });
}

#[test]
fn test_subsume_unextractable_insert_and_merge() {
    // Example adapted from https://github.com/egraphs-good/egglog/pull/301#pullrequestreview-1756826062
    let mut egraph = EGraph::default();

    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
            (datatype Expr
                (f Expr)
                (Num i64))
            (constructor expensive () Expr :cost 100)

              (f (Num 1))
              (subsume (f (Num 1)))
              (f (Num 2))

              (union (Num 2) (Num 1))
              (union (f (Num 2)) (expensive))
              (extract (f (Num 2)))
            "#,
        )
        .unwrap();
    assert!(match &outputs[0] {
        CommandOutput::ExtractBest(termdag, _, term_id) => {
            matches!(termdag.get(*term_id), Term::App(s, ..) if s == "expensive")
        }
        _ => false,
    });
}

#[test]
fn test_subsume_unextractable_action_extract_multiple() {
    // Test when an expression is set as subsumed, it isn't extracted, like with
    // extract multiple
    let mut egraph = EGraph::default();

    let outputs1 = egraph
        .parse_and_run_program(
            None,
            "
            (datatype Math (Num i64))
            (Num 1)
            (union (Num 1) (Num 2))
            (extract (Num 1) 2)
            ",
        )
        .unwrap();
    // Originally should give back two terms when extracted
    assert!(matches!(
        outputs1[0],
        CommandOutput::ExtractVariants(_, ref terms) if terms.len() == 2
    ));
    // Then if we make one unextractable, it should only give back one term
    let outputs2 = egraph
        .parse_and_run_program(
            None,
            "
            (subsume (Num 2))
            (extract (Num 1) 2)
            ",
        )
        .unwrap();
    assert!(matches!(
        outputs2[0],
        CommandOutput::ExtractVariants(_, ref terms) if terms.len() == 1
    ));
}

#[test]
fn test_rewrite_subsumed_unextractable() {
    // When a rewrite is marked as a subsumed, the lhs should not be extracted

    let mut egraph = EGraph::default();

    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
            (datatype Math)
            (constructor expensive () Math :cost 100)
            (constructor cheap () Math :cost 1)
            (rewrite (cheap) (expensive) :subsume)
            (cheap)
            (run 1)
            (extract (cheap))
            "#,
        )
        .unwrap();
    // Should give back expenive term, because cheap is unextractable
    assert_eq!(outputs[1].to_string(), "(expensive)\n");
}

#[test]
fn test_rewrite_subsumed() {
    // When a rewrite is marked as a subsumed, the lhs should not be extracted

    let mut egraph = EGraph::default();

    // If we rerite most-exp to another term, that rewrite shouldnt trigger since its been subsumed.
    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
            (datatype Math)
            (constructor expensive () Math :cost 100)
            (constructor most-exp () Math :cost 1000)
            (rewrite (most-exp) (expensive) :subsume)
            (most-exp)
            (run 1)
            (constructor cheap () Math :cost 1)
            (rewrite (most-exp) (cheap))
            (run 1)
            (extract (most-exp))
            "#,
        )
        .unwrap();
    assert_eq!(outputs[2].to_string(), "(expensive)\n");
}

#[test]
fn test_subsume() {
    // Test that if we mark a term as subsumed than no rewrites will be applied to it.
    // We can test this by adding a commutative additon property, and verifying it isn't applied on one of the terms
    // but is on the other
    let mut egraph = EGraph::default();
    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
        (datatype Math
          (Add Math Math)
          (Num i64))

        (rewrite (Add a b) (Add b a))
        (let x (Add (Num 1) (Num 2)))
        (let y (Add (Num 3) (Num 4)))
        (subsume (Add (Num 1) (Num 2)))
        (run 1)
        (extract y 10)
        "#,
        )
        .unwrap();
    assert!(matches!(
        outputs[1],
        CommandOutput::ExtractVariants(_, ref terms) if terms.len() == 2
    ));

    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
        ;; add something equal to x that can be extracted:
        (constructor otherConst () Math)
        (let other (otherConst))
        (union x other)
        (extract x 10)
        "#,
        )
        .unwrap();
    assert!(matches!(
        outputs[0],
        CommandOutput::ExtractVariants(_, ref terms) if terms.len() == 1
    ));
}

#[test]
fn test_subsume_custom() {
    // Test that we can't subsume  a custom function
    // Only relations and constructors are allowed to be subsumed

    let mut egraph = EGraph::default();
    let res = egraph.parse_and_run_program(
        None,
        r#"
        (function one () i64 :no-merge)
        (set (one) 1)
        (subsume (one))
        "#,
    );
    assert!(res.is_err());
}

#[test]
fn test_subsume_ok() {
    let mut egraph = EGraph::default();
    let res = egraph.parse_and_run_program(
        None,
        r#"
        (sort E)
        (constructor one () E)
        (constructor two () E)
        (one)
        (subsume (one))
        ;; subsuming a non-existent tuple
        (subsume (two))

        (relation R (i64))
        (R 1)
        (subsume (R 1))
        (subsume (R 2))
        "#,
    );
    assert!(res.is_ok());
}

#[test]
fn test_cant_subsume_merge() {
    // Test that we can't subsume something with a merge function

    let mut egraph = EGraph::default();
    let res = egraph.parse_and_run_program(
        None,
        r#"
        (constructor one () i64 :merge old)
        (set (one) 1)
        (subsume (one))
        "#,
    );
    assert!(res.is_err());
}

#[test]
fn constructor_term_constructor_is_rejected() {
    let mut egraph = EGraph::default();
    // Proof-encoding view tables now use this as a function annotation,
    // so constructor syntax should reject `:internal-term-constructor`.
    let res = egraph.parse_and_run_program(
        None,
        r#"
        (sort Expr)
        (sort View)
        (constructor ExprView (Expr Expr) View :internal-term-constructor Expr)
        "#,
    );

    let err = res.unwrap_err();
    assert!(
        err.to_string()
            .contains("could not parse constructor options")
    );
}

#[test]
fn test_value_to_classid() {
    let mut egraph = EGraph::default();

    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
            (datatype Math)
            (constructor expensive () Math )
            (expensive)
            (extract (expensive))
            "#,
        )
        .unwrap();
    let CommandOutput::ExtractBest(termdag, _cost, term) = outputs[0].clone() else {
        panic!();
    };
    let expr = termdag.term_to_expr(&term, span!());
    let (sort, value) = egraph.eval_expr(&expr).unwrap();

    let serialize_output = egraph.serialize(SerializeConfig::default());
    assert!(serialize_output.is_complete());
    let class_id = egraph.value_to_class_id(&sort, value);
    assert!(serialize_output.egraph.class_data.get(&class_id).is_some());
    assert_eq!(value, egraph.class_id_to_value(&class_id));
}

#[test]
fn test_serialize_sort_name_with_dash() {
    // A sort whose name contains '-' (legal, like the built-in `vec-set`) must
    // serialize without panicking, and its class ID must still round-trip.
    let mut egraph = EGraph::default();
    let outputs = egraph
        .parse_and_run_program(
            None,
            r#"
            (datatype Math-Expr (Lit i64))
            (Lit 5)
            (extract (Lit 5))
            "#,
        )
        .unwrap();
    let CommandOutput::ExtractBest(termdag, _cost, term) = outputs[0].clone() else {
        panic!();
    };
    let expr = termdag.term_to_expr(&term, span!());
    let (sort, value) = egraph.eval_expr(&expr).unwrap();
    assert_eq!(sort.name(), "Math-Expr");

    let serialize_output = egraph.serialize(SerializeConfig::default());
    assert!(serialize_output.is_complete());
    let class_id = egraph.value_to_class_id(&sort, value);
    assert!(serialize_output.egraph.class_data.get(&class_id).is_some());
    assert_eq!(value, egraph.class_id_to_value(&class_id));
}

#[test]
fn test_serialize_617() {
    let program = "
        (sort Node)
        (constructor mk (i64) Node)
        (constructor mkb (i64) Node)
        (rewrite (mkb x) (mk x))

        (mkb 1) (mkb 3) (mkb 5) (mkb 6)

        (union (mk 1) (mk 3))
        (union (mk 3) (mk 5))

        (run-schedule (saturate (run)))";

    let mut egraph = EGraph::default();
    egraph.parse_and_run_program(None, program).unwrap();

    let serialize_output = egraph.serialize(SerializeConfig::default());
    assert!(serialize_output.is_complete());
    assert_eq!(serialize_output.egraph.class_data.len(), 6);
    assert_eq!(serialize_output.egraph.nodes.len(), 12);
}

#[test]
fn test_serialize_subsume_status() {
    let mut egraph = EGraph::default();

    egraph
        .parse_and_run_program(
            None,
            r#"
            (datatype Math)
            (constructor a () Math )
            (constructor b () Math )
            (a)
            (b)
            (subsume (a))
            "#,
        )
        .unwrap();

    let serialize_output = egraph.serialize(SerializeConfig::default());
    assert!(serialize_output.is_complete());
    let a_id = egraph.to_node_id(
        None,
        egglog::SerializedNode::Function {
            name: "a".into(),
            offset: 0,
        },
    );
    let b_id = egraph.to_node_id(
        None,
        egglog::SerializedNode::Function {
            name: "b".into(),
            offset: 0,
        },
    );
    assert!(serialize_output.egraph.nodes[&a_id].subsumed);
    assert!(!serialize_output.egraph.nodes[&b_id].subsumed);
}

#[test]
fn test_shadowing_query() {
    let s = "(function f () i64 :no-merge) (set (f) 2) (check (= (f) f) (= f 2))";
    let e = EGraph::default()
        .parse_and_run_program(None, s)
        .unwrap_err();
    assert!(matches!(e, Error::Shadowing(_, _, _)));
}

#[test]
fn test_shadowing_push() {
    let s = "(push) (let x 1) (pop) (let x 1)";
    EGraph::default().parse_and_run_program(None, s).unwrap();
}

#[test]
fn test_print_function_size() {
    let s = "(function f () i64 :no-merge) (set (f) 2) (print-size f)";
    let outputs = EGraph::default().parse_and_run_program(None, s).unwrap();
    assert_eq!(outputs[0].to_string(), "1\n");
}

#[test]
fn test_print_function() {
    let s = "(function f () i64 :no-merge) (set (f) 2) (print-function f)";
    let outputs = EGraph::default().parse_and_run_program(None, s).unwrap();
    assert_eq!(outputs[0].to_string(), "(\n   (f) -> 2\n)\n");
}

#[test]
fn test_print_function_csv() {
    let s = "(function f () i64 :no-merge) (set (f) 2) (print-function f :mode csv)";
    let outputs = EGraph::default().parse_and_run_program(None, s).unwrap();
    assert_eq!(outputs[0].to_string(), "f,2\n");
}

#[test]
fn test_print_stats() {
    let s = "(run 1) (print-stats)";
    let outputs = EGraph::default().parse_and_run_program(None, s).unwrap();
    assert_eq!(
        outputs[1].to_string(),
        "Overall statistics:\nRuleset : search 0.000s, merge 0.000s, rebuild 0.000s\n"
    );
}

#[test]
fn test_run_report() {
    let s = "(run 1)";
    let outputs = EGraph::default().parse_and_run_program(None, s).unwrap();
    assert_eq!(outputs[0].to_string(), "");
    assert!(matches!(outputs[0], CommandOutput::RunSchedule(..)));
}

#[test]
fn test_serialize_message_max_functions() {
    let mut egraph = EGraph::default();
    // Create three zero-arg constructors
    egraph
        .parse_and_run_program(
            None,
            r#"
            (datatype A)
            (constructor a () A)
            (constructor b () A)
            (constructor c () A)
            (a) (b) (c)
            "#,
        )
        .unwrap();
    let serialize_output = egraph.serialize(SerializeConfig {
        max_functions: Some(2),
        max_calls_per_function: None,
        include_temporary_functions: false,
        root_eclasses: vec![],
    });
    assert!(!serialize_output.is_complete());
    assert_eq!(serialize_output.omitted_description(), "Omitted: c\n");
}

#[test]
fn test_serialize_message_max_calls_per_function() {
    let mut egraph = EGraph::default();
    // Single constructor with many distinct calls (different arguments)
    egraph
        .parse_and_run_program(
            None,
            r#"
            (datatype N)
            (constructor mk (i64) N)
            (mk 0) (mk 1) (mk 2) (mk 3)
            "#,
        )
        .unwrap();
    let serialize_output = egraph.serialize(SerializeConfig {
        max_functions: None,
        max_calls_per_function: Some(2),
        include_temporary_functions: false,
        root_eclasses: vec![],
    });
    assert!(!serialize_output.is_complete());
    assert_eq!(serialize_output.omitted_description(), "Truncated: mk\n");
}

#[test]
fn eqsat_basic_term_encoding_roundtrip() {
    fn render_program(commands: &[ResolvedCommand]) -> String {
        let text = sanitize_internal_names(commands)
            .iter()
            .map(|cmd| cmd.to_string())
            .collect::<Vec<_>>()
            .join("\n");
        format!("{text}\n")
    }

    let path = std::path::Path::new("tests/web-demo/eqsat-basic.egg");
    let source = std::fs::read_to_string(path)
        .unwrap_or_else(|err| panic!("failed to read {}: {err}", path.display()));

    // 1. Desugar the program with term encoding enabled.
    let mut egraph = EGraph::new_with_term_encoding();
    let desugared_once = egraph
        .resolve_program(Some(path.display().to_string()), &source)
        .expect("term-encoding desugaring should succeed");
    let text_once = render_program(&desugared_once);

    // 2. Parse and desugar the rendered program with a fresh e-graph.
    let mut egraph = EGraph::default();
    let desugared_twice = egraph
        .resolve_program(None, &text_once)
        .expect("second desugaring should succeed");
    let text_twice = render_program(&desugared_twice);

    // 3. Parse and desugar again to ensure stability using another fresh e-graph.
    let mut egraph = EGraph::default();
    let desugared_thrice = egraph
        .resolve_program(None, &text_twice)
        .expect("third desugaring should succeed");
    let text_thrice = render_program(&desugared_thrice);

    assert_eq!(text_twice, text_thrice, "desugaring should stabilize");

    // 4. Run the stabilized program using term encoding.
    let mut runner = EGraph::default();
    runner
        .parse_and_run_program(None, &text_thrice)
        .expect("final program should execute successfully");
}

#[test]
fn rewrite_name_basic() {
    let mut egraph = EGraph::default();
    egraph
        .parse_and_run_program(
            None,
            "
            (datatype Math (Num i64) (Mul Math Math))
            (rewrite (Mul a (Num 1)) a :name \"mul-identity\")
            (let $x (Mul (Num 42) (Num 1)))
            (run 3)
            (check (= $x (Num 42)))
            ",
        )
        .unwrap();
}

#[test]
fn rewrite_name_birewrite() {
    let mut egraph = EGraph::default();
    egraph
        .parse_and_run_program(
            None,
            "
            (datatype Math (Num i64) (Add Math Math))
            (birewrite (Add a b) (Add b a) :name \"add-comm\")
            (let $x (Add (Num 1) (Num 2)))
            (run 3)
            (check (= $x (Add (Num 2) (Num 1))))
            ",
        )
        .unwrap();
}

#[test]
fn rewrite_name_desugars_correctly() {
    let mut egraph = EGraph::default();
    let desugared = egraph
        .resolve_program(
            None,
            "
            (datatype Math (Num i64) (Mul Math Math) (Add Math Math))
            (rewrite (Mul a (Num 1)) a :name \"mul-identity\")
            (birewrite (Add a b) (Add b a) :name \"add-comm\")
            ",
        )
        .unwrap();

    let joined: String = desugared
        .iter()
        .map(|cmd| format!("{cmd}"))
        .collect::<Vec<_>>()
        .join("\n");

    assert!(
        joined.contains("mul-identity"),
        "expected 'mul-identity' in:\n{joined}"
    );
    assert!(
        joined.contains("add-comm=>"),
        "expected 'add-comm=>' in:\n{joined}"
    );
    assert!(
        joined.contains("add-comm<="),
        "expected 'add-comm<=' in:\n{joined}"
    );
}

#[test]
fn rewrite_without_name_still_works() {
    let mut egraph = EGraph::default();
    egraph
        .parse_and_run_program(
            None,
            "
            (datatype Math (Num i64) (Add Math Math))
            (rewrite (Add a b) (Add b a))
            (let $x (Add (Num 1) (Num 2)))
            (run 3)
            (check (= $x (Add (Num 2) (Num 1))))
            ",
        )
        .unwrap();
}

#[test]
fn rewrite_name_with_ruleset() {
    let mut egraph = EGraph::default();
    egraph
        .parse_and_run_program(
            None,
            "
            (datatype Math (Num i64) (Mul Math Math))
            (ruleset my-rules)
            (rewrite (Mul a (Num 0)) (Num 0) :name \"mul-zero\" :ruleset my-rules)
            (let $x (Mul (Num 99) (Num 0)))
            (run my-rules 3)
            (check (= $x (Num 0)))
            ",
        )
        .unwrap();
}

// =====================================================================
// `clear_function` tests.
//
// The clear path bumps the table's major generation, which is the
// source of most subtle bugs: cached subsets, hash indexes, seminaive
// watermarks, and `RowId` values from the old generation must all be
// invalidated lazily before the next read/write touches them. Each
// test below threads several such failure modes together so the same
// e-graph exercises a realistic sequence rather than one assertion at
// a time.
// =====================================================================

/// Single-function lifecycle: declare → no-op clear of empty table →
/// populate → assert the three different read paths agree on the
/// contents (`get_size`, `eclass_of`, `constructor_enodes`) →
/// clear → assert all three read paths report empty → re-insert with
/// completely new keys → assert the old keys are gone and the new
/// ones are present. Run the populate/clear/re-insert pass repeatedly
/// to make sure the generation counter and the index-reset path keep
/// working past the first cycle.
#[test]
fn clear_function_lifecycle() {
    let mut egraph = EGraph::default();
    egraph
        .parse_and_run_program(None, "(datatype Math (Num i64))")
        .unwrap();

    // Clearing an empty function is a no-op (and does it twice to
    // exercise the `data.len() == 0` early-return inside
    // `SortedWritesTable::clear`).
    assert_eq!(egraph.get_size("Num"), 0);
    egraph.clear_function("Num").unwrap();
    egraph.clear_function("Num").unwrap();
    assert_eq!(egraph.get_size("Num"), 0);

    for round in 0..3i64 {
        let a = round * 10;
        let b = round * 10 + 1;
        let c = round * 10 + 2;

        // Populate, then read through all three paths to warm caches
        // (and any per-table indexes) before we clear.
        egraph
            .parse_and_run_program(None, &format!("(Num {a}) (Num {b}) (Num {c})"))
            .unwrap();
        assert_eq!(egraph.get_size("Num"), 3);

        let key_a = egraph.base_to_value::<i64>(a);
        assert!(
            egraph
                .update(|fs| fs.eclass_of("Num", key_a))
                .unwrap()
                .is_some()
        );

        let mut seen = 0;
        egraph
            .update(|fs| fs.constructor_enodes("Num", |_| seen += 1))
            .unwrap();
        assert_eq!(seen, 3);

        // Now clear and re-read through every access path: each must
        // observe the new (empty) generation, not phantom rows from
        // before the generation bump.
        egraph.clear_function("Num").unwrap();
        assert_eq!(egraph.get_size("Num"), 0);
        assert!(
            egraph
                .update(|fs| fs.eclass_of("Num", key_a))
                .unwrap()
                .is_none()
        );
        let mut seen_after = 0;
        egraph
            .update(|fs| fs.constructor_enodes("Num", |_| seen_after += 1))
            .unwrap();
        assert_eq!(seen_after, 0);
        let check_old = egraph.parse_and_run_program(None, &format!("(check (Num {a}))"));
        assert!(
            check_old.is_err(),
            "round {round}: (Num {a}) should be absent after clear, got {check_old:?}"
        );
    }
}

/// Cross-cutting scenario: a rule that derives from one function,
/// a sibling function we expect not to touch, a `:merge` function
/// whose accumulator state must be reset, and an index over the
/// cleared function that was warmed by an earlier rule run.
///
/// The scenario verifies, in order:
///   1. `clear_function` only clears the named function, not the
///      sibling `Sym` and not the derived `Saw` populated by a rule.
///   2. The `:merge` accumulator on `score` resets — a write after
///      the clear does not silently re-merge with the old value.
///   3. The cleared `Num` does not yield phantom rows via the rule's
///      cached index over the old generation.
///   4. After re-insert, the rule re-fires on the new `Num` rows,
///      which catches seminaive-watermark-not-invalidated bugs.
#[test]
fn clear_function_with_rules_siblings_and_merge() {
    let mut egraph = EGraph::default();
    egraph
        .parse_and_run_program(
            None,
            "
            (datatype Math (Num i64) (Sym i64))
            (relation Saw (i64))
            (rule ((Num x)) ((Saw x)))
            (function score (i64) i64 :merge (max old new))

            (Num 1) (Num 2) (Num 3)
            (Sym 10) (Sym 20)
            (set (score 7) 5)
            (set (score 7) 10)
            (set (score 7) 8)
            (run 1)
            (check (Saw 1)) (check (Saw 2)) (check (Saw 3))
            (check (= (score 7) 10))
            ",
        )
        .unwrap();
    assert_eq!(egraph.get_size("Num"), 3);
    assert_eq!(egraph.get_size("Sym"), 2);
    assert_eq!(egraph.get_size("Saw"), 3);
    assert_eq!(egraph.get_size("score"), 1);

    // (1) Clear Num and score. Sym is a sibling datatype constructor;
    // Saw is derived data populated by the rule. Neither should be
    // affected.
    egraph.clear_function("Num").unwrap();
    egraph.clear_function("score").unwrap();
    assert_eq!(egraph.get_size("Num"), 0);
    assert_eq!(egraph.get_size("score"), 0);
    assert_eq!(egraph.get_size("Sym"), 2);
    assert_eq!(egraph.get_size("Saw"), 3);
    egraph
        .parse_and_run_program(None, "(check (Sym 10))")
        .unwrap();

    // (3) The cleared Num must not yield phantom rows via a cached
    // index — the major-generation bump on clear should force the
    // index to rebuild before the check runs.
    let phantom = egraph.parse_and_run_program(None, "(check (Num 1))");
    assert!(
        phantom.is_err(),
        "old (Num 1) should not be findable after clear, got: {phantom:?}"
    );

    // (2) Repopulate `score` with a smaller value than the cleared
    // accumulator. If the merge state survived the clear, the next
    // line's `check` would see 10 instead of 3.
    egraph
        .parse_and_run_program(
            None,
            "
            (set (score 7) 3)
            (check (= (score 7) 3))
            ",
        )
        .unwrap();

    // (4) Re-insert into Num and re-run the rule. The rule must fire
    // on the new rows, which exercises the seminaive watermark and
    // the rule's table index after a generation bump.
    egraph
        .parse_and_run_program(
            None,
            "
            (Num 100) (Num 200)
            (run 1)
            (check (Saw 100)) (check (Saw 200))
            ",
        )
        .unwrap();
    // 3 original Saw rows + 2 from the new run = 5.
    assert_eq!(egraph.get_size("Saw"), 5);
}

/// `clear_function` on a name that was never declared returns an
/// `UnboundFunction` error rather than panicking. Kept standalone
/// because there's nothing to thread through — the e-graph never
/// transitions out of its empty starting state.
#[test]
fn clear_function_unknown_function_errors() {
    let mut egraph = EGraph::default();
    let err = egraph.clear_function("DoesNotExist").unwrap_err();
    match err {
        Error::TypeError(TypeError::UnboundFunction(name, _)) => {
            assert_eq!(name, "DoesNotExist");
        }
        other => panic!("expected UnboundFunction, got {other:?}"),
    }
}