Fixedpoint (docs.findlib-94.z3.Z3.Fixedpoint)

type fixedpoint

val get_help : fixedpoint -> string

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

val get_param_descrs : fixedpoint -> Params.ParamDescrs.param_descrs

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

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

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

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

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

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

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

val get_answer : fixedpoint -> Expr.expr option

val get_reason_unknown : fixedpoint -> string

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

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

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

val to_string : fixedpoint -> string

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

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

val get_rules : fixedpoint -> Expr.expr list

val get_assertions : fixedpoint -> Expr.expr list

val mk_fixedpoint : context -> fixedpoint

val get_statistics : fixedpoint -> Statistics.statistics

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

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