Object for managing fixedpoints More...
void Assert (params BoolExpr[] constraints) Assert a constraint (or multiple) into the fixedpoint solver. More...property about the predicate. The property is added at level. More...
Object for managing fixedpoints
Definition at line 29 of file Fixedpoint.cs.
◆ Add() void Add ( params BoolExpr[] constraints ) inlineAlias for Assert.
Definition at line 83 of file Fixedpoint.cs.
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the fixedpoint solver.
◆ AddCover() void AddCover ( int level, FuncDecl predicate, Expr property ) inlineAdd property about the predicate. The property is added at level.
Definition at line 215 of file Fixedpoint.cs.
217Native.Z3_fixedpoint_add_cover(
Context.nCtx, NativeObject, level, predicate.NativeObject, property.NativeObject);
Context Context
Access Context object
◆ AddFact() void AddFact ( FuncDecl pred, params uint[] args ) inlineAdd table fact to the fixedpoint solver.
Definition at line 113 of file Fixedpoint.cs.
115Debug.Assert(pred !=
null);
116Debug.Assert(args !=
null);
118 Context.CheckContextMatch(pred);
119Native.Z3_fixedpoint_add_fact(
Context.nCtx, NativeObject, pred.NativeObject, (uint)args.Length, args);
◆ AddRule()Add rule into the fixedpoint solver.
Definition at line 102 of file Fixedpoint.cs.
104Debug.Assert(rule !=
null);
106 Context.CheckContextMatch(rule);
107Native.Z3_fixedpoint_add_rule(
Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name));
◆ Assert() void Assert ( params BoolExpr[] constraints ) inlineAssert a constraint (or multiple) into the fixedpoint solver.
Definition at line 68 of file Fixedpoint.cs.
70Debug.Assert(constraints !=
null);
71Debug.Assert(constraints.All(c => c !=
null));
73 Context.CheckContextMatch<BoolExpr>(constraints);
74 foreach(BoolExpr a
inconstraints)
76Native.Z3_fixedpoint_assert(
Context.nCtx, NativeObject, a.NativeObject);
Referenced by Fixedpoint.Add().
◆ GetAnswer()Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that show unsatisfiability.
Definition at line 179 of file Fixedpoint.cs.
181IntPtr ans = Native.Z3_fixedpoint_get_answer(
Context.nCtx, NativeObject);
182 return(ans == IntPtr.Zero) ? null : Expr.Create(
Context, ans);
◆ GetCoverDelta()Retrieve the cover of a predicate.
Definition at line 205 of file Fixedpoint.cs.
207IntPtr res = Native.Z3_fixedpoint_get_cover_delta(
Context.nCtx, NativeObject, level, predicate.NativeObject);
208 return(res == IntPtr.Zero) ? null : Expr.Create(
Context, res);
◆ GetNumLevels() uint GetNumLevels ( FuncDecl predicate ) inlineRetrieve the number of levels explored for a given predicate.
Definition at line 197 of file Fixedpoint.cs.
199 returnNative.Z3_fixedpoint_get_num_levels(
Context.nCtx, NativeObject, predicate.NativeObject);
◆ GetReasonUnknown() string GetReasonUnknown ( ) inlineRetrieve explanation why fixedpoint engine returned status Unknown.
Definition at line 188 of file Fixedpoint.cs.
191 returnNative.Z3_fixedpoint_get_reason_unknown(
Context.nCtx, NativeObject);
◆ ParseFile()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.
295 usingASTVector av =
newASTVector(
Context, Native.Z3_fixedpoint_from_file(
Context.nCtx, NativeObject, file));
296 returnav.ToBoolExprArray();
◆ ParseString()Similar to ParseFile. Instead it takes as argument a string.
Definition at line 302 of file Fixedpoint.cs.
304 usingASTVector av =
newASTVector(
Context, Native.Z3_fixedpoint_from_string(
Context.nCtx, NativeObject, s));
305 returnav.ToBoolExprArray();
◆ Query() [1/2]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.
130Debug.Assert(query !=
null);
132 Context.CheckContextMatch(query);
138 default:
return Status.UNKNOWN;
Z3_lbool
Lifted Boolean type: false, undefined, true.
◆ Query() [2/2]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.
150Debug.Assert(relations !=
null);
151Debug.Assert(relations.All(rel => rel !=
null));
153 Context.CheckContextMatch<FuncDecl>(relations);
155AST.ArrayLength(relations), AST.ArrayToNative(relations));
160 default:
return Status.UNKNOWN;
◆ RegisterRelation()Register predicate as recursive relation.
Definition at line 91 of file Fixedpoint.cs.
93Debug.Assert(f !=
null);
96Native.Z3_fixedpoint_register_relation(
Context.nCtx, NativeObject, f.NativeObject);
◆ SetPredicateRepresentation()Instrument the Datalog engine on which table representation to use for recursive predicate.
Definition at line 231 of file Fixedpoint.cs.
233Debug.Assert(f !=
null);
235Native.Z3_fixedpoint_set_predicate_representation(
Context.nCtx, NativeObject,
236f.NativeObject, AST.ArrayLength(kinds), Symbol.ArrayToNative(kinds));
◆ ToString() [1/2] override string ToString ( ) inlineRetrieve internal string representation of fixedpoint object.
Definition at line 223 of file Fixedpoint.cs.
225 returnNative.Z3_fixedpoint_to_string(
Context.nCtx, NativeObject, 0,
null);
◆ ToString() [2/2] string ToString ( params BoolExpr[] queries ) inlineConvert benchmark given as set of axioms, rules and queries to a string.
Definition at line 243 of file Fixedpoint.cs.
246 returnNative.Z3_fixedpoint_to_string(
Context.nCtx, NativeObject,
247AST.ArrayLength(queries), AST.ArrayToNative(queries));
◆ UpdateRule()Update named rule into in the fixedpoint solver.
Definition at line 167 of file Fixedpoint.cs.
169Debug.Assert(rule !=
null);
171 Context.CheckContextMatch(rule);
172Native.Z3_fixedpoint_update_rule(
Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name));
◆ AssertionsRetrieve set of assertions added to fixedpoint context.
Definition at line 266 of file Fixedpoint.cs.
271 usingASTVector av =
newASTVector(
Context, Native.Z3_fixedpoint_get_assertions(
Context.nCtx, NativeObject));
272 returnav.ToBoolExprArray();
◆ HelpA string that describes all available fixedpoint solver parameters.
Definition at line 35 of file Fixedpoint.cs.
39 returnNative.Z3_fixedpoint_get_help(
Context.nCtx, NativeObject);
◆ ParameterDescriptionsRetrieves parameter descriptions for Fixedpoint solver.
Definition at line 59 of file Fixedpoint.cs.
61 get{
return newParamDescrs(
Context, Native.Z3_fixedpoint_get_param_descrs(
Context.nCtx, NativeObject)); }
◆ ParametersSets the fixedpoint solver parameters.
Definition at line 46 of file Fixedpoint.cs.
50Debug.Assert(value !=
null);
51 Context.CheckContextMatch(value);
52Native.Z3_fixedpoint_set_params(
Context.nCtx, NativeObject, value.NativeObject);
◆ RulesRetrieve set of rules added to fixedpoint context.
Definition at line 253 of file Fixedpoint.cs.
258 usingASTVector av =
newASTVector(
Context, Native.Z3_fixedpoint_get_rules(
Context.nCtx, NativeObject));
259 returnav.ToBoolExprArray();
◆ StatisticsRetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4