21using System.Diagnostics;
39 return Native.Z3_fixedpoint_get_help(
Context.nCtx, NativeObject);
50 Debug.Assert(value !=
null);
51 Context.CheckContextMatch(value);
52 Native.Z3_fixedpoint_set_params(
Context.nCtx, NativeObject, value.NativeObject);
70 Debug.Assert(constraints !=
null);
71 Debug.Assert(constraints.All(c => c !=
null));
76 Native.Z3_fixedpoint_assert(
Context.nCtx, NativeObject, a.NativeObject);
93 Debug.Assert(f !=
null);
96 Native.Z3_fixedpoint_register_relation(
Context.nCtx, NativeObject, f.NativeObject);
104 Debug.Assert(rule !=
null);
106 Context.CheckContextMatch(rule);
107 Native.Z3_fixedpoint_add_rule(
Context.nCtx, NativeObject, rule.NativeObject,
AST.GetNativeObject(name));
115 Debug.Assert(pred !=
null);
116 Debug.Assert(args !=
null);
118 Context.CheckContextMatch(pred);
119 Native.Z3_fixedpoint_add_fact(
Context.nCtx, NativeObject, pred.NativeObject, (uint)args.Length, args);
130 Debug.Assert(query !=
null);
132 Context.CheckContextMatch(query);
138 default:
return Status.UNKNOWN;
150 Debug.Assert(relations !=
null);
151 Debug.Assert(relations.All(rel => rel !=
null));
155 AST.ArrayLength(relations),
AST.ArrayToNative(relations));
160 default:
return Status.UNKNOWN;
169 Debug.Assert(rule !=
null);
171 Context.CheckContextMatch(rule);
172 Native.Z3_fixedpoint_update_rule(
Context.nCtx, NativeObject, rule.NativeObject,
AST.GetNativeObject(name));
181 IntPtr ans = Native.Z3_fixedpoint_get_answer(
Context.nCtx, NativeObject);
182 return (ans == IntPtr.Zero) ? null :
Expr.Create(
Context, ans);
191 return Native.Z3_fixedpoint_get_reason_unknown(
Context.nCtx, NativeObject);
199 return Native.Z3_fixedpoint_get_num_levels(
Context.nCtx, NativeObject, predicate.NativeObject);
207 IntPtr res = Native.Z3_fixedpoint_get_cover_delta(
Context.nCtx, NativeObject, level, predicate.NativeObject);
208 return (res == IntPtr.Zero) ? null :
Expr.Create(
Context, res);
217 Native.Z3_fixedpoint_add_cover(
Context.nCtx, NativeObject, level, predicate.NativeObject, property.NativeObject);
225 return Native.Z3_fixedpoint_to_string(
Context.nCtx, NativeObject, 0,
null);
233 Debug.Assert(f !=
null);
235 Native.Z3_fixedpoint_set_predicate_representation(
Context.nCtx, NativeObject,
236 f.NativeObject,
AST.ArrayLength(kinds),
Symbol.ArrayToNative(kinds));
246 return Native.Z3_fixedpoint_to_string(
Context.nCtx, NativeObject,
247 AST.ArrayLength(queries),
AST.ArrayToNative(queries));
313 Debug.Assert(ctx !=
null);
315 internal Fixedpoint(Context ctx)
318 Debug.Assert(ctx !=
null);
321 internal class DecRefQueue : IDecRefQueue
323 public DecRefQueue() : base() { }
324 public DecRefQueue(uint move_limit) : base(move_limit) { }
325 internal override void IncRef(Context ctx, IntPtr obj)
327 Native.Z3_fixedpoint_inc_ref(ctx.nCtx, obj);
330 internal override void DecRef(Context ctx, IntPtr obj)
332 Native.Z3_fixedpoint_dec_ref(ctx.nCtx, obj);
336 internal override void IncRef(IntPtr o)
342 internal override void DecRef(IntPtr o)
The abstract syntax tree (AST) class.
BoolExpr[] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
The main interaction with Z3 happens via the Context.
IDecRefQueue Fixedpoint_DRQ
FixedPoint DRQ
Object for managing fixedpoints
BoolExpr[] Assertions
Retrieve set of assertions added to fixedpoint context.
BoolExpr[] Rules
Retrieve set of rules added to fixedpoint context.
string Help
A string that describes all available fixedpoint solver parameters.
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the fixedpoint solver.
void AddRule(BoolExpr rule, Symbol name=null)
Add rule into the fixedpoint solver.
uint GetNumLevels(FuncDecl predicate)
Retrieve the number of levels explored for a given predicate.
Status Query(params FuncDecl[] relations)
Query the fixedpoint solver. A query is an array of relations. The query is satisfiable if there is a...
Params Parameters
Sets the fixedpoint solver parameters.
Statistics Statistics
Fixedpoint statistics.
Expr GetCoverDelta(int level, FuncDecl predicate)
Retrieve the cover of a predicate.
string GetReasonUnknown()
Retrieve explanation why fixedpoint engine returned status Unknown.
ParamDescrs ParameterDescriptions
Retrieves parameter descriptions for Fixedpoint solver.
void RegisterRelation(FuncDecl f)
Register predicate as recursive relation.
BoolExpr[] ParseString(string s)
Similar to ParseFile. Instead it takes as argument a string.
override string ToString()
Retrieve internal string representation of fixedpoint object.
Status Query(BoolExpr query)
Query the fixedpoint solver. A query is a conjunction of constraints. The constraints may include the...
void AddCover(int level, FuncDecl predicate, Expr property)
Add property about the predicate. The property is added at level.
Expr GetAnswer()
Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that...
BoolExpr[] ParseFile(string file)
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context....
void SetPredicateRepresentation(FuncDecl f, Symbol[] kinds)
Instrument the Datalog engine on which table representation to use for recursive predicate.
string ToString(params BoolExpr[] queries)
Convert benchmark given as set of axioms, rules and queries to a string.
void UpdateRule(BoolExpr rule, Symbol name)
Update named rule into in the fixedpoint solver.
void Add(params BoolExpr[] constraints)
Alias for Assert.
void AddFact(FuncDecl pred, params uint[] args)
Add table fact to the fixedpoint solver.
A ParamDescrs describes a set of parameters.
A Params objects represents a configuration in the form of Symbol/value pairs.
Objects of this class track statistical information about solvers.
Symbols are used to name several term and type constructors.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Z3_lbool
Lifted Boolean type: false, undefined, true.
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.