From 530b6acb9462b1596bbf3352758f34ec9ada61eb Mon Sep 17 00:00:00 2001
From: Bruce Mitchener <bruce.mitchener@gmail.com>
Date: Mon, 23 Oct 2023 12:10:11 +0700
Subject: [PATCH] z3: Update to Rust edition 2018. Collapse some imports.

---
 z3/Cargo.toml              |  1 +
 z3/src/ast.rs              | 15 ++++-----------
 z3/src/config.rs           |  4 +++-
 z3/src/context.rs          |  6 +++---
 z3/src/datatype_builder.rs |  4 +++-
 z3/src/func_decl.rs        |  6 +++---
 z3/src/func_entry.rs       |  6 ++++--
 z3/src/func_interp.rs      |  7 +++++--
 z3/src/goal.rs             |  5 +----
 z3/src/lib.rs              |  4 ++--
 z3/src/model.rs            |  8 ++------
 z3/src/ops.rs              |  3 ++-
 z3/src/optimize.rs         | 13 ++++++-------
 z3/src/params.rs           |  6 +++---
 z3/src/pattern.rs          |  6 +++---
 z3/src/probe.rs            |  5 ++---
 z3/src/rec_func_decl.rs    |  6 +++---
 z3/src/solver.rs           | 12 +++---------
 z3/src/sort.rs             |  8 +++-----
 z3/src/statistics.rs       |  4 ++--
 z3/src/symbol.rs           |  5 +++--
 z3/src/tactic.rs           |  9 ++-------
 22 files changed, 63 insertions(+), 80 deletions(-)

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