Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
Fixedpoint Class Reference
+ Inheritance diagram for Fixedpoint:

Public Member Functions

String getHelp () throws Z3Exception
void setParameters (Params value) throws Z3Exception
ParamDescrs getParameterDescriptions () throws Z3Exception
void add (BoolExpr...constraints) throws Z3Exception
void registerRelation (FuncDecl f) throws Z3Exception
void addRule (BoolExpr rule, Symbol name) throws Z3Exception
void addFact (FuncDecl pred, int...args) throws Z3Exception
Status query (BoolExpr query) throws Z3Exception
Status query (FuncDecl[] relations) throws Z3Exception
void push () throws Z3Exception
void pop () throws Z3Exception
void updateRule (BoolExpr rule, Symbol name) throws Z3Exception
Expr getAnswer () throws Z3Exception
String getReasonUnknown () throws Z3Exception
int getNumLevels (FuncDecl predicate) throws Z3Exception
Expr getCoverDelta (int level, FuncDecl predicate) throws Z3Exception
void addCover (int level, FuncDecl predicate, Expr property) throws Z3Exception
String toString ()
void setPredicateRepresentation (FuncDecl f, Symbol[] kinds) throws Z3Exception
String toString (BoolExpr[] queries) throws Z3Exception
BoolExpr[] getRules () throws Z3Exception
BoolExpr[] getAssertions () throws Z3Exception

Package Functions

 Fixedpoint (Context ctx, long obj) throws Z3Exception
 Fixedpoint (Context ctx) throws Z3Exception
void incRef (long o) throws Z3Exception
void decRef (long o) throws Z3Exception

Detailed Description

Object for managing fixedpoints

Definition at line 25 of file Fixedpoint.java.


Constructor & Destructor Documentation

Fixedpoint ( Context  ctx,
long  obj 
) throws Z3Exception [inline, package]

Definition at line 322 of file Fixedpoint.java.

    {
        super(ctx, obj);
    }
Fixedpoint ( Context  ctx) throws Z3Exception [inline, package]

Definition at line 327 of file Fixedpoint.java.

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

Member Function Documentation

void add ( BoolExpr...  constraints) throws Z3Exception [inline]

Assert a constraint (or multiple) into the fixedpoint solver.

Exceptions:
Z3Exception

Definition at line 65 of file Fixedpoint.java.

    {
        getContext().checkContextMatch(constraints);
        for (BoolExpr a : constraints)
        {
            Native.fixedpointAssert(getContext().nCtx(), getNativeObject(),
                    a.getNativeObject());
        }
    }
void addCover ( int  level,
FuncDecl  predicate,
Expr  property 
) throws Z3Exception [inline]

Add property about the predicate. The property is added at level.

Definition at line 243 of file Fixedpoint.java.

    {
        Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
                predicate.getNativeObject(), property.getNativeObject());
    }
void addFact ( FuncDecl  pred,
int...  args 
) throws Z3Exception [inline]

Add table fact to the fixedpoint solver.

Exceptions:
Z3Exception

Definition at line 106 of file Fixedpoint.java.

    {
        getContext().checkContextMatch(pred);
        Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
                pred.getNativeObject(), (int) args.length, args);
    }
void addRule ( BoolExpr  rule,
Symbol  name 
) throws Z3Exception [inline]

Add rule into the fixedpoint solver.

Exceptions:
Z3Exception

Definition at line 93 of file Fixedpoint.java.

    {

        getContext().checkContextMatch(rule);
        Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(),
                rule.getNativeObject(), AST.getNativeObject(name));
    }
void decRef ( long  o) throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 338 of file Fixedpoint.java.

    {
        getContext().fixedpoint_DRQ().add(o);
        super.decRef(o);
    }
Expr getAnswer ( ) throws Z3Exception [inline]

Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that show unsatisfiability.

Exceptions:
Z3Exception

Definition at line 202 of file Fixedpoint.java.

    {
        long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject());
        return (ans == 0) ? null : Expr.create(getContext(), ans);
    }
BoolExpr [] getAssertions ( ) throws Z3Exception [inline]

Retrieve set of assertions added to fixedpoint context.

Exceptions:
Z3Exception

Definition at line 310 of file Fixedpoint.java.

    {

        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;
    }
Expr getCoverDelta ( int  level,
FuncDecl  predicate 
) throws Z3Exception [inline]

Retrieve the cover of a predicate.

Exceptions:
Z3Exception

Definition at line 232 of file Fixedpoint.java.

    {
        long res = Native.fixedpointGetCoverDelta(getContext().nCtx(),
                getNativeObject(), level, predicate.getNativeObject());
        return (res == 0) ? null : Expr.create(getContext(), res);
    }
String getHelp ( ) throws Z3Exception [inline]

A string that describes all available fixedpoint solver parameters.

Definition at line 31 of file Fixedpoint.java.

    {
        return Native.fixedpointGetHelp(getContext().nCtx(), getNativeObject());
    }
int getNumLevels ( FuncDecl  predicate) throws Z3Exception [inline]

Retrieve the number of levels explored for a given predicate.

Definition at line 221 of file Fixedpoint.java.

    {
        return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(),
                predicate.getNativeObject());
    }

Retrieves parameter descriptions for Fixedpoint solver.

Exceptions:
Z3Exception

Definition at line 54 of file Fixedpoint.java.

    {
        return new ParamDescrs(getContext(), Native.fixedpointGetParamDescrs(
                getContext().nCtx(), getNativeObject()));
    }
String getReasonUnknown ( ) throws Z3Exception [inline]

Retrieve explanation why fixedpoint engine returned status Unknown.

Definition at line 211 of file Fixedpoint.java.

    {

        return Native.fixedpointGetReasonUnknown(getContext().nCtx(),
                getNativeObject());
    }
BoolExpr [] getRules ( ) throws Z3Exception [inline]

Retrieve set of rules added to fixedpoint context.

Exceptions:
Z3Exception

Definition at line 293 of file Fixedpoint.java.

    {

        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;
    }
void incRef ( long  o) throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 332 of file Fixedpoint.java.

    {
        getContext().fixedpoint_DRQ().incAndClear(getContext(), o);
        super.incRef(o);
    }
void pop ( ) throws Z3Exception [inline]

Backtrack one backtracking point. Note that an exception is thrown if Pop is called without a corresponding Push

See also:
Push

Definition at line 178 of file Fixedpoint.java.

    {
        Native.fixedpointPop(getContext().nCtx(), getNativeObject());
    }
void push ( ) throws Z3Exception [inline]

Creates a backtracking point.

See also:
Pop

Definition at line 168 of file Fixedpoint.java.

    {
        Native.fixedpointPush(getContext().nCtx(), getNativeObject());
    }
Status query ( BoolExpr  query) throws Z3Exception [inline]

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.

Exceptions:
Z3Exception

Definition at line 122 of file Fixedpoint.java.

    {

        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;
        }
    }
Status query ( FuncDecl[]  relations) throws Z3Exception [inline]

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.

Exceptions:
Z3Exception

Definition at line 147 of file Fixedpoint.java.

    {

        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;
        }
    }
void registerRelation ( FuncDecl  f) throws Z3Exception [inline]

Register predicate as recursive relation.

Exceptions:
Z3Exception

Definition at line 80 of file Fixedpoint.java.

    {

        getContext().checkContextMatch(f);
        Native.fixedpointRegisterRelation(getContext().nCtx(), getNativeObject(),
                f.getNativeObject());
    }
void setParameters ( Params  value) throws Z3Exception [inline]

Sets the fixedpoint solver parameters.

Exceptions:
Z3Exception

Definition at line 41 of file Fixedpoint.java.

    {

        getContext().checkContextMatch(value);
        Native.fixedpointSetParams(getContext().nCtx(), getNativeObject(),
                value.getNativeObject());
    }
void setPredicateRepresentation ( FuncDecl  f,
Symbol[]  kinds 
) throws Z3Exception [inline]

Instrument the Datalog engine on which table representation to use for recursive predicate.

Definition at line 269 of file Fixedpoint.java.

    {

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

    }
String toString ( ) [inline]

Retrieve internal string representation of fixedpoint object.

Definition at line 253 of file Fixedpoint.java.

    {
        try
        {
            return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
                    0, null);
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }
String toString ( BoolExpr[]  queries) throws Z3Exception [inline]

Convert benchmark given as set of axioms, rules and queries to a string.

Definition at line 281 of file Fixedpoint.java.

    {

        return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
                AST.arrayLength(queries), AST.arrayToNative(queries));
    }
void updateRule ( BoolExpr  rule,
Symbol  name 
) throws Z3Exception [inline]

Update named rule into in the fixedpoint solver.

Exceptions:
Z3Exception

Definition at line 188 of file Fixedpoint.java.

    {

        getContext().checkContextMatch(rule);
        Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
                rule.getNativeObject(), AST.getNativeObject(name));
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines