update dependencies

in particular, z3.rs needed some patches for the next features

Cargo.toml

@@ -24,8 +24,8 @@ string-interner = "0.12"
 once_cell = "1.8"
 typed-arena = "2.0"
 lalrpop-util = "0.19"
-z3 = "^0.11.2"
-z3-sys = "^0"
+z3 = "^0.12"
+z3-sys = "^0.8"
 ref-cast = "1.0"
 replace_with = "0.1"
 num = "0.4"
@@ -37,7 +37,6 @@ egg = "0.7"
 tokio = { version = "1", features = ["time", "macros", "rt", "rt-multi-thread"] }
 simple-process-stats = "1.0"
 hdrhistogram = "7.4"
-memchr = "2"
 ariadne = "0.1"
 atty = "0.2"
 shellwords = "1.1.0"
@@ -76,8 +75,12 @@ harness = false
 opt-level = 3
 
 [patch.crates-io]
-z3 = { git = 'https://github.com/Philipp15b/z3.rs.git', rev = '002e5c9ea805563cf33030c969d95b8102c9340f' }
+z3 = { git = 'https://github.com/Philipp15b/z3.rs.git', rev = 'bdd501ca1e50785365b875b3438a0cf953cffbfc' }
+z3-sys = { git = 'https://github.com/Philipp15b/z3.rs.git', rev = 'bdd501ca1e50785365b875b3438a0cf953cffbfc' }
 # to work on z3.rs locally, clone it into the main directory and use the following directive instead:
 # z3 = { path = 'z3.rs/z3' }
 
 lit = { git = 'https://github.com/Philipp15b/lit.git', rev = '40426a541626b90aed4ceaac9b7008b647f06d1e' }
+
+# see https://github.com/heim-rs/darwin-libproc/pull/3#issuecomment-1645444056
+darwin-libproc = { git = "https://github.com/Orycterope/darwin-libproc.git", rev = "f73ddb1002d51ae74c1b41670fae56bd5896b7a3" }

src/front/parser/mod.rs

@@ -139,16 +139,10 @@ struct UnclosedCommentError;
 /// can be fed into our parser, and all non-whitespace locations will be the
 /// same as in the original string.
 fn remove_comments(source: &str) -> Result<String, UnclosedCommentError> {
-    // this function is faster than `iter.find(|ch| *ch == needle)`.
-    fn fast_find_mut<'a>(iter: &mut std::slice::IterMut<'a, u8>, needle: u8) -> Option<&'a mut u8> {
-        let pos = memchr::memchr(needle, iter.as_slice())?;
-        Some(iter.nth(pos).unwrap())
-    }
-
     let mut res = source.as_bytes().to_owned();
     let mut iter = res.iter_mut();
     // iterate over all comment candidates
-    while let Some(ch1) = fast_find_mut(&mut iter, b'/') {
+    while let Some(ch1) = iter.find(|ch| **ch == b'/') {
         match iter.next() {
             // single line comments
             Some(ch2 @ b'/') => {

z3rro/Cargo.toml

@@ -4,7 +4,7 @@ version = "0.1.0"
 edition = "2021"
 
 [dependencies]
-z3 = "^0.11.2"
+z3 = "^0.12"
 ref-cast = "1.0"
 num = "0.4"
 once_cell = "1.8"

z3rro/src/eureal/pair.rs

@@ -143,7 +143,7 @@ impl<'a, 'ctx> Sub<&'a EUReal<'ctx>> for &'a EUReal<'ctx> {
     fn sub(self, rhs: &'a EUReal<'ctx>) -> Self::Output {
         EUReal {
             factory: self.factory.clone(),
-            is_infinite: z3_and!(&self.is_infinite, rhs.is_infinite.not()),
+            is_infinite: z3_and!(&self.is_infinite, &rhs.is_infinite.not()),
             number: &self.number - &rhs.number,
         }
     }
@@ -156,13 +156,13 @@ impl<'a, 'ctx> Mul<&'a EUReal<'ctx>> for &'a EUReal<'ctx> {
 
     fn mul(self, rhs: &'a EUReal<'ctx>) -> Self::Output {
         let zero = UReal::zero(&self.factory.ctx);
-        let a_nonzero = z3_or!(&self.is_infinite, self.number.smt_eq(&zero).not());
-        let b_nonzero = z3_or!(&rhs.is_infinite, rhs.number.smt_eq(&zero).not());
+        let a_nonzero = z3_or!(&self.is_infinite, &self.number.smt_eq(&zero).not());
+        let b_nonzero = z3_or!(&rhs.is_infinite, &rhs.number.smt_eq(&zero).not());
         EUReal {
             factory: self.factory.clone(),
             is_infinite: z3_or!(
-                z3_and!(&self.is_infinite, b_nonzero),
-                z3_and!(&rhs.is_infinite, a_nonzero)
+                z3_and!(&self.is_infinite, &b_nonzero),
+                z3_and!(&rhs.is_infinite, &a_nonzero)
             ),
             number: &self.number * &rhs.number,
         }
@@ -186,7 +186,7 @@ impl<'ctx> SmtPartialOrd<'ctx> for EUReal<'ctx> {
         fn eureal_le<'ctx>(a: &EUReal<'ctx>, b: &EUReal<'ctx>) -> Bool<'ctx> {
             z3_or!(
                 &b.is_infinite,
-                z3_and!(a.is_infinite.not(), a.number.smt_le(&b.number))
+                &z3_and!(&a.is_infinite.not(), &a.number.smt_le(&b.number))
             )
         }
 

z3rro/src/interpreted.rs

@@ -33,7 +33,7 @@ impl<'ctx> FuncDef<'ctx> {
             let domain: Vec<_> = self.args.iter().map(|arg| arg.get_sort()).collect();
             let domain: Vec<_> = domain.iter().collect();
             let decl = RecFuncDecl::new(ctx, self.name.clone(), &domain, &self.body.get_sort());
-            let args: Vec<_> = self.args.iter().collect();
+            let args: Vec<_> = self.args.iter().map(|ast| ast as &dyn Ast).collect();
             decl.add_def(&args, &self.body);
             decl
         })
@@ -44,7 +44,8 @@ impl<'ctx> FuncDef<'ctx> {
     /// A call to this function will initialize the Z3 declaration if needed.
     pub fn apply_call(&self, args: &[&Dynamic<'ctx>]) -> Dynamic<'ctx> {
         let decl = self.get_decl();
-        decl.apply(args)
+        let args: Vec<&dyn Ast> = args.iter().map(|ast| *ast as &dyn Ast).collect();
+        decl.apply(&args)
     }
 
     /// Apply the function by inlining its body and substituting the arguments.

z3rro/src/orders.rs

@@ -101,11 +101,11 @@ where
 impl<'ctx> SmtPartialOrd<'ctx> for Bool<'ctx> {
     fn smt_cmp(&self, other: &Self, ordering: SmtOrdering) -> Bool<'ctx> {
         match ordering {
-            SmtOrdering::Less => z3_and!(self.not(), other),
+            SmtOrdering::Less => Bool::and(self.get_ctx(), &[&self.not(), &other]),
             SmtOrdering::LessOrEqual => self.implies(other),
             SmtOrdering::Equal => self._eq(other),
             SmtOrdering::GreaterOrEqual => other.implies(self),
-            SmtOrdering::Greater => z3_and!(self, other.not()),
+            SmtOrdering::Greater => z3_and!(self, &other.not()),
         }
     }
 }

z3rro/src/scope.rs

@@ -71,7 +71,7 @@ impl<'ctx> SmtScope<'ctx> {
             ctx,
             &self.bounds_dyn(),
             patterns,
-            &z3_and!(self.all_constraints(ctx), body),
+            &Bool::and(ctx, &[&self.all_constraints(ctx), &body]),
         )
     }
 

z3rro/src/util.rs

@@ -13,7 +13,7 @@ macro_rules! z3_and {
         {
             use z3::ast::{Ast, Bool};
             let first = $first;
-            Bool::and(first.get_ctx(),  &[&first, $(&$x,)*])
+            Bool::and(first.get_ctx(),  &[first, $($x,)*])
         }
     };
     ($( $x:expr ),*) => { z3_and!($($x,)*) }
@@ -26,7 +26,7 @@ macro_rules! z3_or {
         {
             use z3::ast::{Ast, Bool};
             let first = $first;
-            Bool::or(first.get_ctx(),  &[&first, $(&$x,)*])
+            Bool::or(first.get_ctx(),  &[first, $($x,)*])
         }
     };
     ($( $x:expr ),*) => { z3_or!($($x,)*) }