Attachable interface for glmc's model-checking backend
Bfr-mcheck operates on hons-AIGs (see aig) whose input variables are natural numbers. This is potentially important because it provides an easy way for a backend to generate new variables that are known to be unused. Some of the variables represent primary inputs and some represent states; the state variables are simply those that are bound in the next-state alist. Below, when we refer to a "single AIG", this means a single hons-AIG object, which represents a single-output Boolean function.
The constraint assumed of
(b* (((mv result ?ctrex-initst ?ctrex-ins) (bfr-mcheck prop constr updates initstp max-bvar))) (implies (and (equal result :proved) (bfr-eval initstp (bfr-env-override (bfr-updates->states updates) init-st (car ins))) (pbfr-vars-bounded max-bvar t prop) (pbfr-vars-bounded max-bvar t constr) (pbfr-vars-bounded max-bvar t initstp) (pbfr-list-vars-bounded max-bvar t (alist-vals (bfr-updates-fix updates))) ;; (subsetp (bfr-vars initstp) (bfr-updates->states updates)) (bfr-varlist-bounded max-bvar (bfr-updates->states updates))) (bfr-constrained-mcrun prop constr updates init-st ins)))
This basically says:
See bfr-mcheck-abc-simple for an example backend that may be attached