fix APIs, add python API

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

src/api/api_opt.cpp

@@ -18,6 +18,7 @@ Revision History:
 #include<iostream>
 #include"z3.h"
 #include"api_log_macros.h"
+#include"api_stats.h"
 #include"api_context.h"
 #include"api_util.h"
 #include"api_model.h"
@@ -25,6 +26,7 @@ Revision History:
 #include"cancel_eh.h"
 #include"scoped_timer.h"
 
+
 extern "C" {
 
     struct Z3_optimize_ref : public api::object {
@@ -207,33 +209,18 @@ extern "C" {
         Z3_CATCH_RETURN("");
     }
 
-
+    Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c,Z3_optimize d) {
-
+        Z3_TRY;
-#if 0
+        LOG_Z3_optimize_get_statistics(c, d);
-
+        RESET_ERROR_CODE();
-    /**
+        Z3_stats_ref * st = alloc(Z3_stats_ref);
-       \brief version with assumptions.
+        to_optimize_ref(d).collect_statistics(st->m_stats);
-
+        mk_c(c)->save_object(st);
-    */
+        Z3_stats r = of_stats(st);
-
+        RETURN_Z3(r);
-    void check_assumptions;
+        Z3_CATCH_RETURN(0);
-
-    /**
-       \brief retrieve the next answer. There are three modes:
-
-       - the optimization context has been configured to produce partial results.
-         It returns with L_UNDEF and an partial result and caller can retrieve
-         the results by querying get_lower and get_upper.
-       - The full result was produced and it returned L_TRUE. 
-         Retrieve the next result that has the same objective optimal.
-       - The context was configured to compute a Pareto front.
-         Search proceeds incrementally identifying feasible boxes.
-         Every return value is a new sub-box or set of sub-boxes.
-     */
-    void Z3_optimize_get_next(Z3_context c, Z3_optimize o) {
     }
-    
+
-    // 
+
-#endif
 
 };

src/api/dotnet/Fixedpoint.cs

@@ -305,6 +305,17 @@ namespace Microsoft.Z3
             }
         }
 
+        public Statistics Statistics
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<Statistics>() != null);
+
+                return new Statistics(Context, Native.Z3_fixedpoint_get_statistics(Context.nCtx, NativeObject));
+            }
+        }
+
+
 
         #region Internal
         internal Fixedpoint(Context ctx, IntPtr obj)

src/api/dotnet/Optimize.cs

@@ -150,11 +150,22 @@ namespace Microsoft.Z3
             return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
         }
 
-	    public override string ToString() 
+        public override string ToString() 
         {
             return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
         }
 
+        public Statistics Statistics
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<Statistics>() != null);
+
+                return new Statistics(Context, Native.Z3_optimize_get_statistics(Context.nCtx, NativeObject));
+            }
+        }
+
+x
         #region Internal
         internal Optimize(Context ctx, IntPtr obj)
             : base(ctx, obj)

src/api/python/z3.py

@@ -297,6 +297,10 @@ class AstRef(Z3PPObject):
         """Return a pointer to the corresponding C Z3_ast object."""
         return self.ast
 
+    def get_id(self):
+	"""Return unique identifier for object. It can be used for hash-tables and maps."""
+	return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+
     def ctx_ref(self):
         """Return a reference to the C context where this AST node is stored."""
         return self.ctx.ref()
@@ -447,6 +451,9 @@ class SortRef(AstRef):
     def as_ast(self):
         return Z3_sort_to_ast(self.ctx_ref(), self.ast)
 
+    def get_id(self):
+	return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+
     def kind(self):
         """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.
         
@@ -585,6 +592,9 @@ class FuncDeclRef(AstRef):
     def as_ast(self):
         return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
 
+    def get_id(self):
+	return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+
     def as_func_decl(self):
         return self.ast
 
@@ -730,6 +740,9 @@ class ExprRef(AstRef):
     def as_ast(self):
         return self.ast
 
+    def get_id(self):
+	return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+
     def sort(self):
         """Return the sort of expression `self`.
         
@@ -1505,6 +1518,9 @@ class PatternRef(ExprRef):
     def as_ast(self):
         return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
 
+    def get_id(self):
+	return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+
 def is_pattern(a):
     """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
 
@@ -1567,6 +1583,9 @@ class QuantifierRef(BoolRef):
     def as_ast(self):
         return self.ast
 
+    def get_id(self):
+	return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+
     def sort(self):
         """Return the Boolean sort."""
         return BoolSort(self.ctx)
@@ -6251,6 +6270,107 @@ class Fixedpoint(Z3PPObject):
         else:
             return Exists(self.vars, fml)
 
+
+#########################################
+#
+# Optimize
+#
+#########################################
+
+class OptimizeObjective:
+    def __init__(self, value):
+	self.value = value	
+
+class Optimize(Z3PPObject):
+    """Optimize API provides methods for solving using objective functions and weighted soft constraints"""
+     
+    def __init__(self, ctx=None):
+        self.ctx    = _get_ctx(ctx)
+	self.optimize = Z3_mk_optimize(self.ctx.ref())
+        Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
+
+    def __del__(self):
+        if self.optimize != None:
+            Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
+
+    def set(self, *args, **keys):
+        """Set a configuration option. The method `help()` return a string containing all available options.        
+        """
+        p = args2params(args, keys, self.ctx)
+        Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
+
+    def help(self):
+        """Display a string describing all available options."""
+        print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
+            
+    def param_descrs(self):
+        """Return the parameter description set."""
+        return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
+    
+    def assert_exprs(self, *args):
+        """Assert constraints as background axioms for the optimize solver."""
+        args = _get_args(args)
+        for arg in args:
+            if isinstance(arg, Goal) or isinstance(arg, AstVector):
+                for f in arg:
+                    Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
+            else:
+                Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
+
+    def add(self, *args):
+        """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
+        self.assert_exprs(*args)
+
+    def add_soft(self, arg, weight = None):
+	"""Add soft constraint with optional weight."""
+	pass
+
+    def maximize(self, arg):
+	"""Add objective function to maximize."""
+	return OptimizeObjective(Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()))
+
+    def minimize(self, arg):
+	"""Add objective function to minimize."""
+	return OptimizeObjective(Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()))
+
+    def check(self):
+	"""Check satisfiability while optimizing objective functions."""
+	return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize))
+
+    def model(self):
+	"""Return a model for the last check()."""
+	try:
+	    return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
+	except Z3Exception:
+	    raise Z3Exception("model is not available")
+
+    def lower(self, obj):
+	if not isinstance(obj, OptimizeObjective):
+	    raise Z3Exception("Expecting objective handle returned by maximize/minimize")
+	return _to_expr_ref(Z3_optimize_get_lower(self.ctx.ref(), self.optimize, obj.value), self.ctx)
+
+    def upper(self, obj):
+	if not isinstance(obj, OptimizeObjective):
+	    raise Z3Exception("Expecting objective handle returned by maximize/minimize")
+	return _to_expr_ref(Z3_optimize_get_upper(self.ctx.ref(), self.optimize, obj.value), self.ctx)    
+    
+    def __repr__(self):
+        """Return a formatted string with all added rules and constraints."""
+        return self.sexpr()
+
+    def sexpr(self):
+        """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.        
+        """
+        return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
+    
+    def statistics(self):
+        """Return statistics for the last `query()`.
+        """
+        return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
+
+
+        
+
 #########################################
 #
 # ApplyResult

src/api/python/z3types.py

@@ -78,6 +78,10 @@ class FixedpointObj(ctypes.c_void_p):
   def __init__(self, fixedpoint): self._as_parameter_ = fixedpoint
   def from_param(obj): return obj
 
+class OptimizeObj(ctypes.c_void_p):
+  def __init__(self, optimize): self._as_parameter_ = optimize
+  def from_param(obj): return obj
+
 class ModelObj(ctypes.c_void_p):
   def __init__(self, model): self._as_parameter_ = model
   def from_param(obj): return obj

src/api/z3_api.h

@@ -6107,6 +6107,12 @@ END_MLAPI_EXCLUDE
     */
     Z3_string Z3_API Z3_optimize_get_help(__in Z3_context c, __in Z3_optimize t);
 
+    /**
+       \brief Retrieve statistics information from the last call to #Z3_optimize_check
+
+       def_API('Z3_optimize_get_statistics', STATS, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    Z3_stats Z3_API Z3_optimize_get_statistics(__in Z3_context c,__in Z3_optimize d);
 
 
 #endif

src/opt/opt_solver.cpp

@@ -210,9 +210,10 @@ namespace opt {
     }
     
     smt::theory_var opt_solver::add_objective(app* term) {
-        m_objective_vars.push_back(get_optimizer().add_objective(term));
+        smt::theory_var v = get_optimizer().add_objective(term);
+        m_objective_vars.push_back(v);
         m_objective_values.push_back(inf_eps(rational(-1), inf_rational()));
-        return m_objective_vars.back();
+        return v;
     }
     
     vector<inf_eps> const& opt_solver::get_objective_values() {

src/opt/optsmt.cpp

@@ -219,7 +219,13 @@ namespace opt {
         }
 
         for (unsigned i = 0; i < m_objs.size(); ++i) {
-            m_vars.push_back(solver.add_objective(m_objs[i].get()));
+            smt::theory_var v = solver.add_objective(m_objs[i].get());
+            if (v == smt::null_theory_var) {
+                std::ostringstream out;
+                out << "Objective function '" << mk_pp(m_objs[i].get(), m) << "' is not supported";
+                throw default_exception(out.str());
+            }
+            m_vars.push_back(v);
         }            
     }
 

src/smt/theory_arith_aux.h

@@ -1061,6 +1061,9 @@ namespace smt {
         TRACE("opt", tout << mk_pp(term, get_manager()) << " |-> v" << v << "\n";);
         TRACE("opt", tout << "data-size: " << m_data.size() << "\n";);
         SASSERT(!is_quasi_base(v));
+        if (!is_linear(get_manager(), term)) {
+            v = null_theory_var;
+        }
         return v;
     }
 

src/smt/theory_dense_diff_logic_def.h

@@ -1000,7 +1000,10 @@ namespace smt {
         theory_var result = m_objectives.size();
         rational q(1), r(0);
         expr_ref_vector vr(get_manager());
-        if (internalize_objective(term, q, r, objective)) {
+        if (!is_linear(get_manager(), term)) {
+            result = null_theory_var;
+        }
+        else if (internalize_objective(term, q, r, objective)) {
             m_objectives.push_back(objective);
             m_objective_consts.push_back(r);
             m_objective_assignments.push_back(vr);

src/smt/theory_diff_logic_def.h

@@ -1173,7 +1173,10 @@ theory_var theory_diff_logic<Ext>::add_objective(app* term) {
     theory_var result = m_objectives.size();
     rational q(1), r(0);
     expr_ref_vector vr(get_manager());
-    if (internalize_objective(term, q, r, objective)) {
+    if (!is_linear(get_manager(), term)) {
+        result = null_theory_var;
+    }
+    else if (internalize_objective(term, q, r, objective)) {
         m_objectives.push_back(objective);
         m_objective_consts.push_back(r);
         m_objective_assignments.push_back(vr);

src/smt/theory_opt.h

@@ -20,6 +20,7 @@ Notes:
 
 #include "inf_rational.h"
 #include "inf_eps_rational.h"
+#include "arith_decl_plugin.h"
 
 #ifndef _THEORY_OPT_H_
 #define _THEORY_OPT_H_
@@ -29,9 +30,11 @@ namespace smt {
     class theory_opt {
     public:
         typedef inf_eps_rational<inf_rational> inf_eps;
-        virtual inf_eps maximize(theory_var v, expr_ref& blocker) = 0; // { UNREACHABLE(); return inf_eps::infinity(); }
+        virtual inf_eps maximize(theory_var v, expr_ref& blocker) = 0; 
-        virtual theory_var add_objective(app* term) { UNREACHABLE(); return null_theory_var; }
+        virtual theory_var add_objective(app* term) = 0;
         virtual expr* mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val) { UNREACHABLE(); return 0; }
+        bool is_linear(ast_manager& m, expr* term);
+        bool is_numeral(arith_util& a, expr* term);
     };
 }