search

pacti-org / pacti

A package for compositional system analysis and design
https://www.pacti.org
BSD 3-Clause "New" or "Revised" License
19 stars 5 forks source link

[Feature request] Add a model finder using SMT #325

Open havelund opened 1 year ago

havelund commented 1 year ago

In a research project at JPL we have encountered the need for obtaining a model from a contract. A model is defined as an assignment to the input variables and output variables that satisfies the conjunction of the assumptions and guarantees.

We suggest to use an SMT solver as a backend for this, and specifically the Z3 SMT solver https://github.com/Z3Prover/z3, which has a convenient Python interface.

There are other SMT solvers, but Z3 has for a long time been one of the main SMT solvers, winning numerous SMT competitions.

An attempt to implement a model finder has been made, adding the following method to the PolyhedralContract class:

def find_model(self) -> Optional[Dict[str, float]]: ...
iincer commented 1 year ago

Adding model finding capabilities via a call

def find_model(self)

is a good idea. Now we have the related function https://github.com/pacti-org/pacti/blob/7a1d27968b68914840e3fb26a5c19baa995adc1f/src/pacti/contracts/polyhedral_iocontract.py#L184

This routine allows us to optimize an arbitrary linear objective. In some situations, we may want a model that optimizes some criteria; in other situations, we may just need a model. The function above, though, is not currently returning the values of the variables that optimize the argument. We can change the function to provide them to the user.

If we changed the prototype of optimize to return values for variables, the two routines above could be used as model finders. Here is a comparison:

Function Technology Supports Optimization Support for unbounded polyhedra
find_model SMT Yes? Always finds a model, if it exists
optimize Linear programming Yes Optima may be unbounded

As find_model is in development using z3, something to consider is the user experience during installation. We will need to add the z3 Python bindings to Pacti's dependencies. Does installing z3 Python bindings include the installation of z3? It would be burdensome on users if we required them to separately install z3 if they don't plan to use find_model.