Object for managing fixedpoints More...

Inheritance diagram for Fixedpoint:

Public Member Functions
void	Assert (params BoolExpr[] constraints)
	Assert a constraint (or multiple) into the fixedpoint solver. More...

void	Add (params BoolExpr[] constraints)
	Alias for Assert. More...

void	RegisterRelation (FuncDecl f)
	Register predicate as recursive relation. More...

void	AddRule (BoolExpr rule, Symbol name=null)
	Add rule into the fixedpoint solver. More...

void	AddFact (FuncDecl pred, params uint[] args)
	Add table fact to the fixedpoint solver. More...

Status	Query (BoolExpr query)
	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. More...

Status	Query (params FuncDecl[] relations)
	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. More...

void	UpdateRule (BoolExpr rule, Symbol name)
	Update named rule into in the fixedpoint solver. More...

Expr	GetAnswer ()
	Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that show unsatisfiability. More...

string	GetReasonUnknown ()
	Retrieve explanation why fixedpoint engine returned status Unknown. More...

uint	GetNumLevels (FuncDecl predicate)
	Retrieve the number of levels explored for a given predicate. More...

Expr	GetCoverDelta (int level, FuncDecl predicate)
	Retrieve the cover of a predicate. More...

void	AddCover (int level, FuncDecl predicate, Expr property)
	Add `property` about the `predicate`. The property is added at `level`. More...

override string	ToString ()
	Retrieve internal string representation of fixedpoint object. More...

void	SetPredicateRepresentation (FuncDecl f, Symbol[] kinds)
	Instrument the Datalog engine on which table representation to use for recursive predicate. More...

string	ToString (params BoolExpr[] queries)
	Convert benchmark given as set of axioms, rules and queries to a string. More...

BoolExpr[]	ParseFile (string file)
	Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file. More...

BoolExpr[]	ParseString (string s)
	Similar to ParseFile. Instead it takes as argument a string. More...

Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object. More...

Properties
string	Help `[get]`
	A string that describes all available fixedpoint solver parameters. More...

Params	Parameters `[set]`
	Sets the fixedpoint solver parameters. More...

ParamDescrs	ParameterDescriptions `[get]`
	Retrieves parameter descriptions for Fixedpoint solver. More...

BoolExpr[]	Rules `[get]`
	Retrieve set of rules added to fixedpoint context. More...

BoolExpr[]	Assertions `[get]`
	Retrieve set of assertions added to fixedpoint context. More...

Statistics	Statistics `[get]`
	Fixedpoint statistics. More...

Properties inherited from Z3Object
Context	Context `[get]`
	Access Context object More...

Detailed Description

Object for managing fixedpoints

Definition at line 29 of file Fixedpoint.cs.

Member Function Documentation

◆ Add()

void Add ( params BoolExpr[] constraints )

inline

Alias for Assert.

Definition at line 83 of file Fixedpoint.cs.

         {
             Assert(constraints);
         }

◆ AddCover()

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

inline

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

Definition at line 215 of file Fixedpoint.cs.

         {
             Native.Z3_fixedpoint_add_cover(Context.nCtx, NativeObject, level, predicate.NativeObject, property.NativeObject);
         }

◆ AddFact()

void AddFact	(	FuncDecl	pred,
		params uint[]	args
	)

inline

Add table fact to the fixedpoint solver.

Definition at line 113 of file Fixedpoint.cs.

         {
             Debug.Assert(pred != null);
             Debug.Assert(args != null);
  
             Context.CheckContextMatch(pred);
             Native.Z3_fixedpoint_add_fact(Context.nCtx, NativeObject, pred.NativeObject, (uint)args.Length, args);
         }

◆ AddRule()

void AddRule	(	BoolExpr	rule,
		Symbol	name = `null`
	)

inline

Add rule into the fixedpoint solver.

Definition at line 102 of file Fixedpoint.cs.

         {
             Debug.Assert(rule != null);
  
             Context.CheckContextMatch(rule);
             Native.Z3_fixedpoint_add_rule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name));
         }

◆ Assert()

void Assert ( params BoolExpr[] constraints )

inline

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

Definition at line 68 of file Fixedpoint.cs.

         {
             Debug.Assert(constraints != null);
             Debug.Assert(constraints.All(c => c != null));
  
             Context.CheckContextMatch<BoolExpr>(constraints);
             foreach (BoolExpr a in constraints)
             {
                 Native.Z3_fixedpoint_assert(Context.nCtx, NativeObject, a.NativeObject);
             }
         }

Referenced by Fixedpoint.Add().

◆ GetAnswer()

Expr GetAnswer ( )

inline

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

Definition at line 179 of file Fixedpoint.cs.

         {
             IntPtr ans = Native.Z3_fixedpoint_get_answer(Context.nCtx, NativeObject);
             return (ans == IntPtr.Zero) ? null : Expr.Create(Context, ans);
         }

◆ GetCoverDelta()

Expr GetCoverDelta	(	int	level,
		FuncDecl	predicate
	)

inline

Retrieve the cover of a predicate.

Definition at line 205 of file Fixedpoint.cs.

         {
             IntPtr res = Native.Z3_fixedpoint_get_cover_delta(Context.nCtx, NativeObject, level, predicate.NativeObject);
             return (res == IntPtr.Zero) ? null : Expr.Create(Context, res);
         }

◆ GetNumLevels()

uint GetNumLevels ( FuncDecl predicate )

inline

Retrieve the number of levels explored for a given predicate.

Definition at line 197 of file Fixedpoint.cs.

         {
             return Native.Z3_fixedpoint_get_num_levels(Context.nCtx, NativeObject, predicate.NativeObject);
         }

◆ GetReasonUnknown()

string GetReasonUnknown ( )

inline

Retrieve explanation why fixedpoint engine returned status Unknown.

Definition at line 188 of file Fixedpoint.cs.

         {
  
             return Native.Z3_fixedpoint_get_reason_unknown(Context.nCtx, NativeObject);
         }

◆ 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 293 of file Fixedpoint.cs.

         {
             using ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file));
             return av.ToBoolExprArray();
         }

◆ ParseString()

BoolExpr [] ParseString ( string s )

inline

Similar to ParseFile. Instead it takes as argument a string.

Definition at line 302 of file Fixedpoint.cs.

         {
             using ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s));
             return av.ToBoolExprArray();
         }

◆ 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.

Definition at line 128 of file Fixedpoint.cs.

         {
             Debug.Assert(query != null);
  
             Context.CheckContextMatch(query);
             Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query(Context.nCtx, NativeObject, query.NativeObject);
             switch (r)
             {
                 case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
                 case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
                 default: return Status.UNKNOWN;
             }
         }

◆ Query() [2/2]

Status Query ( params 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.

Definition at line 148 of file Fixedpoint.cs.

         {
             Debug.Assert(relations != null);
             Debug.Assert(relations.All(rel => rel != null));
  
             Context.CheckContextMatch<FuncDecl>(relations);
             Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query_relations(Context.nCtx, NativeObject,
                                    AST.ArrayLength(relations), AST.ArrayToNative(relations));
             switch (r)
             {
                 case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
                 case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
                 default: return Status.UNKNOWN;
             }
         }

◆ RegisterRelation()

void RegisterRelation ( FuncDecl f )

inline

Register predicate as recursive relation.

Definition at line 91 of file Fixedpoint.cs.

         {
             Debug.Assert(f != null);
  
             Context.CheckContextMatch(f);
             Native.Z3_fixedpoint_register_relation(Context.nCtx, NativeObject, f.NativeObject);
         }

◆ SetPredicateRepresentation()

void SetPredicateRepresentation	(	FuncDecl	f,
		Symbol[]	kinds
	)

inline

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

Definition at line 231 of file Fixedpoint.cs.

         {
             Debug.Assert(f != null);
  
             Native.Z3_fixedpoint_set_predicate_representation(Context.nCtx, NativeObject,
                                f.NativeObject, AST.ArrayLength(kinds), Symbol.ArrayToNative(kinds));
  
         }

◆ ToString() [1/2]

override string ToString ( )

inline

Retrieve internal string representation of fixedpoint object.

Definition at line 223 of file Fixedpoint.cs.

         {
             return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject, 0, null);
         }

◆ ToString() [2/2]

string ToString ( params BoolExpr[] queries )

inline

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

Definition at line 243 of file Fixedpoint.cs.

         {
  
             return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject,
                              AST.ArrayLength(queries), AST.ArrayToNative(queries));
         }

◆ UpdateRule()

void UpdateRule	(	BoolExpr	rule,
		Symbol	name
	)

inline

Update named rule into in the fixedpoint solver.

Definition at line 167 of file Fixedpoint.cs.

         {
             Debug.Assert(rule != null);
  
             Context.CheckContextMatch(rule);
             Native.Z3_fixedpoint_update_rule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name));
         }

Property Documentation

◆ Assertions

BoolExpr [] Assertions

get

Retrieve set of assertions added to fixedpoint context.

Definition at line 266 of file Fixedpoint.cs.

         {
             get
             {
  
                 using ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject));
                 return av.ToBoolExprArray();
             }
         }

◆ Help

string Help

get

A string that describes all available fixedpoint solver parameters.

Definition at line 35 of file Fixedpoint.cs.

         {
             get
             {
                 return Native.Z3_fixedpoint_get_help(Context.nCtx, NativeObject);
             }
         }

◆ ParameterDescriptions

ParamDescrs ParameterDescriptions

get

Retrieves parameter descriptions for Fixedpoint solver.

Definition at line 59 of file Fixedpoint.cs.

         {
             get { return new ParamDescrs(Context, Native.Z3_fixedpoint_get_param_descrs(Context.nCtx, NativeObject)); }
         }

◆ Parameters

Params Parameters

set

Sets the fixedpoint solver parameters.

Definition at line 46 of file Fixedpoint.cs.

         {
             set
             {
                 Debug.Assert(value != null);
                 Context.CheckContextMatch(value);
                 Native.Z3_fixedpoint_set_params(Context.nCtx, NativeObject, value.NativeObject);
             }
         }

◆ Rules

BoolExpr [] Rules

get

Retrieve set of rules added to fixedpoint context.

Definition at line 253 of file Fixedpoint.cs.

         {
             get
             {
  
                 using ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
                 return av.ToBoolExprArray();
             }
         }

◆ Statistics

Statistics Statistics

get

Fixedpoint statistics.

Definition at line 279 of file Fixedpoint.cs.

         {
             get
             {
  
                 return new Statistics(Context, Native.Z3_fixedpoint_get_statistics(Context.nCtx, NativeObject));
             }
         }

Public Member Functions

Properties

Detailed Description

Member Function Documentation

◆ Add()

◆ AddCover()

◆ AddFact()

◆ AddRule()

◆ Assert()

◆ GetAnswer()

◆ GetCoverDelta()

◆ GetNumLevels()

◆ GetReasonUnknown()

◆ ParseFile()

◆ ParseString()

◆ Query() [1/2]

◆ Query() [2/2]

◆ RegisterRelation()

◆ SetPredicateRepresentation()

◆ ToString() [1/2]

◆ ToString() [2/2]

◆ UpdateRule()

Property Documentation

◆ Assertions

◆ Help

◆ ParameterDescriptions

◆ Parameters

◆ Rules

◆ Statistics