package z3

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

type expr

val ast_of_expr : expr -> AST.ast

val expr_of_ast : AST.ast -> expr

val simplify : expr -> Params.params option -> expr

val get_simplify_help : context -> string

val get_simplify_parameter_descrs : context -> Params.ParamDescrs.param_descrs

val get_func_decl : expr -> FuncDecl.func_decl

val get_num_args : expr -> int

val get_args : expr -> expr list

val update : expr -> expr list -> expr

val substitute : expr -> expr list -> expr list -> expr

val substitute_one : expr -> expr -> expr -> expr

val substitute_vars : expr -> expr list -> expr

val translate : expr -> context -> expr

val to_string : expr -> string

val is_numeral : expr -> bool

val is_well_sorted : expr -> bool

val get_sort : expr -> Sort.sort

val is_const : expr -> bool

val mk_const : context -> Symbol.symbol -> Sort.sort -> expr

val mk_const_s : context -> string -> Sort.sort -> expr

val mk_const_f : context -> FuncDecl.func_decl -> expr

val mk_fresh_const : context -> string -> Sort.sort -> expr

val mk_app : context -> FuncDecl.func_decl -> expr list -> expr

val mk_numeral_string : context -> string -> Sort.sort -> expr

val mk_numeral_int : context -> int -> Sort.sort -> expr

val equal : expr -> expr -> bool

val compare : expr -> expr -> int