[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