Z3 from string

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

@@ -27,6 +27,15 @@ impl<'ctx> Optimize<'ctx> {
         unsafe { Self::wrap(ctx, Z3_mk_optimize(ctx.z3_ctx)) }
     }
 
+    /// Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives.
+    /// 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();
+        unsafe {
+            Z3_optimize_from_string(self.ctx.z3_ctx, self.z3_opt, source_cstring.as_ptr());
+        }
+    }
+
     /// Get this optimizers 's context.
     pub fn get_context(&self) -> &'ctx Context {
         self.ctx

z3/src/solver.rs

@@ -1,6 +1,6 @@
 use ast;
 use ast::Ast;
-use std::ffi::CStr;
+use std::ffi::{CStr, CString};
 use std::fmt;
 use z3_sys::*;
 use Context;
@@ -52,6 +52,15 @@ impl<'ctx> Solver<'ctx> {
         unsafe { Self::wrap(ctx, Z3_mk_solver(ctx.z3_ctx)) }
     }
 
+    /// Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives.
+    /// 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();
+        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

@@ -232,6 +232,22 @@ fn test_ast_translate() {
     assert_eq!(slv.check(), SatResult::Unsat);
 }
 
+#[test]
+fn test_solver_new_from_smtlib2() {
+    let cfg = Config::new();
+    let ctx = Context::new(&cfg);
+    let problem = r#"
+(declare -const x Real)
+(declare -const y Real)
+(declare -const z Real)
+(assert (=( -(+(* 3 x) (* 2 y)) z) 1))
+(assert (=(+( -(* 2 x) (* 2 y)) (* 4 z)) -2))
+"#;
+    let solver = Solver::new(&ctx);
+    solver.from_string(problem);
+    assert_eq!(solver.check(), SatResult::Sat);
+}
+
 #[test]
 fn test_solver_translate() {
     let cfg = Config::new();
@@ -679,6 +695,23 @@ fn test_optimize_unknown() {
     assert!(optimize.get_reason_unknown().is_some());
 }
 
+#[test]
+fn test_optimize_new_from_smtlib2() {
+    let _ = env_logger::try_init();
+    let cfg = Config::new();
+    let ctx = Context::new(&cfg);
+    let problem = r#"
+(declare -const x Real)
+(declare -const y Real)
+(declare -const z Real)
+(assert (=( -(+(* 3 x) (* 2 y)) z) 1))
+(assert (=(+( -(* 2 x) (* 2 y)) (* 4 z)) -2))
+"#;
+    let optimize = Optimize::new(&ctx);
+    optimize.from_string(problem);
+    assert_eq!(optimize.check(&[]), SatResult::Sat);
+}
+
 #[test]
 fn test_get_unsat_core() {
     let _ = env_logger::try_init();