3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 01:54:08 +00:00
Commit graph

18202 commits

Author SHA1 Message Date
Nikolaj Bjorner 77dab53e9e track number of Gomory cuts 2023-11-07 19:57:49 +01:00
Nikolaj Bjorner 2d1f4d5d93 remove verbose logging 2023-11-07 19:57:49 +01:00
Nikolaj Bjorner e86eae27e6 #6523 and other heap-use-after-free error 2023-11-07 19:57:49 +01:00
Nikolaj Bjorner eed02b6d86 improved logging, use C++11 for loops instead of iterators 2023-11-07 19:57:49 +01:00
Lev Nachmanson 14312ef8a3 remove some warnings with clang
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-11-02 15:34:41 -07:00
Lev Nachmanson 08d3a82ce0 simplify the jump on entering 2023-11-02 11:09:01 -07:00
Lev Nachmanson bdf1fcf5c1 remove an assert 2023-11-02 09:59:03 -07:00
Lev Nachmanson ca6cb0af95 add changes in lp with validate_bound and maximize_term
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-11-02 09:59:03 -07:00
AE1020 ebd4d1a300
WARNINGS_AS_ERRORS is ON/OFF, not TRUE/FALSE (#6979) 2023-11-02 10:58:09 +01:00
Nikolaj Bjorner 49a071988c remove temporary algebraic numbers from upper layers, move to owner module 2023-11-01 03:52:20 -07:00
Nikolaj Bjorner ea915e5b37 #6971
clear m_a1, m_a2 before calls that may affect model.
2023-11-01 03:36:01 -07:00
Christoph M. Wintersteiger 3af2b36cd7
Add Z3_solver_interrupt to OCaml API (#6976) 2023-10-31 08:48:06 -07:00
Nikolaj Bjorner 91c2139b5d just use std::string
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-30 17:56:44 -07:00
Nikolaj Bjorner fe6f38a160 #6951, fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-30 15:31:56 -07:00
Nikolaj Bjorner c82b7dd241 Merge branch 'master' of https://github.com/z3prover/z3 2023-10-30 14:54:11 -07:00
Nikolaj Bjorner f97dd34028 tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-30 14:54:04 -07:00
Clemens Eisenhofer 996b844cde
Fixed parsing of | and \ (#6975)
* Give users ability to see if propagation failed

* Skip propagations in the new core if they are already satisfied

* Fix registration in final

* Don't make it too complicated...

* Fixed next_split when called in pop
Made delay_units available even without quantifiers

* Missing push calls before "decide"-callback

* Fixed parsing of | and \

* Unit-test for parsing bug
2023-10-30 12:30:23 -07:00
Nikolaj Bjorner 938a89e197 prepare for local version of Gomory cuts
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-29 19:45:14 -07:00
Nikolaj Bjorner 160971df60 fix #6969, again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-29 19:10:46 -07:00
Nikolaj Bjorner a957a5673d remove experiment with theory lemmas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-29 18:48:48 -07:00
Nikolaj Bjorner 3726960969 fix #6969
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-29 17:44:00 -07:00
Nikolaj Bjorner 589024aa1c fix #6969
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-29 17:44:00 -07:00
Christoph M. Wintersteiger 9d57bdd2ef
Assorted fixes for floats (#6968)
* Improve 4be26eb543

* Add-on to 0f4f32c5d0

* Fix mk_numeral

* Fix corner-case in fp.div

* Fixes for corner-cases in mk_to_fp_(un)signed

* Fix out-of-range results in mpf_manager::fma

* Further adjustments for fp.to_fp_(un)signed

* fp.to_fp from real can't be NaN

* fp.to_fp from reals: add bounds

* Fix NaN encodings in theory_fpa.

* Fix fp.fma rounding with tiny floats

* Fix literal creation order in theory_fpa
2023-10-29 17:29:42 -07:00
Nikolaj Bjorner bd8e5eee4b add simplification experiment (disabled) for tracking, some reshuffling of equation/fixed_equation structs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-29 10:21:31 -07:00
Clemens Eisenhofer e7c17e68b8
Fixed next_split call in pop (#6966)
* Give users ability to see if propagation failed

* Skip propagations in the new core if they are already satisfied

* Fix registration in final

* Don't make it too complicated...

* Fixed next_split when called in pop
Made delay_units available even without quantifiers

* Missing push calls before "decide"-callback
2023-10-28 12:46:43 -07:00
Nikolaj Bjorner 52d16a11f9 deal with non-termination in new arithmetic solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-27 16:15:36 -07:00
Nikolaj Bjorner f6c9ead10c #6964
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-27 13:17:20 -07:00
Nikolaj Bjorner 93427f1175 regression test 2447
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-26 08:48:58 -07:00
Nikolaj Bjorner 0b8d7b755d useful string rewrites
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-26 03:48:50 -07:00
Nikolaj Bjorner 5622fd1362 initialize delay bound
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-26 03:26:41 -07:00
Nikolaj Bjorner 76f9e1d2b3 fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-25 17:31:19 -07:00
Nikolaj Bjorner 702744f139 fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-25 16:57:31 -07:00
Nikolaj Bjorner 4434cee5df merge 2023-10-25 16:38:18 -07:00
Nikolaj Bjorner 20c54048f7 use cone of influence reduction before calling nlsat. 2023-10-25 16:19:23 -07:00
Nikolaj Bjorner e2db2b864b add hook for in-processing simplification for NLA
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-25 15:09:21 -07:00
Nikolaj Bjorner 6ba151599e Merge branch 'master' of https://github.com/z3prover/z3 2023-10-25 13:15:26 -07:00
Nikolaj Bjorner 55775bdc20 incremnet log level for debug output on cancelation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-25 13:15:15 -07:00
Bruce Mitchener 236afeb8cb
docs: More intra-doc linking, bit of formatting. (#6963) 2023-10-25 10:07:03 -07:00
Nikolaj Bjorner 7b490543ca add missing simplification; handle nit #6952
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-25 10:00:15 -07:00
Nikolaj Bjorner 0859be5649 #6953
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-25 09:07:04 -07:00
rsetaluri d5fe4b0d78
Update script to use importlib_resources (#6949)
To avoid a deprecation warning, this change updates scripts/update_api.py
to use 'importlib_resources' instead of 'pkg_resources'.

See https://setuptools.pypa.io/en/latest/pkg_resources.html and
https://importlib-resources.readthedocs.io/en/latest/migration.html for
more information.
2023-10-24 13:19:44 -07:00
dependabot[bot] f07c46a396
Bump actions/setup-node from 3 to 4 (#6961)
Bumps [actions/setup-node](https://github.com/actions/setup-node) from 3 to 4.
- [Release notes](https://github.com/actions/setup-node/releases)
- [Commits](https://github.com/actions/setup-node/compare/v3...v4)

---
updated-dependencies:
- dependency-name: actions/setup-node
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
2023-10-24 09:24:29 +01:00
dependabot[bot] 8b04049069
Bump @babel/traverse from 7.19.4 to 7.23.2 in /src/api/js (#6954)
Bumps [@babel/traverse](https://github.com/babel/babel/tree/HEAD/packages/babel-traverse) from 7.19.4 to 7.23.2.
- [Release notes](https://github.com/babel/babel/releases)
- [Changelog](https://github.com/babel/babel/blob/main/CHANGELOG.md)
- [Commits](https://github.com/babel/babel/commits/v7.23.2/packages/babel-traverse)

---
updated-dependencies:
- dependency-name: "@babel/traverse"
  dependency-type: indirect
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
2023-10-23 15:29:42 -07:00
itehax aa703160ce
Update README.md (#6960) 2023-10-23 15:28:02 -07:00
Nikolaj Bjorner 8fac89cdcc enable more simplification in case inequality triggers a change. 2023-10-21 19:58:39 -07:00
Nikolaj Bjorner 4e21e126a8 update add_lemmas to use check-feasible 2023-10-21 19:58:07 -07:00
Nikolaj Bjorner c9d298e57f enable propagate-linear-equations and extend to monomials 2023-10-21 19:57:41 -07:00
Nikolaj Bjorner 53ce18ef34 update backoff for bounded_nla 2023-10-21 19:57:06 -07:00
Nikolaj Bjorner 97058b0d5d allow for propagations the trigger make-feasible check 2023-10-19 16:08:44 -07:00
Nikolaj Bjorner 8c00181815 fix #6955 2023-10-19 10:41:24 -07:00