* updates related to issue #5140
* updated/simplified some cases
* fixing feedback comments
* fixed comments and added missing case for get_re_head_tail_reversed
* two bug fixes and some other code improvements
* 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
* Rename to neg_cond
* Add some logging utilities
* Implement case of forbidden interval covering the whole domain
* Implement diseq_narrow
* Do not activate constraint if we are in a conflict state
* comments
* Assert that lemma isn't undefined
* Update revert_decision to work in the case where narrowing causes propagation
* Fix case of non-disjunctive lemma from forbidden intervals
* Conflict should not leak outside user scope
* Add guard to decide(), some notes
* Add test case
* Add constraints to watchlist of unassigned variable during propagation
* Move common propagation functionality into base class
* Combine eq/diseq narrow
* Compute forbidden interval for equality constraints by considering them as p <=u 0 (or p >u 0 for disequalities)
* Pop assign_eh
* Fix scoped_ptr_vector constructors, add detach()
* Need to copy the returned lemma
* Add test
* Basic inequality tests
* Return disjunctive lemma to caller
* Fix XOR over BDDs
* Add operator<< for find_int_t
* Add equality assertion macro that prints expression values on failure
* Adapt contains_int and find_int to take externally-defined bits
* Add more operations on BDD vectors
* Remove old functions
* Additional bddv functions
* Rename some things
* Make bddv a class and add operators
* Fix find_num/contains_num calls
* Add a few helper methods for encoding sets of integers as BDDs
* Use BDD functions in solver
* Add bdd::find_int
* Use bdd::find_int in solver
* Add narrowing for linear equality constraints
* Simplify code for linear propagation
* Add test for later
* Narrowing can only handle linear constraints with a single variable
* Need to push_cjust
* Add polysat logging support
* Don't really need the usual log levels
* Indent log headings
* Add display method to ptr_vector
* Add some logging to solver
* Use __FUNCSIG__ on MSVC
* CMake: simplify FindGMP.cmake
Remove printing of all the different variables, and let FPHSA output the library
name. Add an imported target, which bundles the library and the include
directories for easier usage.
* fix build: vector::c_ptr() now is vector::data()
* CMake: use Threads::Threads imported module
Otherwise the setting of THREADS_PREFER_PTHREAD_FLAG has no effect.
* CMake: remove needless policy setting
The minimum required version is CMake 3.4, where these policies are already set
to new because they were introduced earlier.
* CMake: remove needless variable expansion
* Expose 'inv' on rationals to get reciprocal value
* Align parameter names with implementation
* Add cached operation that divides PDD by a constant
* Fix display for constant PDDs
* operator^ should probably call ^ instead of + (mk_xor instead of add)
* Add helper function 'pow' on PDDs
