Fixedpoint Class Reference

Inheritance diagram for Fixedpoint:

Public Member Functions
String	getHelp ()
void	setParameters (Params value)
ParamDescrs	getParameterDescriptions ()
final void	add (Expr< BoolSort >... constraints)
void	registerRelation (FuncDecl< BoolSort > f)
void	addRule (Expr< BoolSort > rule, Symbol name)
void	addFact (FuncDecl< BoolSort > pred, int ... args)
Status	query (Expr< BoolSort > query)
Status	query (FuncDecl< BoolSort >[] relations)
void	updateRule (Expr< BoolSort > rule, Symbol name)
Expr<?>	getAnswer ()
String	getReasonUnknown ()
int	getNumLevels (FuncDecl< BoolSort > predicate)
Expr<?>	getCoverDelta (int level, FuncDecl< BoolSort > predicate)
void	addCover (int level, FuncDecl< BoolSort > predicate, Expr<?> property)
String	toString ()
void	setPredicateRepresentation (FuncDecl< BoolSort > f, Symbol[] kinds)
String	toString (Expr< BoolSort >[] queries)
BoolExpr[]	getRules ()
BoolExpr[]	getAssertions ()
Statistics	getStatistics ()
BoolExpr[]	ParseFile (String file)
BoolExpr[]	ParseString (String s)

Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)
static int	arrayLength (Z3Object[] a)

Detailed Description

Object for managing fixedpoints

Definition at line 27 of file Fixedpoint.java.

Member Function Documentation

add()

final void add ( Expr< BoolSort >...  constraints )

inline

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

Exceptions

Z3Exception

Definition at line 68 of file Fixedpoint.java.

    {
        getContext().checkContextMatch(constraints);
        for (Expr<BoolSort> a : constraints)
        {
            Native.fixedpointAssert(getContext().nCtx(), getNativeObject(),
                    a.getNativeObject());
        }
    }

Referenced by Solver.__iadd__().

addCover()

void addCover ( int  level, FuncDecl< BoolSort >  predicate, Expr<?>  property  )

inline

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

Definition at line 221 of file Fixedpoint.java.

    {
        Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level,
                predicate.getNativeObject(), property.getNativeObject());
    }

addFact()

void addFact ( FuncDecl< BoolSort >  pred, int ...  args  )

inline

Add table fact to the fixedpoint solver.

Exceptions

Z3Exception

Definition at line 108 of file Fixedpoint.java.

                                                               {
        getContext().checkContextMatch(pred);
        Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
                pred.getNativeObject(), args.length, args);
    }

addRule()

void addRule ( Expr< BoolSort >  rule, Symbol  name  )

inline

Add rule into the fixedpoint solver.

Parameters

rule	implication (Horn clause) representing rule
name	Nullable rule name.

Exceptions

Z3Exception

Definition at line 97 of file Fixedpoint.java.

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

getAnswer()

Expr<?> getAnswer ( )

inline

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

Exceptions

Z3Exception

Definition at line 181 of file Fixedpoint.java.

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

getAssertions()

BoolExpr[] getAssertions ( )

inline

Retrieve set of assertions added to fixedpoint context.

Exceptions

Z3Exception

Definition at line 275 of file Fixedpoint.java.

    {
        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
        return v.ToBoolExprArray();
    }

getCoverDelta()

Expr<?> getCoverDelta ( int  level, FuncDecl< BoolSort >  predicate  )

inline

Retrieve the cover of a predicate.

Exceptions

Z3Exception

Definition at line 210 of file Fixedpoint.java.

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

getHelp()

String getHelp ( )

inline

A string that describes all available fixedpoint solver parameters.

Definition at line 33 of file Fixedpoint.java.

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

getNumLevels()

int getNumLevels ( FuncDecl< BoolSort >  predicate )

inline

Retrieve the number of levels explored for a given predicate.

Definition at line 199 of file Fixedpoint.java.

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

getParameterDescriptions()

ParamDescrs getParameterDescriptions ( )

inline

Retrieves parameter descriptions for Fixedpoint solver.

Exceptions

Z3Exception

Definition at line 56 of file Fixedpoint.java.

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

getReasonUnknown()

String getReasonUnknown ( )

inline

Retrieve explanation why fixedpoint engine returned status Unknown.

Definition at line 190 of file Fixedpoint.java.

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

getRules()

BoolExpr[] getRules ( )

inline

Retrieve set of rules added to fixedpoint context.

Exceptions

Z3Exception

Definition at line 264 of file Fixedpoint.java.

    {
        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
        return v.ToBoolExprArray();
    }

getStatistics()

Statistics getStatistics ( )

inline

Fixedpoint statistics.

Exceptions

Z3Exception

Definition at line 286 of file Fixedpoint.java.

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

ParseFile()

BoolExpr[] ParseFile ( String  file )

inline

Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file.

Definition at line 297 of file Fixedpoint.java.

    {
        ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
        return av.ToBoolExprArray();
    }

ParseString()

BoolExpr[] ParseString ( String  s )

inline

Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file.

Definition at line 308 of file Fixedpoint.java.

    {
        ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
        return av.ToBoolExprArray();
    }

query() [1/2]

Status query ( Expr< BoolSort >  query )

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 123 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;
        }
    }

Referenced by Fixedpoint.query().

query() [2/2]

Status query ( FuncDecl< BoolSort >[]  relations )

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 146 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;
        }
    }

registerRelation()

void registerRelation ( FuncDecl< BoolSort >  f )

inline

Register predicate as recursive relation.

Exceptions

Z3Exception

Definition at line 83 of file Fixedpoint.java.

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

setParameters()

void setParameters ( Params  value )

inline

Sets the fixedpoint solver parameters.

Exceptions

Z3Exception

Definition at line 43 of file Fixedpoint.java.

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

setPredicateRepresentation()

void setPredicateRepresentation ( FuncDecl< BoolSort >  f, Symbol[]  kinds  )

inline

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

Definition at line 242 of file Fixedpoint.java.

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

toString() [1/2]

String toString ( )

inline

Retrieve internal string representation of fixedpoint object.

Definition at line 232 of file Fixedpoint.java.

    {
        return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
                    0, null);
    }

toString() [2/2]

String toString ( Expr< BoolSort >[]  queries )

inline

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

Definition at line 253 of file Fixedpoint.java.

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

updateRule()

void updateRule ( Expr< BoolSort >  rule, Symbol  name  )

inline

Update named rule into in the fixedpoint solver.

Parameters

rule	implication (Horn clause) representing rule
name	Nullable rule name.

Exceptions

Z3Exception

Definition at line 169 of file Fixedpoint.java.

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