1"""Inference in propositional logic"""
2
3from ..core.sympify import sympify
4from ..utilities import ordered
5from .boolalg import And, Not, conjuncts, to_cnf
6
7
8def literal_symbol(literal):
9    """
10    The symbol in this literal (without the negation).
11
12    Examples
13    ========
14
15    >>> literal_symbol(a)
16    a
17    >>> literal_symbol(~a)
18    a
19
20    """
21    if literal is True or literal is False:
22        return literal
23    try:
24        if literal.is_Symbol:
25            return literal
26        if literal.is_Not:
27            return literal_symbol(literal.args[0])
28        else:
29            raise ValueError
30    except (AttributeError, ValueError):
31        raise ValueError('Argument must be a boolean literal.')
32
33
34def satisfiable(expr, algorithm='dpll2', all_models=False):
35    """
36    Check satisfiability of a propositional sentence.
37    Returns a model when it succeeds.
38    Returns {true: true} for trivially true expressions.
39
40    On setting all_models to True, if given expr is satisfiable then
41    returns a generator of models. However, if expr is unsatisfiable
42    then returns a generator containing the single element False.
43
44    Examples
45    ========
46
47    >>> satisfiable(a & ~b)
48    {a: True, b: False}
49    >>> satisfiable(a & ~a)
50    False
51    >>> satisfiable(True)
52    {true: True}
53    >>> next(satisfiable(a & ~a, all_models=True))
54    False
55    >>> models = satisfiable((a >> b) & b, all_models=True)
56    >>> next(models)
57    {a: False, b: True}
58    >>> next(models)
59    {a: True, b: True}
60    >>> def use_models(models):
61    ...     for model in models:
62    ...         if model:
63    ...             # Do something with the model.
64    ...             return model
65    ...         else:
66    ...             # Given expr is unsatisfiable.
67    ...             print('UNSAT')
68    >>> use_models(satisfiable(a >> ~a, all_models=True))
69    {a: False}
70    >>> use_models(satisfiable(a ^ a, all_models=True))
71    UNSAT
72
73    """
74    expr = to_cnf(expr)
75    if algorithm == 'dpll':
76        from .algorithms.dpll import dpll_satisfiable
77        return dpll_satisfiable(expr)
78    elif algorithm == 'dpll2':
79        from .algorithms.dpll2 import dpll_satisfiable
80        return dpll_satisfiable(expr, all_models)
81    else:
82        raise NotImplementedError
83
84
85def valid(expr):
86    """
87    Check validity of a propositional sentence.
88    A valid propositional sentence is True under every assignment.
89
90    Examples
91    ========
92
93    >>> valid(a | ~a)
94    True
95    >>> valid(a | b)
96    False
97
98    References
99    ==========
100
101    * https://en.wikipedia.org/wiki/Validity
102
103    """
104    return not satisfiable(Not(expr))
105
106
107def pl_true(expr, model={}, deep=False):
108    """
109    Returns whether the given assignment is a model or not.
110
111    If the assignment does not specify the value for every proposition,
112    this may return None to indicate 'not obvious'.
113
114    Parameters
115    ==========
116
117    model : dict, optional, default: {}
118        Mapping of symbols to boolean values to indicate assignment.
119    deep: boolean, optional, default: False
120        Gives the value of the expression under partial assignments
121        correctly. May still return None to indicate 'not obvious'.
122
123
124    Examples
125    ========
126
127    >>> pl_true(a & b, {a: True, b: True})
128    True
129    >>> pl_true(a & b, {a: False})
130    False
131    >>> pl_true(a & b, {a: True})
132    >>> pl_true(a & b, {a: True}, deep=True)
133    >>> pl_true(a >> (b >> a))
134    >>> pl_true(a >> (b >> a), deep=True)
135    True
136    >>> pl_true(a & ~a)
137    >>> pl_true(a & ~a, deep=True)
138    False
139    >>> pl_true(a & b & (~a | ~b), {a: True})
140    >>> pl_true(a & b & (~a | ~b), {a: True}, deep=True)
141    False
142
143    """
144    from ..core import Symbol
145    from .boolalg import BooleanFunction
146    boolean = (True, False)
147
148    def _validate(expr):
149        if isinstance(expr, Symbol) or expr in boolean:
150            return True
151        if not isinstance(expr, BooleanFunction):
152            return False
153        return all(_validate(arg) for arg in expr.args)
154
155    if expr in boolean:
156        return expr
157    expr = sympify(expr)
158    if not _validate(expr):
159        raise ValueError(f'{expr} is not a valid boolean expression')
160    model = {k: v for k, v in model.items() if v in boolean}
161    result = expr.subs(model)
162    if result in boolean:
163        return bool(result)
164    if deep:
165        model = {k: True for k in result.atoms()}
166        if pl_true(result, model):
167            if valid(result):
168                return True
169        else:
170            if not satisfiable(result):
171                return False
172
173
174def entails(expr, formula_set={}):
175    """
176    Check whether the given expr_set entail an expr.
177    If formula_set is empty then it returns the validity of expr.
178
179    Examples
180    ========
181
182    >>> entails(a, [a >> b, b >> c])
183    False
184    >>> entails(c, [a >> b, b >> c, a])
185    True
186    >>> entails(a >> b)
187    False
188    >>> entails(a >> (b >> a))
189    True
190
191    References
192    ==========
193
194    * https://en.wikipedia.org/wiki/Logical_consequence
195
196    """
197    formula_set = list(formula_set)
198    formula_set.append(Not(expr))
199    return not satisfiable(And(*formula_set))
200
201
202class KB:
203    """Base class for all knowledge bases."""
204
205    def __init__(self, sentence=None):
206        self.clauses_ = set()
207        if sentence:
208            self.tell(sentence)
209
210    def tell(self, sentence):
211        raise NotImplementedError
212
213    def ask(self, query):
214        raise NotImplementedError
215
216    def retract(self, sentence):
217        raise NotImplementedError
218
219    @property
220    def clauses(self):
221        return list(ordered(self.clauses_))
222
223
224class PropKB(KB):
225    """A KB for Propositional Logic.  Inefficient, with no indexing."""
226
227    def tell(self, sentence):
228        """Add the sentence's clauses to the KB
229
230        Examples
231        ========
232
233        >>> l = PropKB()
234        >>> l.clauses
235        []
236
237        >>> l.tell(x | y)
238        >>> l.clauses
239        [x | y]
240
241        >>> l.tell(y)
242        >>> l.clauses
243        [y, x | y]
244
245        """
246        for c in conjuncts(to_cnf(sentence)):
247            self.clauses_.add(c)
248
249    def ask(self, query):
250        """Checks if the query is true given the set of clauses.
251
252        Examples
253        ========
254
255        >>> l = PropKB()
256        >>> l.tell(x & ~y)
257        >>> l.ask(x)
258        True
259        >>> l.ask(y)
260        False
261
262        """
263        return entails(query, self.clauses_)
264
265    def retract(self, sentence):
266        """Remove the sentence's clauses from the KB
267
268        Examples
269        ========
270
271        >>> l = PropKB()
272        >>> l.clauses
273        []
274
275        >>> l.tell(x | y)
276        >>> l.clauses
277        [x | y]
278
279        >>> l.retract(x | y)
280        >>> l.clauses
281        []
282
283        """
284        for c in conjuncts(to_cnf(sentence)):
285            self.clauses_.discard(c)
286