package bitwuzla

  1. Overview
  2. Docs

Module Incremental.TermSource

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

A term of 'a kind.

Sourcetype !'a variadic =
  1. | [] : unit variadic
  2. | :: : ([< `Bv | `Fp | `Rm ] as 'c) term * 'b variadic -> ('c -> 'b) variadic
    (*

    Functions accept only bit-vector, rounding-mode or floating-point as argument

    *)

Statically typed list of function argument terms.

Sourcemodule Bl : sig ... end

Boolean

Sourcemodule Bv : sig ... end

Bit-vector

Sourcemodule Rm : sig ... end

Rounding-mode

Sourcemodule Fp : sig ... end

Floating-point

Sourcemodule Ar : sig ... end

Array

Sourcemodule Uf : sig ... end

Uninterpreted function

Sourceval 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.

Sourceval 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: =

Sourceval 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)

Sourceval 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

Sourceval 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.

Sourceval 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.

Sourceval pp : Format.formatter -> 'a term -> unit

pp formatter t pretty print term.

  • parameter formatter

    The outpout formatter

  • parameter t

    The term.

Sourcetype !'a5 view =
  1. | Value : 'a value -> 'a view
  2. | Const : 'a0 sort * string -> 'a0 view
  3. | Var : ([< `Bv | `Fp | `Rm ] as 'd) sort -> 'd view
  4. | Lambda : 'a1 variadic * ([< bv ] as 'e) term -> ('a1, 'e) fn view
  5. | Equal : ([< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ] as 'f) term * 'f term -> bv view
  6. | Distinct : ([< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ] as 'g) term * 'g term -> bv view
  7. | Ite : bv term * ([< `Ar of [< `Bv | `Fp | `Rm ] -> [< `Bv | `Fp | `Rm ] | `Bv | `Fp | `Rm ] as 'h) term * 'h term -> 'h view
  8. | Bv : ('a2, 'b) Bv.operator * 'b -> bv view
  9. | Fp : ('a3, 'b0, 'c) Fp.operator * 'b0 -> 'c view
  10. | Select : ([< `Bv | `Fp | `Rm ] as 'i, [< `Bv | `Fp | `Rm ] as 'j) ar term * 'i term -> 'j view
  11. | Store : ([< `Bv | `Fp | `Rm ] as 'k, [< `Bv | `Fp | `Rm ] as 'l) ar term * 'k term * 'l term -> ('k, 'l) ar view
  12. | Apply : ('a4, [< bv ] as 'm) fn term * 'a4 variadic -> 'm view

Algebraic view of formula terms.

Sourceval view : 'a term -> 'a view

view t destructurate a term.

  • parameter t

    The term.

  • returns

    The view of the term and its children.