Use propt::lcnf instead of propt::l_set_to{true,false} #2033
Conversation
tautschnig
requested review from
kroening,
martin-cs and
peterschrammel
as code owners
| simplify(implication, ns); | ||
| const bvt &bv2 = convert_bv(implication); | ||
| CHECK_RETURN(bv2.size() == 1); | ||
| prop.l_set_to_true(bv2[0]); |
There was a problem hiding this comment.
I recall changing uncached converts to cached ones here and it having a strange impact on performance. It might be worth checking this.
src/solvers/flattening/arrays.cpp
Outdated
| @@ -253,7 +253,7 @@ void arrayst::add_array_constraint(const lazy_constraintt &lazy, bool refine) | |||
| else | |||
| { | |||
| // add the constraint eagerly | |||
| prop.l_set_to_true(convert(lazy.lazy)); | |||
| prop.lcnf(bvt(1, convert(lazy.lazy))); | |||
There was a problem hiding this comment.
This rather assumes that CNF's are cheaper than assignments, which may not always be true. For example, the AIG back-end prefers avoiding CNF. Is there another way this can be done? Do we need a 'set disjunct to true / false' method?
There was a problem hiding this comment.
Also much harder to read. There are many people who don't know what "CNF" is.
Avoids the lower-level l_set_to(..., {true,false}) and may then
highlight opportunities for further optimisation.
tautschnig
force-pushed
the
lcnf-cleanup
branch
from
923bd12 to
8c5303a
Compare
tautschnig
changed the title
|
This is now just the first, (I believe) uncontroversial and very small commit. @martin-cs would you mind taking another look? |
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 8c5303a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102145374
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- 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).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
tautschnig
dismissed
martin-cs’s stale review
Dismissing as the comments only concerned commits no longer in this PR.
Some code cleanup to avoid redundant clauses. Still needs proper evaluation, thus marking do-not-merge.