Goal.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
import com.microsoft.z3.enumerations.Z3_goal_prec;
 
import java.lang.ref.ReferenceQueue;
 
public class Goal extends Z3Object {
    public Z3_goal_prec getPrecision()
    {
        return Z3_goal_prec.fromInt(Native.goalPrecision(getContext().nCtx(),
                getNativeObject()));
    }
 
    public boolean isPrecise()
    {
        return getPrecision() == Z3_goal_prec.Z3_GOAL_PRECISE;
    }
 
    public boolean isUnderApproximation()
    {
        return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER;
    }
 
    public boolean isOverApproximation()
    {
        return getPrecision() == Z3_goal_prec.Z3_GOAL_OVER;
    }
 
    public boolean isGarbage()
    {
        return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER_OVER;
    }
 
    @SafeVarargs
    public final void add(Expr<BoolSort>... constraints)
    {
        getContext().checkContextMatch(constraints);
        for (Expr<BoolSort> c : constraints)
        {
            Native.goalAssert(getContext().nCtx(), getNativeObject(),
                    c.getNativeObject());
        }
    }
 
    public boolean inconsistent()
    {
        return Native.goalInconsistent(getContext().nCtx(), getNativeObject());
    }
 
    public int getDepth()
    {
        return Native.goalDepth(getContext().nCtx(), getNativeObject());
    }
 
    public void reset()
    {
        Native.goalReset(getContext().nCtx(), getNativeObject());
    }
 
    public int size()
    {
        return Native.goalSize(getContext().nCtx(), getNativeObject());
    }
 
    public BoolExpr[] getFormulas()
    {
        int n = size();
        BoolExpr[] res = new BoolExpr[n];
        for (int i = 0; i < n; i++)
            res[i] = (BoolExpr) Expr.create(getContext(), Native.goalFormula(getContext().nCtx(), getNativeObject(), i));
        return res;
    }
 
    public int getNumExprs()
    {
        return Native.goalNumExprs(getContext().nCtx(), getNativeObject());
    }
 
    public boolean isDecidedSat()
    {
        return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject());
    }
 
    public boolean isDecidedUnsat()
    {
        return Native
                .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject());
    }
 
    public Goal translate(Context ctx)
    {
        return new Goal(ctx, Native.goalTranslate(getContext().nCtx(),
                getNativeObject(), ctx.nCtx()));
    }
 
    public Goal simplify()
    {
        Tactic t = getContext().mkTactic("simplify");
        ApplyResult res = t.apply(this);
 
        if (res.getNumSubgoals() == 0)
            throw new Z3Exception("No subgoals");
        else
            return res.getSubgoals()[0];
    }
    
    public Goal simplify(Params p)
    {
        Tactic t = getContext().mkTactic("simplify");
        ApplyResult res = t.apply(this, p);
 
        if (res.getNumSubgoals() == 0)
            throw new Z3Exception("No subgoals");
        else
            return res.getSubgoals()[0];
    }
 
    public String toString() {
        return Native.goalToString(getContext().nCtx(), getNativeObject());
    }
    
    public BoolExpr AsBoolExpr() {
        int n = size();
        if (n == 0) {
            return getContext().mkTrue();
        } else if (n == 1) {
            return getFormulas()[0];
        } else {
            return getContext().mkAnd(getFormulas());
        }
    }
 
    Goal(Context ctx, long obj)
    {
        super(ctx, obj);
    }
 
    Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs) {
        super(ctx, Native.mkGoal(ctx.nCtx(), (models),
            (unsatCores), (proofs)));
    }
 
    public Model convertModel(Model m)
    {
        return new Model(getContext(), 
            Native.goalConvertModel(getContext().nCtx(), getNativeObject(), m.getNativeObject()));
    }
 
 
 
    @Override
    void incRef() {
        Native.goalIncRef(getContext().nCtx(), getNativeObject());
    }
 
    @Override
    void addToReferenceQueue() {
        getContext().getReferenceQueue().storeReference(this, GoalRef::new);
    }
 
    private static class GoalRef extends Z3ReferenceQueue.Reference<Goal> {
 
        private GoalRef(Goal referent, ReferenceQueue<Z3Object> q) {
            super(referent, q);
        }
 
        @Override
        void decRef(Context ctx, long z3Obj) {
            Native.goalDecRef(ctx.nCtx(), z3Obj);
        }
    }
}