Always use num, remove arbitrary-size-numeral feature.

This is always on now.
prove-rs · Oct 24, 2023 · 6527daa · 6527daa
1 parent 1335297
commit 6527daa
Show file tree

Hide file tree

Showing 6 changed files with 3 additions and 29 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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,22 +269,19 @@ 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);
         self.to_str_radix(10)
     }
 }
 
-#[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
@@ -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();