; ACL2 Version 4.0 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2010  University of Texas at Austin

; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
; (C) 1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

; This program is free software; you can redistribute it and/or modify
; it under the terms of the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.

; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
; GNU General Public License for more details.

; You should have received a copy of the GNU General Public License
; along with this program; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

; Written by:  Matt Kaufmann               and J Strother Moore
; email:       Kaufmann@cs.utexas.edu      and Moore@cs.utexas.edu
; Department of Computer Sciences
; University of Texas at Austin
; Austin, TX 78712-1188 U.S.A.

(in-package "ACL2")


;=================================================================


; We continue our development of linear arithmetic.  In particular,
; we define the functions add-polys and linearize.


;=================================================================


; Add-polys

(defun polys-from-type-set (term force-flag dwp type-alist ens wrld ttree)

; If possible, we create a list of polys based upon the type-set
; of term.

; Warning: This function should not be used with any terms that are
; not legitimate pot-vars.  See the definition of good-pot-varp.
; Assuming that term is a legitimate pot-label --- meets all the
; invariants --- we do not have to normalize any of the polys below.

; We check that term is OK and throw an error if not.  It would,
; however, not be very expensive to wrap the below in a call to
; normalize-poly-lst, and thereby avoid the potential error situation.

  (if (good-pot-varp term)
    (mv-let (ts ts-ttree)
      (type-set term force-flag dwp type-alist ens wrld ttree nil nil)
      (cond ((ts-subsetp ts *ts-zero*)
             (list 
              ;; 0 <= term
              (add-linear-terms :rhs term
                                (base-poly ts-ttree
                                           '<=
                                           t
                                           nil))
              ;; term <= 0
              (add-linear-terms :lhs term
                                (base-poly ts-ttree
                                           '<=
                                           t
                                           nil))))
            ((ts-subsetp ts *ts-positive-integer*)
             (list 
              ;; 1 <= term
              (add-linear-terms :lhs *1*
                                :rhs term
                                (base-poly ts-ttree
                                           '<=
                                           t
                                           nil))))
            ((ts-subsetp ts *ts-negative-integer*)
             (list 
              ;; term <= -1
              (add-linear-terms :lhs term
                                :rhs ''-1
                                (base-poly ts-ttree
                                           '<=
                                           t
                                           nil))))
            ((ts-subsetp ts
                         #-:non-standard-analysis *ts-positive-rational*
                         #+:non-standard-analysis *ts-positive-real*)
             (list 
              ;; 0 < term
              (add-linear-terms :rhs term
                                (base-poly ts-ttree
                                           '<
                                           t
                                           nil))))
            ((ts-subsetp ts
                         #-:non-standard-analysis *ts-negative-rational*
                         #+:non-standard-analysis *ts-negative-real*)
             (list 
              ;; term < 0
              (add-linear-terms :lhs term
                                (base-poly ts-ttree
                                           '<
                                           t
                                           nil))))
            ((ts-subsetp ts
                         #-:non-standard-analysis *ts-non-negative-rational*
                         #+:non-standard-analysis *ts-non-negative-real*)
             (list 
              ;; 0 <= term
              (add-linear-terms :rhs term
                                (base-poly ts-ttree
                                           '<=
                                           t
                                           nil))))
            ((ts-subsetp ts
                         #-:non-standard-analysis *ts-non-positive-rational*
                         #+:non-standard-analysis *ts-non-positive-real*)
             (list 
              ;; term <= 0
              (add-linear-terms :lhs term
                                (base-poly ts-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."
        term)))

(defun add-type-set-polys (var-lst new-pot-lst old-pot-lst
                           already-noted-vars
                           pt nonlinearp
                           type-alist ens force-flg wrld)

; We have just finished adding a bunch of polys to a pot-lst.  In ACL2
; versions prior to 2.7, these polys were canceled against any
; type-set information on the fly.  We now add the type-set
; information explicitly.  This function checks which pots have been
; modified (any new polys in these pots would have been canceled
; against type-set knowledge in the past), derives polys (using
; type-set information) about the vars of the modified pots, and adds
; them to the pots.

  (cond ((null var-lst)
         (let ((new-var-lst (changed-pot-vars new-pot-lst old-pot-lst
                                              already-noted-vars)))
           (if new-var-lst
               (add-type-set-polys new-var-lst
                                   new-pot-lst new-pot-lst
                                   new-var-lst
                                   pt nonlinearp
                                   type-alist ens force-flg wrld)
             (mv nil new-pot-lst))))
        (t
         (mv-let (contradictionp new-new-pot-lst)
           (add-polys0 (polys-from-type-set (car var-lst)
                                            force-flg
                                            nil ;;; dwp
                                            type-alist
                                            ens
                                            wrld
                                            nil) ;;; ttree
                       new-pot-lst pt nonlinearp t)
           (cond (contradictionp
                  (mv contradictionp nil))
                 (t
                  (add-type-set-polys (cdr var-lst)
                                      new-new-pot-lst old-pot-lst
                                      already-noted-vars
                                      pt nonlinearp
                                      type-alist ens force-flg wrld)))))))

(defun add-polynomial-inequalities (lst pot-lst pt nonlinearp type-alist ens
                                        force-flg wrld)

; Wrapper for the old add-polys (now add-polys0) so that we can
; eliminate the use of cancel-poly-against-type-set from within add-poly.

; We add the polys in lst to the pot-lst, and then call add-type-set-polys
; which performs a similar function to the old calls to
; cancel-poly-against-type-set.

; Historical Note:  The nearest approximation to this function in Nqthm
; was named add-equations.

  (mv-let (contradictionp new-pot-lst)
          (add-polys0 lst pot-lst pt nonlinearp t)
          (cond (contradictionp
                 (mv contradictionp nil))
                (t
                 (let ((changed-pot-vars
                        (changed-pot-vars new-pot-lst pot-lst nil)))
                   (add-type-set-polys changed-pot-vars
                                       new-pot-lst new-pot-lst
                                       changed-pot-vars
                                       pt nonlinearp
                                       type-alist ens force-flg wrld))))))

#-acl2-loop-only
(defparameter *add-polys-counter*

; This is used by dmr-string to show the cumulative number of calls of
; add-polys, as requested by Robert Krug.

  0)

(defun add-polys (lst pot-lst pt nonlinearp type-alist ens force-flg wrld)
  #-acl2-loop-only
  (when (f-get-global 'dmrp *the-live-state*)
    (return-from
     add-polys
     (progn
       (incf *add-polys-counter*)
       (pstk
        (add-polynomial-inequalities lst pot-lst pt nonlinearp type-alist ens
                                     force-flg wrld)))))
  (add-polynomial-inequalities lst pot-lst pt nonlinearp type-alist ens
                               force-flg wrld))


;=================================================================


; Linearize

(mutual-recursion

(defun eval-ground-subexpressions (term ens wrld state ttree)
  (cond
   ((variablep term) (mv nil term ttree))
   ((fquotep term) (mv nil term ttree))
   ((flambda-applicationp term)
    (mv-let
     (flg args ttree)
     (eval-ground-subexpressions-lst (fargs term) ens wrld state ttree)
     (cond
      ((all-quoteps args)
       (mv-let
        (flg val ttree)
        (eval-ground-subexpressions
         (sublis-var (pairlis$ (lambda-formals (ffn-symb term)) args)
                     (lambda-body (ffn-symb term)))
         ens wrld state ttree)
        (declare (ignore flg))
        (mv t val ttree)))
      (flg

; We could look for just those args that are quoteps, and substitute those,
; presumably then calling make-lambda-application to create a lambda out of the
; result.  But we'll put that off for another time, or even indefinitely,
; noting that through Version_2.9.4 we did not evaluate any ground lambda
; applications.

       (mv t (cons-term (ffn-symb term) args) ttree))
      (t (mv nil term ttree)))))
   ((eq (ffn-symb term) 'if)
    (mv-let
     (flg1 arg1 ttree)
     (eval-ground-subexpressions (fargn term 1) ens wrld state ttree)
     (cond
      ((quotep arg1)
       (if (cadr arg1)
           (mv-let
            (flg2 arg2 ttree)
            (eval-ground-subexpressions (fargn term 2) ens wrld state ttree)
            (declare (ignore flg2))
            (mv t arg2 ttree))
           (mv-let
            (flg3 arg3 ttree)
            (eval-ground-subexpressions (fargn term 3) ens wrld state ttree)
            (declare (ignore flg3))
            (mv t arg3 ttree))))
      (t (mv-let
          (flg2 arg2 ttree)
          (eval-ground-subexpressions (fargn term 2) ens wrld state ttree)
          (mv-let
           (flg3 arg3 ttree)
           (eval-ground-subexpressions (fargn term 3) ens wrld state ttree)
           (mv (or flg1 flg2 flg3)
               (if (or flg1 flg2 flg3)
                   (fcons-term* 'if arg1 arg2 arg3)
                 term)
               ttree)))))))
   (t (mv-let
       (flg args ttree)
       (eval-ground-subexpressions-lst (fargs term) ens wrld state ttree)
       (cond

; The following test was taken from rewrite with a few modifications
; for the formals used.

        ((and (logicalp (ffn-symb term) wrld) ; maybe fn is being admitted
              (all-quoteps args)
              (enabled-xfnp (ffn-symb term) ens wrld)

; We don't mind disallowing constrained functions that have attachments,
; because the call of ev-fncall below disallows the use of attachments (last
; parameter, aok, is nil).

              (not (getprop (ffn-symb term) 'constrainedp nil
                            'current-acl2-world wrld)))
         (mv-let
          (erp val latches)
          (pstk
           (ev-fncall (ffn-symb term)
                      (strip-cadrs args)
                      (f-decrement-big-clock state)
                      nil t nil))
          (declare (ignore latches))
          (cond
           (erp
            (cond (flg
                   (mv t (cons-term (ffn-symb term) args) ttree))
                  (t (mv nil term ttree))))
           (t (mv t
                  (kwote val)
                  (push-lemma (fn-rune-nume (ffn-symb term) nil t wrld)
                              ttree))))))
        (flg (mv t (cons-term (ffn-symb term) args) ttree))
        (t (mv nil term ttree)))))))

(defun eval-ground-subexpressions-lst (lst ens wrld state ttree)
  (cond ((null lst) (mv nil nil ttree))
        (t (mv-let
            (flg1 x ttree)
            (eval-ground-subexpressions (car lst) ens wrld state ttree)
            (mv-let
             (flg2 y ttree)
             (eval-ground-subexpressions-lst (cdr lst) ens wrld state ttree)
             (mv (or flg1 flg2)
                 (if (or flg1 flg2)
                     (cons x y)
                   lst)
                 ttree))))))
)

(defun poly-set (op poly1 poly2)

; Suppose linearize is called on some term, term.  The output of
; linearize is either nil, (list (list poly1 poly2)), or (list (list
; poly1) (list poly2)).  An answer of the first form means "no
; arithmetic information can be extracted from the assumption that
; term is true."  An answer of the second form means "both poly1 and
; poly2 are true if term is true."  An answer of the third form means
; "either poly1 or poly2 is true if term is true."

; This functions takes two polys and an operation, op, and constructs
; the answer returned by linearize.  Op is either 'and or 'or and
; determines whether we construct (list (list poly1 poly2)), when
; op='and, or (list (list poly1) (list poly2)), when op='or.

; However, there are two special cases.

; First, it is sometimes the case that we want to construct an 'and
; but only have one poly, the other one being nil.  This may happen
; when we were going to construct an 'or but noticed that one branch
; is contradictory.  When this happens it is always poly1 that is nil
; and poly2 that we want to return.

; Second, it may happen that either or both of the polys are silly in
; the sense that they are based on false assumptions.  Since silly polys
; are logically true, we act accordingly.  Thus, if we are to return
; a conjunction and one of the polys is silly we return the other.
; But if we are to return a disjunction and one is silly, we return nil,
; meaning we could extract no arithmetic information.  For example,
; suppose poly2 is silly and we are to return (list (list poly1) (list poly2)).
; Then the silliness of poly2 means the second disjunct is true, which
; is represented here as (list (list poly1) nil).  That, by the way, was
; nqthm's answer in this case.  However, this disjunct gives the caller
; no help because it means either poly1 is true or T is true.  So we
; just tell the caller "no information".

; Note about Nqthm:  As remarked above, nqthm's linearize can return
; (list (list poly1) nil).  How is this used?  It is put on the
; split-lst when we start adding polynomials to the pot.  We then see if
; we can get a contradiction from one side and if so, we assume the other.
; We certainly can't get a contradiction from the nil side.  Suppose
; we got a contradiction from the other.  Then we'd assume the other
; side, which is a no-op.  The end result is that returning such an
; answer causes work but is guaranteed to have no effect.

; It is unlikely that we can generate a silly poly2 without generating a
; silly poly1, since silliness stems from requiring a false rationalp
; assumption.  However, rather than convince ourselves that they are
; both silly if either is, we'll just check both.

  (cond ((eq op 'and)
         (cond ((or (eq poly1 nil)
                    (silly-polyp poly1))
                (cond ((silly-polyp poly2) nil)
                      (t (list (list poly2)))))
               ((silly-polyp poly2)
                (list (list poly1)))
               (t (list (list poly1 poly2)))))
        ((or (silly-polyp poly1)
             (silly-polyp poly2))
         nil)
        ((impossible-polyp poly1)
         (list (list (change poly poly2
                             :ttree
                             (cons-tag-trees (access poly poly1 :ttree)
                                             (access poly poly2 :ttree))
                             :parents
                             (marry-parents (access poly poly1 :parents)
                                            (access poly poly2 :parents))))))
        ((impossible-polyp poly2)
         (list (list (change poly poly1
                             :ttree
                             (cons-tag-trees (access poly poly1 :ttree)
                                             (access poly poly2 :ttree))
                             :parents
                             (marry-parents (access poly poly1 :parents)
                                            (access poly poly2 :parents))))))
        (t (list (list poly1) (list poly2)))))

;; RAG - I changed complex-rational to complex, and rational to real,
;; to stand for the non-zero numbers.

(defun linearize1 (term positivep type-alist ens force-flg wrld ttree state)

; See the comment in linearize.  Linearize1 does all the work of linearize
; except that the latter maps normalize-poly over the former.

    (mv-let (flg temp ttree)
      (eval-ground-subexpressions term ens wrld state ttree)
      (declare (ignore flg))
     (mv-let
      (not-flg atm)
      (strip-not temp)

; Let us pause for a moment here.  Term is the original term we are to
; linearize and is preserved for the use of add-linear-assumption.  Temp is
; the result of replacing all ground subexpressions in term by their
; values, and atm is temp with any 'not stripped off.  Recall that we
; are attempting to derive a contradiction by assuming either (1) that
; term is true if positivep is true, or (2) that term is false if
; positivep is false.  Since not-flg tells us whether atm is the
; negation of term/temp, we use it to reset positivep to reflect its
; new role with respect to atm.

      (let ((positivep (if not-flg (not positivep) positivep)))
        (cond
         ((inequalityp atm)
          (let ((lhs (fargn atm 1))
                (rhs (fargn atm 2)))
            (mv-let (ts-lhs ts-ttree)
              (type-set lhs force-flg nil type-alist ens wrld ttree nil nil)
              (mv-let (ts-rhs ts-ttree)
                (type-set rhs force-flg nil type-alist ens wrld ts-ttree nil
                          nil)
                (if positivep ; (< lhs rhs)
                    (cond
                     ((and (ts-integerp ts-lhs)
                           (ts-integerp ts-rhs))

; (implies (and (< lhs rhs)
;               (integerp lhs)
;               (integerp rhs))
;          (<= (1+ lhs) rhs))

                      (poly-set 'and
                                nil
                                (add-linear-terms
                                 :lhs lhs
                                 :lhs *1*
                                 :rhs rhs
                                 (base-poly ts-ttree
                                            '<=
                                            t
                                            nil))))
                     (t ; still (< lhs rhs), but not both integerp
                      (poly-set 'and
                                nil
                                (add-linear-terms
                                 :lhs lhs
                                 :rhs rhs
                                 (let ((rationalp-flg
                                        (and (ts-real/rationalp ts-lhs)
                                             (ts-real/rationalp ts-rhs))))
                                   (base-poly0 (if rationalp-flg
                                                   ts-ttree
                                                 ttree)

; :Parent wart:

; In a slight break from tradition (here and in three other places below that
; refer to this comment), we use the parents from the original ttree.  When
; fixing a (probably long-standing) bug in Version_3.0.1 by recording ts-ttree
; above in the case that rationalp-flg is true, we found that the regression
; suite broke in three places without this tweak on the parents.  Since
; rationalp-flg is only used in non-linear arithmetic, this seems like a minor
; break from our traditional propagation of parent trees.  We considered making
; a similar change for all calls of base-poly in this function, but that led to
; a proof failure in
; books/workshops/2004/schmaltz-borrione/support/routing_defuns.lisp that
; looked like it would be painful to fix, and we took that as a sign that such
; loss of backward compatibility could be painful for other users, and
; potentially even a bad heuristic.

                                               (collect-parents ttree)
                                               '<
                                               rationalp-flg
                                               nil))))))

; The (not positivep) case.  Note:
; (implies (not (< lhs rhs))
;          (<= rhs lhs))

                  (poly-set 'and
                            nil
                            (add-linear-terms
                             :lhs rhs
                             :rhs lhs
                             (let ((rationalp-flg
                                    (and (ts-real/rationalp ts-lhs)
                                         (ts-real/rationalp ts-rhs))))
                               (base-poly0 (if rationalp-flg ts-ttree ttree)

; See the "break from tradition" comment above for a discussion of the
; parents.

                                           (collect-parents ttree)
                                           '<=
                                           rationalp-flg
                                           nil)))))))))
         ((equalityp atm)
          (let ((lhs (fargn atm 1))
                (rhs (fargn atm 2)))
            (mv-let (ts-lhs ts-ttree)
              (type-set lhs force-flg nil type-alist ens wrld ttree nil nil)
              (mv-let (ts-rhs ts-ttree)
                (type-set rhs force-flg nil type-alist ens wrld ts-ttree nil
                          nil)

; Here is the one place that we can construct a poly which is derived
; from a negated equality.  Note that the final argument to base-poly
; is 'T.

                (if positivep

; (implies (equal lhs rhs) 
;          (and (<= lhs rhs) (<= rhs lhs)))

                    (let ((rationalp-flg (and (ts-real/rationalp ts-lhs)
                                              (ts-real/rationalp ts-rhs))))
                      (poly-set 'and
                                (add-linear-terms
                                 :lhs lhs
                                 :rhs rhs
                                 (base-poly0 (if rationalp-flg ts-ttree ttree)

; See the "break from tradition" comment above for a discussion of the
; parents.

                                             (collect-parents ttree)
                                             '<=
                                             rationalp-flg
                                             t))
                                (add-linear-terms
                                 :lhs rhs
                                 :rhs lhs
                                 (base-poly0 (if rationalp-flg ts-ttree ttree)

; See the "break from tradition" comment above for a discussion of the
; parents.

                                             (collect-parents ttree)
                                             '<=
                                             rationalp-flg
                                             t))))

; Other case: (not (equal lhs rhs)).  But we need additional (type) information
; in order to derive inequalities.

                  (cond ((and (ts-subsetp ts-lhs *ts-integer*)
                              (ts-subsetp ts-rhs *ts-integer*))

; (implies (and (not (equal lhs rhs))
;               (integerp lhs)
;               (integerp rhs))
;          (or (<= (1+ lhs) rhs)
;              (<= (1+ rhs) lhs)))

                         (poly-set 'or
                                   (add-linear-terms
                                    :lhs lhs
                                    :lhs *1*
                                    :rhs rhs
                                    (base-poly ts-ttree
                                               '<=
                                               t
                                               nil))
                                   (add-linear-terms
                                    :lhs rhs
                                    :lhs *1*
                                    :rhs lhs
                                    (base-poly ts-ttree
                                               '<=
                                               t
                                               nil))))
                        ((if (ts-subsetp ts-lhs *ts-acl2-number*)
                             (or (ts-subsetp ts-rhs *ts-acl2-number*)
                                 (not (ts-intersectp ts-lhs *ts-zero*)))
                           (and (ts-subsetp ts-rhs *ts-acl2-number*)
                                (not (ts-intersectp ts-rhs *ts-zero*))))

; (implies (and (not (equal lhs rhs))
;               (or (and (acl2-numberp lhs)
;                        (acl2-numberp rhs))
;                   (and (acl2-numberp lhs)
;                        (not (equal lhs 0)))
;                   (and (acl2-numberp rhs)
;                        (not (equal rhs 0)))))
;          (or (< lhs rhs)
;              (< rhs lhs)))

                         (let ((rationalp-flg
                                (and (ts-real/rationalp ts-lhs)
                                     (ts-real/rationalp ts-rhs))))
                           (poly-set 'or
                                     (add-linear-terms
                                      :lhs lhs
                                      :rhs rhs
                                      (base-poly ts-ttree
                                                 '<
                                                 rationalp-flg
                                                 nil))
                                     (add-linear-terms
                                      :lhs rhs
                                      :rhs lhs
                                      (base-poly ts-ttree
                                                 '<
                                                 rationalp-flg
                                                 nil)))))
                        ((and (ts-acl2-numberp ts-lhs)
                              force-flg
                              (ts-intersectp ts-rhs *ts-acl2-number*))

; (implies (and (not (equal lhs rhs))
;               (acl2-numberp lhs)
;               (force (acl2-numberp rhs)))
;          (or (< lhs rhs)
;              (< rhs lhs)))

                         (mv-let (flg new-ttree)
                                 (add-linear-assumption
                                  term
                                  `(acl2-numberp ,rhs)
                                  type-alist ens
                                  (immediate-forcep nil ens)
                                  force-flg wrld ts-ttree)

; We strongly suspect that add-linear-assumption will succeed with flg =
; :added, since (ts-intersectp ts-rhs *ts-acl2-number*).  But we do not depend
; on this without checking it.

                                 (assert$
                                  (and (not (eq flg :failed))
                                       (not (eq flg :known-false)))
                                  (poly-set 'or
                                            (add-linear-terms
                                             :lhs lhs
                                             :rhs rhs
                                             (base-poly new-ttree
                                                        '<
                                                        nil
                                                        nil))
                                            (add-linear-terms
                                             :lhs rhs
                                             :rhs lhs
                                             (base-poly new-ttree
                                                        '<
                                                        nil
                                                        nil))))))
                        ((and (ts-acl2-numberp ts-rhs)
                              force-flg
                              (ts-intersectp ts-lhs *ts-acl2-number*))

; (implies (and (not (equal lhs rhs))
;               (acl2-numberp rhs)
;               (force (acl2-numberp lhs)))
;          (or (< lhs rhs)
;              (< rhs lhs)))

                         (mv-let (flg new-ttree)
                                 (add-linear-assumption
                                  term
                                  `(acl2-numberp ,lhs)
                                  type-alist ens
                                  (immediate-forcep nil ens)
                                  force-flg wrld ts-ttree)
                                 (assert$ ; see comment on preceding assert$
                                  (and (not (eq flg :failed))
                                       (not (eq flg :known-false)))
                                  (poly-set 'or
                                            (add-linear-terms
                                             :lhs lhs
                                             :rhs rhs
                                             (base-poly new-ttree
                                                        '<
                                                        nil
                                                        nil))
                                            (add-linear-terms
                                             :lhs rhs
                                             :rhs lhs
                                             (base-poly new-ttree
                                                        '<
                                                        nil
                                                        nil))))))
                        (t
                         nil)))))))
       ((quotep atm)

; This is a strange one.  It can happen that the
; eval-ground-subexpressions can reduce the term to a constant.  We
; saw this happen in a bug reported by Jun Sawada.  Suppose (<= 2 (foo
; x)) is a :LINEAR lemma about foo.  Suppose we wish to prove (not
; (equal 1 (foo 3))).  This should be obvious.  But we assume the
; negation of the conclusion and get (foo 3) = 1.  We then find the
; linear lemma and instantiate it to get (<= 2 (foo 3)).  We then
; rewrite-linear-concl and get (<= 2 1), which we eval to 'nil!  If we
; do not recognize that we've succeeded here, we do not prove the
; theorem because all manner of other heuristics prevent us from using
; (<= 2 (foo x)) against the current literal.  Not surprisingly, this
; is an example of tail biting: we've used the negation of the goal to
; prevent ourselves from proving it!  One could probably construct a
; more insidious example of tail biting from this example -- an
; example that is not solved by the hack here of recognizing when eval
; solved our problem -- by arranging for rewrite-linear-concl to
; rewrite the inequality to something that we can't use but which
; doesn't eval to nil.    

; Here is another curious example:
#|
 ACL2 !>
 (thm
  (implies (and (not (consp x))
                (true-listp x))
           (equal (reverse (reverse x)) x)))

 But simplification reduces this to T, using the :executable-counterparts
 of EQUAL and REVERSE and linear arithmetic.

 Q.E.D.

 Summary
 Form:  ( THM ...)
 Rules: ((:DEFINITION NOT)
         (:EXECUTABLE-COUNTERPART EQUAL)
         (:EXECUTABLE-COUNTERPART REVERSE)
         (:FAKE-RUNE-FOR-LINEAR NIL))
 Warnings:  None
 Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)

 Proof succeeded.
|#
; Note the presence of (:FAKE-RUNE-FOR-LINEAR NIL).
; This oddity is due to the fact that we now rewrite all terms (not
; just the conclusion of linear lemmas) before adding them to the
; linear-pot-lst.

        (if positivep

; Recall that we are hoping to derive a contradiction from assuming atm
; true.  Hence, we win iff atm is 'NIL.

            (if (equal atm *nil*)
                (poly-set 'and
                          nil
                          (impossible-poly ttree))
              nil)

; We are hoping to derive a contradiction from assuming atm false.  Hence,
; we win iff atm is not 'NIL.

          (if (not (equal atm *nil*))
              (poly-set 'and
                        nil
                        (impossible-poly ttree))
              nil)))
       (t nil))))))

(defun linearize (term positivep type-alist ens force-flg wrld ttree state)

; If positivep we are to linearize term; else we are to linearize the negation
; of term.  The linearization of a term is either NIL, meaning no linear
; information was extracted from the term; or else it is a list of length 1
; containing a list of polynomials ((p1...pn)) such that term implies their
; conjunction (p1&...&pn); or else it is a list of length 2, ((p1...pn)
; (q1...qn)), such that term implies the disjunction (p1&...&pn) \/
; (q1&...&qn).  The claim that the term implies the polys has to be taken with
; a grain of salt: the additional 'assumptions in the ttree fields of the polys
; must be considered.

; There are two situations where this code might add an assumption to the polys
; it creates.  The first is that we sometimes call type-set and may get back a
; ttree with assumptions in it, which then infect our polys.  The second
; involves the linearization of negative equalities, where we insist that both
; x and y be numeric in order to derive (or (< x y) (< y x)) from (not (equal x
; y)).  Otherwise, we do not add any assumptions to our polys.

; We store ttree in the ttree of the poly.

; Trace Note:
#|
  (trace (linearize
          :entry
          (list* (car si::arglist) (cadr si::arglist) (caddr si::arglist)
                 '|ens| (car (cddddr si::arglist)) '(|wrld| |ttree| |state|))
          :exit
          (cond ((null (car values)) (list nil))
                ((null (cdr (car values)))
                 (list (cons 'and (show-poly-lst (car (car values))))))
                (t (list
                    (list 'or
                          (cons 'and (show-poly-lst (car (car values))))
                          (cons 'and (show-poly-lst (cadr (car values))))))))))
|#

  (let ((temp (linearize1 term positivep type-alist ens
                          force-flg wrld ttree state)))
    (cond ((null temp)
           nil)
          ((null (cdr temp))
           (list (normalize-poly-lst (car temp))))
          (t
           (list (normalize-poly-lst (car temp))
                 (normalize-poly-lst (cadr temp)))))))

(defun linearize-lst1
  (term-lst ttrees positivep type-alist ens force-flg wrld state
            poly-lst split-lst)
  (cond ((null term-lst)
         (mv (reverse poly-lst) (reverse split-lst)))
        (t (let ((lst (linearize (car term-lst)
                                 positivep
                                 type-alist ens force-flg wrld
                                 (car ttrees)
                                 state)))
             (cond
              ((null lst)
               (linearize-lst1 (cdr term-lst)
                               (cdr ttrees)
                               positivep
                               type-alist ens force-flg wrld state
                               poly-lst split-lst))
              ((null (cdr lst))
               (linearize-lst1 (cdr term-lst)
                               (cdr ttrees)
                               positivep
                               type-alist ens force-flg wrld state
                               (revappend (car lst) poly-lst) split-lst))
              (t
               (linearize-lst1 (cdr term-lst)
                               (cdr ttrees)
                               positivep
                               type-alist ens force-flg wrld state
                               poly-lst (cons lst split-lst))))))))

(defun linearize-lst
  (term-lst ttrees positivep type-alist ens force-flg wrld state)

; This function linearizes every term in term-lst, using the parity
; indicated by positivep, and type-alist and wrld.  This effectively
; assumes true/false (as per positivep) each term in term-lst and produces
; some polys.  Ttrees is in weak 1:1 correspondence with term-lst and
; enumerates the parent trees to use for each term in all the polys
; generated for the term; if ttrees is nil, no parent tree is stored.

; We return two values, poly-lst and split-lst.  The first is a list of
; polys that may be assumed true.  I.e., all these polys are implied by the
; assumption of term-lst.  The second is a list of doublets (lst1 lst2),
; such that each lst is a list of polys and the assumption of term-lst
; implies one of either lst1 or lst2 for each doublet.

  (linearize-lst1 term-lst ttrees positivep type-alist ens force-flg wrld state
                  nil nil))