src/api/java/Optimize.java

Go to the documentation of this file.

package com.microsoft.z3;

import com.microsoft.z3.enumerations.Z3_lbool;


public class Optimize extends Z3Object
{
    public String getHelp()
    {
        return Native.optimizeGetHelp(getContext().nCtx(), getNativeObject());
    }

    public void setParameters(Params value)
    {
        Native.optimizeSetParams(getContext().nCtx(), getNativeObject(), value.getNativeObject());
    }

    public ParamDescrs getParameterDescriptions()
    {
        return new ParamDescrs(getContext(), Native.optimizeGetParamDescrs(getContext().nCtx(), getNativeObject())); 
    }

    public void Assert(BoolExpr ... constraints)
    {
        getContext().checkContextMatch(constraints);
        for (BoolExpr a : constraints)
        {
            Native.optimizeAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject());
        }
    }

    public void Add(BoolExpr ... constraints)
    {
        Assert(constraints);
    }
    
    public class Handle
    {
        Optimize opt;
        int handle;
        Handle(Optimize opt, int h)
        {
            this.opt = opt;
            this.handle = h;
        }
        
        public ArithExpr getLower()
        {
            return opt.GetLower(handle); 
        }
        
        public ArithExpr getUpper()
        {
            return opt.GetUpper(handle); 
        }
        
        public ArithExpr getValue()
        {
            return getLower(); 
        }

        public String toString() 
        {
            return getValue().toString();
        }
    }

    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()));
    }
    

    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;
        }
    }
    
    public void Push()
    {
        Native.optimizePush(getContext().nCtx(), getNativeObject());
    }


    public void Pop()
    {
        Native.optimizePop(getContext().nCtx(), getNativeObject());
    }


    public Model getModel()
    {
        long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
        if (x == 0)
            return null;
        else
            return new Model(getContext(), x);
    }

    public Handle MkMaximize(ArithExpr e)
    {
        return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
    }
    
    public Handle MkMinimize(ArithExpr e)
    {
        return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
    }
    
    private ArithExpr GetLower(int index)
    {
        return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
    }
    
    
    private ArithExpr GetUpper(int index)
    {
        return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
    }

    public String getReasonUnknown()
    {
        return Native.optimizeGetReasonUnknown(getContext().nCtx(),
                getNativeObject());     
    }
    
    
    public String toString()
    {
        return Native.optimizeToString(getContext().nCtx(), getNativeObject());
    }
    
    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);
    }

}