trit-bdd 0.4.0

use std::collections::HashSet;

use trit_bdd::{BddError, Quantifier, quantify_bdd};
use trit_core::algebra::Algebra;
use trit_core::ast::Expr;
use trit_core::parser::Parser;
use trit_core::value::Ternary;

fn parse(src: &str) -> Expr {
    Parser::parse(src).expect("测试表达式应可解析")
}

#[test]
fn exists_over_one_variable_returns_free_witness() {
    let expr = parse("a & b");
    let q = quantify_bdd(
        &expr,
        &["a".to_string()],
        Quantifier::Exists,
        Algebra::Kleene,
        &HashSet::new(),
    )
    .expect("量化不应报错");
    assert!(q.is_satisfiable());
    assert_eq!(q.free_variables(), ["b".to_string()]);
    let witness = q.witness().expect("应有见证");
    assert_eq!(witness.get("b"), Some(Ternary::True));
    assert_eq!(witness.get("a"), None, "被量化变量不应出现在见证里");
}

#[test]
fn forall_over_one_variable_returns_free_counterexample() {
    let expr = parse("a & b");
    let q = quantify_bdd(
        &expr,
        &["a".to_string()],
        Quantifier::Forall,
        Algebra::Kleene,
        &HashSet::new(),
    )
    .expect("量化不应报错");
    assert!(!q.is_valid());
    let counterexample = q.counterexample().expect("应有反例");
    assert_ne!(
        counterexample.get("b"),
        Some(Ternary::True),
        "b=1 时 a&b 对 a 全称成立，不能是反例"
    );
}

#[test]
fn forall_excluded_middle_depends_on_binary_domain() {
    let expr = parse("a | !a");
    let binary: HashSet<String> = ["a".to_string()].into_iter().collect();
    let binary_q = quantify_bdd(
        &expr,
        &["a".to_string()],
        Quantifier::Forall,
        Algebra::Kleene,
        &binary,
    )
    .expect("量化不应报错");
    assert!(binary_q.is_valid(), "二值域下排中律恒真");

    let ternary_q = quantify_bdd(
        &expr,
        &["a".to_string()],
        Quantifier::Forall,
        Algebra::Kleene,
        &HashSet::new(),
    )
    .expect("量化不应报错");
    assert!(!ternary_q.is_valid(), "三值域下 a=X 时 a|!a=X");
    let counterexample = ternary_q.counterexample().expect("应有反例");
    assert!(
        counterexample.is_empty(),
        "反例只含自由变量，而 a 已被全称量化掉：{counterexample:?}"
    );
}

#[test]
fn exists_of_contradiction_is_unsatisfiable() {
    let expr = parse("a & !a");
    let q = quantify_bdd(
        &expr,
        &["a".to_string()],
        Quantifier::Exists,
        Algebra::Kleene,
        &HashSet::new(),
    )
    .expect("量化不应报错");
    assert!(!q.is_satisfiable());
    assert!(q.witness().is_none());
}

#[test]
fn quantifying_all_variables_yields_a_boolean() {
    let expr = parse("a & b");
    let vars = ["a".to_string(), "b".to_string()];
    let exists = quantify_bdd(
        &expr,
        &vars,
        Quantifier::Exists,
        Algebra::Kleene,
        &HashSet::new(),
    )
    .expect("量化不应报错");
    assert!(exists.is_satisfiable());
    assert!(exists.free_variables().is_empty());
    assert!(exists.witness().is_some_and(|w| w.is_empty()));

    let forall = quantify_bdd(
        &expr,
        &vars,
        Quantifier::Forall,
        Algebra::Kleene,
        &HashSet::new(),
    )
    .expect("量化不应报错");
    assert!(!forall.is_valid());
    assert!(forall.counterexample().is_some_and(|c| c.is_empty()));
}

#[test]
fn unknown_variable_is_an_error() {
    let expr = parse("a & b");
    let err = quantify_bdd(
        &expr,
        &["c".to_string()],
        Quantifier::Exists,
        Algebra::Kleene,
        &HashSet::new(),
    )
    .unwrap_err();
    assert!(matches!(err, BddError::UnknownVariable(v) if v == "c"));
}