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

use crate::formulas::{EncodedFormula, FormulaFactory, Literal, Variable};
use crate::solver::minisat::sat::{mk_lit, MsLit};
use crate::solver::minisat::MiniSat;

// TODO: for MiniSat, we also would need a proposition to be passed to `add_clause` methods
//       (actually, we need the FormulaFactory only for Vec<Formula> and we need a Proposition only for MiniSat)

/// The result of an encoding.
///
/// Encodings are often used only when adding formulas to the SAT solver.
/// Therefore, it is not necessary to generate all the formulas required for the
/// encoding in the formula factory and therefore polluting the factory and the
/// heap.  This class can be used to connect an encoding directly with a SAT
/// solver and therefore introducing the variables only on the solver - not in
/// the factory. When working with many encodings, this can be a large
/// performance gain.
pub trait EncodingResult {
    /// Returns a new auxiliary variable.
    fn new_cc_variable(&mut self, f: &FormulaFactory) -> Variable;
    /// Resets the result.
    fn reset(&mut self);
    /// Adds a clause to the result.
    fn add_clause(&mut self, f: &FormulaFactory, lits: &[Literal]);
    /// Adds a clause of length 1 to the result.
    fn add_clause1(&mut self, f: &FormulaFactory, literal: Literal);
    /// Adds a clause of length 2 to the result.
    fn add_clause2(&mut self, f: &FormulaFactory, literal1: Literal, literal2: Literal);
    /// Adds a clause of length 3 to the result.
    fn add_clause3(&mut self, f: &FormulaFactory, literal1: Literal, literal2: Literal, literal3: Literal);
    /// Adds a clause of length 4 to the result.
    fn add_clause4(&mut self, f: &FormulaFactory, literal1: Literal, literal2: Literal, literal3: Literal, literal4: Literal);
}

impl EncodingResult for MiniSat {
    fn new_cc_variable(&mut self, f: &FormulaFactory) -> Variable {
        let index = self.underlying_solver.new_var(self.config.initial_phase, true);
        let variable = f.new_cc_variable();
        self.underlying_solver.add_variable(variable, index);
        variable
    }

    fn reset(&mut self) {
        // do nothing
    }

    fn add_clause(&mut self, _f: &FormulaFactory, lits: &[Literal]) {
        let mut clause_vec = Vec::<MsLit>::with_capacity(lits.len());
        for lit in lits {
            clause_vec.push(self.add_literal(lit));
        }
        self.underlying_solver.add_clause(clause_vec, &None);
        self.set_solver_to_undef();
    }

    fn add_clause1(&mut self, _f: &FormulaFactory, literal: Literal) {
        let clause_vec = vec![self.add_literal(&literal)];
        self.underlying_solver.add_clause(clause_vec, &None);
        self.set_solver_to_undef();
    }

    fn add_clause2(&mut self, _f: &FormulaFactory, literal1: Literal, literal2: Literal) {
        let clause_vec = vec![self.add_literal(&literal1), self.add_literal(&literal2)];
        self.underlying_solver.add_clause(clause_vec, &None);
        self.set_solver_to_undef();
    }

    fn add_clause3(&mut self, _f: &FormulaFactory, literal1: Literal, literal2: Literal, literal3: Literal) {
        let clause_vec = vec![self.add_literal(&literal1), self.add_literal(&literal2), self.add_literal(&literal3)];
        self.underlying_solver.add_clause(clause_vec, &None);
        self.set_solver_to_undef();
    }

    fn add_clause4(&mut self, _f: &FormulaFactory, literal1: Literal, literal2: Literal, literal3: Literal, literal4: Literal) {
        let clause_vec =
            vec![self.add_literal(&literal1), self.add_literal(&literal2), self.add_literal(&literal3), self.add_literal(&literal4)];
        self.underlying_solver.add_clause(clause_vec, &None);
        self.set_solver_to_undef();
    }
}

impl MiniSat {
    fn add_literal(&mut self, lit: &Literal) -> MsLit {
        let index = self.underlying_solver.idx_for_variable(lit.variable()).unwrap_or_else(|| {
            let new_index = self.underlying_solver.new_var(!self.config.initial_phase, true);
            self.underlying_solver.add_variable(lit.variable(), new_index);
            new_index
        });
        mk_lit(index, !lit.phase())
    }
}

impl EncodingResult for Vec<EncodedFormula> {
    fn new_cc_variable(&mut self, f: &FormulaFactory) -> Variable {
        f.new_cc_variable()
    }

    fn reset(&mut self) {
        self.clear();
    }

    fn add_clause(&mut self, f: &FormulaFactory, lits: &[Literal]) {
        let clause = f.or(&lits.iter().map(|lit| EncodedFormula::from(*lit)).collect::<Box<[_]>>());
        self.push(clause);
    }

    fn add_clause1(&mut self, f: &FormulaFactory, literal: Literal) {
        let clause = f.or(&[literal.into()]);
        self.push(clause);
    }

    fn add_clause2(&mut self, f: &FormulaFactory, literal1: Literal, literal2: Literal) {
        let clause = f.or(&[literal1.into(), literal2.into()]);
        self.push(clause);
    }

    fn add_clause3(&mut self, f: &FormulaFactory, literal1: Literal, literal2: Literal, literal3: Literal) {
        let clause = f.or(&[literal1.into(), literal2.into(), literal3.into()]);
        self.push(clause);
    }

    fn add_clause4(&mut self, f: &FormulaFactory, literal1: Literal, literal2: Literal, literal3: Literal, literal4: Literal) {
        let clause = f.or(&[literal1.into(), literal2.into(), literal3.into(), literal4.into()]);
        self.push(clause);
    }
}