# Copyright 2019 Ingmar Dasseville, Pierre Carbonnelle
#
# This file is part of Interactive_Consultant.
#
# This program is free software: you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation, either version 3 of the License, or
# (at your option) any later version.
#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <https://www.gnu.org/licenses/>.
"""
Methods to simplify a logic expression.
This module monkey-patches the Expression class and sub-classes.
"""
import sys
from typing import List
from .Expression import (
Constructor, Expression, IfExpr, AQuantification, \
BinaryOperator, AEquivalence, AImplication, ADisjunction, \
AConjunction, AComparison, ASumMinus, AMultDiv, APower, \
AUnary, AAggregate, AppliedSymbol, UnappliedSymbol, \
Number, Brackets, Variable, TRUE, FALSE)
from .Parse import Enumeration, Tuple
from .Assignments import Status, Assignment
from .utils import INT
# class Expression ###########################################################
def _change(self, sub_exprs=None, ops=None, value=None, simpler=None,
co_constraint=None):
" change attributes of an expression, and resets derived attributes "
if sub_exprs is not None:
self.sub_exprs = sub_exprs
if ops is not None:
self.operator = ops
if co_constraint is not None:
self.co_constraint = co_constraint
if value is not None:
self.value = value
elif simpler is not None:
if type(simpler) in [Constructor, Number]:
self.value = simpler
elif simpler.value is not None: # example: prime.idp
self.value = simpler.value
else:
self.simpler = simpler
assert self.value is None or type(self.value) in [Constructor,
Number]
assert self.value is not self # avoid infinite loops
# reset derived attributes
self.str = sys.intern(str(self))
return self
Expression._change = _change
def update_exprs(self, new_exprs):
""" change sub_exprs and simplify, while keeping relevant info. """
# default implementation, without simplification
return self._change(sub_exprs=list(new_exprs))
# Expression.update_exprs = update_exprs
for i in [Constructor, AppliedSymbol, UnappliedSymbol, Variable, Number]:
i.update_exprs = update_exprs
def simplify1(self):
return self.update_exprs(self.sub_exprs)
Expression.simplify1 = simplify1
# Class IfExpr ###############################################################
def update_exprs(self, new_exprs):
sub_exprs = list(new_exprs)
if_, then_, else_ = sub_exprs[0], sub_exprs[1], sub_exprs[2]
if if_.same_as(TRUE):
return self._change(simpler=then_, sub_exprs=sub_exprs)
elif if_.same_as(FALSE):
return self._change(simpler=else_, sub_exprs=sub_exprs)
else:
if then_.same_as(else_):
return self._change(simpler=then_, sub_exprs=sub_exprs)
elif then_.same_as(TRUE) and else_.same_as(FALSE):
return self._change(simpler=if_, sub_exprs=sub_exprs)
elif then_.same_as(FALSE) and else_.same_as(TRUE):
return self._change(simpler=AUnary.make('¬', if_),
sub_exprs=sub_exprs)
return self._change(sub_exprs=sub_exprs)
IfExpr.update_exprs = update_exprs
# Class AQuantification ######################################################
def update_exprs(self, new_exprs):
exprs = list(new_exprs)
simpler = exprs[0] if not self.q_vars else None
return self._change(simpler=simpler, sub_exprs=exprs)
AQuantification.update_exprs = update_exprs
# Class AImplication #######################################################
def update_exprs(self, new_exprs):
exprs0 = next(new_exprs)
value, simpler = None, None
if exprs0.same_as(FALSE): # (false => p) is true
# exprs[0] may be false because exprs[1] was false
exprs1 = self.sub_exprs[1] if self.sub_exprs[1].same_as(FALSE)\
else FALSE
value = TRUE
elif exprs0.same_as(TRUE): # (true => p) is p
exprs1 = next(new_exprs)
simpler = exprs1
else:
exprs1 = next(new_exprs)
if exprs1.same_as(TRUE): # (p => true) is true
exprs0 = exprs0 if self.sub_exprs[0].same_as(TRUE) else TRUE
value = TRUE
elif exprs1.same_as(FALSE): # (p => false) is ~p
simpler = AUnary.make('¬', exprs0)
return self._change(value=value, simpler=simpler,
sub_exprs=[exprs0, exprs1])
AImplication.update_exprs = update_exprs
# Class AEquivalence #######################################################
def update_exprs(self, new_exprs):
exprs = list(new_exprs)
if len(exprs) == 1:
return self._change(simpler=exprs[1], sub_exprs=exprs)
for e in exprs:
if e.same_as(TRUE): # they must all be true
return self._change(simpler=AConjunction.make('∧', exprs),
sub_exprs=exprs)
if e.same_as(FALSE): # they must all be false
return self._change(simpler=AConjunction.make('∧', [AUnary.make('¬', e) for e in exprs]),
sub_exprs=exprs)
return self._change(sub_exprs=exprs)
AEquivalence.update_exprs = update_exprs
# Class ADisjunction #######################################################
def update_exprs(self, new_exprs):
exprs, other = [], []
value, simpler = None, None
for i, expr in enumerate(new_exprs):
if expr.same_as(TRUE):
# simplify only if one other sub_exprs was unknown
if any(e.value is None and not i == j for j, e in enumerate(self.sub_exprs)):
return self._change(value=TRUE, sub_exprs=[expr])
value = TRUE
exprs.append(expr)
if not expr.same_as(FALSE):
other.append(expr)
if len(other) == 0: # all disjuncts are False
value = FALSE
if len(other) == 1:
simpler = other[0]
return self._change(value=value, simpler=simpler, sub_exprs=exprs)
ADisjunction.update_exprs = update_exprs
# Class AConjunction #######################################################
# same as ADisjunction, with TRUE and FALSE swapped
def update_exprs(self, new_exprs):
exprs, other = [], []
value, simpler = None, None
for i, expr in enumerate(new_exprs):
if expr.same_as(FALSE):
# simplify only if one other sub_exprs was unknown
if any(e.value is None and not i == j for j, e in enumerate(self.sub_exprs)):
return self._change(value=FALSE, sub_exprs=[expr])
value = FALSE
exprs.append(expr)
if not expr.same_as(TRUE):
other.append(expr)
if len(other) == 0: # all conjuncts are True
value = TRUE
if len(other) == 1:
simpler = other[0]
return self._change(value=value, simpler=simpler, sub_exprs=exprs)
AConjunction.update_exprs = update_exprs
# Class AComparison #######################################################
def update_exprs(self, new_exprs):
operands = list(new_exprs)
operands1 = [e.as_rigid() for e in operands]
if all(e is not None for e in operands1):
acc, acc1 = operands[0], operands1[0]
assert len(self.operator) == len(operands1[1:]), "Internal error"
for op, expr, expr1 in zip(self.operator, operands[1:], operands1[1:]):
if not (BinaryOperator.MAP[op]) (acc1.py_value, expr1.py_value):
return self._change(value=FALSE, sub_exprs=[acc, expr], ops=[op])
acc, acc1 = expr, expr1
return self._change(value=TRUE, sub_exprs=operands)
return self._change(sub_exprs=operands)
AComparison.update_exprs = update_exprs
def as_set_condition(self):
return ((None, None, None) if not self.is_assignment() else
(self.sub_exprs[0], True,
Enumeration(tuples=[Tuple(args=[self.sub_exprs[1]])])))
AComparison.as_set_condition = as_set_condition
#############################################################
def update_arith(self, family, operands):
operands = list(operands)
operands1 = [e.as_rigid() for e in operands]
if all(e is not None for e in operands1):
out = operands1[0].py_value
for e, op in zip(operands1[1:], self.operator):
function = BinaryOperator.MAP[op]
if op == '/' and self.type == INT: # integer division
out //= e.py_value
else:
out = function(out, e.py_value)
value = Number(number=str(out))
return self._change(value=value, sub_exprs=operands)
return self._change(sub_exprs=operands)
# Class ASumMinus #######################################################
def update_exprs(self, new_exprs):
return update_arith(self, '+', new_exprs)
ASumMinus.update_exprs = update_exprs
# Class AMultDiv #######################################################
def update_exprs(self, new_exprs):
operands = list(new_exprs)
if any(op == '%' for op in self.operator): # special case !
operands1 = [e.as_rigid() for e in operands]
if len(operands) == 2 \
and all(e is not None for e in operands1):
out = operands1[0].py_value % operands1[1].py_value
return self._change(value=Number(number=str(out)), sub_exprs=operands)
else:
return self._change(sub_exprs=operands)
return update_arith(self, '*', operands)
AMultDiv.update_exprs = update_exprs
# Class APower #######################################################
def update_exprs(self, new_exprs):
operands = list(new_exprs)
operands1 = [e.as_rigid() for e in operands]
if len(operands) == 2 \
and all(e is not None for e in operands1):
out = operands1[0].py_value ** operands1[1].py_value
return self._change(value=Number(number=str(out)), sub_exprs=operands)
else:
return self._change(sub_exprs=operands)
APower.update_exprs = update_exprs
# Class AUnary #######################################################
def update_exprs(self, new_exprs):
operand = list(new_exprs)[0]
if self.operator == '¬':
if operand.same_as(TRUE):
return self._change(value=FALSE, sub_exprs=[operand])
if operand.same_as(FALSE):
return self._change(value=TRUE, sub_exprs=[operand])
else: # '-'
a = operand.as_rigid()
if a is not None:
if type(a) == Number:
return self._change(value=Number(number=str(- a.translate())), sub_exprs=[operand])
return self._change(sub_exprs=[operand])
AUnary.update_exprs = update_exprs
def as_set_condition(self):
(x, y, z) = self.sub_exprs[0].as_set_condition()
return ((None, None, None) if x is None else
(x, not y, z))
AUnary.as_set_condition = as_set_condition
# Class AAggregate #######################################################
def update_exprs(self, new_exprs):
operands = list(new_exprs)
if self.quantifier_is_expanded:
operands1 = [e.as_rigid() for e in operands]
if all(e is not None for e in operands1):
out = sum(e.py_value for e in operands1)
out = Number(number=str(out))
return self._change(value=out, sub_exprs=operands)
return self._change(sub_exprs=operands)
AAggregate.update_exprs = update_exprs
# Class AppliedSymbol #######################################################
def as_set_condition(self):
# determine core after substitutions
core = AppliedSymbol.make(self.s, self.sub_exprs).copy()
return ((None, None, None) if not self.in_enumeration else
(core, 'not' not in self.is_enumeration, self.in_enumeration))
AppliedSymbol.as_set_condition = as_set_condition
# Class Brackets #######################################################
def update_exprs(self, new_exprs):
expr = list(new_exprs)[0]
return self._change(sub_exprs=[expr], value=expr.value)
Brackets.update_exprs = update_exprs
# set conditions #######################################################
[docs]def join_set_conditions(assignments: List[Assignment]) -> List[Assignment]:
"""In a list of assignments, merge assignments that are set-conditions on the same term.
An equality and a membership predicate (`in` operator) are both set-conditions.
Args:
assignments (List[Assignment]): the list of assignments to make more compact
Returns:
List[Assignment]: the compacted list of assignments
"""
#
for i, c in enumerate(assignments):
(x, belongs, y) = c.as_set_condition()
if x:
for j in range(i):
(x1, belongs1, y1) = assignments[j].as_set_condition()
if x1 and x.same_as(x1):
if belongs and belongs1:
new_tuples = (y.tuples & y1.tuples) # intersect
elif belongs and not belongs1:
new_tuples = (y.tuples ^ y1.tuples) # difference
elif not belongs and belongs1:
belongs = belongs1
new_tuples = (y1.tuples ^ y.tuples)
else:
new_tuples = y.tuples | y1.tuples # union
# sort again
new_tuples = list(new_tuples.values())
out = AppliedSymbol.make(
symbol=x.s, args=x.sub_exprs,
is_enumeration='in',
in_enumeration=Enumeration(tuples=new_tuples)
)
core = AppliedSymbol.make(out.s, out.sub_exprs).copy()
out.simpler = out.in_enumeration.contains([core], False)
out = Assignment(out,
TRUE if belongs else FALSE,
Status.UNKNOWN)
assignments[j] = out # keep the first one
assignments[i] = Assignment(TRUE, TRUE, Status.UNKNOWN)
return [c for c in assignments if c.sentence != TRUE]
Done = True