Expose API to convert solver into SMT-LIB2 format (#267)

Expose API to convert solver into SMT-LIB2 format

z3/src/solver.rs

@@ -309,6 +309,43 @@ impl<'ctx> Solver<'ctx> {
  )
  }
  }
+
+ pub fn to_smt2(&self) -> String {
+ let name = CString::new("benchmark generated from rust API").unwrap();
+ let logic = CString::new("").unwrap();
+ let status = CString::new("unknown").unwrap();
+ let attributes = CString::new("").unwrap();
+ let assumptions = self.get_assertions();
+ let mut num_assumptions = assumptions.len() as u32;
+ let formula = if num_assumptions > 0 {
+ num_assumptions -= 1;
+ assumptions[num_assumptions as usize].z3_ast
+ } else {
+ ast::Bool::from_bool(self.ctx, true).z3_ast
+ };
+ let z3_assumptions = assumptions.iter().map(|a| a.z3_ast).collect::<Vec<_>>();
+
+ let p = unsafe {
+ Z3_benchmark_to_smtlib_string(
+ self.ctx.z3_ctx,
+ name.as_ptr(),
+ logic.as_ptr(),
+ status.as_ptr(),
+ attributes.as_ptr(),
+ num_assumptions,
+ z3_assumptions.as_ptr(),
+ formula,
+ )
+ };
+ if p.is_null() {
+ return String::new();
+ }
+ unsafe { CStr::from_ptr(p) }
+ .to_str()
+ .ok()
+ .map(|s| s.to_string())
+ .unwrap_or_else(String::new)
+ }
 }
 
 impl<'ctx> fmt::Display for Solver<'ctx> {

z3/tests/lib.rs

@@ -258,6 +258,20 @@ fn test_solver_new_from_smtlib2() {
  assert_eq!(solver.check(), SatResult::Sat);
 }
 
+#[test]
+fn test_solver_to_smtlib2() {
+ let cfg = Config::new();
+ let ctx = Context::new(&cfg);
+ let solver1 = Solver::new(&ctx);
+ let t1 = ast::Bool::from_bool(&ctx, true);
+ let t2 = ast::Bool::from_bool(&ctx, true);
+ solver1.assert(&t1._eq(&t2));
+ let s1_smt2 = solver1.to_smt2();
+ let solver2 = Solver::new(&ctx);
+ solver2.from_string(s1_smt2);
+ assert_eq!(solver2.check(), solver1.check());
+}
+
 #[test]
 fn test_solver_translate() {
  let cfg = Config::new();