Filtering...

fixers2

books/acl2s/cgen/fixers2
other
(in-package "CGEN")
other
(include-book "utilities")
other
(include-book "misc/bash" :dir :system)
other
(include-book "data-structures/utilities" :dir :system)
other
(include-book "cgen-state")
other
(program)
other
(set-state-ok t)
s+macro
(defmacro s+
  (&rest args)
  "string/symbol(s) concat to return a symbol.
  :pkg and :separator keyword args recognized."
  `(s+ ,@CGEN::ARGS :pkg "CGEN"))
g1macro
(defmacro g1
  (a x)
  `(get1 ,CGEN::A ,CGEN::X))
collect-varsfunction
(defun collect-vars
  (term)
  (reverse (all-vars term)))
other
(defloop collect-vars-lst
  (terms)
  (for ((term in terms))
    (append (collect-vars term))))
assoc-equal-lstfunction
(defun assoc-equal-lst
  (keys alist)
  "give back the subset of the alist that correspond to these keys. the order
of the entries is same as of the alist"
  (declare (xargs :guard (and (true-listp keys)
        (alistp alist))))
  (if (endp alist)
    nil
    (b* (((cons k &) (car alist)))
      (if (member-equal k keys)
        (cons (car alist)
          (assoc-equal-lst keys (cdr alist)))
        (assoc-equal-lst keys (cdr alist))))))
to-stringfunction
(defun to-string
  (x)
  (declare (xargs :mode :program))
  (coerce (cdr (coerce (fms-to-string "~x0" (list (cons #\0 x)))
        'list))
    'string))
term-namefunction
(defun term-name
  (term)
  (declare (xargs :mode :program))
  (fix-intern-in-pkg-of-sym (to-string term)
    'x))
flatten-output-ftermfunction
(defun flatten-output-fterm
  (x term output-vars)
  (cond ((proper-symbolp term) nil)
    ((quotep term) nil)
    ((atom term) nil)
    (t (and (member-eq x output-vars)
        (list (cons (term-name term) term))))))
other
(defloop flatten-output-fterms
  (sigma output-vars)
  (for ((pair in sigma))
    (append (flatten-output-fterm (car pair)
        (cdr pair)
        output-vars))))
other
(defloop invert-alist
  (alist)
  (declare (xargs :guard (alistp alist)))
  (for ((x.y in alist))
    (collect (cons (cdr x.y) (car x.y)))))
equalitizefunction
(defun equalitize
  (cons-pair)
  `(equal ,(CAR CGEN::CONS-PAIR) ,(CDR CGEN::CONS-PAIR)))
other
(defloop equalitize-lst
  (alst)
  (for ((cons-pair in alst))
    (collect (equalitize cons-pair))))
make-dummy-equality-frule-instancefunction
(defun make-dummy-equality-frule-instance
  (x equal-to-term)
  (b* ((out-vars (list x)) (in-vars (all-vars equal-to-term))
      (fixer-term equal-to-term)
      (constraint-term (list 'equal x equal-to-term))
      (nm (s+ "EQ-"
          (term-name fixer-term)
          "/"
          (to-string x)))
      (rule (list (cons :hyps 'nil)
          (cons :in in-vars)
          (cons :out out-vars)
          (cons :fixer-vars in-vars)
          (cons :fixer-term fixer-term)
          (cons :name nm)
          (cons :constraint-vars (union-eq out-vars in-vars))
          (cons :constraint-term constraint-term)
          (cons :fixer-let-binding `((,CGEN::X ,CGEN::EQUAL-TO-TERM)))
          (cons :fixes (list constraint-term
              `(equal ,CGEN::EQUAL-TO-TERM ,CGEN::X))))))
    (cons nm rule)))
other
(defloop make-dummy-equality-frule-instances
  (x-equal-to-term-lst)
  (for ((x-equal-to-term in x-equal-to-term-lst))
    (collect (make-dummy-equality-frule-instance (second x-equal-to-term)
        (third x-equal-to-term)))))
other
(defloop filter-terms-with-vars
  (terms vars)
  (for ((term in terms))
    (append (and (intersectp-eq (all-vars term) vars)
        (list term)))))
fixer-rule-instancefunction
(defun fixer-rule-instance
  (frule alist)
  (b* ((fixer-termi (sublis-expr alist
         (get1 :fixer-term frule))) (ini (collect-vars-lst (sublis-expr-lst alist (get1 :in frule))))
      (outi (sublis-expr-lst alist (get1 :out frule)))
      (fixer-varsi (union-eq ini outi))
      (fixer-let-binding (get1 :fixer-let-binding frule))
      (bvalues (strip-cadrs fixer-let-binding))
      (bvars (strip-cars fixer-let-binding))
      (bvaluesi (sublis-expr-lst alist bvalues))
      (bvarsi (sublis-expr-lst alist bvars))
      (fixer-let-bindingi (list-up-lists bvarsi bvaluesi))
      (hypsi (sublis-expr-lst alist (get1 :hyps frule)))
      (constraint-termi (sublis-expr alist
          (get1 :constraint-term frule)))
      (constraint-varsi (all-vars constraint-termi))
      (frulei frule)
      (frulei (put-assoc :fixer-term fixer-termi frulei))
      (frulei (put-assoc :in ini frulei))
      (frulei (put-assoc :out outi frulei))
      (frulei (put-assoc :fixer-vars fixer-varsi frulei))
      (frulei (put-assoc :fixer-let-binding fixer-let-bindingi
          frulei))
      (frulei (put-assoc :hyps hypsi frulei))
      (frulei (put-assoc :constraint-term constraint-termi
          frulei))
      (frulei (put-assoc :constraint-vars constraint-varsi
          frulei))
      (fname (s+ (term-name fixer-termi)
          "/"
          (to-string outi)))
      (frulei (put-assoc :name fname frulei))
      (frulei (put-assoc :fixes (list constraint-termi)
          frulei))
      (frulei (put-assoc :preserves (filter-terms-with-vars hypsi outi)
          frulei)))
    frulei))
update-dynamic-fixer-instance-alist/frulefunction
(defun update-dynamic-fixer-instance-alist/frule
  (frule1i |FXRI{}|)
  (b* ((ctx 'update-dynamic-fixer-instance-alist/frule) (nm (get1 :name frule1i))
      (existing-entry (assoc-equal nm |FXRI{}|))
      ((unless existing-entry) (put-assoc-equal nm frule1i |FXRI{}|))
      (fxri-data (cdr existing-entry))
      ((unless (and (equal (get1 :in fxri-data)
             (get1 :in frule1i))
           (equal (get1 :out fxri-data)
             (get1 :out frule1i))
           (equal (get1 :fixer-term fxri-data)
             (get1 :fixer-term frule1i))
           (equal (get1 :fixer-let-binding fxri-data)
             (get1 :fixer-let-binding frule1i)))) (er hard?
          ctx
          "~| Incompatible fixer rule instances have same key; cannot be merged! ~ 
existing: ~x0 new: ~x1~%"
          fxri-data
          frule1i))
      (hyps (union-equal (get1 :hyps fxri-data)
          (get1 :hyps frule1i)))
      (fixes (union-equal (get1 :fixes fxri-data)
          (get1 :fixes frule1i)))
      (fxri-data (put-assoc-equal :hyps hyps
          (put-assoc-equal :fixes fixes fxri-data))))
    (put-assoc-equal nm
      fxri-data
      |FXRI{}|)))
other
(defloop var-term-alistp
  (xs)
  (for ((x in xs))
    (always (and (proper-symbolp (car x))
        (pseudo-termp (cdr x))))))
dumb-unsolvable-equations-pfunction
(defun dumb-unsolvable-equations-p
  (equalities mod-vars)
  (declare (ignorable equalities mod-vars))
  nil)
bash-fnfunction
(defun bash-fn
  (query hints
    verbosep
    ctx
    state)
  (b* ((ohints (override-hints (w state))) ((er ?ign) (table-fn 'default-hints-table
          (list :override 'nil)
          state
          nil))
      ((mv erp res state) (bash-fn query
          hints
          verbosep
          ctx
          state))
      ((er ?ign) (table-fn 'default-hints-table
          (list :override (kwote ohints))
          state
          nil)))
    (mv erp res state)))
equation-pfunction
(defun equation-p
  (term)
  (and (consp term)
    (= (len term) 3)
    (equal (car term) 'equal)
    (or (variablep (second term))
      (variablep (third term)))))
valid-output-symbolsfunction
(defun valid-output-symbols
  (xs)
  (and (proper-symbol-listp xs)
    (no-duplicatesp xs)))
instantiate-fixer-rule/termfunction
(defun instantiate-fixer-rule/term
  (frule cterm
    all-terms
    allvars
    vl
    state
    |W{}|
    |FXRI{}|)
  (declare (xargs :guard (and (pseudo-termp cterm)
        (pseudo-term-listp all-terms)
        (proper-symbol-listp allvars)
        (var-term-alistp |W{}|)
        (alistp |FXRI{}|))))
  (b* ((ctx 'instantiate-fixer-rule/term) (cterm1 (sublis-expr (invert-alist |W{}|) cterm))
      ((mv yesp s-alist) (one-way-unify (get1 :constraint-term frule)
          cterm1))
      ((unless yesp) (value (list nil 'nil |W{}| |FXRI{}|)))
      (meta-precondition (get1 :meta-precondition frule))
      (letb (listlis (strip-cars s-alist)
          (kwote-lst (strip-cdrs s-alist))))
      ((mv erp okp) (if (equal meta-precondition 't)
          (mv nil t)
          (trans-my-ev-w `(let ,CGEN::LETB
              (declare (ignorable ,@(CGEN::STRIP-CARS CGEN::S-ALIST)))
              ,CGEN::META-PRECONDITION)
            ctx
            (w state)
            nil)))
      ((unless (and (not erp) okp)) (value (list nil 'nil |W{}| |FXRI{}|)))
      (|W1{}| (flatten-output-fterms s-alist
          (get1 :out frule)))
      (r-alist (pairlis$ (strip-cars s-alist)
          (sublis-expr-lst (invert-alist |W1{}|)
            (strip-cdrs s-alist))))
      ((unless (valid-output-symbols (sublis-expr-lst r-alist
             (get1 :out frule)))) (value (list nil 'nil |W{}| |FXRI{}|)))
      (frulei (fixer-rule-instance frule r-alist))
      (e (equalitize-lst (append |W1{}|
            (assoc-equal-lst (all-vars cterm1) |W{}|))))
      (unlikely-p (dumb-unsolvable-equations-p e
          (get1 :out frulei)))
      ((when unlikely-p) (prog2$ (cw? (verbose-flag vl)
            "~| Cgen/Note: ~x0 with fixed ~x1 is unlikely to be simultaneously satisfied!~%"
            e
            (get1 :out frulei))
          (value (list nil 'nil |W{}| |FXRI{}|))))
      (curr-vars (union-eq (strip-cars |W1{}|)
          (union-eq (strip-cars |W{}|) allvars)))
      (rule-hyps (filter-terms-with-vars (get1 :hyps frulei)
          curr-vars))
      (backchain-lits (set-difference-equal (get1 :hyps frulei)
          rule-hyps))
      (relieve-hyps-query `(implies (and ,@CGEN::ALL-TERMS ,@CGEN::E)
          (and . ,CGEN::RULE-HYPS)))
      (hints 'nil)
      ((mv erp res state) (bash-fn relieve-hyps-query
          hints
          (debug-flag vl)
          ctx
          state))
      ((unless (and (not erp) (eq res nil))) (prog2$ (cw? (verbose-flag vl)
            "~| Cgen/Note: Unable to relieve query ~x0! Skipping fixer rule ..~%"
            relieve-hyps-query)
          (value (list nil 'nil |W{}| |FXRI{}|))))
      (f-lits (cons (get1 :constraint-term frulei)
          (union-equal backchain-lits e)))
      (|W{}| (union-equal |W{}| |W1{}|))
      (|FXRI{}| (update-dynamic-fixer-instance-alist/frule frulei
          |FXRI{}|)))
    (value (list t f-lits |W{}| |FXRI{}|))))
instantiate-fixer-rules/termfunction
(defun instantiate-fixer-rules/term
  (frules cterm
    all-terms
    allvars
    vl
    state
    |FLITS{}|
    |W{}|
    |FXRI{}|)
  (declare (xargs :guard (and (pseudo-termp cterm)
        (pseudo-term-listp all-terms)
        (alistp |FLITS{}|)
        (var-term-alistp |W{}|)
        (alistp |FXRI{}|))))
  (b* (((when (endp frules)) (value (list |FLITS{}| |W{}| |FXRI{}|))) (frule (car frules))
      ((mv erp
         (list hitp flits |W{}| |FXRI{}|)
         state) (instantiate-fixer-rule/term frule
          cterm
          all-terms
          allvars
          vl
          state
          |W{}|
          |FXRI{}|))
      ((when (or erp (not hitp))) (instantiate-fixer-rules/term (cdr frules)
          cterm
          all-terms
          allvars
          vl
          state
          |FLITS{}|
          |W{}|
          |FXRI{}|))
      (fname hitp)
      (|FLITS{}| (put-assoc-equal fname
          flits
          |FLITS{}|)))
    (instantiate-fixer-rules/term (cdr frules)
      cterm
      all-terms
      allvars
      vl
      state
      |FLITS{}|
      |W{}|
      |FXRI{}|)))
instantiate-fixer-rules/termsfunction
(defun instantiate-fixer-rules/terms
  (cterms frules
    all-terms
    allvars
    vl
    state
    |TERM->FLITS{}|
    new-lits
    |W{}|
    |FXRI{}|)
  (b* (((when (endp cterms)) (value (list |TERM->FLITS{}|
           new-lits
           |W{}|
           |FXRI{}|))) (cterm (car cterms))
      ((mv erp
         (list |FLITS{}| |W{}| |FXRI{}|)
         state) (instantiate-fixer-rules/term frules
          cterm
          all-terms
          allvars
          vl
          state
          'nil
          |W{}|
          |FXRI{}|))
      ((when (or erp (null |FLITS{}|))) (prog2$ (cw? (verbose-stats-flag vl)
            "~| Cgen/Note: No applicable fixer-rule found for ~x0.~%"
            cterm)
          (instantiate-fixer-rules/terms (cdr cterms)
            frules
            all-terms
            allvars
            vl
            state
            (put-assoc-equal cterm nil |TERM->FLITS{}|)
            new-lits
            |W{}|
            |FXRI{}|)))
      (new-lits1 (set-difference-equal (union-lsts (strip-cdrs |FLITS{}|))
          all-terms))
      (new-lits (union-equal new-lits new-lits1))
      (|TERM->FLITS{}| (put-assoc-equal cterm
          |FLITS{}|
          |TERM->FLITS{}|)))
    (instantiate-fixer-rules/terms (cdr cterms)
      frules
      all-terms
      allvars
      vl
      state
      |TERM->FLITS{}|
      new-lits
      |W{}|
      |FXRI{}|)))
other
(include-book "infer-enum-shape")
other
(defloop access-cs%-alst
  (x-cs%-alst)
  (for ((x-cs% in x-cs%-alst))
    (collect (access cs% (cdr x-cs%) :defdata-type))))
make-type-and-eq-hypfunction
(defun make-type-and-eq-hyp
  (x defdata-type
    eq-constraint
    wrld)
  (b* ((p (predicate-name defdata-type)) ((when (eq eq-constraint 'empty-eq-constraint)) (list p x)))
    (list 'equal x eq-constraint)))
other
(defloop make-type-and-eq-hyps
  (v-cs%-alst wrld)
  (for ((v--cs% in v-cs%-alst))
    (collect (make-type-and-eq-hyp (car v--cs%)
        (access cs% (cdr v--cs%) :defdata-type)
        (access cs% (cdr v--cs%) :eq-constraint)
        wrld))))
make-dummy-defdata-type-frule-instancefunction
(defun make-dummy-defdata-type-frule-instance
  (x p wrld)
  (b* ((defdata-type (or (is-type-predicate p wrld)
         'all)) (e (enumerator-name defdata-type))
      (vars (list x))
      (fixer-term (list e))
      (constraint-term (cons p vars))
      (nm (s+ (term-name fixer-term)
          "/"
          (to-string x)))
      (rule (list (cons :hyps 'nil)
          (cons :in 'nil)
          (cons :out vars)
          (cons :fixer-vars vars)
          (cons :fixer-term fixer-term)
          (cons :name nm)
          (cons :constraint-vars vars)
          (cons :constraint-term constraint-term)
          (cons :fixer-let-binding `((,CGEN::X (,CGEN::E))))
          (cons :fixes (list constraint-term)))))
    (cons nm rule)))
destruct-equality-hypfunction
(defun destruct-equality-hyp
  (hyp)
  (case-match hyp
    (('equal x (f . args)) (list x (cons-term f args)))
    (('equal (f . args) x) (list x (cons-term f args)))
    (('equal x y) (list x y))))
make-dummy-cgen-builtin-fxri-entryfunction
(defun make-dummy-cgen-builtin-fxri-entry
  (type-hyp wrld)
  (if (equal (len type-hyp) 2)
    (make-dummy-defdata-type-frule-instance (cadr type-hyp)
      (car type-hyp)
      wrld)
    (b* (((list x equal-to-term) (destruct-equality-hyp type-hyp)))
      (make-dummy-equality-frule-instance x
        equal-to-term))))
other
(defloop make-dummy-cgen-builtin-frule-instances
  (type-hyps wrld)
  (for ((type-hyp in type-hyps))
    (collect (make-dummy-cgen-builtin-fxri-entry type-hyp
        wrld))))
other
(defloop two-level-flatten1
  (lits-lst-list)
  (for ((lits-lst in lits-lst-list))
    (append (union-lsts lits-lst))))
two-level-flattenfunction
(defun two-level-flatten
  (lits-lst-list)
  (remove-duplicates-equal (two-level-flatten1 lits-lst-list)))
other
(defloop singletonize
  (xs)
  (for ((x in xs))
    (collect (list x))))
other
(defloop make-allp-hyps
  (xs)
  (for ((x in xs))
    (collect (list 'allp x))))
is-type-hypfunction
(defun is-type-hyp
  (term wrld)
  (or (is-type-predicate (car term) wrld)
    (and (equal (len term) 3)
      (equal (car term) 'equal)
      (or (proper-symbolp (second term))
        (proper-symbolp (third term))))))
other
(defloop filter-type-hyps
  (terms wrld)
  (for ((term in terms))
    (append (and (consp term)
        (is-type-hyp term wrld)
        (list term)))))
other
(defloop make-dummy-term-flits-alist
  (terms fnames)
  (for ((term in terms) (fname in fnames))
    (collect (cons term (acons fname (list term) nil)))))
instantiate-fixer-rules/terms-iterfunction
(defun instantiate-fixer-rules/terms-iter
  (hyps frules
    vl
    state
    |TERM->FLITS{}|
    |W{}|
    all-hyps
    |FXRI{}|)
  (b* ((wrld (w state)) (type-hyps (filter-type-hyps hyps wrld))
      (type-vars (all-vars1-lst type-hyps 'nil))
      (notype-vars (set-difference-equal (all-vars1-lst hyps 'nil)
          type-vars))
      (allp-hyps (make-allp-hyps notype-vars))
      (type-hyps (append type-hyps allp-hyps))
      (|FXRI0{}| (make-dummy-cgen-builtin-frule-instances type-hyps
          wrld))
      (|TERM->FLITS0{}| (make-dummy-term-flits-alist type-hyps
          (strip-cars |FXRI0{}|)))
      (|TERM->FLITS{}| (union-equal |TERM->FLITS0{}| |TERM->FLITS{}|))
      (|FXRI{}| (union-equal |FXRI0{}| |FXRI{}|))
      (other-hyps (set-difference-equal hyps type-hyps))
      ((when (null other-hyps)) (value (list |TERM->FLITS{}|
            |W{}|
            all-hyps
            |FXRI{}|)))
      (- (cw? (debug-flag vl)
          "~| type-hyps: ~x0 and hyps: ~x1~%"
          type-hyps
          hyps))
      (allvars (all-vars1-lst all-hyps 'nil))
      ((mv ?erp
         (list |TERM->FLITS1{}|
           new-lits
           |W1{}|
           |FXRI1{}|)
         state) (instantiate-fixer-rules/terms other-hyps
          frules
          all-hyps
          allvars
          vl
          state
          'nil
          'nil
          'nil
          'nil))
      (|TERM->FLITS{}| (append |TERM->FLITS1{}| |TERM->FLITS{}|))
      (|W{}| (union-equal |W1{}| |W{}|))
      (|FXRI{}| (union-equal |FXRI1{}| |FXRI{}|))
      (all-hyps (union-equal new-lits all-hyps))
      ((when (null new-lits)) (value (list |TERM->FLITS{}|
            |W{}|
            all-hyps
            |FXRI{}|))))
    (instantiate-fixer-rules/terms-iter new-lits
      frules
      vl
      state
      |TERM->FLITS{}|
      |W{}|
      all-hyps
      |FXRI{}|)))
match-pat/termsfunction
(defun match-pat/terms
  (pat terms)
  (if (endp terms)
    'nil
    (b* (((mv yesp sigma) (one-way-unify pat (car terms))) ((unless yesp) (match-pat/terms pat (cdr terms))))
      (cons sigma
        (match-pat/terms pat (cdr terms))))))
match-pats/terms-alstfunction
(defun match-pats/terms-alst
  (pats terms ans)
  (if (endp pats)
    ans
    (match-pats/terms-alst (cdr pats)
      terms
      (cons (match-pat/terms (car pats) terms)
        ans))))
binary-merge-sigmafunction
(defun binary-merge-sigma
  (sigma1 sigma2)
  (if (endp sigma1)
    (mv nil sigma2)
    (b* (((cons x val) (car sigma1)) ((unless (equal (assoc-eq x sigma2)
             (car sigma1))) (mv t nil)))
      (binary-merge-sigma (cdr sigma1)
        (put-assoc-eq x val sigma2)))))
merge-sigmas1function
(defun merge-sigmas1
  (sigmas ans)
  (if (endp sigmas)
    (mv nil ans)
    (b* ((sigma (car sigmas)) ((mv erp ans) (binary-merge-sigma sigma ans))
        ((when erp) (mv t nil)))
      (merge-sigmas1 (cdr sigmas) ans))))
preservation-rule-instancefunction
(defun preservation-rule-instance
  (prule alist)
  (b* ((fixer-termsi (sublis-expr-lst alist
         (get1 :fixer-terms prule))) (outi (sublis-expr-lst alist (get1 :out prule)))
      (fixer-let-binding (get1 :fixer-let-binding prule))
      (bvalues (strip-cadrs fixer-let-binding))
      (bvars (strip-cars fixer-let-binding))
      (bvaluesi (sublis-expr-lst alist bvalues))
      (bvarsi (sublis-expr-lst alist bvars))
      (fixer-let-bindingi (list-up-lists bvarsi bvaluesi))
      (hypsi (sublis-expr-lst alist (get1 :hyps prule)))
      (constraint-termi (sublis-expr alist
          (get1 :constraint-term prule)))
      (constraint-varsi (all-vars constraint-termi))
      (prulei prule)
      (prulei (put-assoc :fixer-terms fixer-termsi
          prulei))
      (prulei (put-assoc :out outi prulei))
      (prulei (put-assoc :fixer-let-binding fixer-let-bindingi
          prulei))
      (prulei (put-assoc :hyps hypsi prulei))
      (prulei (put-assoc :constraint-term constraint-termi
          prulei))
      (prulei (put-assoc :constraint-vars constraint-varsi
          prulei))
      (prulei (put-assoc :preserves (list constraint-termi)
          prulei)))
    prulei))
find-fxri-rule1function
(defun find-fxri-rule1
  (fxr-term entry)
  (b* (((cons & rulei) entry))
    (and (or (equal fxr-term (get1 :fixer-term rulei))
        (member-equal fxr-term
          (strip-cadrs (get1 :fixer-let-binding rulei))))
      entry)))
other
(defloop find-fxri-rule
  (fxr-term |FXRI{}|)
  (for ((entry in |FXRI{}|))
    (thereis (find-fxri-rule1 fxr-term entry))))
update-dynamic-fixer-instance-alist/prule/fxr-termfunction
(defun update-dynamic-fixer-instance-alist/prule/fxr-term
  (fxr-term prulei vl |FXRI{}|)
  (b* ((ctx 'update-dynamic-fixer-instance-alist/prule/fxr-term) ((cons nm fxri-data) (find-fxri-rule fxr-term |FXRI{}|))
      ((unless fxri-data) (prog2$ (cw? (verbose-flag vl)
            "~| Cgen/Verbose: ~x0 not in fxri{}, skip prule update.~%"
            fxr-term
            ctx)
          |FXRI{}|))
      (preserves (union-equal (get1 :preserves fxri-data)
          (get1 :preserves prulei)))
      (prule-alist (put-assoc-equal (get1 :constraint-term prulei)
          prulei
          (get1 :prule-alist fxri-data)))
      (fxri-data (put-assoc-equal :preserves preserves
          (put-assoc-equal :prule-alist prule-alist
            fxri-data))))
    (put-assoc-equal nm
      fxri-data
      |FXRI{}|)))
update-dynamic-fixer-instance-alist/prule/fxr-termsfunction
(defun update-dynamic-fixer-instance-alist/prule/fxr-terms
  (fxr-terms prulei vl |FXRI{}|)
  (if (endp fxr-terms)
    |FXRI{}|
    (b* ((fxr-term (car fxr-terms)) (|FXRI{}| (update-dynamic-fixer-instance-alist/prule/fxr-term fxr-term
            prulei
            vl
            |FXRI{}|)))
      (update-dynamic-fixer-instance-alist/prule/fxr-terms (cdr fxr-terms)
        prulei
        vl
        |FXRI{}|))))
update-dynamic-fixer-instance-alist/prulefunction
(defun update-dynamic-fixer-instance-alist/prule
  (prulei vl |FXRI{}|)
  (update-dynamic-fixer-instance-alist/prule/fxr-terms (get1 :fixer-terms prulei)
    prulei
    vl
    |FXRI{}|))
instantiate-prule/multiple-substfunction
(defun instantiate-prule/multiple-subst
  (sigmas-lst partial-s
    prule
    all-terms
    vl
    ctx
    state
    |FXRI{}|)
  (b* (((when (endp sigmas-lst)) (value |FXRI{}|)) (sigmas (car sigmas-lst))
      ((mv erp s1) (merge-sigmas1 (cdr sigmas) (car sigmas)))
      ((when erp) (prog2$ (cw? (verbose-flag vl)
            "~| Cgen/Error: ~x0 cannot be merged into one substitution. ~ Skipping this preservation rule instance ..~%"
            sigmas)
          (value |FXRI{}|)))
      (s (append partial-s s1))
      ((unless (valid-output-symbols (sublis-expr-lst s (get1 :out prule)))) (value |FXRI{}|))
      (prulei (preservation-rule-instance prule s))
      (query `(implies (and ,@CGEN::ALL-TERMS)
          (and . ,(CGEN::GET1 :HYPS CGEN::PRULEI))))
      (hints 'nil)
      ((mv erp res state) (bash-fn query
          hints
          (debug-flag vl)
          ctx
          state))
      ((unless (and (not erp) (eq res nil))) (prog2$ (cw? (verbose-flag vl)
            "~| Cgen/Note: Unable to relieve query ~x0! Skipping preservation rule ..~%"
            query)
          (value |FXRI{}|)))
      (|FXRI{}| (update-dynamic-fixer-instance-alist/prule prulei
          vl
          |FXRI{}|)))
    (instantiate-prule/multiple-subst (cdr sigmas-lst)
      partial-s
      prule
      all-terms
      vl
      ctx
      state
      |FXRI{}|)))
other
(defloop singletonize
  (xs)
  (for ((x in xs))
    (collect (list x))))
other
(defloop cross-product/binary1
  (a a2)
  (for ((b in a2))
    (collect (list a b))))
other
(defloop cross-product/binary
  (a1 a2)
  (for ((a in a1))
    (append (cross-product/binary1 a a2))))
generate-all-tuplesfunction
(defun generate-all-tuples
  (a-list)
  "Given Lists A1,A2,...,An generate all n-tuples (a1,...,an) where ai in Ai"
  (if (endp a-list)
    'nil
    (if (endp (cdr a-list))
      (singletonize (car a-list))
      (if (endp (cddr a-list))
        (cross-product/binary (car a-list)
          (cadr a-list))
        (cross-product/binary (car a-list)
          (generate-all-tuples (cdr a-list)))))))
other
(defloop assoc-alists
  (key alists)
  (for ((alist in alists))
    (append (and (assoc-equal key alist)
        (list (cdr (assoc-equal key alist)))))))
instantiate-pres-rule/litfunction
(defun instantiate-pres-rule/lit
  (prule f-lit
    all-terms
    all-fxr-term-instances
    vl
    state
    |FXRI{}|)
  (declare (xargs :guard (and (pseudo-termp f-lit)
        (alistp |FXRI{}|))))
  (b* ((ctx 'instantiate-pres-rule) ((mv yesp partial-s) (one-way-unify (get1 :constraint-term prule)
          f-lit))
      ((unless yesp) (value |FXRI{}|))
      (fxr-terms-pi (sublis-var-lst partial-s
          (get1 :fixer-terms prule)))
      (sigma-list-lst (match-pats/terms-alst fxr-terms-pi
          all-fxr-term-instances
          'nil))
      (sigmas-lst (generate-all-tuples sigma-list-lst)))
    (instantiate-prule/multiple-subst sigmas-lst
      partial-s
      prule
      all-terms
      vl
      ctx
      state
      |FXRI{}|)))
instantiate-pres-rule/litsfunction
(defun instantiate-pres-rule/lits
  (prule f-lits
    all-terms
    all-fxr-term-instances
    vl
    state
    |FXRI{}|)
  (declare (xargs :guard (and (pseudo-term-listp f-lits)
        (pseudo-term-listp all-terms)
        (alistp |FXRI{}|))))
  (if (endp f-lits)
    (value |FXRI{}|)
    (b* ((f-lit (car f-lits)) ((er |FXRI{}|) (instantiate-pres-rule/lit prule
            f-lit
            all-terms
            all-fxr-term-instances
            vl
            state
            |FXRI{}|)))
      (instantiate-pres-rule/lits prule
        (cdr f-lits)
        all-terms
        all-fxr-term-instances
        vl
        state
        |FXRI{}|))))
get-all-fixer-terms1function
(defun get-all-fixer-terms1
  (|FXRI{}| ans)
  (if (endp |FXRI{}|)
    ans
    (b* ((|RULEI{}| (cdr (car |FXRI{}|))) (fxr (get1 :fixer-term |RULEI{}|)))
      (get-all-fixer-terms1 (cdr |FXRI{}|)
        (add-to-set-equal fxr ans)))))
instantiate-pres-rulesfunction
(defun instantiate-pres-rules
  (prules f-lits
    all-terms
    vl
    state
    |FXRI{}|)
  (if (endp prules)
    (value |FXRI{}|)
    (b* ((prule (car prules)) (all-fxr-term-instances (get-all-fixer-terms1 |FXRI{}| 'nil))
        ((er |FXRI{}|) (instantiate-pres-rule/lits prule
            f-lits
            all-terms
            all-fxr-term-instances
            vl
            state
            |FXRI{}|)))
      (instantiate-pres-rules (cdr prules)
        f-lits
        all-terms
        vl
        state
        |FXRI{}|))))
remove-internal-vars/equationsfunction
(defun remove-internal-vars/equations
  (d |W{}|)
  (declare (xargs :guard (alistp d)))
  (if (endp d)
    'nil
    (if (member-equal (cons (caar d) (cadr (car d)))
        |W{}|)
      (remove-internal-vars/equations (cdr d)
        |W{}|)
      (b* (((list var e) (car d)) (e~ (sublis-var |W{}| e)))
        (if (equal var e~)
          (remove-internal-vars/equations (cdr d)
            |W{}|)
          (cons (list var e~)
            (remove-internal-vars/equations (cdr d)
              |W{}|)))))))
remove-intersecting-members-lstfunction
(defun remove-intersecting-members-lst
  (|FLITS{}| remove-list)
  (if (endp |FLITS{}|)
    'nil
    (if (intersectp (cdr (car |FLITS{}|))
        remove-list)
      (remove-intersecting-members-lst (cdr |FLITS{}|)
        remove-list)
      (cons (car |FLITS{}|)
        (remove-intersecting-members-lst (cdr |FLITS{}|)
          remove-list)))))
remove-unfixable-litsfunction
(defun remove-unfixable-lits
  (|TERM->FLITS{}| u-lits)
  (if (endp |TERM->FLITS{}|)
    'nil
    (b* (((cons term |FLITS{}|) (car |TERM->FLITS{}|)) (|FLITS1{}| (remove-intersecting-members-lst |FLITS{}|
            u-lits)))
      (cons (cons term |FLITS1{}|)
        (remove-unfixable-lits (cdr |TERM->FLITS{}|)
          u-lits)))))
remove-unfixable-constraintsfunction
(defun remove-unfixable-constraints
  (|TERM->FLITS{}| vl)
  (declare (xargs :mode :program))
  (b* ((unfixble-terms (get-all-keys nil |TERM->FLITS{}|)) ((when (null unfixble-terms)) |TERM->FLITS{}|)
      (- (cw? (verbose-stats-flag vl)
          "~| Cgen/Note: Unfixable constraints: ~x0~%"
          unfixble-terms))
      (all-terms (strip-cars |TERM->FLITS{}|))
      (fixble-terms (set-difference-equal all-terms
          unfixble-terms))
      (|TERM->FLITS{}| (assoc-equal-lst fixble-terms
          |TERM->FLITS{}|))
      (|TERM->FLITS{}| (remove-unfixable-lits |TERM->FLITS{}|
          unfixble-terms)))
    (remove-unfixable-constraints |TERM->FLITS{}|
      vl)))
fixer-rules-tablefunction
(defun fixer-rules-table
  (wrld)
  (table-alist 'fixer-rules-table wrld))
preservation-rules-tablefunction
(defun preservation-rules-table
  (wrld)
  (table-alist 'preservation-rules-table
    wrld))
other
(defloop collect-flits0
  (|FLITS{}|)
  (for ((fname--flits in |FLITS{}|))
    (append (cdr fname--flits))))
other
(defloop collect-flits
  (|TERM->FLITS{}|)
  (for ((|TERM--FLITS{}| in |TERM->FLITS{}|))
    (append (collect-flits0 (cdr |TERM--FLITS{}|)))))
fixer-arrangement1function
(defun fixer-arrangement1
  (terms all-terms vl ctx state)
  (b* ((wrld (w state)) (frules (strip-cdrs (fixer-rules-table wrld)))
      (prules (strip-cdrs (preservation-rules-table wrld)))
      ((mv ?erp1
         (list |TERM->FLITS{}|
           |?W{}|
           all-terms~
           |FXRI{}|)
         state) (instantiate-fixer-rules/terms-iter terms
          frules
          vl
          state
          'nil
          'nil
          all-terms
          'nil))
      (|TERM->FLITS{}| (remove-unfixable-constraints |TERM->FLITS{}|
          vl))
      (flits (collect-flits |TERM->FLITS{}|))
      ((mv ?erp2 |FXRI{}| state) (instantiate-pres-rules prules
          flits
          all-terms~
          vl
          state
          |FXRI{}|))
      ((when (or erp1 erp2)) (er soft
          ctx
          "~| Cgen/Error in instantiation of fixer or preservation rules!~%"))
      (type-hyps (filter-type-hyps terms wrld))
      (non-type-hyps (set-difference-equal terms type-hyps))
      (fixable-terms (strip-cars |TERM->FLITS{}|))
      (relevant-terms (intersection-equal non-type-hyps
          fixable-terms))
      ((er (list let*-soln0 rterms/true)) (fxri-let*-soln flits
          |TERM->FLITS{}|
          relevant-terms
          |FXRI{}|
          vl
          state))
      (rterms/false (set-difference-equal relevant-terms
          rterms/true))
      (let*-soln (remove-internal-vars/equations let*-soln0
          |W{}|))
      (- (cw? (verbose-stats-flag vl)
          "~| Cgen/Verbose: Fixer-bindings: ~x0~%"
          let*-soln))
      (- (cw? (verbose-stats-flag vl)
          "~| Cgen/Verbose: Fixed terms: ~x0~%"
          rterms/true))
      (- (cw? (verbose-stats-flag vl)
          "~| Cgen/Verbose: Unsat fixable terms: ~x0~%"
          rterms/false))
      (new-hyps0 (set-difference-equal all-terms~
          (equalitize-lst |W{}|)))
      (new-hyps1 (remove-duplicates-equal (sublis-var-lst |W{}| new-hyps0)))
      (new-hyps (set-difference-equal new-hyps1 all-terms)))
    (value (list let*-soln new-hyps rterms/false))))
fixer-arrangement1-lstfunction
(defun fixer-arrangement1-lst
  (terms-lst all-terms
    vl
    ctx
    state)
  (if (endp terms-lst)
    (value (list nil nil nil))
    (b* (((mv erp res1 state) (fixer-arrangement1 (car terms-lst)
           all-terms
           vl
           ctx
           state)) ((when erp) (fixer-arrangement1-lst (cdr terms-lst)
            all-terms
            vl
            ctx
            state))
        ((list b1 new-hyps1 unsat-hyps1) res1)
        ((mv ?erp
           (list b2 new-hyps2 unsat-hyps2)
           state) (fixer-arrangement1-lst (cdr terms-lst)
            all-terms
            vl
            ctx
            state)))
      (value (list (append b1 b2)
          (union-equal new-hyps1 new-hyps2)
          (union-equal unsat-hyps1 unsat-hyps2))))))
other
(logic)
rassoc-dlistfunction
(defun rassoc-dlist
  (v dlist)
  (if (endp dlist)
    nil
    (if (equal (cadr (car dlist)) v)
      (car dlist)
      (rassoc-dlist v (cdr dlist)))))
put-rassoc-dlistfunction
(defun put-rassoc-dlist
  (v key dlist)
  (if (endp dlist)
    (list (list key v))
    (if (equal (cadr (car dlist)) v)
      (cons (list key v) (cdr dlist))
      (cons (car dlist)
        (put-rassoc-dlist v key (cdr dlist))))))
update-mv-bindingfunction
(defun update-mv-binding
  (x i arity mv-term b)
  (b* ((entry (rassoc-dlist mv-term b)) ((unless (consp entry)) (cons (list (cons 'mv
              (update-nth i
                x
                (make-list arity :initial-element '&)))
            mv-term)
          b))
      ((list mv-vars &) entry)
      (mv-vars~ (update-nth (1+ i) x mv-vars))
      (b (put-rassoc-dlist mv-term
          mv-vars~
          b))
      (x-val `(mv-nth ',CGEN::I
          (mv-list ',CGEN::ARITY ,CGEN::MV-TERM)))
      (b (list-up-lists (strip-cars b)
          (sublis-var-lst (list (cons x-val x))
            (strip-cadrs b)))))
    b))
to-b*-mv-binding1function
(defun to-b*-mv-binding1
  (letb ans)
  (if (endp letb)
    (reverse ans)
    (b* (((list var e) (car letb)) ((unless (and (consp e) (equal (car e) 'mv-nth))) (to-b*-mv-binding1 (cdr letb)
            (cons (car letb) ans)))
        (`(mv-nth ',CGEN::INDEX
           (mv-list ',CGEN::ARITY ,CGEN::MV-TERM)) e))
      (to-b*-mv-binding1 (cdr letb)
        (update-mv-binding var
          index
          arity
          mv-term
          ans)))))
to-b*-mv-bindingfunction
(defun to-b*-mv-binding
  (letb)
  (to-b*-mv-binding1 letb 'nil))
inverse-subst/b*-mv-entryfunction
(defun inverse-subst/b*-mv-entry
  (vars i arity exp)
  (if (endp vars)
    'nil
    (if (not (equal (car vars) '&))
      (cons (cons `(mv-nth ',CGEN::I (mv-list ',CGEN::ARITY ,EXP))
          (car vars))
        (inverse-subst/b*-mv-entry (cdr vars)
          (1+ i)
          arity
          exp))
      (inverse-subst/b*-mv-entry (cdr vars)
        (1+ i)
        arity
        exp))))
inverse-subst/b*-entryfunction
(defun inverse-subst/b*-entry
  (key exp)
  (if (atom key)
    (list (cons exp key))
    (if (eq (car key) 'mv)
      (inverse-subst/b*-mv-entry (cdr key)
        0
        (len (cdr key))
        exp)
      nil)))
alist-suffix-starting-withfunction
(defun alist-suffix-starting-with
  (key b)
  (declare (xargs :guard (alistp b)))
  (if (endp b)
    'nil
    (if (equal (caar b) key)
      b
      (alist-suffix-starting-with key (cdr b)))))
other
(program)
subst-b*-entryfunction
(defun subst-b*-entry
  (key exp b)
  (b* ((dup-key-start-block (alist-suffix-starting-with key b)) (prior-block (take (- (len b)
            (len dup-key-start-block))
          b))
      (prior-block (list-up-lists (strip-cars prior-block)
          (sublis-expr-lst (inverse-subst/b*-entry key exp)
            (strip-cadrs prior-block)))))
    (append prior-block dup-key-start-block)))
collapse-b*-bindingfunction
(defun collapse-b*-binding
  (b1 b2)
  (if (endp b1)
    b2
    (cons (car b1)
      (subst-b*-entry (caar b1)
        (cadr (car b1))
        (collapse-b*-binding (cdr b1) b2)))))
fixer-arrangement1/repeatfunction
(defun fixer-arrangement1/repeat
  (c i
    all-terms
    vl
    ctx
    state
    b
    new-hyps)
  (if (endp c)
    (value (list b new-hyps 'nil))
    (b* ((- (cw? (verbose-stats-flag vl)
           "~| Cgen/Note: Recursively fix (loop iteration: ~x0) ~x1~%"
           i
           c)) ((mv erp res state) (fixer-arrangement1 c
            all-terms
            vl
            ctx
            state))
        ((when erp) (value (list b new-hyps c)))
        ((list b1 new-hyps1 c_unsat) res)
        ((unless (< (len c_unsat) (len c))) (value (list b new-hyps c)))
        (b (append b1 b))
        (new-hyps (union-equal new-hyps1 new-hyps)))
      (fixer-arrangement1/repeat c_unsat
        (1+ i)
        all-terms
        vl
        ctx
        state
        b
        new-hyps))))
fixer-arrangement-builtinfunction
(defun fixer-arrangement-builtin
  (hyps concl vl ctx state)
  (b* ((terms (append hyps
         (if (not (logic-termp concl (w state)))
           'nil
           (list (cgen-dumb-negate-lit concl))))) ((mv erp res state) (fixer-arrangement1 terms
          terms
          vl
          ctx
          state))
      ((when erp) (value (list nil nil)))
      ((list b new-hyps c_unsat) res)
      (rec-fixp (acl2s-defaults :get :recursively-fix))
      ((mv ?erp
         (list b new-hyps c_unsat)
         state) (if (and rec-fixp
            (< (len c_unsat) (len terms)))
          (fixer-arrangement1/repeat c_unsat
            1
            terms
            vl
            ctx
            state
            b
            new-hyps)
          (value (list b new-hyps c_unsat))))
      (- (cw? (and (verbose-stats-flag vl)
            rec-fixp
            (consp c_unsat))
          "~| Cgen/Verbose: ~x0 still not fixed! ~%"
          c_unsat))
      (b*-binding (to-b*-mv-binding b))
      (b*-binding (collapse-b*-binding b*-binding nil)))
    (value (list b*-binding new-hyps))))
other
(defttag t)
other
(defattach (fixer-arrangement fixer-arrangement-builtin)
  :skip-checks t)
other
(defttag nil)