Implemented unit propagation (efficiently).
* Renamed: clause.[hc] is now setup.[hc]. * Added: vector_remove_all() to remove an array of indices efficiently * Added: set_remove_all(), a mutating version of set_difference() * Added: set_get_unsafe() to get a mutable pointer * Added: unit test for vector_remove_all(), set_remove_all() * Added: SET_ALIAS for less code duplication * Added: hacky but efficient setup_unit_clauses() It uses the new vector_cmp() to limit consideration to first clauses. * Added: hacky but efficient clause_resolve() It uses set_remove_all() to compute a clause that is derivable by unit resolution and subsumes all other ones. * Added: efficient setup_propagate() * Fixed: literal_cmp() didn't compare the signs (but the pred twice) * Changed: first criterion of vector_cmp() is the length This allows for fast retrieval of unit clauses in a setup.
Loading
Please sign in to comment