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));
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);
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)
355 internal override void DecRef(
Context ctx, IntPtr obj)
361 internal override void IncRef(IntPtr o)
367 internal override void DecRef(IntPtr o)
static void Z3_fixedpoint_dec_ref(Z3_context a0, Z3_fixedpoint a1)
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.
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.
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 Z3_stats Z3_fixedpoint_get_statistics(Z3_context a0, Z3_fixedpoint a1)
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)
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 void Z3_fixedpoint_inc_ref(Z3_context a0, Z3_fixedpoint a1)
BoolExpr[] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
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.
static Z3_fixedpoint Z3_mk_fixedpoint(Z3_context a0)
IDecRefQueue Fixedpoint_DRQ
FixedPoint DRQ
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)