Add functions to access the wrapped z3::Context and z3::Solver from Z…

…3Solver, and to create BVs/Ints/Bools from z3 types and vice versa.

liblisa/src/smt/z3/mod.rs

@@ -7,7 +7,7 @@ mod tests;
 use std::cell::RefCell;
 use std::collections::HashMap;
 use std::fmt::{Debug, Display};
-use std::ops::{Add, BitAnd, BitOr, BitXor, Mul, Not, Sub};
+use std::ops::{Add, BitAnd, BitOr, BitXor, Mul, Neg, Not, Sub};
 use std::time::Duration;
 
 use z3::ast::{forall_const, Ast};
@@ -62,6 +62,16 @@ impl<'ctx> Z3Solver<'ctx> {
             solver,
         }
     }
+
+    /// Returns the [`z3::Context`] wrapped by this struct.
+    pub fn context(&self) -> &'ctx Context {
+        self.context
+    }
+
+    /// Returns the [`z3::Solver`] wrapped by this struct.
+    pub fn solver(&self) -> &z3::Solver<'ctx> {
+        &self.solver
+    }
 }
 
 impl Z3Solver<'static> {
@@ -193,6 +203,18 @@ impl<'ctx> Display for BV<'ctx> {
     }
 }
 
+impl<'ctx> BV<'ctx> {
+    /// Wraps a [`z3::ast::BV`].
+    pub fn from_z3(bv: z3::ast::BV<'ctx>) -> Self {
+        Self(bv)
+    }
+
+    /// Returns the wrapped [`z3::ast::BV`].
+    pub fn as_z3(&self) -> &z3::ast::BV {
+        &self.0
+    }
+}
+
 impl<'ctx> SmtBV<'ctx, Z3Solver<'ctx>> for BV<'ctx> {
     fn concat(self, other: Self) -> Self {
         BV(self.0.concat(&other.0))
@@ -351,6 +373,14 @@ impl<'ctx> Not for BV<'ctx> {
     }
 }
 
+impl<'ctx> Neg for BV<'ctx> {
+    type Output = Self;
+
+    fn neg(self) -> Self::Output {
+        BV(self.0.neg())
+    }
+}
+
 /// A Z3 Int.
 #[derive(Clone, Debug)]
 pub struct Int<'ctx>(z3::ast::Int<'ctx>);
@@ -361,6 +391,18 @@ impl<'ctx> Display for Int<'ctx> {
     }
 }
 
+impl<'ctx> Int<'ctx> {
+    /// Wraps a [`z3::ast::Int`].
+    pub fn from_z3(int: z3::ast::Int<'ctx>) -> Self {
+        Self(int)
+    }
+
+    /// Returns the wrapped [`z3::ast::Int`].
+    pub fn as_z3(&self) -> &z3::ast::Int {
+        &self.0
+    }
+}
+
 impl<'ctx> SmtInt<'ctx, Z3Solver<'ctx>> for Int<'ctx> {
     fn simplify(self) -> Self {
         Int(self.0.simplify())
@@ -413,6 +455,18 @@ impl<'ctx> Display for Bool<'ctx> {
     }
 }
 
+impl<'ctx> Bool<'ctx> {
+    /// Wraps a [`z3::ast::Bool`].
+    pub fn from_z3(bool: z3::ast::Bool<'ctx>) -> Self {
+        Self(bool)
+    }
+
+    /// Returns the wrapped [`z3::ast::Bool`].
+    pub fn as_z3(&self) -> &z3::ast::Bool {
+        &self.0
+    }
+}
+
 impl<'ctx> SmtBool<'ctx, Z3Solver<'ctx>> for Bool<'ctx> {
     fn ite_bv(self, lhs: BV<'ctx>, rhs: BV<'ctx>) -> BV<'ctx> {
         BV(self.0.ite(&lhs.0, &rhs.0))