package encoding

You can search for identifiers within the package.

in-package search v0.2.0

Smt encoding library

Install

md5=dc6d0f89b7b3c38c78c2844a54c6386b

sha512=03b70558322ef654bc1a3ea3ff1c029b8aecd7ed35d98ad4b4089c00905ee6eade180d5a4f4470078217ae60830591528ff2ccdc861083c840a0c52606cb0220

Term definitions of the abstract syntax

Sourcetype t = {

}

Sourceand expr =

Sourceval v : expr -> Ty.t -> t

Sourceval (@:) : expr -> Ty.t -> t

Sourceval equal : t -> t -> bool

Sourceval hash : t -> int

Sourceval mk_symbol : Symbol.t -> t

Sourceval get_symbols : t list -> Symbol.t list

Sourceval negate_relop : t -> (t, string) Result.t

Sourceval pp : Format.formatter -> t -> unit

Sourceval pp_smt : Format.formatter -> t list -> unit

Sourceval pp_list : Format.formatter -> t list -> unit

Sourceval to_string : t -> string

Sourceval simplify : ?extract:bool -> t -> t

Sourcemodule Bitv : sig ... end