Z3 Optimize: add assert_and_track and get_unsat_core (#300)

Add some missing optimize APIs

z3/src/optimize.rs

@@ -1,3 +1,4 @@
+use log::debug;
 use std::convert::TryInto;
 use std::ffi::{CStr, CString};
 use std::fmt;
@@ -50,6 +51,26 @@ impl<'ctx> Optimize<'ctx> {
         unsafe { Z3_optimize_assert(self.ctx.z3_ctx, self.z3_opt, ast.get_z3_ast()) };
     }
 
+    /// Assert a constraint `a` into the solver, and track it (in the
+    /// unsat) core using the Boolean constant `p`.
+    ///
+    /// This API is an alternative to
+    /// [`Optimize::check()`]
+    /// for extracting unsat cores. Both APIs can be used in the same solver.
+    /// The unsat core will contain a combination of the Boolean variables
+    /// provided using [`Optimize::assert_and_track()`]
+    /// and the Boolean literals provided using
+    /// [`Optimize::check()`].
+    ///
+    /// # See also:
+    ///
+    /// - [`Optimize::assert()`]
+    /// - [`Optimize::assert_soft()`]
+    pub fn assert_and_track(&self, ast: &Bool<'ctx>, p: &Bool<'ctx>) {
+        debug!("assert_and_track: {:?}", ast);
+        unsafe { Z3_optimize_assert_and_track(self.ctx.z3_ctx, self.z3_opt, ast.z3_ast, p.z3_ast) };
+    }
+
     /// Assert soft constraint to the optimization context.
     /// Weight is a positive, rational penalty for violating the constraint.
     /// Group is an optional identifier to group soft constraints.
@@ -105,6 +126,45 @@ impl<'ctx> Optimize<'ctx> {
         unsafe { Z3_optimize_minimize(self.ctx.z3_ctx, self.z3_opt, ast.get_z3_ast()) };
     }
 
+    /// Return a subset of the assumptions provided to either the last
+    ///
+    /// * [`Optimize::check`] call, or
+    /// * sequence of [`Optimize::assert_and_track`] calls followed
+    ///   by an [`Optimize::check`] call.
+    ///
+    /// These are the assumptions Z3 used in the unsatisfiability proof.
+    /// Assumptions are available in Z3. They are used to extract unsatisfiable
+    /// cores.  They may be also used to "retract" assumptions. Note that,
+    /// assumptions are not really "soft constraints", but they can be used to
+    /// implement them.
+    ///
+    /// By default, the unsat core will not be minimized. Generation of a minimized
+    /// unsat core can be enabled via the `"sat.core.minimize"` and `"smt.core.minimize"`
+    /// settings for SAT and SMT cores respectively. Generation of minimized unsat cores
+    /// will be more expensive.
+    ///
+    /// # See also:
+    ///
+    /// - [`Optimize::check`]
+    pub fn get_unsat_core(&self) -> Vec<Bool<'ctx>> {
+        let z3_unsat_core = unsafe { Z3_optimize_get_unsat_core(self.ctx.z3_ctx, self.z3_opt) };
+        if z3_unsat_core.is_null() {
+            return vec![];
+        }
+
+        let len = unsafe { Z3_ast_vector_size(self.ctx.z3_ctx, z3_unsat_core) };
+
+        let mut unsat_core = Vec::with_capacity(len as usize);
+
+        for i in 0..len {
+            let elem = unsafe { Z3_ast_vector_get(self.ctx.z3_ctx, z3_unsat_core, i) };
+            let elem = unsafe { Bool::wrap(self.ctx, elem) };
+            unsat_core.push(elem);
+        }
+
+        unsat_core
+    }
+
     /// Create a backtracking point.
     ///
     /// The optimize solver contains a set of rules, added facts and assertions.

z3/tests/lib.rs

@@ -771,6 +771,53 @@ fn test_get_unsat_core() {
     assert!(unsat_core.contains(&x_is_five));
 }
 
+#[test]
+fn test_optimize_get_unsat_core() {
+    let _ = env_logger::try_init();
+
+    let cfg = Config::new();
+    let ctx = Context::new(&cfg);
+    let optimize = Optimize::new(&ctx);
+
+    assert!(
+        optimize.get_unsat_core().is_empty(),
+        "no unsat core before assertions"
+    );
+
+    let x = Int::new_const(&ctx, "x");
+
+    let x_is_three = Bool::new_const(&ctx, "x-is-three");
+    optimize.assert_and_track(&x._eq(&Int::from_i64(&ctx, 3)), &x_is_three);
+
+    let x_is_five = Bool::new_const(&ctx, "x-is-five");
+    optimize.assert_and_track(&x._eq(&Int::from_i64(&ctx, 5)), &x_is_five);
+
+    assert!(
+        optimize.get_unsat_core().is_empty(),
+        "no unsat core before checking"
+    );
+
+    let result = optimize.check(&[]);
+    assert_eq!(result, SatResult::Unsat);
+
+    let unsat_core = optimize.get_unsat_core();
+    assert_eq!(unsat_core.len(), 2);
+    assert!(unsat_core.contains(&x_is_three));
+    assert!(unsat_core.contains(&x_is_five));
+
+    // try check API
+
+    let a = x._eq(&Int::from_i64(&ctx, 4));
+    let b = x._eq(&Int::from_i64(&ctx, 6));
+    let result = optimize.check(&[a.clone(), b.clone()]);
+    assert_eq!(result, SatResult::Unsat);
+
+    let unsat_core = optimize.get_unsat_core();
+    assert_eq!(unsat_core.len(), 2);
+    assert!(unsat_core.contains(&a));
+    assert!(unsat_core.contains(&b));
+}
+
 #[test]
 fn test_datatype_builder() {
     let _ = env_logger::try_init();