Add Checkpointing Support to Kodkod

TeamAmalgam / kodkod

Kodkod relational model finder

Other

3 stars 0 forks source link

Add Checkpointing Support to Kodkod #39

Closed cpkleynhans closed 10 years ago

cpkleynhans commented 10 years ago

Fixes #8

Adds Checkpointing infrastructure to Kodkod data structures
- Adds a new type of SATSolver the CheckpointableSolver
- Adds checkpointing to Bool2CNFTranslator
- Adds CheckpointedSolver as a type of KodkodSolver
- Adds Translation.Checkpointed as a type of translation
Adds Checkpointing support to the Z3 Solver wrapper
Adds Checkpointing support to MiniSat through solver cloning

Reviewers: @AtulanZaman @joseph2625 @mhyee

mhyee commented 10 years ago

Finally done the code review.

Comments are in the diffs, but some of the key points:

Documentation and comments
Whitespace/indentation inconsistencies (I don't think I caught all of them)
Concrete implementations of MultiObjectiveAlgorithm have changed somewhat since CheckpointedGuidedImprovementAlgorithm was written
There's a lot of stuff for Checkpointed that was simply copied from Incremental and slightly tweaked. Would it be better to inherit from Incremental and override as necessary? (And remove any final modifiers.)

cpkleynhans commented 10 years ago

I've addressed some of the code review feedback. Still need to rewrite CGIA to be more similar to IGIA and investigate overriding existing classes instead of creating our own.

mhyee commented 10 years ago

A few other minor comments, but other than that, the new changes look good.

AtulanZaman commented 10 years ago

Reviewed. Looks fine.

cpkleynhans commented 10 years ago

Feedback addressed. @joseph2625 Are we ok to merge?

joseph39 commented 10 years ago

LGTM