Z3_{solver/optimize}_from_string fixes

z3-sys/src/lib.rs

@@ -5566,7 +5566,7 @@ extern "C" {
     ///
     /// - [`Z3_solver_from_file`]
     /// - [`Z3_solver_to_string`]
-    pub fn Z3_solver_from_string(c: Z3_context, s: Z3_solver, file_name: Z3_string);
+    pub fn Z3_solver_from_string(c: Z3_context, s: Z3_solver, c_str: Z3_string);
 
     /// Return the set of asserted formulas on the solver.
     pub fn Z3_solver_get_assertions(c: Z3_context, s: Z3_solver) -> Z3_ast_vector;

z3/src/optimize.rs

@@ -28,18 +28,11 @@ impl<'ctx> Optimize<'ctx> {
     }
 
     /// Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives.
-    /// Add the parsed constraints and objectives to a new created optimization context.
-    pub fn new_from_smtlib2(ctx: &'ctx Context, source_string: String) -> Optimize<'ctx> {
+    /// Add the parsed constraints and objectives to the optimizer.
+    pub fn from_string<T: Into<Vec<u8>>>(&self, source_string: T) {
         let source_cstring = CString::new(source_string).unwrap();
-        Optimize {
-            ctx,
-            z3_opt: unsafe {
-                let _guard = Z3_MUTEX.lock().unwrap();
-                let opt = Z3_mk_optimize(ctx.z3_ctx);
-                Z3_optimize_inc_ref(ctx.z3_ctx, opt);
-                Z3_optimize_from_string(ctx.z3_ctx, opt, source_cstring.as_ptr());
-                opt
-            },
+        unsafe {
+            Z3_optimize_from_string(self.ctx.z3_ctx, self.z3_opt, source_cstring.as_ptr());
         }
     }
 

z3/src/solver.rs

@@ -53,21 +53,14 @@ impl<'ctx> Solver<'ctx> {
     }
 
     /// Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives.
-    /// Add the parsed constraints and objectives to a new created solver context.
-    pub fn new_from_smtlib2(ctx: &'ctx Context, source_string: String) -> Solver<'ctx> {
+    /// Add the parsed constraints and objectives to the solver.
+    pub fn from_string<T: Into<Vec<u8>>>(&self, source_string: T) {
         let source_cstring = CString::new(source_string).unwrap();
-        Solver {
-            ctx,
-            z3_slv: unsafe {
-                let _guard = Z3_MUTEX.lock().unwrap();
-                let opt = Z3_mk_solver(ctx.z3_ctx);
-                Z3_solver_from_string(ctx.z3_ctx, opt, source_cstring.as_ptr());
-                opt
-            },
+        unsafe {
+            Z3_solver_from_string(self.ctx.z3_ctx, self.z3_slv, source_cstring.as_ptr());
         }
     }
 
-
     /// Create a new solver customized for the given logic.
     /// It returns `None` if the logic is unknown or unsupported.
     pub fn new_for_logic<S: Into<Symbol>>(ctx: &'ctx Context, logic: S) -> Option<Solver<'ctx>> {

z3/tests/lib.rs

@@ -243,7 +243,8 @@ fn test_solver_new_from_smtlib2() {
 (assert (=( -(+(* 3 x) (* 2 y)) z) 1))
 (assert (=(+( -(* 2 x) (* 2 y)) (* 4 z)) -2))
 "#;
-    let solver = Solver::new_from_smtlib2(&ctx, problem.into());
+    let solver = Solver::new(&ctx);
+    solver.from_string(problem);
     assert_eq!(solver.check(), SatResult::Sat);
 }
 
@@ -706,7 +707,8 @@ fn test_optimize_new_from_smtlib2() {
 (assert (=( -(+(* 3 x) (* 2 y)) z) 1))
 (assert (=(+( -(* 2 x) (* 2 y)) (* 4 z)) -2))
 "#;
-    let optimize = Optimize::new_from_smtlib2(&ctx, problem.into());
+    let optimize = Optimize::new(&ctx);
+    optimize.from_string(problem);
     assert_eq!(optimize.check(&[]), SatResult::Sat);
 }