bitwuzla 1.0.3 · OCaml Package

type 'b t = 'a term
  constraint
    'b =
    [< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ]

A term of 'a kind.

type !'a variadic =

| [] : unit variadic
| :: : [< `Bv | `Fp | `Rm ] as 'c term * 'b variadic -> ('d -> 'b0) variadic
(*
Functions accept only bit-vector, rounding-mode or floating-point as argument
*)

Statically typed list of function argument terms.

module Bl : sig ... end

Boolean

module Bv : sig ... end

Bit-vector

module Rm : sig ... end

Rounding-mode

module Fp : sig ... end

Floating-point

module Ar : sig ... end

Array

module Uf : sig ... end

Uninterpreted function

val const : 'a sort -> string -> 'a term

const sort symbol create a (first-order) constant of given sort with given symbol.

This creates a 0-arity function symbol.

parameter sort
The sort of the constant.

parameter symbol
The symbol of the constant.

returns
A term representing the constant.

val equal : 
  [< `Ar of
       [< `Bv | `Fp | `Rm ] ->
       [< `Bv | `Fp | `Rm ] & [< `Bv | `Fp | `Rm ] ->
       [< `Bv | `Fp | `Rm ]
  | `Bv
  | `Fp
  | `Rm ] as 'a
    t ->
  'a t ->
  bv t

equal t0 t1 create an equality term.

parameter t0
The first term.

parameter t1
The second term.

returns
SMT-LIB: =

val distinct : 
  [< `Ar of
       [< `Bv | `Fp | `Rm ] ->
       [< `Bv | `Fp | `Rm ] & [< `Bv | `Fp | `Rm ] ->
       [< `Bv | `Fp | `Rm ]
  | `Bv
  | `Fp
  | `Rm ] as 'a
    t ->
  'a t ->
  bv t

distinct t0 t1 create an disequality term.

parameter t0
The first term.

parameter t1
The second term.

returns
SMT-LIB: not (= t0 t1)

val ite : 
  bv t ->
  [< `Ar of
       [< `Bv | `Fp | `Rm ] ->
       [< `Bv | `Fp | `Rm ] & [< `Bv | `Fp | `Rm ] ->
       [< `Bv | `Fp | `Rm ] & [< `Bv | `Fp | `Rm ] ->
       [< `Bv | `Fp | `Rm ]
  | `Bv
  | `Fp
  | `Rm ] as 'a
    t ->
  'a t ->
  'a t

ite t0 t1 t2 create an if-then-else term.

parameter t0
The condition term.

parameter t1
The then term.

parameter t2
The else term.

returns
SMT-LIB: ite

val hash : 
  [< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ] t ->
  int

hash t compute the hash value for a term.

parameter t
The term.

returns
The hash value of the term.

val sort : 
  [< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ] as 'a
    t ->
  'a sort

sort t get the sort of a term.

parameter t
The term.

returns
The sort of the term.

val pp : Stdlib.Format.formatter -> 'a term -> unit

pp formatter t pretty print term.

parameter formatter
The outpout formatter

parameter t
The term.

type !'a9 view =

| Value : 'a value -> 'a0 view
| Const : 'a1 sort * string -> 'a2 view
| Var : [< `Bv | `Fp | `Rm ] as 'd sort -> 'e view
| Lambda : 'a3 variadic * [< bv ] as 'f term -> ('a4, 'g) fn view
| Equal : [< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ] as 'h term * 'i term -> bv view
| Distinct : [< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ] as 'j term * 'k term -> bv view
| Ite : bv term * [< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ] as 'l term * 'm term -> 'n view
| Bv : ('a5, 'b) Bv.operator * 'b0 -> bv view
| Fp : ('a6, 'b1, 'c) Fp.operator * 'b2 -> 'c0 view
| Select : ([< `Bv | `Fp | `Rm ] as 'o, [< `Bv | `Fp | `Rm ] as 'p) ar term * 'q term -> 'r view
| Store : ([< `Bv | `Fp | `Rm ] as 's, [< `Bv | `Fp | `Rm ] as 't) ar term * 'u term * 'v term -> ('w, 'x) ar view
| Apply : ('a7, [< bv ] as 'y) fn term * 'a8 variadic -> 'z view

Algebraic view of formula terms.

val view : 'a term -> 'a view

view t destructurate a term.

parameter t
The term.

returns
The view of the term and its children.

package bitwuzla