diff --git a/examples/prop_satisfiables.txt b/examples/prop_satisfiables.txt
new file mode 100644
index 0000000..1b89fd2
--- /dev/null
+++ b/examples/prop_satisfiables.txt
@@ -0,0 +1,4 @@
+X
+Y
+X&Y
+X|Y
diff --git a/examples/prop_tautologies.txt b/examples/prop_tautologies.txt
new file mode 100644
index 0000000..2c67d66
--- /dev/null
+++ b/examples/prop_tautologies.txt
@@ -0,0 +1,46 @@
+%% Tautologies from:
+%% Melvin Fitting. "First-Order Logic and Automated Theorem Proving".
+
+%% from Tableaux exercises
+((P -> Q) & (Q -> R)) -> -(-R & P)
+(-P -> Q) -> ((P -> Q) -> Q)
+((P -> Q) -> P) -> P
+-(-(P & P) & P)
+--(-(P | Q) | (P | Q))
+-(-P | -Q) <- --(P & Q)
+((((A -> B) -> (-C -> -D)) -> C) -> E) -> ((E -> A) -> (D -> A))
+-(-(P & -(Q & R)) & -(-(P & -(R & P)) & -(-(S & Q) & -(-(P & S) & -(P & S)))))
+-(-(P & -(Q & R)) & -(-(-(S & R) & -(-(P & S) & -(P & S))) & -(P & -(P & Q))))
+
+%% from Resolution example
+((P & Q) | (R -> S)) -> ((P | (R -> S)) & (Q | (R -> S)))
+
+%% Hilbert System Axioms
+X -> (Y -> X)
+(X -> (Y -> Z)) -> ((X -> Y) -> (X -> Z))
+F -> X
+X -> T
+--X -> X
+X -> (-X -> Y)
+% axiom scheme 7 application
+(A & B) -> A
+% axiom scheme 8 application
+(A & B) -> B
+% axiom scheme 9 application
+(A -> X) -> ((B -> X) -> ((A | B) -> X))
+
+%% from Natural Deduction exercises
+% X -> (Y -> X)
+(X -> (Y -> Z)) -> ((X -> Y) -> (X -> Z))
+(-Y -> -X) -> ((-Y -> X) -> Y)
+% ((X -> Y) -> X) -> X
+(X & (Y | Z)) -> ((X & Y) | (X & Z))
+(X -> Y) -> (-(Y | Z) -> -(X | Z))
+-(-(P & P) & P)
+--(-(P | Q) | (P | Q))
+-(-P | -Q) <- --(P & Q)
+
+%% from Davis-Putnam exercises
+((P -> Q) -> (P -> R)) -> (P -> (Q -> R))
+(P & Q) <-> -(-P | -Q)
+(P -> Q) | (Q -> R)
diff --git a/pylogic/gui/gui.py b/pylogic/gui/gui.py
index b6107bf..0eefff2 100755
--- a/pylogic/gui/gui.py
+++ b/pylogic/gui/gui.py
@@ -1,6 +1,7 @@
import sys
import string
import os.path # for file checks
+import time
from PyQt4.QtCore import Qt, SIGNAL
from PyQt4.QtGui import *
@@ -30,6 +31,18 @@ def appendOutput(self, string=""):
outputBox.write(string)
+ def execute(self, func):
+ check_box = self.ui.checkBoxExecutionTime.isChecked()
+ start = 0
+ if check_box:
+ start = time.time()
+ output = func()
+ if check_box:
+ execution_time = time.time() - start
+ self.appendOutput("Execution time: " + execution_time.__str__())
+ return output
+
+
def showAboutBox(self):
aboutBox = MyAboutBox()
aboutBox.setModal(False)
@@ -67,20 +80,23 @@ def propositionalCheck(self):
def propositionalNNF(self):
"""Transform the current formula in input in NNF"""
formula = propositional_parser.parse(self.getInputString())
- output = formula.nnf()
+ func = lambda: formula.nnf()
+ output = self.execute(func)
self.appendOutput(output.__str__())
def propositionalCNF(self):
"""Transform the current formula in input in CNF"""
formula = propositional_parser.parse(self.getInputString())
- output = formula.cnf()
+ func = lambda: formula.cnf()
+ output = self.execute(func)
self.appendOutput(output.__str__())
def propositionalResolution(self):
"""Test if the current formula is a tautology, using the resolution
method"""
formula = propositional_parser.parse(self.getInputString())
- output = propositional_resolution.is_tautology(formula)
+ func = lambda: propositional_resolution.is_tautology(formula)
+ output = self.execute(func)
self.appendOutput("%s: %s" % (str(formula), output.__str__()) )
diff --git a/pylogic/gui/mainwindow.ui b/pylogic/gui/mainwindow.ui
index 5862ffb..4bd7123 100644
--- a/pylogic/gui/mainwindow.ui
+++ b/pylogic/gui/mainwindow.ui
@@ -158,6 +158,19 @@
+ -
+
+
+ true
+
+
+ execution time
+
+
+ true
+
+
+
diff --git a/pylogic/propositional/propositional_logic.py b/pylogic/propositional/propositional_logic.py
index d51a1ed..cf5d224 100644
--- a/pylogic/propositional/propositional_logic.py
+++ b/pylogic/propositional/propositional_logic.py
@@ -36,6 +36,7 @@ def __init__(self, *args):
connective = None
subformula1 = letter
subformula2 = None
+ depth = 0
elif len(args) == 2:
if args[0] != "not" and args[0] != logic.CONN["not"]:
raise Exception("Wrong connective: " + args[0])
@@ -44,6 +45,7 @@ def __init__(self, *args):
connective = "not"
subformula1 = args[1]
subformula2 = None
+ depth = subformula1.depth + 1
else:
if args[0] in list(set(logic.CONN.values()) - set("!")):
connective = [ item[0]
@@ -61,10 +63,13 @@ def __init__(self, *args):
raise Exception("Wrong formula: " + args[2])
subformula1 = args[1]
subformula2 = args[2]
+ depth = max(subformula1.depth, subformula2.depth)
+ depth = depth + 1
self.connective = connective
self.subformula1 = subformula1
self.subformula2 = subformula2
+ self.depth = depth
def __str__(self):
@@ -83,6 +88,8 @@ def __eq__(self, other):
return False
if self.connective == None and other.connective == None:
return self.subformula1 == other.subformula1
+ if self.depth != other.depth:
+ return False
else:
return self.connective == other.connective \
and self.subformula1 == other.subformula1 \
@@ -277,6 +284,42 @@ def __ne__(self, other):
return not self.__eq__(other)
+ def __len__(self):
+ return len(self.list)
+
+
+ def equivalent(self, other):
+ """Check if two generalizations have the same elements independently of
+ their order"""
+ if self.connective != other.connective:
+ return False
+ if len(self.list) != len(other.list):
+ return False
+ other_list = list(other.list)
+ try:
+ for formula in self.list:
+ other_list.remove(formula)
+ except ValueError:
+ return False
+ return not other_list
+
+
+ def subsume(self, other):
+ """Check if the current generalization subsumes the 'other'
+ generalization"""
+ if self.connective != other.connective:
+ return False
+ if len(self.list) > len(other.list):
+ return False
+ other_list = list(other.list)
+ try:
+ for formula in self.list:
+ other_list.remove(formula)
+ except ValueError:
+ return False
+ return True
+
+
def has_non_literal(self):
"""Check if in the list of formulas there are non-literal formulas."""
if len(self.list) == 0:
diff --git a/pylogic/propositional/resolution.py b/pylogic/propositional/resolution.py
index b35694f..3038b61 100644
--- a/pylogic/propositional/resolution.py
+++ b/pylogic/propositional/resolution.py
@@ -3,44 +3,166 @@
from pylogic import logic
+def preliminary_steps(clauses):
+ manage_tops(clauses)
+ manage_complementary(clauses)
+ manage_bottoms(clauses)
+ manage_copies(clauses)
+ manage_duplicated_clauses(clauses)
+ manage_subsumption_rule(clauses)
+
+def manage_tops(clauses):
+ """Remove the clauses containg the top."""
+ removable = []
+ for c in range(len(clauses)):
+ clause = clauses[c]
+ for formula in clause.list:
+ if formula == Formula("T"):
+ removable.append(c)
+ break
+ for i in reversed(removable):
+ clauses.pop(i)
+
+def manage_complementary(clauses):
+ """Remove the clauses containing two complementary formulas."""
+ removable = []
+ for c in range(len(clauses)):
+ clause = clauses[c]
+ found = False
+ f = 0
+ while not found and f < len(clause):
+ formula1 = clause.list[f]
+ for f2 in range(f+1, len(clause)):
+ formula2 = clause.list[f2]
+ if formula1 == formula2.complement():
+ removable.append(c)
+ found = True
+ break
+ f = f + 1
+ for i in reversed(removable):
+ clauses.pop(i)
+
+def manage_bottoms(clauses):
+ """Remove the bottoms from every clause."""
+ for clause in clauses:
+ clause.remove_every(Formula("F"))
+
+def manage_copies(clauses):
+ """Remove from every clause repetions of inner formulas."""
+ for clause in clauses:
+ f = 0
+ while f < len(clause)-1:
+ formula = clause.list[f]
+ f2 = f+1
+ while f2 < len(clause):
+ formula2 = clause.list[f2]
+ if formula == formula2:
+ clause.list.pop(f2)
+ else:
+ f2 = f2+1
+ f = f+1
+
+def manage_duplicated_clauses(clauses):
+ """Remove duplicated clauses, independently of the order of the formulas."""
+ removable = []
+ for i in range(len(clauses)):
+ if i not in removable:
+ clause = clauses[i]
+ for j in range(i + 1, len(clauses)):
+ if j not in removable:
+ clause2 = clauses[j]
+ if clause.equivalent(clause2):
+ removable.append(j)
+ for i in reversed(removable):
+ clauses.pop(i)
+
+def manage_subsumption_rule(clauses):
+ """Remove the clauses subsumed by another clause"""
+ i = 0
+ while i < len(clauses) - 1:
+ cl1 = clauses[i]
+ j = i + 1
+ deleted = False
+ while j < len(clauses) and not deleted:
+ cl2 = clauses[j]
+ if cl1.subsume(cl2):
+ del clauses[j]
+ elif cl2.subsume(cl1):
+ del clauses[i]
+ deleted = True
+ else:
+ j = j + 1
+ if not deleted:
+ i = i + 1
+
+
def is_closed(expansion):
"""Given a list of clauses, return True if it contains an empty clause,
False otherwise"""
- for el in expansion:
- clause = el[1]
- if len(clause.list) == 0:
+ for clause in expansion:
+ if len(clause) == 0:
return True
# else ignore it
return False
-def expand(expansion):
- """Apply the resolution rule to the given expansion.
- Returns True if the resolution rule is applied, False otherwise."""
- # for each formula
- for g in range(len(expansion)):
- if expansion[g][0]:
- continue
- gen = expansion[g][1]
- for f in range(len(gen.list)):
- formula = gen.list[f]
- # check if exists a complement of formula
- # in the rest of the expansion
- for ng in range(g+1, len(expansion)):
- temp_gen = expansion[ng][1]
- for nf in range(len(temp_gen.list)):
- temp_formula = temp_gen.list[nf]
- if formula == temp_formula.complement():
- gen = copy.deepcopy(gen)
- gen2 = copy.deepcopy(temp_gen)
- gen.remove_every(formula)
- gen2.remove_every(temp_formula)
- gen.list.extend(gen2.list)
- expansion.append([False, gen])
- expansion[g][0] = True
- return True
- # else ignore it
- return False
+def is_new(expansion, clause):
+ """Check if the given clause is already present in the given expansion."""
+ found = False
+ i = 0
+ while not found and i < len(expansion):
+ cl = expansion[i]
+ i = i + 1
+ if cl.equivalent(clause):
+ return False
+ return True
+
+
+def resolution_rule(clause1, clause2, formula):
+ """Apply the resolution rule to the given clauses and formula."""
+ new_clause = Generalization("or", [])
+ for f1 in clause1.list:
+ if f1 != formula:
+ new_clause.list.append(f1)
+
+ formula_compl = formula.complement()
+ for f2 in clause2.list:
+ if f2 != formula_compl:
+ new_clause.list.append(f2)
+ return new_clause
+
+
+def apply_resolution_rule(clause1, clause2):
+ """Apply the resolution rule to the given clauses.
+
+ After that apply the preliminary steps on the resulting clause.
+ It assumes that in clause1 and clause2 are already applied
+ the preliminary steps, that is in them there aren't tops or bottoms;
+ so here are not applied manage_tops or manage_bottoms.
+
+ Moreover the resolution rule is applied only on the first formula
+ of which is found the complementary in the other clause.
+ This because if the resolution rule could be applied, for instance,
+ two times it means that in them there are two distinct couples
+ of complementary formulas, this means that after every application
+ of the resolution rule in the resulting clauses there will be
+ a couple of complementary fomulas and so with the preliminary steps
+ the clauses will be removed."""
+ for f in range(len(clause1)):
+ formula = clause1.list[f]
+ # check if exists a complement of formula
+ for f2 in range(len(clause2)):
+ formula2 = clause2.list[f2]
+ if formula == formula2.complement():
+ new_clause = resolution_rule(clause1, clause2, formula)
+ clauses = [new_clause]
+ manage_complementary(clauses)
+ manage_copies(clauses)
+ if clauses == []:
+ return None
+ else:
+ return new_clause
+ return None
def is_tautology(formula):
@@ -52,13 +174,65 @@ def is_tautology(formula):
negation = formula.negate()
cnf = negation.cnf()
print(cnf)
- expansion = [[False, disj] for disj in cnf.list]
- enough = False
- while not is_closed(expansion) and not enough:
- applied = expand(expansion)
- enough = not applied
- disjs = ""
- for g in expansion:
- disjs = disjs + " " + g[1].__str__()
- print(disjs)
- return is_closed(expansion)
+ expansion = cnf.list
+ preliminary_steps(expansion)
+ picker = ClausePicker(expansion)
+ if is_closed(expansion):
+ return True
+ while not picker.is_empty():
+ cl = picker.pick()
+ new_clause = apply_resolution_rule(expansion[cl[0]], expansion[cl[1]])
+ if new_clause is not None:
+ if len(new_clause) == 0:
+ return True
+ if is_new(expansion, new_clause):
+ expansion.append(new_clause)
+ picker.add_clause(new_clause)
+ print(" ".join([cl.__str__() for cl in expansion]))
+ return False
+
+
+
+class ClausePicker():
+ def __init__(self, expansion):
+ self.sizes = [len(clause) for clause in expansion]
+ # dict containing the couples of clauses
+ # (precisely their indexes in the original expansion list)
+ # it is indexed with the sum of the two clauses' sizes
+ self.buckets = dict()
+ for i in range(len(self.sizes)-1):
+ size_i = self.sizes[i]
+ for j in range(i+1, len(self.sizes)):
+ size = size_i + self.sizes[j]
+ if size in self.buckets:
+ self.buckets[size].append((i,j))
+ else:
+ self.buckets[size] = [(i,j)]
+
+
+ def pick(self):
+ if self.is_empty():
+ raise Exception("No more choices")
+ bucket = min(self.buckets.keys())
+ couple = self.buckets[bucket].pop(0)
+ if len(self.buckets[bucket]) == 0:
+ del self.buckets[bucket]
+ return couple
+
+
+ def add_clause(self, clause):
+ i = len(self.sizes) # index in the expansion list
+ # insert in self.sizes
+ size_i = len(clause)
+ self.sizes.append(size_i)
+ # insert in self.buckets
+ for j in range(len(self.sizes)-1):
+ size = size_i + self.sizes[j]
+ if size in self.buckets:
+ self.buckets[size].append((i,j))
+ else:
+ self.buckets[size] = [(i,j)]
+
+
+ def is_empty(self):
+ return len(self.buckets) == 0
diff --git a/pylogic/tests/test_propositional_propositional_logic.py b/pylogic/tests/test_propositional_propositional_logic.py
index 4e52cd3..24ac505 100644
--- a/pylogic/tests/test_propositional_propositional_logic.py
+++ b/pylogic/tests/test_propositional_propositional_logic.py
@@ -277,6 +277,10 @@ def test_cnf_particular(self):
class TestGeneralization(unittest.TestCase):
def setUp(self):
+ self.a1 = Formula("X")
+ self.a2 = Formula("Y")
+ self.a3 = Formula("Z")
+ self.a4 = Formula("W")
self.f1 = Formula("&", Formula("X"), Formula("Y"))
self.f2 = Formula("|", Formula("X"), Formula("Y"))
@@ -336,6 +340,34 @@ def test_eq_ne(self):
self.assertNotEqual(g3, g1)
+ def test_len(self):
+ g1 = Generalization("and", [self.f1, self.f2])
+ g2 = Generalization("and", [self.f1, self.f2, self.f1, self.f2])
+ g3 = Generalization("and", [])
+ self.assertEqual(2, len(g1))
+ self.assertEqual(4, len(g2))
+ self.assertEqual(0, len(g3))
+
+
+ def test_equivalent(self):
+ g1 = Generalization("and", [self.f1, self.f2])
+ g2 = Generalization("and", [self.f2, self.f1])
+ g3 = Generalization("and", [self.f1])
+ g4 = Generalization("or", [self.f2, self.f1])
+ self.assertTrue(g1.equivalent(g2))
+ self.assertFalse(g1.equivalent(g3))
+ self.assertFalse(g1.equivalent(g4))
+
+
+ def test_subsume(self):
+ g1 = Generalization("or", [self.a1, self.a2])
+ g2 = Generalization("or", [self.a2, self.a1, self.a3])
+ g3 = Generalization("or", [self.a2, self.a1, self.a3, self.a4])
+ self.assertTrue(g1.subsume(g2))
+ self.assertTrue(g1.subsume(g3))
+ self.assertFalse(g3.subsume(g1))
+
+
def test_has_non_literal(self):
g1 = Generalization("and", [self.f1, Formula("Z"), self.f2])
g2 = Generalization("or", [Formula("Z"), Formula("!", Formula("Y"))])
diff --git a/pylogic/tests/test_propositional_resolution.py b/pylogic/tests/test_propositional_resolution.py
index 61a2631..18cb81f 100644
--- a/pylogic/tests/test_propositional_resolution.py
+++ b/pylogic/tests/test_propositional_resolution.py
@@ -1,5 +1,7 @@
import unittest
+import copy
from pylogic.propositional.propositional_logic import Formula, Generalization
+from pylogic.propositional.resolution import ClausePicker
from pylogic.propositional import resolution
from pylogic.propositional import parser
@@ -8,49 +10,247 @@ class TestResolution(unittest.TestCase):
def setUp(self):
self.a1 = Formula("X")
self.a2 = Formula("Y")
+ self.a3 = Formula("Z")
+ self.a4 = Formula("W")
+ self.top = Formula("T")
+ self.bottom = Formula("F")
self.l1 = Formula("!", Formula("X"))
+ self.l2 = Formula("!", Formula("Y"))
self.fand1 = Formula("&", Formula("X"), Formula("Y"))
self.for1 = Formula("|", Formula("X"), Formula("Y"))
self.taut1 = parser.parse("((P->Q)&(Q->R))->-(-R&P)")
self.taut2 = parser.parse("(-P->Q)->((P->Q)->Q)")
self.taut3 = parser.parse("((P->Q)->P)->P")
self.taut4 = parser.parse("(P->(Q->R))->((P->Q)->(P->R))")
+ self.taut5 = parser.parse("(F->X)")
- def test_is_tautology(self):
- self.assertFalse(resolution.is_tautology(self.a1))
- self.assertFalse(resolution.is_tautology(self.l1))
- self.assertFalse(resolution.is_tautology(self.fand1))
- self.assertFalse(resolution.is_tautology(self.for1))
- self.assertTrue(resolution.is_tautology(self.taut1))
- self.assertTrue(resolution.is_tautology(self.taut2))
- self.assertTrue(resolution.is_tautology(self.taut3))
- self.assertTrue(resolution.is_tautology(self.taut4))
+ def test_preliminary_steps(self):
+ clauses = [Generalization("or", [self.top, self.a1, self.a2]),
+ Generalization("or", [self.a2, self.a1, self.l1]),
+ Generalization("or", [self.a1, self.a2, self.bottom]),
+ Generalization("or", [self.a1, self.a3, self.a1]),
+ Generalization("or", [self.a1, self.a4])]
+ exp_clauses = [Generalization("or", [self.a1, self.a2]),
+ Generalization("or", [self.a1, self.a3]),
+ Generalization("or", [self.a1, self.a4])]
+ resolution.preliminary_steps(clauses)
+ self.assertEqual(exp_clauses, clauses)
+
+ def test_manage_tops(self):
+ clauses = [Generalization("or", [self.top, self.a1, self.a2])]
+ exp_clauses = []
+ resolution.manage_tops(clauses)
+ self.assertEqual(exp_clauses, clauses)
+
+ clauses = [Generalization("or", [self.top, self.a1, self.a2]),
+ Generalization("or", [self.bottom, self.top, self.a2]),
+ Generalization("or", [self.a1, self.a2, self.top]),
+ Generalization("or", [self.a1, self.a2])]
+ exp_clauses = [Generalization("or", [self.a1, self.a2])]
+ resolution.manage_tops(clauses)
+ self.assertEqual(exp_clauses, clauses)
+
+
+ def test_manage_complementary(self):
+ clauses = [Generalization("or", [self.a1, self.top, self.l1])]
+ exp_clauses = []
+ resolution.manage_complementary(clauses)
+ self.assertEqual(exp_clauses, clauses)
+
+ clauses = [Generalization("or", [self.a1, self.top, self.l1]),
+ Generalization("or", [self.a2, self.a1, self.l1]),
+ Generalization("or", [self.l1, self.top, self.a1]),
+ Generalization("or", [self.a1, self.a2])]
+ exp_clauses = [Generalization("or", [self.a1, self.a2])]
+ resolution.manage_complementary(clauses)
+ self.assertEqual(exp_clauses, clauses)
+
+
+ def test_manage_bottoms(self):
+ clauses = [Generalization("or", [self.bottom, self.a1, self.a2]),
+ Generalization("or", [self.a1, self.bottom, self.a2]),
+ Generalization("or", [self.a1, self.a2, self.bottom]),
+ Generalization("or", [self.a1, self.a2])]
+ exp_clauses = [Generalization("or", [self.a1, self.a2]),
+ Generalization("or", [self.a1, self.a2]),
+ Generalization("or", [self.a1, self.a2]),
+ Generalization("or", [self.a1, self.a2])]
+ resolution.manage_bottoms(clauses)
+ self.assertEqual(exp_clauses, clauses)
+
+
+ def test_manage_copies(self):
+ clauses = [Generalization("or", [self.a1, self.a1, self.a2]),
+ Generalization("or", [self.a1, self.a2, self.a1]),
+ Generalization("or", [self.a2, self.a1, self.a2, self.a1]),
+ Generalization("or", [self.a1, self.a2])]
+ exp_clauses = [Generalization("or", [self.a1, self.a2]),
+ Generalization("or", [self.a1, self.a2]),
+ Generalization("or", [self.a2, self.a1]),
+ Generalization("or", [self.a1, self.a2])]
+ resolution.manage_copies(clauses)
+ self.assertEqual(exp_clauses, clauses)
+
+
+ def test_manage_duplicated_clauses(self):
+ clauses = [Generalization("or", [self.a1, self.a2]),
+ Generalization("or", [self.a2, self.l1, self.a1]),
+ Generalization("or", [self.a2, self.a1]),
+ Generalization("or", [self.a1, self.a2, self.l1])]
+ exp_clauses = [Generalization("or", [self.a1, self.a2]),
+ Generalization("or", [self.a2, self.l1, self.a1])]
+ resolution.manage_duplicated_clauses(clauses)
+ self.assertEqual(exp_clauses, clauses)
+
+
+ def test_manage_subsumption_rule(self):
+ clauses = [Generalization("or", [self.a1, self.a2]),
+ Generalization("or", [self.a2, self.l1, self.a1]),
+ Generalization("or", [self.a2, self.a1, self.a3]),
+ Generalization("or", [self.a2, self.a3, self.a4]),
+ Generalization("or", [self.a2, self.a3])]
+ exp_clauses = [Generalization("or", [self.a1, self.a2]),
+ Generalization("or", [self.a2, self.a3])]
+ resolution.manage_subsumption_rule(clauses)
+ self.assertEqual(exp_clauses, clauses)
def test_is_closed(self):
expansion1 = [Generalization("or", [self.a1, self.l1]),
Generalization("or", [self.a2])]
- expansion1 = [[False, disj] for disj in expansion1]
expansion2 = [Generalization("or", [self.a1, self.l1]),
Generalization("or", []),
Generalization("or", [self.a2])]
- expansion2 = [[False, disj] for disj in expansion2]
self.assertFalse(resolution.is_closed(expansion1))
self.assertTrue(resolution.is_closed(expansion2))
- def test_expand(self):
- expansion1 = [[False, Generalization("or", [self.a2, self.l1])],
- [False, Generalization("or", [self.fand1, self.a1])],
- [False, Generalization("or", [self.fand1, self.for1])]]
- exp1 = [[True, Generalization("or", [self.a2, self.l1])],
- [False, Generalization("or", [self.fand1, self.a1])],
- [False, Generalization("or", [self.fand1, self.for1])],
- [False, Generalization("or", [self.a2, self.fand1])]]
- result = resolution.expand(expansion1)
- self.assertTrue(result)
- self.assertEqual(exp1, expansion1)
+ def test_is_new(self):
+ expansion1 = [Generalization("or", [self.a1, self.l1]),
+ Generalization("or", [self.a2])]
+ gen1 = Generalization("or", [self.l1, self.a1])
+ self.assertFalse(resolution.is_new(expansion1, gen1))
+ expansion2 = [Generalization("or", [self.a1, self.l1]),
+ Generalization("or", []),
+ Generalization("or", [self.a2])]
+ gen2 = Generalization("or", [self.l1])
+ self.assertTrue(resolution.is_new(expansion2, gen2))
+
+
+ def test_resolution_rule(self):
+ cl1 = Generalization("or", [self.a2, self.l1, self.bottom])
+ cl2 = Generalization("or", [self.top, self.a1])
+ form = self.l1
+ exp_cl = Generalization("or", [self.a2, self.bottom, self.top])
+ self.assertEqual(exp_cl, resolution.resolution_rule(cl1, cl2, form))
+
+
+ def test_apply_resolution_rule(self):
+ cl1 = Generalization("or", [self.a2, self.l1, self.a3])
+ cl2 = Generalization("or", [self.a4, self.a1])
+ exp_cls = Generalization("or", [self.a2, self.a3, self.a4])
+ self.assertEqual(exp_cls, resolution.apply_resolution_rule(cl1, cl2))
+ # complementary litterals in the result clause
+ cl1 = Generalization("or", [self.a2, self.l1, self.a3])
+ cl2 = Generalization("or", [self.a4, self.a1, self.l2])
+ exp_cls = None
+ self.assertEqual(exp_cls, resolution.apply_resolution_rule(cl1, cl2))
+ # copied litterals in the result clause
+ cl1 = Generalization("or", [self.a2, self.l1, self.a3])
+ cl2 = Generalization("or", [self.a4, self.a1, self.a2])
+ exp_cls = Generalization("or", [self.a2, self.a3, self.a4])
+ self.assertEqual(exp_cls, resolution.apply_resolution_rule(cl1, cl2))
+ # no complementary formulas in the clauses
+ cl1 = Generalization("or", [self.a2, self.a4, self.a3])
+ cl2 = Generalization("or", [self.a4, self.a1, self.a3])
+ exp_cls = None
+ self.assertEqual(exp_cls, resolution.apply_resolution_rule(cl1, cl2))
+
+
+ def test_is_tautology(self):
+ def test(filename, truth):
+ f = open(filename, "r")
+ for formula_s in f:
+ if len(formula_s) > 0 and formula_s[0] not in ["%", "\n"]:
+ formula = parser.parse(formula_s)
+ self.assertEqual(truth, resolution.is_tautology(formula))
+
+ tautologies_fn = "examples/prop_tautologies.txt"
+ test(tautologies_fn, True)
+ satisfiables_fn = "examples/prop_satisfiables.txt"
+ test(satisfiables_fn, False)
+
+
+
+class TestClausePicker(unittest.TestCase):
+ def setUp(self):
+ self.a1 = Formula("X")
+ self.a2 = Formula("Y")
+ self.a3 = Formula("Z")
+ self.a4 = Formula("W")
+ self.l1 = Formula("!", Formula("X"))
+ self.expansion = [Generalization("or", [self.a1, self.l1, self.a3]),
+ Generalization("or", [self.a2, self.l1]),
+ Generalization("or", [self.l1, self.a1, self.a4]),
+ Generalization("or", [self.a3])]
+ self.sizes = [3, 2, 3, 1]
+ self.buckets = {3: [(1, 3)],
+ 4: [(0, 3), (2, 3)],
+ 5: [(0, 1), (1, 2)],
+ 6: [(0, 2)]}
+
+
+ def test_init(self):
+ cp = ClausePicker(self.expansion)
+ self.assertEqual(self.sizes, cp.sizes)
+ self.assertEqual(self.buckets, cp.buckets)
+
+
+ def test_pick(self):
+ cp = ClausePicker(self.expansion)
+ self.assertEqual((1, 3), cp.pick())
+ self.assertEqual((0, 3), cp.pick())
+ self.assertEqual((2, 3), cp.pick())
+ self.assertEqual((0, 1), cp.pick())
+ self.assertEqual((1, 2), cp.pick())
+ self.assertEqual((0, 2), cp.pick())
+ # empty buckets
+ self.assertRaises(Exception, cp.pick)
+
+
+ def test_add_clause(self):
+ cp = ClausePicker(self.expansion)
+ gen = Generalization("or", [self.a1, self.a2, self.a3, self.a4])
+ cp.add_clause(gen)
+ exp_sizes = list(self.sizes)
+ exp_sizes.append(len(gen))
+ self.assertEqual(exp_sizes, cp.sizes)
+ exp_buckets = copy.deepcopy(self.buckets)
+ new_index = 4
+ exp_buckets[7] = [(new_index, 0)]
+ exp_buckets[6].append((new_index, 1))
+ exp_buckets[7].append((new_index, 2))
+ exp_buckets[5].append((new_index, 3))
+ self.assertEqual(exp_buckets, cp.buckets)
+
+
+ def test_is_empty(self):
+ cp = ClausePicker(self.expansion)
+ self.assertFalse(cp.is_empty())
+ cp.pick()
+ self.assertFalse(cp.is_empty())
+ cp.pick()
+ self.assertFalse(cp.is_empty())
+ cp.pick()
+ self.assertFalse(cp.is_empty())
+ cp.pick()
+ self.assertFalse(cp.is_empty())
+ cp.pick()
+ self.assertFalse(cp.is_empty())
+ cp.pick()
+ self.assertTrue(cp.is_empty())
+
if __name__ == '__main__':