Add binding for Z3_get_implied_equalities

z3-sys/src/lib.rs

@@ -3087,6 +3087,12 @@ extern "C" {
     /// - `container` and `containee` are the same sequence sorts.
     pub fn Z3_mk_seq_contains(c: Z3_context, container: Z3_ast, containee: Z3_ast) -> Z3_ast;
 
+    /// Check if `s1` is lexicographically strictly less than `s2`.
+    pub fn Z3_mk_str_lt(c: Z3_context, s1: Z3_ast, s2: Z3_ast) -> Z3_ast;
+
+    /// Check if `s1` is equal or lexicographically strictly less than `s2`.
+    pub fn Z3_mk_str_le(c: Z3_context, s1: Z3_ast, s2: Z3_ast) -> Z3_ast;
+
     /// Extract subsequence starting at `offset` of `length`.
     pub fn Z3_mk_seq_extract(c: Z3_context, s: Z3_ast, offset: Z3_ast, length: Z3_ast) -> Z3_ast;
 

z3/src/ast.rs

@@ -1158,6 +1158,16 @@ impl<'ctx> String<'ctx> {
         prefix(Z3_mk_seq_prefix, Bool<'ctx>);
         /// Checks whether `Self` is a sufix of the argument
         suffix(Z3_mk_seq_suffix, Bool<'ctx>);
+        le(Z3_mk_str_le, Bool<'ctx>);
+        lt(Z3_mk_str_lt, Bool<'ctx>);
+    }
+
+    pub fn ge(&self, other: &String<'ctx>) -> Bool<'ctx> {
+        other.le(self)
+    }
+
+    pub fn gt(&self, other: &String<'ctx>) -> Bool<'ctx> {
+        other.lt(self)
     }
 }
 
@@ -1715,6 +1725,25 @@ impl<'ctx> Dynamic<'ctx> {
             _ => None,
         }
     }
+
+    pub fn new_const<S: Into<Symbol>>(ctx: &'ctx Context, name: S, sort: &Sort<'ctx>) -> Self {
+        assert_eq!(ctx, sort.ctx);
+
+        unsafe {
+            Self::wrap(
+                ctx,
+                Z3_mk_const(ctx.z3_ctx, name.into().as_z3_symbol(ctx), sort.z3_sort),
+            )
+        }
+    }
+
+    pub fn fresh_const(ctx: &'ctx Context, prefix: &str, sort: &Sort<'ctx>) -> Self {
+        assert_eq!(ctx, sort.ctx);
+
+        let pp = CString::new(prefix).unwrap();
+        let p = pp.as_ptr();
+        unsafe { Self::wrap(ctx, Z3_mk_fresh_const(ctx.z3_ctx, p, sort.z3_sort)) }
+    }
 }
 
 impl<'ctx> Datatype<'ctx> {

z3/src/context.rs

@@ -1,3 +1,5 @@
+use std::ffi::{CStr, CString};
+use ast::Ast;
 use z3_sys::*;
 use Config;
 use Context;
@@ -29,6 +31,18 @@ impl Context {
     pub fn handle(&self) -> ContextHandle {
         ContextHandle { ctx: self }
     }
+
+    pub fn dump_smtlib<'ctx>(&'ctx self, formula: impl Ast<'ctx>) -> String {
+        let name = CString::new("").unwrap();
+        let logic = CString::new("").unwrap();
+        let status = CString::new("").unwrap();
+        let attributes = CString::new("").unwrap();
+        let assumptions: Vec<Z3_ast> = vec![];
+        unsafe {
+            let dump = Z3_benchmark_to_smtlib_string(self.z3_ctx, name.as_ptr(), logic.as_ptr(), status.as_ptr(), attributes.as_ptr(), 0, assumptions.as_ptr(), formula.get_z3_ast());
+            CStr::from_ptr(dump).to_str().unwrap().to_string()
+        }
+    }
 }
 
 impl<'ctx> ContextHandle<'ctx> {

z3/src/solver.rs

@@ -309,6 +309,35 @@ impl<'ctx> Solver<'ctx> {
             )
         }
     }
+
+    pub fn get_implied_equalities(&self, terms: &[&dyn Ast]) -> (Vec<u32>, SatResult) {
+        let mut group_ids = vec![0u32; terms.len()];
+        let terms: Vec<_> = terms.iter().map(|term| term.get_z3_ast()).collect();
+        let result = match unsafe {
+            Z3_get_implied_equalities(self.ctx.z3_ctx, self.z3_slv, terms.len() as u32, terms.as_ptr(), group_ids.as_mut_ptr())
+        } {
+            Z3_L_FALSE => SatResult::Unsat,
+            Z3_L_UNDEF => SatResult::Unknown,
+            Z3_L_TRUE => SatResult::Sat,
+            _ => unreachable!(),
+        };
+        (group_ids, result)
+    }
+
+    pub fn dump_smtlib(&self, formula: impl Ast<'ctx>) -> String {
+        let name = CString::new("").unwrap();
+        let logic = CString::new("").unwrap();
+        let status = CString::new("").unwrap();
+        let attributes = CString::new("").unwrap();
+        let ctx = self.ctx.z3_ctx;
+        let assertions = unsafe { z3_sys::Z3_solver_get_assertions(self.ctx.z3_ctx, self.z3_slv) };
+        let len = unsafe { z3_sys::Z3_ast_vector_size(ctx, assertions) };
+        let assumptions: Vec<_> = (0..len).map(|i| unsafe { z3_sys::Z3_ast_vector_get(ctx, assertions, i) }).collect();
+        unsafe {
+            let dump = Z3_benchmark_to_smtlib_string(self.ctx.z3_ctx, name.as_ptr(), logic.as_ptr(), status.as_ptr(), attributes.as_ptr(), len, assumptions.as_ptr(), formula.get_z3_ast());
+            CStr::from_ptr(dump).to_str().unwrap().to_string()
+        }
+    }
 }
 
 impl<'ctx> fmt::Display for Solver<'ctx> {