Modules
This module exposes options which can be set on a Btor
instance.
Structs
An Array
in Boolector is really just a map from BV
s to BV
s.
A bitvector object: that is, a single symbolic value, consisting of some number of symbolic bits.
A BVSolution
represents a possible solution for one BV
in a given model.
A Btor
represents an instance of the Boolector solver.
Each BV
and Array
is created in a particular Btor
instance.