From 5a95c9f99c47102cc32e7e2c10cd5fd314412f31 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Mon, 13 Mar 2023 10:42:01 -0400
Subject: [PATCH] Z3_{solver/optimize}_from_string fixes

---
 z3-sys/src/lib.rs  |  2 +-
 z3/src/optimize.rs | 15 ++++-----------
 z3/src/solver.rs   | 15 ++++-----------
 z3/tests/lib.rs    |  6 ++++--
 4 files changed, 13 insertions(+), 25 deletions(-)

diff --git a/z3-sys/src/lib.rs b/z3-sys/src/lib.rs
index 7f5b18ef..e9ba970d 100644
--- a/z3-sys/src/lib.rs
+++ b/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;
diff --git a/z3/src/optimize.rs b/z3/src/optimize.rs
index d691e3ff..0c3b96cb 100644
--- a/z3/src/optimize.rs
+++ b/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());
         }
     }
 
diff --git a/z3/src/solver.rs b/z3/src/solver.rs
index b8fa86c2..12699398 100644
--- a/z3/src/solver.rs
+++ b/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>> {
diff --git a/z3/tests/lib.rs b/z3/tests/lib.rs
index 6eda73fa..d06636f9 100644
--- a/z3/tests/lib.rs
+++ b/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);
 }