elim-hint

(defun nominate-destructor-candidate-hint
  (term eliminables
    type-alist
    clause
    fns-to-elim
    ens
    wrld
    votes
    nominations)
  (declare (xargs :mode :program))
  (cond ((flambda-applicationp term) nominations)
    ((not (member-equal (ffn-symb term) fns-to-elim)) nominations)
    (t (let ((rule (getprop (ffn-symb term)
             'eliminate-destructors-rule
             nil
             'current-acl2-world
             wrld)))
        (cond ((null rule) nominations)
          (t (let ((crucial-arg (nth (access elim-rule rule :crucial-position) (fargs term))))
              (cond ((variablep crucial-arg) (let* ((alist (pairlis$ (fargs (access elim-rule rule :destructor-term))
                         (fargs term))) (inst-destructors (sublis-var-lst alist
                          (cons (access elim-rule rule :destructor-term)
                            (access elim-rule rule :destructor-terms))))
                      (pseudo-clause (sublis-expr-lst (pairlis$ inst-destructors nil) clause)))
                    (cond ((not (every-occurrence-equiv-hittablep-in-clausep (access elim-rule rule :equiv)
                           crucial-arg
                           pseudo-clause
                           ens
                           wrld)) nominations)
                      ((assoc-equal term nominations) (second-nomination term votes nominations))
                      ((member crucial-arg eliminables) (cond ((occurs-nowhere-else crucial-arg
                             (fargs term)
                             (access elim-rule rule :crucial-position)
                             0) (let* ((inst-hyps (sublis-var-lst alist (access elim-rule rule :hyps))))
                              (cond ((some-hyp-probably-nilp inst-hyps type-alist ens wrld) nominations)
                                (t (first-nomination term votes nominations)))))
                          (t nominations)))
                      (t nominations))))
                (t (nominate-destructor-candidate-hint crucial-arg
                    eliminables
                    type-alist
                    clause
                    fns-to-elim
                    ens
                    wrld
                    (cons term votes)
                    nominations))))))))))

(defun select-instantiated-elim-rule-hint
  (clause type-alist eliminables fns-to-elim ens wrld)
  (declare (xargs :mode :program))
  (let ((nominations (nominate-destructor-candidates-lst-hint clause
         eliminables
         type-alist
         clause
         fns-to-elim
         ens
         wrld
         nil)))
    (cond ((null nominations) nil)
      (t (let* ((dterm (pick-highest-sum-level-nos nominations wrld nil -1)) (rule (getprop (ffn-symb dterm)
                'eliminate-destructors-rule
                nil
                'current-acl2-world
                wrld))
            (alist (pairlis$ (fargs (access elim-rule rule :destructor-term))
                (fargs dterm))))
          (change elim-rule
            rule
            :hyps (sublis-var-lst alist (access elim-rule rule :hyps))
            :lhs (sublis-var alist (access elim-rule rule :lhs))
            :rhs (sublis-var alist (access elim-rule rule :rhs))
            :destructor-term (sublis-var alist (access elim-rule rule :destructor-term))
            :destructor-terms (sublis-var-lst alist
              (access elim-rule rule :destructor-terms))))))))

(defun pick-highest-sum-level-nos-hint
  (nominations wrld ans max-score)
  (declare (xargs :mode :program))
  (cond ((null nominations) ans)
    (t (let ((score (sum-level-nos (cdr (car nominations)) wrld)))
        (cond ((> score max-score) (pick-highest-sum-level-nos-hint (cdr nominations)
              wrld
              (list (caar nominations))
              score))
          ((equal score max-score) (pick-highest-sum-level-nos-hint (cdr nominations)
              wrld
              (cons (caar nominations) ans)
              score))
          (t (pick-highest-sum-level-nos-hint (cdr nominations)
              wrld
              ans
              max-score)))))))

(defun duplicate-inst-rule
  (inst-rule inst-rule-list)
  (declare (xargs :mode :program))
  (cond ((null inst-rule-list) nil)
    ((equal (access elim-rule inst-rule :destructor-terms)
       (access elim-rule (car inst-rule-list) :destructor-terms)) t)
    (t (duplicate-inst-rule inst-rule (cdr inst-rule-list)))))

(defun select-instantiated-elim-rules-hint1
  (dterms wrld ans)
  (declare (xargs :mode :program))
  (cond ((null dterms) ans)
    (t (let* ((dterm (car dterms)) (rule (getprop (ffn-symb dterm)
              'eliminate-destructors-rule
              nil
              'current-acl2-world
              wrld))
          (alist (pairlis$ (fargs (access elim-rule rule :destructor-term))
              (fargs dterm)))
          (inst-rule (change elim-rule
              rule
              :hyps (sublis-var-lst alist (access elim-rule rule :hyps))
              :lhs (sublis-var alist (access elim-rule rule :lhs))
              :rhs (sublis-var alist (access elim-rule rule :rhs))
              :destructor-term (sublis-var alist (access elim-rule rule :destructor-term))
              :destructor-terms (sublis-var-lst alist
                (access elim-rule rule :destructor-terms)))))
        (if (duplicate-inst-rule inst-rule ans)
          (select-instantiated-elim-rules-hint1 (cdr dterms) wrld ans)
          (select-instantiated-elim-rules-hint1 (cdr dterms)
            wrld
            (cons inst-rule ans)))))))

(defun select-instantiated-elim-rules-hint
  (clause type-alist eliminables fns-to-elim ens wrld ans)
  (declare (xargs :mode :program))
  (let ((nominations (nominate-destructor-candidates-lst-hint clause
         eliminables
         type-alist
         clause
         fns-to-elim
         ens
         wrld
         nil)))
    (cond ((null nominations) nil)
      (t (let ((dterms (pick-highest-sum-level-nos-hint nominations wrld nil -1)))
          (select-instantiated-elim-rules-hint1 dterms wrld ans))))))

(defun eliminate-destructors-hint2
  (cl eliminables avoid-vars fns-to-elim ens wrld)
  (declare (xargs :mode :program))
  (mv-let (contradictionp type-alist ttree)
    (type-alist-clause cl nil t nil ens wrld nil nil)
    (declare (ignore ttree))
    (cond (contradictionp (mv (list cl) nil nil))
      (t (let ((rule (select-instantiated-elim-rule-hint cl
               type-alist
               eliminables
               fns-to-elim
               ens
               wrld)))
          (cond ((null rule) (mv (list cl) nil nil))
            (t (mv-let (new-clause elim-vars1 ele)
                (apply-instantiated-elim-rule rule
                  cl
                  type-alist
                  avoid-vars
                  ens
                  wrld)
                (let ((clauses1 (split-on-assumptions (access elim-rule rule :hyps) cl nil)))
                  (cond ((equal new-clause *true-clause*) (mv clauses1 elim-vars1 (list ele)))
                    (t (mv-let (clauses2 elim-vars2 elim-seq)
                        (eliminate-destructors-hint2 new-clause
                          (union-eq elim-vars1
                            (remove1-eq (access elim-rule rule :rhs) eliminables))
                          avoid-vars
                          fns-to-elim
                          ens
                          wrld)
                        (mv (conjoin-clause-sets clauses1 clauses2)
                          (union-eq elim-vars1 elim-vars2)
                          (cons ele elim-seq))))))))))))))

(defun eliminate-destructors-hint11
  (cl avoid-vars rules type-alist fns-to-elim ens wrld)
  (declare (xargs :mode :program))
  (cond ((null rules) (mv nil nil nil))
    (t (mv-let (clauses-list elim-vars-list elim-seq-list)
        (eliminate-destructors-hint11 cl
          avoid-vars
          (cdr rules)
          type-alist
          fns-to-elim
          ens
          wrld)
        (let ((rule (car rules)))
          (mv-let (clauses0 elim-vars0 elim-seq0)
            (mv-let (new-clause elim-vars1 ele)
              (apply-instantiated-elim-rule rule
                cl
                type-alist
                avoid-vars
                ens
                wrld)
              (let ((clauses1 (split-on-assumptions (access elim-rule rule :hyps) cl nil)))
                (cond ((equal new-clause *true-clause*) (mv clauses1 elim-vars1 (list ele)))
                  (t (mv-let (clauses2 elim-vars2 elim-seq)
                      (eliminate-destructors-hint2 new-clause
                        elim-vars1
                        avoid-vars
                        fns-to-elim
                        ens
                        wrld)
                      (mv (conjoin-clause-sets clauses1 clauses2)
                        (union-eq elim-vars1 elim-vars2)
                        (cons ele elim-seq)))))))
            (mv (cons clauses0 clauses-list)
              (cons elim-vars0 elim-vars-list)
              (cons elim-seq0 elim-seq-list))))))))

(defun eliminate-destructors-hint1
  (cl eliminables avoid-vars fns-to-elim ens wrld)
  (declare (xargs :mode :program))
  (mv-let (contradictionp type-alist ttree)
    (type-alist-clause cl nil t nil ens wrld nil nil)
    (declare (ignore ttree))
    (cond (contradictionp (mv (list cl) nil nil))
      (t (let ((rules (select-instantiated-elim-rules-hint cl
               type-alist
               eliminables
               fns-to-elim
               ens
               wrld
               nil)))
          (eliminate-destructors-hint11 cl
            avoid-vars
            rules
            type-alist
            fns-to-elim
            ens
            wrld))))))

(defun eliminate-destructors-hint
  (clause elim-vars fns-to-elim pspv wrld)
  (declare (xargs :mode :program))
  (mv-let (clauses-list elim-vars-list elim-seq-list)
    (eliminate-destructors-hint1 clause
      (set-difference-eq (all-vars1-lst clause nil) elim-vars)
      nil
      fns-to-elim
      (access rewrite-constant
        (access prove-spec-var pspv :rewrite-constant)
        :current-enabled-structure)
      wrld)
    (cond (elim-seq-list (mv clauses-list elim-vars-list))
      (t (mv nil nil)))))

(defun the-ultimate-clause-processor
  (cl cl-list)
  (declare (ignore cl)
    (xargs :guard t))
  cl-list)

(defun crush-elim-vars
  (elim-vars-list)
  (declare (xargs :guard (true-list-listp elim-vars-list)))
  (if (endp elim-vars-list)
    nil
    (prog2$ (if (and (consp (car elim-vars-list))
          (consp (cadr elim-vars-list))
          (not (equal (car elim-vars-list) (cadr elim-vars-list))))
        (cw "This is bad.  Differing elim-vars found. ~%~x0 and ~x1~%~%"
          (car elim-vars-list)
          (cadr elim-vars-list))
        nil)
      (union-equal (car elim-vars-list)
        (crush-elim-vars (cdr elim-vars-list))))))

(defun generate-elim-hint
  (clauses-list)
  (declare (xargs :guard t))
  (if (atom clauses-list)
    nil
    (cons `(:clause-processor (the-ultimate-clause-processor clause ',(CAR CLAUSES-LIST)))
      (generate-elim-hint (cdr clauses-list)))))

(defun arithmetic-default-hint-11
  (id clause
    stable-under-simplificationp
    hist
    pspv
    world
    last-hint-used
    elim-vars)
  (declare (xargs :guard (and (consp id)
        (consp (cdr id))
        (true-listp (cadr id))
        (consp pspv)
        (consp (car pspv))
        (consp (caar pspv))
        (consp (cdaar pspv))
        (consp (car (cdaar pspv)))
        (consp (caar (cdaar pspv)))
        (consp (cdaar (cdaar pspv)))
        (alistp (cddaar (cdaar pspv))))
      :mode :program))
  (cond ((< 10 (len (cadr id))) `(:use (:theorem nil)))
    (stable-under-simplificationp (cond ((equal last-hint-used nil) (prog2$ (observation-cw 'arithmetic-default-hint-11 "Branch.")
            (let ((e/d '(((:rewrite normalize-factors-gather-exponents) (:rewrite simplify-products-gather-exponents-equal)
                    (:rewrite simplify-products-gather-exponents-<)) ((:rewrite prefer-positive-exponents-scatter-exponents-equal) (:rewrite prefer-positive-exponents-scatter-exponents-<)
                     (:rewrite prefer-positive-exponents-scatter-exponents-<-2)
                     (:rewrite |(expt x (+ m n))|)
                     (:rewrite |(expt x (+ m n)) non-zero (+ m n)|)
                     (:rewrite |(expt x (+ m n)) non-zero x|)
                     (:rewrite normalize-factors-scatter-exponents)
                     (:rewrite simplify-products-scatter-exponents-equal)
                     (:rewrite simplify-products-scatter-exponents-<)))))
              `(:computed-hint-replacement ((arithmetic-default-hint-11 id
                   clause
                   stable-under-simplificationp
                   hist
                   pspv
                   world
                   'check-branch-taken
                   ',ELIM-VARS))
                :or ((:dynamic-e/d ,E/D :nonlinearp nil) (:nonlinearp t))))))
        ((equal last-hint-used 'prefer-positive-exponents) (prog2$ (observation-cw 'arithmetic-default-hint-11
              "Prefer-positive-exponents.")
            `(:computed-hint-replacement ((arithmetic-default-hint-11 id
                 clause
                 stable-under-simplificationp
                 hist
                 pspv
                 world
                 'non-linear-arithmetic
                 ',ELIM-VARS))
              :nonlinearp t)))
        ((equal last-hint-used 'recycle) (prog2$ (observation-cw 'arithmetic-default-hint-11 "Recycle.")
            `(:computed-hint-replacement ((arithmetic-default-hint-11 id
                 clause
                 stable-under-simplificationp
                 hist
                 pspv
                 world
                 'non-linear-arithmetic
                 ',ELIM-VARS))
              :nonlinearp t)))
        ((equal last-hint-used 'non-linear-arithmetic) (prog2$ (observation-cw 'arithmetic-default-hint-11
              "Settled-down-clause.")
            (mv-let (clauses-list elim-vars-list)
              (eliminate-destructors-hint clause
                elim-vars
                '(floor mod)
                pspv
                world)
              (if clauses-list
                `(:computed-hint-replacement ((arithmetic-default-hint-11 id
                     clause
                     stable-under-simplificationp
                     hist
                     pspv
                     world
                     'recycle
                     ',(UNION-EQUAL ELIM-VARS (CRUSH-ELIM-VARS ELIM-VARS-LIST))))
                  :or ,(GENERATE-ELIM-HINT CLAUSES-LIST))
                nil))))
        (t nil)))
    ((equal last-hint-used 'check-branch-taken) (let ((branch-taken (branch-taken id)))
        (cond ((equal branch-taken 2) (prog2$ (observation-cw 'arithmetic-default-hint-11
                "Check-branch-taken prefer-positive-exponents.")
              `(:computed-hint-replacement ((arithmetic-default-hint-11 id
                   clause
                   stable-under-simplificationp
                   hist
                   pspv
                   world
                   'prefer-positive-exponents
                   ',ELIM-VARS))
                :no-op t)))
          ((equal branch-taken 1) (prog2$ (observation-cw 'arithmetic-default-hint-11
                "Check-branch-taken non-linear-arithmetic.")
              `(:computed-hint-replacement ((arithmetic-default-hint-11 id
                   clause
                   stable-under-simplificationp
                   hist
                   pspv
                   world
                   'recycle
                   ',ELIM-VARS))
                :nonlinearp nil)))
          (t (cw "~%~%~ [Note: Computed hint error --- seemingly impossible ~
                  case reached in arithmetic-default-hint-11.  Perhaps there ~
                  are two or more :OR hints interacting in unexpected ways.  ~
                  We do not know what to do here, and so are defaulting to ~
                  doing nothing.~%~%")))))
    ((and (equal last-hint-used 'non-linear-arithmetic)
       (consp hist)
       (consp (car hist))
       (not (equal (caar hist) 'settled-down-clause))) (prog2$ (observation-cw 'arithmetic-default-hint-11
          "Non-linear-arithmetic.")
        `(:computed-hint-replacement ((arithmetic-default-hint-11 id
             clause
             stable-under-simplificationp
             hist
             pspv
             world
             'recycle
             ',ELIM-VARS))
          :nonlinearp nil)))
    (t nil)))