Generate a C expression from an ACL2 term that must be an expression term returning a boolean.
(atc-gen-expr-bool term gin state) → (mv erp gout)
At the same time, we check that the term is an expression term returning a boolean, as described in the user documentation. Based on its form, we dispatch to different code, after recursively processing sub-expressions.
As in atc-gen-expr-pure, we perform C type checks on the ACL2 terms. See atc-gen-expr-pure for an explanation.