Solver.java

Go to the documentation of this file.

package com.microsoft.z3;

import com.microsoft.z3.enumerations.Z3_lbool;

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

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

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

    public int getNumScopes()
    {
        return Native
                .solverGetNumScopes(getContext().nCtx(), getNativeObject());
    }

    public void push()
    {
        Native.solverPush(getContext().nCtx(), getNativeObject());
    }

    public void pop()
    {
        pop(1);
    }

    public void pop(int n)
    {
        Native.solverPop(getContext().nCtx(), getNativeObject(), n);
    }

    public void reset()
    {
        Native.solverReset(getContext().nCtx(), getNativeObject());
    }

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

    public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
    {
        getContext().checkContextMatch(constraints);
        getContext().checkContextMatch(ps);
        if (constraints.length != ps.length)
            throw new Z3Exception("Argument size mismatch");

        for (int i = 0; i < constraints.length; i++)
            Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
                    constraints[i].getNativeObject(), ps[i].getNativeObject());
    }

    public void assertAndTrack(BoolExpr constraint, BoolExpr p)
    {
        getContext().checkContextMatch(constraint);
        getContext().checkContextMatch(p);

        Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
                constraint.getNativeObject(), p.getNativeObject());
    }

    public int getNumAssertions()
    {
        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
        return assrts.size();
    }

    public BoolExpr[] getAssertions()
    {
        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
        return assrts.ToBoolExprArray();
    }

    public Status check(Expr... assumptions)
    {
        Z3_lbool r;
        if (assumptions == null)
            r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
                    getNativeObject()));
        else
            r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
                    .nCtx(), getNativeObject(), (int) 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 Status check()
    {
        return check((Expr[]) null);
    }

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

    public Expr getProof()
    {
        long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
        if (x == 0)
            return null;
        else
            return Expr.create(getContext(), x);
    }

    public BoolExpr[] getUnsatCore()
    {

        ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));        
        return core.ToBoolExprArray();
    }

    public String getReasonUnknown()
    {
        return Native.solverGetReasonUnknown(getContext().nCtx(),
                getNativeObject());
    }

    public Statistics getStatistics()
    {
        return new Statistics(getContext(), Native.solverGetStatistics(
                getContext().nCtx(), getNativeObject()));
    }

    public String toString()
    {
        try
        {
            return Native
                    .solverToString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }

    Solver(Context ctx, long obj)
    {
        super(ctx, obj);
    }

    void incRef(long o)
    {
        getContext().getSolverDRQ().incAndClear(getContext(), o);
        super.incRef(o);
    }

    void decRef(long o)
    {
        getContext().getSolverDRQ().add(o);
        super.decRef(o);
    }
}