From 5e124cefd31f9f67640144ef7e7db8bbb7dbc944 Mon Sep 17 00:00:00 2001 From: Benedikt Radtke Date: Tue, 10 May 2022 22:04:07 +0200 Subject: [PATCH] Use precompiled z3 libs by default --- .github/workflows/rust.yml | 92 ++++----- z3-sys/Cargo.toml | 8 +- z3-sys/build.rs | 200 +++++++++++++------ z3-sys/src/generated.rs | 2 +- z3-sys/src/generated/ast_kind.rs | 13 ++ z3-sys/src/generated/ast_print_mode.rs | 9 + z3-sys/src/generated/decl_kind.rs | 261 +++++++++++++++++++++++++ z3-sys/src/generated/error_code.rs | 19 ++ z3-sys/src/generated/goal_prec.rs | 10 + z3-sys/src/generated/param_kind.rs | 13 ++ z3-sys/src/generated/parameter_kind.rs | 13 ++ z3-sys/src/generated/sort_kind.rs | 20 ++ z3-sys/src/generated/symbol_kind.rs | 8 + z3/Cargo.toml | 7 +- 14 files changed, 552 insertions(+), 123 deletions(-) create mode 100644 z3-sys/src/generated/ast_kind.rs create mode 100644 z3-sys/src/generated/ast_print_mode.rs create mode 100644 z3-sys/src/generated/decl_kind.rs create mode 100644 z3-sys/src/generated/error_code.rs create mode 100644 z3-sys/src/generated/goal_prec.rs create mode 100644 z3-sys/src/generated/param_kind.rs create mode 100644 z3-sys/src/generated/parameter_kind.rs create mode 100644 z3-sys/src/generated/sort_kind.rs create mode 100644 z3-sys/src/generated/symbol_kind.rs diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index 4315c307..0a46e053 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -8,31 +8,50 @@ on: env: CARGO_INCREMENTAL: 0 - RUSTFLAGS: "-D warnings" + Z3_RELEASE: 'z3-4.8.12' + RUST_BACKTRACE: 'full' jobs: build: - runs-on: ubuntu-latest + strategy: + matrix: + os: [ubuntu-latest, windows-latest] + link: [default, static, system] + runs-on: ${{ matrix.os }} steps: - - uses: actions/checkout@v2 - - name: Install Z3 - run: sudo apt-get install libz3-dev - - name: Build - run: cargo build -vv --all - # XXX: Ubuntu's Z3 package seems to be missing some symbols, like - # `Z3_mk_pbeq`, leading to linker errors. Just ignore this, I guess, until - # we figure out how to work around it. At least we have the - # statically-linked Z3 tests below... - if: ${{ success() || failure() }} - - name: Run tests - run: cargo test -vv --all - # See above. - if: ${{ success() || failure() }} - - name: Run tests with `arbitrary-size-numeral` enabled - run: cargo test --manifest-path z3/Cargo.toml -vv --features arbitrary-size-numeral - # See above. - if: ${{ success() || failure() }} + - name: Checkout + uses: actions/checkout@v2 + if: ${{ matrix.link != 'static' }} + + - name: Checkout with submodules + uses: actions/checkout@v2 + if: ${{ matrix.link == 'static' }} + with: + submodules: recursive + + - name: Uninstall Z3 on Linux for non-system builds + if: ${{ matrix.os == 'ubuntu-latest' && matrix.link != 'system' }} + run: sudo apt-get remove libz3-dev + - name: Install Z3 on Windows for system builds + if: ${{ matrix.os == 'windows-latest' && matrix.link == 'system' }} + run: | + curl.exe -L "https://github.com/Z3Prover/z3/releases/download/${env:Z3_RELEASE}/${env:Z3_RELEASE}-x64-win.zip" -o "./${env:Z3_RELEASE}-x64-win.zip" + tar -xf "./${env:Z3_RELEASE}-x64-win.zip" + echo "${PWD}\${env:Z3_RELEASE}-x64-win\bin" >> $env:GITHUB_PATH + echo "LIB=${PWD}\${env:Z3_RELEASE}-x64-win\bin" >> $env:GITHUB_ENV + + - name: Test with Z3 releases + if: ${{ matrix.link == 'default' }} + run: cargo test --lib -vv + + - name: Test with Z3 system installation + if: ${{ matrix.link == 'system' }} + run: cargo test --lib -vv --features dynamic-link-z3 + + - name: Test with static Z3 builds + if: ${{ matrix.link == 'static' }} + run: cargo test --lib -vv --features static-link-z3 build_on_wasm: runs-on: ubuntu-latest steps: @@ -64,36 +83,3 @@ jobs: run: | source ~/emsdk/emsdk_env.sh cargo build --target=wasm32-unknown-emscripten --manifest-path z3/Cargo.toml -vv --features static-link-z3 - build_z3_statically: - strategy: - matrix: - build: [linux, macos, windows] - include: - - build: linux - os: ubuntu-latest - - build: macos - os: macos-latest - - build: windows - os: windows-latest - runs-on: ${{ matrix.os }} - steps: - - uses: actions/checkout@v2 - with: - submodules: recursive - - name: Install LLVM and Clang # required for bindgen to work, see https://github.com/rust-lang/rust-bindgen/issues/1797 - uses: KyleMayes/install-llvm-action@v1 - if: matrix.os == 'windows-latest' - with: - version: "11.0" - directory: ${{ runner.temp }}/llvm - - name: Set LIBCLANG_PATH - run: echo "LIBCLANG_PATH=$((gcm clang).source -replace "clang.exe")" >> $env:GITHUB_ENV - if: matrix.os == 'windows-latest' - - name: Build z3-sys with statically linked Z3 - run: cargo build --manifest-path z3-sys/Cargo.toml -vv --features static-link-z3 - - name: Build z3 with statically linked Z3 - run: cargo build --manifest-path z3/Cargo.toml -vv --features static-link-z3 - - name: Test `z3` with statically linked Z3 - run: cargo test --manifest-path z3/Cargo.toml -vv --features static-link-z3 - - name: Test `z3` with statically linked Z3 and `arbitrary-size-numeral` enabled - run: cargo test --manifest-path z3/Cargo.toml -vv --features 'static-link-z3 arbitrary-size-numeral' diff --git a/z3-sys/Cargo.toml b/z3-sys/Cargo.toml index 0984ca87..82200e73 100644 --- a/z3-sys/Cargo.toml +++ b/z3-sys/Cargo.toml @@ -16,10 +16,10 @@ homepage = "https://github.com/prove-rs/z3.rs" repository = "https://github.com/prove-rs/z3.rs.git" [build-dependencies] -bindgen = { version = "0.64.0", default-features = false, features = ["runtime"] } +bindgen = { version = "0.64.0", default-features = false, features = ["runtime"], optional = true } cmake = { version = "0.1.49", optional = true } [features] -# Enable this feature to statically link our own build of Z3, rather than -# dynamically linking to the system's `libz3.so`. -static-link-z3 = ["cmake"] +static-link-z3 = ["cmake"] # Locally build and statically link a fresh Z3 build. +use-bindgen = ["bindgen"] # Generate fresh bindings with bindgen. +dynamic-link-z3 = [] # Dynamically link the system's Z3 installation. diff --git a/z3-sys/build.rs b/z3-sys/build.rs index 18ab9edf..c21db923 100644 --- a/z3-sys/build.rs +++ b/z3-sys/build.rs @@ -1,57 +1,78 @@ -use std::env; - +#[cfg(feature = "use-bindgen")] const Z3_HEADER_VAR: &str = "Z3_SYS_Z3_HEADER"; -fn main() { - #[cfg(feature = "static-link-z3")] - build_z3(); +#[cfg(not(feature = "dynamic-link-z3"))] +#[cfg(not(feature = "static-link-z3"))] +const Z3_RELEASE: &str = "z3-4.8.12"; +#[cfg(target_os = "windows")] +const Z3_ARCH: &str = "x64-win"; +#[cfg(target_os = "linux")] +const Z3_ARCH: &str = "x64-glibc-2.31"; + +fn main() { println!("cargo:rerun-if-changed=build.rs"); + get_z3(); + #[cfg(feature = "use-bindgen")] + bindgen(); +} - let header = if cfg!(feature = "static-link-z3") { - "z3/src/api/z3.h".to_string() - } else if let Ok(header_path) = std::env::var(Z3_HEADER_VAR) { - header_path - } else { - "wrapper.h".to_string() - }; - println!("cargo:rerun-if-env-changed={}", Z3_HEADER_VAR); - println!("cargo:rerun-if-changed={}", header); - let out_path = std::path::PathBuf::from(std::env::var("OUT_DIR").unwrap()); +#[cfg(not(feature = "dynamic-link-z3"))] +#[cfg(not(feature = "static-link-z3"))] +/// Use precompiled Z3 binaries. +fn get_z3() { + let out_dir = std::path::PathBuf::from(std::env::var("OUT_DIR").unwrap()); + let archive_filename = format!("{}-{}", Z3_RELEASE, Z3_ARCH); + let archive_url = format!("https://github.com/Z3Prover/z3/releases/download/{}/{}.zip", Z3_RELEASE, archive_filename); + let archive_path = out_dir.join(format!("{}.zip", archive_filename)); + let release_folder = out_dir.join(archive_filename); - for x in &[ - "ast_kind", - "ast_print_mode", - "decl_kind", - "error_code", - "goal_prec", - "param_kind", - "parameter_kind", - "sort_kind", - "symbol_kind", - ] { - let mut enum_bindings = bindgen::Builder::default() - .header(&header) - .parse_callbacks(Box::new(bindgen::CargoCallbacks)) - .generate_comments(false) - .rustified_enum(format!("Z3_{}", x)) - .allowlist_type(format!("Z3_{}", x)); - if env::var("TARGET").unwrap() == "wasm32-unknown-emscripten" { - enum_bindings = enum_bindings.clang_arg(format!( - "--sysroot={}/upstream/emscripten/cache/sysroot", - env::var("EMSDK").expect("$EMSDK env var missing. Is emscripten installed?") - )); - } - enum_bindings - .generate() - .expect("Unable to generate bindings") - .write_to_file(out_path.join(format!("{}.rs", x))) - .expect("Couldn't write bindings!"); - } + let curl = std::process::Command::new("curl") + .arg("-L") + .arg("-o") + .arg(&archive_path.to_str().unwrap()) + .arg(&archive_url) + .spawn() + .unwrap() + .wait() + .unwrap(); + assert!(curl.success()); + + #[cfg(target_os = "windows")] + let tar = std::process::Command::new("tar") + .current_dir(archive_path.parent().unwrap()) + .arg("-x") + .arg("-f") + .arg(&archive_path.to_str().unwrap()) + .spawn() + .unwrap() + .wait() + .unwrap(); + + #[cfg(not(target_os = "windows"))] + let tar = std::process::Command::new("unzip") + .current_dir(archive_path.parent().unwrap()) + .arg(&archive_path.to_str().unwrap()) + .spawn() + .unwrap() + .wait() + .unwrap(); + assert!(tar.success()); + + // Add lib folder to the library search path. + println!("cargo:rustc-link-search=native={}/bin", &release_folder.to_str().unwrap()); } +#[cfg(feature = "dynamic-link-z3")] +#[cfg(not(feature = "static-link-z3"))] +/// Use the system's Z3 installation. +fn get_z3() {} + +#[cfg(not(feature = "dynamic-link-z3"))] #[cfg(feature = "static-link-z3")] -fn build_z3() { +#[cfg(not(target_os = "windows"))] +/// Build and link Z3 statically on Linux/MacOS +fn get_z3() { let mut cfg = cmake::Config::new("z3"); cfg // Don't build `libz3.so`, build `libz3.a` instead. @@ -61,16 +82,6 @@ fn build_z3() { // Don't build the tests. .define("Z3_BUILD_TEST_EXECUTABLES", "false"); - if cfg!(target_os = "windows") { - // The compiler option -MP and the msbuild option -m - // can sometimes make builds slower but is measurably - // faster building Z3 with many cores. - cfg.cxxflag("-MP"); - cfg.build_arg("-m"); - cfg.cxxflag("-DWIN32"); - cfg.cxxflag("-D_WINDOWS"); - } - let dst = cfg.build(); // Z3 needs a C++ standard library. Customize which one we use with the @@ -119,13 +130,80 @@ fn build_z3() { "Should have found the lib directory for our built Z3" ); - if cfg!(target_os = "windows") { - println!("cargo:rustc-link-lib=static=libz3"); - } else { - println!("cargo:rustc-link-lib=static=z3"); - } - if let Some(cxx) = cxx { println!("cargo:rustc-link-lib={}", cxx); } } + +#[cfg(not(feature = "dynamic-link-z3"))] +#[cfg(feature = "static-link-z3")] +#[cfg(target_os = "windows")] +/// Build and link Z3 statically on Windows +fn get_z3() { + let mut cfg = cmake::Config::new("z3"); + cfg + // Don't build `libz3.so`, build `libz3.a` instead. + .define("Z3_BUILD_LIBZ3_SHARED", "false") + // Don't build the Z3 repl. + .define("Z3_BUILD_EXECUTABLE", "false") + // Don't build the tests. + .define("Z3_BUILD_TEST_EXECUTABLES", "false"); + // The compiler option -MP and the msbuild option -m + // can sometimes make builds slower but is measurably + // faster building Z3 with many cores. + cfg.cxxflag("-MP"); + cfg.build_arg("-m"); + cfg.cxxflag("-DWIN32"); + cfg.cxxflag("-D_WINDOWS"); + + let dst = cfg.build(); + + // Add lib folder to the library search path. + println!("cargo:rustc-link-search=native={}/lib", dst.to_str().unwrap()); +} + +#[cfg(feature = "use-bindgen")] +fn bindgen() { + let header = if cfg!(feature = "static-link-z3") { + "z3/src/api/z3.h".to_string() + } else if let Ok(header_path) = std::env::var(Z3_HEADER_VAR) { + header_path + } else { + "wrapper.h".to_string() + }; + println!("cargo:rerun-if-env-changed={}", Z3_HEADER_VAR); + println!("cargo:rerun-if-changed={}", header); + let out_path = std::path::PathBuf::from("generated".unwrap()); + + for x in &[ + "ast_kind", + "ast_print_mode", + "decl_kind", + "error_code", + "goal_prec", + "param_kind", + "parameter_kind", + "sort_kind", + "symbol_kind", + ] { + let enum_bindings = bindgen::Builder::default() + .header(&header) + .parse_callbacks(Box::new(bindgen::CargoCallbacks)) + .generate_comments(false) + .rustified_enum(format!("Z3_{}", x)) + .allowlist_type(format!("Z3_{}", x)) + .generate() + .expect("Unable to generate bindings"); + + if env::var("TARGET").unwrap() == "wasm32-unknown-emscripten" { + enum_bindings = enum_bindings.clang_arg(format!( + "--sysroot={}/upstream/emscripten/cache/sysroot", + env::var("EMSDK").expect("$EMSDK env var missing. Is emscripten installed?") + )); + } + + enum_bindings + .write_to_file(out_path.join(format!("{}.rs", x))) + .expect("Couldn't write bindings!"); + } +} diff --git a/z3-sys/src/generated.rs b/z3-sys/src/generated.rs index e5ad8d04..388e7d79 100644 --- a/z3-sys/src/generated.rs +++ b/z3-sys/src/generated.rs @@ -7,7 +7,7 @@ macro_rules! declare_generated_mods { // code. #[allow(dead_code)] mod $mod_name { - include!(concat!(env!("OUT_DIR"), "/", stringify!($mod_name), ".rs")); + include!(concat!("generated", "/", stringify!($mod_name), ".rs")); } )* }; diff --git a/z3-sys/src/generated/ast_kind.rs b/z3-sys/src/generated/ast_kind.rs new file mode 100644 index 00000000..f8bddc76 --- /dev/null +++ b/z3-sys/src/generated/ast_kind.rs @@ -0,0 +1,13 @@ +/* automatically generated by rust-bindgen 0.59.2 */ + +#[repr(u32)] +#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)] +pub enum Z3_ast_kind { + Z3_NUMERAL_AST = 0, + Z3_APP_AST = 1, + Z3_VAR_AST = 2, + Z3_QUANTIFIER_AST = 3, + Z3_SORT_AST = 4, + Z3_FUNC_DECL_AST = 5, + Z3_UNKNOWN_AST = 1000, +} diff --git a/z3-sys/src/generated/ast_print_mode.rs b/z3-sys/src/generated/ast_print_mode.rs new file mode 100644 index 00000000..5e3d9d0e --- /dev/null +++ b/z3-sys/src/generated/ast_print_mode.rs @@ -0,0 +1,9 @@ +/* automatically generated by rust-bindgen 0.59.2 */ + +#[repr(u32)] +#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)] +pub enum Z3_ast_print_mode { + Z3_PRINT_SMTLIB_FULL = 0, + Z3_PRINT_LOW_LEVEL = 1, + Z3_PRINT_SMTLIB2_COMPLIANT = 2, +} diff --git a/z3-sys/src/generated/decl_kind.rs b/z3-sys/src/generated/decl_kind.rs new file mode 100644 index 00000000..422989fb --- /dev/null +++ b/z3-sys/src/generated/decl_kind.rs @@ -0,0 +1,261 @@ +/* automatically generated by rust-bindgen 0.59.2 */ + +#[repr(u32)] +#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)] +pub enum Z3_decl_kind { + Z3_OP_TRUE = 256, + Z3_OP_FALSE = 257, + Z3_OP_EQ = 258, + Z3_OP_DISTINCT = 259, + Z3_OP_ITE = 260, + Z3_OP_AND = 261, + Z3_OP_OR = 262, + Z3_OP_IFF = 263, + Z3_OP_XOR = 264, + Z3_OP_NOT = 265, + Z3_OP_IMPLIES = 266, + Z3_OP_OEQ = 267, + Z3_OP_ANUM = 512, + Z3_OP_AGNUM = 513, + Z3_OP_LE = 514, + Z3_OP_GE = 515, + Z3_OP_LT = 516, + Z3_OP_GT = 517, + Z3_OP_ADD = 518, + Z3_OP_SUB = 519, + Z3_OP_UMINUS = 520, + Z3_OP_MUL = 521, + Z3_OP_DIV = 522, + Z3_OP_IDIV = 523, + Z3_OP_REM = 524, + Z3_OP_MOD = 525, + Z3_OP_TO_REAL = 526, + Z3_OP_TO_INT = 527, + Z3_OP_IS_INT = 528, + Z3_OP_POWER = 529, + Z3_OP_STORE = 768, + Z3_OP_SELECT = 769, + Z3_OP_CONST_ARRAY = 770, + Z3_OP_ARRAY_MAP = 771, + Z3_OP_ARRAY_DEFAULT = 772, + Z3_OP_SET_UNION = 773, + Z3_OP_SET_INTERSECT = 774, + Z3_OP_SET_DIFFERENCE = 775, + Z3_OP_SET_COMPLEMENT = 776, + Z3_OP_SET_SUBSET = 777, + Z3_OP_AS_ARRAY = 778, + Z3_OP_ARRAY_EXT = 779, + Z3_OP_SET_HAS_SIZE = 780, + Z3_OP_SET_CARD = 781, + Z3_OP_BNUM = 1024, + Z3_OP_BIT1 = 1025, + Z3_OP_BIT0 = 1026, + Z3_OP_BNEG = 1027, + Z3_OP_BADD = 1028, + Z3_OP_BSUB = 1029, + Z3_OP_BMUL = 1030, + Z3_OP_BSDIV = 1031, + Z3_OP_BUDIV = 1032, + Z3_OP_BSREM = 1033, + Z3_OP_BUREM = 1034, + Z3_OP_BSMOD = 1035, + Z3_OP_BSDIV0 = 1036, + Z3_OP_BUDIV0 = 1037, + Z3_OP_BSREM0 = 1038, + Z3_OP_BUREM0 = 1039, + Z3_OP_BSMOD0 = 1040, + Z3_OP_ULEQ = 1041, + Z3_OP_SLEQ = 1042, + Z3_OP_UGEQ = 1043, + Z3_OP_SGEQ = 1044, + Z3_OP_ULT = 1045, + Z3_OP_SLT = 1046, + Z3_OP_UGT = 1047, + Z3_OP_SGT = 1048, + Z3_OP_BAND = 1049, + Z3_OP_BOR = 1050, + Z3_OP_BNOT = 1051, + Z3_OP_BXOR = 1052, + Z3_OP_BNAND = 1053, + Z3_OP_BNOR = 1054, + Z3_OP_BXNOR = 1055, + Z3_OP_CONCAT = 1056, + Z3_OP_SIGN_EXT = 1057, + Z3_OP_ZERO_EXT = 1058, + Z3_OP_EXTRACT = 1059, + Z3_OP_REPEAT = 1060, + Z3_OP_BREDOR = 1061, + Z3_OP_BREDAND = 1062, + Z3_OP_BCOMP = 1063, + Z3_OP_BSHL = 1064, + Z3_OP_BLSHR = 1065, + Z3_OP_BASHR = 1066, + Z3_OP_ROTATE_LEFT = 1067, + Z3_OP_ROTATE_RIGHT = 1068, + Z3_OP_EXT_ROTATE_LEFT = 1069, + Z3_OP_EXT_ROTATE_RIGHT = 1070, + Z3_OP_BIT2BOOL = 1071, + Z3_OP_INT2BV = 1072, + Z3_OP_BV2INT = 1073, + Z3_OP_CARRY = 1074, + Z3_OP_XOR3 = 1075, + Z3_OP_BSMUL_NO_OVFL = 1076, + Z3_OP_BUMUL_NO_OVFL = 1077, + Z3_OP_BSMUL_NO_UDFL = 1078, + Z3_OP_BSDIV_I = 1079, + Z3_OP_BUDIV_I = 1080, + Z3_OP_BSREM_I = 1081, + Z3_OP_BUREM_I = 1082, + Z3_OP_BSMOD_I = 1083, + Z3_OP_PR_UNDEF = 1280, + Z3_OP_PR_TRUE = 1281, + Z3_OP_PR_ASSERTED = 1282, + Z3_OP_PR_GOAL = 1283, + Z3_OP_PR_MODUS_PONENS = 1284, + Z3_OP_PR_REFLEXIVITY = 1285, + Z3_OP_PR_SYMMETRY = 1286, + Z3_OP_PR_TRANSITIVITY = 1287, + Z3_OP_PR_TRANSITIVITY_STAR = 1288, + Z3_OP_PR_MONOTONICITY = 1289, + Z3_OP_PR_QUANT_INTRO = 1290, + Z3_OP_PR_BIND = 1291, + Z3_OP_PR_DISTRIBUTIVITY = 1292, + Z3_OP_PR_AND_ELIM = 1293, + Z3_OP_PR_NOT_OR_ELIM = 1294, + Z3_OP_PR_REWRITE = 1295, + Z3_OP_PR_REWRITE_STAR = 1296, + Z3_OP_PR_PULL_QUANT = 1297, + Z3_OP_PR_PUSH_QUANT = 1298, + Z3_OP_PR_ELIM_UNUSED_VARS = 1299, + Z3_OP_PR_DER = 1300, + Z3_OP_PR_QUANT_INST = 1301, + Z3_OP_PR_HYPOTHESIS = 1302, + Z3_OP_PR_LEMMA = 1303, + Z3_OP_PR_UNIT_RESOLUTION = 1304, + Z3_OP_PR_IFF_TRUE = 1305, + Z3_OP_PR_IFF_FALSE = 1306, + Z3_OP_PR_COMMUTATIVITY = 1307, + Z3_OP_PR_DEF_AXIOM = 1308, + Z3_OP_PR_ASSUMPTION_ADD = 1309, + Z3_OP_PR_LEMMA_ADD = 1310, + Z3_OP_PR_REDUNDANT_DEL = 1311, + Z3_OP_PR_CLAUSE_TRAIL = 1312, + Z3_OP_PR_DEF_INTRO = 1313, + Z3_OP_PR_APPLY_DEF = 1314, + Z3_OP_PR_IFF_OEQ = 1315, + Z3_OP_PR_NNF_POS = 1316, + Z3_OP_PR_NNF_NEG = 1317, + Z3_OP_PR_SKOLEMIZE = 1318, + Z3_OP_PR_MODUS_PONENS_OEQ = 1319, + Z3_OP_PR_TH_LEMMA = 1320, + Z3_OP_PR_HYPER_RESOLVE = 1321, + Z3_OP_RA_STORE = 1536, + Z3_OP_RA_EMPTY = 1537, + Z3_OP_RA_IS_EMPTY = 1538, + Z3_OP_RA_JOIN = 1539, + Z3_OP_RA_UNION = 1540, + Z3_OP_RA_WIDEN = 1541, + Z3_OP_RA_PROJECT = 1542, + Z3_OP_RA_FILTER = 1543, + Z3_OP_RA_NEGATION_FILTER = 1544, + Z3_OP_RA_RENAME = 1545, + Z3_OP_RA_COMPLEMENT = 1546, + Z3_OP_RA_SELECT = 1547, + Z3_OP_RA_CLONE = 1548, + Z3_OP_FD_CONSTANT = 1549, + Z3_OP_FD_LT = 1550, + Z3_OP_SEQ_UNIT = 1551, + Z3_OP_SEQ_EMPTY = 1552, + Z3_OP_SEQ_CONCAT = 1553, + Z3_OP_SEQ_PREFIX = 1554, + Z3_OP_SEQ_SUFFIX = 1555, + Z3_OP_SEQ_CONTAINS = 1556, + Z3_OP_SEQ_EXTRACT = 1557, + Z3_OP_SEQ_REPLACE = 1558, + Z3_OP_SEQ_AT = 1559, + Z3_OP_SEQ_NTH = 1560, + Z3_OP_SEQ_LENGTH = 1561, + Z3_OP_SEQ_INDEX = 1562, + Z3_OP_SEQ_LAST_INDEX = 1563, + Z3_OP_SEQ_TO_RE = 1564, + Z3_OP_SEQ_IN_RE = 1565, + Z3_OP_STR_TO_INT = 1566, + Z3_OP_INT_TO_STR = 1567, + Z3_OP_STRING_LT = 1568, + Z3_OP_STRING_LE = 1569, + Z3_OP_RE_PLUS = 1570, + Z3_OP_RE_STAR = 1571, + Z3_OP_RE_OPTION = 1572, + Z3_OP_RE_CONCAT = 1573, + Z3_OP_RE_UNION = 1574, + Z3_OP_RE_RANGE = 1575, + Z3_OP_RE_LOOP = 1576, + Z3_OP_RE_INTERSECT = 1577, + Z3_OP_RE_EMPTY_SET = 1578, + Z3_OP_RE_FULL_SET = 1579, + Z3_OP_RE_COMPLEMENT = 1580, + Z3_OP_LABEL = 1792, + Z3_OP_LABEL_LIT = 1793, + Z3_OP_DT_CONSTRUCTOR = 2048, + Z3_OP_DT_RECOGNISER = 2049, + Z3_OP_DT_IS = 2050, + Z3_OP_DT_ACCESSOR = 2051, + Z3_OP_DT_UPDATE_FIELD = 2052, + Z3_OP_PB_AT_MOST = 2304, + Z3_OP_PB_AT_LEAST = 2305, + Z3_OP_PB_LE = 2306, + Z3_OP_PB_GE = 2307, + Z3_OP_PB_EQ = 2308, + Z3_OP_SPECIAL_RELATION_LO = 40960, + Z3_OP_SPECIAL_RELATION_PO = 40961, + Z3_OP_SPECIAL_RELATION_PLO = 40962, + Z3_OP_SPECIAL_RELATION_TO = 40963, + Z3_OP_SPECIAL_RELATION_TC = 40964, + Z3_OP_SPECIAL_RELATION_TRC = 40965, + Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN = 45056, + Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY = 45057, + Z3_OP_FPA_RM_TOWARD_POSITIVE = 45058, + Z3_OP_FPA_RM_TOWARD_NEGATIVE = 45059, + Z3_OP_FPA_RM_TOWARD_ZERO = 45060, + Z3_OP_FPA_NUM = 45061, + Z3_OP_FPA_PLUS_INF = 45062, + Z3_OP_FPA_MINUS_INF = 45063, + Z3_OP_FPA_NAN = 45064, + Z3_OP_FPA_PLUS_ZERO = 45065, + Z3_OP_FPA_MINUS_ZERO = 45066, + Z3_OP_FPA_ADD = 45067, + Z3_OP_FPA_SUB = 45068, + Z3_OP_FPA_NEG = 45069, + Z3_OP_FPA_MUL = 45070, + Z3_OP_FPA_DIV = 45071, + Z3_OP_FPA_REM = 45072, + Z3_OP_FPA_ABS = 45073, + Z3_OP_FPA_MIN = 45074, + Z3_OP_FPA_MAX = 45075, + Z3_OP_FPA_FMA = 45076, + Z3_OP_FPA_SQRT = 45077, + Z3_OP_FPA_ROUND_TO_INTEGRAL = 45078, + Z3_OP_FPA_EQ = 45079, + Z3_OP_FPA_LT = 45080, + Z3_OP_FPA_GT = 45081, + Z3_OP_FPA_LE = 45082, + Z3_OP_FPA_GE = 45083, + Z3_OP_FPA_IS_NAN = 45084, + Z3_OP_FPA_IS_INF = 45085, + Z3_OP_FPA_IS_ZERO = 45086, + Z3_OP_FPA_IS_NORMAL = 45087, + Z3_OP_FPA_IS_SUBNORMAL = 45088, + Z3_OP_FPA_IS_NEGATIVE = 45089, + Z3_OP_FPA_IS_POSITIVE = 45090, + Z3_OP_FPA_FP = 45091, + Z3_OP_FPA_TO_FP = 45092, + Z3_OP_FPA_TO_FP_UNSIGNED = 45093, + Z3_OP_FPA_TO_UBV = 45094, + Z3_OP_FPA_TO_SBV = 45095, + Z3_OP_FPA_TO_REAL = 45096, + Z3_OP_FPA_TO_IEEE_BV = 45097, + Z3_OP_FPA_BVWRAP = 45098, + Z3_OP_FPA_BV2RM = 45099, + Z3_OP_INTERNAL = 45100, + Z3_OP_UNINTERPRETED = 45101, +} diff --git a/z3-sys/src/generated/error_code.rs b/z3-sys/src/generated/error_code.rs new file mode 100644 index 00000000..5e4cb7fd --- /dev/null +++ b/z3-sys/src/generated/error_code.rs @@ -0,0 +1,19 @@ +/* automatically generated by rust-bindgen 0.59.2 */ + +#[repr(u32)] +#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)] +pub enum Z3_error_code { + Z3_OK = 0, + Z3_SORT_ERROR = 1, + Z3_IOB = 2, + Z3_INVALID_ARG = 3, + Z3_PARSER_ERROR = 4, + Z3_NO_PARSER = 5, + Z3_INVALID_PATTERN = 6, + Z3_MEMOUT_FAIL = 7, + Z3_FILE_ACCESS_ERROR = 8, + Z3_INTERNAL_FATAL = 9, + Z3_INVALID_USAGE = 10, + Z3_DEC_REF_ERROR = 11, + Z3_EXCEPTION = 12, +} diff --git a/z3-sys/src/generated/goal_prec.rs b/z3-sys/src/generated/goal_prec.rs new file mode 100644 index 00000000..6107c090 --- /dev/null +++ b/z3-sys/src/generated/goal_prec.rs @@ -0,0 +1,10 @@ +/* automatically generated by rust-bindgen 0.59.2 */ + +#[repr(u32)] +#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)] +pub enum Z3_goal_prec { + Z3_GOAL_PRECISE = 0, + Z3_GOAL_UNDER = 1, + Z3_GOAL_OVER = 2, + Z3_GOAL_UNDER_OVER = 3, +} diff --git a/z3-sys/src/generated/param_kind.rs b/z3-sys/src/generated/param_kind.rs new file mode 100644 index 00000000..1e9b1ea0 --- /dev/null +++ b/z3-sys/src/generated/param_kind.rs @@ -0,0 +1,13 @@ +/* automatically generated by rust-bindgen 0.59.2 */ + +#[repr(u32)] +#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)] +pub enum Z3_param_kind { + Z3_PK_UINT = 0, + Z3_PK_BOOL = 1, + Z3_PK_DOUBLE = 2, + Z3_PK_SYMBOL = 3, + Z3_PK_STRING = 4, + Z3_PK_OTHER = 5, + Z3_PK_INVALID = 6, +} diff --git a/z3-sys/src/generated/parameter_kind.rs b/z3-sys/src/generated/parameter_kind.rs new file mode 100644 index 00000000..4df538e5 --- /dev/null +++ b/z3-sys/src/generated/parameter_kind.rs @@ -0,0 +1,13 @@ +/* automatically generated by rust-bindgen 0.59.2 */ + +#[repr(u32)] +#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)] +pub enum Z3_parameter_kind { + Z3_PARAMETER_INT = 0, + Z3_PARAMETER_DOUBLE = 1, + Z3_PARAMETER_RATIONAL = 2, + Z3_PARAMETER_SYMBOL = 3, + Z3_PARAMETER_SORT = 4, + Z3_PARAMETER_AST = 5, + Z3_PARAMETER_FUNC_DECL = 6, +} diff --git a/z3-sys/src/generated/sort_kind.rs b/z3-sys/src/generated/sort_kind.rs new file mode 100644 index 00000000..f09c48ff --- /dev/null +++ b/z3-sys/src/generated/sort_kind.rs @@ -0,0 +1,20 @@ +/* automatically generated by rust-bindgen 0.59.2 */ + +#[repr(u32)] +#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)] +pub enum Z3_sort_kind { + Z3_UNINTERPRETED_SORT = 0, + Z3_BOOL_SORT = 1, + Z3_INT_SORT = 2, + Z3_REAL_SORT = 3, + Z3_BV_SORT = 4, + Z3_ARRAY_SORT = 5, + Z3_DATATYPE_SORT = 6, + Z3_RELATION_SORT = 7, + Z3_FINITE_DOMAIN_SORT = 8, + Z3_FLOATING_POINT_SORT = 9, + Z3_ROUNDING_MODE_SORT = 10, + Z3_SEQ_SORT = 11, + Z3_RE_SORT = 12, + Z3_UNKNOWN_SORT = 1000, +} diff --git a/z3-sys/src/generated/symbol_kind.rs b/z3-sys/src/generated/symbol_kind.rs new file mode 100644 index 00000000..c24c86e3 --- /dev/null +++ b/z3-sys/src/generated/symbol_kind.rs @@ -0,0 +1,8 @@ +/* automatically generated by rust-bindgen 0.59.2 */ + +#[repr(u32)] +#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)] +pub enum Z3_symbol_kind { + Z3_INT_SYMBOL = 0, + Z3_STRING_SYMBOL = 1, +} diff --git a/z3/Cargo.toml b/z3/Cargo.toml index 5361461b..eae1a31f 100644 --- a/z3/Cargo.toml +++ b/z3/Cargo.toml @@ -16,10 +16,9 @@ repository = "https://github.com/prove-rs/z3.rs.git" [features] default = [] arbitrary-size-numeral = ["num"] - -# Enable this feature to statically link our own build of Z3, rather than -# dynamically linking to the system's `libz3.so`. -static-link-z3 = ["z3-sys/static-link-z3"] +static-link-z3 = ["z3-sys/static-link-z3"] # Locally build and statically link a fresh Z3 build. +use-bindgen = ["z3-sys/use-bindgen"] # Generate fresh bindings with bindgen. +dynamic-link-z3 = ["z3-sys/dynamic-link-z3"] # Dynamically link the system's Z3 installation. [dependencies] log = "0.4"