Integrate Z3 as a prover.

TeamAmalgam / kodkod

Kodkod relational model finder

Other

3 stars 0 forks source link

Integrate Z3 as a prover. #24

Closed cpkleynhans closed 10 years ago

cpkleynhans commented 10 years ago

Dependencies: #23

Once Z3 has been integrated as a solver it would be nice to make use of its proving capabilities as well.

cpkleynhans commented 10 years ago

This looks like its going to be complicated. Since this isn't directly related to our project (we don't care about proofs of unsatisfiabilty) I'm going to remove this from the Final Demo Milestone.

mhyee commented 10 years ago

Closing for now, since this is incredibly complicated.