Drop clause if it contains an impossible BinaryConstraint #2376
Conversation
Some BinaryConstraint atoms can be determined to be impossible during synthesis. Introduce a transform to eliminate clauses containing such impossible atoms. These kinds of atoms are not likely to be written directly, but can easily arise with inlined code.
Codecov Report
Additional details and impacted files@@ Coverage Diff @@
## master #2376 +/- ##
=======================================
Coverage 77.52% 77.53%
=======================================
Files 467 469 +2
Lines 30778 30833 +55
=======================================
+ Hits 23862 23906 +44
- Misses 6916 6927 +11
|
There was a problem hiding this comment.
Could this be done more generally by introducing a constant folding transformer that runs before the RemoveBooleanConstraintsTransformer ?
The RemoveBooleanConstraintsTransformer removes clauses that contain the false constraint.
The constant folding transformer would transform non-satisfiable binary constraints into the false BinaryConstraint, and always-satisfiable binary constraints into the true BinaryConstraint.
Other constant folding operations could be performed as well.
That sounds to me like an approach that would make sense, although we'd have to do some tweaking of the transform pipeline order to get everything working as desired. As I noted, these kind of impossible constraints arise most often in inlined relations. I was only able to get my changes to have the desired result with it after both Do you think it would make sense to move |
|
Hi @quentin, I pushed another commit to refactor the new transform as Of course, we could support rewriting more Let me know if you have further feedback! |
| namespace souffle::ast::transform { | ||
|
|
||
| /** | ||
| * Eliminate clauses containing unsatisfiable constant binary constraints |
There was a problem hiding this comment.
this transform does not eliminate clauses, it simplifies binary constraints into boolean constraints.
There was a problem hiding this comment.
Good catch, updated the docstring.
adamjseitz
force-pushed
the
eliminate-constant-binary-constraint
branch
from
678d1aa
to
fc3eb44
Compare
Some BinaryConstraint atoms can be determined to be impossible during synthesis. This PR introduces a transform to eliminate clauses containing such impossible atoms.
These kinds of atoms are not likely to be written directly, but can easily arise with inlined code.
In ddisasm (with a small work-in-progress change to take greater advantage of this), across its various arch configurations, Souffle generates between 5.0% and 12% fewer lines of C++ with this patch. This yields build time improvements of 2.5% - 10% depending on arch configuration and compiler.
This is my first attempt at adding a transformer pass, so please apply additional scrutiny.