-
Notifications
You must be signed in to change notification settings - Fork 30
Adding Pumpkin solver #669
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: master
Are you sure you want to change the base?
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
looking good, some comments and a few questions
cpmpy/solvers/pumpkin.py
Outdated
return self.pum_solver | ||
|
||
|
||
def solve(self, time_limit=None, proof=None, assumptions=None): |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
so in GCS we already made some decisions for the 'solve' api to proof logging...
there we decided an attribute 'prove' if it should store its proof, and 'verify' if it should be verified... then we also have proof_name and proof_location; I'm not sure these are the best choices, e,g. 'proof=True, proof_file=...' would also make sense, but I do think we should have both solvers have equally named attributes
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hmm yeah having both proof-name and proof-location seems a bit redundant. But we shouldn't change the gcs interface in this PR...
So I'll now mimic the gcs interface, and then we change later on if we want.
(Related: probably we can also enable prooflogging in pysat and exact using the same inteface?)
Processed review. |
Updated the interface with the new "table" and "negative table" constraints, and implemented the time_limit argument. The package name was also updated (not available on pip yet) so updated doc too. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
so does this PR depend on the PR of the linearize change? because if we merge this it will also merge the linearize change...
nice. a few minor comments, will be great to add (even if its not on pip yet...)
@@ -1,3 +1,4 @@ | |||
import inspect |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think you need inspect
super().__init__(name="pumpkin", cpm_model=cpm_model) | ||
|
||
@property | ||
def native_model(self): |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
do we do that for other solvers? there its just in the docs that it is called self.pum_solver, and we don't provide an indirect/abstraction?
:return: list of Expression | ||
""" | ||
# apply transformations | ||
cpm_cons = toplevel_list(cpm_expr) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
also partial?
also, csemap has since been merged I think
|
||
def _get_constraint(self, cpm_expr): | ||
""" | ||
Get a solver's constraint by a supported CPMpy constraint |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
'by a'? confusing
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
also, add to the docs "expects a transformed cpm_expr as input, this is a separate function so we can add an indicator variable to it if needed"
Adding the LCG-Pumpkin solver.
WIP and need to update a bunch of tests still