CPMpy z3 interface (cpmpy.solvers.z3)

Interface to z3’s API

Requires that the ‘z3-solver’ python package is installed:

$ pip install z3-solver

Z3 is a highly versatile and effective theorem prover from Microsoft. Underneath, it is an SMT solver with a wide scala of theory solvers. We will interface to the finite-domain integer related parts of the API

Documentation of the solver’s own Python API: https://z3prover.github.io/api/html/namespacez3py.html

Terminology note: a ‘model’ for z3 is a solution!

List of classes

CPM_z3

Interface to z3's API

Module details

class cpmpy.solvers.z3.CPM_z3(cpm_model=None, subsolver='sat')[source]

Interface to z3’s API

Requires that the ‘z3-solver’ python package is installed: $ pip install z3-solver

See detailed installation instructions at: https://github.com/Z3Prover/z3#python

Creates the following attributes (see parent constructor for more):

  • z3_solver: object, z3’s Solver() object

The DirectConstraint, when used, calls a function in the z3 namespace and z3_solver.add()’s the result.

get_core()[source]

For use with s.solve(assumptions=[…]). Only meaningful if the solver returned UNSAT. In that case, get_core() returns a small subset of assumption variables that are unsat together.

CPMpy will return only those variables that are False (in the UNSAT core)

Note that there is no guarantee that the core is minimal, though this interface does upon up the possibility to add more advanced Minimal Unsatisfiabile Subset algorithms on top. All contributions welcome!

has_objective()[source]

Returns whether the solver has an objective function or not.

maximize(expr)

Post the given expression to the solver as objective to maximize

maximize() can be called multiple times, only the last one is stored

minimize(expr)

Post the given expression to the solver as objective to minimize

minimize() can be called multiple times, only the last one is stored

property native_model

Returns the solver’s underlying native model (for direct solver access).

objective(expr, minimize=True)[source]

Post the given expression to the solver as objective to minimize/maximize

‘objective()’ can be called multiple times, only the last one is stored

(technical side note: any constraints created during conversion of the objective are premanently posted to the solver)

objective_value()

Returns the value of the objective function of the latest solver run on this model

Returns:

an integer or ‘None’ if it is not run, or a satisfaction problem

solution_hint(cpm_vars, vals)

For warmstarting the solver with a variable assignment

Typically implemented in SAT-based solvers

Parameters:

  • cpm_vars – list of CPMpy variables

  • vals – list of (corresponding) values for the variables

solve(time_limit=None, assumptions=[], **kwargs)[source]

Call the z3 solver

Arguments: - time_limit: maximum solve time in seconds (float, optional) - assumptions: list of CPMpy Boolean variables (or their negation) that are assumed to be true.

For repeated solving, and/or for use with s.get_core(): if the model is UNSAT, get_core() returns a small subset of assumption variables that are unsat together.

  • kwargs: any keyword argument, sets parameters of solver object

Arguments that correspond to solver parameters:

  • … (no common examples yet)

The full list doesn’t seem to be documented online, you have to run its help() function: ` import z3 z3.Solver().help() `

Warning! Some parameternames in z3 have a ‘.’ in their name, such as (arbitrarily chosen): ‘sat.lookahead_simplify’ You have to construct a dictionary of keyword arguments upfront: ` params = {"sat.lookahead_simplify": True} s.solve(**params) `

solveAll(display=None, time_limit=None, solution_limit=None, call_from_model=False, **kwargs)

Compute all solutions and optionally display the solutions.

This is the generic implementation, solvers can overwrite this with a more efficient native implementation

Arguments:
  • display: either a list of CPMpy expressions, OR a callback function, called with the variables after value-mapping

    default/None: nothing displayed

  • time_limit: stop after this many seconds (default: None)

  • solution_limit: stop after this many solutions (default: None)

  • call_from_model: whether the method is called from a CPMpy Model instance or not

  • any other keyword argument

Returns: number of solutions found

solver_var(cpm_var)[source]

Creates solver variable for cpmpy variable or returns from cache if previously created

solver_vars(cpm_vars)

Like solver_var() but for arbitrary shaped lists/tensors

status()
static supported()[source]

Check for support in current system setup. Return True if the system has package installed or supports solver, else returns False.

Returns:

[bool]: Solver support by current system setup.

transform(cpm_expr)[source]

Transform arbitrary CPMpy expressions to constraints the solver supports

Implemented through chaining multiple solver-independent transformation functions from the cpmpy/transformations/ directory.

See the ‘Adding a new solver’ docs on readthedocs for more information.

Parameters:

cpm_expr (Expression or list of Expression) – CPMpy expression, or list thereof

Returns:

list of Expression