Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update base Z3 to v4.13.0 #133

Merged
merged 851 commits into from
Apr 23, 2024
Merged

Update base Z3 to v4.13.0 #133

Changes from 1 commit
Commits
Show all changes
851 commits
Select commit Hold shift + click to select a range
c4fa719
revert last two commits; MSVC doesn't like to statically allocate fle…
nunoplopes Dec 20, 2023
4317d13
refactor: move gomory functionaly from int_solver to gomory
levnach Dec 20, 2023
a00eb08
Merge branch 'master' of https://github.com/z3prover/z3
levnach Dec 20, 2023
e9fa7db
revert smt_enode
levnach Dec 21, 2023
19f3ad4
fix the build
levnach Dec 21, 2023
68a2c08
Add Z3_get_estimated_alloc_size to OCaml API (#7068)
wintersteiger Dec 21, 2023
b09c237
rudimentary bin cover solver using the user propagator
NikolajBjorner Dec 21, 2023
ae1d927
improve add bin/item functions
NikolajBjorner Dec 21, 2023
766f5f0
reduce memory allocs in params
nunoplopes Dec 21, 2023
4fe4234
bugfix on slack
NikolajBjorner Dec 21, 2023
ab22e76
some code simplifications in mpn
nunoplopes Dec 22, 2023
cab3c45
remove unnecessary parameter copies
nunoplopes Dec 22, 2023
606a9a7
fix test build
nunoplopes Dec 22, 2023
e321643
move sls core functionality to be independent of tactic
NikolajBjorner Dec 22, 2023
5f45118
missing cmake list
NikolajBjorner Dec 22, 2023
7adb402
add missing dependencies
NikolajBjorner Dec 22, 2023
cd331b8
remove reference to tactic.h
NikolajBjorner Dec 22, 2023
ad07e0e
add sub and super-slice functionality directory to euf-bv-plugin
NikolajBjorner Dec 23, 2023
ebe5ebf
Add branch and bound solver, for fun
NikolajBjorner Dec 23, 2023
d7931b9
Bump microsoft/setup-msbuild from 1.1 to 1.3 (#7071)
dependabot[bot] Dec 26, 2023
af76912
adding the polarity bound
levnach Dec 24, 2023
a3529a0
create bounds for gomory cuts with big numbers
levnach Dec 24, 2023
5796e88
use vector instead of unordered_map in gomory
levnach Dec 24, 2023
0728b81
add parameter lp_settings.m_gomory_simplify
levnach Dec 27, 2023
53c95e3
cleanup
levnach Dec 28, 2023
ec2b8eb
Merge shared parts from polysat branch (#7063)
JakobR Dec 28, 2023
d66df26
Fix some typos. (#7075)
waywardmonkeys Dec 29, 2023
fd2b6c6
bug fix in gomory polarity
levnach Jan 1, 2024
84997f8
move a TRACE statement
levnach Jan 1, 2024
a7bfdcd
readd big cuts
NikolajBjorner Jan 2, 2024
b75367f
port improvements to arith rewriter
NikolajBjorner Jan 3, 2024
239d68e
return conflict on an empty term in Gomory cuts
levnach Jan 4, 2024
696b70f
fix
NikolajBjorner Jan 4, 2024
2934618
remove simplify_inequality from gomory.cpp
levnach Jan 4, 2024
75005d9
add validation option for debugging regressions
NikolajBjorner Jan 9, 2024
2ca1187
fix a bug in polarity
levnach Jan 10, 2024
955c80e
import updates from poly branch
NikolajBjorner Jan 11, 2024
aa4e1b3
update Julia versions
NikolajBjorner Jan 11, 2024
b239371
try to remove version spec
NikolajBjorner Jan 11, 2024
1b39290
try to remove version spec
NikolajBjorner Jan 11, 2024
2ac866a
take the coefficient from cut_result, not lia
levnach Jan 11, 2024
2b974a0
do not delay update for the polar case
levnach Jan 11, 2024
2d24436
remove a blank line
levnach Jan 11, 2024
999e67d
address Nikolaj's comments in Gomory cut
levnach Jan 12, 2024
59b18d4
create as_bin as_hex wrappers for display
NikolajBjorner Jan 12, 2024
2717159
Update sat_params.pyg
NikolajBjorner Jan 12, 2024
3381fd2
spell check from https://github.com/microsoft/z3guide/pull/165
NikolajBjorner Jan 12, 2024
ddf2eb5
deleted parameter
NikolajBjorner Jan 12, 2024
7d7fef0
add explanations and fix polarity
levnach Jan 13, 2024
2eadcf0
avoid duplicate explanations
levnach Jan 13, 2024
e2fb4fb
fix dependencies for Gomory polarity
levnach Jan 14, 2024
d8df203
remove an unused declaration
levnach Jan 14, 2024
91ca55e
change the definition of Gomory row
levnach Jan 14, 2024
4ff352f
fix #7084
NikolajBjorner Jan 15, 2024
afba43a
fix #7085
NikolajBjorner Jan 16, 2024
c340233
fix #7081
NikolajBjorner Jan 16, 2024
4f75153
Update z3_api.h
NikolajBjorner Jan 17, 2024
fef1596
pin expression passed to validate_eq
NikolajBjorner Jan 17, 2024
c591a7a
force int bound on int columns, call term_is_int() after subst
levnach Jan 17, 2024
6e9a938
Merge branch 'master' of https://github.com/z3prover/z3
levnach Jan 18, 2024
d084a19
take care of strategy undecided, Nikolaj's comments
levnach Jan 18, 2024
2c55aa5
remove unused code
NikolajBjorner Jan 18, 2024
d2706ba
Fixes in Java's User Propagator (#7088)
ThomasHaas Jan 18, 2024
a2993f7
encapsulate mpz a bit more
NikolajBjorner Jan 20, 2024
548be4c
add explicit move constructor to deal with unit test regression test-…
NikolajBjorner Jan 20, 2024
1754523
encapsulate anum functionality
NikolajBjorner Jan 20, 2024
d32dcfc
free memory the clean way
NikolajBjorner Jan 20, 2024
910b302
free memory the clean way
NikolajBjorner Jan 20, 2024
2dd45f8
add Windows build
NikolajBjorner Jan 21, 2024
e722dc7
add status badge for windows build, remove windows build from Azure p…
NikolajBjorner Jan 21, 2024
302ebff
prepare for release
NikolajBjorner Jan 21, 2024
7486e87
track quantifier instantiation method in proof hint #7080
NikolajBjorner Jan 21, 2024
a7b564c
update release scripts and notes
NikolajBjorner Jan 21, 2024
414c33f
Bump mymindstorm/setup-emsdk from 13 to 14 (#7095)
dependabot[bot] Jan 22, 2024
69f118e
use assignment
NikolajBjorner Jan 18, 2024
0ebd8d6
prepare for printing more cases of root objects in SMT
NikolajBjorner Jan 22, 2024
839b710
add ability to multiply term
NikolajBjorner Jan 22, 2024
8d4e7fa
add diagnostics option to new arithmetic solver
NikolajBjorner Jan 23, 2024
125a82b
improved diagnostics
NikolajBjorner Jan 23, 2024
be7856c
fix #7027
NikolajBjorner Jan 23, 2024
36453c5
use while (true) in do loops with continue
NikolajBjorner Jan 23, 2024
98c9fa7
prepare for handling integer intervals
NikolajBjorner Jan 23, 2024
fad4283
prepare for integer intervals
NikolajBjorner Jan 23, 2024
1b94d43
fix build
NikolajBjorner Jan 24, 2024
1335466
update minor version number
NikolajBjorner Jan 24, 2024
bdb9106
Api (#7097)
NikolajBjorner Jan 25, 2024
ee2be7d
attempting to build ARM
NikolajBjorner Jan 25, 2024
9d59d86
update cmake build
NikolajBjorner Jan 25, 2024
dec5715
Expose forall and exists to Julia (#7099)
remysucre Jan 25, 2024
637ffcd
Update mk_win_dist_cmake.py
NikolajBjorner Jan 25, 2024
c8c2e3a
update java install/build
NikolajBjorner Jan 25, 2024
527f824
update java install/build
NikolajBjorner Jan 25, 2024
2af1cff
updating java cmake scrip
NikolajBjorner Jan 28, 2024
f8a3b6f
fix #7102
NikolajBjorner Jan 28, 2024
2b68394
fix #7103
NikolajBjorner Jan 28, 2024
908aaa0
fix #7101
NikolajBjorner Jan 29, 2024
4be8b7d
update win-dist
NikolajBjorner Jan 30, 2024
bef67f8
special purpose dotnet copy
NikolajBjorner Jan 30, 2024
f7ed4ad
update path for win distributions
NikolajBjorner Jan 30, 2024
9bd8e35
adapt paths to new distribution
NikolajBjorner Jan 30, 2024
b3b95db
move installation directories to under bin
NikolajBjorner Jan 30, 2024
680b0f5
add download stage for arm64
NikolajBjorner Jan 30, 2024
e0bed3b
build Julia for x64
NikolajBjorner Jan 30, 2024
5d4303f
build Julia for x64
NikolajBjorner Jan 30, 2024
f811801
remove optional Julia build
NikolajBjorner Jan 30, 2024
67e5ba9
update release scripts
NikolajBjorner Jan 30, 2024
28c44a6
fix #7105
NikolajBjorner Jan 30, 2024
99ebbd6
porting unix distribution script to cmake
NikolajBjorner Jan 31, 2024
50deece
fix #7098
NikolajBjorner Jan 31, 2024
738c5b6
add warning messages for #7100
NikolajBjorner Jan 31, 2024
ac1f971
move nightly builds of Unixes to use cmake
NikolajBjorner Jan 31, 2024
4b4e057
install ninja
NikolajBjorner Jan 31, 2024
d3fbb9d
add line continuations to nightly.yaml
NikolajBjorner Jan 31, 2024
5c4ad4f
cd to dist in nightly.yaml
NikolajBjorner Jan 31, 2024
5551f1e
update nightly
NikolajBjorner Jan 31, 2024
e26344e
update nightly
NikolajBjorner Jan 31, 2024
e820701
fix #7107
NikolajBjorner Jan 31, 2024
9a095cc
Update nightly.yaml for Azure Pipelines
NikolajBjorner Feb 1, 2024
f16afe5
Update nightly.yaml for Azure Pipelines
NikolajBjorner Feb 1, 2024
0a1a57c
Update nightly.yaml for Azure Pipelines
NikolajBjorner Feb 1, 2024
d624eec
Update nightly.yaml
NikolajBjorner Feb 1, 2024
432432b
update ubuntu builds
NikolajBjorner Feb 1, 2024
8507297
update ubuntu builds
NikolajBjorner Feb 1, 2024
ec6640d
Update nightly.yaml
NikolajBjorner Feb 1, 2024
ca0e9a1
remove explicit option for shared build, set to Release mode. .so art…
NikolajBjorner Feb 1, 2024
5cac9b8
fix build warnings
NikolajBjorner Feb 1, 2024
28d62bf
move to use release.yml version for windows build
NikolajBjorner Feb 1, 2024
06466be
disable arm64 nightly
NikolajBjorner Feb 2, 2024
bd2d96e
update folder names to align with mk_win_dist_cmake
NikolajBjorner Feb 2, 2024
77b98d5
update folder names to align with mk_win_dist_cmake
NikolajBjorner Feb 2, 2024
93cbcd0
rename
NikolajBjorner Feb 2, 2024
d231913
remove period
NikolajBjorner Feb 2, 2024
30c14f5
include variable ReleaseVersion in Nightly
NikolajBjorner Feb 2, 2024
4260206
include variable ReleaseVersion in Nightly
NikolajBjorner Feb 2, 2024
0d24ec3
add 'dist' to folder path
NikolajBjorner Feb 2, 2024
2280e95
Improve instructions for working with the Julia API (#7108)
remysucre Feb 2, 2024
9db834c
add back legacy build-win-signed
NikolajBjorner Feb 2, 2024
485a018
add back legacy build-win-signed
NikolajBjorner Feb 2, 2024
05d625b
fixing paths and re-add arm64
NikolajBjorner Feb 2, 2024
cfc8774
move windows builds to use mk_win_dist_cmake in nightly
NikolajBjorner Feb 2, 2024
736d634
move windows builds to use mk_win_dist_cmake in nightly
NikolajBjorner Feb 2, 2024
14fb235
update mk-win-dist-cmake
NikolajBjorner Feb 3, 2024
bd082ab
update mk-win-dist-cmake
NikolajBjorner Feb 3, 2024
e398f84
update build-win-signed-cmake
NikolajBjorner Feb 3, 2024
e295ac9
update build-win-signed-cmake
NikolajBjorner Feb 3, 2024
24ffef8
fix typo
NikolajBjorner Feb 3, 2024
a5a819c
port updates to egraph from poly
NikolajBjorner Feb 3, 2024
9425c41
port remaining egraph update
NikolajBjorner Feb 3, 2024
bc70282
mute some compiler warnings
NikolajBjorner Feb 3, 2024
b9bec18
copy over dotnet files
NikolajBjorner Feb 4, 2024
c926705
update assembly names
NikolajBjorner Feb 4, 2024
a2fa4ff
update assembly names
NikolajBjorner Feb 4, 2024
3b90816
add option to persist clauses #7109
NikolajBjorner Feb 4, 2024
3cec3fc
bypass replaying new clause within propagation
NikolajBjorner Feb 4, 2024
7970e4f
add clause persistence to sat/smt solver
NikolajBjorner Feb 5, 2024
548b9d0
move libz3.so from lib to bin, remove lib from distribution
NikolajBjorner Feb 5, 2024
b9528b1
update self-validator to handle root expressions
NikolajBjorner Feb 5, 2024
d743e1b
add note that the encoding is a first approximation
NikolajBjorner Feb 5, 2024
446a9de
distinguish vs-arch from arch identifier
NikolajBjorner Feb 5, 2024
f4474a3
typo
NikolajBjorner Feb 5, 2024
8555f25
add todo note, and log more lemmas
NikolajBjorner Feb 5, 2024
683070a
finish encoding of n'th root
NikolajBjorner Feb 5, 2024
f4eaa6f
improve logging
NikolajBjorner Feb 5, 2024
c40e72a
include debug output
NikolajBjorner Feb 5, 2024
937d4aa
move files from lib and java directory to bin
NikolajBjorner Feb 6, 2024
53f89a8
Fix some typos. (#7115)
waywardmonkeys Feb 8, 2024
f1d97c7
allow callbacks to be nested
NikolajBjorner Feb 13, 2024
4d06c39
replace DEBUG_CODE by #ifdef Z3DEBUG in nlsat
levnach Feb 13, 2024
dba2f78
ci: Update `microsoft/setup-msbuild` to `v2` from `v1.3`. (#7119)
waywardmonkeys Feb 14, 2024
155dfb1
Fix some typos in identifiers. (#7118)
waywardmonkeys Feb 14, 2024
2b14793
#7117
NikolajBjorner Feb 14, 2024
84d592c
fix #7121
NikolajBjorner Feb 16, 2024
199ef30
conditionally depend on importlib_resources (#7116)
cj81499 Feb 18, 2024
f7691d3
fix generic example
NikolajBjorner Feb 21, 2024
a3d00ce
Improved Java phantom references (#7131)
ThomasHaas Feb 21, 2024
79b7d8a
throttle squash-store #7134
NikolajBjorner Feb 21, 2024
785f71b
prepare for 12.6
NikolajBjorner Feb 22, 2024
143a35d
Fix typos. (#7137)
waywardmonkeys Feb 22, 2024
c0621cb
ci: Stop using deprecated `::set-output`. (#7136)
waywardmonkeys Feb 22, 2024
019c064
Update coverage.yml
NikolajBjorner Feb 22, 2024
19f5e7f
ci: Really fix set-output. (#7138)
waywardmonkeys Feb 22, 2024
85425a6
Update nightly.yaml for Azure Pipelines (#7139)
jfleisher Feb 24, 2024
fa2c0e0
enable release publish
NikolajBjorner Feb 24, 2024
c67200e
update versions
NikolajBjorner Feb 26, 2024
2880ea3
convert formatting tabs to spaces (#7140)
jfleisher Feb 26, 2024
91886da
some code cleaning and complexity improvements (#7133)
zapashcanon Feb 29, 2024
57c20be
fix #7143: type punning in test
nunoplopes Mar 4, 2024
4050a43
Add arm64 for linux python wheels to nightly (#7145)
smoy Mar 5, 2024
77a07bb
detect arm64 for manylinux setup
NikolajBjorner Mar 5, 2024
7694bca
For many linux build, use aarch64 instead of arm64 (#7147)
smoy Mar 5, 2024
1068708
Revert "For many linux build, use aarch64 instead of arm64 (#7147)" (…
NikolajBjorner Mar 5, 2024
f39756c
initial stab at new bv-sls based on repair actions
NikolajBjorner Feb 13, 2024
bd323d6
save
NikolajBjorner Feb 13, 2024
1cf008d
updates
NikolajBjorner Feb 14, 2024
ddf2d28
add tests for evaluation
NikolajBjorner Feb 16, 2024
388b2f5
n/a
NikolajBjorner Feb 16, 2024
046db66
na
NikolajBjorner Feb 18, 2024
9915378
fixes based on unit tests
NikolajBjorner Feb 19, 2024
4391c90
na
NikolajBjorner Feb 19, 2024
7dc4ce8
use tuned gcd to compute mult inverse
NikolajBjorner Feb 20, 2024
ab0459e
bugfixes
NikolajBjorner Feb 20, 2024
d7e419b
fixes and checks
NikolajBjorner Feb 20, 2024
9cde4f7
bugfixes
NikolajBjorner Feb 21, 2024
cd6382f
fix alias bug
NikolajBjorner Feb 21, 2024
659e384
bugfixes
NikolajBjorner Feb 21, 2024
cf72a91
bugfixes, adding plugin solver
NikolajBjorner Feb 21, 2024
b14499f
prepare for sls experiment
NikolajBjorner Feb 22, 2024
5379fab
include thread
NikolajBjorner Feb 22, 2024
cfa6bd4
update python build dependencies
NikolajBjorner Feb 22, 2024
acc9c21
move to hide bits
NikolajBjorner Feb 22, 2024
48026ed
move to hide bits
NikolajBjorner Feb 22, 2024
74e73f2
reorg to use datatypes
NikolajBjorner Feb 23, 2024
63804c5
na
NikolajBjorner Feb 23, 2024
c451e4e
na
NikolajBjorner Feb 23, 2024
8f85df0
fb
NikolajBjorner Feb 23, 2024
a328366
move to single path mode for search
NikolajBjorner Feb 24, 2024
0e5b504
remove bw setting
NikolajBjorner Feb 24, 2024
58474df
na
NikolajBjorner Feb 24, 2024
2590d67
na
NikolajBjorner Feb 26, 2024
8f139e8
updates to multiplication
NikolajBjorner Feb 26, 2024
d774f07
add eval field to sls-valuation to track temporary values.
NikolajBjorner Feb 26, 2024
f46c378
bugfixes
NikolajBjorner Feb 27, 2024
9888d87
na
NikolajBjorner Feb 27, 2024
5455603
na
NikolajBjorner Feb 28, 2024
803f0f0
na
NikolajBjorner Feb 28, 2024
dfd5c27
na
NikolajBjorner Feb 29, 2024
5be8872
na
NikolajBjorner Feb 29, 2024
22616da
updates
NikolajBjorner Mar 1, 2024
8679c08
fix test
NikolajBjorner Mar 1, 2024
657aaf9
na
NikolajBjorner Mar 2, 2024
531bda3
fix alias bug
NikolajBjorner Mar 2, 2024
d6f522e
na
NikolajBjorner Mar 5, 2024
e8c8d8a
Put in workaround to rename manylinux_arm64 to manylinux_aarch64 (#7149)
smoy Mar 5, 2024
017367d
Handle cross compile within manylinux (#7150)
smoy Mar 6, 2024
aad8cbd
Add LinuxBuildsArm64 ci azure-pipelines for testing (#7152)
smoy Mar 6, 2024
620efbb
add aacrhc
NikolajBjorner Mar 6, 2024
364da19
remove test
NikolajBjorner Mar 6, 2024
e873664
Downgrade arm cross compile toolchain to glibc 2.34 (#7153)
smoy Mar 7, 2024
7b7084d
Add LinuxBuildsArm64 to python wheels in release (#7155)
smoy Mar 7, 2024
6254844
update release notes
NikolajBjorner Mar 7, 2024
f9ce332
update release notes
NikolajBjorner Mar 7, 2024
3049f57
add download of Arm64 to python packaging
NikolajBjorner Mar 7, 2024
9c54c84
Merge branch 'master' into new-new-z3
jurajsic Apr 10, 2024
19370da
update readmes
jurajsic Apr 10, 2024
c6e2868
try removing new rewriter rules
jurajsic Apr 11, 2024
22a91b7
Revert "try removing new rewriter rules"
jurajsic Apr 11, 2024
3524a85
replace: equivalent
vhavlena Apr 12, 2024
76ef5ef
update readme
jurajsic Apr 12, 2024
3233733
commment one rewriter rule
jurajsic Apr 18, 2024
ec4ce36
update pubs in readme
jurajsic Apr 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
ci: Stop using deprecated ::set-output. (Z3Prover#7136) 
This has been deprecated and the replacement functionality is
described here:

https://github.blog/changelog/2022-10-11-github-actions-deprecating-save-state-and-set-output-commands/
  • Loading branch information
@waywardmonkeys
waywardmonkeys authored Feb 22, 2024
commit c0621cb760f50278ec4fdd8ae5f2ca0b83276b14
1 change: 1 addition & 0 deletions .github/workflows/coverage.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -90,6 +90,7 @@ jobs:
- name: Get date
id: date
run: echo "::set-output name=date::$(date +'%Y-%m-%d')"
run: echo "date=$(date +'%Y-%m-%d')" >> $GITHUB_OUTPUT

- uses: actions/upload-artifact@v4
with:
Expand Down