package bitwuzla

  1. Overview
  2. Docs
SMT solver for AUFBVFP

Install 

dune-project
 Dependency

bitwuzla.github.io Readme Changelog MIT License Edit opam file Versions (7)

Authors

  1. F
    Frédéric Recoules

Maintainers

  1. F
    Frédéric Recoules <frederic.recoules@cea.fr>

Sources

bitwuzla-1.0.5.tbz
sha256=bf329089e4fbf78e5d4caff349227a0b98a75d2f174931c9429ae8c5949c6a6c
sha512=bcd5fa342fba50c28290e87f4754d63975da148d466af65fc0d6305840d5202d37e7dd7ba231887b41e48ec76039d16c9c9fa7ce6190fdbb6fe3eb4aa5d54bfd

doc/bitwuzla/Bitwuzla/Unsat_core/index.html

Module Bitwuzla.Unsat_coreSource

Create a new Bitwuzla session in incremental mode while enabling unsatifiable core generation.

Parameters

Signature

include sig ... end
Sourcetype bv = [
  1. | `Bv
]

The bit-vector kind.

Sourcetype rm = [
  1. | `Rm
]

The rounding-mode kind.

Sourcetype fp = [
  1. | `Fp
]

The floating-point kind.

Sourcetype (!'a, !'b) ar = [
  1. | `Ar of 'a -> 'b
] constraint 'a = [< `Bv | `Fp | `Rm ] constraint 'b = [< `Bv | `Fp | `Rm ]

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 = [
  1. | `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.

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
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 =
  1. | Sat
    (*

    sat

    *)
  2. | Unsat
    (*

    unsat

    *)
  3. | 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.

Sourceval push : int -> unit

push nlevels push context levels.

  • parameter nlevels

    The number of context levels to push.

Sourceval pop : int -> unit

pop nlevels pop context levels.

  • parameter nlevels

    The number of context levels to pop.

Sourceval check_sat_assuming : ?interrupt:(('a -> int) * 'a) -> ?names:string array -> bv term array -> result

check_sat_assuming ~interrupt ~names assumptions check satisfiability of current input formula, with the search for a solution guided by the given assumptions.

An input formula consists of assertions added via assert' combined with assumptions via Boolean and. Unsatifiable assumptions can be queried via get_unsat_assumptions.

  • parameter interrupt

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

  • parameter names

    The assumption names, if any.

  • parameter assumption

    The set of assumptions guiding the research of solutions.

  • 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 get_unsat_assumptions : unit -> bv term array

get_unsat_assumptions () get the set of unsat assumptions.

Unsat assumptions are assumptions that force an input formula to become unsatisfiable. Unsat assumptions handling in Bitwuzla is analogous to failed assumptions in MiniSAT.

Requires that the last check_sat query returned Unsat.

  • returns

    An array with unsat assumptions.

Sourceval get_unsat_core : unit -> bv term array

get_unsat_core () get the set unsat core (unsat assertions).

The unsat core consists of the set of assertions that force an input formula to become unsatisfiable.

Requires that the last check_sat query returned Unsat.

  • returns

    An array with unsat assertions.