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.

Inputs:

prop : Single AIG giving the invariant property to prove.constr : Single AIG giving the invariant constraint to assume.updates : Alist mapping each state variable to a single AIG representing its next-state function.initstp : Single AIG assumed to be true of any initial state.max-bvar : Natural number greater than all variables used in the AIGs.

Outputs:

result : one of the symbols:proved ,:refuted , or:failed , indicating the status of the check.ctrex-initst : when refuted, an alist mapping each state variable to its Boolean initial state in the counterexample.ctrex-ins : when refuted, a list of alists representing the frames of the counterexample, each alist mapping each non-state variable to a Boolean value.

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
to