warthog-logic / warthog

A Logic Framework in Scala
16 stars 5 forks source link

Changed Picosat class to object; Multiple call of init/reset method now ... #6

Closed ghost closed 9 years ago

ghost commented 11 years ago

...possible

kuebler commented 11 years ago

please double check with Christoph if he's comfortable with your PR, as far as I'm concerned I would prefer if you'd perform the suggested changes (see comments in the code) and resubmit the PR.

czengler commented 11 years ago

Actually I am fine with the PR.

a) Picosat really should be an object, because there can only be one instance - this way we avoid multiple instantiations.

b) The 'contract', that init and reset can be executed only once is not specified anywhere. And for other solvers this is also not the case. So I would be happier, if we would not enforce this contract but let the user just perform multiple inits and resets and just handle that it happens only once in the code. So the user does not need to worry about this kind of stuff - I would hate to get some kind of double-init exceptions for that.

But as usual I am open for discussion :)

kuebler commented 11 years ago

The 'contract' is indeed picosat specific. However, I would still expect double initialisation to have some effect (e.g. taking the solver to an empty state - no variables, no clauses), the current version just ignores any init call after init has been called once. In my opinion, resetting the solver state on double initialization would be just fine. But that's just my 0.02 $ :).

ghost commented 11 years ago

Thank you for commenting.

I commited the format styles. I do not know, if another Pull Request is necessary now (or does the Pull Request just take the branch, not a specific commit ?). Please let me know, if another one is necessary.

I think there are two possibilities: a) Set the solver to an empty state (reset) after a second init method call as Andreas suggested (which makes a separate reset method unnecessary, because you just have to call the init method again to get the solver reseted) b) Ignore any further init call after the solver is initialized (as implemented in the Pull Request), which makes a separate reset method necessary.

ghost commented 11 years ago

Please let me know, which of both possibilities you prefer and I will do so. :-)

ghost commented 11 years ago

@Andreas : I have not heard from you since 15 days. The question above still remains. If you do not want those changes, please close this request.

kuebler commented 11 years ago

Sorry, have been busy lately. I'd still go for option (a) :)

ghost commented 11 years ago

@Andreas: Thank your for the feedback. @czengler: If you agree with solution a), I will adapt the pull request to this one.

andreas commented 11 years ago

@rwalter Please use the correct user names that you intend to notify. Thanks.