		Search-engine friendly clone of the ACL2 documentation.

Representation-of-integer-operations

Sint-from-boolean

Turn an ACL2 boolean into an int value 0 or 1.

Signature
(sint-from-boolean b) → x
Arguments: b — Guard (booleanp b).
Returns: x — Type (sintp x).

This is essentially (but not exactly) the inverse of boolean-from-sint. Together with boolean-from-sint and other boolean-from-... operations, it can be used to represent in ACL2 shallowly embedded C logical conjunctions and disjunctions, which must be integers in C, but must be booleans in ACL2 to represent their non-strictness.

Definitions and Theorems

Function: sint-from-boolean

(defun sint-from-boolean (b)
       (declare (xargs :guard (booleanp b)))
       (if b (sint-from-integer 1)
           (sint-from-integer 0)))

Theorem: sintp-of-sint-from-boolean

(defthm sintp-of-sint-from-boolean
        (b* ((x (sint-from-boolean b)))
            (sintp x))
        :rule-classes :rewrite)

Theorem: sint-from-boolean-of-bool-fix-b

(defthm sint-from-boolean-of-bool-fix-b
        (equal (sint-from-boolean (acl2::bool-fix b))
               (sint-from-boolean b)))

Theorem: sint-from-boolean-iff-congruence-on-b

(defthm sint-from-boolean-iff-congruence-on-b
        (implies (iff b b-equiv)
                 (equal (sint-from-boolean b)
                        (sint-from-boolean b-equiv)))
        :rule-classes :congruence)