Rewrote Clause::Subsumes(), Clause::PropagateUnit[s]().
Using explicit for loops instead of std::[any|all]_of(). For Clause::Subsumes(), this reduces the average performance to n+m instead of n*m. For short clauses as we usually have them the performance gain is minimal. It might be substantial however for the new Clause::PropagateUnits(), which could be used when Setup manages the unit clauses in a sorted set structure. Also moved Literal::Complementary() and Literal::Subsumes() back to readable versions. It seems the compiler optimises these expressions to some expression with the same performance as the bitwise expressions.
Loading
Please register or sign in to comment