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

Change Download Binary URL for ubuntu-20.04 #1

Open
wants to merge 10 commits into
base: master
Choose a base branch
from
Open

Change Download Binary URL for ubuntu-20.04 #1

Show file tree
Hide file tree
Changes from 9 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
00377c9
add ubuntu-20.04 CI
niiyama-kota Sep 21, 2023
749917e
empty commit
niiyama-kota Sep 21, 2023
5406bbb
change build.rs for ubuntu-20.04
niiyama-kota Sep 21, 2023
b89bc71
empty commit
niiyama-kota Sep 21, 2023
02b3c5e
apply format
niiyama-kota Sep 21, 2023
cbf8b20
change downloaded z3 version 4.12.2
niiyama-kota Sep 26, 2023
c344339
Merge branch 'master' of github.com:niiyama-kota/z3.rs
niiyama-kota Sep 26, 2023
9786998
update submodule to the latest of master
niiyama-kota Oct 3, 2023
8ce3931
fix z3-sys/tests smoke_test()
niiyama-kota Oct 18, 2023
697427e
remove debug print
niiyama-kota Oct 19, 2023
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
4 changes: 2 additions & 2 deletions .github/workflows/rust.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ jobs:
strategy:
fail-fast: false
matrix:
os: [ubuntu-latest, windows-latest, macos-latest]
os: [ubuntu-latest, ubuntu-20.04, windows-latest, macos-latest]
link: [download, build, system]
runs-on: ${{ matrix.os }}
steps:
Expand All @@ -45,7 +45,7 @@ jobs:
choco install vcredist2017
echo "LIBCLANG_PATH=$((gcm clang).source -replace "clang.exe")" >> $env:GITHUB_ENV
- name: Uninstall Z3 on Linux for non-system builds
if: runner.os == 'Linux' && matrix.link != 'system'
if: (matrix.os == 'ubuntu-latest' || matrix.os == 'ubuntu-20.04') && matrix.link != 'system'
run: sudo apt-get remove libz3-dev
- name: Setup homebrew (macOS)
if: runner.os == 'macOS' && matrix.link == 'system'
Expand Down
41 changes: 29 additions & 12 deletions z3-sys/build.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -198,6 +198,7 @@ fn download_z3() -> Option<String> {
.map_err(|e| e.to_string())?;
if sha256 != "PASS" {
let hash = Sha256::digest(&buf);
println!("{:?}", format!("{:x}", hash));
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(ミーティングディスカッション) デバッグ用なので消したほうがよさそう

if format!("{:x}", hash) != sha256 {
return Err("Hash check failed".to_string());
}
Expand All @@ -207,37 +208,53 @@ fn download_z3() -> Option<String> {

fn get_archive_url() -> Option<(String, String)> {
if cfg!(target_os = "linux") && cfg!(target_arch = "x86_64") {
Some((
"https://github.com/Z3Prover/z3/releases/download/z3-4.12.1/z3-4.12.1-x64-glibc-2.35.zip".into(),
"c5360fd157b0f861ec8780ba3e51e2197e9486798dc93cd878df69a4b0c2b7c5".into(),
))
let output = std::process::Command::new("ldd")
.arg("--version")
.output()
.expect("Failed to run ldd");

let output_str = String::from_utf8_lossy(&output.stdout);
if output_str.contains("2.31") {
Some((
"https://github.com/Z3Prover/z3/releases/download/z3-4.12.2/z3-4.12.2-x64-glibc-2.31.zip".into(),
"a198851a7403d8b25bab920bd4a4792efe1af5c28a5a932d840af0472d3a83eb".into(),
))
} else if output_str.contains("2.35") {
Some((
"https://github.com/Z3Prover/z3/releases/download/z3-4.12.2/z3-4.12.2-x64-glibc-2.35.zip".into(),
"29604c87d74855690f5f43fa2ecb8e214af89bdddffac378ce403e29c6ea30ec".into(),
))
} else {
println!("{:?}", output_str);
panic!()
}
} else if cfg!(target_os = "macos") && cfg!(target_arch = "x86_64") {
Some((
"https://github.com/Z3Prover/z3/releases/download/z3-4.12.1/z3-4.12.1-x64-osx-10.16.zip".into(),
"7601f844de6d906235140d0f76cca58be7ac716f3e2c29c35845aa24b24f73b9".into(),
"https://github.com/Z3Prover/z3/releases/download/z3-4.12.2/z3-4.12.2-x64-osx-10.16.zip".into(),
"7f5ed527c022683d663108cdd00a2c89f43ae231b26fe7baf8b0b89bbf7d2aa7".into(),
))
} else if cfg!(target_os = "macos") && cfg!(target_arch = "aarch64") {
Some((
"https://github.com/Z3Prover/z3/releases/download/z3-4.12.1/z3-4.12.1-arm64-osx-11.0.zip".into(),
"91664cb7c10279e533f7ec568d63e0d04ada352217a6710655d41739c4ea1fc8".into(),
"https://github.com/Z3Prover/z3/releases/download/z3-4.12.2/z3-4.12.2-arm64-osx-11.0.zip".into(),
"2509f1a5250c70679347b3878b980a42640cd0b603bc87716f991d078b5a5959".into(),
))
} else if cfg!(target_os = "windows")
&& cfg!(target_arch = "x86_64")
&& cfg!(target_env = "msvc")
{
Some((
"https://github.com/Z3Prover/z3/releases/download/z3-4.12.1/z3-4.12.1-x64-win.zip"
"https://github.com/Z3Prover/z3/releases/download/z3-4.12.2/z3-4.12.2-x64-win.zip"
.into(),
"ce2d658d007c4f5873d2279bd031d4e72500b388e1ef2d716bd5f86af19b20d2".into(),
"ea33132e4531dbdc2c98b5f3c01257ca2f954e0f9c9115e63ea4e2530550e1d4".into(),
))
} else if cfg!(target_os = "windows")
&& cfg!(target_arch = "x86")
&& cfg!(target_env = "msvc")
{
Some((
"https://github.com/Z3Prover/z3/releases/download/z3-4.12.1/z3-4.12.1-x86-win.zip"
"https://github.com/Z3Prover/z3/releases/download/z3-4.12.2/z3-4.12.2-x86-win.zip"
.into(),
"1fbe8e2a87f42ca6f3348b8c48a1ffcd8fc376ac3144c9b588a5452de01ca2ef".into(),
"39c5f72eb7fcb4cdf6d5019fb22d13b40efc1c90cfc36c7f92adc9d1774091bd".into(),
))
} else {
None
Expand Down
19 changes: 14 additions & 5 deletions z3-sys/tests/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,16 @@ fn smoketest() {

let const_x = Z3_mk_const(ctx, sym_x, int_sort);
let const_y = Z3_mk_const(ctx, sym_y, int_sort);
let gt = Z3_mk_gt(ctx, const_x, const_y);
let const_zero = Z3_mk_int(ctx, 0, int_sort);
let gt = Z3_mk_and(
ctx,
2,
[
Z3_mk_gt(ctx, const_x, const_y),
Z3_mk_gt(ctx, const_y, const_zero),
]
.as_ptr(),
);

let solver = Z3_mk_simple_solver(ctx);
Z3_solver_assert(ctx, solver, gt);
Expand All @@ -33,8 +42,8 @@ fn smoketest() {
let model_str = CStr::from_ptr(model_s).to_str().unwrap();
let model_elements = model_str.split_terminator('\n').collect::<Vec<_>>();
assert_eq!(model_elements.len(), 2);
assert!(model_elements.contains(&"y -> (- 1)"));
assert!(model_elements.contains(&"x -> 0"));
assert!(model_elements.contains(&"y -> 1"));
assert!(model_elements.contains(&"x -> 2"));

// Grab the actual constant values out of the model
let mut interp_x: Z3_ast = const_x;
Expand All @@ -46,8 +55,8 @@ fn smoketest() {
let mut val_y: i32 = -5;
assert!(Z3_get_numeral_int(ctx, interp_x, &mut val_x));
assert!(Z3_get_numeral_int(ctx, interp_y, &mut val_y));
assert_eq!(val_x, 0);
assert_eq!(val_y, -1);
assert_eq!(val_x, 2);
assert_eq!(val_y, 1);

Z3_del_context(ctx);
Z3_del_config(cfg);
Expand Down
2 changes: 1 addition & 1 deletion z3-sys/z3
Open in desktop
Submodule z3 updated 655 files