CPMpy cvc5 interface (cpmpy.solvers.cvc5)

Interface to CVC5’s Python API.

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems that supports a large number of theories and their combination. It is the successor of CVC4 and is intended to be an open and extensible SMT engine. cvc5 is a joint project led by Stanford University and the University of Iowa.(see https://cvc5.github.io/)

This implemantation makes use of cvc5’s “pythonic” API, closely replicating the Z3 API.

Always use cp.SolverLookup.get("cvc5") to instantiate the solver object.

Installation

Requires that the ‘cvc5’ python package is installed:

$ pip install cvc5

See detailed installation instructions at: https://cvc5.github.io/docs/latest/api/python/python.html

The rest of this documentation is for advanced users.

List of classes

CPM_cvc5

Interface to cvc5's Python API.

Module details

class cpmpy.solvers.cvc5.CPM_cvc5(cpm_model=None, subsolver='sat')

Interface to cvc5’s Python API.

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

• cvc5_solver: object, cvc5’s Solver() object

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

Documentation of the solver’s own Python API: https://cvc5.github.io/api/python/pythonic/cvc5.html

Note

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

add(cpm_expr)

CVC5 supports nested expressions so translate expression tree and post to solver API directly

Any CPMpy expression given is immediately transformed (through transform()) and then posted to the solver in this function.

This can raise ‘NotImplementedError’ for any constraint not supported after transformation

The variables used in expressions given to add are stored as ‘user variables’. Those are the only ones the user knows and cares about (and will be populated with a value after solve). All other variables are auxiliary variables created by transformations.

Parameters:

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

Returns:

self

get_core()

For use with s.solve(assumptions=[...]). Only meaningful if the solver returned UNSAT.

Typically implemented in SAT-based solvers

Returns a small subset of assumption literals that are unsat together. (a literal is either a _BoolVarImpl or a NegBoolView in case of its negation, e.g. x or ~x) Setting these literals to True makes the model UNSAT, setting any to False makes it SAT

has_objective()

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)

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

Parameters:

• expr – Expression, the CPMpy expression that represents the objective function

• minimize – Bool, whether it is a minimization problem (True) or maximization problem (False)

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

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)

Call the cvc5 solver

Parameters:

• time_limit (float, optional) – maximum solve time in seconds

• 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

An overview of the cvc5 solver parameters can found at https://cvc5.github.io/docs/cvc5-1.0.8/options.html

You can use any of these parameters as keyword argument to solve() and they will be forwarded to the solver. Examples include:

Argument	Description
rlimit-per	set resource limit
random_seed	random seed
compute-partitions	number of parallel workers (default=0)

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

Parameters:

• 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

• argument (- any other keyword)

Returns:

number of solutions found

solver_var(cpm_var)

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()

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

Returns:

Solver support by current system setup.

Return type:

[bool]

supported_global_constraints: frozenset[str] = frozenset({})

supported_reified_global_constraints: frozenset[str] = frozenset({})

transform(cpm_expr)

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

classmethod version() → str | None

Returns the installed version of the solver’s Python API.