Optimize.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
import com.microsoft.z3.enumerations.Z3_lbool;
 
import java.lang.ref.ReferenceQueue;
 
 
@SuppressWarnings("unchecked")
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(Expr<BoolSort>... constraints)
    {
        getContext().checkContextMatch(constraints);
        for (Expr<BoolSort> a : constraints)
        {
            Native.optimizeAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject());
        }
    }
 
    public void Add(Expr<BoolSort>... constraints)
    {
        Assert(constraints);
    }
 
    public void AssertAndTrack(Expr<BoolSort> constraint, Expr<BoolSort> p)
    {
        getContext().checkContextMatch(constraint);
        getContext().checkContextMatch(p);
 
        Native.optimizeAssertAndTrack(getContext().nCtx(), getNativeObject(),
                constraint.getNativeObject(), p.getNativeObject());
    }
 
    public static class Handle<R extends Sort> {
 
        private final Optimize opt;
        private final int handle;
 
        Handle(Optimize opt, int h)
        {
            this.opt = opt;
            this.handle = h;
        }
 
        public Expr<R> getLower()
        {
            return opt.GetLower(handle);
        }
 
        public Expr<R> getUpper()
        {
            return opt.GetUpper(handle);
        }
 
        public Expr<?>[] getUpperAsVector()
        {
            return opt.GetUpperAsVector(handle);
        }
 
        public Expr<?>[] getLowerAsVector()
        {
            return opt.GetLowerAsVector(handle);
        }
 
        public Expr<R> getValue()
        {
            return getLower();
        }
 
        @Override
        public String toString()
        {
            return getValue().toString();
        }
    }
 
    public Handle<?> AssertSoft(Expr<BoolSort> constraint, int weight, String group)
    {
        return AssertSoft(constraint, Integer.toString(weight), group);
    }
    
    public Handle<?> AssertSoft(Expr<BoolSort> constraint, String weight, String group)
    {
        getContext().checkContextMatch(constraint);
        Symbol s = getContext().mkSymbol(group);
        return new Handle<>(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), weight, s.getNativeObject()));
    }
 
    public Status Check(Expr<BoolSort>... assumptions)
    {
        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;
            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 BoolExpr[] getUnsatCore()
    {
        ASTVector core = new ASTVector(getContext(), Native.optimizeGetUnsatCore(getContext().nCtx(), getNativeObject()));        
        return core.ToBoolExprArray();
    }
 
    public <R extends Sort> Handle<R> MkMaximize(Expr<R> e)
    {
        return new Handle<>(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
    }
 
    public <R extends Sort> Handle<R> MkMinimize(Expr<R> e)
    {
        return new Handle<>(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
    }
    
    private <R extends Sort> Expr<R> GetLower(int index)
    {
        return (Expr<R>) Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
    }
 
    private <R extends Sort> Expr<R> GetUpper(int index)
    {
        return (Expr<R>) Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
    }
 
    private Expr<?>[] GetUpperAsVector(int index) {
        return unpackObjectiveValueVector(
                Native.optimizeGetUpperAsVector(
                        getContext().nCtx(), getNativeObject(), index
                )
        );
    }
 
    private Expr<?>[] GetLowerAsVector(int index) {
        return unpackObjectiveValueVector(
                Native.optimizeGetLowerAsVector(
                        getContext().nCtx(), getNativeObject(), index
                )
        );
    }
 
    private Expr<?>[] unpackObjectiveValueVector(long nativeVec) {
        ASTVector vec = new ASTVector(
                getContext(), nativeVec
        );
        return new Expr[] {
                (Expr<?>) vec.get(0), (Expr<?>) vec.get(1), (Expr<?>) vec.get(2)
        };
 
    }
 
    public String getReasonUnknown()
    {
        return Native.optimizeGetReasonUnknown(getContext().nCtx(), getNativeObject());
    }
 
    @Override
    public String toString()
    {
        return Native.optimizeToString(getContext().nCtx(), getNativeObject());
    }
 
    public void fromFile(String file)
    {
        Native.optimizeFromFile(getContext().nCtx(), getNativeObject(), file);
    }
 
    public void fromString(String s)
    {
        Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s);
    }
 
    public BoolExpr[] getAssertions() 
    {
        ASTVector assertions = new ASTVector(getContext(), Native.optimizeGetAssertions(getContext().nCtx(), getNativeObject()));
        return assertions.ToBoolExprArray();
    }
 
    public Expr<?>[] getObjectives()
    {
        ASTVector objectives = new ASTVector(getContext(), Native.optimizeGetObjectives(getContext().nCtx(), getNativeObject()));
        return objectives.ToExprArray();
    }
 
    public void setInitialValue(Expr<?> var, Expr<?> value)
    {
        getContext().checkContextMatch(var);
        getContext().checkContextMatch(value);
        Native.optimizeSetInitialValue(getContext().nCtx(), getNativeObject(),
            var.getNativeObject(), value.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()));
    }
 
    @Override
    void incRef() {
        Native.optimizeIncRef(getContext().nCtx(), getNativeObject());
    }
 
    @Override
    void addToReferenceQueue() {
        getContext().getReferenceQueue().storeReference(this, OptimizeRef::new);
    }
 
    private static class OptimizeRef extends Z3ReferenceQueue.Reference<Optimize> {
 
        private OptimizeRef(Optimize referent, ReferenceQueue<Z3Object> q) {
            super(referent, q);
        }
 
        @Override
        void decRef(Context ctx, long z3Obj) {
            Native.optimizeDecRef(ctx.nCtx(), z3Obj);
        }
    }
}