[pypy-svn] r22589 - pypy/dist/pypy/lib/logic
auc at codespeak.net
auc at codespeak.net
Tue Jan 24 14:12:44 CET 2006
Author: auc
Date: Tue Jan 24 14:12:41 2006
New Revision: 22589
Modified:
pypy/dist/pypy/lib/logic/constraint.py
pypy/dist/pypy/lib/logic/test_unification.py
pypy/dist/pypy/lib/logic/unification.py
pypy/dist/pypy/lib/logic/variable.py
Log:
(auc, ale)
* add satisfiability check on constraints within the store
* more tests
Modified: pypy/dist/pypy/lib/logic/constraint.py
==============================================================================
--- pypy/dist/pypy/lib/logic/constraint.py (original)
+++ pypy/dist/pypy/lib/logic/constraint.py Tue Jan 24 14:12:41 2006
@@ -124,6 +124,7 @@
if var.dom is None:
raise DomainlessVariables
self._names_to_vars[var.name] = var
+ var.add_constraint(self)
self._variables = variables
def affectedVariables(self):
Modified: pypy/dist/pypy/lib/logic/test_unification.py
==============================================================================
--- pypy/dist/pypy/lib/logic/test_unification.py (original)
+++ pypy/dist/pypy/lib/logic/test_unification.py Tue Jan 24 14:12:41 2006
@@ -234,11 +234,90 @@
u.add_constraint(k)
assert k in u._store.constraints
- def test_narrowing_domains(self):
+ def test_narrowing_domains_failure(self):
x,y,z = u.var('x'), u.var('y'), u.var('z')
x.dom = c.FiniteDomain([1, 2])
y.dom = c.FiniteDomain([2, 3])
z.dom = c.FiniteDomain([3, 4])
k = c.Expression([x, y, z], 'x == y + z')
raises(c.ConsistencyFailure, k.narrow)
+
+ def test_narrowing_domains_success(self):
+ x,y,z = u.var('x'), u.var('y'), u.var('z')
+ x.dom = c.FiniteDomain([1, 2, 5])
+ y.dom = c.FiniteDomain([2, 3])
+ z.dom = c.FiniteDomain([3, 4])
+ k = c.Expression([x, y, z], 'x == y + z')
+ k.narrow()
+ assert x.dom == c.FiniteDomain([5])
+ assert y.dom == c.FiniteDomain([2])
+ assert z.dom == c.FiniteDomain([3])
+
+ def test_store_satisfiable_success(self):
+ x,y,z = u.var('x'), u.var('y'), u.var('z')
+ x.dom = c.FiniteDomain([1, 2, 5])
+ y.dom = c.FiniteDomain([2, 3])
+ z.dom = c.FiniteDomain([3, 4])
+ k = c.Expression([x, y, z], 'x == y + z')
+ u.add_constraint(k)
+ assert u.satisfiable(k) == True
+ assert x.dom == c.FiniteDomain([1, 2, 5])
+ assert y.dom == c.FiniteDomain([2, 3])
+ assert z.dom == c.FiniteDomain([3, 4])
+
+ def test_store_satisfiable_failure(self):
+ x,y,z = u.var('x'), u.var('y'), u.var('z')
+ x.dom = c.FiniteDomain([1, 2])
+ y.dom = c.FiniteDomain([2, 3])
+ z.dom = c.FiniteDomain([3, 4])
+ k = c.Expression([x, y, z], 'x == y + z')
+ u.add_constraint(k)
+ assert u.satisfiable(k) == False
+ assert x.dom == c.FiniteDomain([1, 2])
+ assert y.dom == c.FiniteDomain([2, 3])
+ assert z.dom == c.FiniteDomain([3, 4])
+
+ def test_satisfy_many_const_success(self):
+ x,y,z,w = (u.var('x'), u.var('y'),
+ u.var('z'), u.var('w'))
+ x.dom = c.FiniteDomain([1, 2, 5])
+ y.dom = c.FiniteDomain([2, 3])
+ z.dom = c.FiniteDomain([3, 4])
+ w.dom = c.FiniteDomain([1, 4, 5])
+ k1 = c.Expression([x, y, z], 'x == y + z')
+ k2 = c.Expression([z, w], 'z < w')
+ u.add_constraint(k1)
+ u.add_constraint(k2)
+ assert u.satisfiable(k1) == True
+ assert x.dom == c.FiniteDomain([1, 2, 5])
+ assert y.dom == c.FiniteDomain([2, 3])
+ assert z.dom == c.FiniteDomain([3, 4])
+ assert w.dom == c.FiniteDomain([1, 4, 5])
+ assert u.satisfiable(k2) == True
+ assert x.dom == c.FiniteDomain([1, 2, 5])
+ assert y.dom == c.FiniteDomain([2, 3])
+ assert z.dom == c.FiniteDomain([3, 4])
+ assert w.dom == c.FiniteDomain([1, 4, 5])
+
+ def test_satisfy_many_const_failure(self):
+ x,y,z,w = (u.var('x'), u.var('y'),
+ u.var('z'), u.var('w'))
+ x.dom = c.FiniteDomain([1, 2, 5])
+ y.dom = c.FiniteDomain([2, 3])
+ z.dom = c.FiniteDomain([3, 4])
+ w.dom = c.FiniteDomain([1])
+ k1 = c.Expression([x, y, z], 'x == y + z')
+ k2 = c.Expression([z, w], 'z < w')
+ u.add_constraint(k1)
+ u.add_constraint(k2)
+ assert u.satisfiable(k1) == False
+ assert x.dom == c.FiniteDomain([1, 2, 5])
+ assert y.dom == c.FiniteDomain([2, 3])
+ assert z.dom == c.FiniteDomain([3, 4])
+ assert w.dom == c.FiniteDomain([1])
+ assert u.satisfiable(k2) == False
+ assert x.dom == c.FiniteDomain([1, 2, 5])
+ assert y.dom == c.FiniteDomain([2, 3])
+ assert z.dom == c.FiniteDomain([3, 4])
+ assert w.dom == c.FiniteDomain([1])
Modified: pypy/dist/pypy/lib/logic/unification.py
==============================================================================
--- pypy/dist/pypy/lib/logic/unification.py (original)
+++ pypy/dist/pypy/lib/logic/unification.py Tue Jan 24 14:12:41 2006
@@ -121,7 +121,7 @@
import threading
from variable import EqSet, Var, VariableException, NotAVariable
-from constraint import FiniteDomain
+from constraint import FiniteDomain, ConsistencyFailure
#----------- Store Exceptions ----------------------------
class UnboundVariable(VariableException):
@@ -196,11 +196,47 @@
raise AlreadyBound
var.dom = FiniteDomain(dom)
- #-- Add constraints -------------------------
+ #-- Constraints -------------------------
def add_constraint(self, constraint):
self.constraints.add(constraint)
+ def satisfiable(self, constraint):
+ """ * satisfiable (k) checks that the constraint k
+ can be satisfied wrt its variable domains
+ and other constraints on these variables
+ * does NOT mutate the store
+ """
+ # Satisfiability of one constraints entails
+ # satisfiability of the transitive closure
+ # of all constraints associated with the vars
+ # of our given constraint.
+ # We make a copy of the domains
+ # then traverse the constraints & attached vars
+ # to collect all (in)directly affected vars
+ # then compute narrow() on all (in)directly
+ # affected constraints.
+ assert constraint in self.constraints
+ varset = set()
+ constset = set()
+ compute_dependant_vars(constraint, varset, constset)
+ old_domains = {}
+ for var in varset:
+ old_domains[var] = FiniteDomain(var.dom)
+
+ def restore_domains(domains):
+ for var, dom in domains.items():
+ var.dom = dom
+
+ for const in constset:
+ try:
+ const.narrow()
+ except ConsistencyFailure:
+ restore_domains(old_domains)
+ return False
+ restore_domains(old_domains)
+ return True
+
#-- BIND -------------------------------------------
def bind(self, var, val):
@@ -344,6 +380,19 @@
return True
+def compute_dependant_vars(constraint, varset,
+ constset):
+ if constraint in constset: return
+ constset.add(constraint)
+ for var in constraint.affectedVariables():
+ varset.add(var)
+ dep_consts = var.constraints
+ for const in dep_consts:
+ if const in constset:
+ continue
+ compute_dependant_vars(const, varset, constset)
+
+
#-- Unifiability checks---------------------------------------
#--
#-- quite costly & could be merged back in unify
@@ -423,6 +472,9 @@
def add_constraint(constraint):
return _store.add_constraint(constraint)
+def satisfiable(constraint):
+ return _store.satisfiable(constraint)
+
def bind(var, val):
return _store.bind(var, val)
Modified: pypy/dist/pypy/lib/logic/variable.py
==============================================================================
--- pypy/dist/pypy/lib/logic/variable.py (original)
+++ pypy/dist/pypy/lib/logic/variable.py Tue Jan 24 14:12:41 2006
@@ -39,6 +39,8 @@
self._val = NoValue
# domain
self.dom = None
+ # constraints
+ self.constraints = set()
# when updated in a 'transaction', keep track
# of our initial value (for abort cases)
self.previous = None
@@ -92,6 +94,10 @@
def __hash__(self):
return self.name.__hash__()
+
+ def add_constraint(self, constraint):
+ self.constraints.add(constraint)
+
#---- Concurrent public ops --------------------------
def is_bound(self):
More information about the Pypy-commit
mailing list