src/api/java/Fixedpoint.java

Go to the documentation of this file.

package com.microsoft.z3;

import com.microsoft.z3.enumerations.Z3_lbool;

public class Fixedpoint extends Z3Object
{

    public String getHelp() throws Z3Exception
    {
        return Native.fixedpointGetHelp(getContext().nCtx(), getNativeObject());
    }

    public void setParameters(Params value) throws Z3Exception
    {

        getContext().checkContextMatch(value);
        Native.fixedpointSetParams(getContext().nCtx(), getNativeObject(),
                value.getNativeObject());
    }

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

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

    public void registerRelation(FuncDecl f) throws Z3Exception
    {

        getContext().checkContextMatch(f);
        Native.fixedpointRegisterRelation(getContext().nCtx(), getNativeObject(),
                f.getNativeObject());
    }

    public void addRule(BoolExpr rule, Symbol name) throws Z3Exception
    {

        getContext().checkContextMatch(rule);
        Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(),
                rule.getNativeObject(), AST.getNativeObject(name));
    }

    public void addFact(FuncDecl pred, int ... args) throws Z3Exception
    {
        getContext().checkContextMatch(pred);
        Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
                pred.getNativeObject(), (int) args.length, args);
    }

    public Status query(BoolExpr query) throws Z3Exception
    {

        getContext().checkContextMatch(query);
        Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(getContext().nCtx(),
                getNativeObject(), query.getNativeObject()));
        switch (r)
        {
        case Z3_L_TRUE:
            return Status.SATISFIABLE;
        case Z3_L_FALSE:
            return Status.UNSATISFIABLE;
        default:
            return Status.UNKNOWN;
        }
    }

    public Status query(FuncDecl[] relations) throws Z3Exception
    {

        getContext().checkContextMatch(relations);
        Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQueryRelations(getContext()
                .nCtx(), getNativeObject(), AST.arrayLength(relations), AST
                .arrayToNative(relations)));
        switch (r)
        {
        case Z3_L_TRUE:
            return Status.SATISFIABLE;
        case Z3_L_FALSE:
            return Status.UNSATISFIABLE;
        default:
            return Status.UNKNOWN;
        }
    }

    public void push() throws Z3Exception
    {
        Native.fixedpointPush(getContext().nCtx(), getNativeObject());
    }

    public void pop() throws Z3Exception
    {
        Native.fixedpointPop(getContext().nCtx(), getNativeObject());
    }

    public void updateRule(BoolExpr rule, Symbol name) throws Z3Exception
    {

        getContext().checkContextMatch(rule);
        Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
                rule.getNativeObject(), AST.getNativeObject(name));
    }

    public Expr getAnswer() throws Z3Exception
    {
        long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
        return (ans == 0) ? null : Expr.create(getContext(), ans);
    }

    public String getReasonUnknown() throws Z3Exception
    {

        return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
                getNativeObject());
    }

    public int getNumLevels(FuncDecl predicate) throws Z3Exception
    {
        return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
                predicate.getNativeObject());
    }

    public Expr getCoverDelta(int level, FuncDecl predicate) throws Z3Exception
    {
        long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
                getNativeObject(), level, predicate.getNativeObject());
        return (res == 0) ? null : Expr.create(getContext(), res);
    }

    public void addCover(int level, FuncDecl predicate, Expr property)
            throws Z3Exception
    {
        Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
                predicate.getNativeObject(), property.getNativeObject());
    }

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

    public void setPredicateRepresentation(FuncDecl f, Symbol[] kinds) throws Z3Exception
    {

        Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
                getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
                Symbol.arrayToNative(kinds));

    }

    public String toString(BoolExpr[] queries) throws Z3Exception
    {

        return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
                AST.arrayLength(queries), AST.arrayToNative(queries));
    }

    public BoolExpr[] getRules() throws Z3Exception
    {

        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(
                getContext().nCtx(), getNativeObject()));
        int n = v.size();
        BoolExpr[] res = new BoolExpr[n];
        for (int i = 0; i < n; i++)
            res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
        return res;
    }

    public BoolExpr[] getAssertions() throws Z3Exception
    {

        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(
                getContext().nCtx(), getNativeObject()));
        int n = v.size();
        BoolExpr[] res = new BoolExpr[n];
        for (int i = 0; i < n; i++)
            res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
        return res;
    }

    Fixedpoint(Context ctx, long obj) throws Z3Exception
    {
        super(ctx, obj);
    }

    Fixedpoint(Context ctx) throws Z3Exception
    {
        super(ctx, Native.mkFixedpoint(ctx.nCtx()));
    }

    void incRef(long o) throws Z3Exception
    {
        getContext().fixedpoint_DRQ().incAndClear(getContext(), o);
        super.incRef(o);
    }

    void decRef(long o) throws Z3Exception
    {
        getContext().fixedpoint_DRQ().add(o);
        super.decRef(o);
    }
}