module Expr:sig
..end
type
expr =
| |
Expr of |
val ast_of_expr : expr -> AST.ast
val expr_of_ast : AST.ast -> expr
val simplify : expr -> Params.params option -> expr
Expr.get_simplify_help
val get_simplify_help : context -> string
Expr.Simplify
.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
from[i]
in the expression with to[i]
, for i
smaller than num_exprs
.
The result is the new expression. The arrays from
and to
must have size num_exprs
.
For every i
smaller than num_exprs
, we must have that
sort of from[i]
must be equal to sort of to[i]
.
val substitute_one : expr -> expr -> expr -> expr
val substitute_vars : expr -> expr list -> expr
For every i
smaller than num_exprs
, the variable with de-Bruijn index i
is replaced with term to[i]
.
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
MakeNumeral
since it is not necessary to parse a string.val equal : expr -> expr -> bool
val compare : expr -> expr -> int