Module `Bitwuzla.Once`Source

Create a new Bitwuzla session (check_sat can only be called once).

Parameters

Signature

Phantom type

Phantom types are annotations that allow the compiler to statically catch some sort mismatch errors. Size mismatch errors will still be caught at runtime.

Sourcetype bv = [

| `Bv

]

The bit-vector kind.

Sourcetype rm = [

| `Rm

]

The rounding-mode kind.

Sourcetype fp = [

| `Fp

]

The floating-point kind.

Sourcetype ('a, 'b) ar = [

| `Ar of 'a -> 'b

] constraint 'a = [< bv | rm | fp ] constraint 'b = [< bv | rm | fp ]

The array kind with 'a index and 'b element.

Both index and element should be of bit-vector, rounding-mode or floating-point kind

Sourcetype ('a, 'b) fn = [

| `Fn of 'a -> 'b

] constraint 'b = [< bv ]

The function kind taking 'a argument and returning 'b element.

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

Core types

Sourcetype 'a sort

A sort of 'a kind.

Sourcetype 'a term

A term of 'a kind.

Sourcetype 'a value = private 'a term

A value of 'a kind.

Values are subtype of terms and can be downcasted using :> operator.

Sourcemodule Sort : sig ... end

Sourcemodule Term : sig ... end

Formula

Sourceval assert' : ?name:string -> bv term -> unit

assert' ~name t assert that the condition t is true.

t must be a boolean term (bv term of size 1).

parameter name
The name of the assertion, if any.

parameter t
The formula term to assert.

Sourcetype result =

| Sat
(*
sat
*)
| Unsat
(*
unsat
*)
| Unknown
(*
unknown
*)

A satisfiability result.

Sourceval pp_result : Format.formatter -> result -> unit

pp formatter result pretty print result.

parameter formatter
The output formatter.

parameter result
The result to print.

Sourceval check_sat : ?interrupt:(('a -> int) * 'a) -> unit -> result

check_sat ~interrupt () check satisfiability of current input formula.

parameter interrupt
Stop the research and return Unknown if the callback function returns a positive value. Run into completion otherwise.

returns
Sat if the input formula is satisfiable and Unsat if it is unsatisfiable, and Unknown when neither satistifiability nor unsatisfiability was determined, for instance when it was terminated by timeout.

Sourceval timeout : float -> (?interrupt:((float -> int) * float) -> 'b) -> 'b

timeout t f configure the interruptible function f with a timeout of t seconds.

timeout can be used to limit the time spend on check_sat or check_sat_assuming. For instance, for a 1 second time credit, use:

(timeout 1. check_sat) ()
(timeout 1. check_sat_assuming) assumptions

parameter t
Timeout in second.

parameter f
The function to configure.

returns
An interruptible function configured to stop on timeout.

Sourceval get_value : 'a term -> 'a value

get_value t get a term representing the model value of a given term.

Requires that the last check_sat query returned Sat.

parameter t
The term to query a model value for.

returns
A term representing the model value of term t.

Sourceval unsafe_close : unit -> unit

unafe_close () close the session.

UNSAFE: call this ONLY to release the resources earlier if the session is about to be garbage collected.

package bitwuzla