fix #1577

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_opt.cpp

@@ -124,10 +124,16 @@ extern "C" {
     }
 
 
-    Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o) {
+    Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[]) {
         Z3_TRY;
-        LOG_Z3_optimize_check(c, o);
+        LOG_Z3_optimize_check(c, o, num_assumptions, assumptions);
         RESET_ERROR_CODE();
+        for (unsigned i = 0; i < num_assumptions; i++) {
+            if (!is_expr(to_ast(assumptions[i]))) {
+                SET_ERROR_CODE(Z3_INVALID_ARG, "assumption is not an expression");
+                return Z3_L_UNDEF;
+            }
+        }
         lbool r = l_undef;
         cancel_eh<reslimit> eh(mk_c(c)->m().limit());
         unsigned timeout = to_optimize_ptr(o)->get_params().get_uint("timeout", mk_c(c)->get_timeout());
@@ -137,7 +143,9 @@ extern "C" {
             scoped_timer timer(timeout, &eh);
             scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
             try {
-                r = to_optimize_ptr(o)->optimize();
+                expr_ref_vector asms(mk_c(c)->m());
+                asms.append(num_assumptions, to_exprs(assumptions));
+                r = to_optimize_ptr(o)->optimize(asms);
             }
             catch (z3_exception& ex) {
                 if (!mk_c(c)->m().canceled()) {
@@ -157,6 +165,22 @@ extern "C" {
         Z3_CATCH_RETURN(Z3_L_UNDEF);
     }
 
+    Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o) {
+        Z3_TRY;
+        LOG_Z3_optimize_get_unsat_core(c, o);
+        RESET_ERROR_CODE();
+        expr_ref_vector core(mk_c(c)->m());
+        to_optimize_ptr(o)->get_unsat_core(core);
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
+        mk_c(c)->save_object(v);
+        for (expr* e : core) {
+            v->m_ast_vector.push_back(e);
+        }
+        RETURN_Z3(of_ast_vector(v));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+
     Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize o) {
         Z3_TRY;
         LOG_Z3_optimize_to_string(c, o);

src/api/c++/z3++.h

@@ -2455,8 +2455,19 @@ namespace z3 {
         void pop() {
             Z3_optimize_pop(ctx(), m_opt);
         }
-        check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt); check_error(); return to_check_result(r); }
+        check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt, 0, 0); check_error(); return to_check_result(r); }
+        check_result check(expr_vector const& asms) { 
+            array<Z3_ast> _asms(n);
+            for (unsigned i = 0; i < n; i++) {
+                check_context(*this, asms[i]);
+                _asms[i] = asms[i];
+            }
+            Z3_lbool r = Z3_optimize_check(ctx(), m_opt, n, _asms.ptr()); 
+            check_error(); 
+            return to_check_result(r); 
+        }
         model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
+        expr_vector unsat_core() const { Z3_ast_vector r = Z3_optimize_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
         void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
         expr lower(handle const& h) {
             Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());

src/api/dotnet/Optimize.cs

@@ -183,9 +183,9 @@ namespace Microsoft.Z3
         /// don't use strict inequalities) meets the objectives.
         /// </summary>
         ///
-        public Status Check()
+        public Status Check(params Expr[] assumptions)
         {
-            Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject);
+            Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
             switch (r)
             {
                 case Z3_lbool.Z3_L_TRUE:
@@ -236,6 +236,25 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// The unsat core of the last <c>Check</c>.
+        /// </summary>
+        /// <remarks>
+        /// The unsat core is a subset of <c>assumptions</c>
+        /// The result is empty if <c>Check</c> was not invoked before,
+        /// if its results was not <c>UNSATISFIABLE</c>, or if core production is disabled.
+        /// </remarks>
+        public BoolExpr[] UnsatCore
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<Expr[]>() != null);
+
+                ASTVector core = new ASTVector(Context, Native.Z3_optimize_get_unsat_core(Context.nCtx, NativeObject));                
+                return core.ToBoolExprArray();
+            }
+        }
+
         /// <summary>
         /// Declare an arithmetical maximization objective.
         /// Return a handle to the objective. The handle is used as

src/api/java/Optimize.java

@@ -161,9 +161,23 @@ public class Optimize extends Z3Object {
      * Produce a model that (when the objectives are bounded and 
      * don't use strict inequalities) meets the objectives.
      **/
-    public Status Check()
+    public Status Check(Expr... assumptions)
     {
-        Z3_lbool r = Z3_lbool.fromInt(Native.optimizeCheck(getContext().nCtx(), getNativeObject()));
+        Z3_lbool r;
+        if (assumptions == null) {
+          r = Z3_lbool.fromInt(
+              Native.optimizeCheck(
+                  getContext().nCtx(), 
+                  getNativeObject(), 0, null);
+        }
+        else {
+          r = Z3_lbool.fromInt(
+              Native.optimizeCheck(
+                  getContext().nCtx(), 
+                  getNativeObject(), 
+                  assumptions.length, 
+                  AST.arrayToNative(assumptions)));
+        }
         switch (r) {
             case Z3_L_TRUE:
                 return Status.SATISFIABLE;
@@ -209,6 +223,21 @@ public class Optimize extends Z3Object {
         }
     }
 
+    /**
+     * The unsat core of the last {@code Check}.
+     * Remarks:  The unsat core
+     * is a subset of {@code Assumptions} The result is empty if
+     * {@code Check} was not invoked before, if its results was not
+     * {@code UNSATISFIABLE}, or if core production is disabled. 
+     * 
+     * @throws Z3Exception
+     **/
+    public BoolExpr[] getUnsatCore()
+    {
+        ASTVector core = new ASTVector(getContext(), Native.optimizeGetUnsatCore(getContext().nCtx(), getNativeObject()));        
+        return core.ToBoolExprArray();
+    }
+
     /**
      *  Declare an arithmetical maximization objective.
      *  Return a handle to the objective. The handle is used as

src/api/ml/z3.ml

@@ -1947,7 +1947,7 @@ struct
   let minimize (x:optimize) (e:Expr.expr) = mk_handle x (Z3native.optimize_minimize (gc x) x e)
 
   let check (x:optimize) =
-    let r = lbool_of_int (Z3native.optimize_check (gc x) x) in
+    let r = lbool_of_int (Z3native.optimize_check (gc x) x) 0 [] in
     match r with
     | L_TRUE -> Solver.SATISFIABLE
     | L_FALSE -> Solver.UNSATISFIABLE

src/api/python/z3/z3.py

@@ -7311,10 +7311,15 @@ class Optimize(Z3PPObject):
         """restore to previously created backtracking point"""
         Z3_optimize_pop(self.ctx.ref(), self.optimize)
 
-    def check(self):
+    def check(self, *assumptions):
         """Check satisfiability while optimizing objective functions."""
-        return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize))
-
+        assumptions = _get_args(assumptions)
+        num = len(assumptions)
+        _assumptions = (Ast * num)()
+        for i in range(num):
+            _assumptions[i] = assumptions[i].as_ast()
+        return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
+    
     def reason_unknown(self):
         """Return a string that describes why the last `check()` returned `unknown`."""
         return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
@@ -7326,6 +7331,9 @@ class Optimize(Z3PPObject):
         except Z3Exception:
             raise Z3Exception("model is not available")
 
+    def unsat_core(self):
+        return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
+
     def lower(self, obj):
         if not isinstance(obj, OptimizeObjective):
             raise Z3Exception("Expecting objective handle returned by maximize/minimize")

src/api/z3_optimization.h

@@ -117,10 +117,12 @@ extern "C" {
        \brief Check consistency and produce optimal values.
        \param c - context
        \param o - optimization context
+       \param num_assumptions - number of additional assumptions
+       \param assumptions - the additional assumptions
 
-       def_API('Z3_optimize_check', INT, (_in(CONTEXT), _in(OPTIMIZE)))
+       def_API('Z3_optimize_check', INT, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT), _in_array(2, AST)))
     */
-    Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o);
+    Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[]);
 
 
     /**
@@ -143,6 +145,14 @@ extern "C" {
     */
     Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o);
 
+    /**
+       \brief Retrieve the unsat core for the last #Z3_optimize_chec
+       The unsat core is a subset of the assumptions \c a.
+
+       def_API('Z3_optimize_get_unsat_core', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE)))       
+     */
+    Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o);
+
     /**
        \brief Set parameters on optimization context.