729 lines
28 KiB
Python
729 lines
28 KiB
Python
# 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
|