Fixedpoint class
Interface to the Z3 fixedpoint solver.
The default fixed-point engine is a bottom-up Datalog engine. It works with finite relations and uses finite table representations as hash tables as the default way to represent finite relations.
Properties
- hashCode → int
-
The hash code for this object.
no setterinherited
- runtimeType → Type
-
A representation of the runtime type of the object.
no setterinherited
Methods
-
addConstraint(
Expr axiom, int level) → void - Adds a constraint. (?)
-
addCover(
int level, FuncDecl pred, AST property) → void -
Add a property of predicate
predatlevel. It gets pushed forward when possible. -
addFact(
FuncDecl relation, List< int> args) → void - Adds a fact to this solver.
-
addRule(
Expr rule, Sym name) → void - Adds a rule to this solver.
-
addSmtlib(
String s) → List< AST> - Parses an SMT-LIB file with fixedpoint rules and adds them to this context, returning the queries.
-
addSmtlibFile(
File file) → List< AST> - Same as addSmtlib but reads from a file.
-
assertConstraint(
Expr axiom) → void - Assert a constraint as a background axiom.
-
getAnswer(
) → AST - Gets the answer to the last query, assuming it was satisfiable.
-
getAssertions(
) → List< Expr> - Returns the set of background assertions.
-
getCoverDelta(
int level, FuncDecl pred) → void -
Retrieve the current cover of
predup tolevelunfoldings. -
getHelp(
) → String - Returns a description of the available parameters.
-
getNumLevels(
FuncDecl pred) → void - Query the PDR engine for the maximal levels properties are known about predicate.
-
getParamDescriptions(
) → ParamDescs - Returns a description of the available parameters.
-
getReasonUnknown(
) → String - Gets the reason why the last query was unsatisfiable.
-
getRules(
) → List< Expr> - Returns the set of rules.
-
getStatistics(
) → Stats - Gets statistics (timing, memory consumption, etc) collected of the last call to query.
-
noSuchMethod(
Invocation invocation) → dynamic -
Invoked when a nonexistent method or property is accessed.
inherited
-
query(
Expr query) → bool? - Query the rule table, returns true if the query is satisfiable.
-
queryRelations(
List< FuncDecl> relations) → bool? - Query multiple relations, returns true if the query is satisfiable.
-
registerRelation(
FuncDecl relation) → void - Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics. For example, the relation is empty if it does not occur in a head or a fact.
-
setOnLemma(
void f(AST, int level)?) → void - Registers a callback for lemmas.
-
setOnPredecessor(
void f()?) → void - Registers a callback for predecessors.
-
setOnReduceApply(
AST? f(FuncDecl func, List< AST> args)?) → void - Registers a callback for for building terms based on the relational operators.
-
setOnReduceAssign(
List< AST> f(List<AST> args, List<AST> outs)?) → void - Registers a callback for destructive updates.
-
setOnUnfold(
void f()?) → void - Registers a callback for unfolding.
-
setParams(
Params params) → void - Sets the parameters for this solver, see getParamDescriptions for a description of the available parameters.
-
setPredicateRepresentation(
FuncDecl relation, List< Sym> kinds) → void - Configure the predicate representation.
-
toString(
[List< AST> ? extra]) → String -
A string representation of this object.
override
-
updateRule(
Expr rule, Sym name) → void - Update a named rule.
Operators
-
operator ==(
Object other) → bool -
The equality operator.
inherited