package bitwuzla-cxx

  1. Overview
  2. Docs

Solver

type t

The Bitwuzla solver.

val configure_terminator : t -> (unit -> bool) option -> unit

configure_terminator t f configure a termination callback function.

If terminator has been connected, Bitwuzla calls this function periodically to determine if the connected instance should be terminated.

  • parameter t

    The Bitwuzla instance.

  • parameter f

    The callback function, returns true if t should be terminated.

val create : Options.t -> t

create options create a new Bitwuzla instance.

The returned instance can be deleted earlier via unsafe_delete.

  • parameter options

    The associated options instance. Options must be configured at this point.

  • returns

    The created Bitwuzla instance.

Formula

val push : t -> int -> unit

push t nlevels push context levels.

  • parameter t

    The Bitwuzla instance.

  • parameter nlevels

    The number of context levels to push.

val pop : t -> int -> unit

pop t nlevels pop context levels.

  • parameter t

    The Bitwuzla instance.

  • parameter nlevels

    The number of context levels to pop.

val assert_formula : t -> Term.t -> unit

mk_assert t term assert formula.

  • parameter t

    The Bitwuzla instance.

  • parameter term

    The formula to assert.

val get_assertions : t -> Term.t array

get_assertions t get the set of currently asserted formulas.

  • returns

    The assertion formulas.

val pp_formula : Format.formatter -> t -> unit

pp_formula formatter t print the current input formula.

  • parameter formatter

    The output formatter.

  • parameter t

    The Bitwuzla instance.

Check

val simplify : t -> unit

simplify t simplify the current input formula.

  • parameter t

    The Bitwuzla instance.

val check_sat : ?assumptions:Term.t array -> t -> Result.t

check_sat ~assumptions t check satisfiability of current input formula.

An input formula consists of assertions added via assert_formula. The search for a solution can by guided by making assumptions via assumptions.

Assertions and assumptions are combined via Boolean and.

  • parameter t

    The Bitwuzla instance.

  • returns

    Sat if the input formula is satisfiable and Unsat if it is unsatisfiable, and Unknown when neither satisfiability nor unsatisfiability was determined. This can happen when t was terminated via a termination callback.

Sat

val get_value : t -> Term.t -> Term.t

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

Requires that the last check_sat query returned Sat.

  • parameter t

    The Bitwuzla instance.

  • parameter term

    The term to query a model value for.

  • returns

    A term representing the model value of term term.

Unsat

val is_unsat_assumption : t -> Term.t -> bool

is_unsat_assumption t term determine if an assumption is an unsat assumption.

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 unsat assumption generation has been enabled via Options.set.

Requires that the last check_sat query returned Unsat.

  • parameter t

    The Bitwuzla instance.

  • parameter term

    The assumption to check for.

  • returns

    true if given assumption is an unsat assumption.

val get_unsat_assumptions : t -> Term.t array

get_unsat_assumptions t 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 unsat assumption generation has been enabled via Options.set.

Requires that the last check_sat query returned Unsat.

  • parameter t

    The Bitwuzla instance.

  • returns

    An array with unsat assumptions.

val get_unsat_core : t -> Term.t array

get_unsat_core t 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 unsat core generation has been enabled via Options.set.

Requires that the last check_sat query returned Unsat.

  • parameter t

    The Bitwuzla instance.

  • returns

    An array with unsat assertions.

val unsafe_delete : t -> unit

Expert

delete t delete a Bitwuzla instance.

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

  • parameter t

    The Bitwuzla instance to delete.

val pp_statistics : Format.formatter -> t -> unit
OCaml

Innovation. Community. Security.