39 Contract.Ensures(Contract.Result<
string>() != null);
40 return Native.Z3_fixedpoint_get_help(
Context.nCtx, NativeObject);
51 Contract.Requires(value != null);
52 Context.CheckContextMatch(value);
53 Native.Z3_fixedpoint_set_params(
Context.nCtx, NativeObject, value.NativeObject);
71 Contract.Requires(constraints != null);
72 Contract.Requires(Contract.ForAll(constraints, c => c != null));
77 Native.Z3_fixedpoint_assert(
Context.nCtx, NativeObject, a.NativeObject);
94 Contract.Requires(f != null);
97 Native.Z3_fixedpoint_register_relation(
Context.nCtx, NativeObject, f.NativeObject);
105 Contract.Requires(rule != null);
107 Context.CheckContextMatch(rule);
108 Native.Z3_fixedpoint_add_rule(
Context.nCtx, NativeObject, rule.NativeObject,
AST.GetNativeObject(name));
116 Contract.Requires(pred != null);
117 Contract.Requires(args != null);
119 Context.CheckContextMatch(pred);
120 Native.Z3_fixedpoint_add_fact(
Context.nCtx, NativeObject, pred.NativeObject, (uint)args.Length, args);
131 Contract.Requires(query != null);
133 Context.CheckContextMatch(query);
139 default:
return Status.UNKNOWN;
151 Contract.Requires(relations != null);
152 Contract.Requires(Contract.ForAll(0, relations.Length, i => relations[i] != null));
156 AST.ArrayLength(relations),
AST.ArrayToNative(relations));
161 default:
return Status.UNKNOWN;
171 Native.Z3_fixedpoint_push(
Context.nCtx, NativeObject);
181 Native.Z3_fixedpoint_pop(
Context.nCtx, NativeObject);
190 Contract.Requires(rule != null);
192 Context.CheckContextMatch(rule);
193 Native.Z3_fixedpoint_update_rule(
Context.nCtx, NativeObject, rule.NativeObject,
AST.GetNativeObject(name));
202 IntPtr ans = Native.Z3_fixedpoint_get_answer(
Context.nCtx, NativeObject);
203 return (ans == IntPtr.Zero) ? null :
Expr.Create(
Context, ans);
211 Contract.Ensures(Contract.Result<
string>() != null);
213 return Native.Z3_fixedpoint_get_reason_unknown(
Context.nCtx, NativeObject);
221 return Native.Z3_fixedpoint_get_num_levels(
Context.nCtx, NativeObject, predicate.NativeObject);
229 IntPtr res = Native.Z3_fixedpoint_get_cover_delta(
Context.nCtx, NativeObject, level, predicate.NativeObject);
230 return (res == IntPtr.Zero) ? null :
Expr.Create(
Context, res);
239 Native.Z3_fixedpoint_add_cover(
Context.nCtx, NativeObject, level, predicate.NativeObject, property.NativeObject);
247 return Native.Z3_fixedpoint_to_string(
Context.nCtx, NativeObject, 0, null);
255 Contract.Requires(f != null);
257 Native.Z3_fixedpoint_set_predicate_representation(
Context.nCtx, NativeObject,
258 f.NativeObject,
AST.ArrayLength(kinds),
Symbol.ArrayToNative(kinds));
268 return Native.Z3_fixedpoint_to_string(
Context.nCtx, NativeObject,
269 AST.ArrayLength(queries),
AST.ArrayToNative(queries));
279 Contract.Ensures(Contract.Result<
BoolExpr[]>() != null);
293 Contract.Ensures(Contract.Result<
BoolExpr[]>() != null);
307 Contract.Ensures(Contract.Result<
Statistics>() != null);
338 Contract.Requires(ctx != null);
341 : base(ctx, Native.Z3_mk_fixedpoint(ctx.nCtx))
343 Contract.Requires(ctx != null);
348 public DecRefQueue() : base() { }
349 public DecRefQueue(uint move_limit) : base(move_limit) { }
350 internal override void IncRef(
Context ctx, IntPtr obj)
352 Native.Z3_fixedpoint_inc_ref(ctx.nCtx, obj);
355 internal override void DecRef(
Context ctx, IntPtr obj)
357 Native.Z3_fixedpoint_dec_ref(ctx.nCtx, obj);
361 internal override void IncRef(IntPtr o)
367 internal override void DecRef(IntPtr o)
string ToString(BoolExpr[] queries)
Convert benchmark given as set of axioms, rules and queries to a string.
void Add(params BoolExpr[] constraints)
Alias for Assert.
Objects of this class track statistical information about solvers.
void UpdateRule(BoolExpr rule, Symbol name)
Update named rule into in the fixedpoint solver.
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the fixedpoint solver.
Expr GetCoverDelta(int level, FuncDecl predicate)
Retrieve the cover of a predicate.
string GetReasonUnknown()
Retrieve explanation why fixedpoint engine returned status Unknown.
void SetPredicateRepresentation(FuncDecl f, Symbol[] kinds)
Instrument the Datalog engine on which table representation to use for recursive predicate.
BoolExpr [] ParseString(string s)
Similar to ParseFile. Instead it takes as argument a string.
BoolExpr [] ParseFile(string file)
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context...
Z3_lbool
Lifted Boolean type: false, undefined, true.
void AddCover(int level, FuncDecl predicate, Expr property)
Add property about the predicate. The property is added at level.
Status Query(FuncDecl[] relations)
Query the fixedpoint solver. A query is an array of relations. The query is satisfiable if there is a...
BoolExpr [] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
Expr GetAnswer()
Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that...
A Params objects represents a configuration in the form of Symbol/value pairs.
A ParamDescrs describes a set of parameters.
void AddFact(FuncDecl pred, params uint[] args)
Add table fact to the fixedpoint solver.
The main interaction with Z3 happens via the Context.
IDecRefQueue Fixedpoint_DRQ
FixedPoint DRQ
The abstract syntax tree (AST) class.
uint GetNumLevels(FuncDecl predicate)
Retrieve the number of levels explored for a given predicate.
Object for managing fixedpoints
void Pop()
Backtrack one backtracking point.
void RegisterRelation(FuncDecl f)
Register predicate as recursive relation.
void Push()
Creates a backtracking point.
void AddRule(BoolExpr rule, Symbol name=null)
Add rule into the fixedpoint solver.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
override string ToString()
Retrieve internal string representation of fixedpoint object.
Symbols are used to name several term and type constructors.
Status Query(BoolExpr query)
Query the fixedpoint solver. A query is a conjunction of constraints. The constraints may include the...