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()
    {
        return Native.fixedpointGetHelp(getContext().nCtx(), getNativeObject());
    }

    public void setParameters(Params value)
    {

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

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

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

    public void registerRelation(FuncDecl f)
    {

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

    public void addRule(BoolExpr rule, Symbol name)
    {

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

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

    public Status query(BoolExpr query)
    {

        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)
    {

        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()
    {
        Native.fixedpointPush(getContext().nCtx(), getNativeObject());
    }

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

    public void updateRule(BoolExpr rule, Symbol name)
    {

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

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

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

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

    public Expr getCoverDelta(int level, FuncDecl predicate)
    {
        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)
           
    {
        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)
    {

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

    }

    public String toString(BoolExpr[] queries)
    {

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

    public BoolExpr[] getRules()
    {
        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
        return v.ToBoolExprArray();
    }

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

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

    public BoolExpr[] ParseFile(String file)
    {
        ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
        return av.ToBoolExprArray();
    }

    public BoolExpr[] ParseString(String s)
    {
        ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
        return av.ToBoolExprArray();
    }
    

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

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

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

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