z3: Update to Rust edition 2018. Collapse some imports.

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]

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> {

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.

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 {

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,
 };

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 {

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 {

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 {

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 {

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).
 ///

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> {

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());

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::{

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> {

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.

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> {

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 {

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> {

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> {

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`].
 ///

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 {

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> {