Litp
Representation of a literal (a Boolean variable or its negation).
- Signature
(litp x) → bool
- Returns
- bool — Type (booleanp bool).
Think of a LITERAL as an abstract data type that can either
represent a Boolean variable or its negation. More concretely, you can think
of a literal as an structure with two fields:
- var, a variable, represented as a natural number, and
- neg, a bit that says whether the variable is negated or not,
represented as a bitp.
In the implementation, we use an efficient natural-number encoding rather
than some kind of cons structure: neg is the bottom bit of the literal,
and var is the remaining bits. (This trick exploits the representation of
identifiers as natural numbers.)
Definitions and Theorems
Function: litp
(defun litp (x)
(declare (xargs :guard t))
(let ((__function__ 'litp))
(declare (ignorable __function__))
(natp x)))
Theorem: booleanp-of-litp
(defthm booleanp-of-litp
(b* ((bool (litp x))) (booleanp bool))
:rule-classes :tau-system)
Theorem: litp-compound-recognizer
(defthm litp-compound-recognizer
(equal (litp x) (natp x))
:rule-classes :compound-recognizer)
Subtopics
- Lit-negate-cond
- Efficiently negate a literal.
- Lit-negate
- Efficiently negate a literal.
- Make-lit
- Construct a literal with the given var and neg.
- Lit-equiv
- Basic equivalence relation for literals.
- Lit->var
- Access the var component of a literal.
- Lit->neg
- Access the neg bit of a literal.
- Lit-list
- List of literals
- Maybe-litp
- Recognizer for lits and nil.
- Lit-fix
- Basic fixing function for literals.
- Lit-list-list
- List of lit-lists
