Merge remote-tracking branch 'remotes/origin/master'

books/centaur/sv/cosims/run.lsp

@@ -172,6 +172,7 @@
         ;; indicates error -- but allow for now since iverilog is a new/optional feature
         ;; (er hard? 'output-lines-iv "~@0" lines)
         (mv nil state))
+       (lines (drop-comment-lines lines))
        ((unless (eql (len lines) (len *input-lines*)))
         (er hard? 'output-lines-iv "Wrong number of lines read: ~x0, expecting ~x1"
             (len lines) (len *input-lines*))

books/misc/expander.lisp

@@ -666,15 +666,7 @@ directly with ACL2.</p>
 ; decided to avoid extending current-clause using that body.
 
                                      :current-clause current-clause
-                                     :force-info
-
-; It probably makes sense simply to set the following to t.  Up through October
-; 2016 it has been 'weak, so we leave it that way for backward compatibility --
-; for now.
-
-                                     (if (ffnnamep-lst 'if current-clause)
-                                         'weak
-                                       t)))
+                                     :force-info t))
                             (pts
                              ;; (current-clause-pts (enumerate-elements current-clause 0))
                              nil))
@@ -684,7 +676,9 @@ directly with ACL2.</p>
                                          pts
                                          (access rewrite-constant
                                                  rcnst :force-info)
-                                         nil wrld ens
+                                         nil wrld
+                                         (access rewrite-constant rcnst
+                                                 :current-enabled-structure)
                                          (access rewrite-constant rcnst
                                                  :oncep-override)
                                          state)
@@ -811,7 +805,9 @@ directly with ACL2.</p>
                                                (er-let* ((new-ttree
                                                           (prove-loop1
                                                            1 nil pairs pspv
-                                                           thints ens wrld
+                                                           thints
+                                                           ens
+                                                           wrld
                                                            ctx state)))
                                                  (let* ((runes
                                                          (all-runes-in-ttree
@@ -1561,3 +1557,117 @@ x=0. Maybe we should think about how to do this and do it.
 
 
 |#
+
+; Finally, we add defsimp.  Documentation will hopefully come later.  For now,
+; here are a couple of examples:
+
+; (defsimp (car (cons x y)) nil test1 :print :only)
+; (defsimp (car (cons x y)) nil test2) ; same as :print :all
+; (defsimp (+ x 0) ((integerp x)) test3 :print t :rule-classes nil)
+
+; Here is an example with forcing.
+
+; (defun my-true (x) (if (consp x) (my-true (cdr x)) t))
+; (in-theory (disable (:t my-true)))
+; (defstub p1 (x) t)
+; (defaxiom p1-ax (implies (force (my-true x)) (equal (p1 x) t)))
+; (defsimp (p1 a) nil foo)
+
+(defun defsimp-fn
+  (term hyps equiv state in-theory expand translate-flg must-rewrite-flg
+        defthm-name rule-classes print)
+
+; See tool2-fn.  Here we create a corresponding defthm event.
+
+; Equiv is the equivalence relation, which is implicitly 'equal if equiv is t
+; or nil.
+
+  (let ((ctx 'defsimp)
+        (wrld (w state))
+        (ens (ens state))
+        (hints `(,@(and (not (eq in-theory :none))
+                        `((:in-theory ,in-theory)))
+                 ,@(and expand
+                        `((:expand ,expand))))))
+    (er-let* ((runes/new-term/assumptions
+               (tool2-fn0 term hyps equiv ctx ens wrld state hints
+                          t ; prove-assumptions
+                          t ; inhibit-output
+                          translate-flg
+                          nil ; print-flg
+                          must-rewrite-flg)))
+      (let ((runes (car runes/new-term/assumptions))
+            (new-term (cadr runes/new-term/assumptions))
+            (assumptions (cddr runes/new-term/assumptions)))
+        (cond
+         (assumptions
+          (er soft ctx
+              "Implementation error: assumptions were unexpectedly forced.  ~
+               Please contact the maintainers of books/misc/expander.lisp"))
+         ((not (true-listp hyps))
+          (er soft ctx
+              "The given hypotheses must be a true list, but ~x0 is not."
+              hyps))
+         (t
+          (let* ((formula
+                  (if hyps
+                      (list 'implies
+                            (if (cdr hyps)
+                                (cons 'and hyps)
+                              (car hyps))
+                            (list (or equiv 'equal) term new-term))
+                    (list (or equiv 'equal) term new-term)))
+                 (runes+ `(union-theories (theory 'minimal-theory)
+                                          ',runes))
+                 (event-form
+                  `(defthm ,defthm-name
+                     ,formula
+                     :instructions
+                     ((:in-theory ,runes+)
+                      ,@(and hyps '(:promote))
+                      (:dive 1)
+                      (:then (:s :backchain-limit 500)
+
+; Deal with forced assumptions, if any.
+
+                             (:prove
+                              ,@(and expand
+                                     `(:hints
+                                       (("Goal" :expand ,expand))))))
+                      :up
+                      :s-prop)
+                     ,@(and (not (eq rule-classes :rewrite))
+                            `(:rule-classes ,rule-classes)))))
+            (pprogn
+             (cond
+              ((eq print t)
+               (fms "New term:~|~x0~|~%"
+                    (list (cons #\0 new-term))
+                    (standard-co state) state nil))
+              ((eq print :all)
+               (fms "~x0~|~%"
+                    (list (cons #\0 event-form))
+                    (standard-co state) state nil))
+              (t state))
+             (value event-form)))))))))
+
+(defmacro defsimp (term hyps defthm-name
+                        &key
+                        (rule-classes ':rewrite)
+                        (in-theory ':none)
+                        expand
+                        equiv
+                        (translate-flg 't)
+                        (must-rewrite-flg 't)
+                        (print ':all))
+  (let ((form `(defsimp-fn ',term ',hyps ',equiv state ',in-theory ',expand
+                 ',translate-flg
+                 ,must-rewrite-flg ; evaluated, as for tool2 macro
+                 ',defthm-name ',rule-classes ',print)))
+
+    `(with-output :off :all :on error
+       ,(if (eq print :only)
+            `(make-event (er-let* ((form ,form))
+                           (value (list 'value-triple
+                                        (list 'quote form)))))
+          `(make-event ,form)))))

books/system/doc/acl2-doc.lisp

@@ -74060,6 +74060,36 @@ it."
 ; constant is used in chk-embedded-event-form; the big quoted list was formerly
 ; there, but Eric Smith found it useful to have it installed as a defconst.
 
+; With the change for :s to use linear arithmetic, we now flatten the governors
+; when creating the full set of assumptions.  That may not make a difference in
+; the type-alist computed, but it can help with derivation of the linear
+; pot-lst.
+
+; Here are a couple of examples where the additional use of linear arithmetic
+; strengthens the :s command.  Neither of the two theorems at the end were
+; proved before that change.
+
+;   (defstub p1 (x) t)
+;   (defstub p2 (x) t)
+;   (defstub p3 (x) t)
+;   (defstub p4 (x) t)
+;   (defaxiom p1-type (integerp (p1 x)) :rule-classes :type-prescription)
+;   (defaxiom p2-type (integerp (p2 x)) :rule-classes :type-prescription)
+;   (defaxiom p3-type (integerp (p3 x)) :rule-classes :type-prescription)
+;   (defaxiom p4-prop (implies (< (p1 x) (p3 x)) (p4 x)))
+;   (in-theory (disable (tau-system)))
+;   (defthm test1
+;     (implies (and (< (p1 a) (p2 a)) (< (p2 a) (p3 a)))
+;              (p4 a))
+;     :rule-classes nil
+;     :instructions (:promote (s :backchain-limit 500)))
+;   (defthm test2
+;     (if (and (< (p1 a) (p2 a)) (< (p2 a) (p3 a)))
+;         (p4 a)
+;       t)
+;     :rule-classes nil
+;     :instructions ((:dv 2) (s :backchain-limit 500) :top :s-prop))
+;
   :parents (release-notes)
   :short "ACL2 Version  7.3 (xx, xxxx) Notes"
   :long "<p>NOTE!  New users can ignore these release notes, because the @(see
@@ -74408,6 +74438,12 @@ it."
  hints) when editing a proof-builder command by copying hints from an event
  being developed.</p>
 
+ <p>By default, the @(see proof-builder) command @(':s') now uses contextual
+ information when doing linear arithmetic.  The new keyword argument
+ @(':linear') can be set to @('nil') to get the previous behavior.  See @(see
+ acl2-pc::s).  Thanks to Eric Smith for requests that led us to make this
+ change.</p>
+
  <h3>New Features</h3>
 
  <p>New optional arguments allow the @(tsee pso) utility to restrict output to
@@ -115433,7 +115469,7 @@ simplify the current subterm"
         expanded during the rewriting process
 
   General Form:
-  (s &key rewrite normalize backchain-limit repeat in-theory hands-off
+  (s &key rewrite linear normalize backchain-limit repeat in-theory hands-off
           expand)
  })
 
@@ -115454,6 +115490,19 @@ simplify the current subterm"
  <p>When non-@('nil'), instructs the system to use ACL2's rewriter (or,
  something close to it) during simplification.</p>
 
+ @({
+  :linear -- default t (except, default nil if :rewrite has value nil)
+ })
+
+ <p>When non-@('nil'), instructs the system to use ACL2's <see topic='@(url
+ linear-arithmetic)'>linear arithmetic</see> to build a suitable context (a
+ ``linear pot list'') from the assumptions
+ (the top-level hypotheses and the <see topic='@(url
+ acl2-pc::hyps)'>governors</see>).  Note that linear arithmetic is used by the
+ rewriter regardless; by default, when @(':s') invokes the rewriter then linear
+ arithmetic can take advantage of the information in the top-level hypotheses
+ and the governors.</p>
+
  @({
   :normalize -- default t
  })

doc.lisp

@@ -73093,6 +73093,12 @@ Changes to Existing Features
   editing a proof-builder command by copying hints from an event
   being developed.
 
+  By default, the [proof-builder] command :s now uses contextual
+  information when doing linear arithmetic. The new keyword argument
+  :linear can be set to nil to get the previous behavior. See
+  [ACL2-pc::s]. Thanks to Eric Smith for requests that led us to make
+  this change.
+
 
 New Features
 
@@ -115851,7 +115857,7 @@ Subtopics
           expanded during the rewriting process
 
     General Form:
-    (s &key rewrite normalize backchain-limit repeat in-theory hands-off
+    (s &key rewrite linear normalize backchain-limit repeat in-theory hands-off
             expand)
 
   Simplify the current subterm according to the keyword parameters
@@ -115870,6 +115876,16 @@ Subtopics
   When non-nil, instructs the system to use ACL2's rewriter (or,
   something close to it) during simplification.
 
+    :linear -- default t (except, default nil if :rewrite has value nil)
+
+  When non-nil, instructs the system to use ACL2's linear arithmetic
+  (see [LINEAR-ARITHMETIC]) to build a suitable context (a ``linear
+  pot list'') from the assumptions (the top-level hypotheses and the
+  governors (see [ACL2-PC::HYPS])). Note that linear arithmetic is
+  used by the rewriter regardless; by default, when :s invokes the
+  rewriter then linear arithmetic can take advantage of the
+  information in the top-level hypotheses and the governors.
+
     :normalize -- default t
 
   When non-nil, instructs the system to use [normalization] (as