aspire 0.2.0

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

use aspire::{Control, ShowType, Symbol};

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

    let mut handle = ctl.solve_iter().unwrap();
    let mut models = Vec::new();
    while let Some(model) = handle.next_model().unwrap() {
        models.push(model.symbols(ShowType::Shown).unwrap());
    }
    let result = handle.close().unwrap();

    assert!(result.satisfiable);
    assert!(result.exhausted);
    assert_eq!(models.len(), 1);

    let a = Symbol::id("a", true).unwrap();
    let b = Symbol::id("b", true).unwrap();
    assert!(models[0].contains(&a));
    assert!(models[0].contains(&b));
}

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

    let mut handle = ctl.solve_iter().unwrap();
    let mut count = 0;
    while handle.next_model().unwrap().is_some() {
        count += 1;
    }
    let result = handle.close().unwrap();

    assert!(result.satisfiable);
    assert!(result.exhausted);
    assert_eq!(count, 4);
}

#[test]
fn solve_stop_early() {
    let mut ctl = Control::new(&["0"]).unwrap();
    ctl.add("base", &[], "{a}. {b}. {c}.").unwrap();
    ctl.ground_base().unwrap();

    let mut handle = ctl.solve_iter().unwrap();
    let model = handle.next_model().unwrap();
    assert!(model.is_some());
    // drop handle without exhausting — stops early
    let result = handle.close().unwrap();
    assert!(result.satisfiable);
    assert!(!result.exhausted);
}

#[test]
fn solve_unsat() {
    let mut ctl = Control::new(&["0"]).unwrap();
    ctl.add("base", &[], "a. :- a.").unwrap();
    ctl.ground_base().unwrap();

    let mut handle = ctl.solve_iter().unwrap();
    assert!(handle.next_model().unwrap().is_none());
    let result = handle.close().unwrap();
    assert!(result.unsatisfiable);
}

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

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

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

#[test]
fn model_number() {
    let mut ctl = Control::new(&["0"]).unwrap();
    ctl.add("base", &[], "{a}.").unwrap();
    ctl.ground_base().unwrap();

    let mut handle = ctl.solve_iter().unwrap();
    let mut numbers = Vec::new();
    while let Some(model) = handle.next_model().unwrap() {
        numbers.push(model.number().unwrap());
    }

    numbers.sort();
    assert_eq!(numbers, vec![1, 2]);
}