From 6527daa47373ed6828ff69631bfc779822e8e378 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Mon, 23 Oct 2023 13:08:35 +0700 Subject: [PATCH] Always use `num`, remove `arbitrary-size-numeral` feature. This is always on now. --- .github/workflows/rust.yml | 9 +-------- z3/Cargo.toml | 3 +-- z3/src/ast.rs | 3 --- z3/src/lib.rs | 1 - z3/src/optimize.rs | 7 ------- z3/tests/lib.rs | 9 +-------- 6 files changed, 3 insertions(+), 29 deletions(-) diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index d085caf9..72b984e9 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -32,10 +32,6 @@ jobs: # we figure out how to work around it. At least we have the # statically-linked Z3 tests below... if: ${{ success() || failure() }} - - name: Run tests with `arbitrary-size-numeral` enabled - run: cargo test --workspace --features arbitrary-size-numeral - # See above. - if: ${{ success() || failure() }} build_on_wasm: runs-on: ubuntu-latest @@ -86,8 +82,7 @@ jobs: if: matrix.os == 'windows-latest' - name: Test `z3-sys` and `z3` with statically linked Z3 run: cargo test --workspace --features static-link-z3 - - name: Test `z3` with statically linked Z3 and `arbitrary-size-numeral` enabled - run: cargo test --workspace --features 'static-link-z3 arbitrary-size-numeral' + build_with_vcpkg_installed_z3: strategy: matrix: @@ -133,8 +128,6 @@ jobs: run: rustup default - name: Test `z3-sys` and `z3` with vcpkg installed Z3 run: cargo test --workspace --features vcpkg - - name: Test `z3` with vcpkg installed Z3 and `arbitrary-size-numeral` enabled - run: cargo test --workspace --features 'vcpkg arbitrary-size-numeral' run_clippy: runs-on: macos-latest diff --git a/z3/Cargo.toml b/z3/Cargo.toml index 20964a1b..fb04a6d6 100644 --- a/z3/Cargo.toml +++ b/z3/Cargo.toml @@ -16,7 +16,6 @@ edition = "2018" [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`. @@ -28,7 +27,7 @@ vcpkg = ["z3-sys/vcpkg"] log = "0.4" # optional dependencies -num = { version = "0.4.0", optional=true } +num = "0.4" [dev-dependencies] env_logger = "0.10" diff --git a/z3/src/ast.rs b/z3/src/ast.rs index ae9037f9..6fe354dc 100644 --- a/z3/src/ast.rs +++ b/z3/src/ast.rs @@ -12,7 +12,6 @@ use z3_sys::*; use crate::{Context, FuncDecl, IsNotApp, Pattern, Sort, SortDiffers, Symbol}; -#[cfg(feature = "arbitrary-size-numeral")] use num::{bigint::BigInt, rational::BigRational}; /// [`Ast`] node representing a boolean value. @@ -556,7 +555,6 @@ impl_from_try_into_dynamic!(Set, as_set); impl_ast!(Regexp); impl<'ctx> Int<'ctx> { - #[cfg(feature = "arbitrary-size-numeral")] pub fn from_big_int(ctx: &'ctx Context, value: &BigInt) -> Int<'ctx> { Int::from_str(ctx, &value.to_str_radix(10)).unwrap() } @@ -577,7 +575,6 @@ impl<'ctx> Int<'ctx> { } impl<'ctx> Real<'ctx> { - #[cfg(feature = "arbitrary-size-numeral")] pub fn from_big_rational(ctx: &'ctx Context, value: &BigRational) -> Real<'ctx> { let num = value.numer(); let den = value.denom(); diff --git a/z3/src/lib.rs b/z3/src/lib.rs index a6236338..772fe9f8 100644 --- a/z3/src/lib.rs +++ b/z3/src/lib.rs @@ -11,7 +11,6 @@ extern crate log; extern crate z3_sys; -#[cfg(feature = "arbitrary-size-numeral")] extern crate num; use std::ffi::CString; diff --git a/z3/src/optimize.rs b/z3/src/optimize.rs index 39d42f08..6f62f6d4 100644 --- a/z3/src/optimize.rs +++ b/z3/src/optimize.rs @@ -9,7 +9,6 @@ use crate::{ Context, Model, Optimize, SatResult, Statistics, Symbol, }; -#[cfg(feature = "arbitrary-size-numeral")] use num::{ bigint::{BigInt, BigUint, Sign}, rational::BigRational, @@ -270,7 +269,6 @@ impl_weight! { u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize } -#[cfg(feature = "arbitrary-size-numeral")] impl Weight for BigInt { fn to_string(&self) -> String { assert_ne!(self.sign(), Sign::Minus); @@ -278,14 +276,12 @@ impl Weight for BigInt { } } -#[cfg(feature = "arbitrary-size-numeral")] impl Weight for BigUint { fn to_string(&self) -> String { self.to_str_radix(10) } } -#[cfg(feature = "arbitrary-size-numeral")] impl Weight for BigRational { fn to_string(&self) -> String { assert_ne!(self.numer().sign(), Sign::Minus); @@ -309,11 +305,8 @@ macro_rules! impl_sealed { impl Sealed for ($ty, $ty) {} )* - #[cfg(feature = "arbitrary-size-numeral")] impl Sealed for BigInt {} - #[cfg(feature = "arbitrary-size-numeral")] impl Sealed for BigUint {} - #[cfg(feature = "arbitrary-size-numeral")] impl Sealed for BigRational {} } }; diff --git a/z3/tests/lib.rs b/z3/tests/lib.rs index 01c03a84..f78fb895 100644 --- a/z3/tests/lib.rs +++ b/z3/tests/lib.rs @@ -9,13 +9,8 @@ use std::time::Duration; use z3::ast::{Array, Ast, Bool, Int, BV}; use z3::*; -#[cfg(feature = "arbitrary-size-numeral")] extern crate num; -#[cfg(feature = "arbitrary-size-numeral")] -use num::bigint::BigInt; -#[cfg(feature = "arbitrary-size-numeral")] -use num::rational::BigRational; -#[cfg(feature = "arbitrary-size-numeral")] +use num::{bigint::BigInt, rational::BigRational}; use std::str::FromStr; #[test] @@ -458,7 +453,6 @@ fn test_arbitrary_size_int() { assert_eq!(solver.check(), SatResult::Sat); } -#[cfg(feature = "arbitrary-size-numeral")] #[test] fn test_arbitrary_size_real_from_bigrational() { let cfg = Config::new(); @@ -476,7 +470,6 @@ fn test_arbitrary_size_real_from_bigrational() { assert_eq!(solver.check(), SatResult::Sat); } -#[cfg(feature = "arbitrary-size-numeral")] #[test] fn test_arbitrary_size_int_from_bigint() { let cfg = Config::new();