sig
  type fixedpoint
  val get_help : Z3.Fixedpoint.fixedpoint -> string
  val set_parameters : Z3.Fixedpoint.fixedpoint -> Z3.Params.params -> unit
  val get_param_descrs :
    Z3.Fixedpoint.fixedpoint -> Z3.Params.ParamDescrs.param_descrs
  val add : Z3.Fixedpoint.fixedpoint -> Z3.Expr.expr list -> unit
  val register_relation :
    Z3.Fixedpoint.fixedpoint -> Z3.FuncDecl.func_decl -> unit
  val add_rule :
    Z3.Fixedpoint.fixedpoint ->
    Z3.Expr.expr -> Z3.Symbol.symbol option -> unit
  val add_fact :
    Z3.Fixedpoint.fixedpoint -> Z3.FuncDecl.func_decl -> int list -> unit
  val query : Z3.Fixedpoint.fixedpoint -> Z3.Expr.expr -> Z3.Solver.status
  val query_r :
    Z3.Fixedpoint.fixedpoint ->
    Z3.FuncDecl.func_decl list -> Z3.Solver.status
  val update_rule :
    Z3.Fixedpoint.fixedpoint -> Z3.Expr.expr -> Z3.Symbol.symbol -> unit
  val get_answer : Z3.Fixedpoint.fixedpoint -> Z3.Expr.expr option
  val get_reason_unknown : Z3.Fixedpoint.fixedpoint -> string
  val get_num_levels :
    Z3.Fixedpoint.fixedpoint -> Z3.FuncDecl.func_decl -> int
  val get_cover_delta :
    Z3.Fixedpoint.fixedpoint ->
    int -> Z3.FuncDecl.func_decl -> Z3.Expr.expr option
  val add_cover :
    Z3.Fixedpoint.fixedpoint ->
    int -> Z3.FuncDecl.func_decl -> Z3.Expr.expr -> unit
  val to_string : Z3.Fixedpoint.fixedpoint -> string
  val set_predicate_representation :
    Z3.Fixedpoint.fixedpoint ->
    Z3.FuncDecl.func_decl -> Z3.Symbol.symbol list -> unit
  val to_string_q : Z3.Fixedpoint.fixedpoint -> Z3.Expr.expr list -> string
  val get_rules : Z3.Fixedpoint.fixedpoint -> Z3.Expr.expr list
  val get_assertions : Z3.Fixedpoint.fixedpoint -> Z3.Expr.expr list
  val mk_fixedpoint : Z3.context -> Z3.Fixedpoint.fixedpoint
  val get_statistics : Z3.Fixedpoint.fixedpoint -> Z3.Statistics.statistics
  val parse_string : Z3.Fixedpoint.fixedpoint -> string -> Z3.Expr.expr list
  val parse_file : Z3.Fixedpoint.fixedpoint -> string -> Z3.Expr.expr list
end