Crate boolector

Modules

option

This module exposes options which can be set on a Btor instance.

Structs

Array

An Array in Boolector is really just a map from BVs to BVs.

BV

A bitvector object: that is, a single symbolic value, consisting of some number of symbolic bits.

BVSolution

A BVSolution represents a possible solution for one BV in a given model.

Btor

A Btor represents an instance of the Boolector solver. Each BV and Array is created in a particular Btor instance.

Enums

SolverResult