An implementation of Babelsberg allowing constraint-based programming in Python (using the Z3 theorem prover).

See also Babelsberg/R, Babelsberg/JS.

It allows you to write code like the following:

from pybelsberg import always

class Point:
    def __init__(self, x, y):
        self.x = x
        self.y = y
    def distance(self, other):
        return math.sqrt((self.x - other.x)**2 + (self.y - other.y)**2)

a = Point(10.0, 0.0)
b = Point(0.0, 0.0)

# Declare a constraint that should always be satisfied
@always
def constant_distance():
    yield a.distance(b) == 20

print(a.x, a.y) # -> 20.0 0.0
print(b.x, b.y) # -> 0.0 0.0

a.x, a.y = 50.0
print(a.x, a.y) # -> 50.0 50.0
print(b.x, b.y) # -> 30.0 50.0

Pybelsberg requires Python version >= 3.3.

Z3 needs to be built from the unstable branch (using the provided instructions) because only this branch (as of August 2014) supports Python 3.x. Make sure the Z3 directory is in the PYTHONPATH.

Pybelsberg uses tox and py.test for testing.

All of the supported functionality is covered by tests in the /tests directory. Files beginning with "demo" represent more complex use cases. All tests that are marked as "xfail" represent functionality that is not supported yet.

Pybelsberg is open-source and licensed under the BSD 3-Clause License.