acl2-source 6.3-5 / usr / share / acl2-6.3 / linear-a.lisp

; ACL2 Version 6.3 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2013, Regents of the University of Texas

; 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 LICENSE file distributed with ACL2.

; 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
; LICENSE for more details.

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

(in-package "ACL2")

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

; This file defines the basics of the linear arithmetic decision
; procedure.  We also include clause histories, parent trees,
; tag-trees, and assumptions; all of which are needed by add-poly
; and friends.

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

; We begin with some general support functions.  They should
; probably be organized and moved to axioms.lisp.

(defabbrev ts-acl2-numberp (ts)
  (ts-subsetp ts *ts-acl2-number*))

(defabbrev ts-rationalp (ts)
  (ts-subsetp ts *ts-rational*))

(defabbrev ts-real/rationalp (ts)
  #+non-standard-analysis
  (ts-subsetp ts *ts-real*)
  #-non-standard-analysis
  (ts-subsetp ts *ts-rational*))

(defabbrev ts-integerp (ts)
  (ts-subsetp ts *ts-integer*))

(defun all-quoteps (lst)
  (cond ((null lst) t)
        (t (and (quotep (car lst))
                (all-quoteps (cdr lst))))))

(mutual-recursion

(defun dumb-occur (x y)

; This function determines if term x occurs in term y, but does not
; look for x inside of quotes.  It is thus equivalent to occur if you
; know that x is not a quotep.

  (cond ((equal x y) t)
        ((variablep y) nil)
        ((fquotep y) nil)
        (t (dumb-occur-lst x (fargs y)))))

(defun dumb-occur-lst (x lst)
  (cond ((null lst) nil)
        (t (or (dumb-occur x (car lst))
               (dumb-occur-lst x (cdr lst))))))

)

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

; Clause Histories

; Clauses carry with them their histories, which describe which processes
; have produced them.  A clause history is a list of history-entry records.
; A process, such as simplify-clause, might inspect the history of its
; input clause to help decide whether to perform a certain transformation.

(defrec history-entry

; Important Note: This record is laid out this way so that we can use
; assoc-eq on histories to detect the presence of a history-entry for
; a given processor.  Do not move the processor field!

  (processor ttree clause signal . cl-id)
  t)

; Processor is a waterfall processor (e.g., 'simplify-clause).  The
; ttree and signal are, respectively, the ttree and signal produced by
; the processor on clause.  Each history-entry is built in the
; waterfall, but we inspect them for the first time in this file.

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

; Essay on Parent Trees

; Structurally, a "parent tree" or pt is either nil, a number, or the cons
; of two parent trees.  Parent trees are used to represent sets of
; literals.  In particular, every number in a pt is the position of some
; literal in the current-clause variable of simplify-clause1 and the tree
; may be thought of as representing that set of literals.  Pts are used
; to avoid tail biting.  An earlier implementation of this used "clause-tails."
; We explain everything below.

; "Tail biting" is our name for the insidious phenomenon that occurs when
; one assumes p false while trying to prove p and then, carelessly,
; rewrites the goal p to false on the basis of that assumption.  Observe
; that this is sound but detrimental to success.  One way to prevent
; tail biting is to not assume p false while trying to prove it, but we
; found that too weak.  The way we avoid tail biting is to keep careful
; track of what we're trying to prove, which literal we are working on,
; and what assumptions have been used to derive what results; we never use
; the assumption that p is false (or anything derived from it) to rewrite
; p to false.  Despite our efforts, tail biting by simplify-clause is
; possible.  See "On Tail Biting by Simplify-clause" for more.

; The easiest to understand use of parent trees in this regard is in
; linear arithmetic.  In simplify-clause1 we setup the
; simplify-clause-pot-lst, by expressing all the arithmetic hypotheses of
; the conjecture as polynomial inequalities.  When new inequalities are
; introduced, as when trying to relieve the hypothesis of some rule, we
; can combine them with the preprocessed "polys" to quickly settle certain
; arithmetic statements.  To avoid duplication of effort, our
; simplify-clause-pot-lst contains polys derived from all possible
; literals of the current clause.  This is because a great deal of work
; may be done (via linear lemmas and rewriting) to derive a poly about a
; given suggestive subterm of a given literal and we do not want to do it
; each time we assume that literal false.  Note the ease with which we
; could bite our tail: the list of inequalities is derived from the
; negations of every literal so we might easily use an inequality to
; falsify the literal from which it was derived.  To avoid this, each poly
; is tagged with one or more parent trees.  Intuitively the poly derived
; from an inequality literal is tagged with that literal.  But other
; literals may have been used, e.g., to establish certain terms rational,
; so one must think of the polys as being tagged with sets of literals.
; Then, when we are rewriting a particular literal we tell ourselves (by
; making a note in the :pt field of the rcnst) to avoid any poly
; descending from the goal literal.  Similar use is made of parent trees
; in the fc-pair-lst -- a list of preprocessed conclusions obtained by
; forward chaining from the current clause.

; The problem is made subtle by the fact that the literals we are
; rewriting change before we get to them and thus cannot be recognized by
; their structure alone.  Consider the clause {lit1 lit2 lit3}.  Now
; suppose we forward chain from ~lit3 and deduce concl.  Then fc-pair-lst
; will contain (concl . ttree) where ttree contains a parent tree
; acknowledging our dependence on lit3.  We may thus use concl when we are
; working on lit1 and lit2.  But suppose that in simplifying lit1 we
; produce the literal (not (equal var 27)).  Then we can substitute 27 for
; var everywhere and will actually do so.  Thus, by the time we get to
; work on the third literal of the clause above it will not be lit3 but
; some reduced instance, lit3', of lit3.  If the parent tree literally
; contained lit3, it would be impossible to recognize that concl was to be
; avoided.

; Therefore, we actually refer to literals by their position in the
; current-clause of simplify-clause1 (from which the preprocessing was
; done) and we keep careful track as we simplify what the original pt for
; each literal was.  As we scan over the literals to simplify we maintain
; a map, an enumeration of pts, giving the pt for each literal.  Thus,
; while we actually go to work on lit3' above, we will actually have in
; our hand the fact that lit3 is its parent.  Keeping track of the parents
; of the literals we are working on is made harder by the fact that
; sometimes literal merge.  For example, in {lit1 lit2 lit3} lit1 may
; simplify to lit3 and thus we may merge them.  The surviving literal is
; given the parent tree that contains both 1 and 3 so we know not to use
; conclusions derived from either.  The rewrite-constant, rcnst, in use
; below simplify-clause1 contains as one of its fields the
; :current-clause.  Thus, given the rewrite-constant and a pt it is
; possible to recover the original parent literals.

; We generally use "pt" to refer to a single parent tree.  "Pts" is a list
; of parent trees, implicitly in "weak 1:1 correspondence" with some list
; of terms.  By "weak" we mean pts may be shorter than the list of terms
; and "excess terms" have the nil pt.  That is, it is ok to cdr pts as you
; cdr down the list of terms and every time you need a pt for a term you
; take the car of pts.  There is no need to store the nil pt in tag-trees,
; so we don't.  Thus, a commonly used convention is to supply a pts of nil
; to a function that stores 'pts, causing it to store no pts.

; In the early days we did not use parent trees but "clause-tails" -- the
; tail of clause starting with the parent literal.  This was adopted to
; avoid the confusion caused by duplicate literals.  But it was rendered
; unworkable when we implemented the Satriani hacks and started
; substituting for variables as we went.  It also suffered other problems
; due to sloppy implementation.

(defun pt-occur (n pt)

; Determine whether n occurs in the set denoted by pt.

  (cond ((null pt) nil)
        ((consp pt) (or (pt-occur n (car pt)) (pt-occur n (cdr pt))))
        (t (= n pt))))

(defun pt-intersectp (pt1 pt2)

; Determine whether the intersection of the sets denoted by pt1 and pt2
; is nonempty.

  (cond ((null pt1) nil)
        ((consp pt1)
         (or (pt-intersectp (car pt1) pt2)
             (pt-intersectp (cdr pt1) pt2)))
        (t (pt-occur pt1 pt2))))

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

; Essay on Tag-Trees

; If you add a new tag, be sure to include it in all-runes-in-ttree!

; Tags in Tag-Trees

; After Version_4.2 we switched to a representation of a tag-tree as an alist,
; associating a key with a non-empty list of values, rather than building up
; tag-trees with operations (acons tag value ttree) and (cons ttree1 ttree2).
; Note that we view these lists as sets, and are free to ignore order and
; duplications (though we attempt to avoid duplicates).   Our motivation was to
; allow the addition of a new key, associated with many values, without
; degrading performance significantly.

; Each definition of a primitive for manipulating tag-trees has the comment: "
; Note: Tag-tree primitive".

; See all-runes-in-ttree for the set of all legal tags and their associated
; values.  Some of the tags and associated values are as follows.

; 'lemma

; The tagged object is either a lemma name (a symbolp) or else is the
; integer 0 indicating the use of linear arithmetic.

; 'pt

; The tagged object is a "parent tree".  See the Essay on Parent Trees.
; The tree identifies a set of literals in the current-clause of
; simplify-clause1 used in the derivation of poly or term with which the
; tree is associated.  We need this information for two reasons.  First,
; in order to avoid tail biting (see below) we do not use any poly that
; descends from the assumption of the falsity of the literal we are trying
; to prove.  Second, in find-equational-poly we seek two polys that can be
; combined to derive an equality, and we use 'pt to identify those that
; themselves descend from equality hypotheses.

; 'assumption

; The tagged object is an assumption record containing, among other things, a
; type-alist and a term which must be true under the type-alist in order to
; assure the validity of the poly or rewrite with which the tree is associated.
; We cannot linearize (- x), for example, without knowing (rationalp x).  If we
; cannot establish it by type set reasoning, we add that 'assumption to the
; poly generated.  If we eventually use the poly in a derivation, the
; 'assumption will infect it and when we get up to the simplify-clause level we
; will split on them.

; 'find-equational-poly

; The tagged object is a pair of polynomials.  During simplify clause
; we try to find two polys that can be combined to form an equation we
; don't have explicitly in the clause.  If we succeed, we add the
; equation to the clause.  However, it may be simplified into
; unrecognizable form and we need a way to avoid re-generation of the
; equation in future calls of simplify.  We do this by infecting the
; tag-tree with this tag and the two polys used.

; Historical Note from the days when tag-trees were constructed using (acons
; tag value ttree) and (cons-tag-trees ttree1 ttree2):

; ; The invention of tag-trees came about during the designing of the linear
; ; package.  Polynomials have three "arithmetic" fields, the constant, alist,
; ; and relation.  But they then have many other fields, like lemmas,
; ; assumptions, and literals.  At the time of this writing they have 5 other
; ; fields.  All of these fields are contaminants in the sense that all of the
; ; contaminants of a poly contaminate any result formed from that poly.  The
; ; same is true with the second answer of rewrite.

; ; If we represented the 5-tuple of the ttree of a poly as full-fledged fields
; ; in the poly the best we could do is to use a balanced binary tree with 8
; ; tips.  In that case the average time to change some field (including the
; ; time to cons a new element onto any of the 5 contaminants) is 3.62 conses.
; ; But if we clump all the contaminants into a single field represented as a
; ; tag-tree, the cost of adding a single element to any one of them is 2
; ; conses and the average cost of changing any of the 4 fields in a poly is
; ; 2.5 conses.  Furthermore, we can effectively union all 5 contaminants of
; ; two different polys in one cons!

(deflabel ttree
  :doc
  ":Doc-Section Miscellaneous

  tag-trees~/

  Many low-level ACL2 functions take and return ``tag trees'' or
  ``ttrees'' (pronounced ``tee-trees'') which contain various useful bits of
  information such as the lemmas used, the linearize assumptions made, etc.~/

  Abstractly a tag-tree represents a list of sets, each member set having a
  name given by one of the ``tags'' (which are symbols) of the ttree.  The
  elements of the set named ~c[tag] are all of the objects tagged ~c[tag] in
  the tree.  You are invited to browse the source code.  Definitions of
  primitives are labeled with the comment ``; Note: Tag-tree primitive''.

  The rewriter, for example, takes a term and a ttree (among other things), and
  returns a new term, term', and new ttree, ttree'.  Term' is equivalent to
  term (under the current assumptions) and the ttree' is an extension of ttree.
  If we focus just on the set associated with the tag ~c[LEMMA] in the ttrees,
  then the set for ttree' is the extension of that for ttree obtained by
  unioning into it all the ~il[rune]s used by the rewrite.  The set associated
  with ~c[LEMMA] can be obtained by ~c[(tagged-objects 'LEMMA ttree)].")

; The following function determines whether val with tag tag occurs in
; tree:

(defun tag-tree-occur (tag val ttree)

; Note: Tag-tree primitive

  (let ((pair (assoc-eq tag ttree)))
    (and pair ; optimization
         (member-equal val (cdr pair)))))

(defun remove-tag-from-tag-tree (tag ttree)

; Note: Tag-tree primitive

; In this function we do not assume that tag is a key of ttree.  See also
; remove-tag-from-tag-tree, which does make that assumption.

  (cond ((assoc-eq tag ttree)
         (delete-assoc-eq tag ttree))
        (t ttree)))

(defun remove-tag-from-tag-tree! (tag ttree)

; Note: Tag-tree primitive

; In this function we assume that tag is a key of ttree.  See also
; remove-tag-from-tag-tree, which does not make that assumption.

  (delete-assoc-eq tag ttree))

; To add a tagged object to a tree we use the following function.  Observe
; that it does nothing if the object is already present.

; Note:
; If you add a new tag, be sure to include it in all-runes-in-ttree!

(defmacro extend-tag-tree (tag vals ttree)

; Note: Tag-tree primitive

; Warning: We assume that tag is not a key of ttree and vals is not nil.

  `(acons ,tag ,vals ,ttree))

(defun add-to-tag-tree (tag val ttree)

; Note: Tag-tree primitive

; See also add-to-tag-tree!, for the case that tag is known not to be a key of
; ttree.

  (cond
   ((eq ttree nil) ; optimization
    (list (list tag val)))
   (t
    (let ((pair (assoc-eq tag ttree)))
      (cond (pair (cond ((member-equal val (cdr pair))
                         ttree)
                        (t (acons tag
                                  (cons val (cdr pair))
                                  (remove-tag-from-tag-tree! tag ttree)))))
            (t (acons tag (list val) ttree)))))))

(defun add-to-tag-tree! (tag val ttree)

; Note: Tag-tree primitive

; It is legal (and more efficient) to use this instead of add-to-tag-tree if we
; know that tag is not a key of ttree.

  (extend-tag-tree tag (list val) ttree))

; A Little Foreshadowing:

; We will soon introduce the notion of a "rune" or "rule name."  To
; each rune there corresponds a numeric equivalent, or "nume," which
; is the index into the "enabled structure" for the named rule.  We
; push runes into ttrees under the 'lemma property to record their
; use.

; We have occasion for "fake-runes" which look like runes but are not.
; See the Essay on Fake-Runes below.  One such rune is shown below,
; and is the name of otherwise anonymous rules that are always considered
; enabled.  When this rune is used, its use is not recorded in the
; tag-tree.

(defconst *fake-rune-for-anonymous-enabled-rule*
  '(:FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE nil))

(defabbrev push-lemma (rune ttree)

; This is just (add-to-tag-tree 'lemma rune ttree) and is named in honor of the
; corresponding act in Nqthm.  We do not record uses of the fake rune.  Rather
; than pay the price of recognizing the *fake-rune-for-anonymous-enabled-rule*
; perfectly we exploit the fact that no true rune has
; :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE as its token.

  (cond ((eq (car rune) :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE) ttree)
        (t (add-to-tag-tree 'lemma rune ttree))))

; Historical Note from the days when tag-trees were constructed using (acons
; tag value ttree) and (cons-tag-trees ttree1 ttree2):

; ; To join two trees we use cons-tag-trees.  Observe that if the first tree is
; ; nil we return the second (we can't cons a nil tag-tree on and their union
; ; is the second anyway).  Otherwise we cons, possibly duplicating elements.

; ; But starting in Version_3.2, we keep tagged objects unique in tag-trees, by
; ; calling scons-tag-trees when necessary, unioning the tag-trees rather than
; ; merely consing them.  The immediate prompt for this change was a report
; ; from Eric Smith on getting stack overflows from tag-tree-occur, but this
; ; problem has also occurred in the past (as best Matt can recall).

(defun delete-assoc-eq-assoc-eq-1 (alist1 alist2)
  (declare (xargs :guard (and (symbol-alistp alist1)
                              (symbol-alistp alist2))))
  (cond ((endp alist2)
         (mv nil nil))
        (t (mv-let (changedp x)
                   (delete-assoc-eq-assoc-eq-1 alist1 (cdr alist2))
                   (cond ((assoc-eq (caar alist2) alist1)
                          (mv t x))
                         (changedp
                          (mv t (cons (car alist2) x)))
                         (t (mv nil alist2)))))))

(defun delete-assoc-eq-assoc-eq (alist1 alist2)
  (mv-let (changedp x)
          (delete-assoc-eq-assoc-eq-1 alist1 alist2)
          (declare (ignore changedp))
          x))

(defun cons-tag-trees1 (ttree1 ttree2 ttree3)

; Note: Tag-tree primitive supporter

; Accumulate into ttree3, whose keys are disjoint from those of ttree1, the
; values of keys in ttree1 each augmented by their values in ttree2.

; It might be more efficient to accumulate into ttree3, so that this function
; is tail-recursive.  But we prefer that the tags at the front of ttree1 are
; also at the front of the returned ttree, since presumably the values of those
; tags are more likely to be updated frequently, and an update generates fewer
; conses the closer the tag is to the front of the ttree.

  (cond ((endp ttree1) ttree3)
        (t (let ((pair (assoc-eq (caar ttree1) ttree2)))
             (cond (pair (acons (caar ttree1)
                                (union-equal (cdar ttree1) (cdr pair))
                                (cons-tag-trees1 (cdr ttree1) ttree2 ttree3)))
                   (t (cons (car ttree1)
                            (cons-tag-trees1 (cdr ttree1) ttree2 ttree3))))))))

(defun cons-tag-trees (ttree1 ttree2)

; Note: Tag-tree primitive

; We return a tag-tree whose set of keys is the union of the keys of ttree1 and
; ttree2, and whose value for each key is the union of the values of the key in
; ttree1 and ttree2 (in that order).  In addition, we attempt to avoid needless
; consing.

  (cond ((null ttree1) ttree2)
        ((null ttree2) ttree1)
        ((null (cdr ttree2))
         (let* ((pair2 (car ttree2))
                (tag (car pair2))
                (pair1 (assoc-eq tag ttree1)))
           (cond (pair1 (acons tag
                               (union-equal (cdr pair1) (cdr pair2))
                               (delete-assoc-eq tag ttree1)))
                 (t (cons pair2 ttree1)))))
        (t (let ((ttree3 (delete-assoc-eq-assoc-eq ttree1 ttree2)))
             (cons-tag-trees1 ttree1 ttree2 ttree3)))))

(defmacro tagged-objects (tag ttree)

; Note: Tag-tree primitive

; See also tagged-objectsp for a corresponding predicate.

  `(cdr (assoc-eq ,tag ,ttree)))

(defmacro tagged-objectsp (tag ttree)

; Note: Tag-tree primitive

; This is used instead of tagged-objects (but is Boolean equivalent to it) when
; we want to emphasize that our only concern is whether or not there is at
; least one tagged object associated with tag in ttree.

  `(assoc-eq ,tag ,ttree))

(defun tagged-object (tag ttree)

; Note: Tag-tree primitive

; This function returns obj for the unique obj associated with tag in ttree, or
; nil if there is no object with that tag.  If there may be more than one
; object associated with tag in ttree, use (car (tagged-objects tag ttree))
; instead to obtain one such object, or use (tagged-objectsp tag ttree) if you
; only want to answer the question "Is there any object associated with tag in
; ttree?".

  (let ((objects (tagged-objects tag ttree)))
    (and objects
         (assert$ (null (cdr objects))
                  (car objects)))))

; We accumulate our ttree into the state global 'accumulated-ttree so that if a
; proof attempt is aborted, we can still recover the lemmas used within it.  If
; we know a ttree is going to be part of the ttree returned by a successful
; event, then we want to store it in state.  We are especially concerned about
; storing a ttree if we are about to inform the user, via output, that the
; runes in it have been used.  (That is, we want to make sure that if a proof
; fails after the system has reported using some rune then that rune is tagged
; as a 'lemma in the 'accumulated-ttree of the final state.)  This encourages
; us to cons a new ttree into the accumulator every time we do output.

(deflock *ttree-lock*)

(defun@par accumulate-ttree-and-step-limit-into-state (ttree step-limit state)

; We add ttree to the 'accumulated-ttree in state and return an error triple
; whose value is ttree.  Before Version_3.2 we handled tag-trees a bit
; differently, allowing duplicates and using special markers for portions that
; had already been accumulated into state.  Now we keep tag-trees
; duplicate-free and avoid adding such markers to the returned value.

; We similarly save the given step-limit in state, unless its value is :skip.

  (declare (ignorable state))
  (pprogn@par
   (cond ((eq step-limit :skip) (state-mac@par))
         (t

; Parallelism no-fix: the following call of (f-put-global@par 'last-step-limit
; ...) may be overridden by another similar call performed by a concurrent
; thread.  But we can live with that because step-limits do not affect
; soundness.

          (f-put-global@par 'last-step-limit step-limit state)))
   (cond
    ((eq ttree nil) (value@par nil))
    (t (pprogn@par
        (with-ttree-lock

; In general, it is dangerous to set the same state global in two different
; threads, because the first setting is blown away by the second.  But here, we
; are _accumulating_ into a state global (namely, 'accumulated-ttree), and we
; don't care about the order in which the accumulation occurs (even though such
; nondeterminism isn't explained logically -- after all, we are modifying state
; without passing it in, so we already are punting on providing a logical story
; here).  Our only concern is that two such accumulations interfere with each
; other, but the lock just above takes care of that (i.e., provides mutual
; exclusion).

         (f-put-global@par 'accumulated-ttree
                           (cons-tag-trees ttree
                                           (f-get-global 'accumulated-ttree
                                                         state))
                           state))
        (value@par ttree))))))

(defun pts-to-ttree-lst (pts)
  (cond ((null pts) nil)
        (t (cons (add-to-tag-tree! 'pt (car pts) nil)
                 (pts-to-ttree-lst (cdr pts))))))

; Previously, we stored the parents of a poly in the poly's :ttree field
; and used to-be-ignoredp.  However, tests have shown that under certain
; conditions to-be-ignoredp was taking up to 80% of the time spent by
; add-poly.  We now store the poly's parents in a seperate field and
; use ignore-polyp.  The next few functions are used in the implementation
; of this change.

(defun marry-parents (parents1 parents2)

; We return the 'eql union of the two arguments.  When we create a
; new poly from two other polys via cancellation, we need to ensure
; that the new poly depends on all the literals that either of the
; others do.

  (if (null parents1)
      parents2
    (marry-parents (cdr parents1)
                   (add-to-set-eql (car parents1) parents2))))

(defun collect-parents1 (pt ans)
  (cond ((null pt)
         ans)
        ((consp pt)
         (collect-parents1 (car pt)
                           (collect-parents1 (cdr pt) ans)))
        (t
         (add-to-set-eql pt ans))))

(defun collect-parents0 (pts ans)
  (cond
   ((null pts) ans)
   (t
    (collect-parents0 (cdr pts)
                      (collect-parents1 (car pts) ans)))))

(defun collect-parents (ttree)

; We accumulate in reverse order all the objects (parents) in the pts in the
; ttree.  When we create a new poly via linearize, we extract a list of all its
; parents from the poly's 'ttree and store this list in the poly's 'parents
; field.  This function does the extracting.

  (collect-parents0 (tagged-objects 'pt ttree) nil))

(defun ignore-polyp (parents pt)

; Consider the set, P, of all parents mentioned in the list parents.
; Consider the set, B, of all parents mentioned in the parent tree pt.  We
; return t iff P and B have a non-empty intersection.  From a more applied
; perspective, assuming parents is the parents list associated with some
; poly, P is the set of literals upon which the poly depends.  B is
; generally the set of literals we are to avoid dependence upon.  The poly
; should be ignored if it depends on some literal we are to avoid.

  (if (null parents)
      nil
    (or (pt-occur (car parents) pt)
        (ignore-polyp (cdr parents) pt))))

(defun to-be-ignoredp1 (pts pt)
  (cond ((endp pts) nil)
        (t (or (pt-intersectp (car pts) pt)
               (to-be-ignoredp1 (cdr pts) pt)))))

(defun to-be-ignoredp (ttree pt)

; Consider the set, P, of all parents mentioned in the 'pt tags of ttree.
; Consider the set, B, of all parents mentioned in the parent tree pt.  We
; return t iff P and B have a non-empty intersection.  From a more applied
; perspective, assuming ttree is the tree associated with some poly, P is the
; set of literals upon which the poly depends.  B is generally the set of
; literals we are to avoid dependence upon.  The poly should be ignored if it
; depends on some literal we are to avoid.

; This function was originally written to do the job described above.  But then
; Robert Krug suggested the efficiency of maintaining the parents list and
; introduced ignore-polyp.  Now this function is only used elsewhere, but the
; above comments still apply mutatis mutandis.

  (to-be-ignoredp1 (tagged-objects 'pt ttree) pt))


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


; Assumptions

; We are prepared to force assumptions of certain terms by adding
; them to the tag-tree under the 'assumption tag.  This is always done
; via force-assumption.  All assumptions are embedded in an
; assumption record:

(defrec assumnote (cl-id rune . target) t)

; The cl-id is the clause id (as maintained by the waterfall) of the clause
; currently being worked upon.  Rune is either the rune (or a symbol, as per
; force-assumption) that forced this assumption.  Target is the term to which
; rune was being applied.  Because the :assumnotes field of an assumption is
; always non-nil, there is at least one assumnote in it, but the cl-id field in
; that assumnote might be nil because we do not know the clause id just yet.
; We fill in the :cl-id field later so that we don't have to pass such static
; information all the way down to the places where assumptions are forced.
; When an assumption is generated, it has exactly one assumnote.  But later we
; will "merge" assumptions together (actually, delete some via subsumption) and
; when we do we will union the assumnotes together to keep track of why we are
; dealing with that assumption.

(defrec assumption
  ((type-alist . term) immediatep rewrittenp . assumnotes)
  t)

; An assumption record records the fact that we must prove term under
; the assumption of type-alist.  Immediatep indicates whether it is
; the user's desire to split the main goal on term immediately
; (immediatep = 'case-split), prove the term under alist immediately
; (t) or delay the proof to a forcing round (nil).

; WARNING: The system can be unsound if immediatep takes on any but
; these three values.  In functions like collect-assumptions we assume
; that collecting all the 'case-splits and then collecting all the t's
; gets all the non-nils!

; Assumnotes is involved with explaining to the user what we are doing.  It is
; a non-empty list of assumnote records.

; We now turn to the question of whether term has been rewritten or not.  If it
; has not been, and we know the context in which rewriting should be tried, it
; is presumably a good idea to try to rewrite term before we try a full-fledged
; proof: a proof requires converting the type-alist and term into a clause and
; then simplifying all the literals of that clause, whereas we expect many
; times that the type-alist will allow term to rewrite to t.  One might ask why
; we don't always rewrite before forcing.  The answer is simple: type-set
; forces and cannot use the rewriter because it is defined well before the
; rewriter.  So type-set forces unrewritten terms often.  The problem with the
; simple idea of trying first to prove those terms by rewriting is that REWRITE
; takes many additional context-specifying arguments, the most complicated
; being the simplify-clause-pot-lst.  Having set the stage for an explanation,
; we now give it:

; Rewrittenp indicates whether we have already tried to rewrite term.  Recall
; that relieve-hyp first rewrites and forces the rewritten term only if
; rewriting fails.  Thus, at least within the rewriter, we will see both
; rewritten and unrewritten assumptions coming back in the ttrees we generate.
; Rewrittenp is either a term or nil.  If it is a term, forced-term, then it is
; the term we were asked to force and term is the result of rewriting
; forced-term.  We use the unrewritten term in a heuristic that sometimes
; throws out supposedly irrelevant hypotheses from the clauses we ultimately
; prove to establish the assumptions.  See the discussion of "disguarding."  If
; rewrittenp is nil, we have not yet tried to rewrite term and term is
; literally what was forced.  The simplifier will collect the unrewritten
; assumptions generated during rewrite and will rewrite them in the
; "appropriate context" as discussed below.

; The view we take is that from within the rewriter, all assumptions are
; rewritten before being forced.  That cannot be implemented directly, so
; we do it cleverly, by rewriting them after the force but not telling
; the user.  It just seems like a good idea for the rewriter, of all the
; processes, to produce only rewritten assumptions.  Now those rewritten
; assumptions aren't maximally rewritten.  For example, an assumption
; might rewrite to an if and normalization etc. might produce a provable
; set of assumptions.  But we do not use normalization or clausification on
; assumptions until it is time to hit them with the full prover.

; The following record definition is decidedly out of place, belonging as it
; does to the code for forward-chaining.  But we must make it now to allow
; us to define contain-assumptionp.  This record is documented in comments
; in the essay entitled:  "Forward Chaining Derivations - fc-derivation - fcd"

(defrec fc-derivation
  (((concl . ttree) . (fn-cnt . p-fn-cnt))
   .
   ((inst-trigger . rune) . (fc-round . unify-subst)))
  t)

; WARNING: If you change fc-derivation, go visit the "virtual" declaration of
; the record in simplify.lisp and update the comments.  See the essay "Forward
; Chaining Derivations - fc-derivation - fcd".

(mutual-recursion

(defun contains-assumptionp (ttree)

; We return t iff ttree contains an assumption "at some level" where we
; know that 'fc-derivations contain ttrees that may contain assumptions.
; See the discussion in force-assumption.

  (or (tagged-objectsp 'assumption ttree)
      (contains-assumptionp-fc-derivations
       (tagged-objects 'fc-derivation ttree))))

(defun contains-assumptionp-fc-derivations (lst)
  (cond ((endp lst) nil)
        (t (or (contains-assumptionp (access fc-derivation (car lst) :ttree))
               (contains-assumptionp-fc-derivations (cdr lst))))))
)

(defun remove-assumption-entries-from-type-alist (type-alist)

; We delete from type-alist any entry, (term ts . ttree), whose ttree contains
; an assumption.  Thus, if ttree2 below is the
; only one of the three to contain an assumption, the type-alist
; ((v1 ts1 . ttree1)(v2 ts2 . ttree2)(v3 ts3 . ttree3))
; is transformed into
; ((v1 ts1 . ttree1)(v3 ts3 . ttree3)).

; It is always sound to delete a hypothesis.  See the discussion in
; force-assumption.

  (cond
   ((endp type-alist) nil)
   ((contains-assumptionp (cddar type-alist))
    (remove-assumption-entries-from-type-alist (cdr type-alist)))
   (t (cons (car type-alist)
            (remove-assumption-entries-from-type-alist (cdr type-alist))))))

(defun force-assumption1
  (rune target term type-alist rewrittenp immediatep ttree)

  (let* ((term (cond ((equal term *nil*)
                      (er hard 'force-assumption
                          "Attempt to force nil!"))
                     ((null rune)
                      (er hard 'force-assumption
                          "Attempt to force the nil rune!"))
                     (t term))))
    (cond ((not (member-eq immediatep '(t nil case-split)))
           (er hard 'force-assumption1
               "The :immediatep of an ASSUMPTION record must be ~
                t, nil, or 'case-split, but we have tried to create ~
                one with ~x0."
               immediatep))
          (t
           (add-to-tag-tree 'assumption
                            (make assumption
                                  :type-alist type-alist
                                  :term term
                                  :rewrittenp rewrittenp
                                  :immediatep immediatep
                                  :assumnotes
                                  (list (make assumnote
                                              :cl-id nil
                                              :rune rune
                                              :target target)))
                            ttree)))))

(defun dumb-occur-in-type-alist (var type-alist)
  (cond
   ((null type-alist)
    nil)
   ((dumb-occur var (caar type-alist))
    t)
   (t
    (dumb-occur-in-type-alist var (cdr type-alist)))))

(defun all-dumb-occur-in-type-alist (vars type-alist)
  (cond
   ((null vars)
    t)
   (t (and (dumb-occur-in-type-alist (car vars) type-alist)
           (all-dumb-occur-in-type-alist (cdr vars) type-alist)))))

(defun force-assumption
  (rune target term type-alist rewrittenp immediatep force-flg ttree)

; Warning:  Rune may not be a rune!  It may be a function symbol.

; This function adds (implies type-alist' term) as an 'assumption to ttree.
; Rewrittenp is either nil, meaning term has not yet been rewritten, or is the
; term that was rewritten to obtain term.  Rune is the name of the rule in
; whose behalf term is being assumed, and rune is being applied to the target
; term target.  If rune is a symbol then it is actually a primitive
; function symbol and this is a split on the guard of that symbol.  There is
; even an exception to that: sometimes rune is the function symbol equal.  But
; the guard of equal is t and so is never forced!  What is going on?  In
; linearize we force term2 to be real if term1 is real and we are
; linearizing (equal term1 term2).

; The type-alist actually stored in the assumption record, type-alist', is not
; type-alist!  We remove from type-alist all the entries depending upon
; assumptions.  It is legitimate to throw away any hypothesis, thus we can
; delete the entries we choose.  Why do we throw out the type-alist entries
; depending on assumptions?  The reason is that in the forcing round we
; actually generate a formula representing (implies type-alist' term) and this
; formula does not encode the fact that a given hyp depends upon certain
; assumptions.

; Because assumptions can be generated during forward chaining, the type-alist
; may contain 'fc-derivations tags among its ttrees.  These records record how
; a given hypothesis was derived and may itself have 'assumptions in its ttree.
; We therefore consider a ttree to "contain assumptions" if it contains an
; fc-derivation that contains assumptions.

; It could be thought that the creation of type-alist' from type-alist is
; merely an efficiency aimed at saving a few conses.  This is not correct.
; This change has a dramatic effect on the size of our ttrees.  Before we did
; this, it was possible for a ttree to contain an assumption which (by virtue
; of the :type-alist) contained a ttree which contained an assumption which
; contained a ttree, etc.  We have seen this sort of thing nested to depth 9.
; Furthermore, it was frequently the case that a ttree contained some proper
; subttree x which occurred also in an assumption contained in the parent
; ttree.  Thus, the ttree x was duplicated.  While the parent ttree was small
; (in the sense that it contained on a few nodes) the tree was very large when
; printed, because of this duplication.  We have seen a ttree that contained 5
; million nodes (when explored in this root-and-branch way through 'assumptions
; and 'fc-derivations) but which actually was composed of only 100 distinct
; (non-equal) subtrees.  Again, one might think this was a problem only if one
; printed out the ttree, but some processes, such as expunge-fc-derivations, do
; root-and-branch exploration.  On the tree in question the system simply hung
; up and appeared to be in an infinite loop.  This fix keeps ttrees small (even
; when viewed in the root-and-branch way) and is crucial to our practice of
; using them.

; Once upon a time, we allowed rune to be nil.  We have since changed that and
; now use the *fake-rune-for-anonymous-enabled-rule* when we don't know a
; better rune.  But we have put a check in here to make sure no one uses the
; nil "rune" anymore.  Wanting a genuine rune here is just a reflection of the
; output routine that explains the origins of each forcing round.

; Force-flg is known to be non-nil; it may be either t or 'weak.  It's tempting
; to allow force-flg = nil and handle that case here (trivially), but the case
; structure in functions like type-set-binary-+ suggests that it's better to
; deal with that case up front, in order to avoid lots of tests that are
; irrelevant (since the same trivial thing happens in all cases when force-flg
; is nil).

; This function is a No-Change Loser, meaning that if it fails and returns nil
; as its first result, it returns the unmodified ttree as its second.  Note
; that either force-flg or nil is returned as the first argument; hence, a
; "successful" force with force-flg = 'weak will result in an unchanged
; force-flg being returned.  If the first value returned is nil, we are to
; pretend that we weren't allowed to force in the first place.

; At the time of this writing we have temporarily abandoned the idea of
; allowing force-flg to be 'weak:  it will always be t or nil.  See the comment
; in ok-to-force.

  (let ((type-alist (remove-assumption-entries-from-type-alist type-alist)))
    (cond
     ((not force-flg)
      (mv force-flg
          (er hard 'force-assumption
              "Force-assumption called with null force-flg!")))

; We experimented with allowing force-flg to be 'weak.  However, currently
; force-flg is known to be t or nil.  See the comment in ok-to-force.

;    ((or (eq force-flg t)
;         (all-dumb-occur-in-type-alist (all-vars term) type-alist))
;     (mv force-flg
;         (force-assumption1
;          rune target term type-alist rewrittenp immediatep ttree)))
;    (t
;     (mv nil ttree))

     (t (mv force-flg
            (force-assumption1
             rune target term type-alist rewrittenp immediatep ttree))))))

(defun tag-tree-occur-assumption-nil-1 (lst)
  (cond ((endp lst) nil)
        ((equal (access assumption (car lst) :term)
                *nil*)
         t)
        (t (tag-tree-occur-assumption-nil-1 (cdr lst)))))

(defun tag-tree-occur-assumption-nil (ttree)

; This is just (tag-tree-occur 'assumption <*nil*> ttree) where by <*nil*> we
; mean any assumption record with :term *nil*.

  (tag-tree-occur-assumption-nil-1 (tagged-objects 'assumption ttree)))

(defun assumption-free-ttreep (ttree)

; This is a predicate that returns t if ttree contains no 'assumption tag.  It
; also checks for 'fc-derivation tags, since they could hide 'assumptions.  An
; error-causing version of this function is chk-assumption-free-ttree.  Keep
; these two in sync.

; This check is stronger than necessary, of course, since an fc-derivation
; object need not contain an assumption.  See also contains-assumptionp (and
; chk-assumption-free-ttree-1) for a slightly more expensive, but more precise,
; check.

  (cond ((tagged-objectsp 'assumption ttree) nil)
        ((tagged-objectsp 'fc-derivation ttree) nil)
        (t t)))

; The following assumption is impossible to satisfy and is used as a marker
; that we sometimes put into a ttree to indicate to our caller that the
; attempted force should be abandoned.

(defconst *impossible-assumption*
  (make assumption
        :type-alist nil
        :term *nil*
        :rewrittenp *nil*
        :immediatep nil ; must be t, nil, or 'case-split
        :assumnotes (list (make assumnote
                                :cl-id nil
                                :rune *fake-rune-for-anonymous-enabled-rule*
                                :target *nil*))))


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


; We are about to get into the linear arithmetic stuff quite heavily.
; This code started in Nqthm in 1979 and migrated more or less
; untouched into ACL2, with the exception of the addition of the
; rationals.  However, around 1998, Robert Krug began working on an
; improved arithmetic book and after a year or so realized he wanted
; to make serious changes in the linear arithmetic procedures.
; Robert's hand is now felt all over this code.


; Essay on the Logical Basis for Linear Arithmetic.

; This essay was written for some early version of ACL2.  It still
; applies to the linear arithmetic decision procedure as of Version_2.7,
; although some of the details may need revision.

; We list here the "algebraic laws" we assume.  We point back to this
; list from the places we assume them.  It is crucial to realize that
; by < and + here we do not mean the familiar "guarded" functions of
; Common Lisp and algebra, but rather the "completed" functions of the
; ACL2 logic.  In particular, nonnumeric arguments to + are defaulted
; to 0 and complex numbers may be added to rational ones to yield
; complex ones, etc.  The < relation coerces nonnumeric arguments to 0
; and then compares the resulting numbers lexicographically on the
; real and imaginary parts, using the familiar less-than relation on
; the rationals.

; Let us use << as the "familiar" less-than.  Then
; (< x y) = (let ((x1 (if (acl2-numberp x) x 0))
;                 (y1 (if (acl2-numberp y) y 0)))
;            (or (<< (realpart x1) (realpart y1))
;                (and (= (realpart x1) (realpart y1))
;                     (<< (imagpart x1) (imagpart y1)))))

; The wonderful thing about this definition, is that it enjoys the algebraic
; laws we need to support linear arithmetic.  The "box" below contains the
; complete listing of the algegraic laws supporting linear arithmetic
; ("alsla").

; However, interspersed around them in the box are some events that ACL2's
; completed < and + have the ALSLA properties.  To enable us to use the theorem
; prover, we define some new symbols like < and + and prove that those symbols
; have the desired properties.  This is a bit tricky because the completed <
; and + must be defined in terms of the partial < and + which work on the
; rationals and complexes, respectively, and we do not want to rely on any
; built in properties of those primitive symbols.

; Therefore, we constrain three new symbols, PLUS, TIMES, and LESSP which you
; may think of as being the familiar, partial versions of +, *, and <.
; (Indeed, the witnesses in the constraints are those primitives.  The
; encapsulate below merely exports the properties that we are going to assume.)
; Then we define completed versions of these functions, called CPLUS, CTIMES,
; and CLESSP and we prove the ALSLA properties of those functions.

; Note: This exercise is still suspicious because it involves equality
; goals between arithmetic terms and there is no reason to believe that our
; "untrusted" linear arithmetic isn't contributing to their proof.  Well, a
; search through the output produces no sign of "linear" after the
; encapsulation below, but that could indicate an io bug.  A more convincing
; proof would be to eliminate the use of the arithmetic data types altogether
; but that would be a little nasty, faking rationals and complexes.  A still
; more convincing proof would be to construct the proof formally, as we hope to
; do when we have proof objects.

; (progn
;
; ; Perhaps this axiom can be proved from given ones, but I haven't taken the
; ; time to work it out.  I will add it.  I believe it!
;
; (defaxiom *-preserves-<
;   (implies (and (rationalp c)
;                 (rationalp x)
;                 (rationalp y)
;                 (< 0 c))
;            (equal (< (* c x) (* c y))
;                   (< x y))))
;
; (defthm realpart-rational
;   (implies (rationalp x) (equal (realpart x) x)))
;
; (defthm imagpart-rational
;   (implies (rationalp x) (equal (imagpart x) 0)))
;
; (encapsulate (((plus * *) => *)
;               ((times * *) => *)
;               ((lessp * *) => *))
;
; ; Plus and lessp here are the rational versions of those functions.  They are
; ; intended to be the believable, intuitive, functions.  You should read the
; ; properties we export to make sure you believe that the high school plus and
; ; lessp have those properties.  We prove the properties, but we prove them from
; ; witnesses of plus and lessp that are ACL2's completed + and < supported by
; ; ACL2's linear arithmetic and hence, if the soundness of ACL2's arithmetic is
; ; in doubt, as it is in this exercise, then no assurrance can be drawn from the
; ; constructive nature of this axiomatization of rational arithmetic.
;
;              (local (defun plus (x y)
;                       (declare (xargs :verify-guards nil))
;                       (+ x y)))
;              (local (defun times (x y)
;                       (declare (xargs :verify-guards nil))
;                       (* x y)))
;              (local (defun lessp (x y)
;                       (declare (xargs :verify-guards nil))
;                       (< x y)))
;              (defthm rationalp-plus
;                (implies (and (rationalp x)
;                              (rationalp y))
;                         (rationalp (plus x y)))
;                :rule-classes (:rewrite :type-prescription))
;              (defthm plus-0
;                (implies (rationalp x)
;                         (equal (plus 0 x) x)))
;              (defthm plus-commutative-and-associative
;                (and (implies (and (rationalp x)
;                                   (rationalp y))
;                              (equal (plus x y) (plus y x)))
;                     (implies (and (rationalp x)
;                                   (rationalp y)
;                                   (rationalp z))
;                              (equal (plus x (plus y z))
;                                     (plus y (plus x z))))
;                     (implies (and (rationalp x)
;                                   (rationalp y)
;                                   (rationalp z))
;                              (equal (plus (plus x y) z)
;                                     (plus x (plus y z))))))
;              (defthm rationalp-times
;                (implies (and (rationalp x)
;                              (rationalp y))
;                         (rationalp (times x y))))
;              (defthm times-commutative-and-associative
;                (and (implies (and (rationalp x)
;                                   (rationalp y))
;                              (equal (times x y) (times y x)))
;                     (implies (and (rationalp x)
;                                   (rationalp y)
;                                   (rationalp z))
;                              (equal (times x (times y z))
;                                     (times y (times x z))))
;                     (implies (and (rationalp x)
;                                   (rationalp y)
;                                   (rationalp z))
;                              (equal (times (times x y) z)
;                                     (times x (times y z)))))
;                :hints
;                (("Subgoal 2"
;                  :use ((:instance associativity-of-*)
;                        (:instance commutativity-of-* (x x)(y (* y z)))))))
;              (defthm times-distributivity
;                (implies (and (rationalp x)
;                              (rationalp y)
;                              (rationalp z))
;                         (equal (times x (plus y z))
;                                (plus (times x y) (times x z)))))
;              (defthm times-0
;                (implies (rationalp x)
;                         (equal (times 0 x) 0)))
;              (defthm times-1
;                (implies (rationalp x)
;                         (equal (times 1 x) x)))
;              (defthm plus-inverse
;                (implies (rationalp x)
;                         (equal (plus x (times -1 x)) 0))
;                :hints
;                (("Goal"
;                  :use ((:theorem (implies (rationalp x)
;                                           (not (< 0 (+ x (* -1 x))))))
;                        (:theorem (implies (rationalp x)
;                                           (not (< (+ x (* -1 x)) 0))))))))
;              (defthm plus-inverse-unique
;                (implies (and (rationalp x)
;                              (rationalp y)
;                              (equal (plus x (times -1 y)) 0))
;                         (equal x y))
;                :rule-classes nil)
;              (defthm lessp-irreflexivity
;                (implies (rationalp x)
;                         (not (lessp x x))))
;              (defthm lessp-antisymmetry
;                (implies (and (rationalp x)
;                              (rationalp y)
;                              (lessp x y))
;                         (not (lessp y x))))
;              (defthm lessp-trichotomy
;                (implies (and (rationalp x)
;                              (rationalp y)
;                              (not (equal x y))
;                              (not (lessp x y)))
;                         (lessp y x)))
;              (defthm lessp-plus
;                (implies (and (rationalp x)
;                              (rationalp y)
;                              (rationalp u)
;                              (rationalp v)
;                              (lessp x y)
;                              (not (lessp v u)))
;                         (lessp (plus x u) (plus y v))))
;              (defthm not-lessp-plus
;                (implies (and (rationalp x)
;                              (rationalp y)
;                              (rationalp u)
;                              (rationalp v)
;                              (not (lessp y x))
;                              (not (lessp v u)))
;                         (not (lessp (plus y v) (plus x u)))))
;              (defthm 1+trick-for-lessp
;                (implies (and (integerp x)
;                              (integerp y)
;                              (lessp x y))
;                         (not (lessp y (plus 1 x)))))
;              (defthm times-positive-preserves-lessp
;                (implies (and (rationalp c)
;                              (rationalp x)
;                              (rationalp y)
;                              (lessp 0 c))
;                         (equal (lessp (times c x) (times c y))
;                                (lessp x y)))))
;
; ; Now we "complete" +, *, <, and <= to the complex rationals and thence to the
; ; entire universe.  The results are CPLUS, CTIMES, CLESSP, and CLESSEQP.  You
; ; should buy into the claim that these functions are what we intended in ACL2's
; ; completed arithmetic.
;
; ; Note: At first sight it seems odd to do it this way.  Why not just assume
; ; plus, above, is the familiar operation on the complex rationals?  We tried
; ; it and it didn't work very well, because ACL2 does not reason very well
; ; about complex arithmetic.  It seemed more direct to make the definition of
; ; complex addition and multiplication be explicit for the purposes of this
; ; proof.
;
; (defun cplus (x y)
;   (declare (xargs :verify-guards nil))
;   (let ((x1 (fix x))
;         (y1 (fix y)))
;     (complex (plus (realpart x1) (realpart y1))
;              (plus (imagpart x1) (imagpart y1)))))
;
; (defun ctimes (x y)
;   (declare (xargs :verify-guards nil))
;   (let ((x1 (fix x))
;         (y1 (fix y)))
;     (complex (plus (times (realpart x1) (realpart y1))
;                    (times -1 (times (imagpart x1) (imagpart y1))))
;              (plus (times (realpart x1) (imagpart y1))
;                    (times (imagpart x1) (realpart y1))))))
;
; (defun clessp (x y)
;   (declare (xargs :verify-guards nil))
;   (let ((x1 (fix x))
;         (y1 (fix y)))
;     (or (lessp (realpart x1) (realpart y1))
;         (and (equal (realpart x1) (realpart y1))
;              (lessp (imagpart x1) (imagpart y1))))))
;
; (defun clesseqp (x y)
;   (declare (xargs :verify-guards nil))
;   (not (clessp y x)))
;
; ; A trivial theorem about fix, allowing us hereafter to disable it.
;
; (defthm fix-id (implies (acl2-numberp x) (equal (fix x) x)))
;
; (in-theory (disable fix))
;
; ;-----------------------------------------------------------------------------
; ; The Algebraic Laws Supporting Linear Arithmetic (ALSLA)
;
; ; All the operators FIX their arguments
; ; (equal (+ x y) (+ (fix x) (fix y)))
; ; (equal (* x y) (* (fix x) (fix y)))
; ; (equal (< x y) (< (fix x) (fix y)))
; ; (fix x) = (if (acl2-numberp x) x 0)
;
; (defthm operators-fix-their-arguments
;   (and (equal (cplus x y) (cplus (fix x) (fix y)))
;        (equal (ctimes x y) (ctimes (fix x) (fix y)))
;        (equal (clessp x y) (clessp (fix x) (fix y)))
;        (equal (fix x) (if (acl2-numberp x) x 0)))
;   :rule-classes nil
;   :hints (("Subgoal 1" :in-theory (enable fix))))
;
; ; + Associativity, Commutativity, and Zero
; ; (equal (+ (+ x y) z) (+ x (+ y z)))
; ; (equal (+ x y) (+ y x))
; ; (equal (+ 0 y) (fix y))
;
; (defthm cplus-associativity-etc
;   (and (equal (cplus (cplus x y) z) (cplus x (cplus y z)))
;        (equal (cplus x y) (cplus y x))
;        (equal (cplus 0 y) (fix y))))
;
; ; * Distributes Over +
; ; (equal (+ (* c x) (* d x)) (* (+ c d) x))
;
; (defthm ctimes-distributivity
;   (equal (cplus (ctimes c x) (ctimes d x)) (ctimes (cplus c d) x)))
;
; ; * Associativity, Commutativity, Zero and One
; ; (equal (* (* x y) z) (* x (* y z)))   ; See note below
; ; (equal (* x y) (* y x))
; ; (equal (* 0 x) 0)
; ; (equal (* 1 x) (fix x))
;
; (defthm ctimes-associativity-etc
;   (and (equal (ctimes (ctimes x y) z) (ctimes x (ctimes y z)))
;        (equal (ctimes x y) (ctimes y x))
;        (equal (ctimes 0 y) 0)
;        (equal (ctimes 1 x) (fix x))))
;
; ; + Inverse
; ; (equal (+ x (* -1 x)) 0)
;
; (defthm cplus-inverse
;   (equal (cplus x (ctimes -1 x)) 0))
;
; ; Reflexivity of <=
; ; (<= x x)
;
; (defthm clesseqp-reflexivity
;   (clesseqp x x))
;
; ; Antisymmetry
; ; (implies (< x y) (not (< y x)))   ; (implies (< x y) (<= x y))
;
; (defthm clessp-antisymmetry
;   (implies (clessp x y)
;            (not (clessp y x))))
;
; ; Trichotomy
; ; (implies (and (acl2-numberp x)
; ;               (acl2-numberp y))
; ;          (or (< x y)
; ;              (< y x)
; ;              (equal x y)))
;
; (defthm clessp-trichotomy
;   (implies (and (acl2-numberp x)
;                 (acl2-numberp y))
;            (or (clessp x y)
;                (clessp y x)
;                (equal x y)))
;   :rule-classes nil)
;
; ; Additive Properties of < and <=
; ; (implies (and (<  x y) (<= u v)) (<  (+ x u) (+ y v)))
; ; (implies (and (<= x y) (<= u v)) (<= (+ x u) (+ y v)))
;
; ; We have to prove three lemmas first.  But then we nail these suckers!
;
;  (defthm not-lessp-plus-instance-u=v
;    (implies (and (rationalp x)
;                  (rationalp y)
;                  (rationalp u)
;                  (not (lessp y x)))
;             (not (lessp (plus y u) (plus x u)))))
;
;  (defthm lessp-plus-commuted1
;    (implies (and (rationalp x)
;                  (rationalp y)
;                  (rationalp u)
;                  (rationalp v)
;                  (lessp x y)
;                  (not (lessp v u)))
;             (lessp (plus u x) (plus v y)))
;    :hints (("goal" :use (:instance lessp-plus))))
;
;  (defthm irreflexive-revisited-and-commuted
;    (implies (and (rationalp x)
;                  (rationalp y)
;                  (lessp y x))
;             (equal (equal x y) nil)))
;
; (defthm clessp-additive-properties
;   (and (implies (and (clessp x y)
;                      (clesseqp u v))
;                 (clessp (cplus x u) (cplus y v)))
;        (implies (and (clesseqp x y)
;                      (clesseqp u v))
;                 (clesseqp (cplus x u) (cplus y v)))))
;
; ; The 1+ Trick
; ; (implies (and (integerp x)
; ;               (integerp y)
; ;               (< x y))
; ;          (<= (+ 1 x) y))
;
; (defthm cplus-1-trick
;   (implies (and (integerp x)
;                 (integerp y)
;                 (clessp x y))
;            (clesseqp (cplus 1 x) y)))
;
; ; Cross-Multiplying Allows Cancellation
; ; (implies (and (< c1 0)
; ;               (< 0 c2))
; ;          (equal (+ (* c1 (abs c2)) (* c2 (abs c1))) 0))
;
; ; Three lemmas lead to the result.
;
;  (defthm times--1--1
;    (equal (times -1 -1) 1)
;    :hints
;    (("goal"
;      :use ((:instance plus-inverse-unique (x (times -1 -1)) (y 1))))))
;
;  (defthm times--1-times--1
;    (implies (rationalp x)
;             (equal (times -1 (times -1 x)) x))
;    :hints (("Goal"
;             :use (:instance times-commutative-and-associative
;                             (x -1)
;                             (y -1)
;                             (z x)))))
;  (defthm reassocate-to-cancel-plus
;    (implies (and (rationalp x)
;                  (rationalp y))
;             (equal (plus x (plus y (plus (times -1 x) (times -1 y))))
;                    0))
;    :hints
;    (("Goal" :use ((:instance plus-commutative-and-associative
;                              (x y)
;                              (y (times -1 x))
;                              (z (times -1 y)))))))
;
; ; Multiplication by Positive Preserves Inequality
; ;(implies (and (rationalp c)     ; see note below
; ;              (< 0 c))
; ;         (iff (< x y)
; ;              (< (* c x) (* c y))))
;
; (defthm multiplication-by-positive-preserves-inequality
;   (implies (and (rationalp c)
;                 (clessp 0 c))
;            (iff (clessp x y)
;                 (clessp (ctimes c x) (ctimes c y)))))
;
; ; The Zero Trichotomy Trick
; ; (implies (and (acl2-numberp x)
; ;               (not (equal x 0))
; ;               (not (equal x y)))
; ;          (or (< x y) (< y x)))
;
;  (defthm complex-equal-0
;    (implies (and (rationalp x)
;                  (rationalp y))
;             (equal (equal (complex x y) 0)
;                    (and (equal x 0)
;                         (equal y 0)))))
;
; (defthm zero-trichotomy-trick
;  (implies (and (acl2-numberp x)
;                (not (equal x 0))
;                (not (equal x y)))
;           (or (clessp x y) (clessp y x)))
;  :rule-classes nil :hints (("goal" :in-theory (enable fix))))
;
;
; ; The Find Equational Poly Trick
; ; (implies (and (<= x y) (<= y x)) (equal (fix x) (fix y)))
;
; (defthm find-equational-poly-trick
;   (implies (and (clesseqp x y)
;                 (clesseqp y x))
;
;            (equal (fix x) (fix y)))
;   :hints (("Goal" :in-theory (enable fix))))
;
; )

;-----------------------------------------------------------------------------
; Thus ends the ALSLA.  However, there are, no doubt, a few more that we
; will discover when we implement proof objects!

; Note that in Multiplication by Positive Preserves Inequality we require the
; positive to be rational.  Multiplication by a "positive" complex rational
; does not preserve the inequality.  For example, the following evaluates
; to nil:
; (let ((c #c(1 -10))
;       (x #c(1 1))
;       (y #c(2 -2)))
;  (implies (and ; (rationalp c)          ; omit the rationalp hyp
;                  (< 0 c))
;           (iff (< x y)                  ; t
;                (< (* c x) (* c y)))))   ; nil

; Thus, the coefficients in our polys must be rational.

; End of Essay on the Logical Basis for Linear Arithmetic.

(deflabel linear-arithmetic
  :doc
  ":Doc-Section Miscellaneous

  A description of the linear arithmetic decision procedure~/~/

  We describe the procedure very roughly here.
  Fundamental to the procedure is the notion of a linear polynomial
  inequality.  A ``linear polynomial'' is a sum of terms, each of
  which is the product of a rational constant and an ``unknown.''  The
  ``unknown'' is permitted to be ~c[1] simply to allow a term in the sum
  to be constant.  Thus, an example linear polynomial is
  ~c[3*x + 7*a + 2]; here ~c[x] and ~c[a] are the (interesting) unknowns.
  However, the unknowns need not be variable symbols.  For
  example, ~c[(length x)] might be used as an unknown in a linear
  polynomial.  Thus, another linear polynomial is ~c[3*(length x) + 7*a].
  A ``linear polynomial inequality'' is an inequality
  (either ~ilc[<] or ~ilc[<=])
  relation between two linear polynomials.  Note that an equality may
  be considered as a pair of inequalities; e.q., ~c[3*x + 7*a + 2 = 0]
  is the same as the conjunction of ~c[3*x + 7*a + 2 <= 0] and
  ~c[0 <= 3*x + 7*a + 2].

  Certain linear polynomial
  inequalities can be combined by cross-multiplication and addition to
  permit the deduction of a third inequality with
  fewer unknowns.  If this deduced inequality is manifestly false, a
  contradiction has been deduced from the assumed inequalities.

  For example, suppose we have two assumptions
  ~bv[]
  p1:       3*x + 7*a <  4
  p2:               3 <  2*x
  ~ev[]
  and we wish to prove that, given ~c[p1] and ~c[p2], ~c[a < 0].  As
  suggested above, we proceed by assuming the negation of our goal
  ~bv[]
  p3:               0 <= a.
  ~ev[]
  and looking for a contradiction.

  By cross-multiplying and adding the first two inequalities, (that is,
  multiplying ~c[p1] by ~c[2], ~c[p2] by ~c[3] and adding the respective
  sides), we deduce the intermediate result
  ~bv[]
  p4:  6*x + 14*a + 9 < 8 + 6*x
  ~ev[]
  which, after cancellation, is:
  ~bv[]
  p4:        14*a + 1 <  0.
  ~ev[]
  If we then cross-multiply and add ~c[p3] to ~c[p4], we get
  ~bv[]
  p5:               1 <= 0,
  ~ev[]
  a contradiction.  Thus, we have proved that ~c[p1] and ~c[p2] imply the
  negation of ~c[p3].

  All of the unknowns of an inequality must be eliminated by
  cancellation in order to produce a constant inequality.  We can
  choose to eliminate the unknowns in any order, but we eliminate them in
  term-order, largest unknowns first.  (~l[term-order].)  That is, two
  polys are cancelled against each other only when they have the same
  largest unknown.  For instance, in the above example we see that ~c[x]
  is the largest unknown in each of ~c[p1] and ~c[p2], and ~c[a] in
  ~c[p3] and ~c[p4].

  Now suppose that this procedure does not produce a contradiction but
  instead yields a set of nontrivial inequalities.  A contradiction
  might still be deduced if we could add to the set some additional
  inequalities allowing further cancellations.  That is where
  ~c[:linear] lemmas come in.  When the set of inequalities has stabilized
  under cross-multiplication and addition and no contradiction is
  produced, we search the database of ~c[:]~ilc[linear] rules for rules about
  the unknowns that are candidates for cancellation (i.e., are the
  largest unknowns in their respective inequalities).  ~l[linear]
  for a description of how ~c[:]~ilc[linear] rules are used.

  See also ~ilc[non-linear-arithmetic] for a description of an extension
  to the linear-arithmetic procedure described here.")

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

; Arith-term-order

; As of Version_2.6, we now use a different term-order when ordering
; the alist of a poly.  Arith-term-order is almost the same as
; term-order (which was used previously) except that 'UNARY-/ is
; `invisible' when it is directly inside a 'BINARY-*.  The motivation
; for this change lies in an observation that, when reasoning about
; floor and mod, terms such as (< (/ x y) (floor x y)) are common.
; However, when represented within the linear-pot-lst, (BINARY-* X
; (UNARY-/ Y)) was a heavier term than (FLOOR X Y) and so the linear
; rule (<= (floor x y) (/ x y)) never got a chance to fire.  Now,
; (FLOOR X Y) is the heavier term.

; Note that this function is something of a hack in that it works
; because "F" is later in the alphabet than "B".  It might be better
; to allow the user to specify an order; but, if the linear rules
; present in the community books are representative this
; is sufficient.  Perhaps this should be reconsidered later.

;; RAG - I thought about adding lines here for real numbers, but since we
;; cannot construct actual real constants, I don't think this is
;; needed here.  Besides, I'm not sure what the right value would be
;; for a real number!

(defmacro fn-count-evg-max-val ()

; Warning: (* 2 (fn-count-evg-max-val)) must be a (signed-byte 30); see
; fn-count-evg-rec and max-form-count-lst.  Modulo that requirement, we just
; pick a large natural number rather arbitrarily.

  200000)

(defmacro fn-count-evg-max-val-neg ()
  (-f (fn-count-evg-max-val)))

(defmacro fn-count-evg-max-calls ()

; Warning: The following plus 2 must be a (signed-byte 30); see
; fn-count-evg-rec.

; Modulo that requirement, the choice of 1000 below is rather arbitrary.  We
; chose 1000 for *default-rewrite-stack-limit*, so for no great reason we
; repeat that choice here.

  1000)

(defun min-fixnum (x y)

; This is a fast version of min, for fixnums.  We avoid the name minf because
; it's already used in the regression suite.

  (declare (type (signed-byte 30) x y))
  (the (signed-byte 30) (if (< x y) x y)))

(defun fn-count-evg-rec (evg acc calls)

; See the comment in var-fn-count for an explanation of how this function
; counts the size of evgs.

  (declare (xargs :measure (acl2-count evg)
                  :ruler-extenders :all)
           (type (unsigned-byte 29) acc calls))
  (the
   (unsigned-byte 29)
   (cond
    ((or (>= calls (fn-count-evg-max-calls))
         (>= acc (fn-count-evg-max-val)))
     (fn-count-evg-max-val))
    ((atom evg)
     (cond ((rationalp evg)
            (cond ((integerp evg)
                   (cond ((< evg 0)
                          (cond ((<= evg (fn-count-evg-max-val-neg))
                                 (fn-count-evg-max-val))
                                (t (min-fixnum (fn-count-evg-max-val)
                                               (+f 2 acc (-f evg))))))
                         (t
                          (cond ((<= (fn-count-evg-max-val) evg)
                                 (fn-count-evg-max-val))
                                (t (min-fixnum (fn-count-evg-max-val)
                                               (+f 1 acc evg)))))))
                  (t
                   (fn-count-evg-rec (numerator evg)
                                     (fn-count-evg-rec (denominator evg)
                                                       (1+f acc)
                                                       (1+f calls))
                                     (+f 2 calls)))))
           #+:non-standard-analysis
           ((realp evg)
            (prog2$ (er hard? 'fn-count-evg
                        "Encountered an irrational in fn-count-evg!")
                    0))
           ((complex-rationalp evg)
            (fn-count-evg-rec (realpart evg)
                              (fn-count-evg-rec (imagpart evg)
                                                (1+f acc)
                                                (1+f calls))
                              (+f 2 calls)))
           #+:non-standard-analysis
           ((complexp evg)
            (prog2$ (er hard? 'fn-count-evg
                        "Encountered a complex irrational in ~ fn-count-evg!")
                    0))
           ((symbolp evg)
            (cond ((null evg) ; optimization: len below is 3
                   (min-fixnum (fn-count-evg-max-val)
                               (+f 8 acc)))
                  (t
                   (let ((len (length (symbol-name evg))))
                     (cond ((<= (fn-count-evg-max-val) len)
                            (fn-count-evg-max-val))
                           (t (min-fixnum (fn-count-evg-max-val)
                                          (+f 2 acc (*f 2 len)))))))))
           ((stringp evg)
            (let ((len (length evg)))
              (cond ((<= (fn-count-evg-max-val) len)
                     (fn-count-evg-max-val))
                    (t (min-fixnum (fn-count-evg-max-val)
                                   (+f 1 acc (*f 2 len)))))))
           (t ; (characterp evg)
            (1+f acc))))
    (t (fn-count-evg-rec (cdr evg)
                         (fn-count-evg-rec (car evg)
                                           (1+f acc)
                                           (1+f calls))
                         (+f 2 calls))))))

(defmacro fn-count-evg (evg)
  `(fn-count-evg-rec ,evg 0 0))

(defun var-fn-count-1 (flg x var-count-acc fn-count-acc p-fn-count-acc
                           invisible-fns invisible-fns-table)

; Warning: Keep this in sync with fn-count-1.

; We return a triple --- the variable count, the function count, and the
; pseudo-function count --- derived from term (and the three input
; accumulators).  "Invisible" functions not inside quoted objects are ignored,
; in the sense of the global invisible-fns-table.

; The fn count of a term is the number of function symbols in the unabbreviated
; term.  Thus, the fn count of (+ (f x) y) is 2.  The primitives of ACL2,
; however, do not give very natural expression of the constants of the logic in
; pure first order form, i.e., as a variable-free nest of function
; applications.  What, for example, is 2?  It can be written (+ 1 (+ 1 0)),
; where 1 and 0 are considered primitive constants, i.e., 1 is (one) and 0 is
; (zero).  That would make the fn count of 2 be 5.  However, one cannot even
; write a pure first order term for NIL or any other symbol or string unless
; one adopts NIL and 'STRING as primitives too.  It is probably fair to say
; that the primitives of CLTL were not designed for the inductive construction
; of the objects in an orderly way.  But we would like for our accounting for a
; constant to somehow reflect the structure of the constant rather than the
; structure of the rather arbitrary CLTL term for constructing it.  'A seems to
; have relatively little to do with (intern (coerce (cons #\A 'NIL) 'STRING))
; and it is odd that the fn count of 'A should be larger than that of 'STRING,
; and odder still that the fn count of "STRING" be larger than that of 'STRING
; since the latter is built from the former with intern.

; We therefore adopt a story for how the constants of ACL2 are actually
; constructed inductively and the pseudo-fn count is the number of symbols in
; that construction.  The story is as follows.  (z), zero, is the only
; primitive integer.  Positive integers are constructed from it by the
; successor function s.  Negative integers are constructed from positive
; integers by unary minus.  Ratios are constructed by the dyadic function quo
; on an integer and a natural.  For example, -2/3 is inductively built as (quo
; (- (s(s(z)))) (s(s(s(z))))).  Complex rationals are similarly constructed
; from pairs of rationals.  All characters are primitive and are constructed by
; the function of the same name.  Strings are built from the empty string, (o),
; by "string-cons", cs, which adds a character to a string.  Thus "AB" is
; formally (cs (#\A) (cs (#\B) (o))).  Symbols are constructed by "packing" a
; string with p.  Conses are conses, as usual.  Again, this story is nowhere
; else relevant to ACL2; it just provides a consistent model for answering the
; question "how big is a constant?"  (Note that we bound the pseudo-fn count;
; see fn-count-evg.)

; Previously we had made no distinction between the fn-count and the
; pseudo-fn-count, but Jun Sawada ran into difficulty because (term-order (f)
; '2).  Note also that before we had
; (term-order (a (b (c (d (e (f (g (h (i x))))))))) (foo y '2/3))
; but
; (term-order (foo y '1/2) (a (b (c (d (e (f (g (h (i x)))))))))).

  (declare (xargs :guard (and (if flg
                                  (pseudo-term-listp x)
                                (pseudo-termp x))
                              (integerp var-count-acc)
                              (integerp fn-count-acc)
                              (integerp p-fn-count-acc)
                              (symbol-listp invisible-fns)
                              (alistp invisible-fns-table)
                              (symbol-list-listp invisible-fns-table))
                  :verify-guards NIL))
  (cond
   (flg
    (cond
     ((atom x)
      (mv var-count-acc fn-count-acc p-fn-count-acc))
     (t
      (mv-let
       (var-cnt fn-cnt p-fn-cnt)
       (let* ((term (car x))
              (fn (and (nvariablep term)
                       (not (fquotep term))
                       (ffn-symb term)))
              (invp (and fn
                         (not (flambdap fn)) ; optimization
                         (member-eq fn invisible-fns))))
         (cond (invp (var-fn-count-1
                      t
                      (fargs term)
                      var-count-acc fn-count-acc p-fn-count-acc
                      (cdr (assoc-eq fn invisible-fns-table))
                      invisible-fns-table))
               (t (var-fn-count-1 nil term
                                  var-count-acc fn-count-acc p-fn-count-acc
                                  nil invisible-fns-table))))
       (var-fn-count-1 t (cdr x) var-cnt fn-cnt p-fn-cnt
                       invisible-fns invisible-fns-table)))))
   ((variablep x)
    (mv (1+ var-count-acc) fn-count-acc p-fn-count-acc))
   ((fquotep x)
    (mv var-count-acc
        fn-count-acc
        (+ p-fn-count-acc (fn-count-evg (cadr x)))))
   (t (var-fn-count-1 t (fargs x)
                      var-count-acc (1+ fn-count-acc) p-fn-count-acc
                      (and invisible-fns-table ; optimization
                           (let ((fn (ffn-symb x)))
                             (and (symbolp fn)
                                  (cdr (assoc-eq fn invisible-fns-table)))))
                      invisible-fns-table))))

(defmacro var-fn-count (term invisible-fns-table)

; See the comments in var-fn-count-1.

  `(var-fn-count-1 nil ,term 0 0 0 nil ,invisible-fns-table))

(defmacro var-or-fn-count-< (var-count1 var-count2 fn-count1 fn-count2
                                        p-fn-count1 p-fn-count2)

; We use this utility when deciding if an ancestors check should inhibit
; further backchaining.  It says that either the var-counts are in order, or
; else the fn-counts are in (lexicographic) order.

; We added the var-counts check after analyzing an example from Robert Krug, in
; which the ancestors check was refusing to allow relieve-hyp on a ground term.
; Originally we tried a lexicographic order based on the var-count first, then
; (as before) the fn-count and p-fn-count.  But this led to at least two
; regression failures that led us to reconsider.  The current solution meets
; the goal of weakening the ancestors check (for example, to allow backchaining
; on ground terms as in Robert's example).

  (declare (xargs :guard ; avoid capture
                  (and (symbolp var-count1)
                       (symbolp var-count2)
                       (symbolp fn-count1)
                       (symbolp fn-count2)
                       (symbolp p-fn-count1)
                       (symbolp p-fn-count2))))
  `(cond ((< ,var-count1 ,var-count2) t)
         ((< ,fn-count1 ,fn-count2) t)
         ((> ,fn-count1 ,fn-count2) nil)
         (t (< ,p-fn-count1 ,p-fn-count2))))

(defun term-order1 (term1 term2 invisible-fns-table)

; A simple -- or complete or total -- ordering is a relation satisfying:
; "antisymmetric" XrY & YrX -> X=Y, "transitive" XrY & Y&Z -> XrZ, and
; "trichotomy" XrY v YrX.  A partial order weakens trichotomy to "reflexive"
; XrX.

; Term-order1 is a simple ordering on terms.  (term-order1 term1 term2 nil) if
; and only if (a) the number of occurrences of variables in term1 is strictly
; less than the number in term2, or (b) the numbers of variable occurrences are
; equal and the fn-count of term1 is strictly less than that of term2, or (c)
; the numbers of variable occurrences are equal, the fn-counts are equal, and
; the pseudo-fn-count of term1 is strictly less than that of term2, or (d) the
; numbers of variable occurrences are equal, the fn-counts are equal, the
; pseudo-fn-counts are equal, and (lexorder term1 term2).  If the third
; argument is non-nil, then it has the form as returned by function
; invisible-fns-table, and in the same manner as the table of that name,
; specifies functions to ignore when doing the above counts.  However, for
; simplicity we use lexorder, independent of invisible-fns-table, if all the
; counts agree between the two terms.

; Moreover, we usually call term-order1 with a third argument of nil.  The third
; argument is new in Version_3.5, as a way of eliminating the
; arithmetic-specific counting functions that had been used in defining
; function arith-term-order.  It may be worth reconsidering our use of the
; wrapper term-order+ for term-order1 in loop-stopper-rec, now that a third
; argument of term-order1 makes it more flexible; but this seems unimportant.

; Fix a third argument, tbl, and let (STRICT-TERM-ORDER X Y) be the LISP
; function defined as (AND (TERM-ORDER1 X Y tbl) (NOT (EQUAL X Y))).  For a
; fixed, finite set of function symbols and variable symbols STRICT-TERM-ORDER
; is well founded, as can be proved with the following lemma.

; Lemma.  Suppose that M is a function whose range is well ordered by r and
; such that the inverse image of any member of the range is finite.  Suppose
; that L is a total order.  Define (LESSP x y) = (OR (r (M x) (M y)) (AND
; (EQUAL (M x) (M y)) (L x y) (NOT (EQUAL x y)))). < is a well-ordering.
; Proof.  Suppose ... < t3 < t2 < t1 is an infinite descending sequence. ...,
; (M t3), (M t2), (M t1) is weakly descending but not infinitely descending and
; so has a least element.  WLOG assume ... = (M t3) = (M t2) = (M t1).  By the
; finiteness of the inverse image of (M t1), { ..., t3, t2, t1} is a finite
; set, which has a least element under L, WLOG t27.  But t28 L t27 and t28 /=
; t27 by t28 < t27, contradicting the minimality of t27.  QED

; If (TERM-ORDER1 x y nil) and t2 results from replacing one occurrence of y
; with x in t1, then (TERM-ORDER1 t2 t1 nil).  Cases on why x is less than y.
; 1. If the number of occurrences of variables in x is strictly smaller than in
; y, then the number in t2 is strictly smaller than in t1.  2. If the number of
; occurrences of variables in x is equal to the number in y but the fn-count of
; x is smaller than the fn-count of y, then the number of variable occurrences
; in t1 is equal to the number in t2 but the fn-count of t1 is less than the
; fn-count of t2.  3. A similar argument to the above applies if the number of
; variable occurrences and fn-counts are the same but the pseudo-fn-count of x
; is smaller than that of y.  4. If the number of variable occurrences and
; parenthesis occurrences in x and y are the same, then (LEXORDER x y).
; (TERM-ORDER1 t2 t1 nil) reduces to (LEXORDER t2 t1) because the number of
; variable and parenthesis occurrences in t2 and t1 are the same.  The
; lexicographic scan of t1 and t2 will be all equals until x and y are hit.

  (mv-let (var-count1 fn-count1 p-fn-count1)
          (var-fn-count term1 invisible-fns-table)
          (mv-let (var-count2 fn-count2 p-fn-count2)
                  (var-fn-count term2 invisible-fns-table)
                  (cond ((< var-count1 var-count2) t)
                        ((> var-count1 var-count2) nil)
                        ((< fn-count1 fn-count2) t)
                        ((> fn-count1 fn-count2) nil)
                        ((< p-fn-count1 p-fn-count2) t)
                        ((> p-fn-count1 p-fn-count2) nil)
                        (t (lexorder term1 term2))))))

(defun arith-term-order (term1 term2)
  (term-order1 term1 term2 '((BINARY-* UNARY-/))))

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


; Polys

; Historical note: Polys are now
; (<  0 (+ constant (* k1 t1) ... (* kn tn)))
; rather than
; (<  (+ constant (* k1 t1) ... (* kn tn)) 0)
; as in Version_2.6 and before.

(defrec poly
    (((alist parents . ttree)
      .
      (constant relation rational-poly-p . derived-from-not-equalityp)))
    t)

; A poly represents an implication hyps -> concl, where hyps is the
; conjunction of the terms in the 'assumptions of the ttree and concl is

; (<  0 (+ constant (* k1 t1) ... (* kn tn))), if relation = '<
; (<= 0 (+ constant (* k1 t1) ... (* kn tn))), otherwise.

; Constant is an ACL2 numberp, possibly complex-rationalp but usually
; rationalp.  Alist is an alist of pairs of the form (ti . ki) where ti is a
; term and ki is a rationalp.  The alist is kept ordered by arith-term-order on
; the ti.  The largest ti is at the front.  Relation is either '< or '<=.

; The ttree in a poly is a tag-tree.
; There are three tags we use here: lemma, assumption, and pt.  The lemma tag
; indicates a lemma name used to produce the poly.  The assumption tag
; indicates a term assumed true to produce the poly.  For example, an
; assumption might be (rationalp (foo a b)).  The pt tag indicates literals of
; current-clause used in the production of the poly.

; The parents field is generally a list of parents and is set-eql to the union
; over all 'pt tags in ttree of the tips of the pts.  (But see the comment
; labeled ":parent wart" in linear-b.lisp for an exception.)  It is used in the
; code that ignores polynomials descended from the current literal.  (This used
; to be done by to-be-ignoredp, which used to take up to 80% of the time spent
; by add-poly.)  See collect-parents and marry-parents for how we establish and
; maintain this relationship, and ignore-polyp for its use.

; Rational-poly-p is a booolean flag used in non-linear arithmetic.  When it is
; true, then the right-hand side of the inequality (the polynomial) is known to
; have a rational number value.  (But note that for ACL2(r), i.e. for
; #+:non-standard-analysis, the value need only be real.  Through the linear
; and non-linear arithmetic code, references to "rational" should be considered
; as references to "real".)  The flag is needed because of the presence of
; complex numbers in ACL2's logic.  Note that sums and products of rational
; polys are rational.  When rational-poly-p is true we know that the product of
; two positive polys is also positive.

; Derived-from-not-equalityp keeps track of whether the poly in question was
; derived directly from a top-level negated equality.  This field is new to
; v2_8 --- previously its value was calculated as needed.  In the rest of this
; comment, we address two issues --- (1) What derived-from-not-equalityp is
; used for.  (2) Differences from earlier behavior.

; (1) What derived-from-not-equalityp is used for: In process-equational-polys,
; we scan through the simplify-clause-pot-lst and look for complementary pairs
; of inequalities from which we can derive an equality.  Example: from (<= x y)
; and (<= y x) we can derive (equal x y).  However, the two inequalities could
; have themselves been derived from the very equality we are about to generate,
; and this could lead to looping.  Thus, we tag those inequalities which stem
; directly from the linearization of a (negated) equality with
; :derived-from-not-equalityp = t.  This field is then examined in
; process-equational-polys (or rather its sub-functions), and the result is
; used to prune the list of candidate inequalities.

; (2) Differences from earlier behavior:
; Previously, the function descends-from-not-equalityp played the role of the
; new field :derived-from-not-equalityp.  This function was much more
; conservative in its judgement and threw out any poly which descended from an
; inequality in any way, rather than only those which were derived directly
; from a (negated) equality.  Matt Kaufmann noticed difference and provoked an
; email exchange with Robert Krug, who did the research and initial coding
; leading to this version of linear).  Here is Robert's reply.

;   Matt is right, I did inadvertantly change ACL2's meaning for
;   descends-from-not-equalityp.  Perhaps this change is also responsible
;   for some of the patches required for the regression suite.  However,
;   this change was inadvertant only because I did not properly understand
;   the old behaviour which seems odd to me.  I believe that the new
;   behaviour is the ``correct'' one.  Let us look at an example:
;
;   Input:
;
;   x = y       (1)
;   a + y >= b  (2)
;   a + x <= b  (3)
;
;   After cancellation:
;
;   y: x <= y      (1a)
;      b <= y + a  (2)
;
;      y <= x      (1b)
;
;   x: x + a <= b  (3)
;
;      b <= x + a  (4) = (1b + 2)
;
;   I think that some form of x + a = b should be generated and added to
;   the clause.  Under the new order, (3) and (4) would be allowed to
;   combine, because neither of them descended \emph{directly} from an
;   inequality.  This seems like the kind of fact that I, as a user, would
;   expect ACL2 to know and use.  Under the old regime however, since (1b)
;   was used in the derivation of (4), this was not allowed.
;
;   This raises the qestion of whether the new test is too liberal.  For
;   example, from
;
;   input:
;   x = y
;   a + x = b + y
;
;   We would now generate the equality a = b.  I do not see any harm in
;   this.  Perhaps another example will convince me that we need to
;   tighten the heuristic up.

; [End of Robert's reply.]

; Note: In Nqthm, we thought of polynomials being inequalities in a different
; logic, or at least, in an extension of the Nqthm logic that included the
; rationals.  In ACL2, we think of a poly as simply being an alternative
; represention of a term, in which we have normalized by the use of certain
; algebraic laws governing the ACL2 function symbols <, <=, +, and *.  We
; noted these above (see ALSLA).  In addition, we think of the operations
; performed upon polys being just ordinary inferences within the logic,
; justified by still other algebraic laws, such as that allowing the addition
; of inequalities.  The basic idea behind the linear arithmetic procedure is
; to convert the (arithmetic) assumptions in a problem (including the
; negation of the conclusion) to their normal forms, make a bunch of ordinary
; forward-chaining-like inferences from those assumptions guided by certain
; principles, and if a contradiction is found, deduce that the original
; assumptions imply the original conclusion.  The point is that linear
; arithmetic is not some model-theoretic step appealing to the correspondence
; of theorems in two different theories but rather an entirely
; proof-theoretic step.

(defabbrev first-var (p) (caar (access poly p :alist)))

(defabbrev first-coefficient (p) (cdar (access poly p :alist)))

; We expect polys to meet the following invariant implied in the discussion
; above:
; 1. The leading coefficient is +/-1
; 2. The leading unknown:
;    a. Is not a quoted constant --- Not much of an unknown/variable
;    b. Is not itself a sum --- A poly represents a sum of terms
;    c. Is not of the form (* c x), where c is a rational constant ---
;       The c should have been ``pulled out''.
;    d. Is not of the form (- c), (* c d), or (+ c d) where c and d are
;       rational constants --- These terms should be evaluated and added
;       onto the constant, not used as an unknown.
;    Some of these are implied by others, but we check them each
;    independently.

; The following three functions (weakly) capture this notion.

; Note: These invariants are referred to elsewhere by number, e.g.,
; ``2.a'' If you change the above, search for occurrences of
; ``good-polyp''.  If you refer to these invariants, be sure to
; include the string ``good-polyp'' somewhere nearby.

(defun good-coefficient (c)
  (equal (abs c) 1))

(defun good-pot-varp (x)
  (and (not (quotep x))
       (not (equal (fn-symb x) 'BINARY-+))
       (not (and (equal (fn-symb x) 'BINARY-*)
                 (quotep (fargn x 1))
                 (real/rationalp (unquote (fargn x 1)))))
       (not (and (equal (fn-symb x) 'UNARY--)
                 (quotep (fargn x 1))
                 (real/rationalp (unquote (fargn x 1)))))))

(defun good-polyp (p)
  (and (good-coefficient (first-coefficient p))
       (good-pot-varp (first-var p))))

; We need to define executable versions of the logical functions for <, <=,
; and abs.  We know, however, that we will only apply them to acl2-numberps
; so we do not need to consider fixing the arguments.

;; RAG - I changed rational to real in the test to use < as the comparator.

(defun logical-< (x y)
  (declare (xargs :guard (and (acl2-numberp x) (acl2-numberp y))))
  (cond ((and (real/rationalp x)
              (real/rationalp y))
         (< x y))
        ((< (realpart x) (realpart y))
         t)
        (t (and (= (realpart x) (realpart y))
                (< (imagpart x) (imagpart y))))))

;; RAG - Another change of rational to real in the test to use <= as the
;; comparator.

(defun logical-<= (x y)
  (declare (xargs :guard (and (acl2-numberp x) (acl2-numberp y))))
  (cond ((and (real/rationalp x)
              (real/rationalp y))
         (<= x y))
        ((< (realpart x) (realpart y))
         t)
        (t (and (= (realpart x) (realpart y))
                (<= (imagpart x) (imagpart y))))))

(defun evaluate-ground-poly (p)

; We assume the :alist of poly p is nil and thus p is a ground poly.
; We compute its truth value.

  (if (eq (access poly p :relation) '<)
      (logical-< 0 (access poly p :constant))
      (logical-<= 0 (access poly p :constant))))

(defun impossible-polyp (p)
  (and (null (access poly p :alist))
       (eq (evaluate-ground-poly p) nil)))

(defun true-polyp (p)
  (and (null (access poly p :alist))
       (evaluate-ground-poly p)))

(defun silly-polyp (poly)

; For want of a better name, we say a poly is "silly" if it contains
; the *nil* assumption among its 'assumptions.

  (tag-tree-occur-assumption-nil (access poly poly :ttree)))

(defun impossible-poly (ttree)
  (make poly
        :alist nil
        :parents (collect-parents ttree)
        :rational-poly-p t
        :derived-from-not-equalityp nil
        :ttree ttree
        :constant -1
        :relation '<))

(defun base-poly0 (ttree parents relation rational-poly-p derived-from-not-equalityp)

; Warning: Keep this in sync with base-poly.

  (make poly
        :alist nil
        :parents parents
        :rational-poly-p rational-poly-p
        :derived-from-not-equalityp derived-from-not-equalityp
        :ttree ttree
        :constant 0
        :relation relation))

(defun base-poly (ttree relation rational-poly-p derived-from-not-equalityp)

; Warning: Keep this in sync with base-poly0.

  (make poly
        :alist nil
        :parents (collect-parents ttree)
        :rational-poly-p rational-poly-p
        :derived-from-not-equalityp derived-from-not-equalityp
        :ttree ttree
        :constant 0
        :relation relation))

(defun poly-alist-equal (alist1 alist2)

; This function is essentially EQUAL for two alists, but is faster
; (at least with poly alists).

  (cond ((null alist1)
         (null alist2))
        ((null alist2)
         nil)
        (t
         (and (eql (cdar alist1) (cdar alist2))
              (equal (caar alist1) (caar alist2))
              (poly-alist-equal (cdr alist1) (cdr alist2))))))

(defun poly-equal (poly1 poly2)

; This function is essentially EQUAL for two polys, but is faster.

  (and (eql (access poly poly1 :constant)
            (access poly poly2 :constant))
       (eql (access poly poly1 :relation)
            (access poly poly2 :relation))
       (poly-alist-equal (access poly poly1 :alist)
                         (access poly poly2 :alist))))

(defun poly-weakerp (poly1 poly2 parents-check)

; We return t if poly1 is ``weaker'' than poly2.

; Pseudo-examples:
; (<= 3 (* x y)) is weaker than both (< 3 (* x y)) and (<= 17/5 (* x y));
; but is not weaker than (< 17 (+ w (* x y))), (< 17 (* 5 x y)),
; or (< 17 (* y x)).

; Normally parents-check is t; if poly2 has a parent not in the parents of
; poly1, then poly1 might be usable in a context where poly2 is not usable.
; Use parents-check = nil if such a consideration does not apply.

  (let ((c1 (access poly poly2 :constant))
        (c2 (access poly poly1 :constant)))
    (and (or (logical-< c1 c2)

; The above inequality test is potentially confusing.  In the comments, it is
; said that (<= 3 (* x y)) is weaker than (<= 17/5 (* x y)).  Recall that the
; polys are stored in a format suggested by: (< (+ constant (* k1 t1) ... (* kn
; tn)) 0).  Thus, the two constants would be stored as a -3 and a -17/5, and
; the above test is correct.  -17/5 < -3.

             (and (eql c1 c2)
                  (or (eq (access poly poly1 :relation) '<=)
                      (eq (access poly poly2 :relation) '<))))
         (poly-alist-equal (access poly poly1 :alist)
                           (access poly poly2 :alist))
         (if parents-check
             (subsetp (access poly poly2 :parents)
                      (access poly poly1 :parents))
           t))))

(defun poly-member (p lst)

; P is a poly and lst is a list of polys.  This function used to return t if p
; was in lst (ignoring tag-trees).  Now, it returns t if p is weaker than
; some poly in lst.

; This change was motivated by an observation that after several linear rules
; have fired and a couple of rounds of cancellation have occurred, one will
; occasionally see the linear pot fill up with weak polys.  In most cases
; this idea makes no real performance difference; but Robert Krug has seen
; examples where it makes a tremendous difference.

  (and (consp lst)
       (or (poly-weakerp p (car lst) t)
           (poly-member p (cdr lst)))))

(defun new-and-ugly-linear-varsp (lst flag term)

; Lst is a list of polys, term is the linear var which triggered the
; addition of the polys in lst, and flag is a boolean indicating
; whether we have maxed out the the loop-stopper-value associated
; with term.  If flag is true, we check whether any of the polys are
; arith-term-order worse than term.

; Historical Note: Once upon a time, in Version_2.5 and earlier, this
; function actually insured that term wasn't in lst, i.e., that term was
; "new".  But in Version_2.6, we changed the meaning of the function without
; changing its name.  The word "new" in the name is now a mere artifact.

; This is intended to catch certain loops that can arise from linear
; lemmas.  See the "Mini-essay on looping and linear arithmetic" below.


  (cond ((not flag)
         nil)
        ((null lst)
         nil)
        ((arith-term-order term
                           (first-var (car lst)))
         t)
        (t (new-and-ugly-linear-varsp (cdr lst) flag term))))

(defun filter-polys (lst ans)

; We scan the list of polys lst.  If we find an impossible one, we
; return it as our first result.  If we find a true one we skip it.
; If we find a poly that is ``weaker'' (see poly-member and poly-weakerp)
; than one of those already filtered, we skip it.
; Otherwise we just accumulate them into ans.  We return two values:
; the standard indication of contradiction and, otherwise in the
; second, the filtered list.  This list in the reverse order from that
; produced by nqthm.

  (cond ((null lst)
         (mv nil ans))
        ((impossible-polyp (car lst))
         (mv (car lst) nil))
        ((true-polyp (car lst))
         (filter-polys (cdr lst) ans))
        ((poly-member (car lst) ans)
         (filter-polys (cdr lst) ans))
        (t
         (filter-polys (cdr lst) (cons (car lst) ans)))))


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

; Here we define some functions for constructing polys.

(defun add-linear-variable1 (n var alist)

; N is a rational constant and var is an arbitrary term -- a linear "variable".
; Alist is a polynomial alist and we are to add the new pair (var . n) to it.
; We keep the alist sorted on term-order on the terms with the largest var
; first.  Furthermore, if there is already an entry for var we merely add n to
; it.  If the resulting coefficient is 0 we delete the pair.

; We assume n is not 0 to begin with.

  (cond ((null alist)
         (cons (cons var n) nil))
        ((arith-term-order var (caar alist))
         (cond ((equal var (caar alist))
                (let ((k (+ (cdar alist)
                            n)))
                  (cond ((= k 0) (cdr alist))
                        (t (cons (cons var k) (cdr alist))))))
               (t (cons (car alist)
                        (add-linear-variable1 n var
                                              (cdr alist))))))
        (t (cons (cons var n)
                 alist))))

(defun zero-factor-p (term)

; The following code recognizes terms of the form (* a1 ... 0 ... ak)
; so that we can treat them as though they were 0.  Two sources of these
; 0-factor terms are: the original clause for which we are
; constructing a pot-lst, and a term introduced by forward chaining,
; which doesn't use rewrite.  (The latter might commonly occur via an
; fc rule like (implies (and (< 0 x) (< y y+)) (< (* x y) (* x y+)))
; triggered by (* x y+).  The free var y might be chosen to be 0, as
; would happen if (< 0 y+) were available.  The result would be the
; term (* 0 y).)

  (cond ((variablep term) nil)
        ((fquotep term)
         (equal term *0*))
        ((eq (ffn-symb term) 'BINARY-*)
         (or (zero-factor-p (fargn term 1))
             (zero-factor-p (fargn term 2))))
        (t
         nil)))

(defun get-coefficient (term acc)

; We are about to add term onto a poly.  We want to enforce the
; poly invariant 2.c. (Described shortly before the definition of
; good-polyp.)  We therefore accumulate onto acc any leading constant
; coefficients.  We return the (possibly) stripped term and its
; coefficient.

  (if (and (eq (fn-symb term) 'BINARY-*)
           (quotep (fargn term 1))
           (real/rationalp (unquote (fargn term 1))))
      (get-coefficient (fargn term 2) (* (unquote (fargn term 1)) acc))
    (mv acc term)))

(defun add-linear-variable (term side p)
  (mv-let (n term)
    (cond ((zero-factor-p term)
           (mv 0 nil))
          ((and (eq (fn-symb term) 'BINARY-*)
                (quotep (fargn term 1))
                (real/rationalp (unquote (fargn term 1))))
           (mv-let (coeff new-term)
             (get-coefficient term 1)
             (if (eq side 'lhs)
                 (mv (- coeff) new-term)
               (mv coeff new-term))))
          ((eq side 'lhs)
           (mv -1 term))
          (t
           (mv 1 term)))
    (if (= n 0)
        p
      (change poly p
              :alist
              (add-linear-variable1 n term (access poly p :alist))))))

(defun dumb-eval-yields-quotep (term)

; We are about to add term onto a poly.  We want to enforce the poly invariant
; 2.d. (Described shortly before the definition of good-polyp.)   Here, we
; check whether we should evaluate term.  If so, we do the evaluation in
; dumb-eval immediately below.

  (cond ((variablep term)
         nil)
        ((fquotep term)
         t)
        ((equal (ffn-symb term) 'BINARY-*)
         (and (dumb-eval-yields-quotep (fargn term 1))
              (dumb-eval-yields-quotep (fargn term 2))))
        ((equal (ffn-symb term) 'BINARY-+)
         (and (dumb-eval-yields-quotep (fargn term 1))
              (dumb-eval-yields-quotep (fargn term 2))))
        ((equal (ffn-symb term) 'UNARY--)
         (dumb-eval-yields-quotep (fargn term 1)))
        (t
         nil)))

(defun dumb-eval (term)

; See dumb-eval-yields-quotep, above.  This function evaluates (fix
; ,term) and produces the corresponding evg, not a term.  Thus,
; (binary-+ '1 '2) dumb-evals to 3 not '3, and (quote abc) dumb-evals
; to 0.

  (cond ((variablep term)
         (er hard 'dumb-eval
             "Bad term. We were expecting a constant, but encountered
              the variable ~x."
             term))
        ((fquotep term)
         (if (acl2-numberp (unquote term))
             (unquote term)
           0))
        ((equal (ffn-symb term) 'BINARY-*)
         (* (dumb-eval (fargn term 1))
            (dumb-eval (fargn term 2))))
        ((equal (ffn-symb term) 'BINARY-+)
         (+ (dumb-eval (fargn term 1))
            (dumb-eval (fargn term 2))))
        ((equal (ffn-symb term) 'UNARY--)
         (- (dumb-eval (fargn term 1))))
        (t
         (er hard 'dumb-eval
             "Bad term. The term ~x was not as expected by dumb-eval."
             term))))

(defun add-linear-term (term side p)

; Side is either 'rhs or 'lhs.  This function adds term to the
; indicated side of the poly p.  It is the main way we construct a
; poly.  See linearize.

  (cond
   ((variablep term)
    (add-linear-variable term side p))

; We enforce poly invariant 2.d.   (Described shortly before the
; definition of good-polyp.)

   ((dumb-eval-yields-quotep term)
    (let ((temp (dumb-eval term)))
      (if (eq side 'lhs)
          (change poly p
                  :constant
                  (+ (access poly p :constant) (- temp)))
        (change poly p
                :constant
                (+ (access poly p :constant) temp)))))

   (t
    (let ((fn1 (ffn-symb term)))
      (case fn1
            (binary-+
             (add-linear-term (fargn term 1) side
                              (add-linear-term (fargn term 2) side p)))
            (unary--
             (add-linear-term (fargn term 1)
                              (if (eq side 'lhs) 'rhs 'lhs)
                              p))
            (binary-*

; We enforce the poly invariants 2.b. and 2.c.  (Described shortly
; before the definition of good-polyp.)

             (cond
              ((and (quotep (fargn term 1))
                    (real/rationalp (unquote (fargn term 1)))
                    (equal (fn-symb (fargn term 2)) 'BINARY-+))
               (add-linear-term
                (mcons-term* 'BINARY-+
                             (mcons-term* 'BINARY-*
                                          (fargn term 1)
                                          (fargn (fargn term 2) 1))
                             (mcons-term* 'BINARY-*
                                          (fargn term 1)
                                          (fargn (fargn term 2) 2)))
                side
                p))
              ((and (quotep (fargn term 1))
                    (real/rationalp (unquote (fargn term 1)))
                    (equal (fn-symb (fargn term 2)) 'BINARY-*)
                    (quotep (fargn (fargn term 2) 1))
                    (real/rationalp (unquote (fargn (fargn term 2) 1))))
               (add-linear-term
                (mcons-term* 'BINARY-*
                             (kwote (* (unquote (fargn term 1))
                                       (unquote (fargn (fargn term 2) 1))))
                             (fargn (fargn term 2) 2))
                side
                p))
              (t
               (add-linear-variable term side p))))

            (otherwise
             (add-linear-variable term side p)))))))

(defun add-linear-terms-fn (rst)
  (cond ((null (cdr rst))
         (car rst))
        ((eq (car rst) :lhs)
         `(add-linear-term ,(cadr rst) 'lhs
                           ,(add-linear-terms-fn (cddr rst))))
        ((eq (car rst) :rhs)
         `(add-linear-term ,(cadr rst) 'rhs
                           ,(add-linear-terms-fn (cddr rst))))
        (t
         (er hard 'add-linear-terms-fn
             "Bad term ~x0"
             rst))))

(defmacro add-linear-terms (&rest rst)

; There are a couple of spots where we wish to add several pieces at
; a time to a poly.  This macro and its associated function enable us
; to circumvent ACL2's requirement that all functions take a fixed
; number of arguments.

; Example usage:
; (add-linear-terms :lhs term1
;                   :lhs ''1
;                   :rhs term2
;                   (base-poly ts-ttree
;                             '<=
;                             t
;                             nil))

  (add-linear-terms-fn rst))

(defun normalize-poly1 (coeff alist)
  (cond ((null alist)
         nil)
        (t
         (acons (caar alist) (/ (cdar alist) coeff)
                (normalize-poly1 coeff (cdr alist))))))

(defun normalize-poly (p)

; P is a poly.  We normalize it, so that the leading coefficient
; is +/-1.

  (if (access poly p :alist)
      (let ((c (abs (first-coefficient p))))
        (cond
         ((eql c 1)
          p)
         (t
          (change poly p
                  :alist (normalize-poly1 c (access poly p :alist))
                  :constant (/ (access poly p :constant) c)))))
    p))

(defun normalize-poly-lst (poly-lst)
  (cond ((null poly-lst)
         nil)
        (t
         (cons (normalize-poly (car poly-lst))
               (normalize-poly-lst (cdr poly-lst))))))


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


; Linear Pots

(defrec linear-pot ((loop-stopper-value . negatives) . (var . positives)) t)

; Var is a "linear variable", i.e., any term.  Positives and negatives are
; lists of polys with the properties that var is the first (heaviest) linear
; variable in each poly in each list and var occurs positively in the one and
; negatively in the other.  Loop-stopper-value is a natural number counter that
; is used to avoid looping, starting at 0 and incremented, using
; *max-linear-pot-loop-stopper-value* as a bound.

(defun modify-linear-pot (pot pos neg)

; We do the equivalent of:

; (change linear-pot pot :positives pos :negatives neg)

; except that we avoid unnecessary consing.

  (if (equal neg (access linear-pot pot :negatives))
      (if (equal pos (access linear-pot pot :positives))
          pot
        (change linear-pot pot :positives pos))
    (if (equal pos (access linear-pot pot :positives))
        (change linear-pot pot :negatives neg)
      (change linear-pot pot
              :positives pos
              :negatives neg))))

; Mini-essay on looping and linear arithmetic

; Robert Krug has written code to solve a problem with infinite loops related
; to linear arithmetic.  The following example produces the loop in ACL2
; Versions 2.4 and earlier.

;  (defaxiom *-strongly-monotonic
;    (implies (and (< a b))
;             (< (* a c) (* b c)))
;    :rule-classes :linear)
;
;  (defaxiom commutativity-2-of-*
;    (equal (* x y z)
;           (* y x z)))
;
;  (defstub foo (x) t)
;
;  (thm
;   (implies (and (< a (* a c))
;                 (< 0 evil))
;            (foo x)))

; The defconst below stops the loop.  We may want to increase it in the future,
; but it appears to be sufficient for certifying ACL2 community books.  It is
; used together with the field loop-stopper-value of the record linear-pot.
; When a linear-pot is first created, its loop-stopper-value is 0 (see
; add-poly).  See add-linear-lemma for how loop-stopper-value is used to detect
; loops.

; Robert has provided the following trace, in which one can still see the first
; few iterations of the loop before it is caught by the loop-stopping mechanism
; now added.  He suggests tracing new-and-ugly-linear-varp and worse-than to
; get some idea as to why this loop was not caught before due to the presence
; of the inequality (< 0 evil).

; (trace (add-linear-lemma
;         :entry (list (list 'term (nth 0 si::arglist))
;                      (list 'lemma (access linear-lemma
;                                           (nth 1 si::arglist)
;                                           :rune))
;                      (list 'max-term (access linear-lemma
;                                              (nth 1 si::arglist)
;                                              :max-term))
;                      (list 'conclusion (access linear-lemma
;                                                (nth 1 si::arglist)
;                                                :concl))
;                      (list 'type-alist (show-type-alist
;                                         (nth 2 si::arglist))))
;         :exit (if (equal (nth 9 si::arglist)
;                          (mv-ref 1))
;                   '(no change)
;                   (list (list 'old-pot-list
;                               (show-pot-lst (nth 9 si::arglist)))
;                         (list 'new-potlist
;                               (show-pot-lst (mv-ref 1)))))))

(defconst *max-linear-pot-loop-stopper-value* 3)

(defun loop-stopper-value-of-var (var pot-lst)

; We return the value of loop-stopper-value associated with var in the
; pot-lst.  If var does not appear we return 0.

  (cond ((null pot-lst) 0)
        ((equal var (access linear-pot (car pot-lst) :var))
         (access linear-pot (car pot-lst) :loop-stopper-value))
        (t
         (loop-stopper-value-of-var var (cdr pot-lst)))))

(defun set-loop-stopper-values (new-vars new-pot-lst term value)

; New-vars is a list of new variables in new-pot-lst.  Term is the trigger-term
; which caused the new pots to be added, and value is the loop-stopper-value
; associated with it.  If a new-var is term-order greater than term, we set its
; loop-stopper-value to value + 1.  Otherwise, we set it to value.

; Note that new-vars is in the same order as the vars of new-pot-lst.

  (cond ((null new-vars) new-pot-lst)
        ((equal (car new-vars) (access linear-pot (car new-pot-lst) :var))
           (cond ((arith-term-order term (car new-vars))
                    (cons (change linear-pot (car new-pot-lst)
                                  :loop-stopper-value (1+ value))
                          (set-loop-stopper-values (cdr new-vars)
                                                   (cdr new-pot-lst)
                                                   term
                                                   value)))
                 (t
                    (cons (change linear-pot (car new-pot-lst)
                                  :loop-stopper-value value)
                          (set-loop-stopper-values (cdr new-vars)
                                                   (cdr new-pot-lst)
                                                   term
                                                   value)))))
        (t
           (cons (car new-pot-lst)
                 (set-loop-stopper-values new-vars
                                          (cdr new-pot-lst)
                                          term
                                          value)))))

(defun var-in-pot-lst-p (var pot-lst)

; Test whether var is the label of any of the pots in pot-lst.

  (cond ((null pot-lst) nil)
        ((equal var (access linear-pot (car pot-lst) :var))
         t)
        (t
         (var-in-pot-lst-p var (cdr pot-lst)))))

(defun bounds-poly-with-var (poly-lst pt bounds-poly)

; We cdr down poly-lst, looking for a bounds poly.  Poly-lst is either the
; :positives or :negatives from a pot.  We would like to believe that the first
; bounds poly we find is, in fact, the strongest one present in poly-lst
; because we filter out any ones that are weaker than one already present with
; poly-member before adding it.  However, that filtering was done using
; poly-weakerp with parameter parents-check = t, yet here we do not have any
; preference based on parents, other than that they do not disqualify the poly
; (based on argument pt) -- we just want the strongest bounds poly.

  (cond ((null poly-lst)
         bounds-poly)
        ((and (null (cdr (access poly (car poly-lst) :alist)))
              (rationalp (access poly (car poly-lst) :constant))
              (not (ignore-polyp (access poly (car poly-lst) :parents) pt)))
         (bounds-poly-with-var
          (cdr poly-lst)
          pt
          (cond ((and bounds-poly
                      (poly-weakerp (car poly-lst) bounds-poly nil))
                 bounds-poly)
                (t (car poly-lst)))))
        (t
         (bounds-poly-with-var (cdr poly-lst) pt bounds-poly))))

(defun bounds-polys-with-var (var pot-lst pt)

; A bounds poly is one in which the there is only one var in the
; alist.  Such a poly can be regarded as "bounding" said var.

; Pseudo-examples:
; 3 < x is a bounds poly.
; 3 < x + y is not.
; #(1,1) < x is not.

; We insist that the constant c be rational.

; We return a list of the strongest bounds polys in the pot labeled
; with var.  If there are no such polys, we return nil.

  (cond ((null pot-lst) nil)
        ((equal var (access linear-pot (car pot-lst) :var))
         (let ((neg (bounds-poly-with-var
                     (access linear-pot (car pot-lst) :negatives) pt nil))
               (pos (bounds-poly-with-var
                     (access linear-pot (car pot-lst) :positives) pt nil)))
           (cond (neg (if pos (list neg pos) (list neg)))
                 (t   (if pos (list     pos) nil)))))
        (t (bounds-polys-with-var var (cdr pot-lst) pt))))

(defun polys-with-var1 (var pot-lst)
  (cond ((null pot-lst) nil)
        ((equal var (access linear-pot (car pot-lst) :var))
         (append (access linear-pot (car pot-lst) :negatives)
                 (access linear-pot (car pot-lst) :positives)))
        (t (polys-with-var1 var (cdr pot-lst)))))

(defun polys-with-var (var pot-lst)

; We return a list of all the polys in the pot labeled with var.
; If there is no pot in pot-lst labeled with var, we return nil.
; We may occasionally be calling this function with an improper
; var.  We catch this early, rather than stepping through the whole
; pot (see add-inverse-polys and add-inverse-polys1).

  (if (eq (fn-symb var) 'BINARY-+)
      nil
    (polys-with-var1 var pot-lst)))

(defun polys-with-pots (polys pot-lst ans)

; We filter out those polys in polys which do not have a pot in
; pot-lst to hold them.  Ans is initially nil.

  (cond ((null polys)
         ans)
        ((var-in-pot-lst-p (first-var (car polys))
                           pot-lst)
         (polys-with-pots (cdr polys) pot-lst (cons (car polys) ans)))
        (t
         (polys-with-pots (cdr polys) pot-lst ans))))

(defun new-vars-in-pot-lst (new-pot-lst old-pot-lst include-variableps)

; We return all the new vars of new-pot-lst.  A "var" of a pot-lst is the :var
; component of a linear-pot in the pot-lst.  A var is considered "new" if the
; var is not a var of the old-pot-lst and moreover, if include-variableps is
; false then it is not a variablep (i.e., is a function application).
; New-pot-lst is an extension of old-pot-lst, obtained by successive calls of
; add-poly.  Every variable of old-pot-lst is in the new, but not vice versa.
; Since both lists are ordered by the vars we can recur down both the new and
; the old pot lists simultaneously.

  (cond ((null new-pot-lst)
         nil)

; This function used to be wrong!  We incorrectly optimized the case for a pot
; with a variablep :var.  Consider an old-pot-lst with one pot, (foo x), and a
; new-pot-lst with two pots, x and (foo x).  Previously, since (variablep
; (access linear-pot (car new-pot-lst) :var)) would be true, we would recur on
; the cdr of both pots and then determine that (foo x) was new.  I suspect that
; the variablep test was added to the function after the rest had been written
; (and, the include-variablesp argument was definitely added more recently than
; any of the rest of this comment).  Here is the old code.  This bug was
; discovered by Robert Krug.

;               (or all-new-flg
;                   (null old-pot-lst)
;                   (not (equal (access linear-pot (car new-pot-lst) :var)
;                               (access linear-pot (car old-pot-lst) :var)))))
;          (cons (access linear-pot (car new-pot-lst) :var)
;                (new-vars-in-pot-lst (cdr new-pot-lst)
;                                     old-pot-lst all-new-flg)))

        ((or (null old-pot-lst)
             (not (equal (access linear-pot (car new-pot-lst) :var)
                         (access linear-pot (car old-pot-lst) :var))))
         (if (or include-variableps
                 (not (variablep (access linear-pot (car new-pot-lst) :var))))
             (cons (access linear-pot (car new-pot-lst) :var)
                   (new-vars-in-pot-lst (cdr new-pot-lst)
                                        old-pot-lst
                                        include-variableps))
           (new-vars-in-pot-lst (cdr new-pot-lst)
                                old-pot-lst
                                include-variableps)))
        (t (new-vars-in-pot-lst (cdr new-pot-lst)
                                (cdr old-pot-lst)
                                include-variableps))))

(defun changed-pot-vars (new-pot-lst old-pot-lst to-be-ignored-lst)

; New-pot-lst is an extension of old-pot-lst. To-be-ignored-lst is a
; list of pots which we are to ignore.  We return the list of pot
; labels (i.e., vars) of the pots which are changed with respect to
; old-pot-lst (a new pot is considered changed) which are not in
; to-be-ignored-lst.

  (cond ((null new-pot-lst)
         nil)
        ((equal (access linear-pot (car new-pot-lst) :var)
                (access linear-pot (car old-pot-lst) :var))
         (if (or (equal (car new-pot-lst)
                        (car old-pot-lst))
                 (member-equal (access linear-pot (car new-pot-lst) :var)
                               to-be-ignored-lst))
             (changed-pot-vars (cdr new-pot-lst) (cdr old-pot-lst)
                               to-be-ignored-lst)
           (cons (access linear-pot (car new-pot-lst) :var)
                 (changed-pot-vars (cdr new-pot-lst) (cdr old-pot-lst)
                                   to-be-ignored-lst))))
        (t
         (cons (access linear-pot (car new-pot-lst) :var)
               (changed-pot-vars (cdr new-pot-lst) old-pot-lst
                                 to-be-ignored-lst)))))

(defun infect-polys (lst ttree parents)

; We extend the :ttree of every poly in lst with ttree.  We similarly
; expand :parents with parents.

  (cond ((null lst) nil)
        (t (cons (change poly (car lst)
                         :ttree
                         (cons-tag-trees ttree
                                         (access poly (car lst) :ttree))
                         :parents (marry-parents
                                   parents
                                   (access poly (car lst) :parents)))
                 (infect-polys (cdr lst) ttree parents)))))

(defun infect-first-n-polys (lst n ttree parents)

; We assume that parents is always (collect-parents ttree) when this is called.
; See infect-new-polys.

  (cond ((int= n 0) lst)
        (t (cons (change poly (car lst)
                         :ttree
                         (cons-tag-trees ttree
                                         (access poly (car lst) :ttree))
                         :parents (marry-parents
                                   parents
                                   (access poly (car lst) :parents)))
                 (infect-first-n-polys (cdr lst) (1- n) ttree parents)))))

(defun infect-new-polys (new-pot-lst old-pot-lst ttree)

; We must infect with ttree every poly in new-pot-lst that is not in
; old-pot-lst.  By "infect" we mean cons ttree onto the ttree of the
; poly.  However, we know that new-pot-lst is an extension of
; old-pot-lst via add-poly.  For every linear-pot in old-pot-lst there
; is a pot in the new pot-lst with the same var.  Furthermore, the
; linear pots are ordered so that by cdring down both new and old
; simultaneously when they have equal vars we keep them in step.
; Finally, every list of polys in new is an extension of its
; corresponding list in old.  I.e., the positives of some pot in new
; with the same var as a pot in old is an extension of the positives
; of that pot in old.  Hence, to visit every new poly in that list it
; suffices to visit just the first n, where n is the difference in the
; lengths of the new and old positives.

; See add-disjunct-polys-and-lemmas.

  (cond ((null new-pot-lst) nil)
        ((or (null old-pot-lst)
             (not (equal (access linear-pot (car new-pot-lst) :var)
                         (access linear-pot (car old-pot-lst) :var))))
         (let ((new-new-pot-lst
                (infect-new-polys (cdr new-pot-lst)
                                  old-pot-lst
                                  ttree)))
           (cons (modify-linear-pot
                  (car new-pot-lst)
                  (infect-polys (access linear-pot (car new-pot-lst)
                                        :positives)
                                ttree
                                (collect-parents ttree))
                  (infect-polys (access linear-pot (car new-pot-lst)
                                        :negatives)
                                ttree
                                (collect-parents ttree)))
                 new-new-pot-lst)))
        (t
         (let ((new-new-pot-lst
                (infect-new-polys (cdr new-pot-lst)
                                  (cdr old-pot-lst)
                                  ttree)))
           (cons (modify-linear-pot
                  (car new-pot-lst)
                  (infect-first-n-polys
                   (access linear-pot (car new-pot-lst) :positives)
                   (- (length (access linear-pot (car new-pot-lst)
                                      :positives))
                      (length (access linear-pot (car old-pot-lst)
                                      :positives)))
                   ttree
                   (collect-parents ttree))
                  (infect-first-n-polys
                   (access linear-pot (car new-pot-lst) :negatives)
                   (- (length (access linear-pot (car new-pot-lst)
                                      :negatives))
                      (length (access linear-pot (car old-pot-lst)
                                      :negatives)))
                   ttree
                   (collect-parents ttree)))
                 new-new-pot-lst)))))

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


; Process-equational-polys

; Having set up the simplify-clause-pot-lst simplify clause we take
; advantage of it to find derived equalities that can help simplify
; the clause.  In this section we develop process-equational-polys.

(defun fcomplementary-multiplep1 (alist1 alist2)

; Both alists are polynomial alists, e.g., the car of each pair is a
; term and the cdr of each pair is a rational.  We determine whether
; negating each cdr in alist2 yields alist1.

  (cond ((null alist1) (null alist2))
        ((null alist2) nil)
        ((and (equal (caar alist1) (caar alist2))
              (= (cdar alist1) (- (cdar alist2))))
         (fcomplementary-multiplep1 (cdr alist1) (cdr alist2)))
        (t nil)))

(defun fcomplementary-multiplep (poly1 poly2)

; We determine whether multiplying poly2 by some negative rational
; produces poly1.  We assume that both polys have the same relation,
; e.g., <=, and the same first-var.

; Since we now normalize polys so that their first coefficient is
; +/-1.  That makes this function simpler.  In particular, we now need
; only check whether poly2 is the (arithmetic) negation of poly1.

    (and (= (access poly poly1 :constant)
            (- (access poly poly2 :constant)))
         (fcomplementary-multiplep1 (cdr (access poly poly1 :alist))
                                    (cdr (access poly poly2 :alist)))))

(defun already-used-by-find-equational-polyp-lst (poly1 lst)
  (cond ((endp lst) nil)
        (t (or (poly-equal (car (car lst)) poly1)
               (already-used-by-find-equational-polyp-lst poly1 (cdr lst))))))

(defun already-used-by-find-equational-polyp (poly1 hist)

; Poly1 is a positive poly.  Let poly2 be its negative version.  We are
; considering using them to create an equation as part of
; find-equational-poly.  We wish to know whether they have ever been
; so used before.  The answer is found by looking into the history of
; the clause being worked on, hist, for every 'simplify-clause entry.
; Each such entry is of the form (simplify-clause clause ttree).  We
; search ttree for (poly1 . poly2) tagged with 'find-equational-poly.

; Historical Note: Once upon a time, polys were not normalized in the
; sense that the leading coefficient is 1.  Thus, 2x <= 6 and 3 <= x
; were complementary.  To discover whether a poly had been used
; before, we had to know both the positive and the negative form
; involved.  But now polys are normalized and the only complement to 3
; <= x is x <= 3.  Thus, we could change the tag value to be a single
; positive poly instead of both.  You will note that we never actually
; need poly2.

  (cond ((null hist) nil)
        ((and (eq (access history-entry (car hist) :processor)
                  'simplify-clause)
              (already-used-by-find-equational-polyp-lst
               poly1
               (tagged-objects 'find-equational-poly
                               (access history-entry (car hist) :ttree))))
         t)
        (t (already-used-by-find-equational-polyp poly1 (cdr hist)))))

(defun cons-term-binary-+-constant (x term)

; x is an acl2-numberp, possibly complex, term is a rational type term.  We
; make a term equivalent to (binary-+ 'x term).

  (cond ((= x 0) term)
        ((quotep term) (kwote (+ x (cadr term))))
        (t (fcons-term* 'binary-+ (kwote x) term))))

(defun cons-term-unary-- (term)
  (cond ((variablep term) (fcons-term* 'unary-- term))
        ((fquotep term) (kwote (- (cadr term))))
        ((eq (ffn-symb term) 'unary--) (fargn term 1))
        (t (fcons-term* 'unary-- term))))

(defun cons-term-binary-*-constant (x term)

; x is a number (possibly complex), term is a rational type term.  We make a
; term equivalent to (binary-* 'x term).

  (cond ((= x 0) (kwote 0))
        ((= x 1) term)
        ((= x -1) (cons-term-unary-- term))
        ((quotep term) (kwote (* x (cadr term))))
        (t (fcons-term* 'binary-* (kwote x) term))))

(defun find-equational-poly-rhs1 (alist)

; See find-equational-poly-rhs.

  (cond ((null alist) *0*)
        ((null (cdr alist))
         (cons-term-binary-*-constant (- (cdar alist))
                                      (caar alist)))
        (t (cons-term 'binary-+
                      (list
                       (cons-term-binary-*-constant (- (cdar alist))
                                                    (caar alist))
                       (find-equational-poly-rhs1 (cdr alist)))))))

(defun find-equational-poly-rhs (poly1)

; Suppose poly1 and poly2 are complementary multiple <= polys, as
; described in find-equational-poly.  We wish to form the rhs term
; returned by that function.  We know the two polys have the form

; poly1:   k0 + k1*t1 + k2*t2 ... <= 0,      k1 positive
; poly2    j0 + j1*t1 + j2*t2 ... <= 0,      j1 negative

; and if q = k1/j1 then q is negative and ji*q = -ki for each i.

; Thus, k0 + k1*t1 + k2*t2 ... = 0.

; The equation created by find-equational-poly will be lhs = rhs, where lhs
; is t1.  We are to create rhs.  That is:

; rhs = -k0/k1 - k2/k1*t2 ...

; which, if we let c be -1/k1

; rhs = (+ c*k0 (+ c*k2*t2 ...))

; which is what we return.

; However now that we normalize polys, k1 = 1 and j1 = -1, so that q =
; -1 and c = -1.  Hence we now negate, rather than multiplying by c.

  (cons-term-binary-+-constant (- (access poly poly1 :constant))
                               (find-equational-poly-rhs1
                                (cdr (access poly poly1 :alist)))))

(defun find-equational-poly3 (poly1 poly2 hist)

; See find-equational-poly.  This is the function that actually builds
; the affirmative answer returned by that function.  Between this function
; and that one are two others whose only job is to iterate across all the
; potentially acceptable positives and negatives and give to this function
; a potentially appropriate poly1 and poly2.

; We know that poly1 is a positive <= poly that does not descend from
; a (not (equal & &)).  We know that poly2 is a negative <= poly that
; does not descend from a (not (equal & &)).  We know they have the same
; first-var.

; We first determine whether they are complementary multiples of eachother
; and have not been used by find-equational-poly already.  If so, we
; return a ttree and two terms, as described by find-equational-poly.

  (cond ((and (fcomplementary-multiplep poly1 poly2)
              (not (already-used-by-find-equational-polyp poly1 hist)))
         (mv (add-to-tag-tree
              'find-equational-poly
              (cons poly1 poly2)
              (cons-tag-trees (access poly poly1 :ttree)
                              (access poly poly2 :ttree)))
             (first-var poly1)
             (find-equational-poly-rhs poly1)))
        (t (mv nil nil nil))))

(defun find-equational-poly2 (poly1 negatives hist)

; See find-equational-poly.  Poly1 is a positive <= poly with the same
; first var as all the members of negatives.  We scan negatives looking
; for a poly2 that is acceptable.

  (cond
   ((null negatives)
    (mv nil nil nil))
   ((or (not (eq (access poly (car negatives) :relation) '<=))
        (access poly (car negatives) :derived-from-not-equalityp))
    (find-equational-poly2 poly1 (cdr negatives) hist))
   (t
    (mv-let (msg lhs rhs)
      (find-equational-poly3 poly1 (car negatives) hist)
      (cond
       (msg (mv msg lhs rhs))
       (t (find-equational-poly2 poly1 (cdr negatives)
                                 hist)))))))

(defun find-equational-poly1 (positives negatives hist)

; See find-equational-poly.  Positives and negatives are the
; appropriate fields of the same linear pot.  All the first-vars are
; equal.  We scan the positives and for each <= poly there we look for
; an acceptable member of the negatives.

  (cond
   ((null positives)
    (mv nil nil nil))
   ((or (not (eq (access poly (car positives) :relation) '<=))
        (access poly (car positives) :derived-from-not-equalityp))
    (find-equational-poly1 (cdr positives) negatives hist))
   (t
    (mv-let (msg lhs rhs)
      (find-equational-poly2 (car positives) negatives hist)
      (cond
       (msg (mv msg lhs rhs))
       (t (find-equational-poly1 (cdr positives) negatives hist)))))))

(defun find-equational-poly (pot hist)

; Look for an equation to be derived from this pot.  We look for a
; weak inequality in positives whose negation is a member of
; negatives, which was not the result of linearizing a (not (equal lhs
; rhs)), and which has never been found (and recorded in hist) before.
; The message we look for is our business (we generate and recognize
; them) but they must be in the tag-tree stored in the 'simplify-clause
; entries of hist.

; We return three values.  If we find no acceptable poly, we return
; three nils.  Otherwise we return a non-nil ttree and two terms, lhs
; and rhs.  In this case, it is a truth (assuming pot and the
; 'assumptions in the ttree) that lhs = rhs.  As a matter of fact, lhs
; will be the var of the linear-pot pot and rhs will be a +-tree of
; lighter vars.  Of course, the equation can be rearranged and used
; arbitrarily by the caller.

; If the equation is used in the current simplification, the ttree we
; return must find its way into the hist entry for that
; simplify-clause.

; Historical note: The affect of the newly (v2_8) introduced field,
; :derived-from-not-equalityp, is different from that of the
; earlier function descends-from-not-equalityp.  We are now more
; liberal about the polys we can generate here.  See the discussion
; accompanying the definition of a poly.  (Search for ``(defrec poly''.))

  (find-equational-poly1 (access linear-pot pot :positives)
                         (access linear-pot pot :negatives)
                         hist))

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


; Add-polys

(defun get-coeff-for-cancel1 (alist1 alist2)

; Alist1 and alist2 are the alists from two polys which we are about
; to cancel.  We calculate the absolute value of what would be the
; leading coefficient if we added the two alists.  This is in support
; of cancel, which see.

  (cond ((null alist1)
         (if (null alist2)
             1
           (abs (cdar alist2))))
        ((null alist2)
         (abs (cdar alist1)))
        ((not (arith-term-order (caar alist1) (caar alist2)))
         (abs (cdar alist1)))
        ((equal (caar alist1) (caar alist2))
         (let ((temp (+ (cdar alist1)
                        (cdar alist2))))
           (if (eql temp 0)
               (get-coeff-for-cancel1 (cdr alist1) (cdr alist2))
             (abs temp))))
        (t
         (abs (cdar alist2)))))

(defun cancel2 (alist coeff)
  (cond ((null alist)
         nil)
        (t
         (cons (cons (caar alist)
                     (/ (cdar alist) coeff))
               (cancel2 (cdr alist) coeff)))))

(defun cancel1 (alist1 alist2 coeff)

; Alist1 and alist2 are the alists from two polys which we are about
; to cancel.  We create a new alist by adding alist1 and alist2, using
; coeff to normalize the result.

  (cond ((null alist1)
         (cancel2 alist2 coeff))
        ((null alist2)
         (cancel2 alist1 coeff))
        ((not (arith-term-order (caar alist1) (caar alist2)))
         (cons (cons (caar alist1)
                     (/ (cdar alist1) coeff))
               (cancel1 (cdr alist1) alist2 coeff)))
        ((equal (caar alist1) (caar alist2))
         (let ((temp (/ (+ (cdar alist1)
                           (cdar alist2))
                        coeff)))
           (cond ((= temp 0)
                  (cancel1 (cdr alist1) (cdr alist2) coeff))
                 (t (cons (cons (caar alist1) temp)
                          (cancel1 (cdr alist1) (cdr alist2) coeff))))))
        (t (cons (cons (caar alist2)
                       (/ (cdar alist2) coeff))
                 (cancel1 alist1 (cdr alist2) coeff)))))

(defun cancel (p1 p2)

; P1 and p2 are polynomials with the same first var and opposite
; signs.  We construct the poly obtained by cross-multiplying and
; adding p1 and p2 so as to cancel out the first var.

; Polys are now normalized such that the leading coefficients are
; +/-1.  Hence we no longer need to cross-multiply before adding
; p1 and p2.  (The variables co1 and co2 in the original version
; are now guaranteed to be 1.)  We do add a twist to the naive
; implementation though.  Rather than adding the two alists, and
; then normalizing the result, we calculate what would have been
; the leading coeficient and normalize as we go (dividing by its
; absolute value).

; We return two values.  The first indicates whether we have
; discovered a contradiction.  If the first result is non-nil then it
; is the impossible poly formed by cancelling p1 and p2.  The ttree of
; that poly will be interesting to our callers because it contains
; such things as the assumptions made and the lemmas used to get the
; contradiction.  When we return a contradiction, the second result is
; always nil.  Otherwise, the second result is either nil (meaning that
; the cancellation yeilded a trivially true poly) or is the newly
; formed poly.

; Historical note: The affect of the newly (v2_8) introduced field,
; :derived-from-not-equalityp, is different from that of the
; earlier function descends-from-not-equalityp.  See the discussion
; accompanying the definition of a poly.  (Search for ``(defrec poly''.))

; Note:  It is sometimes convenient to trace this function with

;   (trace (cancel
;           :entry (list (show-poly (car si::arglist))
;                        (show-poly (cadr si::arglist)))
;           :exit (let ((flg (car values))
;                       (val (car (mv-refs 1))))
;                   (cond (flg (append values (mv-refs 1)))
;                         (val (list nil (show-poly val)))
;                         (t (list nil nil))))))

; Since we now normalize polys, the cars of the two alists will
; cancel each other out and all we have to concern ourselves with
; are their cdrs.

  (let* ((alist1 (cdr (access poly p1 :alist)))
         (alist2 (cdr (access poly p2 :alist)))
         (coeff (get-coeff-for-cancel1 alist1 alist2))
         (p (make poly
                  :constant (/ (+ (access poly p1 :constant)
                                  (access poly p2 :constant))
                               coeff)
                  :alist (cancel1 alist1
                                  alist2
                                  coeff)
                  :relation  (if (or (eq (access poly p1 :relation) '<)
                                     (eq (access poly p2 :relation) '<))
                                 '<
                               '<=)
                  :ttree (cons-tag-trees (access poly p1 :ttree)
                                         (access poly p2 :ttree))
                  :rational-poly-p (and (access poly p1 :rational-poly-p)
                                        (access poly p2 :rational-poly-p))
                  :parents (marry-parents (access poly p1 :parents)
                                          (access poly p2 :parents))
                  :derived-from-not-equalityp nil)))
    (cond ((impossible-polyp p) (mv p nil))
          ((true-polyp p) (mv nil nil))
          (t (mv nil p)))))

(defun cancel-poly-against-all-polys (p polys pt ans)

; P is a poly, polys is a list of polys, the first var of p is the same
; as the first of every poly in polys and has opposite sign.  We are to
; cancel p against each member of polys, getting in each case a
; contradiction, a true poly (which we discard) or a new shorter poly.
; Pt is a parent tree indicating literals we are to avoid.

; We return two answers.  The first is either nil or the first
; contradiction we find.  When the first is a contradiction, the
; second is nil.  Otherwise, the second is the list of all newly
; produced polys.

; Ans is supposed to be nil initially and is the site at which we
; accumulate the new polys.  This is a No-Change Loser.

  (cond ((null polys)
         (mv nil ans))
        ((ignore-polyp (access poly (car polys) :parents) pt)
         (cancel-poly-against-all-polys p (cdr polys)
                                        pt ans))
        (t (mv-let (contradictionp new-p)
             (cancel p (car polys))
             (cond (contradictionp
                    (mv contradictionp nil))
                   (t
                    (cancel-poly-against-all-polys
                     p
                     (cdr polys)
                     pt

; We discard polys which are ``weaker'' (see poly-member and
; poly-weakerp) than one already accumulated into ans.

                     (if (and new-p
                              (not (poly-member new-p ans)))
                         (cons new-p ans)
                       ans))))))))

; Historical note:

; The following functions --- add-polys0 and its callees --- have been
; substantially rewritten.  Previous to Version_2.8 the following
; two comments were in add-poly and add-poly1 (which no longer exists)
; respectively:

; Add-poly historical comment

; ; This is the fundamental function for changing a pot-lst.  It adds a
; ; single poly p to pot-lst.  All the other functions which construct
; ; pot lists do it, ultimately, via calls to add-poly.
;
; ; In nqthm this function was called add-equation but since its argument
; ; is a poly we renamed it.
;
; ; This function adds a poly p to the pot-lst.  Since the pot-lst is
; ; ordered by term-order on the vars, we recurse down the pot-lst just
; ; far enough to find where p fits.  There are three cases: p goes
; ; before the current pot, p goes in the current pot, or p goes after
; ; the current pot.  The first is simplest: make a pot for p and stick
; ; it at the front of the pot-lst.  The second is not too bad: cancel p
; ; against every poly of opposite sign in this pot to generate a bunch
; ; of new polys that belong earlier in the pot-lst and then add p to
; ; the current pot.  The third is the worst: Recursively add p to the
; ; rest of the pot-lst, get back a bunch of polys that need processing,
; ; process the ones that belong where you're standing and pass up the
; ; ones that go earlier.

; Add-poly1 historical comment

; ; This is a subroutine of add-poly.  See the comment there.  Suppose
; ; we've just gotten back from a recursive call of add-poly and it
; ; returned to us a bunch of polys that belong earlier in the pot-lst
; ; (from it).  Some of those polys may belong here where we are
; ; standing.  Others should be passed up.
;
; ; To-do is the list of polys produced by the recursive add-poly.  Var,
; ; positives, and negatives are the appropriate components of the pot
; ; that add-poly is standing on.  We process those polys in to-do that
; ; go here, producing new positives and negatives, and set aside those
; ; that don't go here.  The processing of the ones that do go here may
; ; create some additional polys that don't go here.  To-do-next is the
; ; accumulation site for the to-do's we don't handle and the ones our
; ; processing creates.

; Add-poly is still the fundamental routine for adding a poly to the
; pot-lst.  However, we now merely gather up newly generated polys and
; pass them back out to add-polys --- changing the routines which
; add polys to the pot list from a depth-first search to a
; breadth-first search.

(defun add-poly (p pot-lst to-do-next pt nonlinearp)

; This is the fundamental function for changing a pot-lst.  It adds a
; single poly p to pot-lst.  All the other functions which construct
; pot lists do it, ultimately, via calls to add-poly.

; This function adds a poly p to the pot-lst and returns 3 values.
; The first is the standard contradictionp.  The second value, of
; interest only when we don't find a contradiction, is the new pot-lst
; obtained by adding p to pot-lst.  The third value is a list of new
; polys generated by the adding of p to pot-lst, which must be
; processed.  We cons our own generated polys onto the incoming
; to-do-next to form this result.

; An invariant exploited by infect-new-polys is that all of the new
; polys in any linear pot occur at the front of the list and no polys
; are ever deleted.  That is, if this or any other function wants to
; add a poly to the positives, say, it must cons it onto the front.
; In general, if we have an old linear pot and a new one produced from
; it and we want to process all the polys in the positives, say, of the
; new pot that are not in the old one, it suffices to process the first
; n elements of the new positives, where n is the difference in their
; lengths.

; Note:  If adding a poly creates a new pot, its loop-stopper value is set to
; 0.  This is changed to the correct value (if necessary) in
; add-linear-lemma.

; Trace Note:
;   (trace (add-poly
;           :entry (let ((args si::arglist))
;                    (list (show-poly (nth 0 args)) ;p
;                          (show-pot-lst (nth 1 args)) ;pot-lst
;                          (show-poly-lst (nth 2 args)) ;to-do-next
;                          (nth 3 args)
;                          (nth 4 args)
;                          '|ens| (nth 6 args) '|wrld|))
;           :exit (cond ((null (car values))
;                        (list nil
;                              (show-pot-lst (mv-ref 1))
;                              (show-poly-lst (mv-ref 2))))

  (cond
   ((time-limit5-reached-p
     "Out of time in linear arithmetic (add-poly).") ; nil, or throws
    (mv nil nil nil))
   ((or (null pot-lst)
        (not (arith-term-order (access linear-pot (car pot-lst) :var)
                               (first-var p))))
    (mv nil
        (cons (if (< 0 (first-coefficient p)) ; p is normalized (below too)
                  (make linear-pot
                        :var (first-var p)
                        :loop-stopper-value 0
                        :positives (list p)
                        :negatives nil)
                (make linear-pot
                      :var (first-var p)
                      :loop-stopper-value 0
                      :positives nil
                      :negatives (list p)))
              pot-lst)
        to-do-next))
   ((equal (access linear-pot (car pot-lst) :var)
           (first-var p))
    (cond
     ((poly-member p
                   (if (< 0 (first-coefficient p))
                       (access linear-pot (car pot-lst) :positives)
                     (access linear-pot (car pot-lst) :negatives)))
      (mv nil pot-lst to-do-next))
     (t (mv-let (contradictionp to-do-next)
          (cancel-poly-against-all-polys
           p
           (if (< 0 (first-coefficient p))
               (access linear-pot (car pot-lst) :negatives)
             (access linear-pot (car pot-lst) :positives))
           pt
           to-do-next)
          (cond
           (contradictionp (mv contradictionp nil nil))

; Non-linear optimization
; Magic number.  If non-linear arithmetic is enabled, and there are
; more than 20 polys in the appropriate side of the pot, we give up
; and do not add the new poly.  This has proven to be a useful heuristic.
; Increasing this number will slow ACL2 down sometimes, but it may
; allow more proofs to go through.  So far I have not seen one which
; needs more than 20, but less than 100 --- which is too much.
; Note that the pot-lst isn't changed (i.e., poly wasn't added to its
; pot) but we will propagate the children poly and (possibly) add them
; to their pots.  These children are "orphans" because a parent is
; missing from the pot-lst.


           ((and nonlinearp
                 (>=-len (if (< 0 (first-coefficient p))
                             (access linear-pot (car pot-lst)
                                     :positives)
                           (access linear-pot (car pot-lst)
                                   :negatives))
                         21))
            (mv nil
                pot-lst
                to-do-next))
           (t (mv nil
                  (cons
                   (if (< 0 (first-coefficient p))
                       (change linear-pot (car pot-lst)
                               :positives
                               (cons p (access linear-pot (car pot-lst)
                                               :positives)))
                     (change linear-pot (car pot-lst)
                             :negatives
                             (cons p (access linear-pot (car pot-lst)
                                             :negatives))))
                   (cdr pot-lst))
                  to-do-next)))))))
   (t
    (mv-let
      (contradictionp cdr-pot-lst to-do-next)
      (add-poly p (cdr pot-lst) to-do-next pt nonlinearp)
      (cond
       (contradictionp (mv contradictionp nil nil))
       (t
        (mv nil (cons (car pot-lst) cdr-pot-lst) to-do-next)))))))

(defun prune-poly-lst (poly-lst ans)
  (cond ((null poly-lst)
         ans)
        ((endp (cddr (access poly (car poly-lst) :alist)))
         (prune-poly-lst (cdr poly-lst) (cons (car poly-lst) ans)))
        (t
         (prune-poly-lst (cdr poly-lst) ans))))

(defun add-polys1 (lst pot-lst new-lst pt nonlinearp max-rounds
                       rounds-completed)

; This function adds every element of the poly list lst to pot-lst and
; accumulates the new polys in new-lst.  When lst is exhausted it
; starts over on the ones in new-lst and iterates that until no new polys
; are produced.  It returns 2 values:  the standard contradictionp in the
; the first and the final pot-lst in the second.

  (cond ((eql max-rounds rounds-completed)
         (mv nil pot-lst))
        ((null lst)
         (cond ((null new-lst)
                (mv nil pot-lst))

; Non-linear optimization
; Magic number.  If non-linear arithmetic is enabled, and there are
; more than 100 polys in lst waiting to be added to the pot-lst, we
; try pruning the list of new polys.  This has proven to be a useful
; heuristic.  Increasing this number will slow ACL2 down sometimes,
; but it may allow more proofs to go through.  So far I have not seen
; one which needs more than 100, but less than 500 --- which is too
; much.  After Version_5.0, we eliminated the nonlinearp condition
; and prune when there are more than 100 polys in the new list.

               ((and ; nonlinearp
                     (>=-len new-lst 101))
                (add-polys1 (prune-poly-lst new-lst nil)
                            pot-lst nil pt nonlinearp
                            max-rounds (+ 1 rounds-completed)))
               (t
                (add-polys1 new-lst pot-lst nil
                            pt nonlinearp
                            max-rounds (+ 1 rounds-completed)))))
        (t (mv-let (contradictionp new-pot-lst new-lst)
             (add-poly (car lst) pot-lst new-lst pt nonlinearp)
             (cond (contradictionp (mv contradictionp nil))
                   (t (add-polys1 (cdr lst)
                                  new-pot-lst
                                  new-lst
                                  pt
                                  nonlinearp
                                  max-rounds
                                  rounds-completed)))))))

(defun add-polys0 (lst pot-lst pt nonlinearp max-rounds)

; Lst is a list of polys.  We filter out the true ones (and detect any
; impossible ones) and then normalize and add the rest to pot-lst.
; Any new polys thereby produced are also added until there's nothing
; left to do.  We return the standard contradictionp and a new pot-lst.

  (mv-let (contradictionp lst)
    (filter-polys lst nil)
    (cond (contradictionp (mv contradictionp nil))
          (t (add-polys1 lst pot-lst nil pt nonlinearp max-rounds 0)))))

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

; "Show-" functions

; The next group of "show-" functions are not part of the system but are
; convenient for system debugging.  (show-poly poly) will create a list
; structure that prints so as to show a polynomial in the conventional
; notation.  The term enclosed in an extra set of parentheses is the leading
; term of the poly.  An example show-poly is '(3 J + (I) + 77 <= 4 M + 2 N).

; (defun show-poly2 (pair lst)
;   (let ((n (abs (cdr pair)))
;         (x (car pair)))
;     (cond ((= n 1) (cond ((null lst) (list x))
;                          (t (list* x '+ lst))))
;           (t (cond ((null lst) (list n x))
;                    (t (list* n x '+ lst)))))))
;
; (defun show-poly1 (alist lhs rhs)
;
; ; Note: This function ought to return (mv lhs rhs) but when it is used in
; ; tracing multiply valued functions that functionality hurts us: the
; ; computation performed during the tracing destroys the multiple value being
; ; manipulated by the function being traced.  So that we can use this function
; ; conveniently during tracing, we make it a single valued function.
;
;   (cond ((null alist) (cons lhs rhs))
;         ((logical-< 0 (cdar alist))
;          (show-poly1 (cdr alist) lhs (show-poly2 (car alist) rhs)))
;         (t (show-poly1 (cdr alist) (show-poly2 (car alist) lhs) rhs))))
;
; (defun show-poly (poly)
;   (let* ((pair (show-poly1
;                    (cond ((null (access poly poly :alist)) nil)
;                          (t (cons (cons (list (caar (access poly poly :alist)))
;                                         (cdar (access poly poly :alist)))
;                                   (cdr (access poly poly :alist)))))
;                    (cond ((= (access poly poly :constant) 0)
;                           nil)
;                          ((logical-< 0 (access poly poly :constant)) nil)
;                          (t (cons (- (access poly poly :constant)) nil)))
;                    (cond ((= (access poly poly :constant) 0)
;                           nil)
;                          ((logical-< 0 (access poly poly :constant))
;                           (cons (access poly poly :constant) nil))
;                          (t nil))))
;          (lhs (car pair))
;          (rhs (cdr pair)))
;
; ; The let* above would be (mv-let (lhs rhs) (show-poly1 ...) ...) had
; ; show-poly1 been specified to return two values instead of a pair.
; ; See note above.
;
;     (append (or lhs '(0))
;             (cons (access poly poly :relation) (or rhs '(0))))))
;
; (defun show-poly-lst (poly-lst)
;   (cond ((null poly-lst) nil)
;         (t (cons (show-poly (car poly-lst))
;                  (show-poly-lst (cdr poly-lst))))))
;
;
; (defun show-pot-lst (pot-lst)
;   (cond
;    ((null pot-lst) nil)
;    (t (cons
;        (list* :var (access linear-pot (car pot-lst) :var)
;               (append (show-poly-lst
;                        (access linear-pot (car pot-lst) :negatives))
;                       (show-poly-lst
;                        (access linear-pot (car pot-lst) :positives))))
;        (show-pot-lst (cdr pot-lst))))))
;
; (defun show-type-alist (type-alist)
;   (cond ((endp type-alist) nil)
;         (t (cons (list (car (car type-alist))
;                        (decode-type-set (cadr (car type-alist))))
;                  (show-type-alist (cdr type-alist))))))
;
;
; (defun number-of-polys (pot-lst)
;   (cond ((null pot-lst) 0)
;         (t (+ (len (access linear-pot (car pot-lst) :negatives))
;               (len (access linear-pot (car pot-lst) :positives))
;               (number-of-polys (cdr pot-lst))))))