* Refactor: remove sign and dep from constraint
* fix some bugs
* improve log messages
* Add missing premises to lemma
* Rename getter in an attempt to fix linux build
* update example to match slides
* Add normalized view of inequalities
* workaround
* Add a conflict explanation rule
* unit clauses should be asserted at the base level
* Add src constraint to interval
* support non-strict case in first rule
* print conflict constraints only once
* update second rule
* update third rule as well
* update include paths
* bdd fixes
* update/fix some tests
* work around assertion failure when constraint from clause becomes unit
* Remove old code
* use clause_builder
* Verify model when returning SAT
* log
* fix
* display constraint's extra info in one place
* Add stub for conflict explainer
* Add helper functions to check whether constraint is active at base level
* Add helper class tmp_assign
* Add clause_builder; it skips unnecessary literals during clause creation
* some fixes
* Use clause_builder for forbidden intervals
* remove old comments
* fixes/comments in solver
* print redundant clauses
* First pass at conflict_explainer
* remove unused model class
* Choose value for k
* also print min/max k
* Add macro to disable linear solver for development
* Move new_* and add_* to header
* Add ref_vector_core::push_back(ref<T>&&)
* Attempt to simplify lifetime handling
* Make operator bool() explicit
* clause improvements
* display boolean assignment
* clause::resolve
* bug fixes
* more fixes
* final case of backtrack
* Extend search state by boolean literals
* Only resolve against positive equality
* mk_dep_ref
* Make clause non-owning
* scoped_clause
* Use scoped_clause
* minor
* scoped_ptr move assignment
* WIP: internal handling of disjunctive constraints
* leaf_value
* disjunctive constraints continued
* Fix bool_lit
* Actually add constraints to storage
* Some fixes
* more fixes
* constraint should have a bool_lit instead of a bool_var
* propagate(bool_lit)
* updates
* interface changes
* small fixes
* Make sat::dimacs_lit's constructor explicit
(otherwise, calling operator<< with sat::literal is ambiguous)
* Use sat::literal
* Print test name at the beginning
* Convention: constraint corresponds to the positive boolean literal
* Make constraint ownership more explicit
* clause stores literals
