Functor Syntax.MakeSimplifyingContext

module MakeSimplifyingContext: functor (* : sig
end) -> Context

Create a context which simplifies expressions on the fly

Parameters:

* : ()

type t

val context : t Syntax.context

type term = (t, Syntax.typ_arith) Syntax.expr

type formula = (t, Syntax.typ_bool) Syntax.expr

val mk_symbol : ?name:string -> Syntax.typ -> Syntax.symbol

val mk_const : Syntax.symbol -> (t, 'typ) Syntax.expr

val mk_app : Syntax.symbol ->
       (t, 'b) Syntax.expr list ->
       (t, 'typ) Syntax.expr

val mk_var : int -> Syntax.typ_fo -> (t, 'typ) Syntax.expr

val mk_add : term list -> term

val mk_mul : term list -> term

val mk_div : term -> term -> term

val mk_idiv : term -> term -> term

val mk_mod : term -> term -> term

val mk_real : QQ.t -> term

val mk_floor : term -> term

val mk_neg : term -> term

val mk_sub : term -> term -> term

val mk_forall : ?name:string ->
       Syntax.typ_fo -> formula -> formula

val mk_exists : ?name:string ->
       Syntax.typ_fo -> formula -> formula

val mk_forall_const : Syntax.symbol -> formula -> formula

val mk_exists_const : Syntax.symbol -> formula -> formula

val mk_and : formula list -> formula

val mk_or : formula list -> formula

val mk_not : formula -> formula

val mk_eq : term -> term -> formula

val mk_lt : term -> term -> formula

val mk_leq : term -> term -> formula

val mk_true : formula

val mk_false : formula

val mk_ite : formula ->
       (t, 'a) Syntax.expr ->
       (t, 'a) Syntax.expr -> (t, 'a) Syntax.expr