		Search-engine friendly clone of the ACL2 documentation.

Advanced-equivalence-checking-with-fgl

Solve-lane-by-lane-masked+

Equality check that works around hard SAT/fraiging problems caused by writemasking, solving each case separately.

Signature
(solve-lane-by-lane-masked+ x y mask width) → *

See solve-lane-by-lane-masked for a general discussion of the problem this addresses.

The approach of this function differs from that of solve-lane-by-lane-masked in that instead of using fgl-pathcond-fix to try to fold in the mask conditions, this function solves each case as a separate SAT problem. The AIGNET observability transform is often useful in order to make the mask conditions yield comparable internal nodes.

The SAT checks use FGL SAT config objects produced by attachments to the 0-ary functions solve-lane-by-lane-masked+-config0 and solve-lane-by-lane-masked+-config1, which respectively determine how to check when the mask bit is assumed to be 0 and when the mask bit is assumed 1. Default attachments assume that we want to use incremental SAT for the (typically easy) mask 0 case and monolithic SAT, possibly with AIG simplification transforms, for the (typically harder) mask 1 case.

Recommended transformations for the mask 1 case can be set up like this:

(local (include-book "centaur/ipasir/ipasir-backend" :dir :system))
(local (include-book "centaur/aignet/transforms" :dir :system))
(local (defun transforms-config ()
         (declare (Xargs :guard t))
         #!aignet
         (list (make-observability-config)
               (make-balance-config :search-higher-levels t
                                    :search-second-lit t)
               (change-fraig-config *fraig-default-config*
                                    :random-seed-name 'my-random-seed
                                    :ctrex-queue-limit 32
                                    :sim-words 1
                                    :ctrex-force-resim nil
                                    :ipasir-limit 1)

               (change-fraig-config *fraig-default-config*
                                    :random-seed-name 'my-random-seed2
                                    :ctrex-queue-limit 32
                                    :ipasir-limit 25))))
(local (defattach fgl-aignet-transforms-config transforms-config))

Definitions and Theorems

Function: solve-lane-by-lane-masked+

(defun solve-lane-by-lane-masked+
       (x y mask width)
       (declare (xargs :guard t))
       (let ((__function__ 'solve-lane-by-lane-masked+))
            (declare (ignorable __function__))
            (equal x y)))

Theorem: solve-lane-by-lane-masked+-impl

(defthm
 solve-lane-by-lane-masked+-impl
 (implies
  (and (syntaxp (posp width))
       (integerp x)
       (integerp y))
  (equal
   (solve-lane-by-lane-masked+ x y mask width)
   (if
    (and (check-int-endp x-endp x)
         (check-int-endp y-endp y))
    (equal x y)
    (b*
     ((config0
           (syntax-bind
                config0
                (g-concrete (solve-lane-by-lane-masked+-config0))))
      (config1
           (syntax-bind
                config1
                (g-concrete (solve-lane-by-lane-masked+-config1)))))
     (and* (fgl-validity-check config1
                               (implies (logbitp 0 mask)
                                        (equal (loghead width x)
                                               (loghead width y))))
           (fgl-validity-check config0
                               (implies (not (logbitp 0 mask))
                                        (equal (loghead width x)
                                               (loghead width y))))
           (solve-lane-by-lane-masked+ (logtail width x)
                                       (logtail width y)
                                       (logcdr mask)
                                       width)))))))