Skip to content

Check which rules can directly generate a clause

Currently a common pattern is to have a rule which generates a unit clause where the literal starts with an or and to then directly use the or rule to deconstruct the disjunctive.

We now emphasize the importance of clauses. Hence, we should probably eliminate this pattern and directly create clauses. There might also be some rules that create implications which are subsequently deconstructed into disjunctions.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information