Module Z3.Fixedpoint

module Fixedpoint: sig .. end

Fixedpoint solving

type fixedpoint

val get_help : fixedpoint -> string

A string that describes all available fixedpoint solver parameters.

val set_parameters : fixedpoint -> Params.params -> unit

Sets the fixedpoint solver parameters.

val get_param_descrs : fixedpoint -> Params.ParamDescrs.param_descrs

Retrieves parameter descriptions for Fixedpoint solver.

val add : fixedpoint -> Expr.expr list -> unit

Assert a constraints into the fixedpoint solver.

val register_relation : fixedpoint -> FuncDecl.func_decl -> unit

val add_rule : fixedpoint -> Expr.expr -> Symbol.symbol option -> unit

Add rule into the fixedpoint solver.

val add_fact : fixedpoint -> FuncDecl.func_decl -> int list -> unit

Add table fact to the fixedpoint solver.

val query : fixedpoint -> Expr.expr -> Solver.status

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.

val query_r : fixedpoint -> FuncDecl.func_decl list -> Solver.status

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.

val update_rule : fixedpoint -> Expr.expr -> Symbol.symbol -> unit

Update named rule into in the fixedpoint solver.

val get_answer : fixedpoint -> Expr.expr option

Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that show unsatisfiability.

val get_reason_unknown : fixedpoint -> string

Retrieve explanation why fixedpoint engine returned status Unknown.

val get_num_levels : fixedpoint -> FuncDecl.func_decl -> int

Retrieve the number of levels explored for a given predicate.

val get_cover_delta : fixedpoint ->
       int -> FuncDecl.func_decl -> Expr.expr option

Retrieve the cover of a predicate.

val add_cover : fixedpoint ->
       int -> FuncDecl.func_decl -> Expr.expr -> unit

Add <tt>property</tt> about the <tt>predicate</tt>. The property is added at <tt>level</tt>.

val to_string : fixedpoint -> string

Retrieve internal string representation of fixedpoint object.

val set_predicate_representation : fixedpoint ->
       FuncDecl.func_decl -> Symbol.symbol list -> unit

Instrument the Datalog engine on which table representation to use for recursive predicate.

val to_string_q : fixedpoint -> Expr.expr list -> string

Convert benchmark given as set of axioms, rules and queries to a string.

val get_rules : fixedpoint -> Expr.expr list

Retrieve set of rules added to fixedpoint context.

val get_assertions : fixedpoint -> Expr.expr list

Retrieve set of assertions added to fixedpoint context.

val mk_fixedpoint : context -> fixedpoint

Create a Fixedpoint context.

val get_statistics : fixedpoint -> Statistics.statistics

Retrieve statistics information from the last call to #Z3_fixedpoint_query.

val parse_string : fixedpoint -> string -> Expr.expr list

Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the string.

val parse_file : fixedpoint -> string -> Expr.expr list

Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file.