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

use crate::datastructures::Assignment;
use crate::formulas::{EncodedFormula, Formula, FormulaFactory, Literal};

/// Restricts this formula with the give assignment.
///
/// [`FormulaFactory`] also provides this transformation as a method. So you
/// can also use `f.restrict(formula, assignment)` instead of `restrict(formula,
/// assignment, f)`.
///
/// # Examples
///
/// Basic usage:
///
/// ```
/// # use logicng::formulas::{FormulaFactory, ToFormula};
/// # use logicng::datastructures::Assignment;
/// # use logicng::operations::transformations::restrict;
///
/// let f = FormulaFactory::new();
///
/// let a = f.var("a");
/// let b = f.var("b");
/// let formula = "a & b".to_formula(&f);
///
/// let assignment1 = Assignment::from_variables(&[a], &[]);
/// let assignment2 = Assignment::from_variables(&[], &[a]);
///
/// let restricted1 = restrict(formula, &assignment1, &f);
/// let restricted2 = restrict(formula, &assignment2, &f);
///
/// assert_eq!(restricted1.to_string(&f), "b");
/// assert_eq!(restricted2.to_string(&f), "$false");
/// ```
pub fn restrict(formula: EncodedFormula, assignment: &Assignment, f: &FormulaFactory) -> EncodedFormula {
    use Formula::{And, Cc, Equiv, False, Impl, Lit, Not, Or, Pbc, True};
    match formula.unpack(f) {
        Lit(lit) => assignment.restrict_lit(lit),
        Equiv((left, right)) => {
            let rec_left = restrict(left, assignment, f);
            let rec_right = restrict(right, assignment, f);
            f.equivalence(rec_left, rec_right)
        }
        Impl((left, right)) => {
            let rec_left = restrict(left, assignment, f);
            let rec_right = restrict(right, assignment, f);
            f.implication(rec_left, rec_right)
        }
        Or(ops) => {
            let rec_ops = ops.map(|op| restrict(op, assignment, f)).collect::<Box<[_]>>();
            f.or(&rec_ops)
        }
        And(ops) => {
            let rec_ops = ops.map(|op| restrict(op, assignment, f)).collect::<Box<[_]>>();
            f.and(&rec_ops)
        }
        Not(op) => {
            let rec_op = restrict(op, assignment, f);
            f.not(rec_op)
        }
        True | False => formula,
        Pbc(pbc) => pbc.clone().restrict(assignment, f),
        Cc(cc) => cc.clone().restrict(assignment, f),
    }
}

pub fn restrict_lit(formula: EncodedFormula, lit: Literal, f: &FormulaFactory) -> EncodedFormula {
    use Formula::{And, Cc, Equiv, False, Impl, Lit, Not, Or, Pbc, True};
    match formula.unpack(f) {
        Lit(this_lit) => {
            if this_lit.variable() != lit.variable() {
                formula
            } else if this_lit.phase() == lit.phase() {
                f.verum()
            } else {
                f.falsum()
            }
        }
        Equiv((left, right)) => {
            let rec_left = restrict_lit(left, lit, f);
            let rec_right = restrict_lit(right, lit, f);
            f.equivalence(rec_left, rec_right)
        }
        Impl((left, right)) => {
            let rec_left = restrict_lit(left, lit, f);
            let rec_right = restrict_lit(right, lit, f);
            f.implication(rec_left, rec_right)
        }
        Or(ops) => {
            let rec_ops = ops.map(|op| restrict_lit(op, lit, f)).collect::<Box<[_]>>();
            f.or(&rec_ops)
        }
        And(ops) => {
            let rec_ops = ops.map(|op| restrict_lit(op, lit, f)).collect::<Box<[_]>>();
            f.and(&rec_ops)
        }
        Not(op) => {
            let rec_op = restrict_lit(op, lit, f);
            f.not(rec_op)
        }
        True | False => formula,
        Pbc(pbc) => pbc.clone().restrict(&Assignment::from_lit(lit), f),
        Cc(cc) => cc.clone().restrict(&Assignment::from_lit(lit), f),
    }
}