[pypy-svn] r22718 - pypy/dist/pypy/lib/logic
auc at codespeak.net
auc at codespeak.net
Fri Jan 27 10:56:24 CET 2006
Author: auc
Date: Fri Jan 27 10:56:20 2006
New Revision: 22718
Added:
pypy/dist/pypy/lib/logic/problems.py
Removed:
pypy/dist/pypy/lib/logic/test_unification.py
pypy/dist/pypy/lib/logic/unification.py
Modified:
pypy/dist/pypy/lib/logic/computationspace.py
pypy/dist/pypy/lib/logic/constraint.py
pypy/dist/pypy/lib/logic/distributor.py
pypy/dist/pypy/lib/logic/test_computationspace.py
pypy/dist/pypy/lib/logic/test_variable.py
pypy/dist/pypy/lib/logic/variable.py
Log:
(ale, auc)
merge store and computation space
- the diff contains a lot of garbage
Modified: pypy/dist/pypy/lib/logic/computationspace.py
==============================================================================
--- pypy/dist/pypy/lib/logic/computationspace.py (original)
+++ pypy/dist/pypy/lib/logic/computationspace.py Fri Jan 27 10:56:20 2006
@@ -1,4 +1,4 @@
-## The Constraint-based computation model
+# The Constraint-based computation model
## ======================================
## A computation space collects together basic constraints (in fact
@@ -177,14 +177,21 @@
## space = ComputationSpace(fun=my_problem)
-from unification import Store, var
-from constraint import ConsistencyFailure
-from threading import Thread, Condition
+from threading import Thread, Condition, RLock, local
-class Unprocessed:
+from variable import EqSet, Var, \
+ VariableException, NotAVariable, AlreadyInStore
+from constraint import FiniteDomain, ConsistencyFailure
+
+EmptyDom = FiniteDomain([])
+
+class Succeeded:
+ """It contains no choice points but a solution to
+ the logic program.
+ """
pass
-class Working:
+class Distributable:
pass
class Failed(Exception):
@@ -197,38 +204,372 @@
"""
pass
-class Succeeded:
- """It contains no choice points but a solution to
- the logic program.
- """
- pass
+class Alternatives(object):
+ def __init__(self, nb_alternatives):
+ self._nbalt = nb_alternatives
+ def __eq__(self, other):
+ if other is None: return False
+ return self._nbalt == other._nbalt
+
+
+#----------- Store Exceptions ----------------------------
+class UnboundVariable(VariableException):
+ def __str__(self):
+ return "%s has no value yet" % self.name
+
+class AlreadyBound(VariableException):
+ def __str__(self):
+ return "%s is already bound" % self.name
+
+class NotInStore(VariableException):
+ def __str__(self):
+ return "%s not in the store" % self.name
+
+class OutOfDomain(VariableException):
+ def __str__(self):
+ return "value not in domain of %s" % self.name
+
+class UnificationFailure(Exception):
+ def __init__(self, var1, var2, cause=None):
+ self.var1, self.var2 = (var1, var2)
+ self.cause = cause
+ def __str__(self):
+ diag = "%s %s can't be unified"
+ if self.cause:
+ diag += " because %s" % self.cause
+ return diag % (self.var1, self.var2)
+
+class IncompatibleDomains(Exception):
+ def __init__(self, var1, var2):
+ self.var1, self.var2 = (var1, var2)
+ def __str__(self):
+ return "%s %s have incompatible domains" % \
+ (self.var1, self.var2)
+
+class Foo(object):
+ pass
+
+#---- ComputationSpace -------------------------------
class ComputationSpace(object):
+ """The Store consists of a set of k variables
+ x1,...,xk that are partitioned as follows:
+ * set of unbound variables that are equal
+ (also called equivalence sets of variables).
+ The variables in each set are equal to each
+ other but not to any other variables.
+ * variables bound to a number, record or procedure
+ (also called determined variables)."""
+
+ def __init__(self, problem, parent=None):
+ self.parent = parent
- def __init__(self, program, parent=None):
+ # current/working computation space, per thread
+ # self.TLS = local()
+ self.TLS = Foo()
+ self.TLS.current_cs = self
+
+ # consistency-preserving stuff
+ self.in_transaction = False
+ self.bind_lock = RLock()
+ self.status = None
+ self.status_condition = Condition()
+
if parent is None:
- self.store = Store()
- self.root = self.store.var('root')
- self.store.bind(self.root, program(self))
+ self.vars = set()
+ # mapping of names to vars (all of them)
+ self.names = {}
+ # mapping of vars to constraints
+ self.var_const_map = {}
+ # set of all constraints
+ self.constraints = set()
+ self.root = self.var('__root__')
+ self.bind(self.root, problem(self))
else:
- self.store = parent.store
+ self.vars = parent.vars
+ self.names = parent.names
+ self.var_const_map = parent.var_const_map
+ self.constraints = parent.constraints
self.root = parent.root
- self.program = program
- self.parent = parent
- # status
- self.status = Unprocessed
- self.status_condition = Condition()
+
# run ...
self._process()
+ #-- Variables ----------------------------
+
+ def var(self, name):
+ """creates a variable of name name and put
+ it into the store"""
+ v = Var(name, self)
+ self.add_unbound(v)
+ return v
+
+ def add_unbound(self, var):
+ """add unbound variable to the store"""
+ if var in self.vars:
+ raise AlreadyInStore(var.name)
+ print "adding %s to the store" % var
+ self.vars.add(var)
+ self.names[var.name] = var
+ # put into new singleton equiv. set
+ var.val = EqSet([var])
+
+ def set_domain(self, var, dom):
+ """bind variable to domain"""
+ assert(isinstance(var, Var) and (var in self.vars))
+ if var.is_bound():
+ raise AlreadyBound
+ var.dom = FiniteDomain(dom)
+
+ def get_var_by_name(self, name):
+ try:
+ return self.names[name]
+ except KeyError:
+ raise NotInStore(name)
+
+ #-- Constraints -------------------------
+
+ def add_constraint(self, constraint):
+ self.constraints.add(constraint)
+ for var in constraint.affectedVariables():
+ self.var_const_map.setdefault(var, [])
+ self.var_const_map[var].append(constraint)
+
+ def get_variables_with_a_domain(self):
+ varset = set()
+ for var in self.vars:
+ if var.dom != EmptyDom: varset.add(var)
+ return varset
+
+ 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()
+ self._compute_dependant_vars(constraint, varset, constset)
+ old_domains = collect_domains(varset)
+
+ for const in constset:
+ try:
+ const.narrow()
+ except ConsistencyFailure:
+ restore_domains(old_domains)
+ return False
+ restore_domains(old_domains)
+ return True
+
+
+ def get_satisfying_domains(self, constraint):
+ assert constraint in self.constraints
+ varset = set()
+ constset = set()
+ self._compute_dependant_vars(constraint, varset,
+ constset)
+ old_domains = collect_domains(varset)
+
+ for const in constset:
+ try:
+ const.narrow()
+ except ConsistencyFailure:
+ restore_domains(old_domains)
+ return {}
+ narrowed_domains = collect_domains(varset)
+ restore_domains(old_domains)
+ return narrowed_domains
+
+ def satisfy(self, constraint):
+ assert constraint in self.constraints
+ varset = set()
+ constset = set()
+ self._compute_dependant_vars(constraint, varset, constset)
+ old_domains = collect_domains(varset)
+
+ for const in constset:
+ try:
+ const.narrow()
+ except ConsistencyFailure:
+ restore_domains(old_domains)
+ raise
+
+ def satisfy_all(self):
+ old_domains = collect_domains(self.vars)
+ for const in self.constraints:
+ try:
+ const.narrow()
+ except ConsistencyFailure:
+ restore_domains(old_domains)
+ raise
+
+ def _compute_dependant_vars(self, constraint, varset,
+ constset):
+ if constraint in constset: return
+ constset.add(constraint)
+ for var in constraint.affectedVariables():
+ varset.add(var)
+ dep_consts = self.var_const_map[var]
+ for const in dep_consts:
+ if const in constset:
+ continue
+ self._compute_dependant_vars(const, varset,
+ constset)
+
+ #-- BIND -------------------------------------------
+
+ def bind(self, var, val):
+ """1. (unbound)Variable/(unbound)Variable or
+ 2. (unbound)Variable/(bound)Variable or
+ 3. (unbound)Variable/Value binding
+ """
+ try:
+ self.bind_lock.acquire()
+ assert(isinstance(var, Var) and (var in self.vars))
+ if var == val:
+ return
+ if _both_are_vars(var, val):
+ if _both_are_bound(var, val):
+ raise AlreadyBound(var.name)
+ if var._is_bound(): # 2b. var is bound, not var
+ self.bind(val, var)
+ elif val._is_bound(): # 2a.var is bound, not val
+ self._bind(var.val, val.val)
+ else: # 1. both are unbound
+ self._merge(var, val)
+ else: # 3. val is really a value
+ print "%s, is that you ?" % var
+ if var._is_bound():
+ raise AlreadyBound(var.name)
+ self._bind(var.val, val)
+ finally:
+ self.bind_lock.release()
+
+
+ def _bind(self, eqs, val):
+ # print "variable - value binding : %s %s" % (eqs, val)
+ # bind all vars in the eqset to val
+ for var in eqs:
+ if var.dom != EmptyDom:
+ if val not in var.dom.get_values():
+ print val, var.dom, var.dom.get_values()
+ # undo the half-done binding
+ for v in eqs:
+ v.val = eqs
+ raise OutOfDomain(var)
+ var.val = val
+
+ def _merge(self, v1, v2):
+ for v in v1.val:
+ if not _compatible_domains(v, v2.val):
+ raise IncompatibleDomains(v1, v2)
+ self._really_merge(v1.val, v2.val)
+
+ def _really_merge(self, eqs1, eqs2):
+ # print "unbound variables binding : %s %s" % (eqs1, eqs2)
+ if eqs1 == eqs2: return
+ # merge two equisets into one
+ eqs1 |= eqs2
+ # let's reassign everybody to the merged eq
+ for var in eqs1:
+ var.val = eqs1
+
+ #-- UNIFY ------------------------------------------
+
+ def unify(self, x, y):
+ self.in_transaction = True
+ try:
+ try:
+ self._really_unify(x, y)
+ for var in self.vars:
+ if var.changed:
+ var._commit()
+ except Exception, cause:
+ for var in self.vars:
+ if var.changed:
+ var._abort()
+ if isinstance(cause, UnificationFailure):
+ raise
+ raise UnificationFailure(x, y, cause)
+ finally:
+ self.in_transaction = False
+
+ def _really_unify(self, x, y):
+ # print "unify %s with %s" % (x,y)
+ if not _unifiable(x, y): raise UnificationFailure(x, y)
+ if not x in self.vars:
+ if not y in self.vars:
+ # duh ! x & y not vars
+ if x != y: raise UnificationFailure(x, y)
+ else: return
+ # same call, reverse args. order
+ self._unify_var_val(y, x)
+ elif not y in self.vars:
+ # x is Var, y a value
+ self._unify_var_val(x, y)
+ elif _both_are_bound(x, y):
+ self._unify_bound(x,y)
+ elif x._is_bound():
+ self.bind(x,y)
+ else:
+ self.bind(y,x)
+
+ def _unify_var_val(self, x, y):
+ if x.val != y:
+ try:
+ self.bind(x, y)
+ except AlreadyBound:
+ raise UnificationFailure(x, y)
+
+ def _unify_bound(self, x, y):
+ # print "unify bound %s %s" % (x, y)
+ vx, vy = (x.val, y.val)
+ if type(vx) in [list, set] and isinstance(vy, type(vx)):
+ self._unify_iterable(x, y)
+ elif type(vx) is dict and isinstance(vy, type(vx)):
+ self._unify_mapping(x, y)
+ else:
+ if vx != vy:
+ raise UnificationFailure(x, y)
+
+ def _unify_iterable(self, x, y):
+ print "unify sequences %s %s" % (x, y)
+ vx, vy = (x.val, y.val)
+ idx, top = (0, len(vx))
+ while (idx < top):
+ self._really_unify(vx[idx], vy[idx])
+ idx += 1
+
+ def _unify_mapping(self, x, y):
+ # print "unify mappings %s %s" % (x, y)
+ vx, vy = (x.val, y.val)
+ for xk in vx.keys():
+ self._really_unify(vx[xk], vy[xk])
+
+#-- Computation Space -----------------------------------------
+
+
def _process(self):
try:
- self.store.satisfy_all()
+ self.satisfy_all()
except ConsistencyFailure:
self.status = Failed
else:
- self.status = Succeeded
+ if self._distributable():
+ self.status = Distributable
+ else:
+ self.status = Succeeded
def _stable(self):
#XXX: really ?
@@ -246,12 +587,18 @@
def _distributable(self):
if self.status not in (Failed, Succeeded, Merged):
- return self.distributor.findSmallestDomain() > 1
+ return self._distributable_domains()
# in The Book : "the space has one thread that is
# suspended on a choice point with two or more alternatives.
# A space canhave at most one choice point; attempting to
# create another gives an error."
+ def _distributable_domains(self):
+ for var in self.vars:
+ if var.dom.size() > 1 :
+ return True
+ return False
+
def set_distributor(self, dist):
self.distributor = dist
@@ -262,7 +609,7 @@
while not self._stable():
self.status_condition.wait()
if self._distributable():
- return self.distributor.nb_subdomains()
+ return Alternatives(self.distributor.nb_subdomains())
return self.status
finally:
self.status_condition.release()
@@ -309,4 +656,137 @@
self.do_something_with(result)
+
+
+
+#-------------------------------------------------------
+
+
+def _compatible_domains(var, eqs):
+ """check that the domain of var is compatible
+ with the domains of the vars in the eqs
+ """
+ if var.dom == EmptyDom: return True
+ empty = set()
+ for v in eqs:
+ if v.dom == EmptyDom: continue
+ if v.dom.intersection(var.dom) == empty:
+ return False
+ return True
+
+#-- collect / restore utilities for domains
+
+def collect_domains(varset):
+ """makes a copy of domains of a set of vars
+ into a var -> dom mapping
+ """
+ dom = {}
+ for var in varset:
+ if var.dom != EmptyDom:
+ dom[var] = FiniteDomain(var.dom)
+ return dom
+
+def restore_domains(domains):
+ """sets the domain of the vars in the domains mapping
+ to their (previous) value
+ """
+ for var, dom in domains.items():
+ var.dom = dom
+
+
+#-- Unifiability checks---------------------------------------
+#--
+#-- quite costly & could be merged back in unify
+
+def _iterable(thing):
+ return type(thing) in [list, set]
+
+def _mapping(thing):
+ return type(thing) is dict
+
+# memoizer for _unifiable
+_unifiable_memo = set()
+
+def _unifiable(term1, term2):
+ global _unifiable_memo
+ _unifiable_memo = set()
+ return _really_unifiable(term1, term2)
+def _really_unifiable(term1, term2):
+ """Checks wether two terms can be unified"""
+ if ((id(term1), id(term2))) in _unifiable_memo: return False
+ _unifiable_memo.add((id(term1), id(term2)))
+ # print "unifiable ? %s %s" % (term1, term2)
+ if _iterable(term1):
+ if _iterable(term2):
+ return _iterable_unifiable(term1, term2)
+ return False
+ if _mapping(term1) and _mapping(term2):
+ return _mapping_unifiable(term1, term2)
+ if not(isinstance(term1, Var) or isinstance(term2, Var)):
+ return term1 == term2 # same 'atomic' object
+ return True
+
+def _iterable_unifiable(c1, c2):
+ """Checks wether two iterables can be unified"""
+ # print "unifiable sequences ? %s %s" % (c1, c2)
+ if len(c1) != len(c2): return False
+ idx, top = (0, len(c1))
+ while(idx < top):
+ if not _really_unifiable(c1[idx], c2[idx]):
+ return False
+ idx += 1
+ return True
+
+def _mapping_unifiable(m1, m2):
+ """Checks wether two mappings can be unified"""
+ # print "unifiable mappings ? %s %s" % (m1, m2)
+ if len(m1) != len(m2): return False
+ if m1.keys() != m2.keys(): return False
+ v1, v2 = (m1.items(), m2.items())
+ v1.sort()
+ v2.sort()
+ return _iterable_unifiable([e[1] for e in v1],
+ [e[1] for e in v2])
+
+#-- Some utilities -----------------------------------------------
+
+def _both_are_vars(v1, v2):
+ return isinstance(v1, Var) and isinstance(v2, Var)
+
+def _both_are_bound(v1, v2):
+ return v1._is_bound() and v2._is_bound()
+
+
+
+#--
+#-- the global store
+from problems import dummy_problem
+_store = ComputationSpace(dummy_problem)
+
+#-- global accessor functions
+def var(name):
+ v = Var(name, _store)
+ _store.add_unbound(v)
+ return v
+
+def set_domain(var, dom):
+ return _store.set_domain(var, dom)
+
+def add_constraint(constraint):
+ return _store.add_constraint(constraint)
+
+def satisfiable(constraint):
+ return _store.satisfiable(constraint)
+
+def get_satisfying_domains(constraint):
+ return _store.get_satisfying_domains(constraint)
+
+def satisfy(constraint):
+ return _store.satisfy(constraint)
+
+def bind(var, val):
+ return _store.bind(var, val)
+
+def unify(var1, var2):
+ return _store.unify(var1, var2)
Modified: pypy/dist/pypy/lib/logic/constraint.py
==============================================================================
--- pypy/dist/pypy/lib/logic/constraint.py (original)
+++ pypy/dist/pypy/lib/logic/constraint.py Fri Jan 27 10:56:20 2006
@@ -109,22 +109,27 @@
if other is None: return False
return self._values == other._values
+ def __ne__(self, other):
+ return not self == other
+
def intersection(self, other):
if other is None: return self.get_values()
return self._values & other._values
+
#-- Constraints ------------------------------------------
+EmptyDom = FiniteDomain([])
+
class AbstractConstraint(object):
def __init__(self, variables):
"""variables is a list of variables which appear in the formula"""
self._names_to_vars = {}
for var in variables:
- if var.dom is None:
+ if var.dom == EmptyDom:
raise DomainlessVariables
self._names_to_vars[var.name] = var
- var.add_constraint(self)
self._variables = variables
def affectedVariables(self):
@@ -194,12 +199,12 @@
"""A constraint represented as a python expression."""
_FILTER_CACHE = {}
- def __init__(self, variables, formula, type='fd.Expression'):
+ def __init__(self, variables, formula, typ='fd.Expression'):
"""variables is a list of variables which appear in the formula
formula is a python expression that will be evaluated as a boolean"""
- AbstractConstraint.__init__(self, variables)
self.formula = formula
- self.type = type
+ self.type = typ
+ AbstractConstraint.__init__(self, variables)
try:
self.filterFunc = Expression._FILTER_CACHE[formula]
except KeyError:
Modified: pypy/dist/pypy/lib/logic/distributor.py
==============================================================================
--- pypy/dist/pypy/lib/logic/distributor.py (original)
+++ pypy/dist/pypy/lib/logic/distributor.py Fri Jan 27 10:56:20 2006
@@ -19,7 +19,7 @@
"""returns the variable having the smallest domain.
(or one of such varibles if there is a tie)
"""
- vars_ = [var for var in self.c_space.store.get_variables_with_a_domain()
+ vars_ = [var for var in self.c_space.get_variables_with_a_domain()
if var.dom.size() > 1]
best = vars_[0]
@@ -33,7 +33,7 @@
"""returns the variable having the largest domain.
(or one of such variables if there is a tie)
"""
- vars_ = [var for var in self.c_space.store.get_variables_with_a_domain()
+ vars_ = [var for var in self.c_space.get_variables_with_a_domain()
if var.dom.size() > 1]
best = vars_[0]
@@ -52,7 +52,7 @@
"""do the minimal job and let concrete class distribute variables
"""
self.verbose = verbose
- variables = self.c_space.store.get_variables_with_a_domain()
+ variables = self.c_space.get_variables_with_a_domain()
replicas = []
for i in range(self.nb_subdomains()):
replicas.append(make_new_domains(variables))
Added: pypy/dist/pypy/lib/logic/problems.py
==============================================================================
--- (empty file)
+++ pypy/dist/pypy/lib/logic/problems.py Fri Jan 27 10:56:20 2006
@@ -0,0 +1,52 @@
+import computationspace as cs
+import constraint as c
+import distributor as di
+
+
+def satisfiable_problem(computation_space):
+ cs = computation_space
+ x, y, z, w = (cs.var('x'), cs.var('y'),
+ cs.var('z'), cs.var('w'))
+ x.cs_set_dom(cs, c.FiniteDomain([2, 6]))
+ y.cs_set_dom(cs, c.FiniteDomain([2, 3]))
+ z.cs_set_dom(cs, c.FiniteDomain([4, 5]))
+ w.cs_set_dom(cs, c.FiniteDomain([1, 4, 5, 6, 7]))
+ cs.add_constraint(c.Expression([x, y, z], 'x == y + z'))
+ cs.add_constraint(c.Expression([z, w], 'z < w'))
+ # set up a distribution strategy
+ cs.set_distributor(di.DichotomyDistributor(cs))
+ return (x, w, y)
+
+def one_solution_problem(computation_space):
+ cs = computation_space
+ x, y, z, w = (cs.var('x'), cs.var('y'),
+ cs.var('z'), cs.var('w'))
+ x.cs_set_dom(cs, c.FiniteDomain([2, 6]))
+ y.cs_set_dom(cs, c.FiniteDomain([2, 3]))
+ z.cs_set_dom(cs, c.FiniteDomain([4, 5]))
+ w.cs_set_dom(cs, c.FiniteDomain([1, 4, 5]))
+ cs.add_constraint(c.Expression([x, y, z], 'x == y + z'))
+ cs.add_constraint(c.Expression([z, w], 'z < w'))
+ # set up a distribution strategy
+ cs.set_distributor(di.DichotomyDistributor(cs))
+ return (x, w, y)
+
+
+def unsatisfiable_problem(computation_space):
+ cs = computation_space
+ x, y, z, w = (cs.var('x'), cs.var('y'),
+ cs.var('z'), cs.var('w'))
+ x.cs_set_dom(cs, c.FiniteDomain([2, 6]))
+ y.cs_set_dom(cs, c.FiniteDomain([2, 3]))
+ z.cs_set_dom(cs, c.FiniteDomain([4, 5]))
+ w.cs_set_dom(cs, c.FiniteDomain([1]))
+ cs.add_constraint(c.Expression([x, y, z], 'x == y + z'))
+ cs.add_constraint(c.Expression([z, w], 'z < w'))
+ # set up a distribution strategy
+ cs.set_distributor(di.DichotomyDistributor(cs))
+ return (x, w, y)
+
+def dummy_problem(computation_space):
+ ret = computation_space.var('__dummy__')
+ ret.dom = c.FiniteDomain([1, 2])
+ return ret
Modified: pypy/dist/pypy/lib/logic/test_computationspace.py
==============================================================================
--- pypy/dist/pypy/lib/logic/test_computationspace.py (original)
+++ pypy/dist/pypy/lib/logic/test_computationspace.py Fri Jan 27 10:56:20 2006
@@ -1,51 +1,412 @@
-import unification as u
+from threading import Thread
+
import variable as v
import constraint as c
import computationspace as cs
import distributor as di
+from problems import *
from py.test import raises
-#-- utility ------------------
+#-- helpers -----------------
-class hdict(dict):
- """a hashable dict"""
- def __hash__(self):
- return id(self)
+#-- meat ------------------------
-#-- helpers -----------------
+class FunThread(Thread):
-def satisfiable_problem(computation_space):
- cs = computation_space
- s = cs.store
- x, y, z, w = (s.var('x'), s.var('y'),
- s.var('z'), s.var('w'))
- s.set_domain(x, c.FiniteDomain([2, 6]))
- s.set_domain(y, c.FiniteDomain([2, 3]))
- s.set_domain(z, c.FiniteDomain([4, 5]))
- s.set_domain(w, c.FiniteDomain([1, 4, 5, 6, 7]))
- s.add_constraint(c.Expression([x, y, z], 'x == y + z'))
- s.add_constraint(c.Expression([z, w], 'z < w'))
- # set up a distribution strategy
- cs.set_distributor(di.DichotomyDistributor(cs))
- return (x, w, y)
-
-def unsatisfiable_problem(computation_space):
- cs = computation_space
- s = cs.store
- x, y, z, w = (s.var('x'), s.var('y'),
- s.var('z'), s.var('w'))
- s.set_domain(x, c.FiniteDomain([2, 6]))
- s.set_domain(y, c.FiniteDomain([2, 3]))
- s.set_domain(z, c.FiniteDomain([4, 5]))
- s.set_domain(w, c.FiniteDomain([1]))
- s.add_constraint(c.Expression([x, y, z], 'x == y + z'))
- s.add_constraint(c.Expression([z, w], 'z < w'))
- # set up a distribution strategy
- cs.set_distributor(di.DichotomyDistributor(cs))
- return (x, w, y)
+ def __init__(self, fun, *args):
+ Thread.__init__(self)
+ self.fun = fun
+ self.args = args
+
+ def run(self):
+ self.fun(self, *self.args)
+
+class TestStoreUnification:
+
+ def setup_method(self, meth):
+ cs._store = cs.ComputationSpace(dummy_problem)
+
+ def test_already_in_store(self):
+ x = cs.var('x')
+ raises(v.AlreadyInStore, cs.var, 'x')
+
+ def test_already_bound(self):
+ x = cs.var('x')
+ cs.bind(x, 42)
+ raises(cs.AlreadyBound, cs.bind, x, 42)
+
+ def test_bind_var_var(self):
+ x = cs.var('x')
+ y = cs.var('y')
+ z = cs.var('z')
+ cs.bind(x, z)
+ assert x.val == cs.EqSet([x, z])
+ assert y.val == cs.EqSet([y])
+ assert z.val == cs.EqSet([x, z])
+
+ def test_bind_var_val(self):
+ x, y, z = cs.var('x'), cs.var('y'), cs.var('z')
+ cs.bind(x, z)
+ cs.bind(y, 42)
+ cs.bind(z, 3.14)
+ assert x.val == 3.14
+ assert y.val == 42
+ assert z.val == 3.14
+
+ def test_unify_same(self):
+ x,y,z,w = (cs.var('x'), cs.var('y'),
+ cs.var('z'), cs.var('w'))
+ cs.bind(x, [42, z])
+ cs.bind(y, [z, 42])
+ cs.bind(w, [z, 43])
+ raises(cs.UnificationFailure, cs.unify, x, w)
+ cs.unify(x, y)
+ assert z.val == 42
+
+ def test_double_unification(self):
+ x, y, z = (cs.var('x'), cs.var('y'),
+ cs.var('z'))
+ cs.bind(x, 42)
+ cs.bind(y, z)
+ cs.unify(x, y)
+ assert z.val == 42
+ cs.unify(x, y)
+ assert (z.val == x.val) and (x.val == y.val)
+
+
+ def test_unify_values(self):
+ x, y = cs.var('x'), cs.var('y')
+ cs.bind(x, [1, 2, 3])
+ cs.bind(y, [1, 2, 3])
+ cs.unify(x, y)
+ assert x.val == [1, 2, 3]
+ assert y.val == [1, 2, 3]
+
+ def test_unify_lists_success(self):
+ x,y,z,w = (cs.var('x'), cs.var('y'),
+ cs.var('z'), cs.var('w'))
+ cs.bind(x, [42, z])
+ cs.bind(y, [w, 44])
+ cs.unify(x, y)
+ assert x.val == [42, z]
+ assert y.val == [w, 44]
+ assert z.val == 44
+ assert w.val == 42
+
+ def test_unify_dicts_success(self):
+ x,y,z,w = (cs.var('x'), cs.var('y'),
+ cs.var('z'), cs.var('w'))
+ cs.bind(x, {1:42, 2:z})
+ cs.bind(y, {1:w, 2:44})
+ cs.unify(x, y)
+ assert x.val == {1:42, 2:z}
+ assert y.val == {1:w, 2:44}
+ assert z.val == 44
+ assert w.val == 42
+
+ def test_unify_failure(self):
+ x,y,z = cs.var('x'), cs.var('y'), cs.var('z')
+ cs.bind(x, [42, z])
+ cs.bind(y, [z, 44])
+ raises(cs.UnificationFailure, cs.unify, x, y)
+ # check store consistency
+ assert x.val == [42, z]
+ assert y.val == [z, 44]
+ assert z.val == cs.EqSet([z])
+
+ def test_unify_failure2(self):
+ x,y,z,w = (cs.var('x'), cs.var('y'),
+ cs.var('z'), cs.var('w'))
+ cs.bind(x, [42, z])
+ cs.bind(y, [w, 44])
+ cs.bind(z, w)
+ assert cs._store.in_transaction == False
+ raises(cs.UnificationFailure, cs.unify, x, y)
+ assert cs._store.in_transaction == False
+ # check store consistency
+ assert x.val == [42, z]
+ assert y.val == [w, 44]
+ assert z.val == cs.EqSet([z,w])
+ assert w.val == cs.EqSet([z,w])
+
+ def test_unify_circular(self):
+ x, y, z, w, a, b = (cs.var('x'), cs.var('y'),
+ cs.var('z'), cs.var('w'),
+ cs.var('a'), cs.var('b'))
+ cs.bind(x, [y])
+ cs.bind(y, [x])
+ raises(cs.UnificationFailure, cs.unify, x, y)
+ cs.bind(z, [1, w])
+ cs.bind(w, [z, 2])
+ raises(cs.UnificationFailure, cs.unify, z, w)
+ cs.bind(a, {1:42, 2:b})
+ cs.bind(b, {1:a, 2:42})
+ raises(cs.UnificationFailure, cs.unify, a, b)
+ # check store consistency
+ assert x.val == [y]
+ assert y.val == [x]
+ assert z.val == [1, w]
+ assert w.val == [z, 2]
+ assert a.val == {1:42, 2:b}
+ assert b.val == {1:a, 2:42}
+
+
+ def test_threads_creating_vars(self):
+ def create_var(thread, *args):
+ x = cs.var('x')
+
+ def create_var2(thread, *args):
+ raises(v.AlreadyExists, cs.var, 'x')
+
+ t1, t2 = (FunThread(create_var),
+ FunThread(create_var2))
+ t1.start()
+ t2.start()
+
+
+ def test_threads_binding_vars(self):
+
+ def do_stuff(thread, var, val):
+ thread.raised = False
+ try:
+ # pb. with TLS (thread-local-stuff) in
+ # cs class
+ cs.bind(var, val)
+ except Exception, e:
+ print e
+ thread.raised = True
+ assert isinstance(e, cs.AlreadyBound)
+
+ x = cs.var('x')
+ vars_ = []
+ for nvar in range(1000):
+ v = cs.var('x-'+str(nvar))
+ cs.bind(x, v)
+ vars_.append(v)
+
+ for var in vars_:
+ assert var in cs._store.vars
+ assert var.val == x.val
+
+ t1, t2 = (FunThread(do_stuff, x, 42),
+ FunThread(do_stuff, x, 43))
+ t1.start()
+ t2.start()
+ t1.join()
+ t2.join()
+ #check that every var is really bound to 42 or 43
+ for var in vars_:
+ assert var in cs._store.vars
+ assert var.val == x.val
+ assert (t2.raised and not t1.raised) or \
+ (t1.raised and not t2.raised)
+
+
+ def test_set_var_domain(self):
+ x = cs.var('x')
+ cs.set_domain(x, [1, 3, 5])
+ assert x.dom == c.FiniteDomain([1, 3, 5])
+
+ def test_bind_with_domain(self):
+ x = cs.var('x')
+ cs.set_domain(x, [1, 2, 3])
+ raises(cs.OutOfDomain, cs.bind, x, 42)
+ cs.bind(x, 3)
+ assert x.val == 3
+
+ def test_bind_with_incompatible_domains(self):
+ x, y = cs.var('x'), cs.var('y')
+ cs.set_domain(x, [1, 2])
+ cs.set_domain(y, [3, 4])
+ raises(cs.IncompatibleDomains, cs.bind, x, y)
+ cs.set_domain(y, [2, 4])
+ cs.bind(x, y)
+ # check x and y are in the same equiv. set
+ assert x.val == y.val
+
+
+ def test_unify_with_domains(self):
+ x,y,z = cs.var('x'), cs.var('y'), cs.var('z')
+ cs.bind(x, [42, z])
+ cs.bind(y, [z, 42])
+ cs.set_domain(z, [1, 2, 3])
+ raises(cs.UnificationFailure, cs.unify, x, y)
+ cs.set_domain(z, [41, 42, 43])
+ cs.unify(x, y)
+ assert z.val == 42
+ assert z.dom == c.FiniteDomain([41, 42, 43])
+
+ def test_add_constraint(self):
+ x,y,z = cs.var('x'), cs.var('y'), cs.var('z')
+ raises(c.DomainlessVariables,
+ c.Expression, [x, y, z], 'x == y + 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')
+ cs.add_constraint(k)
+ assert k in cs._store.constraints
+
+ def test_narrowing_domains_failure(self):
+ x,y,z = cs.var('x'), cs.var('y'), cs.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 = cs.var('x'), cs.var('y'), cs.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 = cs.var('x'), cs.var('y'), cs.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')
+ cs.add_constraint(k)
+ assert cs.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 = cs.var('x'), cs.var('y'), cs.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')
+ cs.add_constraint(k)
+ assert cs.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_compute_dependant_vars(self):
+ x,y,z,w = (cs.var('x'), cs.var('y'),
+ cs.var('z'), cs.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')
+ cs.add_constraint(k1)
+ cs.add_constraint(k2)
+ varset = set()
+ constset = set()
+ cs._store._compute_dependant_vars(k1, varset, constset)
+ assert varset == set([x, y, z, w])
+ assert constset == set([k1, k2])
+
+ def test_satisfiable_many_const_success(self):
+ x,y,z,w = (cs.var('x'), cs.var('y'),
+ cs.var('z'), cs.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')
+ cs.add_constraint(k1)
+ cs.add_constraint(k2)
+ assert cs.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 cs.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])
+ narrowed_doms = cs.get_satisfying_domains(k1)
+ assert narrowed_doms == {x:c.FiniteDomain([5]),
+ y:c.FiniteDomain([2]),
+ z:c.FiniteDomain([3]),
+ w:c.FiniteDomain([4, 5])}
+ narrowed_doms = cs.get_satisfying_domains(k2)
+ assert narrowed_doms == {x:c.FiniteDomain([5]),
+ y:c.FiniteDomain([2]),
+ z:c.FiniteDomain([3]),
+ w:c.FiniteDomain([4, 5])}
+
+
+ def test_satisfiable_many_const_failure(self):
+ x,y,z,w = (cs.var('x'), cs.var('y'),
+ cs.var('z'), cs.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')
+ cs.add_constraint(k1)
+ cs.add_constraint(k2)
+ assert cs.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 cs.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])
+ narrowed_doms = cs.get_satisfying_domains(k1)
+ assert narrowed_doms == {}
+ narrowed_doms = cs.get_satisfying_domains(k2)
+ assert narrowed_doms == {}
+
+ def test_satisfy_many_const_failure(self):
+ x,y,z,w = (cs.var('x'), cs.var('y'),
+ cs.var('z'), cs.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')
+ cs.add_constraint(k1)
+ cs.add_constraint(k2)
+ raises(cs.ConsistencyFailure, cs.satisfy, k1)
+ 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])
+ raises(cs.ConsistencyFailure, cs.satisfy, k2)
+ 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])
+
+ def test_satisfy_many_const_success(self):
+ x,y,z,w = (cs.var('x'), cs.var('y'),
+ cs.var('z'), cs.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')
+ cs.add_constraint(k1)
+ cs.add_constraint(k2)
+ cs.satisfy(k2)
+ print x.dom
+ assert x.dom == c.FiniteDomain([5])
+ assert y.dom == c.FiniteDomain([2])
+ assert z.dom == c.FiniteDomain([3])
+ assert w.dom == c.FiniteDomain([4, 5])
-#-- meat ------------------------
class TestComputationSpace:
@@ -54,26 +415,30 @@
def test_bind_cs_root(self):
spc = cs.ComputationSpace(satisfiable_problem)
- assert 'root' in spc.store.names
+ assert '__root__' in spc.names
assert set(['x', 'y', 'w']) == \
set([var.name for var in spc.root.val])
- def test_process_and_ask_success(self):
- spc = cs.ComputationSpace(satisfiable_problem)
+ def test_ask_success(self):
+ spc = cs.ComputationSpace(one_solution_problem)
assert spc.ask() == cs.Succeeded
-
- def test_process_and_ask_failure(self):
+
+ def test_ask_failure(self):
spc = cs.ComputationSpace(unsatisfiable_problem)
assert spc.ask() == cs.Failed
+ def test_ask_alternatives(self):
+ spc = cs.ComputationSpace(satisfiable_problem)
+ assert spc.ask() == cs.Alternatives(2)
+
def test_distribute(self):
spc = cs.ComputationSpace(satisfiable_problem)
new_domains = [tuple(d.items()) for d in
spc.distributor.distribute()]
- x, y, z, w = (spc.store.get_var_by_name('x'),
- spc.store.get_var_by_name('y'),
- spc.store.get_var_by_name('z'),
- spc.store.get_var_by_name('w'))
+ x, y, z, w = (spc.get_var_by_name('x'),
+ spc.get_var_by_name('y'),
+ spc.get_var_by_name('z'),
+ spc.get_var_by_name('w'))
expected_domains = [tuple({x: c.FiniteDomain([6]),
y: c.FiniteDomain([2]),
z: c.FiniteDomain([4]),
Modified: pypy/dist/pypy/lib/logic/test_variable.py
==============================================================================
--- pypy/dist/pypy/lib/logic/test_variable.py (original)
+++ pypy/dist/pypy/lib/logic/test_variable.py Fri Jan 27 10:56:20 2006
@@ -1,7 +1,10 @@
+from threading import Thread
+
from py.test import raises
-import unification as u
+
+import computationspace as u
import variable as v
-from threading import Thread
+from problems import *
class Consumer(Thread):
@@ -22,7 +25,7 @@
class TestVariable:
def setup_method(self, meth):
- u._store = u.Store()
+ u._store = u.ComputationSpace(dummy_problem)
def test_no_same_name(self):
x = u.var('x')
Modified: pypy/dist/pypy/lib/logic/variable.py
==============================================================================
--- pypy/dist/pypy/lib/logic/variable.py (original)
+++ pypy/dist/pypy/lib/logic/variable.py Fri Jan 27 10:56:20 2006
@@ -1,7 +1,8 @@
-# First cut at representing Oz dataflow variable
-
import threading
+from constraint import FiniteDomain
+
+
#----------- Exceptions ---------------------------------
class VariableException(Exception):
def __init__(self, name):
@@ -30,19 +31,15 @@
class Var(object):
- def __init__(self, name, store):
- if name in store.names:
+ def __init__(self, name, cs):
+ if name in cs.names:
raise AlreadyInStore(name)
self.name = name
- self.store = store
+ self.cs = cs
# top-level 'commited' binding
self._val = NoValue
- # domain in a flat world
- self.dom = None
# domains in multiple spaces
- self.doms = {}
- # constraints
- self.constraints = set()
+ self._doms = {cs : FiniteDomain([])}
# when updated in a 'transaction', keep track
# of our initial value (for abort cases)
self.previous = None
@@ -51,7 +48,7 @@
self.mutex = threading.Lock()
self.value_condition = threading.Condition(self.mutex)
- # for consumption by the global store
+ # for consumption by the global cs
def _is_bound(self):
return not isinstance(self._val, EqSet) \
@@ -69,7 +66,7 @@
# value accessors
def _set_val(self, val):
self.value_condition.acquire()
- if self.store.in_transaction:
+ if self.cs.in_transaction:
if not self.changed:
self.previous = self._val
self.changed = True
@@ -103,15 +100,27 @@
is_bound = _is_bound
def cs_set_dom(self, cs, dom):
- self.doms[cs] = dom
+ self._doms[cs] = dom
def cs_get_dom(self, cs):
- return self.doms[cs]
+ return self._doms[cs]
#---- Concurrent public ops --------------------------
# should be used by threads that want to block on
# unbound variables
+
+ def set_dom(self, dom):
+ self.cs_set_dom(self.cs.TLS.current_cs, dom)
+
+ def get_dom(self):
+ return self.cs_get_dom(self.cs.TLS.current_cs)
+
+ dom = property(get_dom, set_dom)
+
def get(self):
+ """Make threads wait on the variable
+ being bound
+ """
try:
self.value_condition.acquire()
while not self._is_bound():
More information about the Pypy-commit
mailing list