search

TeamAmalgam / kodkod

Kodkod relational model finder
Other
3 stars 0 forks source link

Integrate Z3 as a solver. #23

Closed cpkleynhans closed 11 years ago

cpkleynhans commented 11 years ago

We would like to integrate Z3 into kodkod as a solver since it exposes nice capabilities such as checkpointing. The first step is to add Z3 as a SATSolver.

cpkleynhans commented 11 years ago

I've added the basic solver functionality in the amalgam-z3 branch. Now I just need to ensure that it handles error cases as required by the SATSolver interface and create some more test cases.