Module Sym
module Sym: sig end
Function symbols for the theory of S-expressions.
type arith =
type pair =
| |
Cons |
| |
Car |
| |
Cdr |
(* | Function symbols for the theory of S-expressions. | *) |
type coproduct =
| |
InL |
| |
InR |
| |
OutL |
| |
OutR |
type bv =
| |
Const of Bitv.t |
| |
Conc of int * int |
| |
Sub of int * int * int |
| |
Bitwise of int |
type pprod =
type apply =
| |
Apply of Dom.t option |
| |
Abs |
type arrays =
| |
Create |
| |
Select |
| |
Update |
type bvarith =
type t =
val cmp : 'a -> 'a -> int
val hash : t -> int
val eq : t -> t -> bool
val eq_interp : bvarith -> bvarith -> bool
val eq_bv : bv -> bv -> bool
val eq_pair : pair -> pair -> bool
val eq_apply : apply -> apply -> bool
val eq_arith : arith -> arith -> bool
val eq_arrays : arrays -> arrays -> bool
val eq_pp : pprod -> pprod -> bool
val pp : Format.formatter -> t -> unit
| Parameters: |
|
fmt |
: |
Format.formatter
|
|
s |
: |
t
|
|
val width : t -> int option
Width of bitvector function symbols.
val width_bv : bv -> int
val add : t