Kirill A. Korinsky
203941b8e8
It uses C++20 BTW
2024-10-20 20:53:59 +02:00
Nikolaj Bjorner
a23a8cdfc5
add variables from definitions
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-16 19:08:33 -07:00
Nikolaj Bjorner
92376e67f2
better model replay for loose entries
2024-10-16 13:07:18 -07:00
Nikolaj Bjorner
5a5e39ae74
fix incrementality bug for pre-processing: replay has to be invoked on every push regardless.
2024-10-16 13:07:18 -07:00
stormckey
8ff4036f68
update unit_lim to the correct value ( #7423 )
...
Co-authored-by: stormckey <chenhaogao123@gmail.com>
2024-10-16 10:23:13 -07:00
stormckey
3896e18227
fix the code to cube at the correct frequency ( #7422 )
...
Co-authored-by: stormckey <chenhaogao123@gmail.com>
2024-10-15 08:56:35 -07:00
Nikolaj Bjorner
5993735b34
simplify string patterns into prefix/suffix constraints
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-14 14:32:39 -07:00
Nikolaj Bjorner
62478db7d5
Update docker-image.yml
...
make docker publish manual
2024-10-13 19:50:56 -07:00
Nikolaj Bjorner
56b706ac55
fixes for #7420 #7405
2024-10-13 15:52:13 -07:00
Nikolaj Bjorner
3a8195b9c3
#7419
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-12 11:48:37 -07:00
Nikolaj Bjorner
7a0b58bcd5
increment minor version number
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-10 17:27:07 -07:00
Nikolaj Bjorner
efde656036
fix recursive self call for slice_solver check-sat-cc method
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-10 16:38:00 -07:00
Nikolaj Bjorner
54d30f26f7
add _0 to platform tag for pypi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-10 15:52:10 -07:00
Nikolaj Bjorner
6e3b99fb9e
downgrade to macos13 in builds until fully supported by pypi
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-10 14:19:23 -07:00
Nikolaj Bjorner
b268b56519
update release notes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-10 10:34:31 -07:00
Nikolaj Bjorner
00f1f1b83d
fix typo in setup.py
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-09 14:19:10 -07:00
Nikolaj Bjorner
fe71b75ffd
remove : from setup.py
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-09 13:21:27 -07:00
Nikolaj Bjorner
5dc1b1acd4
remove hard-wired osx=11.0
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-09 13:01:27 -07:00
Nikolaj Bjorner
48aa2f6988
setup python dist to remove internal build suffix for macos
2024-10-09 12:47:17 -07:00
Nikolaj Bjorner
da614c65e5
remove m_level attribute, use s->get_scope_level directly
2024-10-08 19:56:57 -07:00
Nikolaj Bjorner
6bd46b0922
fix #7363 . Replay relevancy on unit literals that are re-asserted during backtracking.
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-08 19:40:37 -07:00
Nikolaj Bjorner
cfd00ad672
add slice solver option to command context
2024-10-08 09:24:52 -07:00
Nikolaj Bjorner
8a95dd4d65
A slice solver option for interactive use case
...
A slice solver prunes the set of active assertions based on symbol occurrences in a goal that is tracked as a @query.
Ground assertions that have symbols intersecting with the query are included in the solver state, and quantifiers that with patterns that intersect with the slice are included. The slice is the fixedpoint of including symbols from all included assertions.
Enable the functionality for command-line use by setting solver.slice=true
2024-10-08 09:24:52 -07:00
Nikolaj Bjorner
0fec7efc7b
micro-tuning
2024-10-08 09:24:52 -07:00
Nikolaj Bjorner
c6cd25c822
mico-tuning
2024-10-08 09:24:52 -07:00
Peli de Halleux
24d7b05c0d
refactor and optimize git operations for commit messages and failure analysis ( #7412 )
2024-10-04 16:55:00 -07:00
Nikolaj Bjorner
2ae4ac8d0a
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-04 08:38:52 -07:00
Nikolaj Bjorner
b60e1a2ed2
fixup variables
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-03 20:06:45 -07:00
Nikolaj Bjorner
969511ac00
fixup std-order / inv-order
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-03 19:35:16 -07:00
Nikolaj Bjorner
66bb310966
reset before manager is deallocated
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-03 18:19:14 -07:00
Nikolaj Bjorner
a98c925069
optimize var_subst
2024-10-03 18:14:47 -07:00
Nikolaj Bjorner
f5db6bf92b
install Julia for macos build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-03 12:48:15 -07:00
Nikolaj Bjorner
e58eb9f302
fix indentation for mbp
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-03 12:47:12 -07:00
Nuno Lopes
3586b613f7
remove default destructors
2024-10-02 22:20:12 +01:00
Nikolaj Bjorner
b170f10148
reorder template definition
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-02 13:41:02 -07:00
dependabot[bot]
6dec943b29
Bump docker/build-push-action from 6.7.0 to 6.9.0 ( #7408 )
...
Bumps [docker/build-push-action](https://github.com/docker/build-push-action ) from 6.7.0 to 6.9.0.
- [Release notes](https://github.com/docker/build-push-action/releases )
- [Commits](https://github.com/docker/build-push-action/compare/v6.7.0...v6.9.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>
2024-10-02 13:23:39 -07:00
Nikolaj Bjorner
d686e92bfa
disambiguate
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-02 10:45:16 -07:00
Nikolaj Bjorner
93ff89bf98
add == for const_ref and ref to disambiguate equality.
2024-10-02 10:45:16 -07:00
Nikolaj Bjorner
c7af97364a
fixes for #7402
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-10-01 15:15:47 -07:00
Nikolaj Bjorner
328616b8b2
fix build warnings
2024-09-30 17:25:19 -07:00
Nikolaj Bjorner
8c39863019
fix typo in arch for setup.py
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-09-30 16:17:40 -07:00
Nikolaj Bjorner
4cefc513eb
add sequoia to os versions #7407
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-09-30 16:05:53 -07:00
Nikolaj Bjorner
19f63cd6e3
add sequoia to os versions #7407
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-09-30 15:57:49 -07:00
Nikolaj Bjorner
86b97186b0
fix build warnings
2024-09-30 15:51:48 -07:00
Nikolaj Bjorner
551cc53a2f
fix un-intialized variable warnings
2024-09-30 15:08:33 -07:00
Nikolaj Bjorner
2c94a3a1b3
fix build warnings
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-09-30 13:09:01 -07:00
Nikolaj Bjorner
7da58b9e84
fix build warnings
2024-09-30 10:34:26 -07:00
Nikolaj Bjorner
30b4fe69e4
2nd attempt to use uniform java library location under bin #7406
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-09-30 10:05:09 -07:00
Nikolaj Bjorner
b65afd41ed
attempt to use uniform java library location under bin #7406
2024-09-30 08:58:21 -07:00
Nikolaj Bjorner
5413018d86
Update euf_ac_plugin.cpp
2024-09-30 08:43:17 -07:00
