aspire 0.5.2

Rust bindings for Clingo
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

use aspire::{Atom, Control, ExternalType, GroundStatement, Sign, Symbol};

#[test]
fn observe_rules() {
    let mut ctl = Control::new(&[]).unwrap();
    // Non-trivial program so atoms aren't simplified away
    ctl.add("base", &[], "a :- not b. b :- not a.").unwrap();
    let stmts = ctl.ground_base_observed().unwrap();

    let rules: Vec<_> = stmts
        .iter()
        .filter(|s| matches!(s, GroundStatement::Rule { .. }))
        .collect();
    assert!(!rules.is_empty());

    let a = Symbol::id("a", true).unwrap();
    let b = Symbol::id("b", true).unwrap();

    // "a :- not b." should appear with positive head a, negative body b
    let has_a_rule = stmts.iter().any(|s| match s {
        GroundStatement::Rule {
            choice: false,
            head,
            body,
        } => {
            head.iter().any(|at| *at == Atom::Symbol(a))
                && body
                    .iter()
                    .any(|lit| lit.0 == Sign::Neg && lit.1 == Atom::Symbol(b))
        }
        _ => false,
    });
    assert!(has_a_rule);
}

#[test]
fn observe_choice_rule() {
    let mut ctl = Control::new(&[]).unwrap();
    ctl.add("base", &[], "{a}. {b}.").unwrap();
    let stmts = ctl.ground_base_observed().unwrap();

    let choice_rules: Vec<_> = stmts
        .iter()
        .filter(|s| matches!(s, GroundStatement::Rule { choice: true, .. }))
        .collect();
    assert!(!choice_rules.is_empty());
}

#[test]
fn observe_external() {
    let mut ctl = Control::new(&[]).unwrap();
    ctl.add("base", &[], "#external a.").unwrap();
    let stmts = ctl.ground_base_observed().unwrap();

    let externals: Vec<_> = stmts
        .iter()
        .filter(|s| matches!(s, GroundStatement::External { .. }))
        .collect();
    assert!(!externals.is_empty());
    assert!(externals.iter().any(|s| matches!(
        s,
        GroundStatement::External {
            external_type: ExternalType::False,
            ..
        }
    )));
}

#[test]
fn still_solvable_after_observe() {
    let mut ctl = Control::new(&["0"]).unwrap();
    ctl.add("base", &[], "a :- not b. b :- not a.").unwrap();
    let _stmts = ctl.ground_base_observed().unwrap();

    let mut handle = ctl.solve_iter().unwrap();
    let model = handle.next_model().unwrap();
    assert!(model.is_some());
}

#[test]
fn facts_simplified_away() {
    // Pure facts are simplified by the grounder — they don't appear
    // as resolved symbols in the observer output.
    let mut ctl = Control::new(&[]).unwrap();
    ctl.add("base", &[], "a.").unwrap();
    let stmts = ctl.ground_base_observed().unwrap();

    // The rule exists but the head atom is Aux (no output_atom mapping)
    let rules: Vec<_> = stmts
        .iter()
        .filter(|s| matches!(s, GroundStatement::Rule { .. }))
        .collect();
    assert!(!rules.is_empty());
}

#[test]
fn assign_external_after_observe() {
    // Regression: ground_observed used to leave a dangling observer pointer,
    // causing a segfault on subsequent operations.
    let mut ctl = Control::new(&[]).unwrap();
    ctl.add("base", &[], "#external state(a). #external state(b).")
        .unwrap();
    let _stmts = ctl.ground_base_observed().unwrap();

    let sym = Symbol::parse("state(a)").unwrap();
    ctl.assign_external(sym, aspire::TruthValue::True).unwrap();
}