Sat delete_set_literal()

in include/poac/core/sat.hpp [79:105]

• 23 lines of code
• 9 McCabe index (conditional complexity)

    Sat delete_set_literal(std::vector<std::vector<int>>& clauses, const int& index, const int& set_val) {
        for (auto itr1 = clauses.begin(); itr1 != clauses.end(); ++itr1) {
            for (auto itr2 = itr1->begin(); itr2 != itr1->end(); ++itr2) {
                // set_val -> unassigned(-1) -> always false
                // set_val -> true(0) -> value == index + 1
                // set_val -> false(1) -> value == -(index + 1)
                if (set_val >= 0 && (set_val == 0 ? index + 1 : -1 * (index + 1)) == *itr2) {
                    clauses.erase(itr1);
                    --itr1; // reset iterator
                    if (clauses.empty()) {
                        return Sat::satisfied;
                    }
                    break; // to the next clause
                }
                else if (index == literal_to_index(*itr2)) { // the literal with opposite polarity
                    itr1->erase(itr2); // remove the literal from the clause
                    --itr2; // reset iterator
                    if (itr1->empty()) {
                        // unsatisfiable currently
                        return Sat::unsatisfied;
                    }
                    break; // to the next clause
                }
            }
        }
        return Sat::normal;
    }