Equality check that works around hard SAT/fraiging problems caused by writemasking, solving each case separately.
(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
The SAT checks use FGL SAT config objects produced by attachments to the
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))
(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)))
(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)))))))