Conversation
|
I created #505 so we can actually get some concrete data on the impact of this change. |
|
I did some benchmarking. Here are the results. Big conjunction
Many small conjunctions
|
|
On my laptop the results are a bit different, but overall the same message. I'll dig a bit deeper because the results are not what I expected. |
|
Sounds good! These are from mantella. I didn't try to interpret the results, I was a bit in a hurry for leaving home... |
|
Actually, the results are quite different on my laptop :D |
aehyvari
left a comment
aehyvari
left a comment
There was a problem hiding this comment.
Here are some tiny comments.
src/logics/Logic.cc
Outdated
|
|
||
| namespace { | ||
| struct LessThanPTRefIgnoreNot { | ||
| Logic & logic; |
src/logics/Logic.cc
Outdated
| @@ -430,89 +442,53 @@ Logic::mkIte(vec<PTRef>&& args) | |||
| PTRef Logic::mkAnd(vec<PTRef>&& args) { | |||
| if (args.size() == 0) { return getTerm_true(); } | |||
There was a problem hiding this comment.
We could remove this special case. I'm not sure if it's worth it? What do you think, @blishko ?
There was a problem hiding this comment.
Same for Logic::mkOr of course.
There was a problem hiding this comment.
I agree, it is extremely rare case and it is handled later correctly anyway.
It might help the code optimization if we remove this branch.
2 participants
This PR suggests to change the simplification code of
mkAndandmkOrmethods.It uses slightly more complicated comparison method for sorting the arguments, but the benefits are
mkNotwhich is currently called for every negated argument.mkNotseems like a simple operation, but it itself needs to use auxiliary vector for its single argument and it needs to do the lookup in the boolean term table.Profiles suggest that sorting is typically very fast, while the lookup and copies are more expensive, so I believe this is a good tradeoff.
This could be followed by automatically sorting all commutative operators in
Logic::mkFun, as proposed in #491, in which case, we could introduce (developers-only) versions ofmkAnd/mkOrthat would skip the simplification altogether (if we are sure the arguments are already simplified.