simplifiers layer is a common substrate for global non-incremental and incremental processing.
The first two layers are new, but others are to be ported form tactics.
- bv::slice - rewrites equations to cut-dice-slice bit-vector extractions until they align. It creates opportunities for rewriting portions of bit-vectors to common sub-expressions, including values.
- euf::completion - generalizes the KB simplifcation from asserted formulas to use the E-graph to establish a global and order-independent canonization.
The interface dependent_expr_simplifier is amenable to forming tactics. Plugins for asserted-formulas is also possible but not yet realized.
* WiP: test build specific version number
* update mk_win_dist for assembly-version
* Add print statements for version
* remove stray semicolon
* undo quote change in projectstr
* nit fixes
* revert print formatting for Mac build
* fix spaces
* 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>
These are all unused and shouldn't be needed. Mostly we need
something for differentiating between POSIX and non-POSIX
(until we can reduce some of those differences as well).
We shouldn't need to modify the build system to build on a new
OS if it is basically a Unix and is supported by cmake.
This was only being enabled on Windows, Linux, and FreeBSD. (FreeBSD
only had it enabled in the legacy build system, not in cmake.)
`thread_local` is part of C++11, so now that we require C++17
or later and more recent compilers, this should work everywhere
that threading does, so only disable it within a `SINGLE_THREAD`
build.
