Skip to content

Pybelsberg/pybelsberg

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

23 Commits
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

pybelsberg

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

Setup

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.

Documentation

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.

License

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

About

A Python implementation of Babelsberg

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages