Module Binsec_smtlib.SolverSource

Sourcetype status = Binsec_smtlib_bindings.status =
  1. | Sat
  2. | Unsat
  3. | Unknown
include module type of struct include Solver end
module Command : sig ... end
type t =
  1. | Boolector
  2. | Bitwuzla
  3. | Z3
  4. | CVC4
  5. | Yices
val pp : Format.formatter -> t -> unit
val is_boolector : t -> bool
val is_yices : t -> bool
val ping : t -> bool

ping solver return true if the command was found in the path.

val name_of : t -> string

Accessors

val command : ?incremental:bool -> ?options:string -> int -> t -> Command.t
val timeout_s : int -> t -> int
module Session : sig ... end
Sourcetype backend =
  1. | None : backend
  2. | Text : {
    1. session : (module Session.S with type arg = 'a);
    2. arg : 'a;
    } -> backend
  3. | Binding : {
    1. factory : (module Bindings.OPEN);
    2. complete_fold_ax_values : bool;
      (*

      complete_fold_ax_values is true if there is an explicit value for each accessed address, false when there can exist a missed default value.

      *)
    } -> backend
Sourceval default_backend : unit -> backend