package z3

  1. Overview
  2. Docs
type fixedpoint
val get_help : fixedpoint -> string
val set_parameters : fixedpoint -> Params.params -> unit
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 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
OCaml

Innovation. Community. Security.