non-linear

(defun cleanse-type-alist
  (type-alist pt)
  (cond ((null type-alist) nil)
    ((to-be-ignoredp (cddar type-alist) pt) (cleanse-type-alist (cdr type-alist) pt))
    (t (cons (car type-alist)
        (cleanse-type-alist (cdr type-alist) pt)))))

(defun var-with-divisionp
  (var)
  (cond ((eq (fn-symb var) 'expt) (let ((base (fargn var 1)) (exponent (fargn var 2)))
        (or (and (eq (fn-symb base) 'unary-/)
            (not (eq (fn-symb (fargn base 1)) 'binary-+)))
          (and (not (eq (fn-symb base) 'binary-+))
            (quotep exponent)
            (integerp (unquote exponent))
            (< (unquote exponent) 0))
          (and (not (eq (fn-symb base) 'binary-+))
            (eq (fn-symb exponent) 'binary-*)
            (quotep (fargn exponent 1))
            (integerp (unquote (fargn exponent 1)))
            (< (unquote (fargn exponent 1)) 0)))))
    (t (and (eq (fn-symb var) 'unary-/)
        (not (eq (fn-symb (fargn var 1)) 'binary-+))))))

(defun varify
  (x)
  (cond ((quotep x) (er hard
        'varify
        "This should not have happened.  The supposed ~
              variable, ~x0, is instead a constant."
        x))
    ((equal (fn-symb x) 'binary-+) (if (quotep (fargn x 1))
        (varify (fargn x 2))
        (varify (fargn x 1))))
    ((and (equal (fn-symb x) 'binary-*) (quotep (fargn x 1))) (varify (fargn x 2)))
    (t x)))

(defun varify!
  (x)
  (let ((temp (varify x)))
    (if (good-pot-varp temp)
      temp
      (er hard
        'varify!
        "Varify! is supposed to return a good-pot-varp, but ~
           returned ~x0 on ~x1."
        temp
        x))))

(defun varify!-lst1
  (lst acc)
  (if (null lst)
    acc
    (varify!-lst1 (cdr lst) (cons (varify! (car lst)) acc))))

(defun varify!-lst (lst) (varify!-lst1 lst nil))

(defun invert-var
  (var)
  (cond ((eq (fn-symb var) 'expt) (let ((base (fargn var 1)) (exponent (fargn var 2)))
        (cond ((eql exponent ''-1) (varify! base))
          ((eq (fn-symb base) 'unary-/) (fcons-term* 'expt (fargn base 1) exponent))
          ((eq (fn-symb exponent) 'unary--) (fcons-term* 'expt base (fargn exponent 1)))
          ((and (quotep exponent)
             (integerp (unquote exponent))
             (< (unquote exponent) 0)) (fcons-term* 'expt base (kwote (- (unquote exponent)))))
          ((and (eq (fn-symb exponent) 'binary-*)
             (quotep (fargn exponent 1))
             (integerp (unquote (fargn exponent 1)))
             (< (unquote (fargn exponent 1)) 0)) (fcons-term* 'expt
              base
              (cons-term 'binary-*
                (list (kwote (- (unquote (fargn exponent 1))))
                  (fargn exponent 2)))))
          (t (fcons-term* 'expt
              (cons-term 'unary-/ (list base))
              exponent)))))
    ((eq (fn-symb var) 'unary-/) (varify! (fargn var 1)))
    (t (cons-term 'unary-/ (list var)))))

(defun part-of1
  (var1 var2)
  (cond ((or (variablep var2) (fquotep var2)) (if (equal var1 var2)
        *1*
        nil))
    ((eq (ffn-symb var2) 'binary-*) (let ((arg1 (fargn var2 1)) (arg2 (fargn var2 2)))
        (if (equal var1 arg1)
          arg2
          (let ((new-var2 (part-of1 var1 arg2)))
            (cond ((null new-var2) nil)
              ((equal new-var2 ''1) arg1)
              (t (cons-term 'binary-* (list arg1 new-var2))))))))
    (t (if (equal var1 var2)
        *1*
        nil))))

(defun part-of
  (var1 var2)
  (cond ((or (variablep var1) (fquotep var1)) (part-of1 var1 var2))
    ((eq (ffn-symb var1) 'binary-*) (let ((new-var2 (part-of (fargn var1 1) var2)))
        (cond (new-var2 (part-of (fargn var1 2) new-var2)) (t nil))))
    (t (part-of1 var1 var2))))

(defun product-already-triedp
  (var-list products-already-tried)
  (cond ((null products-already-tried) nil)
    (t (or (equal var-list (car products-already-tried))
        (product-already-triedp var-list
          (cdr products-already-tried))))))

(defun too-many-polysp
  (var-lst pot-lst counter)
  (cond ((null var-lst) (< 20 counter))
    (t (too-many-polysp (cdr var-lst)
        pot-lst
        (* counter (length (polys-with-var1 (car var-lst) pot-lst)))))))

(defun expanded-new-vars-in-pot-lst2
  (new-var vars-to-skip vars-to-return)
  (cond ((or (member-equal new-var vars-to-skip)
       (quotep new-var)
       (eq (fn-symb new-var) 'binary-+)) (mv vars-to-skip vars-to-return))
    ((eq (fn-symb new-var) 'binary-*) (let ((new-factor (fargn new-var 1)))
        (if (or (member-equal new-factor vars-to-skip)
            (quotep new-factor)
            (eq (fn-symb new-factor) 'binary-+))
          (expanded-new-vars-in-pot-lst2 (fargn new-var 2)
            vars-to-skip
            vars-to-return)
          (expanded-new-vars-in-pot-lst2 (fargn new-var 2)
            (cons new-factor vars-to-skip)
            (cons new-factor vars-to-return)))))
    ((var-with-divisionp new-var) (let ((inverted-var (invert-var new-var)))
        (if (member-equal inverted-var vars-to-skip)
          (mv (cons new-var vars-to-skip)
            (cons new-var vars-to-return))
          (mv (cons new-var (cons inverted-var vars-to-skip))
            (cons new-var (cons inverted-var vars-to-return))))))
    (t (mv (cons new-var vars-to-skip)
        (cons new-var vars-to-return)))))

(defun expanded-new-vars-in-pot-lst1
  (new-pot-lst vars-to-skip vars-to-return)
  (if (null new-pot-lst)
    vars-to-return
    (let ((new-var (access linear-pot (car new-pot-lst) :var)))
      (cond ((member-equal new-var vars-to-skip) (expanded-new-vars-in-pot-lst1 (cdr new-pot-lst)
            vars-to-skip
            vars-to-return))
        ((var-with-divisionp new-var) (let* ((inverse-var (invert-var new-var)) (new-vars-to-skip (if (member-equal inverse-var vars-to-skip)
                  (cons new-var vars-to-skip)
                  (cons new-var (cons inverse-var vars-to-skip))))
              (new-vars-to-return (if (member-equal inverse-var vars-to-skip)
                  (cons new-var vars-to-return)
                  (cons new-var (cons inverse-var vars-to-return)))))
            (expanded-new-vars-in-pot-lst1 (cdr new-pot-lst)
              new-vars-to-skip
              new-vars-to-return)))
        ((eq (fn-symb new-var) 'binary-*) (mv-let (new-vars-to-skip new-vars-to-return)
            (expanded-new-vars-in-pot-lst2 new-var
              vars-to-skip
              vars-to-return)
            (expanded-new-vars-in-pot-lst1 (cdr new-pot-lst)
              (cons new-var new-vars-to-skip)
              (cons new-var new-vars-to-return))))
        (t (expanded-new-vars-in-pot-lst1 (cdr new-pot-lst)
            (cons new-var vars-to-skip)
            (cons new-var vars-to-return)))))))

(defun expanded-new-vars-in-pot-lst
  (new-pot-lst old-pot-lst)
  (let ((vars-to-skip (expanded-new-vars-in-pot-lst1 old-pot-lst nil nil)))
    (varify!-lst (expanded-new-vars-in-pot-lst1 new-pot-lst vars-to-skip nil))))

(defun extract-bounds
  (bounds-polys)
  (cond ((null bounds-polys) (mv nil nil nil nil nil nil))
    ((null (cdr bounds-polys)) (if (< (first-coefficient (car bounds-polys)) 0)
        (mv nil
          nil
          nil
          (access poly (car bounds-polys) :constant)
          (access poly (car bounds-polys) :relation)
          (access poly (car bounds-polys) :ttree))
        (mv (- (access poly (car bounds-polys) :constant))
          (access poly (car bounds-polys) :relation)
          (access poly (car bounds-polys) :ttree)
          nil
          nil
          nil)))
    (t (if (< (first-coefficient (car bounds-polys)) 0)
        (mv (- (access poly (cadr bounds-polys) :constant))
          (access poly (cadr bounds-polys) :relation)
          (access poly (cadr bounds-polys) :ttree)
          (access poly (car bounds-polys) :constant)
          (access poly (car bounds-polys) :relation)
          (access poly (car bounds-polys) :ttree))
        (mv (- (access poly (car bounds-polys) :constant))
          (access poly (car bounds-polys) :relation)
          (access poly (car bounds-polys) :ttree)
          (access poly (cadr bounds-polys) :constant)
          (access poly (cadr bounds-polys) :relation)
          (access poly (cadr bounds-polys) :ttree))))))

(defun good-bounds-in-pot
  (var pot-lst pt)
  (let ((bounds-polys (bounds-polys-with-var var pot-lst pt)))
    (mv-let (var-lbd var-lbd-rel
        var-lbd-ttree
        var-ubd
        var-ubd-rel
        var-ubd-ttree)
      (extract-bounds bounds-polys)
      (declare (ignore var-lbd-ttree var-ubd-ttree))
      (or (and (eql var-lbd 0) (eql var-ubd 0))
        (and var-lbd (< 0 var-lbd))
        (and (eql var-lbd 0) (eq var-lbd-rel '<))
        (and var-ubd (< var-ubd 0))
        (and (eql var-ubd 0) (eq var-ubd-rel '<))))))

(defun inverse-polys
  (var inv-var pot-lst ttree pt)
  (if (and (good-pot-varp var) (good-pot-varp inv-var))
    (let ((bounds-polys-for-var (bounds-polys-with-var var pot-lst pt)) (bounds-polys-for-inv-var (bounds-polys-with-var inv-var pot-lst pt)))
      (mv-let (var-lbd var-lbd-rel
          var-lbd-ttree
          var-ubd
          var-ubd-rel
          var-ubd-ttree)
        (extract-bounds bounds-polys-for-var)
        (mv-let (inv-var-lbd inv-var-lbd-rel
            inv-var-lbd-ttree
            inv-var-ubd
            inv-var-ubd-rel
            inv-var-ubd-ttree)
          (extract-bounds bounds-polys-for-inv-var)
          (cond ((and (or (eql var-lbd 0) (eql inv-var-lbd 0))
               (or (eql var-ubd 0) (eql inv-var-ubd 0))) (list (add-linear-terms :rhs var
                  (base-poly (cons-tag-trees ttree
                      (cons-tag-trees var-lbd-ttree inv-var-lbd-ttree))
                    '<=
                    t
                    nil))
                (add-linear-terms :lhs var
                  (base-poly (cons-tag-trees ttree
                      (cons-tag-trees var-ubd-ttree inv-var-ubd-ttree))
                    '<=
                    t
                    nil))
                (add-linear-terms :rhs inv-var
                  (base-poly (cons-tag-trees ttree
                      (cons-tag-trees var-lbd-ttree inv-var-lbd-ttree))
                    '<=
                    t
                    nil))
                (add-linear-terms :lhs inv-var
                  (base-poly (cons-tag-trees ttree
                      (cons-tag-trees var-ubd-ttree inv-var-ubd-ttree))
                    '<=
                    t
                    nil))))
            ((or (and var-lbd (< 0 var-lbd))
               (and inv-var-lbd (< 0 inv-var-lbd))) (let* ((ttree1 (cons-tag-trees ttree
                     (cons-tag-trees var-lbd-ttree inv-var-lbd-ttree))) (bounds-polys1 (cond ((and var-ubd
                         (not (eql var-ubd 0))
                         (or (null inv-var-lbd) (< inv-var-lbd (/ var-ubd)))) (list (add-linear-terms :lhs (kwote (/ var-ubd))
                            :rhs inv-var
                            (base-poly (cons-tag-trees ttree1 var-ubd-ttree)
                              var-ubd-rel
                              t
                              nil))))
                      ((null inv-var-lbd) (list (add-linear-terms :rhs inv-var (base-poly ttree1 '< t nil))))
                      (t nil)))
                  (bounds-polys2 (cond ((and inv-var-ubd
                         (not (eql inv-var-ubd 0))
                         (or (null var-lbd) (< var-lbd (/ inv-var-ubd)))) (cons (add-linear-terms :lhs (kwote (/ inv-var-ubd))
                            :rhs var
                            (base-poly (cons-tag-trees ttree1 inv-var-ubd-ttree)
                              inv-var-ubd-rel
                              t
                              nil))
                          bounds-polys1))
                      ((null var-lbd) (cons (add-linear-terms :rhs var (base-poly ttree1 '< t nil))
                          bounds-polys1))
                      (t bounds-polys1)))
                  (bounds-polys3 (cond ((and var-lbd
                         (not (eql var-lbd 0))
                         (or (null inv-var-ubd) (< (/ var-lbd) inv-var-ubd))) (cons (add-linear-terms :lhs inv-var
                            :rhs (kwote (/ var-lbd))
                            (base-poly ttree1 var-lbd-rel t nil))
                          bounds-polys2))
                      (t bounds-polys2)))
                  (bounds-polys4 (cond ((and inv-var-lbd
                         (not (eql inv-var-lbd 0))
                         (or (null var-ubd) (< (/ inv-var-lbd) var-ubd))) (cons (add-linear-terms :lhs var
                            :rhs (kwote (/ inv-var-lbd))
                            (base-poly ttree1 inv-var-lbd-rel t nil))
                          bounds-polys3))
                      (t bounds-polys3))))
                bounds-polys4))
            ((or (and var-ubd (< var-ubd 0))
               (and inv-var-ubd (< inv-var-ubd 0))) (let* ((ttree1 (cons-tag-trees ttree
                     (cons-tag-trees var-ubd-ttree inv-var-ubd-ttree))) (bounds-polys1 (cond ((and var-lbd
                         (not (eql var-lbd 0))
                         (or (null inv-var-ubd) (< (/ var-lbd) inv-var-ubd))) (list (add-linear-terms :lhs inv-var
                            :rhs (kwote (/ var-lbd))
                            (base-poly (cons-tag-trees ttree1 var-lbd-ttree)
                              var-lbd-rel
                              t
                              nil))))
                      ((null inv-var-ubd) (list (add-linear-terms :lhs inv-var (base-poly ttree1 '< t nil))))
                      (t nil)))
                  (bounds-polys2 (cond ((and inv-var-lbd
                         (not (eql inv-var-lbd 0))
                         (or (null var-ubd) (< (/ inv-var-lbd) var-ubd))) (cons (add-linear-terms :lhs var
                            :rhs (kwote (/ inv-var-lbd))
                            (base-poly (cons-tag-trees ttree1 inv-var-lbd-ttree)
                              var-lbd-rel
                              t
                              nil))
                          bounds-polys1))
                      ((null var-ubd) (cons (add-linear-terms :lhs var (base-poly ttree1 '< t nil))
                          bounds-polys1))
                      (t bounds-polys1)))
                  (bounds-polys3 (cond ((and var-ubd
                         (not (eql var-ubd 0))
                         (or (null inv-var-lbd) (< inv-var-lbd (/ var-ubd)))) (cons (add-linear-terms :lhs (kwote (/ var-ubd))
                            :rhs inv-var
                            (base-poly ttree1 var-ubd-rel t nil))
                          bounds-polys2))
                      (t bounds-polys2)))
                  (bounds-polys4 (cond ((and inv-var-ubd
                         (not (eql inv-var-ubd 0))
                         (or (null var-lbd) (< var-lbd (/ inv-var-ubd)))) (cons (add-linear-terms :lhs (kwote (/ inv-var-ubd))
                            :rhs var
                            (base-poly ttree1 inv-var-ubd-rel t nil))
                          bounds-polys3))
                      (t bounds-polys3))))
                bounds-polys4))
            ((and (eql var-lbd 0) (eq var-lbd-rel '<)) (list (add-linear-terms :rhs inv-var
                  (base-poly (cons-tag-trees ttree var-lbd-ttree) '< t nil))))
            ((and (eql inv-var-lbd 0) (eq inv-var-lbd-rel '<)) (list (add-linear-terms :rhs var
                  (base-poly (cons-tag-trees ttree inv-var-lbd-ttree)
                    '<
                    t
                    nil))))
            ((and (eql var-ubd 0) (eq var-ubd-rel '<)) (list (add-linear-terms :lhs inv-var
                  (base-poly (cons-tag-trees ttree var-ubd-ttree) '< t nil))))
            ((and (eql inv-var-ubd 0) (eq inv-var-ubd-rel '<)) (list (add-linear-terms :lhs var
                  (base-poly (cons-tag-trees ttree inv-var-ubd-ttree)
                    '<
                    t
                    nil))))
            (t nil)))))
    (er hard
      'inverse-polys
      "A presumptive pot-label, ~x0,  has turned out to be illegitimate. ~
         If possible, please send a script reproducing this error ~
         to the authors of ACL2."
      (if (good-pot-varp var)
        inv-var
        var))))

(defun add-inverse-polys
  (var type-alist
    wrld
    simplify-clause-pot-lst
    force-flg
    ens
    pt)
  (if (var-with-divisionp var)
    (let ((inverted-var (invert-var var)))
      (mv-let (base-ts base-ttree)
        (type-set inverted-var
          force-flg
          nil
          type-alist
          ens
          wrld
          nil
          nil
          nil)
        (if (ts-real/rationalp base-ts)
          (let ((inverse-polys (inverse-polys var
                 inverted-var
                 simplify-clause-pot-lst
                 base-ttree
                 pt)))
            (add-polys inverse-polys
              simplify-clause-pot-lst
              pt
              t
              type-alist
              ens
              force-flg
              wrld))
          (mv nil simplify-clause-pot-lst))))
    (mv nil simplify-clause-pot-lst)))

(defun add-polys-from-type-set
  (var pot-lst type-alist pt force-flg ens wrld)
  (if (good-pot-varp var)
    (add-polys (polys-from-type-set var
        force-flg
        nil
        type-alist
        ens
        wrld
        nil)
      pot-lst
      pt
      t
      type-alist
      ens
      force-flg
      wrld)
    (mv (er hard
        'add-polys-from-type-set
        "A presumptive pot-label, ~x0,  has turned out to be illegitimate. ~
         If possible, please send a script  reproducing this error ~
         to the authors of ACL2."
        var)
      nil)))

(defun length-of-shortest-polys-with-var
  (poly-lst pt n)
  (cond ((null poly-lst) n)
    ((and (or (eq n t)
         (< (length (access poly (car poly-lst) :alist)) n))
       (not (ignore-polyp (access poly (car poly-lst) :parents) pt))) (length-of-shortest-polys-with-var (cdr poly-lst)
        pt
        (length (access poly (car poly-lst) :alist))))
    (t (length-of-shortest-polys-with-var (cdr poly-lst) pt n))))

(defun shortest-polys-with-var1
  (poly-lst pt n)
  (cond ((or (null poly-lst) (eq n t)) nil)
    ((and (or (equal (length (access poly (car poly-lst) :alist)) n)
         (equal (length (access poly (car poly-lst) :alist)) (+ n 1)))
       (not (ignore-polyp (access poly (car poly-lst) :parents) pt))) (cons (car poly-lst)
        (shortest-polys-with-var1 (cdr poly-lst) pt n)))
    (t (shortest-polys-with-var1 (cdr poly-lst) pt n))))

(defun shortest-polys-with-var
  (var pot-lst pt)
  (cond ((null pot-lst) nil)
    ((equal var (access linear-pot (car pot-lst) :var)) (let ((n (length-of-shortest-polys-with-var (append (access linear-pot (car pot-lst) :negatives)
               (access linear-pot (car pot-lst) :positives))
             pt
             t)))
        (append (shortest-polys-with-var1 (access linear-pot (car pot-lst) :negatives)
            pt
            n)
          (shortest-polys-with-var1 (access linear-pot (car pot-lst) :positives)
            pt
            n))))
    (t (shortest-polys-with-var var (cdr pot-lst) pt))))

(defun binary-*-leaves
  (term)
  (if (eq (fn-symb term) 'binary-*)
    (cons (fargn term 1) (binary-*-leaves (fargn term 2)))
    (list term)))

(defun binary-*-tree
  (leaves)
  (cond ((null (cdr leaves)) (car leaves))
    ((null (cddr leaves)) (cons-term 'binary-* (list (car leaves) (cadr leaves))))
    (t (cons-term 'binary-*
        (list (car leaves) (binary-*-tree (cdr leaves)))))))

(defun merge-arith-term-order
  (l1 l2)
  (cond ((null l1) l2)
    ((null l2) l1)
    ((arith-term-order (car l2) (car l1)) (cons (car l2) (merge-arith-term-order l1 (cdr l2))))
    (t (cons (car l1) (merge-arith-term-order (cdr l1) l2)))))

(defun insert-arith-term-order
  (item list)
  (cond ((null list) (list item))
    ((arith-term-order item (car list)) (cons item list))
    (t (cons (car list) (insert-arith-term-order item (cdr list))))))

(defun sort-arith-term-order
  (list)
  (cond ((null list) nil)
    (t (insert-arith-term-order (car list)
        (sort-arith-term-order (cdr list))))))

(defun multiply-alist-and-const
  (alist const poly)
  (cond ((null alist) poly)
    (t (let ((temp-poly (add-linear-term (cons-term 'binary-*
               (list (kwote (* const (cdar alist))) (caar alist)))
             'rhs
             poly)))
        (multiply-alist-and-const (cdr alist) const temp-poly)))))

(defun collect-rational-poly-p-lst
  (poly-lst)
  (cond ((endp poly-lst) nil)
    ((access poly (car poly-lst) :rational-poly-p) (cons (car poly-lst)
        (collect-rational-poly-p-lst (cdr poly-lst))))
    (t (collect-rational-poly-p-lst (cdr poly-lst)))))