Nikolaj Bjorner
|
e7d083304b
|
Update pyodide.yml
|
2024-11-15 19:29:28 -08:00 |
|
|
Nikolaj Bjorner
|
bd5f8b17d6
|
Update pyodide.yml
|
2024-11-15 19:26:24 -08:00 |
|
|
Nikolaj Bjorner
|
751d666e16
|
Update pyodide.yml
|
2024-11-15 19:16:54 -08:00 |
|
|
Nikolaj Bjorner
|
24f9a86539
|
Update pyodide.yml
|
2024-11-15 18:49:51 -08:00 |
|
|
Nikolaj Bjorner
|
dba167472e
|
Update pyodide.yml
|
2024-11-15 18:43:51 -08:00 |
|
|
Nikolaj Bjorner
|
704278caa9
|
Update pyodide.yml
|
2024-11-15 18:40:17 -08:00 |
|
|
Nikolaj Bjorner
|
231248d610
|
Update pyodide.yml
|
2024-11-15 18:36:13 -08:00 |
|
|
Nikolaj Bjorner
|
329e1ddb10
|
Update pyodide.yml
|
2024-11-15 18:30:41 -08:00 |
|
|
Nikolaj Bjorner
|
aab6c1e909
|
Update pyodide.yml
Add flags from src\api\js\scripts\build-wasm.ts
|
2024-11-15 16:57:11 -08:00 |
|
|
Nikolaj Bjorner
|
ccbe6c33ae
|
fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-11-15 09:29:30 -08:00 |
|
|
Nikolaj Bjorner
|
88048901f0
|
Update pyodide.yml
|
2024-11-15 08:45:51 -08:00 |
|
|
Nikolaj Bjorner
|
ea590def47
|
remove breaking experiment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-11-15 08:03:57 -08:00 |
|
|
Nikolaj Bjorner
|
1d8a904e99
|
build fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-11-14 22:10:59 -08:00 |
|
|
Nikolaj Bjorner
|
77eacef2ae
|
build fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-11-14 22:08:13 -08:00 |
|
|
Nikolaj Bjorner
|
3f407982f3
|
build fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-11-14 21:55:44 -08:00 |
|
|
Nikolaj Bjorner
|
ca6ec0d9e4
|
fixes to pyodide action
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-11-14 21:45:47 -08:00 |
|
|
Nikolaj Bjorner
|
8e3b9f6686
|
add sequential option for SLS, fixes to import/export methods SLS<->SMT
|
2024-11-14 21:43:40 -08:00 |
|
|
Nikolaj Bjorner
|
6a9d5910cb
|
add method for resetting limit
|
2024-11-14 21:43:40 -08:00 |
|
|
Nikolaj Bjorner
|
6eae3f0863
|
add cases for unconstrained sequences and strings
|
2024-11-14 21:43:40 -08:00 |
|
|
Nikolaj Bjorner
|
62db7642ec
|
refine rewriting depth for lt constraints
|
2024-11-14 21:43:40 -08:00 |
|
Audrey Dutcher
|
3fed840233
|
update pyodide.yml
|
2024-11-14 22:15:57 -07:00 |
|
|
Nikolaj Bjorner
|
eab49da274
|
Update pyodide.yml
switch to ubuntu 24
|
2024-11-14 20:49:33 -08:00 |
|
|
Nikolaj Bjorner
|
75d0dd891b
|
Update pyodide.yml
fix typo emv -> env
|
2024-11-14 20:12:30 -08:00 |
|
|
Nikolaj Bjorner
|
e53ea005a0
|
Update pyodide.yml
|
2024-11-14 19:26:03 -08:00 |
|
|
Nikolaj Bjorner
|
4cdc3d6b1a
|
Update pyodide.yml
|
2024-11-14 18:59:53 -08:00 |
|
|
Nikolaj Bjorner
|
4d0394e33f
|
Update pyodide.yml
trying to understand paths
|
2024-11-14 18:54:23 -08:00 |
|
|
Nikolaj Bjorner
|
0dc4c5e58b
|
Create pyodide.yml
|
2024-11-14 18:47:43 -08:00 |
|
Linus
|
d3009dabfc
|
Proposed fix for #7451 (#7452)
|
2024-11-13 09:11:40 -08:00 |
|
|
Nikolaj Bjorner
|
c0e748a51a
|
fix #7446, by adding rewrite simplification
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-11-11 19:16:11 -08:00 |
|
|
Nikolaj Bjorner
|
1cc808c58d
|
fix #7446, by adding rewrite simplification
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-11-11 19:08:11 -08:00 |
|
|
Nikolaj Bjorner
|
30ad22a4ef
|
fix #7449
|
2024-11-11 15:45:18 -08:00 |
|
|
Nikolaj Bjorner
|
879bb4b1f0
|
avoid circular dependencies in justifications that get updated. fixes #7443
|
2024-11-10 19:35:01 -08:00 |
|
|
Nikolaj Bjorner
|
1856ab72d9
|
fix #7448
|
2024-11-10 14:40:28 -08:00 |
|
|
Nikolaj Bjorner
|
4f060dd2b1
|
fix #7445
|
2024-11-10 14:40:04 -08:00 |
|
|
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
|
42894f729a
|
add noexcept for signature compatibility
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-11-04 11:13:49 -08:00 |
|
|
Audrey Dutcher
|
75e46778fa
|
Make build process work with pyodide (#7442)
|
2024-11-04 11:09:51 -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
|
1957b4d991
|
fix reporting on cancelation when based on cancel flag
|
2024-11-02 12:48:12 -07:00 |
|
Jonas Jongejan
|
604714ba40
|
js: Add pseudo-boolean high-level functions (#7426)
* js: Add pseudo-boolean high-level functions
* Add check for arg length
|
2024-11-02 12:34:15 -07: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 |
|
|
Nikolaj Bjorner
|
ecdfab81a6
|
fix #7434
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-10-28 17:51:01 -07:00 |
|
|
Nikolaj Bjorner
|
b0fef6429f
|
Add assert_and_track support to Optimize class in .NET binding (#7437)
Related to #7436
#7436
---
For more details, open the [Copilot Workspace session](https://copilot-workspace.githubnext.com/Z3Prover/z3/issues/7436?shareId=XXXX-XXXX-XXXX-XXXX).
|
2024-10-26 01:33:09 -07:00 |
|
|
Nikolaj Bjorner
|
8b657f27aa
|
add shortcut to retrieve kind of application
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-10-22 13:05:58 -07:00 |
|
|
Nikolaj Bjorner
|
78d1139ba0
|
add shortcut to retrieve kind of application
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-10-22 13:04:41 -07:00 |
|
|
Nikolaj Bjorner
|
0ebea1c298
|
remove debug out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2024-10-22 11:58:16 -07:00 |
|
|
Nikolaj Bjorner
|
253f7d7675
|
fix non-termination bug in elim-unconstrained, add parameter validation to fix #7432
|
2024-10-22 09:59:20 -07:00 |
|
|
Nikolaj Bjorner
|
d18831c8d5
|
Update sat_ddfw.cpp
|
2024-10-22 09:59:20 -07:00 |
|