mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-27 09:49:23 +00:00
Code Activity
18836 commits 45 branches 52 tags 177 MiB
Commit graph

18836 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
11ab583232 fix #6956 2023-10-19 10:34:31 -07:00
Nikolaj Bjorner
37fe9cc764 add Horner saturation to Grobner conflict detection 
- throttle Grobner
- add (disabled) propagate_linear_equation to prepare for additional propagation.
- add validation code is_nla_conflict/add_nla_conflict to establish missed conflicts
 2023-10-17 21:19:57 -07:00
Nikolaj Bjorner
0a1cc4c054 fix exception safety in pdd-solver 2023-10-17 19:50:34 -07:00
Nikolaj Bjorner
3fa67777e5 fix exception safety in pdd-solver 2023-10-17 19:50:13 -07:00
Nikolaj Bjorner
c9c5dbc347 #6523 2023-10-16 09:27:22 -07:00
Nikolaj Bjorner
f678861aef fix #6947 2023-10-16 08:43:08 -07:00
Nikolaj Bjorner
ba881d9c9b add facility to experiment with nla justified conflicts from Grobner equations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-16 00:40:43 -07:00
Nikolaj Bjorner
18fc6914d3 add facility to experiment with nla justified conflicts from Grobner equations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-16 00:40:24 -07:00
Nikolaj Bjorner
bdac86501d add facility to check for missing propagations 2023-10-15 20:33:48 -07:00
Nikolaj Bjorner
cafe3acff1 delay detach 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-15 12:41:34 -07:00
Nikolaj Bjorner
891ab8bac5 #6523 
fixup looping
 2023-10-15 12:37:14 -07:00
Nikolaj Bjorner
6553382ec8 remove extra assume-eqs 2023-10-15 12:30:24 -07:00
Nikolaj Bjorner
b2efa592ce #6523 
deal with memory leak on exceptions
 2023-10-15 12:17:08 -07:00
Nikolaj Bjorner
41b1f47d77 #6523 
deal with memory leak when there is an exception
 2023-10-15 12:15:28 -07:00
Nikolaj Bjorner
5942dc24bd #6523 2023-10-15 11:41:25 -07:00
Nikolaj Bjorner
5619ed0586 resurrect old bounds propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-14 13:55:56 -07:00