Expand description
This module contains the core data-structures for representing logical formulae, as well as auxiliary data-structures that describe how formulae behave (i.e. variable orderings and decompositions)
(i.e., conjunctive normal forms, arbitrary logical formulae, etc.)
Structs§
- Assignment
Iter - BddNode
- Core BDD node storage
- BinarySDD
- Specialized SDD node for a right-linear sub-vtree SDDs for these fragments are binary decisions
- Cnf
- CnfHasher
- Probabilistically hashes a partially instantiated CNF, used primarily for component caching during bottom-up compilation (a component is a partially instantiated CNF).
- Fold
- Folds in the style of foldl on
hackage.
This performs specialized folds over
FoldNoderepresentations. With a (currently non-existent) composition, one can perform multiple folds in a single walk of the BDD. - Fold
Node - The intermediate representation for a BddPtr that is being folded in a
Foldcomputation. - HashedCNF
- Literal
- Literal, a variable label and its corresponding truth assignment
- Partial
Model - SATSolver
- SddAnd
- SddNode
Iter - Produces a node iterator for SDD or-nodes from an SDD pointer
- SddOr
- An SddOr node is a vector of (prime, sub) pairs.
- Unit
Propagate - A data-structure for efficient implementation of unit propagation with CNFs. It implements a two-literal watching scheme. For instance, for the CNF: c0 c1 (A / !B) /\ (C / !A / B) ^ ^ ^ ^ The literals A and !B are watched in c0, and C and !A are watched in c1 This is stored in the watch lists as: watch_list_pos: A: [ c0 ] B: [ ] C: [ c1 ] watch_list_neg: A: [ c1 ] B: [ c0 ] C: [ ]
- VTree
Index - A vtree index uniquely identifies a node in a vtree via a left-first depth-first traversal. For example, each node in vtree is given the following indexing structure: 6 2 5 0 1 3 4
- VTree
Manager - Handles VTree related operations
- VarLabel
- a label for each distinct variable in the BDD
- VarOrder
- VarSet
- A structure that contains sets of variables
- WmcParams
- Weighted model counting parameters for a BDD. It primarily is a storage for the weight on each variable.
Enums§
- BddPtr
- Core BDD pointer datatype
- DDNNF
- A base d-DNNF type
- DTree
- Decision
Result - Logical
Expr - SddPtr
Traits§
- DDNNF
Ptr - Partial
Variable Order - Structs that implement this trait expose an optional VarLabel with each item. These are then used for sorting and other ordering operations; None (typically reserved for constants) is considered to be “greater than” other objects (i.e. comes last), and no guaranteed ordering exists between None objects.
Functions§
- create_
semantic_ hash_ map - creates a weighting that can be used for semantically hashing a DDNNF node
the constant
Pdenotes the size of the field over which the semantic hash will be computed. For more info, see https://tr.inf.unibe.ch/pdf/iam-06-001.pdf