21 using System.Diagnostics.Contracts;
28 [ContractVerification(
true)]
39 Contract.Ensures(Contract.Result<
string>() != null);
51 Contract.Requires(value != null);
52 Context.CheckContextMatch(value);
71 Contract.Requires(constraints != null);
72 Contract.Requires(Contract.ForAll(constraints, c => c != null));
74 Context.CheckContextMatch(constraints);
94 Contract.Requires(f != null);
105 Contract.Requires(rule != null);
107 Context.CheckContextMatch(rule);
116 Contract.Requires(pred != null);
117 Contract.Requires(args != null);
119 Context.CheckContextMatch(pred);
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));
154 Context.CheckContextMatch(relations);
156 AST.ArrayLength(relations),
AST.ArrayToNative(relations));
161 default:
return Status.UNKNOWN;
190 Contract.Requires(rule != null);
192 Context.CheckContextMatch(rule);
203 return (ans == IntPtr.Zero) ? null :
Expr.Create(
Context, ans);
211 Contract.Ensures(Contract.Result<
string>() != null);
230 return (res == IntPtr.Zero) ? null :
Expr.Create(
Context, res);
255 Contract.Requires(f != null);
258 f.NativeObject,
AST.ArrayLength(kinds),
Symbol.ArrayToNative(kinds));
269 AST.ArrayLength(queries),
AST.ArrayToNative(queries));
275 for (uint i = 0; i < n; i++)
283 public BoolExpr[] Rules
287 Contract.Ensures(Contract.Result<
BoolExpr[]>() != null);
300 Contract.Ensures(Contract.Result<
BoolExpr[]>() != null);
328 Contract.Requires(ctx != null);
330 internal Fixedpoint(Context ctx)
333 Contract.Requires(ctx != null);
336 internal class DecRefQueue : IDecRefQueue
338 public DecRefQueue() : base() { }
339 public DecRefQueue(uint move_limit) : base(move_limit) { }
340 internal override void IncRef(Context ctx, IntPtr obj)
342 Native.Z3_fixedpoint_inc_ref(ctx.nCtx, obj);
345 internal override void DecRef(Context ctx, IntPtr obj)
347 Native.Z3_fixedpoint_dec_ref(ctx.nCtx, obj);
351 internal override void IncRef(IntPtr o)
353 Context.Fixedpoint_DRQ.IncAndClear(Context, o);
357 internal override void DecRef(IntPtr o)
359 Context.Fixedpoint_DRQ.Add(o);
static void Z3_fixedpoint_push(Z3_context a0, Z3_fixedpoint a1)
string ToString(BoolExpr[] queries)
Convert benchmark given as set of axioms, rules and queries to a string.
static Z3_ast Z3_fixedpoint_get_answer(Z3_context a0, Z3_fixedpoint a1)
static void Z3_fixedpoint_register_relation(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2)
void Add(params BoolExpr[] constraints)
Alias for Assert.
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.
static void Z3_fixedpoint_set_params(Z3_context a0, Z3_fixedpoint a1, Z3_params a2)
Expr GetCoverDelta(int level, FuncDecl predicate)
Retrieve the cover of a predicate.
static int Z3_fixedpoint_query(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2)
static void Z3_fixedpoint_pop(Z3_context a0, Z3_fixedpoint a1)
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.
static void Z3_fixedpoint_assert(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2)
static void Z3_fixedpoint_set_predicate_representation(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2, uint a3, [In] IntPtr[] a4)
BoolExpr[] ParseString(string s)
Similar to ParseFile. Instead it takes as argument a string.
static void Z3_fixedpoint_add_rule(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2, IntPtr a3)
BoolExpr[] ParseFile(string file)
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context...
static void Z3_fixedpoint_update_rule(Z3_context a0, Z3_fixedpoint a1, Z3_ast a2, IntPtr a3)
uint Size
The size of the vector
static int Z3_fixedpoint_query_relations(Z3_context a0, Z3_fixedpoint a1, uint a2, [In] Z3_func_decl[] a3)
static string Z3_fixedpoint_get_help(Z3_context a0, Z3_fixedpoint a1)
static void Z3_fixedpoint_add_fact(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2, uint a3, [In] uint[] a4)
static void Z3_fixedpoint_add_cover(Z3_context a0, Z3_fixedpoint a1, int a2, Z3_func_decl a3, Z3_ast a4)
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.
static Z3_ast_vector Z3_fixedpoint_get_rules(Z3_context a0, Z3_fixedpoint a1)
static Z3_ast_vector Z3_fixedpoint_get_assertions(Z3_context a0, Z3_fixedpoint a1)
Status Query(FuncDecl[] relations)
Query the fixedpoint solver. A query is an array of relations. The query is satisfiable if there is a...
static string Z3_fixedpoint_get_reason_unknown(Z3_context a0, Z3_fixedpoint a1)
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.
static Z3_ast_vector Z3_fixedpoint_from_file(Z3_context a0, Z3_fixedpoint a1, string a2)
void AddFact(FuncDecl pred, params uint[] args)
Add table fact to the fixedpoint solver.
The main interaction with Z3 happens via the Context.
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(__in Z3_context c)
Create a new fixedpoint context.
static Z3_ast_vector Z3_fixedpoint_from_string(Z3_context a0, Z3_fixedpoint a1, string a2)
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.
static uint Z3_fixedpoint_get_num_levels(Z3_context a0, Z3_fixedpoint a1, Z3_func_decl a2)
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.
static string Z3_fixedpoint_to_string(Z3_context a0, Z3_fixedpoint a1, uint a2, [In] Z3_ast[] a3)
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...
static Z3_ast Z3_fixedpoint_get_cover_delta(Z3_context a0, Z3_fixedpoint a1, int a2, Z3_func_decl a3)
static Z3_param_descrs Z3_fixedpoint_get_param_descrs(Z3_context a0, Z3_fixedpoint a1)