Add Z3 wrapper as a SAT Solver.

TeamAmalgam / kodkod

Kodkod relational model finder

Other

3 stars 0 forks source link

Add Z3 wrapper as a SAT Solver. #27

Closed cpkleynhans closed 11 years ago

cpkleynhans commented 11 years ago

Fixes #23

Reviewers: @AtulanZaman @joseph2625 @mhyee

cpkleynhans commented 11 years ago

Ping @AtulanZaman @joseph2625 @mhyee Any comments?

mhyee commented 11 years ago

Missed a test for adding a negative number of variables, eg addVariables(-1).

Besides that and my other comment, looks good.

cpkleynhans commented 11 years ago

Added a test for clause with variable 0 and adding negative number of variables.

cpkleynhans commented 11 years ago

@joseph2625 @AtulanZaman Any comments?

joseph39 commented 11 years ago

looks good.

AtulanZaman commented 11 years ago

We have test for the incremental solver. Is it possible to have a test for the "pop" functionality of Z3 for removing constraint?

cpkleynhans commented 11 years ago

Pop functionality is being worked on in a different branch. This is just adding the basic SAT solving functionality of Z3. Adding pop requires a lot of changes to core kodkod structures.

AtulanZaman commented 11 years ago

Looks fine