Object for managing fixedpoints More...
Data Structures | |
class | DecRefQueue |
Public Member Functions | |
void | Assert (params BoolExpr[] constraints) |
Assert a constraint (or multiple) into the fixedpoint solver. More... | |
void | Add (params BoolExpr[] constraints) |
Alias for Assert. More... | |
void | RegisterRelation (FuncDecl f) |
Register predicate as recursive relation. More... | |
void | AddRule (BoolExpr rule, Symbol name=null) |
Add rule into the fixedpoint solver. More... | |
void | AddFact (FuncDecl pred, params uint[] args) |
Add table fact to the fixedpoint solver. More... | |
Status | Query (BoolExpr query) |
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. More... | |
Status | Query (FuncDecl[] relations) |
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. More... | |
void | Push () |
Creates a backtracking point. More... | |
void | Pop () |
Backtrack one backtracking point. More... | |
void | UpdateRule (BoolExpr rule, Symbol name) |
Update named rule into in the fixedpoint solver. More... | |
Expr | GetAnswer () |
Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that show unsatisfiability. More... | |
string | GetReasonUnknown () |
Retrieve explanation why fixedpoint engine returned status Unknown. More... | |
uint | GetNumLevels (FuncDecl predicate) |
Retrieve the number of levels explored for a given predicate. More... | |
Expr | GetCoverDelta (int level, FuncDecl predicate) |
Retrieve the cover of a predicate. More... | |
void | AddCover (int level, FuncDecl predicate, Expr property) |
Add property about the predicate . The property is added at level . More... | |
override string | ToString () |
Retrieve internal string representation of fixedpoint object. More... | |
void | SetPredicateRepresentation (FuncDecl f, Symbol[] kinds) |
Instrument the Datalog engine on which table representation to use for recursive predicate. More... | |
string | ToString (BoolExpr[] queries) |
Convert benchmark given as set of axioms, rules and queries to a string. More... | |
BoolExpr[] | ParseFile (string file) |
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file. More... | |
BoolExpr[] | ParseString (string s) |
Similar to ParseFile. Instead it takes as argument a string. More... | |
![]() | |
void | Dispose () |
Disposes of the underlying native Z3 object. More... | |
Properties | |
string | Help [get] |
A string that describes all available fixedpoint solver parameters. More... | |
Params | Parameters [set] |
Sets the fixedpoint solver parameters. More... | |
ParamDescrs | ParameterDescriptions [get] |
Retrieves parameter descriptions for Fixedpoint solver. More... | |
BoolExpr[] | Rules [get] |
Retrieve set of rules added to fixedpoint context. More... | |
BoolExpr[] | Assertions [get] |
Retrieve set of assertions added to fixedpoint context. More... | |
Statistics | Statistics [get] |
Fixedpoint statistics. More... | |
Object for managing fixedpoints
Definition at line 29 of file Fixedpoint.cs.
|
inline |
Alias for Assert.
Definition at line 84 of file Fixedpoint.cs.
Add property
about the predicate
. The property is added at level
.
Definition at line 237 of file Fixedpoint.cs.
|
inline |
Add table fact to the fixedpoint solver.
Definition at line 114 of file Fixedpoint.cs.
Add rule into the fixedpoint solver.
Definition at line 103 of file Fixedpoint.cs.
|
inline |
Assert a constraint (or multiple) into the fixedpoint solver.
Definition at line 69 of file Fixedpoint.cs.
|
inline |
Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that show unsatisfiability.
Definition at line 200 of file Fixedpoint.cs.
Retrieve the cover of a predicate.
Definition at line 227 of file Fixedpoint.cs.
|
inline |
Retrieve the number of levels explored for a given predicate.
Definition at line 219 of file Fixedpoint.cs.
|
inline |
Retrieve explanation why fixedpoint engine returned status Unknown.
Definition at line 209 of file Fixedpoint.cs.
|
inline |
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 318 of file Fixedpoint.cs.
|
inline |
Similar to ParseFile. Instead it takes as argument a string.
Definition at line 327 of file Fixedpoint.cs.
|
inline |
Backtrack one backtracking point.
Note that an exception is thrown if Pop is called without a corresponding Push
Definition at line 179 of file Fixedpoint.cs.
|
inline |
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 129 of file Fixedpoint.cs.
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 149 of file Fixedpoint.cs.
|
inline |
Register predicate as recursive relation.
Definition at line 92 of file Fixedpoint.cs.
Instrument the Datalog engine on which table representation to use for recursive predicate.
Definition at line 253 of file Fixedpoint.cs.
|
inline |
Retrieve internal string representation of fixedpoint object.
Definition at line 245 of file Fixedpoint.cs.
|
inline |
Convert benchmark given as set of axioms, rules and queries to a string.
Definition at line 265 of file Fixedpoint.cs.
Update named rule into in the fixedpoint solver.
Definition at line 188 of file Fixedpoint.cs.
|
get |
Retrieve set of assertions added to fixedpoint context.
Definition at line 290 of file Fixedpoint.cs.
|
get |
A string that describes all available fixedpoint solver parameters.
Definition at line 36 of file Fixedpoint.cs.
|
get |
Retrieves parameter descriptions for Fixedpoint solver.
Definition at line 61 of file Fixedpoint.cs.
|
set |
Sets the fixedpoint solver parameters.
Definition at line 48 of file Fixedpoint.cs.
|
get |
Retrieve set of rules added to fixedpoint context.
Definition at line 276 of file Fixedpoint.cs.
|
get |
Fixedpoint statistics.
Definition at line 304 of file Fixedpoint.cs.