Inheritance diagram for Fixedpoint:

Public Member Functions
String	getHelp ()

void	setParameters (Params value)

ParamDescrs	getParameterDescriptions ()

void	add (BoolExpr ... constraints)

void	registerRelation (FuncDecl f)

void	addRule (BoolExpr rule, Symbol name)

void	addFact (FuncDecl pred, int ... args)

Status	query (BoolExpr query)

Status	query (FuncDecl[] relations)

void	push ()

void	pop ()

void	updateRule (BoolExpr rule, Symbol name)

Expr	getAnswer ()

String	getReasonUnknown ()

int	getNumLevels (FuncDecl predicate)

Expr	getCoverDelta (int level, FuncDecl predicate)

void	addCover (int level, FuncDecl predicate, Expr property)

String	toString ()

void	setPredicateRepresentation (FuncDecl f, Symbol[] kinds)

String	toString (BoolExpr[] queries)

BoolExpr []	getRules ()

BoolExpr []	getAssertions ()

Statistics	getStatistics ()

BoolExpr []	ParseFile (String file)

BoolExpr []	ParseString (String s)

Detailed Description

Object for managing fixedpoints

Definition at line 25 of file Fixedpoint.java.

Member Function Documentation

◆ add()

void add ( BoolExpr ... constraints )

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());
         }
     }

Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().

◆ addCover()

void addCover	(	int	level,
		FuncDecl	predicate,
		Expr	property
	)

inline

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

Definition at line 236 of file Fixedpoint.java.

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

◆ addFact()

void addFact	(	FuncDecl	pred,
		int ...	args
	)

inline

Add table fact to the fixedpoint solver.

Exceptions

Z3Exception

Definition at line 105 of file Fixedpoint.java.

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

◆ addRule()

void addRule	(	BoolExpr	rule,
		Symbol	name
	)

inline

Add rule into the fixedpoint solver.

Parameters

name	Nullable rule name.

Exceptions

Z3Exception

Definition at line 94 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 196 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 292 of file Fixedpoint.java.

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

◆ getCoverDelta()

Expr getCoverDelta	(	int	level,
		FuncDecl	predicate
	)

inline

Retrieve the cover of a predicate.

Exceptions

Z3Exception

Definition at line 225 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 31 of file Fixedpoint.java.

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

◆ getNumLevels()

int getNumLevels ( FuncDecl predicate )

inline

Retrieve the number of levels explored for a given predicate.

Definition at line 214 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 54 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 205 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 281 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 303 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 314 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 325 of file Fixedpoint.java.

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

◆ pop()

void pop ( )

inline

Backtrack one backtracking point. Remarks: Note that an exception is thrown if

pop

is called without a corresponding

push

See also: push

Definition at line 174 of file Fixedpoint.java.

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

◆ push()

void push ( )

inline

Creates a backtracking point.

See also: pop

Definition at line 163 of file Fixedpoint.java.

                        {
         Native.fixedpointPush(getContext().nCtx(), getNativeObject());
     }

◆ query() [1/2]

Status query ( BoolExpr 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 120 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;
         }
     }

◆ query() [2/2]

Status query ( FuncDecl [] 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 143 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 f )

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());
     }

◆ setParameters()

void setParameters ( Params value )

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());
     }

◆ setPredicateRepresentation()

void setPredicateRepresentation	(	FuncDecl	f,
		Symbol []	kinds
	)

inline

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

Definition at line 257 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 247 of file Fixedpoint.java.

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

◆ toString() [2/2]

String toString ( BoolExpr [] queries )

inline

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

Definition at line 269 of file Fixedpoint.java.

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

◆ updateRule()

void updateRule	(	BoolExpr	rule,
		Symbol	name
	)

inline

Update named rule into in the fixedpoint solver.

Parameters

name	Nullable rule name.

Exceptions

Z3Exception

Definition at line 184 of file Fixedpoint.java.

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

Public Member Functions

Detailed Description

Member Function Documentation

◆ add()

◆ addCover()

◆ addFact()

◆ addRule()

◆ getAnswer()

◆ getAssertions()

◆ getCoverDelta()

◆ getHelp()

◆ getNumLevels()

◆ getParameterDescriptions()

◆ getReasonUnknown()

◆ getRules()

◆ getStatistics()

◆ ParseFile()

◆ ParseString()

◆ pop()

◆ push()

◆ query() [1/2]

◆ query() [2/2]

◆ registerRelation()

◆ setParameters()

◆ setPredicateRepresentation()

◆ toString() [1/2]

◆ toString() [2/2]

◆ updateRule()