Clean up decision_proceduret #4440
Conversation
peterschrammel
requested review from
cesaro,
chrisr-diffblue,
cristina-david,
danpoe,
hannes-steffenhagen-diffblue,
kroening,
martin-cs,
pkesseli,
smowton and
tautschnig
as code owners
|
clang-format asks for a minor reformatting. |
peterschrammel
force-pushed
the
clean-up-decision-procedure
branch
from
4fc1e92 to
2f8e740
Compare
peterschrammel
assigned kroening, martin-cs and chrisr-diffblue and unassigned peterschrammel
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 2f8e740).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105913707
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
Patch does what is described. I'm not sure why it has been moved out of util. I'm very pro SMT-LIB as an interface to solvers so I am going to be in favour of something conceptually like prop_convt becoming our base BUT we should consider if there are other decision procedures we might want to use that don't or can't fit this interface. For example : I think @dcattaruzza was using mixed integer or linear programming solvers, what about fuzzing approaches ( @cesaro was working on something like this?), are any of the people doing machine leaning things working on this?
There certainly are, but then they also can't be used as drop-in solvers in CBMC as it stands today. |
| inline decision_proceduret &operator<<( | ||
| decision_proceduret &dest, | ||
| const exprt &src) | ||
| /// Push Boolean constraint \p src into decision procedure \p dest |
There was a problem hiding this comment.
Push? Is that the same as add?
There was a problem hiding this comment.
Yes. I'll change it to add.
|
On Wed, 2019-03-27 at 01:50 -0700, Peter Schrammel wrote:
There certainly are, but then they also can't be used as drop-in
solvers in CBMC as it stands today.
I'm also in favour of building things in a general way, but there
must be at least two (current, not future) use cases to enjoy the
benefit; otherwise we'll waste our time maintaining generic
frameworks that are not used.
Fair. I guess it's up to them to shout if they want it.
|
All modules that use decision_proceduret also use solvers. So, there is no need to have this interface in util.
That's not specific to prop_convt.
There is no instance in the code base of using decision_proceduret without these functions.
According to comment in the code.
Complete documentation and reorder methods to make the interface more readable.
Operator for conversion is not intuitive anyway.
peterschrammel
force-pushed
the
clean-up-decision-procedure
branch
from
2f8e740 to
c56f992
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: c56f992).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105996039
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.
decision_proceduretis only used throughprop_convt, because it is lacking essential conversion functions. Moving these functions intodecision_proceduretwill enable to replaceprop_convtbydecision_proceduretthroughout the code base (which is much more intuitive and makes the code more readable).prop_convtwill then evolve into interfaces to support advanced features for incremental solving, etc.