Module `Once.Term`Source

Sourcetype 'a t = 'a term constraint 'a = [< bv | rm | fp | ('b, 'c) ar ]

A term of 'a kind.

Sourcetype 'a variadic =

| [] : unit variadic
| :: : ([< bv | rm | fp ] as 'a) term * 'b variadic -> ('a -> 'b) variadic
(*
Functions accept only bit-vector, rounding-mode or floating-point as argument
*)

Statically typed list of function argument terms.

Constructor

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 : '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 : '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 -> '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 : 'a t -> int

hash t compute the hash value for a term.

parameter t
The term.

returns
The hash value of the term.

Sourceval sort : '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.

View

Sourcetype 'a view =

| Value : 'a value -> 'a view
| Const : 'a sort * string -> 'a view
| Var : ([< bv | rm | fp ] as 'a) sort -> 'a view
| Lambda : 'a variadic * 'b term -> ('a, 'b) fn view
| Equal : ([< bv | rm | fp | ('b, 'c) ar ] as 'a) term * 'a term -> bv view
| Distinct : ([< bv | rm | fp | ('b, 'c) ar ] as 'a) term * 'a term -> bv view
| Ite : bv term * ([< bv | rm | fp | ('b, 'c) ar ] as 'a) term * 'a term -> 'a view
| Bv : ('a, 'b) Bv.operator * 'b -> bv view
| Fp : ('a, 'b, 'c) Fp.operator * 'b -> 'c view
| Select : ('a, 'b) ar term * 'a term -> 'b view
| Store : ('a, 'b) ar term * 'a term * 'b term -> ('a, 'b) ar view
| Apply : ('a, 'b) fn term * 'a variadic -> 'b 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.

package bitwuzla

Module Once.TermSource

Constructor

View

Module `Once.Term`Source