add java Optimize context

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

src/api/java/Optimize.java

@@ -0,0 +1,261 @@
+/**
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    Optimize.java
+
+Abstract:
+
+    Z3 Java API: Optimizes
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-07-16
+
+Notes:
+    
+**/
+
+package com.microsoft.z3;
+
+import com.microsoft.z3.enumerations.Z3_lbool;
+
+
+/**
+ * Object for managing optimizization context
+ **/
+public class Optimize extends Z3Object
+{
+    /**
+     * A string that describes all available optimize solver parameters.
+     **/
+    public String getHelp()
+    {
+	return Native.optimizeGetHelp(getContext().nCtx(), getNativeObject());
+    }
+
+    /**
+     * Sets the optimize solver parameters.
+     *
+     * @throws Z3Exception
+     **/
+    public void setParameters(Params value)
+    {
+	Native.optimizeSetParams(getContext().nCtx(), getNativeObject(), value.getNativeObject());
+    }
+
+    /**
+     * Retrieves parameter descriptions for Optimize solver.
+     **/
+    public ParamDescrs getParameterDescriptions()
+    {
+	return new ParamDescrs(getContext(), Native.optimizeGetParamDescrs(getContext().nCtx(), getNativeObject())); 
+    }
+
+    /**
+     * Assert a constraint (or multiple) into the optimize solver.
+     **/        
+    public void Assert(BoolExpr ... constraints)
+    {
+        getContext().checkContextMatch(constraints);
+        for (BoolExpr a : constraints)
+        {
+            Native.optimizeAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject());
+        }
+    }
+
+    /**
+     * Alias for Assert.
+     **/        
+    public void Add(BoolExpr ... constraints)
+    {
+	Assert(constraints);
+    }
+    
+    /**
+     * Handle to objectives returned by objective functions.
+     **/
+    public class Handle
+    {
+	Optimize opt;
+	int handle;
+	Handle(Optimize opt, int h)
+	{
+	    this.opt = opt;
+	    this.handle = h;
+	}
+	
+	/**
+	 * Retrieve a lower bound for the objective handle.
+	 **/        	   	
+	public ArithExpr getLower()
+	{
+	    return opt.GetLower(handle); 
+	}
+	
+	/**            
+	 * Retrieve an upper bound for the objective handle.
+	 **/        	   	
+	public ArithExpr getUpper()
+	{
+	    return opt.GetUpper(handle); 
+	}
+	
+	/**
+	 * Retrieve the value of an objective.
+	 **/        	   	
+	public ArithExpr getValue()
+	{
+	    return getLower(); 
+	}
+    }
+
+    /**        
+     * Assert soft constraint
+     *
+     * Return an objective which associates with the group of constraints.
+     *
+     **/        
+
+    public Handle AssertSoft(BoolExpr constraint, int weight, String group)
+    {
+	getContext().checkContextMatch(constraint);
+	Symbol s = getContext().mkSymbol(group);
+	return new Handle(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
+    }
+    
+
+    /**        
+     * Check satisfiability of asserted constraints.
+     * Produce a model that (when the objectives are bounded and 
+     * don't use strict inequalities) meets the objectives.
+     **/
+
+    public Status Check()
+    {
+	Z3_lbool r = Z3_lbool.fromInt(Native.optimizeCheck(getContext().nCtx(), getNativeObject()));
+	switch (r) {
+	case Z3_L_TRUE:
+	    return Status.SATISFIABLE;
+	case Z3_L_FALSE:
+	    return Status.UNSATISFIABLE;
+	default:
+	    return Status.UNKNOWN;
+	}
+    }
+    
+    /**
+     * Creates a backtracking point.
+     **/
+    public void Push()
+    {
+	Native.optimizePush(getContext().nCtx(), getNativeObject());
+    }
+
+
+    /** 
+     * Backtrack one backtracking point.
+     *
+     * Note that an exception is thrown if Pop is called without a corresponding Push.
+     **/
+     
+    public void Pop()
+    {
+	Native.optimizePop(getContext().nCtx(), getNativeObject());
+    }
+
+
+    /**
+     * The model of the last Check.
+     *
+     * The result is null if Check was not invoked before,
+     * if its results was not SATISFIABLE, or if model production is not enabled.
+     **/
+    public Model getModel()
+    {
+	long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
+	if (x == 0)
+	    return null;
+	else
+	    return new Model(getContext(), x);
+    }
+
+    /** 
+     *  Declare an arithmetical maximization objective.
+     *  Return a handle to the objective. The handle is used as
+     *  to retrieve the values of objectives after calling Check.
+     **/        	
+    public Handle MkMaximize(ArithExpr e)
+    {
+	return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
+    }
+    
+    /**
+     *  Declare an arithmetical minimization objective. 
+     *  Similar to MkMaximize.
+     **/        	
+    public Handle MkMinimize(ArithExpr e)
+    {
+	return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
+    }
+    
+    /**
+     *  Retrieve a lower bound for the objective handle.
+     **/        	
+    private ArithExpr GetLower(int index)
+    {
+	return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
+    }
+    
+    
+    /**
+     *  Retrieve an upper bound for the objective handle.
+     **/        	
+    private ArithExpr GetUpper(int index)
+    {
+	return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
+    }
+    
+    
+    /**
+     *  Print the context to a String (SMT-LIB parseable benchmark).
+     **/        	
+    public String toString()
+    {
+	return Native.optimizeToString(getContext().nCtx(), getNativeObject());
+    }
+    
+    /**
+     *  Optimize statistics.
+     **/
+    public Statistics getStatistics()
+    {
+	return new Statistics(getContext(), Native.optimizeGetStatistics(getContext().nCtx(), getNativeObject()));
+    }
+
+
+    Optimize(Context ctx, long obj) throws Z3Exception
+    {
+	super(ctx, obj);
+    }
+
+    Optimize(Context ctx) throws Z3Exception
+    {
+	super(ctx, Native.mkOptimize(ctx.nCtx()));
+    }
+
+    
+    void incRef(long o)
+    {
+        getContext().getOptimizeDRQ().incAndClear(getContext(), o);
+        super.incRef(o);
+    }
+
+    void decRef(long o)
+    {
+        getContext().getOptimizeDRQ().add(o);
+        super.decRef(o);
+    }
+
+}

src/api/java/OptimizeDecRefQueue.java

@@ -0,0 +1,53 @@
+/**
+Copyright (c) 2012-2015 Microsoft Corporation
+   
+Module Name:
+
+    OptimizeDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
+
+package com.microsoft.z3;
+
+class OptimizeDecRefQueue extends IDecRefQueue
+{
+    public OptimizeDecRefQueue() 
+    {
+        super();
+    }
+
+    public OptimizeDecRefQueue(int move_limit) 
+    {
+        super(move_limit);
+    }
+
+    protected void incRef(Context ctx, long obj)
+    {
+        try
+        {
+            Native.fixedpointIncRef(ctx.nCtx(), obj);
+        } catch (Z3Exception e)
+        {
+            // OK.
+        }
+    }
+
+    protected void decRef(Context ctx, long obj)
+    {
+        try
+        {
+            Native.fixedpointDecRef(ctx.nCtx(), obj);
+        } catch (Z3Exception e)
+        {
+            // OK.
+        }
+    }
+};