z3/src/api/java/Fixedpoint.java

/**
Copyright (c) 2012-2014 Microsoft Corporation
   
Module Name:

    Fixedpoint.java

Abstract:

Author:

    @author Christoph Wintersteiger (cwinter) 2012-03-15

Notes:
    
**/ 

package com.microsoft.z3;

import com.microsoft.z3.enumerations.Z3_lbool;

/**
 * Object for managing fixedpoints
 **/
public class Fixedpoint extends Z3Object
{

    /**
     * A string that describes all available fixedpoint solver parameters.
     **/
    public String getHelp()
    {
        return Native.fixedpointGetHelp(getContext().nCtx(), getNativeObject());
    }

    /**
     * Sets the fixedpoint solver parameters.
     * 
     * @throws Z3Exception
     **/
    public void setParameters(Params value)
    {

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

    /**
     * Retrieves parameter descriptions for Fixedpoint solver.
     * 
     * @throws Z3Exception
     **/
    public ParamDescrs getParameterDescriptions()
    {
        return new ParamDescrs(getContext(), Native.fixedpointGetParamDescrs(
                getContext().nCtx(), getNativeObject()));
    }

    /**
     * Assert a constraint (or multiple) into the fixedpoint solver.
     * 
     * @throws Z3Exception
     **/
    @SafeVarargs
    public final void add(Expr<BoolSort>... constraints)
    {
        getContext().checkContextMatch(constraints);
        for (Expr<BoolSort> a : constraints)
        {
            Native.fixedpointAssert(getContext().nCtx(), getNativeObject(),
                    a.getNativeObject());
        }
    }

    /**
     * Register predicate as recursive relation.
     * 
     * @throws Z3Exception
     **/
    public void registerRelation(FuncDecl<BoolSort> f)
    {
        getContext().checkContextMatch(f);
        Native.fixedpointRegisterRelation(getContext().nCtx(), getNativeObject(),
                f.getNativeObject());
    }

    /**
     * Add rule into the fixedpoint solver.
     *
     * @param rule implication (Horn clause) representing rule
     * @param name Nullable rule name.
     * @throws Z3Exception
     **/
    public void addRule(Expr<BoolSort> rule, Symbol name) {
        getContext().checkContextMatch(rule);
        Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(),
                rule.getNativeObject(), AST.getNativeObject(name));
    }

    /**
     * Add table fact to the fixedpoint solver.
     * 
     * @throws Z3Exception
     **/
    public void addFact(FuncDecl<BoolSort> pred, int ... args) {
        getContext().checkContextMatch(pred);
        Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
                pred.getNativeObject(), args.length, args);
    }

    /**
     * Query the fixedpoint solver. A query is a conjunction of constraints. The
     * constraints may include the recursively defined relations. The query is
     * satisfiable if there is an instance of the query variables and a
     * derivation for it. The query is unsatisfiable if there are no derivations
     * satisfying the query variables.
     * 
     * @throws Z3Exception
     **/
    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;
        }
    }

    /**
     * Query the fixedpoint solver. A query is an array of relations. The query
     * is satisfiable if there is an instance of some relation that is
     * non-empty. The query is unsatisfiable if there are no derivations
     * satisfying any of the relations.
     * 
     * @throws Z3Exception
     **/
    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;
        }
    }

    /**
     * Update named rule into in the fixedpoint solver.
     *
     * @param rule implication (Horn clause) representing rule
     * @param name Nullable rule name.
     * @throws Z3Exception
     **/
    public void updateRule(Expr<BoolSort> rule, Symbol name) {
        getContext().checkContextMatch(rule);
        Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
                rule.getNativeObject(), AST.getNativeObject(name));
    }

    /**
     * Retrieve satisfying instance or instances of solver, or definitions for
     * the recursive predicates that show unsatisfiability.
     * 
     * @throws Z3Exception
     **/
    public Expr<?> getAnswer()
    {
        long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
        return (ans == 0) ? null : Expr.create(getContext(), ans);
    }

    /**
     * Retrieve explanation why fixedpoint engine returned status Unknown.
     **/
    public String getReasonUnknown()
    {
        return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
                getNativeObject());
    }

    /**
     * Retrieve the number of levels explored for a given predicate.
     **/
    public int getNumLevels(FuncDecl<BoolSort> predicate)
    {
        return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
                predicate.getNativeObject());
    }

    /**
     * Retrieve the cover of a predicate.
     * 
     * @throws Z3Exception
     **/
    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);
    }

    /**
     * Add <tt>property</tt> about the <tt>predicate</tt>. The property is added
     * at <tt>level</tt>.
     **/
    public void addCover(int level, FuncDecl<BoolSort> predicate, Expr<?> property)
           
    {
        Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
                predicate.getNativeObject(), property.getNativeObject());
    }

    /**
     * Retrieve internal string representation of fixedpoint object.
     **/
    @Override
    public String toString()
    {
        return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
                    0, null);
    }

    /**
     * Instrument the Datalog engine on which table representation to use for
     * recursive predicate.
     **/
    public void setPredicateRepresentation(FuncDecl<BoolSort> f, Symbol[] kinds)
    {
        Native.fixedpointSetPredicateRepresentation(getContext().nCtx(),
                getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds),
                Symbol.arrayToNative(kinds));

    }

    /**
     * Convert benchmark given as set of axioms, rules and queries to a string.
     **/
    public String toString(Expr<BoolSort>[] queries)
    {
        return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
                AST.arrayLength(queries), AST.arrayToNative(queries));
    }

    /**
     * Retrieve set of rules added to fixedpoint context.
     * 
     * @throws Z3Exception
     **/
    public BoolExpr[] getRules()
    {
        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
        return v.ToBoolExprArray();
    }

    /**
     * Retrieve set of assertions added to fixedpoint context.
     * 
     * @throws Z3Exception
     **/
    public BoolExpr[] getAssertions()
    {
        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
        return v.ToBoolExprArray();
    }

    /**
     * Fixedpoint statistics.
     * 
     * @throws Z3Exception
     **/
    public Statistics getStatistics()
    {
        return new Statistics(getContext(), Native.fixedpointGetStatistics(
                getContext().nCtx(), getNativeObject()));
    }

    /** 
     * Parse an SMT-LIB2 file with fixedpoint rules. 
     * Add the rules to the current fixedpoint context. 
     * Return the set of queries in the file.
     **/        
    public BoolExpr[] ParseFile(String file)
    {
        ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
        return av.ToBoolExprArray();
    }

    /** 
     * Parse an SMT-LIB2 string with fixedpoint rules. 
     * Add the rules to the current fixedpoint context. 
     * Return the set of queries in the file.
     **/ 
    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().getFixedpointDRQ().storeReference(getContext(), this);
    }

    @Override
    void checkNativeObject(long obj) { }
}