Aig2c-boolean-sanity-check-p
- Signature
(aig2c-boolean-sanity-check-p type op-and op-not) → *
- Arguments
- type — Guard (stringp type).
- op-and — Guard (stringp op-and).
- op-not — Guard (stringp op-not).
Definitions and Theorems
Function: aig2c-boolean-sanity-check-p
(defun aig2c-boolean-sanity-check-p (type op-and op-not)
(declare (xargs :guard (and (stringp type)
(stringp op-and)
(stringp op-not))))
(let ((__function__ 'aig2c-boolean-sanity-check-p))
(declare (ignorable __function__))
(b*
((tokens (str::strtok type '(#\Space #\Newline #\Tab)))
((unless (or (equal tokens '("bool"))
(equal tokens '("const" "bool"))))
t)
((unless (and (equal op-and "&&")
(equal op-not "!")))
(raise
"Insane AIG2C configuration. You are trying to make an aig2c ~
configuration using bool variables, but with operators other ~
than && and !. The bitwise operators won't work here. See ~
:xdoc aig2c-config-p for more information.")))
t)))
