Fixedpoint.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
import com.microsoft.z3.enumerations.Z3_lbool;
 
import java.lang.ref.ReferenceQueue;
 
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()));
    }
 
    @SafeVarargs
    public final void add(Expr<BoolSort>... constraints)
    {
        getContext().checkContextMatch(constraints);
        for (Expr<BoolSort> a : constraints)
        {
            Native.fixedpointAssert(getContext().nCtx(), getNativeObject(),
                    a.getNativeObject());
        }
    }
 
    public void registerRelation(FuncDecl<BoolSort> f)
    {
        getContext().checkContextMatch(f);
        Native.fixedpointRegisterRelation(getContext().nCtx(), getNativeObject(),
                f.getNativeObject());
    }
 
    public void addRule(Expr<BoolSort> rule, Symbol name) {
        getContext().checkContextMatch(rule);
        Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(),
                rule.getNativeObject(), AST.getNativeObject(name));
    }
 
    public void addFact(FuncDecl<BoolSort> pred, int ... args) {
        getContext().checkContextMatch(pred);
        Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
                pred.getNativeObject(), args.length, args);
    }
 
    public Status query(Expr<BoolSort> 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<BoolSort>[] 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 updateRule(Expr<BoolSort> 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<BoolSort> predicate)
    {
        return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
                predicate.getNativeObject());
    }
 
    public Expr<?> getCoverDelta(int level, FuncDecl<BoolSort> 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<BoolSort> predicate, Expr<?> property)
           
    {
        Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
                predicate.getNativeObject(), property.getNativeObject());
    }
 
    @Override
    public String toString()
    {
        return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
                    0, null);
    }
 
    public void setPredicateRepresentation(FuncDecl<BoolSort> f, Symbol[] kinds)
    {
        Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
                getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
                Symbol.arrayToNative(kinds));
 
    }
 
    public String toString(Expr<BoolSort>[] 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()));
    }
 
    @Override
    void incRef() {
        Native.fixedpointIncRef(getContext().nCtx(), getNativeObject());
    }
 
    @Override
    void addToReferenceQueue() {
        getContext().getReferenceQueue().storeReference(this, FixedpointRef::new);
    }
 
    private static class FixedpointRef extends Z3ReferenceQueue.Reference<Fixedpoint> {
 
        private FixedpointRef(Fixedpoint referent, ReferenceQueue<Z3Object> q) {
            super(referent, q);
        }
 
        @Override
        void decRef(Context ctx, long z3Obj) {
            Native.fixedpointDecRef(ctx.nCtx(), z3Obj);
        }
    }
}