logicng 0.1.0-alpha.3

A Library for Creating, Manipulating, and Solving Boolean Formulas
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

use crate::solver::minisat::sat::Tristate;
use crate::solver::minisat::sat::Tristate::False;
use crate::solver::minisat::{MiniSat, MiniSatConfig, SolverState};
use crate::solver::tests::generate_pigeon_hole;
use crate::util::test_util::F;
use Tristate::True;

#[test]
fn test_inc_dec() {
    let ff = F::new();
    let f = &ff.f;
    let mut s = MiniSat::new();
    s.add(f.variable("a"), f);
    let state1 = s.save_state();
    assert_eq!(state1, SolverState::new(0, [1, 1, 0, 0, 1, 0, 0]));
    assert_eq!(s.sat(), True);

    s.add(generate_pigeon_hole(5, f), f);
    assert_eq!(s.sat(), False);
    s.load_state(&state1);
    assert_eq!(s.sat(), True);

    s.add(f.literal("a", false), f);
    assert_eq!(s.sat(), False);
    s.load_state(&state1);
    assert_eq!(s.sat(), True);

    s.add(generate_pigeon_hole(5, f), f);
    let state2 = s.save_state();
    assert_eq!(state2, SolverState::new(1, [1, 31, 81, 0, 1, 0, 0]));
    s.add(generate_pigeon_hole(4, f), f);
    assert_eq!(s.sat(), False);
    s.load_state(&state2);
    assert_eq!(s.sat(), False);
    s.load_state(&state1);
    assert_eq!(s.sat(), True);
}

#[test]
#[should_panic(expected = "The given solver state is not valid anymore.")]
fn test_inc_dec_deep_1() {
    let ff = F::new();
    let f = &ff.f;
    let mut s = MiniSat::new();
    s.add(f.variable("a"), f);
    let state1 = s.save_state();
    s.add(f.variable("b"), f);
    assert_eq!(s.sat(), True);

    let state2 = s.save_state();
    s.add(f.literal("a", false), f);
    assert_eq!(s.sat(), False);
    s.load_state(&state1);
    s.load_state(&state2);
}

#[test]
#[should_panic(expected = "The given solver state is not valid anymore.")]
fn test_inc_dec_deep_2() {
    let ff = F::new();
    let f = &ff.f;
    let mut s = MiniSat::new();
    s.add(f.variable("a"), f);
    let state1 = s.save_state();
    s.add(f.variable("b"), f);
    assert_eq!(s.sat(), True);

    let _state2 = s.save_state();
    s.add(f.literal("a", false), f);
    assert_eq!(s.sat(), False);
    s.load_state(&state1);

    s.add(f.literal("b", false), f);
    assert_eq!(s.sat(), True);
    let state3 = s.save_state();
    s.add(f.literal("a", false), f);
    assert_eq!(s.sat(), False);
    s.load_state(&state3);
    s.add(f.variable("c"), f);
    let state4 = s.save_state();
    let state5 = s.save_state();
    s.load_state(&state4);
    s.load_state(&state5);
}

#[test]
#[should_panic(expected = "The given solver state is not valid anymore.")]
fn test_inc_dec_deep_3() {
    let ff = F::new();
    let f = &ff.f;
    let mut s = MiniSat::new();
    s.add(f.variable("a"), f);
    let state1 = s.save_state();
    s.add(f.variable("b"), f);
    assert_eq!(s.sat(), True);

    let _state2 = s.save_state();
    s.add(f.literal("a", false), f);
    assert_eq!(s.sat(), False);
    s.load_state(&state1);

    s.add(f.literal("b", false), f);
    assert_eq!(s.sat(), True);
    let state3 = s.save_state();
    s.add(f.literal("a", false), f);
    assert_eq!(s.sat(), False);
    s.load_state(&state3);
    s.add(f.variable("c"), f);
    let state4 = s.save_state();
    let _state5 = s.save_state();
    s.load_state(&state4);
    assert_eq!(s.sat(), True);
    s.load_state(&state1);
    assert_eq!(s.sat(), True);
    s.load_state(&state3);
}

#[test]
#[should_panic(expected = "Cannot save a state when the incremental mode is deactivated")]
fn test_not_incremental_1() {
    let mut s = MiniSat::new_with_config(MiniSatConfig::default().incremental(false));
    s.save_state();
}

#[test]
#[should_panic(expected = "Cannot load a state when the incremental mode is deactivated")]
fn test_not_incremental_2() {
    let mut s = MiniSat::new_with_config(MiniSatConfig::default().incremental(false));
    s.underlying_solver.load_state([0, 0, 0, 0, 0, 0, 0]);
}