floating points may also track bit-literals.
Since the legacy solver doesn't handle dual tracking of literals we just let the floating point solver track.
previous scheme has Ackmerman module instrument main solver to backjump and simplify when reaching a threshold.
This destroys overall performance: simplification does many more things than invoking Ackerman axioms.
Having a dependency between simplification (in-processing) and depleting a priority queue of auxiliary axioms therefore hurts overall performance. It has to be decoupled. The current approach is now to empty the axiom queue on occasion.
It is still not ideal - it should be coupled with the search level - axioms don't survive higher levels where redundant clauses get garbage collected as they don't have a chance of being used.
CMAKE_ANDROID_API will set CMAKE_SYSTEM_VERSION if it's not defined.
Also remove setting CMake variable values that don't affect the ability
to successfully configure in CI.
* WiP: publish symbols for package
* set debugtype to full
* fix internal nuget feed publishing
* Try pipeline github authorization
* Update github service connection
* WiP: try symbol publish in build
* try Z3Prover for GitHub connection
* WiP: collect symbols
* revert symbol type to pdbonly (only portable is not supported for publishing)
* Publish symbols in nightly and release
* Revert this: comment out publish to test release build pipe
* restore publishing
* Turn of index sources to eliminate warning that it is not supported for Github
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
- add option smt.bv.reduce_size.
- it allows to apply incremental pre-processing of bit-vectors by identifying ranges that are known to be constant.
This rewrite is beneficial, for instance, when bit-vectors are constrained to have many high-level bits set to 0.
elimination of mod/div should be applied to all occurrences of x under mod/div at the same time. It affects performance and termination to perform elimination on each occurrence since substituting in two new variables for eliminated x doubles the number of variables under other occurrences.
Also generalize inequality resolution to use div.
The new features are still disabled.
