fix: a star in docs
This commit is contained in:
728
logic/logic.py
Normal file
728
logic/logic.py
Normal file
@ -0,0 +1,728 @@
|
||||
# logic.py
|
||||
# --------
|
||||
# Licensing Information: You are free to use or extend these projects for
|
||||
# educational purposes provided that (1) you do not distribute or publish
|
||||
# solutions, (2) you retain this notice, and (3) you provide clear
|
||||
# attribution to UC Berkeley, including a link to http://ai.berkeley.edu.
|
||||
#
|
||||
# Attribution Information: The Pacman AI projects were developed at UC Berkeley.
|
||||
# The core projects and autograders were primarily created by John DeNero
|
||||
# (denero@cs.berkeley.edu) and Dan Klein (klein@cs.berkeley.edu).
|
||||
# Student side autograding was added by Brad Miller, Nick Hay, and
|
||||
# Pieter Abbeel (pabbeel@cs.berkeley.edu).
|
||||
|
||||
|
||||
"""Representations and Inference for the CS 188 Logic Project
|
||||
|
||||
Code originally from https://code.google.com/p/aima-python/
|
||||
Modified heavily with additional convenience classes and functions as well
|
||||
as an interface to the pycosat (picoSAT wrapper) library.
|
||||
https://pypi.python.org/pypi/pycosat.
|
||||
Original package contained implementations of functions and data structures
|
||||
for Knowledge bases and First-Order Logic.
|
||||
"""
|
||||
|
||||
import itertools, re
|
||||
from typing import Tuple
|
||||
import agents
|
||||
from logic_utils import *
|
||||
import pycosat
|
||||
|
||||
#______________________________________________________________________________
|
||||
|
||||
class Expr:
|
||||
"""A symbolic mathematical expression. We use this class for logical
|
||||
expressions, and for terms within logical expressions. In general, an
|
||||
Expr has an op (operator) and a list of args. The op can be:
|
||||
Null-ary (no args) op:
|
||||
A number, representing the number itself. (e.g. Expr(42) => 42)
|
||||
A symbol, representing a variable or constant (e.g. Expr('F') => F)
|
||||
Unary (1 arg) op:
|
||||
'~', '-', representing NOT, negation (e.g. Expr('~', Expr('P')) => ~P)
|
||||
Binary (2 arg) op:
|
||||
'>>', '<<', representing forward and backward implication
|
||||
'+', '-', '*', '/', '**', representing arithmetic operators
|
||||
'<', '>', '>=', '<=', representing comparison operators
|
||||
'<=>', '^', representing logical equality and XOR
|
||||
N-ary (0 or more args) op:
|
||||
'&', '|', representing conjunction and disjunction
|
||||
A symbol, representing a function term or FOL proposition
|
||||
|
||||
Exprs can be constructed with operator overloading: if x and y are Exprs,
|
||||
then so are x + y and x & y, etc. Also, if F and x are Exprs, then so is
|
||||
F(x); it works by overloading the __call__ method of the Expr F. Note
|
||||
that in the Expr that is created by F(x), the op is the str 'F', not the
|
||||
Expr F. See http://www.python.org/doc/current/ref/specialnames.html
|
||||
to learn more about operator overloading in Python.
|
||||
|
||||
WARNING: x == y and x != y are NOT Exprs. The reason is that we want
|
||||
to write code that tests 'if x == y:' and if x == y were the same
|
||||
as Expr('==', x, y), then the result would always be true; not what a
|
||||
programmer would expect. But we still need to form Exprs representing
|
||||
equalities and disequalities. We concentrate on logical equality (or
|
||||
equivalence) and logical disequality (or XOR). You have 3 choices:
|
||||
(1) Expr('<=>', x, y) and Expr('^', x, y)
|
||||
Note that ^ is bitwise XOR in Python (and Java and C++)
|
||||
(2) expr('x <=> y') and expr('x =/= y').
|
||||
See the doc string for the function expr.
|
||||
(3) (x % y) and (x ^ y).
|
||||
It is very ugly to have (x % y) mean (x <=> y), but we need
|
||||
SOME operator to make (2) work, and this seems the best choice.
|
||||
|
||||
WARNING: if x is an Expr, then so is x + 1, because the int 1 gets
|
||||
coerced to an Expr by the constructor. But 1 + x is an error, because
|
||||
1 doesn't know how to add an Expr. (Adding an __radd__ method to Expr
|
||||
wouldn't help, because int.__add__ is still called first.) Therefore,
|
||||
you should use Expr(1) + x instead, or ONE + x, or expr('1 + x').
|
||||
"""
|
||||
|
||||
# Initialize a counter object
|
||||
counter = 0
|
||||
def __init__(self, op, *args):
|
||||
"Op is a string or number; args are Exprs (or are coerced to Exprs)."
|
||||
assert isinstance(op, str) or (isnumber(op) and not args)
|
||||
self.op = num_or_str(op)
|
||||
self.args = tuple(map(expr, args)) ## Coerce args to Exprs
|
||||
if not args and not is_prop_symbol(self.op):
|
||||
raise SyntaxError("Unacceptable symbol base name (%s). Name must start with an upper-case alphabetic character that and is not TRUE or FALSE. Furthermore, only the following are allowed: capital and lower case alphabetic, 0-9, _, \",\", [, and ]." % self.op)
|
||||
# Increment the counter when an object is created
|
||||
type(self).counter += 1
|
||||
|
||||
def __call__(self, *args):
|
||||
"""Self must be a symbol with no args, such as Expr('F'). Create a new
|
||||
Expr with 'F' as op and the args as arguments."""
|
||||
assert is_symbol(self.op) and not self.args
|
||||
return Expr(self.op, *args)
|
||||
|
||||
def __repr__(self):
|
||||
"Show something like 'P' or 'P(x, y)', or '~P' or '(P | Q | R)'"
|
||||
if not self.args: # Constant or proposition with arity 0
|
||||
return str(self.op)
|
||||
elif is_symbol(self.op): # Functional or propositional operator
|
||||
return '%s(%s)' % (self.op, ', '.join(map(repr, self.args)))
|
||||
elif len(self.args) == 1: # Prefix operator
|
||||
return self.op + repr(self.args[0])
|
||||
else: # Infix operator
|
||||
return '(%s)' % (' '+self.op+' ').join(map(repr, self.args))
|
||||
|
||||
def __eq__(self, other):
|
||||
"""x and y are equal iff their ops and args are equal."""
|
||||
return (other is self) or (isinstance(other, Expr)
|
||||
and self.op == other.op and self.args == other.args)
|
||||
|
||||
def __ne__(self, other):
|
||||
return not self.__eq__(other)
|
||||
|
||||
def __hash__(self):
|
||||
"Need a hash method so Exprs can live in dicts."
|
||||
return hash(self.op) ^ hash(tuple(self.args))
|
||||
|
||||
# See http://www.python.org/doc/current/lib/module-operator.html
|
||||
# Not implemented: not, abs, pos, concat, contains, *item, *slice
|
||||
def __lt__(self, other): return Expr('<', self, other)
|
||||
def __le__(self, other): return Expr('<=', self, other)
|
||||
def __ge__(self, other): return Expr('>=', self, other)
|
||||
def __gt__(self, other): return Expr('>', self, other)
|
||||
def __add__(self, other): return Expr('+', self, other)
|
||||
def __sub__(self, other): return Expr('-', self, other)
|
||||
def __and__(self, other): return Expr('&', self, other)
|
||||
def __div__(self, other): return Expr('/', self, other)
|
||||
def __truediv__(self, other):return Expr('/', self, other)
|
||||
def __invert__(self): return Expr('~', self)
|
||||
def __lshift__(self, other): return Expr('<<', self, other)
|
||||
def __rshift__(self, other): return Expr('>>', self, other)
|
||||
def __mul__(self, other): return Expr('*', self, other)
|
||||
def __neg__(self): return Expr('-', self)
|
||||
def __or__(self, other): return Expr('|', self, other)
|
||||
def __pow__(self, other): return Expr('**', self, other)
|
||||
def __xor__(self, other): return Expr('^', self, other)
|
||||
def __mod__(self, other): return Expr('<=>', self, other)
|
||||
|
||||
class PropSymbolExpr(Expr):
|
||||
"""An extension of Expr intended to represent a symbol. This SymbolExpr
|
||||
is a convenience for naming symbols, especially symbols whose names
|
||||
indicate an indexed value (e.g. Position[x,y] or Fluent[t]).
|
||||
Symbol name must begin with a capital letter. This class helps to add
|
||||
brackets with enumerated indices to the end of the name.
|
||||
"""
|
||||
# copied from logicPlan.py; preferably do this better
|
||||
pacman_str = 'P'
|
||||
food_str = 'FOOD'
|
||||
wall_str = 'WALL'
|
||||
DIRECTIONS = {'North', 'South', 'East', 'West'}
|
||||
# rules
|
||||
double_index = {pacman_str, food_str, wall_str}
|
||||
time_index = {pacman_str, food_str} | DIRECTIONS
|
||||
all_checked = double_index | time_index
|
||||
|
||||
def __init__(self, sym_str: str, *index: Tuple[int], time: int = None):
|
||||
"""Constructor taking a propositional logic symbol name and an optional set of index values,
|
||||
creating a symbol with the base name followed by brackets with the specific
|
||||
indices.
|
||||
sym_str: String representing base name for symbol. Must begin with a capital letter.
|
||||
Examples:
|
||||
>>> red = PropSymbolExpr("R")
|
||||
>>> print(red)
|
||||
R
|
||||
>>> turnLeft7 = PropSymbolExpr("Left",7)
|
||||
>>> print(turnLeft7)
|
||||
Left[7]
|
||||
>>> pos_2_3 = PropSymbolExpr("P",2,3)
|
||||
>>> print(pos_2_3)
|
||||
P[2,3]
|
||||
"""
|
||||
if not is_prop_symbol(sym_str):
|
||||
raise SyntaxError("Unacceptable symbol base name (%s). Name must start with an upper-case alphabetic character that and is not TRUE or FALSE. Furthermore, only the following are allowed: capital and lower case alphabetic, 0-9, _, \",\", [, and ]." % sym_str)
|
||||
if sym_str in self.all_checked:
|
||||
if sym_str in self.double_index:
|
||||
if len(index) != 2:
|
||||
raise SyntaxError("Unexpected " + sym_str + " Symbol. Was expecting 2 coordinates.")
|
||||
elif len(index) != 0:
|
||||
raise SyntaxError("Unexpected " + sym_str + " Symbol. Was expecting 0 coordinates.")
|
||||
if sym_str in self.time_index:
|
||||
if time == None:
|
||||
raise SyntaxError("Unexpected " + sym_str + " Symbol. Was expecting time stamp.")
|
||||
elif time != None:
|
||||
raise SyntaxError("Unexpected " + sym_str + " Symbol. Was expecting no time stamp.")
|
||||
self.sym_str = sym_str
|
||||
self.indicies = index
|
||||
self.time = time
|
||||
if len(index) > 0:
|
||||
if len(index) > 4:
|
||||
raise SyntaxError("Too many arguments to SymbolExpr constructor. SymbolExpr(symbol_str, [index1], [index2], [index3], [index4], time=[time]), or fewer indicies -- possibly 0.")
|
||||
if len(index) == 1:
|
||||
sym_str = '%s[%d]' % (sym_str, *index)
|
||||
elif len(index) == 2:
|
||||
sym_str = '%s[%d,%d]' % (sym_str, *index)
|
||||
elif len(index) == 3:
|
||||
sym_str = '%s[%d,%d,%d]' % (sym_str, *index)
|
||||
elif len(index) == 4:
|
||||
sym_str = '%s[%d,%d,%d,%d]' % (sym_str, *index)
|
||||
if time != None:
|
||||
sym_str = '%s_%d' % (sym_str, int(time))
|
||||
Expr.__init__(self, sym_str)
|
||||
|
||||
def getBaseName(self):
|
||||
return self.sym_str
|
||||
|
||||
def getIndex(self):
|
||||
return self.indicies
|
||||
|
||||
def getTime(self):
|
||||
return self.time
|
||||
|
||||
def parseExpr(symbol):
|
||||
"""A simple expression parser, takes in a PropSymbolExpr and returns
|
||||
its deconstruction in the form ( sym_str, indices, time ).
|
||||
Examples:
|
||||
>>> parseExpr("North[3]")
|
||||
('North', None, (3))
|
||||
>>> parseExpr("A")
|
||||
(A, None, ())
|
||||
>>> parseExpr("P[3,4]_1")
|
||||
('P', 1, (3, 4))
|
||||
"""
|
||||
tokens = re.split(r"_", str(symbol))
|
||||
time = None
|
||||
if len(tokens) == 2:
|
||||
symbol = tokens[0]
|
||||
time = int(tokens[1])
|
||||
|
||||
tokens = re.findall(r"[\w]+", str(symbol))
|
||||
if len(tokens) == 1:
|
||||
return (tokens[0], (), time)
|
||||
return (tokens[0], tuple(map(int,tokens[1:])), time)
|
||||
|
||||
def expr(s):
|
||||
"""Create an Expr representing a logic expression by parsing the input
|
||||
string. Symbols and numbers are automatically converted to Exprs.
|
||||
In addition you can use alternative spellings of these operators:
|
||||
'x ==> y' parses as (x >> y) # Implication
|
||||
'x <== y' parses as (x << y) # Reverse implication
|
||||
'x <=> y' parses as (x % y) # Logical equivalence
|
||||
'x =/= y' parses as (x ^ y) # Logical disequality (xor)
|
||||
But BE CAREFUL; precedence of implication is wrong. expr('P & Q ==> R & S')
|
||||
is ((P & (Q >> R)) & S); so you must use expr('(P & Q) ==> (R & S)').
|
||||
>>> expr('P <=> Q(1)')
|
||||
(P <=> Q(1))
|
||||
>>> expr('P & Q | ~R(x, F(x))')
|
||||
((P & Q) | ~R(x, F(x)))
|
||||
"""
|
||||
if isinstance(s, Expr): return s
|
||||
if isnumber(s): return Expr(s)
|
||||
## Replace the alternative spellings of operators with canonical spellings
|
||||
s = s.replace('==>', '>>').replace('<==', '<<')
|
||||
s = s.replace('<=>', '%').replace('=/=', '^')
|
||||
## Replace a symbol or number, such as 'P' with 'Expr("P")'
|
||||
s = re.sub(r'([a-zA-Z0-9_.]+)', r'Expr("\1")', s)
|
||||
## Now eval the string. (A security hole; do not use with an adversary.)
|
||||
return eval(s, {'Expr':Expr})
|
||||
|
||||
def is_symbol(s):
|
||||
"A string s is a symbol if it starts with an alphabetic char."
|
||||
return isinstance(s, str) and s[:1].isalpha()
|
||||
|
||||
def is_var_symbol(s):
|
||||
"A logic variable symbol is an initial-lowercase string."
|
||||
return is_symbol(s) and s[0].islower()
|
||||
|
||||
def is_prop_symbol(s):
|
||||
"""A proposition logic symbol is an initial-uppercase string other than
|
||||
TRUE or FALSE."""
|
||||
return is_symbol(s) and s[0].isupper() and s != 'TRUE' and s != 'FALSE' and re.match(r'[a-zA-Z0-9_\[\],]*$', s)
|
||||
|
||||
def variables(s):
|
||||
"""Return a set of the variables in expression s.
|
||||
>>> ppset(variables(F(x, A, y)))
|
||||
set([x, y])
|
||||
>>> ppset(variables(F(G(x), z)))
|
||||
set([x, z])
|
||||
>>> ppset(variables(expr('F(x, x) & G(x, y) & H(y, z) & R(A, z, z)')))
|
||||
set([x, y, z])
|
||||
"""
|
||||
result = set([])
|
||||
def walk(s):
|
||||
if is_variable(s):
|
||||
result.add(s)
|
||||
else:
|
||||
for arg in s.args:
|
||||
walk(arg)
|
||||
walk(s)
|
||||
return result
|
||||
|
||||
def is_definite_clause(s):
|
||||
"""returns True for exprs s of the form A & B & ... & C ==> D,
|
||||
where all literals are positive. In clause form, this is
|
||||
~A | ~B | ... | ~C | D, where exactly one clause is positive.
|
||||
>>> is_definite_clause(expr('Farmer(Mac)'))
|
||||
True
|
||||
>>> is_definite_clause(expr('~Farmer(Mac)'))
|
||||
False
|
||||
>>> is_definite_clause(expr('(Farmer(f) & Rabbit(r)) ==> Hates(f, r)'))
|
||||
True
|
||||
>>> is_definite_clause(expr('(Farmer(f) & ~Rabbit(r)) ==> Hates(f, r)'))
|
||||
False
|
||||
>>> is_definite_clause(expr('(Farmer(f) | Rabbit(r)) ==> Hates(f, r)'))
|
||||
False
|
||||
"""
|
||||
if is_symbol(s.op):
|
||||
return True
|
||||
elif s.op == '>>':
|
||||
antecedent, consequent = s.args
|
||||
return (is_symbol(consequent.op)
|
||||
and every(lambda arg: is_symbol(arg.op), conjuncts(antecedent)))
|
||||
else:
|
||||
return False
|
||||
|
||||
def parse_definite_clause(s):
|
||||
"Return the antecedents and the consequent of a definite clause."
|
||||
assert is_definite_clause(s)
|
||||
if is_symbol(s.op):
|
||||
return [], s
|
||||
else:
|
||||
antecedent, consequent = s.args
|
||||
return conjuncts(antecedent), consequent
|
||||
|
||||
## Useful constant Exprs used in examples and code:
|
||||
class SpecialExpr(Expr):
|
||||
"""Exists solely to allow the normal Expr constructor to assert valid symbol
|
||||
syntax while still having some way to create the constants
|
||||
TRUE, FALSE, ZERO, ONE, and, TWO
|
||||
"""
|
||||
def __init__(self, op, *args):
|
||||
"Op is a string or number; args are Exprs (or are coerced to Exprs)."
|
||||
assert isinstance(op, str) or (isnumber(op) and not args)
|
||||
self.op = num_or_str(op)
|
||||
self.args = tuple(map(expr, args)) ## Coerce args to Exprs
|
||||
|
||||
TRUE, FALSE = tuple(map(SpecialExpr, ['TRUE', 'FALSE']))
|
||||
ZERO, ONE, TWO = tuple(map(SpecialExpr, [0, 1, 2]))
|
||||
A, B, C, D, E, F, G, P, Q = tuple(map(Expr, 'ABCDEFGPQ'))
|
||||
|
||||
#______________________________________________________________________________
|
||||
def prop_symbols(x):
|
||||
"Return a list of all propositional symbols in x."
|
||||
if not isinstance(x, Expr):
|
||||
return []
|
||||
elif is_prop_symbol(x.op):
|
||||
return [x]
|
||||
else:
|
||||
return list(set(symbol for arg in x.args
|
||||
for symbol in prop_symbols(arg)))
|
||||
|
||||
def pl_true(exp, model={}):
|
||||
"""Return True if the propositional logic expression is true in the model,
|
||||
and False if it is false. If the model does not specify the value for
|
||||
every proposition, this may return None to indicate 'not obvious';
|
||||
this may happen even when the expression is tautological."""
|
||||
op, args = exp.op, exp.args
|
||||
if exp == TRUE:
|
||||
return True
|
||||
elif exp == FALSE:
|
||||
return False
|
||||
elif is_prop_symbol(op):
|
||||
return model.get(exp)
|
||||
elif op == '~':
|
||||
p = pl_true(args[0], model)
|
||||
if p is None: return None
|
||||
else: return not p
|
||||
elif op == '|':
|
||||
result = False
|
||||
for arg in args:
|
||||
p = pl_true(arg, model)
|
||||
if p is True: return True
|
||||
if p is None: result = None
|
||||
return result
|
||||
elif op == '&':
|
||||
result = True
|
||||
for arg in args:
|
||||
p = pl_true(arg, model)
|
||||
if p is False: return False
|
||||
if p is None: result = None
|
||||
return result
|
||||
p, q = args
|
||||
if op == '>>':
|
||||
return pl_true(~p | q, model)
|
||||
elif op == '<<':
|
||||
return pl_true(p | ~q, model)
|
||||
pt = pl_true(p, model)
|
||||
if pt is None: return None
|
||||
qt = pl_true(q, model)
|
||||
if qt is None: return None
|
||||
if op == '<=>':
|
||||
return pt == qt
|
||||
elif op == '^':
|
||||
return pt != qt
|
||||
else:
|
||||
raise ValueError("illegal operator in logic expression" + str(exp))
|
||||
|
||||
#______________________________________________________________________________
|
||||
|
||||
## Convert to Conjunctive Normal Form (CNF)
|
||||
|
||||
def to_cnf(s):
|
||||
"""Convert a propositional logical sentence s to conjunctive normal form.
|
||||
That is, to the form ((A | ~B | ...) & (B | C | ...) & ...) [p. 253]
|
||||
>>> to_cnf("~(B|C)")
|
||||
(~B & ~C)
|
||||
>>> to_cnf("B <=> (P1|P2)")
|
||||
((~P1 | B) & (~P2 | B) & (P1 | P2 | ~B))
|
||||
>>> to_cnf("a | (b & c) | d")
|
||||
((b | a | d) & (c | a | d))
|
||||
>>> to_cnf("A & (B | (D & E))")
|
||||
(A & (D | B) & (E | B))
|
||||
>>> to_cnf("A | (B | (C | (D & E)))")
|
||||
((D | A | B | C) & (E | A | B | C))
|
||||
"""
|
||||
if isinstance(s, str): s = expr(s)
|
||||
s = eliminate_implications(s) # Steps 1, 2 from p. 253
|
||||
s = move_not_inwards(s) # Step 3
|
||||
s = distribute_and_over_or(s) # Step 4
|
||||
return s
|
||||
|
||||
def eliminate_implications(s):
|
||||
"""Change >>, <<, and <=> into &, |, and ~. That is, return an Expr
|
||||
that is equivalent to s, but has only &, |, and ~ as logical operators.
|
||||
>>> eliminate_implications(A >> (~B << C))
|
||||
((~B | ~C) | ~A)
|
||||
>>> eliminate_implications(A ^ B)
|
||||
((A & ~B) | (~A & B))
|
||||
"""
|
||||
if not s.args or is_symbol(s.op): return s ## (Atoms are unchanged.)
|
||||
args = tuple(map(eliminate_implications, s.args))
|
||||
a, b = args[0], args[-1]
|
||||
if s.op == '>>':
|
||||
return (b | ~a)
|
||||
elif s.op == '<<':
|
||||
return (a | ~b)
|
||||
elif s.op == '<=>':
|
||||
return (a | ~b) & (b | ~a)
|
||||
elif s.op == '^':
|
||||
assert len(args) == 2 ## TODO: relax this restriction
|
||||
return (a & ~b) | (~a & b)
|
||||
else:
|
||||
assert s.op in ('&', '|', '~')
|
||||
return Expr(s.op, *args)
|
||||
|
||||
def move_not_inwards(s):
|
||||
"""Rewrite sentence s by moving negation sign inward.
|
||||
>>> move_not_inwards(~(A | B))
|
||||
(~A & ~B)
|
||||
>>> move_not_inwards(~(A & B))
|
||||
(~A | ~B)
|
||||
>>> move_not_inwards(~(~(A | ~B) | ~~C))
|
||||
((A | ~B) & ~C)
|
||||
"""
|
||||
if s.op == '~':
|
||||
NOT = lambda b: move_not_inwards(~b)
|
||||
a = s.args[0]
|
||||
if a.op == '~': return move_not_inwards(a.args[0]) # ~~A ==> A
|
||||
if a.op =='&': return associate('|', tuple(map(NOT, a.args)))
|
||||
if a.op =='|': return associate('&', tuple(map(NOT, a.args)))
|
||||
return s
|
||||
elif is_symbol(s.op) or not s.args:
|
||||
return s
|
||||
else:
|
||||
return Expr(s.op, *map(move_not_inwards, s.args))
|
||||
|
||||
def distribute_and_over_or(s):
|
||||
"""Given a sentence s consisting of conjunctions and disjunctions
|
||||
of literals, return an equivalent sentence in CNF.
|
||||
>>> distribute_and_over_or((A & B) | C)
|
||||
((A | C) & (B | C))
|
||||
"""
|
||||
if s.op == '|':
|
||||
s = associate('|', s.args)
|
||||
if s.op != '|':
|
||||
return distribute_and_over_or(s)
|
||||
if len(s.args) == 0:
|
||||
return FALSE
|
||||
if len(s.args) == 1:
|
||||
return distribute_and_over_or(s.args[0])
|
||||
conj = find_if((lambda d: d.op == '&'), s.args)
|
||||
if not conj:
|
||||
return s
|
||||
others = [a for a in s.args if a is not conj]
|
||||
rest = associate('|', others)
|
||||
return associate('&', [distribute_and_over_or(c|rest)
|
||||
for c in conj.args])
|
||||
elif s.op == '&':
|
||||
return associate('&', map(distribute_and_over_or, s.args))
|
||||
else:
|
||||
return s
|
||||
|
||||
def associate(op, args):
|
||||
"""Given an associative op, return an expression with the same
|
||||
meaning as Expr(op, *args), but flattened -- that is, with nested
|
||||
instances of the same op promoted to the top level.
|
||||
>>> associate('&', [(A&B),(B|C),(B&C)])
|
||||
(A & B & (B | C) & B & C)
|
||||
>>> associate('|', [A|(B|(C|(A&B)))])
|
||||
(A | B | C | (A & B))
|
||||
"""
|
||||
args = dissociate(op, args)
|
||||
if len(args) == 0:
|
||||
return _op_identity[op]
|
||||
elif len(args) == 1:
|
||||
return args[0]
|
||||
else:
|
||||
return Expr(op, *args)
|
||||
|
||||
_op_identity = {'&':TRUE, '|':FALSE, '+':ZERO, '*':ONE}
|
||||
|
||||
def conjoin(exprs, *args):
|
||||
"""Given a list of expressions, returns their conjunction. Can be called either
|
||||
with one argument that is a list of expressions, or with several arguments that
|
||||
are each an expression.
|
||||
If exprs is a singular expression or contains only one expression, return that
|
||||
expression directly.
|
||||
If exprs is an empty list, throw an error.
|
||||
>>> conjoin([(A&B),(B|C),(B&C)])
|
||||
(A & B & (B | C) & B & C)
|
||||
>>> conjoin((A&B), (B|C), (B&C))
|
||||
(A & B & (B | C) & B & C)
|
||||
>>> conjoin([A])
|
||||
A
|
||||
"""
|
||||
if args:
|
||||
return conjoin([exprs] + list(args))
|
||||
if (type(exprs) != list):
|
||||
return exprs
|
||||
|
||||
assert len(exprs) > 0, "List to conjoin cannot be empty."
|
||||
|
||||
# It is a list. Enforce everything in the list is an Expr
|
||||
for expr in exprs:
|
||||
assert isinstance(expr, Expr), "An item in list to conjoin is not an Expr."
|
||||
|
||||
if (len(exprs) == 1):
|
||||
return exprs[0]
|
||||
return associate('&', exprs)
|
||||
|
||||
def disjoin(exprs, *args):
|
||||
"""Given a list of expressions, returns their disjunction. Can be called either
|
||||
with one argument that is a list of expressions, or with several arguments that
|
||||
are each an expression.
|
||||
If exprs is a singular expression or contains only one expression, return that
|
||||
expression directly.
|
||||
If exprs is an empty list, throw an error.
|
||||
>>> disjoin([C, (A&B), (D&E)])
|
||||
(C | (A & B) | (D & E))
|
||||
>>> disjoin(C, (A&B), (D&E))
|
||||
(C | (A & B) | (D & E))
|
||||
>>> disjoin([C])
|
||||
D
|
||||
"""
|
||||
if args:
|
||||
return disjoin([exprs] + list(args))
|
||||
if (type(exprs) != list):
|
||||
return exprs
|
||||
|
||||
assert len(exprs) > 0, "List to disjoin cannot be empty."
|
||||
|
||||
# It is a list. Enforce everything in the list is an Expr
|
||||
for expr in exprs:
|
||||
assert isinstance(expr, Expr), "An item in list to disjoin is not an Expr."
|
||||
|
||||
if (len(exprs) == 1):
|
||||
return exprs[0]
|
||||
return associate('|', exprs)
|
||||
|
||||
def dissociate(op, args):
|
||||
"""Given an associative op, return a flattened list result such
|
||||
that Expr(op, *result) means the same as Expr(op, *args)."""
|
||||
result = []
|
||||
def collect(subargs):
|
||||
for arg in subargs:
|
||||
if arg.op == op: collect(arg.args)
|
||||
else: result.append(arg)
|
||||
collect(args)
|
||||
return result
|
||||
|
||||
def conjuncts(s):
|
||||
"""Return a list of the conjuncts in the sentence s.
|
||||
>>> conjuncts(A & B)
|
||||
[A, B]
|
||||
>>> conjuncts(A | B)
|
||||
[(A | B)]
|
||||
"""
|
||||
return dissociate('&', [s])
|
||||
|
||||
def disjuncts(s):
|
||||
"""Return a list of the disjuncts in the sentence s.
|
||||
>>> disjuncts(A | B)
|
||||
[A, B]
|
||||
>>> disjuncts(A & B)
|
||||
[(A & B)]
|
||||
"""
|
||||
return dissociate('|', [s])
|
||||
|
||||
def is_valid_cnf(exp):
|
||||
if not isinstance(exp, Expr):
|
||||
print("Input is not an expression.")
|
||||
return False
|
||||
|
||||
clauses = conjuncts(exp);
|
||||
|
||||
for c in clauses:
|
||||
literals = disjuncts(c)
|
||||
|
||||
for lit in literals:
|
||||
if len(lit.args) == 0:
|
||||
symbol = lit;
|
||||
elif len(lit.args) == 1:
|
||||
symbol = lit.args[0]
|
||||
|
||||
if len(symbol.args) != 0:
|
||||
print("Found a NOT outside of %s" % symbol)
|
||||
return False
|
||||
|
||||
else:
|
||||
print("Found %s where only a literal should be." % lit)
|
||||
return False
|
||||
|
||||
symbol_str = str(symbol)
|
||||
|
||||
if not is_symbol(symbol_str):
|
||||
print("%s is not a valid symbol." % symbol_str)
|
||||
return False
|
||||
elif not symbol_str[0].isupper():
|
||||
print("The symbol %s must begin with an upper-case letter." % symbol_str)
|
||||
return False
|
||||
elif symbol_str == 'TRUE':
|
||||
print("TRUE is not a valid symbol.")
|
||||
return False
|
||||
elif symbol_str == 'FALSE':
|
||||
print("FALSE is not a valid symbol.")
|
||||
return False
|
||||
|
||||
return True
|
||||
|
||||
#______________________________________________________________________________
|
||||
# pycosat python wrapper around PicoSAT software.
|
||||
# https://pypi.python.org/pypi/pycosat
|
||||
|
||||
def pycoSAT(expr):
|
||||
"""Check satisfiability of an expression.
|
||||
Given a CNF expression, returns a model that causes the input expression
|
||||
to be true. Returns false if it cannot find a satisfible model.
|
||||
A model is simply a dictionary with Expr symbols as keys with corresponding values
|
||||
that are booleans: True if that symbol is true in the model and False if it is
|
||||
false in the model.
|
||||
Calls the pycosat solver: https://pypi.python.org/pypi/pycosat
|
||||
>>> ppsubst(pycoSAT(A&~B))
|
||||
{A: True, B: False}
|
||||
>>> pycoSAT(P&~P)
|
||||
False
|
||||
"""
|
||||
|
||||
clauses = conjuncts(expr)
|
||||
|
||||
# Load symbol dictionary
|
||||
symbol_dict = mapSymbolAndIndices(clauses)
|
||||
# Convert Expr to integers
|
||||
clauses_int = exprClausesToIndexClauses(clauses, symbol_dict)
|
||||
|
||||
model_int = pycosat.solve(clauses_int)
|
||||
|
||||
if model_int == 'UNSAT' or model_int == 'UNKNOWN':
|
||||
return False
|
||||
|
||||
model = indexModelToExprModel(model_int, symbol_dict)
|
||||
|
||||
return model
|
||||
|
||||
def mapSymbolAndIndices(clauses):
|
||||
"""
|
||||
Create a dictionary that maps each clause to an integer index.
|
||||
Uses a bidirectional dictionary {key1:value1, value1:key1, ...} for quick
|
||||
access from symbol to index and index to symbol.
|
||||
"""
|
||||
symbol_dict = {}
|
||||
idx = 1
|
||||
for clause in clauses:
|
||||
symbols = prop_symbols(clause)
|
||||
for symbol in symbols:
|
||||
if symbol not in symbol_dict:
|
||||
symbol_dict[symbol] = idx
|
||||
symbol_dict[idx] = symbol
|
||||
idx +=1
|
||||
|
||||
return symbol_dict
|
||||
|
||||
def exprClausesToIndexClauses(clauses, symbol_dict):
|
||||
"""
|
||||
Convert each Expr in a list of clauses (CNF) into its corresponding index in
|
||||
the symbol_dict (see mapSymbolAndIndices)
|
||||
"""
|
||||
clauses_int = []
|
||||
for c in clauses:
|
||||
c_disj = disjuncts(c)
|
||||
|
||||
c_int = []
|
||||
for lit in c_disj:
|
||||
# If literal is symbol, convert to index and add it.
|
||||
# Otherwise it is ~symbol, in which case, we extract the symbol,
|
||||
# convert it to index, and add the negative of the index
|
||||
if len(lit.args) == 0:
|
||||
c_int += [symbol_dict[lit]]
|
||||
else:
|
||||
c_int += [-symbol_dict[lit.args[0]]]
|
||||
clauses_int += [c_int]
|
||||
|
||||
return clauses_int
|
||||
|
||||
def indexModelToExprModel(model_int, symbol_dict):
|
||||
"""
|
||||
Convert a model with indices into a model with the corresponding Expr in
|
||||
the symbol_dict (see mapSymbolAndIndices)
|
||||
>>>
|
||||
"""
|
||||
model = {}
|
||||
for lit_int in model_int:
|
||||
if lit_int > 0:
|
||||
model[symbol_dict[lit_int]] = True
|
||||
else:
|
||||
model[symbol_dict[-lit_int]] = False
|
||||
|
||||
return model
|
Reference in New Issue
Block a user