Bool package:what4
Declares a datatype for representing n-way conjunctions or
disjunctions in a way that efficiently captures important algebraic
laws like commutativity, associativity and resolution.
A representation of a conjunction or a disjunction.
This data structure keeps track of a collection of expressions
together with their polarities. The implementation uses a map from
expression values to their polarities, and thus automatically
implements the associative, commutative and idempotency laws common to
both conjunctions and disjunctions. Moreover, if the same expression
occurs in the collection with opposite polarities, the entire
collection collapses via a resolution step to an "inconsistent" map.
For conjunctions this corresponds to a contradiction and represents
false; for disjunction, this corresponds to the law of the excluded
middle and represents true.
The annotation on the
AnnotatedMap is an incremental hash
(
IncrHash) of the map, used to support a fast
Hashable
instance.
An inconsistent bool map, represents the dual of the operation unit
The terms appearing in the bool map, of which there is at least one
A bool map with no expressions, represents the unit of the
corresponding operation
Represents the state of a
BoolMap (either a conjunction or
disjunction).
If you know you are dealing with a
BoolMap that represents a
conjunction, consider using
ConjMap and
viewConjMap for
the sake of clarity.
This module provides an interface for running Boolector and parsing
the results back.
Standard option style for boolean-valued configuration options