cheshire/pyices

Python bindings for Yices SMT solver

Pyices

Python bindings for Yices SMT solver. Works as a layer on top of C API, on top of the layer generated by ctypesgen.

Installation

1. Download Yices.
2. Set the YICES_PATH environment variable to the Yices folder (namely, the .so file should be under $YICES_PATH/lib and the header files should be under $YICES_PATH/include.
3. Install the package: python setup.py install. NOTE: Pyices uses custom hooks for installation, so the build command will not work properly! Use install.

Usage Example

Unit tests under pyices/tests contain comprehensive usage examples, including pushing and popping and namespaces.

A simple example is copied below:

x = YicesExpression.from_real_var("x")
y = YicesExpression.from_real_var("y")
z = YicesExpression.from_real_var("z")

expr = (x == y + z) & (z >= 10) & (y >= 5)

ctx = YicesContext.from_term(expr)
sat = ctx.check_sat()

self.assertEquals(
    sat,
    True
)

x_val = ctx.get_real_value("x")
y_val = ctx.get_real_value("y")
z_val = ctx.get_real_value("z")

self.assertEquals(
    x_val, y_val + z_val
)