[acl2/acl2] 763733: Add several AIGNET transformations, including frai...

[GitHub]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: 763733e4b7ad03667a7f3d32ff90e59b4079588c
https://github.com/acl2/acl2/commit/763733e4b7ad03667a7f3d32ff90e59b4079588c
Author: Sol Swords <ssw...@centtech.com>
Date: 2017-08-17 (Thu, 17 Aug 2017)

Changed paths:
A books/centaur/aignet/abc-wrappers.lisp
A books/centaur/aignet/balance.lisp
A books/centaur/aignet/count.lisp
A books/centaur/aignet/equiv-classes.lisp
A books/centaur/aignet/fraig.lisp
A books/centaur/aignet/observability.lisp
A books/centaur/aignet/transform-utils.lisp
A books/centaur/aignet/transforms.lisp
A books/centaur/gl/bfr-fraig-satlink.acl2
A books/centaur/gl/bfr-fraig-satlink.lisp
A books/centaur/sv/tutorial/sums.lisp
A books/centaur/sv/tutorial/sums.sv

Log Message:
-----------
Add several AIGNET transformations, including fraiging, and a hook into GL to use them before calling SAT


Commit: bac0fece6a7f070d64c61cae10b258a1f430e35d
https://github.com/acl2/acl2/commit/bac0fece6a7f070d64c61cae10b258a1f430e35d
Author: Sol Swords <ssw...@centtech.com>
Date: 2017-08-17 (Thu, 17 Aug 2017)

Changed paths:
M acl2-init.lisp
M axioms.lisp
M books/acl2s/cgen/build-enumcalls.lisp
M books/acl2s/cgen/cert.acl2
M books/acl2s/cgen/incremental-search.lisp
M books/acl2s/cgen/simple-search.lisp
M books/acl2s/cgen/testing-regression.lsp
M books/acl2s/cgen/top.lisp
M books/acl2s/defdata/base.lisp
M books/acl2s/defdata/builtin-combinators.lisp
M books/acl2s/defdata/defdata-core.lisp
M books/acl2s/defdata/defdata-regression.lsp
M books/acl2s/defdata/defdata-util.lisp
M books/acl2s/defdata/enumerators-gen.lisp
M books/acl2s/defdata/random-state.lisp
M books/acl2s/defdata/register-type.lisp
M books/acl2s/defdata/sig.lisp
M books/acl2s/mode-acl2s-dependencies.lisp
M books/add-ons/hash-stobjs.lisp
A books/centaur/misc/try-gl-concls.lisp
M books/doc/relnotes.lisp
M books/doc/top.lisp
M books/kestrel/apt/package.lsp
M books/kestrel/apt/restrict-reference.lisp
M books/kestrel/apt/restrict-tests.lisp
M books/kestrel/apt/restrict.lisp
M books/kestrel/apt/tailrec-reference.lisp
M books/kestrel/apt/tailrec-tests.lisp
M books/kestrel/apt/tailrec.lisp
M books/kestrel/apt/top.lisp
M books/kestrel/utilities/error-checking.lisp
M books/kestrel/utilities/named-formulas.lisp
M books/misc/check-acl2-exports.lisp
M books/projects/apply-model/Makefile
M books/projects/x86isa/doc.lisp
M books/projects/x86isa/machine/instructions/x86-jump-and-loop-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-push-and-pop-instructions.lisp
M books/projects/x86isa/machine/x86-decoding-and-spec-utils.lisp
M books/projects/x86isa/machine/x86-environment.lisp
M books/projects/x86isa/machine/x86-ia32e-paging.lisp
M books/projects/x86isa/machine/x86-programmer-level-memory.lisp
M books/projects/x86isa/machine/x86-top-level-memory.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/portcullis/sharp-dot-constants.lisp
A books/projects/x86isa/proofs/codewalker-examples/acl2-customization.lsp
A books/projects/x86isa/proofs/codewalker-examples/base.lisp
A books/projects/x86isa/proofs/codewalker-examples/cert.acl2
A books/projects/x86isa/proofs/codewalker-examples/factorial.lisp
A books/projects/x86isa/proofs/codewalker-examples/popcount-32.lisp
M books/projects/x86isa/proofs/dataCopy/dataCopy-init.lisp
M books/projects/x86isa/proofs/dataCopy/dataCopy-loop-base.lisp
M books/projects/x86isa/proofs/dataCopy/dataCopy-loop-recur.lisp
M books/projects/x86isa/proofs/dataCopy/dataCopy.lisp
M books/projects/x86isa/proofs/dissertation-examples/clc-stc-programmer-mode.lisp
M books/projects/x86isa/proofs/dissertation-examples/clc-stc-system-level-marking-mode.lisp
M books/projects/x86isa/proofs/dissertation-examples/clc-stc-system-level-non-marking-mode.lisp
M books/projects/x86isa/proofs/factorial/fact-inductive-assertions.lisp
M books/projects/x86isa/proofs/factorial/fact-wormhole-abstraction.lisp
M books/projects/x86isa/proofs/popcount/popcount-general.lisp
M books/projects/x86isa/proofs/popcount/popcount.lisp
M books/projects/x86isa/proofs/powOfTwo/powOfTwo.lisp
M books/projects/x86isa/proofs/top.lisp
M books/projects/x86isa/proofs/utilities/disjoint.lisp
M books/projects/x86isa/proofs/utilities/general-memory-utils.lisp
M books/projects/x86isa/proofs/utilities/programmer-level-mode/programmer-level-memory-utils.lisp
M books/projects/x86isa/proofs/utilities/programmer-level-mode/top.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/bind-free-utils.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/common-system-level-utils.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/gl-lemmas.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-top.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-utils.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/non-marking-mode-top.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/paging/common-paging-lemmas.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/paging/gather-paging-structures.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/paging/la-to-pa-lemmas.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/paging/page-walk-side-effects.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/paging/paging-basics.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/paging/top.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/physical-memory-utils.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/top.lisp
M books/projects/x86isa/proofs/utilities/x86-row-wow-thms.lisp
M books/projects/x86isa/proofs/wordCount/wc-addr-byte.lisp
M books/projects/x86isa/proofs/wordCount/wc.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy-init.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy-part-1.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy-part-2.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy.lisp
M books/projects/x86isa/proofs/zeroCopy/non-marking-mode/zeroCopy.lisp
A books/projects/x86isa/tools/execution/examples/push.c
M books/projects/x86isa/tools/execution/top.lisp
M books/projects/x86isa/tools/execution/x86-init-page-tables.lisp
M books/projects/x86isa/tools/execution/x86-init-state.lisp
M books/system/doc/acl2-doc.lisp
M books/tools/flag.lisp
M boot-strap-pass-2.lisp
M defuns.lisp
M doc.lisp
M other-events.lisp
M translate.lisp

Log Message:
-----------
Merge branch 'testing' of github.com:acl2/acl2


Commit: cb0af2364444fdca922a6f19b8bc5b921afc525a
https://github.com/acl2/acl2/commit/cb0af2364444fdca922a6f19b8bc5b921afc525a
Author: Sol Swords <ssw...@centtech.com>
Date: 2017-08-17 (Thu, 17 Aug 2017)

Changed paths:
M books/centaur/aignet/abc-wrappers.lisp
M books/centaur/aignet/balance.lisp
M books/centaur/aignet/fraig.lisp
M books/centaur/aignet/observability.lisp
M books/centaur/aignet/transforms.lisp
M books/centaur/gl/bfr-fraig-satlink.lisp
M books/doc/relnotes.lisp
M books/doc/top.lisp

Log Message:
-----------
fix up some documentation and add release notes for some previous commits


Compare: https://github.com/acl2/acl2/compare/14d07aa39cbe...cb0af2364444

[GitHub]

Branch: refs/heads/master