Replaced Clause::[MIN|MAX]_UNIT with Clause::Set::first_unit().
Removed [Atom|Literal]::[MIN|MAX] and Clause::[MIN|MAX]_UNIT because they were only used to iterate over all unit clauses of a setup in Setup::PropagateUnits(). Now there's a Clause::Set::first_unit() method which simply goes to the first or second element or to end() of the set depending on whether or not there is no empty clause but some unit, the empty clause and some unit, or no unit clause, respectively. The loops in Setup::PropagateUnits() to count / resolve with the unit clauses now simply start at first_unit() and stop when is_unit() returns false. That's simpler and even more efficient than the old solution which involved to search operations.
Loading
Please register or sign in to comment