* Added function to select the next variable to split on
* Fixed typo
* Small fixes
* uint -> int
* Fixed missing assignment for binary clauses
* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically
* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation
* Update (not compiling yet)
* #6429
* remove ternary clause optimization
Removing ternary clause optimization from sat_solver simplifies special case handling of ternary clauses throughout the sat solver and dependent solvers (pb_solver). Benchmarking on QF_BV suggests the ternary clause optimization does not have any effect. While removing ternary clause optimization two bugs in unit propagation were also uncovered: it missed propagations when the only a single undef literal remained in the non-watched literals and it did not update blocked literals in cases where it could in the watch list. These performance bugs were for general clauses, ternary clause propagation did not miss propagations (and don't use blocked literals), but fixing these issues for general clauses appear to have made ternary clause optimization irrelevant based on what was measured.
* Update: Missing data-structures (still not compiling)
* Nearly compiling
* Some missing arguments
* Polishing
* Only conflicts/propagations/justifications are missing for making it compile
* Added propagation (justifications for them are still missing)
* Use the right deallocation
* Use Z3's memory allocation system
* Ported "seen"
* Polishing
* Added 64-bit "1" counting
* More polishing
* minor fixes
- ensure mk_extract performs simplification to distribute over extract and removing extract if the range is the entire bit-vector
- ensure bool_rewriter simplifeis disjunctions when applicable.
* adding simplifiers layer
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.
* Create bv_slice_tactic.cpp
missing file
* adding virtual destructor
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Added 64-bit "1" counting (#6434)
* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically
* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation
* Added 64-bit "1" counting
* remove incorrect assertion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Added limit to "visit" to allow detecting multiple visits (#6435)
* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically
* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation
* Added limit to "visit" to allow detecting multiple visits
* Putting visit in a separate class
(Reason: We will probably need two of them in the sat::solver)
* Bugfix
* init solve_eqs
* working on solve_eqs
* Update .gitignore
* wip - converting the equation solver as a simplifier
* make visited_helper independent of literals
re-introduce shorthands in sat::solver for visited and have them convert literals to unsigned.
* build fix
* move model and proof converters to self-contained module
* Create solve_eqs2_tactic.h
* add converters module to python build
* move tactic_params to params
* move more converters
* move horn_subsume_model_converter to ast/converters
* add initial stubs for model reconstruction trail
* fixing build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixes#6439#6436
* It's compiling (However, two important functions are commented out)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* 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.
* Use int64 for ocaml api functions that require it
Signed-off-by: Stefan Muenzel <source@s.muenzel.net>
* Use elif
Signed-off-by: Stefan Muenzel <source@s.muenzel.net>
