Nikolaj Bjorner
abd16740ce
inherit more exceptions from std::exception
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-04 13:52:14 -08:00
Nikolaj Bjorner
a38bf3e22f
port to inherit from std::exception
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-04 13:25:14 -08:00
Nikolaj Bjorner
407bad3693
add noexcept
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-04 11:21:55 -08:00
Nikolaj Bjorner
92065462b4
use std::exception as base class to z3_exception
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-11-04 11:08:15 -08:00
Nikolaj Bjorner
91dc02d862
Sls ( #7439 )
...
* reorg sls
* sls
* na
* split into base and plugin
* move sat_params to params directory, add op_def repair options
* move sat_ddfw to sls, initiate sls-bv-plugin
* porting bv-sls
* adding basic plugin
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add sls-sms solver
* bv updates
* updated dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* updated dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use portable ptr-initializer
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* move definitions to cpp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use template<> syntax
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix compiler errors for gcc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Bump docker/build-push-action from 6.0.0 to 6.1.0 (#7265 )
Bumps [docker/build-push-action](https://github.com/docker/build-push-action ) from 6.0.0 to 6.1.0.
- [Release notes](https://github.com/docker/build-push-action/releases )
- [Commits](https://github.com/docker/build-push-action/compare/v6.0.0...v6.1.0 )
---
updated-dependencies:
- dependency-name: docker/build-push-action
dependency-type: direct:production
update-type: version-update:semver-minor
...
Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
* set clean shutdown for local search and re-enable local search when it parallelizes with PB solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Bump docker/build-push-action from 6.1.0 to 6.2.0 (#7269 )
Bumps [docker/build-push-action](https://github.com/docker/build-push-action ) from 6.1.0 to 6.2.0.
- [Release notes](https://github.com/docker/build-push-action/releases )
- [Commits](https://github.com/docker/build-push-action/compare/v6.1.0...v6.2.0 )
---
updated-dependencies:
- dependency-name: docker/build-push-action
dependency-type: direct:production
update-type: version-update:semver-minor
...
Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
* Fix a comment for Z3_solver_from_string (#7271 )
Z3_solver_from_string accepts a string buffer with solver
assertions, not a string buffer with filename.
* trigger the build with a comment change
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* remove macro distinction #7270
* fix #7268
* kludge to address #7232 , probably superseeded by planned revision to setup/pypi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add new ema invariant (#7288 )
* Bump docker/build-push-action from 6.2.0 to 6.3.0 (#7280 )
Bumps [docker/build-push-action](https://github.com/docker/build-push-action ) from 6.2.0 to 6.3.0.
- [Release notes](https://github.com/docker/build-push-action/releases )
- [Commits](https://github.com/docker/build-push-action/compare/v6.2.0...v6.3.0 )
---
updated-dependencies:
- dependency-name: docker/build-push-action
dependency-type: direct:production
update-type: version-update:semver-minor
...
Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
* merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix unit test build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove shared attribute
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove stale files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix build of unit test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixes and rename sls-cc to sls-euf-plugin
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* testing / debugging arithmetic
* updates to repair logic, mainly arithmetic
* fixes to sls
* evolve sls arith
* bugfixes in sls-arith
* fix typo
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* bug fixes
* Update sls_test.cpp
* fixes
* fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* refactor basic plugin and clause generation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixes to ite and other
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* updates
* update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix division by 0
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* disable fail restart
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* disable tabu when using reset moves
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* update sls_test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add factoring
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixes to semantics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* re-add tabu override
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* generalize factoring
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix bug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove restart
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* disable tabu in fallback modes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* localize impact of factoring
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* delay factoring
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* flatten products
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* perform lookahead update + nested mul
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* disable nested mul
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* disable nested mul, use non-lookahead
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* make reset updates recursive
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* include linear moves
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* include 5% reset probability
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* separate linear update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* separate linear update remove 20% threshold
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove linear opt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* enable multiplier expansion, enable linear move
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use unit coefficients for muls
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* disable non-tabu version of find_nl_moves
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove coefficient from multiplication definition
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* reorg monomials
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add smt params to path
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* avoid negative reward
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use reward as proxy for score
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use reward as proxy for score
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use exponential decay with breaks
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use std::pow
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixes to bv
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixes to fixed
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixup repairs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* reserve for multiplication
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixing repair
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* include bounds checks in set random
* na
* fixes to mul
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix mul inverse
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixes to handling signed operators
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* logging and fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* gcm
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* peli
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Add .env to gitignore to prevent environment files from being tracked
* Add m_num_pelis counter to stats in sls_context
* Remove m_num_pelis member from stats struct in sls_context
* Enhance bv_sls_eval with improved repair and logging, refine is_bv_predicate in sls_bv_plugin
* Remove verbose logging in register_term function of sls_basic_plugin and fix formatting in sls_context
* Rename source files for consistency in `src/ast/sls` directory
* Refactor bv_sls files to sls_bv with namespace and class name adjustments
* Remove typename from member declarations in bv_fixed class
* fixing conca
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Add initial implementation of bit-vector SLS evaluation module in bv_sls_eval.cpp
* Remove bv_sls_eval.cpp as part of code cleanup and refactoring
* Refactor alignment of member variables in bv_plugin of sls namespace
* Rename SLS engine related files to reflect their specific use for bit-vectors
* Refactor SLS engine and evaluator components for bit-vector specifics and adjust memory manager alignment
* Enhance bv_eval with use_current, lookahead strategies, and randomization improvements in SLS module
* Refactor verbose logging and fix logic in range adjustment functions in sls bv modules
* Remove commented verbose output in sls_bv_plugin.cpp during repair process
* Add early return after setting fixed subterms in sls_bv_fixed.cpp
* Remove redundant return statement in sls_bv_fixed.cpp
* fixes to new value propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Refactor sls bv evaluation and fix logic checks for bit operations
* Add array plugin support and update bv_eval in ast_sls module
* Add array, model value, and user sort plugins to SLS module with enhancements in array propagation logic
* Refactor array_plugin in sls to improve handling of select expressions with multiple arguments
* Enhance array plugin with early termination and propagation verification, and improve euf and user sort plugins with propagation adjustments and debugging enhancements
* Add support for handling 'distinct' expressions in SLS context and user sort plugin
* Remove model value and user sort plugins from SLS theory
* replace user plugin by euf plugin
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove extra file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Refactor handling of term registration and enhance distinct handling in sls_euf_plugin
* Add TODO list for enhancements in sls_euf_plugin.cpp
* add incremental mode
* updated package
* fix sls build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* break sls build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix build
* break build again
* fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixing incremental
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* avoid units
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixup handling of disequality propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fx
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* recover shift-weight loop
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* alternate
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* throttle save model
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* allow for alternating
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix test for new signature of flip
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* bug fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* restore use of value_hash
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* adding dt plugin
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* adt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* dt updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* added cycle detection
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* updated sls-datatype
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Refactor context management, improve datatype handling, and enhance logging in sls plugins.
* axiomatize dt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add missing factory plugins to model
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixup finite domain search
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixup finite domain search
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* redo dfs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixing model construction for underspecified operators
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixes to occurs check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixup interpretation building
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* saturate worklist
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* delay distinct axiom
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* adding model-based sls for datatatypes
* update the interface in sls_solver to transfer phase between SAT and SLS
* add value transfer option
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* rename aux functions
* Track shared variables using a unit set
* debugging parallel integration
* fix dirty flag setting
* update log level
* add plugin to smt_context, factor out sls_smt_plugin functionality.
* bug fixes
* fixes
* use common infrastructure for sls-smt
* fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove declaration of context
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add virtual destructor
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* build warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* reorder inclusion order to define smt_context before theory_sls
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* change namespace for single threaded
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* check delayed eqs before nla
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use independent completion flag for sls to avoid conflating with genuine cancelation
* validate sls-arith lemmas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* bugfixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add intblast to legacy SMT solver
* fixup model generation for theory_intblast
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* mk_value needs to accept more cases where integer expression doesn't evalate
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use th-axioms to track origins of assertions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add missing operator handling for bitwise operators
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add missing operator handling for bitwise operators
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* normalizing inequality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add virtual destructor
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* rework elim_unconstrained
* fix non-termination
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use glue as computed without adjustment
* update model generation to fix model bug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fixes to model construction
* remove package and package lock
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix build warning
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* use original gai
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Signed-off-by: dependabot[bot] <support@github.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Co-authored-by: Sergey Bronnikov <estetus@gmail.com>
Co-authored-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: LiviaSun <33578456+ChuyueSun@users.noreply.github.com>
2024-11-02 12:32:48 -07:00
Nuno Lopes
3586b613f7
remove default destructors
2024-10-02 22:20:12 +01:00
Nikolaj Bjorner
826835fd7c
fixes to build warnings
2024-09-30 08:23:31 -07:00
Nikolaj Bjorner
11bb19d99b
make default tactic cases lazy
2024-09-27 15:11:43 +01:00
Nikolaj Bjorner
40b0210dda
fixes to lazy tactic uses
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-09-27 14:33:09 +01:00
Nikolaj Bjorner
01cf0427b4
fix #7404 , relates to #7400 .
2024-09-27 11:36:10 +01:00
Nikolaj Bjorner
5a6dc18d0d
Override convert_initialize_value method in bit_blaster_model_converter.cpp
2024-09-23 13:46:50 +01:00
Nuno Lopes
737c2208fa
delete more default constructors
...
reduces code size by 0.1%
2024-09-23 12:59:04 +01:00
Nuno Lopes
a62fede64b
remove a few default constructors
2024-09-23 08:17:58 +01:00
Nikolaj Bjorner
a9f8ec1bcb
updated handling of value initialization for bit-vectors
2024-09-22 21:30:11 +03:00
Nikolaj Bjorner
0c48a50d59
Add support for initializing variable values in solver and optimize contexts in Z3
2024-09-20 18:28:26 +03:00
Nikolaj Bjorner
a3f35b6830
Add command to set initial value hints for solver in various components
2024-09-18 17:48:03 +03:00
Nikolaj Bjorner
48712b4f60
Add initial value setting for variables in Z3 API, solver, and optimize modules
2024-09-18 16:13:15 +03:00
Nuno Lopes
8061765574
remove default destructors & some default constructors
...
Another ~700 KB reduction in binary size
2024-09-04 22:30:23 +01:00
Nikolaj Bjorner
6a68cc55bb
#7353 - clear pointer when existing stack
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-08-26 09:59:56 -07:00
Lev Nachmanson
bf34600f08
add release nodes and add the author reference in qfnra_tactic
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2024-08-12 08:49:55 -10:00
Lev Nachmanson
752c999e0a
cleanup
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2024-08-11 12:45:36 -10:00
Lev Nachmanson
1a5bddb4f0
port more from hybridSMT
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2024-08-11 12:45:36 -10:00
Nikolaj Bjorner
26b8d634a3
add max conflict throttle to SAT based QFNIA tactic #7329
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-08-03 11:34:28 -07:00
Nikolaj Bjorner
974ea7b68d
maintain ownership of dependency
2024-04-10 17:57:14 -07:00
Nikolaj Bjorner
bab7ca2b70
fixes to bv-sls
2024-04-07 14:24:13 -07:00
Nikolaj Bjorner
51f1e2655c
updates to sls
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-03-30 12:59:05 -07:00
Nikolaj Bjorner
b8a69987c3
fix #7165
2024-03-17 16:33:40 -07:00
Nikolaj Bjorner
22616da63b
updates
2024-03-05 12:28:31 -08:00
Nikolaj Bjorner
4391c90960
na
2024-03-05 12:28:30 -08:00
Nikolaj Bjorner
f39756c74b
initial stab at new bv-sls based on repair actions
2024-03-05 12:28:29 -08:00
Bruce Mitchener
53f89a81c1
Fix some typos. ( #7115 )
2024-02-07 23:06:43 -08:00
Nikolaj Bjorner
e321643bf5
move sls core functionality to be independent of tactic
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-12-22 12:00:52 -08:00
Nikolaj Bjorner
924c296704
add logging
2023-11-18 12:30:40 -08:00
Nikolaj Bjorner
8fac89cdcc
enable more simplification in case inequality triggers a change.
2023-10-21 19:58:39 -07:00
Nikolaj Bjorner
33c35b0c31
fix #6851
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-13 14:49:25 -07:00
Nikolaj Bjorner
3d8f75b3d8
enable on-clause with dependencies
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-07-18 16:59:02 -07:00
Clemens Eisenhofer
4cb158a79b
User Propagator: Return if propagated lemma is redundant ( #6791 )
...
* Give users ability to see if propagation failed
* Skip propagations in the new core if they are already satisfied
2023-07-07 09:58:41 -07:00
Clemens Eisenhofer
82667bd86b
Fix UP's decide callback ( #6707 )
...
* Query Boolean Assignment in the UP
* UP's decide ref arguments => next_split
* Fixed wrapper
* More fixes
2023-06-02 09:52:54 +02:00
Nikolaj Bjorner
b783879752
#6687
2023-04-13 08:45:17 -07:00
Nikolaj Bjorner
fe348b84c9
fix #6652
2023-03-27 16:20:33 -07:00
Nikolaj Bjorner
adec937296
fix #6650
2023-03-27 14:02:23 -07:00
Nikolaj Bjorner
f366772f0c
use field 'm' for streamlined representation
2023-03-27 14:02:22 -07:00
Nikolaj Bjorner
9ca0faa091
enable interactive example
2023-03-25 18:13:44 +01:00
Nikolaj Bjorner
d1c7ff1a36
add unconstrained elimination for sequences
2023-03-20 17:07:04 +01:00
Nikolaj Bjorner
e87fa1c299
remove stale file
2023-02-28 17:40:08 -08:00
Nikolaj Bjorner
102eee77dc
patch regressions
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-12 20:12:01 -08:00
Nikolaj Bjorner
cac5052685
fixes related to #6577
...
- enforce elim-and in bool-rewriter when invoking hoisting.
- make cnf tactic more resilient to non-normalized input.
- enable eliminate predicates on ground formulas
2023-02-12 13:43:44 -08:00
Nikolaj Bjorner
46c8d78ece
fixes for #6577
...
- the literal false should not appear in clauses
- the literal true forces a tautology
- fix early return in is_cnf check. It should check all clauses for nested Booleans.
2023-02-11 09:33:42 -08:00
Nikolaj Bjorner
e6f8fe359e
remove empty file
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-31 12:32:28 -08:00
Nikolaj Bjorner
d263b373ed
update release notes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-31 12:19:33 -08:00