Up – Package index » binsec » Library libsolver » Libsolver

Module `Libsolver`Source

binsec
- CHANGES
- LICENSE
- README
- Library binsec
  - Binsec
- Library binsec.amd64decoder
  - Amd64decoder
- Library binsec.armv7decoder
  - Armv7decoder
- Library binsec.armv8decoder
  - Armv8decoder
- Library binsec.domains
  - Domains
- Library binsec.parser
  - Libparser
- Library binsec.ppc64decoder
  - Ppc64decoder
- Library binsec.smt
  - Smt
- Library binsec.sparcv8decoder
  - Sparcv8decoder
- Library binsec.sse
  - Libsse
- Library binsec.sse_register
  - Sse
- Library checkct
  - Checkct
- Library libformula
  - Libformula
- Library libsolver
  - Libsolver
    - TERM
    - S
    - F
- Library libterm
  - Libterm
- Library shadow_stack
  - Shadow_stack
- Sources

Sourcetype status =

| Sat
| Unsat
| Unknown

Sourcemodule type TERM = sig ... end

Sourcemodule type S = sig ... end

An incremental solver instance.

Sourcemodule type F = functor () -> S

A solver instance factory.

type ('bl, 'bv, 'ax) t =
  (module S
  with type Ax.t = 'ax
   and type Bl.t = 'bl
   and type Bv.t = 'bv)

Sourceval bitwuzla_c : (module F) option

Factory for the legacy Bitwuzla solver.

Sourceval bitwuzla_cxx : (module F) option

Factory for the Bitwuzla solver.

Sourceval z3 : (module F) option

Factory for the Z3 solver.