File: linear-b.lisp

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (853 lines) | stat: -rw-r--r-- 36,835 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
; ACL2 Version 3.1 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2006  University of Texas at Austin

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

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

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

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

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

(in-package "ACL2")


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


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


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


; Add-polys

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

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

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

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

  (if (good-pot-varp term)
    (mv-let (ts ts-ttree)
      (type-set term force-flag dwp type-alist ancestors ens wrld ttree
                nil nil)
      (cond ((ts-subsetp ts *ts-zero*)
             (list 
              ;; 0 <= term
              (add-linear-terms :rhs term
                                (base-poly ts-ttree
                                           '<=
                                           t
                                           nil))
              ;; term <= 0
              (add-linear-terms :lhs term
                                (base-poly ts-ttree
                                           '<=
                                           t
                                           nil))))
            ((ts-subsetp ts *ts-positive-integer*)
             (list 
              ;; 1 <= term
              (add-linear-terms :lhs *1*
                                :rhs term
                                (base-poly ts-ttree
                                           '<=
                                           t
                                           nil))))
            ((ts-subsetp ts *ts-negative-integer*)
             (list 
              ;; term <= -1
              (add-linear-terms :lhs term
                                :rhs ''-1
                                (base-poly ts-ttree
                                           '<=
                                           t
                                           nil))))
            ((ts-subsetp ts
                         #-:non-standard-analysis *ts-positive-rational*
                         #+:non-standard-analysis *ts-positive-real*)
             (list 
              ;; 0 < term
              (add-linear-terms :rhs term
                                (base-poly ts-ttree
                                           '<
                                           t
                                           nil))))
            ((ts-subsetp ts
                         #-:non-standard-analysis *ts-negative-rational*
                         #+:non-standard-analysis *ts-negative-real*)
             (list 
              ;; term < 0
              (add-linear-terms :lhs term
                                (base-poly ts-ttree
                                           '<
                                           t
                                           nil))))
            ((ts-subsetp ts
                         #-:non-standard-analysis *ts-non-negative-rational*
                         #+:non-standard-analysis *ts-non-negative-real*)
             (list 
              ;; 0 <= term
              (add-linear-terms :rhs term
                                (base-poly ts-ttree
                                           '<=
                                           t
                                           nil))))
            ((ts-subsetp ts
                         #-:non-standard-analysis *ts-non-positive-rational*
                         #+:non-standard-analysis *ts-non-positive-real*)
             (list 
              ;; term <= 0
              (add-linear-terms :lhs term
                                (base-poly ts-ttree
                                           '<=
                                           t
                                           nil))))
            (t
             nil)))
    (er hard 'inverse-polys
        "A presumptive pot-label, ~x0,  has turned out to be illegitimate. ~
         If possible, please send a script reproducing this error ~
         to the authors of ACL2."
        term)))

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

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

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

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

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

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

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

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


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


; Linearize

(mutual-recursion

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

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

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

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

        ((and (logicalp (ffn-symb term) wrld) ; maybe fn is being admitted
              (all-quoteps args)
              (enabled-xfnp (ffn-symb term) ens wrld)
              (not (getprop (ffn-symb term) 'constrainedp nil
                            'current-acl2-world wrld)))
         (mv-let
          (erp val latches)
          (pstk
           (ev-fncall (ffn-symb term)
                      (strip-cadrs args)
                      (f-decrement-big-clock state)
                      nil
                      t))
          (declare (ignore latches))
          (cond
           (erp
            (cond (flg
                   (mv t (cons-term (ffn-symb term) args) ttree))
                  (t (mv nil term ttree))))
           (t (mv t
                  (kwote val)
                  (push-lemma (fn-rune-nume (ffn-symb term) nil t wrld)
                              ttree))))))
        (flg (mv t (cons-term (ffn-symb term) args) ttree))
        (t (mv nil term ttree)))))))

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


(defun poly-set (op poly1 poly2)

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

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

; However, there are two special cases.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                (if positivep

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 Q.E.D.

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

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

        (if positivep

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

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

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

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

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

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

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

; We store ttree in the ttree of the poly.

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

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

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

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

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

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