[acl2/acl2] 895171: Improved the proof-builder's :s command to take mo...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 8951711c5b8db220a35823533f213ef2ca397f4a
https://github.com/acl2/acl2/commit/8951711c5b8db220a35823533f213ef2ca397f4a
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2016-11-28 (Mon, 28 Nov 2016)

Changed paths:
M books/misc/expander.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M proof-builder-b.lisp

Log Message:
-----------
Improved the proof-builder's :s command to take more advantage of linear arithmetic. Tweaked expander to use forcing more often, and added defsimp utility to expander.lisp.

Quoting :doc note-7-3:

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.

Technical additional change, quoting a comment in (defxdoc note-7-3 ...):

; 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.

Below that comment can be found "a couple of examples where the
additional use of linear arithmetic strengthens the :s command".

Modifications to books/misc/expander.lisp:

- Forcing had been avoided in tool2 if any IF call is in the
hypotheses. That is no longer the case (a comment suggested that
this change might come).

- New macro defsimp proves a theorem on correctness of the expander
(tool2-fn) result (thanks, Eric Smith, for the request). I'm
currently planning to document it after it's been used a bit.
Examples are in comments near the end of the file.


Commit: 91b236d55dc4c4ed663c8241f1620eca7b6707cf
https://github.com/acl2/acl2/commit/91b236d55dc4c4ed663c8241f1620eca7b6707cf
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2016-11-28 (Mon, 28 Nov 2016)

Changed paths:
M books/misc/expander.lisp

Log Message:
-----------
Tweaked new utility, defsimp, to deal properly with forcing.


Commit: 6df548e3b25e14d9dc28d67e6ad1b5a237015189
https://github.com/acl2/acl2/commit/6df548e3b25e14d9dc28d67e6ad1b5a237015189
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2016-11-28 (Mon, 28 Nov 2016)

Changed paths:
M books/misc/expander.lisp

Log Message:
-----------
Further expander tweak: use the specified theory, not the current-theory, when forward-chaining.


Compare: https://github.com/acl2/acl2/compare/4dea1f388910...6df548e3b25e

[GitHub]

Branch: refs/heads/testing