diff --git a/z3/Cargo.toml b/z3/Cargo.toml index 11c3c7a3..20964a1b 100644 --- a/z3/Cargo.toml +++ b/z3/Cargo.toml @@ -11,6 +11,7 @@ readme = "README.md" documentation = "https://docs.rs/z3/" homepage = "https://github.com/prove-rs/z3.rs" repository = "https://github.com/prove-rs/z3.rs.git" +edition = "2018" [features] diff --git a/z3/src/ast.rs b/z3/src/ast.rs index bd7efc99..ae9037f9 100644 --- a/z3/src/ast.rs +++ b/z3/src/ast.rs @@ -6,21 +6,14 @@ use std::convert::{TryFrom, TryInto}; use std::ffi::{CStr, CString}; use std::fmt; use std::hash::{Hash, Hasher}; -use z3_sys::*; -use Context; -use FuncDecl; -use IsNotApp; -use Pattern; -use Sort; -use SortDiffers; -use Symbol; pub use z3_sys::AstKind; +use z3_sys::*; + +use crate::{Context, FuncDecl, IsNotApp, Pattern, Sort, SortDiffers, Symbol}; #[cfg(feature = "arbitrary-size-numeral")] -use num::bigint::BigInt; -#[cfg(feature = "arbitrary-size-numeral")] -use num::rational::BigRational; +use num::{bigint::BigInt, rational::BigRational}; /// [`Ast`] node representing a boolean value. pub struct Bool<'ctx> { diff --git a/z3/src/config.rs b/z3/src/config.rs index 6f1d8328..2a1e3b97 100644 --- a/z3/src/config.rs +++ b/z3/src/config.rs @@ -1,6 +1,8 @@ use std::ffi::CString; + use z3_sys::*; -use Config; + +use crate::Config; impl Config { /// Create a configuration object for the Z3 context object. diff --git a/z3/src/context.rs b/z3/src/context.rs index 8e736923..9ecab83e 100644 --- a/z3/src/context.rs +++ b/z3/src/context.rs @@ -1,8 +1,8 @@ use std::ffi::CString; + use z3_sys::*; -use Config; -use Context; -use ContextHandle; + +use crate::{Config, Context, ContextHandle}; impl Context { pub fn new(cfg: &Config) -> Context { diff --git a/z3/src/datatype_builder.rs b/z3/src/datatype_builder.rs index 5b7fe94f..c94a92ec 100644 --- a/z3/src/datatype_builder.rs +++ b/z3/src/datatype_builder.rs @@ -1,8 +1,10 @@ //! Helpers for building custom [datatype sorts](DatatypeSort). use std::{convert::TryInto, ptr::null_mut}; + use z3_sys::*; -use { + +use crate::{ Context, DatatypeAccessor, DatatypeBuilder, DatatypeSort, DatatypeVariant, FuncDecl, Sort, Symbol, }; diff --git a/z3/src/func_decl.rs b/z3/src/func_decl.rs index fc120e37..0d4f73e9 100644 --- a/z3/src/func_decl.rs +++ b/z3/src/func_decl.rs @@ -1,10 +1,10 @@ -use ast; -use ast::Ast; use std::convert::TryInto; use std::ffi::CStr; use std::fmt; + use z3_sys::*; -use {Context, FuncDecl, Sort, Symbol}; + +use crate::{ast, ast::Ast, Context, FuncDecl, Sort, Symbol}; impl<'ctx> FuncDecl<'ctx> { pub(crate) unsafe fn wrap(ctx: &'ctx Context, z3_func_decl: Z3_func_decl) -> Self { diff --git a/z3/src/func_entry.rs b/z3/src/func_entry.rs index 3054fcff..a1e2f33d 100644 --- a/z3/src/func_entry.rs +++ b/z3/src/func_entry.rs @@ -1,9 +1,11 @@ use std::fmt; -use ast::Ast; use z3_sys::*; -use {ast::Dynamic, Context, FuncEntry}; +use crate::{ + ast::{Ast, Dynamic}, + Context, FuncEntry, +}; impl<'ctx> FuncEntry<'ctx> { pub(crate) unsafe fn wrap(ctx: &'ctx Context, z3_func_entry: Z3_func_entry) -> Self { diff --git a/z3/src/func_interp.rs b/z3/src/func_interp.rs index f148b709..e334ac22 100644 --- a/z3/src/func_interp.rs +++ b/z3/src/func_interp.rs @@ -1,8 +1,11 @@ -use ast::Ast; use std::fmt; + use z3_sys::*; -use {ast::Dynamic, Context, FuncEntry, FuncInterp}; +use crate::{ + ast::{Ast, Dynamic}, + Context, FuncEntry, FuncInterp, +}; impl<'ctx> FuncInterp<'ctx> { pub(crate) unsafe fn wrap(ctx: &'ctx Context, z3_func_interp: Z3_func_interp) -> Self { diff --git a/z3/src/goal.rs b/z3/src/goal.rs index 8688734d..66a9e951 100644 --- a/z3/src/goal.rs +++ b/z3/src/goal.rs @@ -3,10 +3,7 @@ use std::fmt; use z3_sys::*; -use crate::ast; -use crate::ast::Ast; -use Context; -use Goal; +use crate::{ast, ast::Ast, Context, Goal}; impl<'ctx> Clone for Goal<'ctx> { fn clone(&self) -> Self { diff --git a/z3/src/lib.rs b/z3/src/lib.rs index 34e63b59..a6236338 100644 --- a/z3/src/lib.rs +++ b/z3/src/lib.rs @@ -39,8 +39,8 @@ mod statistics; mod symbol; mod tactic; -pub use params::{get_global_param, reset_all_global_params, set_global_param}; -pub use statistics::{StatisticsEntry, StatisticsValue}; +pub use crate::params::{get_global_param, reset_all_global_params, set_global_param}; +pub use crate::statistics::{StatisticsEntry, StatisticsValue}; /// Configuration used to initialize [logical contexts](Context). /// diff --git a/z3/src/model.rs b/z3/src/model.rs index e0d0f970..5cf4b318 100644 --- a/z3/src/model.rs +++ b/z3/src/model.rs @@ -1,13 +1,9 @@ -use ast::Ast; use std::ffi::CStr; use std::fmt; + use z3_sys::*; -use Context; -use Model; -use Optimize; -use Solver; -use crate::{FuncDecl, FuncInterp}; +use crate::{ast::Ast, Context, FuncDecl, FuncInterp, Model, Optimize, Solver}; impl<'ctx> Model<'ctx> { unsafe fn wrap(ctx: &'ctx Context, z3_mdl: Z3_model) -> Model<'ctx> { diff --git a/z3/src/ops.rs b/z3/src/ops.rs index b9594140..30b5fb98 100644 --- a/z3/src/ops.rs +++ b/z3/src/ops.rs @@ -1,9 +1,10 @@ -use crate::ast::{Ast, Bool, Float, Int, Real, BV}; use std::ops::{ Add, AddAssign, BitAnd, BitAndAssign, BitOr, BitOrAssign, BitXor, BitXorAssign, Div, DivAssign, Mul, MulAssign, Neg, Not, Rem, RemAssign, Shl, ShlAssign, Sub, SubAssign, }; +use crate::ast::{Ast, Bool, Float, Int, Real, BV}; + macro_rules! mk_const_bv { ($constant:expr, $function:ident, $val:expr, $other:expr) => { $constant = BV::$function($other.get_ctx(), $val, $other.get_size()); diff --git a/z3/src/optimize.rs b/z3/src/optimize.rs index cf91f99b..39d42f08 100644 --- a/z3/src/optimize.rs +++ b/z3/src/optimize.rs @@ -1,14 +1,13 @@ -use ast::{Ast, Bool, Dynamic}; use std::convert::TryInto; use std::ffi::{CStr, CString}; use std::fmt; + use z3_sys::*; -use Context; -use Model; -use Optimize; -use SatResult; -use Statistics; -use Symbol; + +use crate::{ + ast::{Ast, Bool, Dynamic}, + Context, Model, Optimize, SatResult, Statistics, Symbol, +}; #[cfg(feature = "arbitrary-size-numeral")] use num::{ diff --git a/z3/src/params.rs b/z3/src/params.rs index 0cca03f9..307f32e0 100644 --- a/z3/src/params.rs +++ b/z3/src/params.rs @@ -1,9 +1,9 @@ use std::ffi::{CStr, CString}; use std::fmt; + use z3_sys::*; -use Context; -use Params; -use Symbol; + +use crate::{Context, Params, Symbol}; impl<'ctx> Params<'ctx> { unsafe fn wrap(ctx: &'ctx Context, z3_params: Z3_params) -> Params<'ctx> { diff --git a/z3/src/pattern.rs b/z3/src/pattern.rs index 5d61afe6..9d869720 100644 --- a/z3/src/pattern.rs +++ b/z3/src/pattern.rs @@ -1,10 +1,10 @@ -use ast::Ast; use std::convert::TryInto; use std::ffi::CStr; use std::fmt; + use z3_sys::*; -use Context; -use Pattern; + +use crate::{ast::Ast, Context, Pattern}; impl<'ctx> Pattern<'ctx> { /// Create a pattern for quantifier instantiation. diff --git a/z3/src/probe.rs b/z3/src/probe.rs index 42ac85c0..2fa44e55 100644 --- a/z3/src/probe.rs +++ b/z3/src/probe.rs @@ -4,9 +4,8 @@ use std::result::Result; use std::str::Utf8Error; use z3_sys::*; -use Context; -use Goal; -use Probe; + +use crate::{Context, Goal, Probe}; impl<'ctx> Probe<'ctx> { unsafe fn wrap(ctx: &'ctx Context, z3_probe: Z3_probe) -> Probe<'ctx> { diff --git a/z3/src/rec_func_decl.rs b/z3/src/rec_func_decl.rs index 2bd8be98..f1dd65b6 100644 --- a/z3/src/rec_func_decl.rs +++ b/z3/src/rec_func_decl.rs @@ -1,11 +1,11 @@ -use ast; -use ast::Ast; use std::convert::TryInto; use std::ffi::CStr; use std::fmt; use std::ops::Deref; + use z3_sys::*; -use {Context, FuncDecl, RecFuncDecl, Sort, Symbol}; + +use crate::{ast, ast::Ast, Context, FuncDecl, RecFuncDecl, Sort, Symbol}; impl<'ctx> RecFuncDecl<'ctx> { pub(crate) unsafe fn wrap(ctx: &'ctx Context, z3_func_decl: Z3_func_decl) -> Self { diff --git a/z3/src/solver.rs b/z3/src/solver.rs index e2162846..b7f2b06f 100644 --- a/z3/src/solver.rs +++ b/z3/src/solver.rs @@ -1,15 +1,9 @@ -use ast; -use ast::Ast; use std::ffi::{CStr, CString}; use std::fmt; + use z3_sys::*; -use Context; -use Model; -use Params; -use SatResult; -use Solver; -use Statistics; -use Symbol; + +use crate::{ast, ast::Ast, Context, Model, Params, SatResult, Solver, Statistics, Symbol}; impl<'ctx> Solver<'ctx> { pub(crate) unsafe fn wrap(ctx: &'ctx Context, z3_slv: Z3_solver) -> Solver<'ctx> { diff --git a/z3/src/sort.rs b/z3/src/sort.rs index 79739603..8c236730 100644 --- a/z3/src/sort.rs +++ b/z3/src/sort.rs @@ -1,12 +1,10 @@ use std::convert::TryInto; use std::ffi::CStr; use std::fmt; + use z3_sys::*; -use Context; -use FuncDecl; -use Sort; -use SortDiffers; -use Symbol; + +use crate::{Context, FuncDecl, Sort, SortDiffers, Symbol}; impl<'ctx> Sort<'ctx> { pub(crate) unsafe fn wrap(ctx: &'ctx Context, z3_sort: Z3_sort) -> Sort<'ctx> { diff --git a/z3/src/statistics.rs b/z3/src/statistics.rs index 85d93eb4..db3b1885 100644 --- a/z3/src/statistics.rs +++ b/z3/src/statistics.rs @@ -2,8 +2,8 @@ use std::ffi::CStr; use std::fmt; use z3_sys::*; -use Context; -use Statistics; + +use crate::{Context, Statistics}; /// The value for a key in [`Statistics`]. /// diff --git a/z3/src/symbol.rs b/z3/src/symbol.rs index 302fd742..2384fcfa 100644 --- a/z3/src/symbol.rs +++ b/z3/src/symbol.rs @@ -1,7 +1,8 @@ use std::ffi::CString; + use z3_sys::*; -use Context; -use Symbol; + +use crate::{Context, Symbol}; impl Symbol { pub fn as_z3_symbol(&self, ctx: &Context) -> Z3_symbol { diff --git a/z3/src/tactic.rs b/z3/src/tactic.rs index 90416ea2..57bfbb2f 100644 --- a/z3/src/tactic.rs +++ b/z3/src/tactic.rs @@ -7,13 +7,8 @@ use std::str::Utf8Error; use std::time::Duration; use z3_sys::*; -use ApplyResult; -use Context; -use Goal; -use Params; -use Probe; -use Solver; -use Tactic; + +use crate::{ApplyResult, Context, Goal, Params, Probe, Solver, Tactic}; impl<'ctx> ApplyResult<'ctx> { unsafe fn wrap(ctx: &'ctx Context, z3_apply_result: Z3_apply_result) -> ApplyResult<'ctx> {