[acl2/acl2] cecec3: x86isa: Added a general version of the popcount pr...

[GitHub]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: cecec362eeab777da002332414b0c5dd5159f5a0
https://github.com/acl2/acl2/commit/cecec362eeab777da002332414b0c5dd5159f5a0
Author: Shilpi Goel <shi...@cs.utexas.edu>
Date: 2016-10-01 (Sat, 01 Oct 2016)

Changed paths:
M books/projects/x86isa/proofs/dataCopy/dataCopy.lisp
A books/projects/x86isa/proofs/popcount/popcount-general.lisp
M books/projects/x86isa/proofs/popcount/popcount.lisp
M books/projects/x86isa/proofs/top.lisp

Log Message:
-----------
x86isa: Added a general version of the popcount proof that doesn't suffer from the (create-x86) problem.


Commit: 2ce3d3828fa3165a7bf9a13ad6e8c1e7d6bf5677
https://github.com/acl2/acl2/commit/2ce3d3828fa3165a7bf9a13ad6e8c1e7d6bf5677
Author: Shilpi Goel <shi...@cs.utexas.edu>
Date: 2016-10-01 (Sat, 01 Oct 2016)

Changed paths:
M acl2-fns.lisp
M books/GNUmakefile
M books/README.md
M books/arithmetic-5/README
M books/centaur/sv/cosims/Makefile
A books/centaur/sv/cosims/alwaysmulti/no_ncv
A books/centaur/sv/cosims/alwaysmulti/spec.sv
A books/centaur/sv/cosims/alwaysmulti/twovalued
A books/centaur/sv/cosims/case_wilds/spec.sv
A books/centaur/sv/cosims/pp1/spec.sv
A books/centaur/sv/cosims/pp2/spec.sv
A books/centaur/sv/cosims/pp3/spec.sv
A books/centaur/sv/cosims/pp4/spec.sv
A books/centaur/sv/cosims/pp5/spec.sv
A books/centaur/sv/cosims/protect/spec.sv
M books/centaur/sv/cosims/run.lsp
A books/centaur/sv/cosims/un_plus/no_iv
A books/centaur/sv/failtest/protect1.v
A books/centaur/sv/failtest/protect2.v
M books/centaur/sv/mods/lhs.lisp
M books/centaur/sv/svex/eval.lisp
M books/centaur/sv/svex/rewrite.lisp
A books/centaur/sv/svex/select.lisp
M books/centaur/sv/vl/expr.lisp
M books/centaur/sv/vl/moddb.lisp
M books/centaur/sv/vl/svstmt-compile.lisp
M books/centaur/sv/vl/svstmt.lisp
M books/centaur/sv/vl/vl-svstmt.lisp
M books/centaur/vl/kit/lint.lisp
M books/centaur/vl/lint/lucid.lisp
M books/centaur/vl/linttest/Makefile
M books/centaur/vl/linttest/bits/check.rb
M books/centaur/vl/linttest/dpi/check.rb
M books/centaur/vl/linttest/duplicates/check.rb
M books/centaur/vl/linttest/extension/check.rb
M books/centaur/vl/linttest/fussy/check.rb
M books/centaur/vl/linttest/implicit/check.rb
M books/centaur/vl/linttest/leftright/check.rb
M books/centaur/vl/linttest/lucid/check.rb
M books/centaur/vl/linttest/multi/check.rb
M books/centaur/vl/linttest/oddexpr/check.rb
M books/centaur/vl/linttest/overflow/check.rb
M books/centaur/vl/linttest/params/check.rb
M books/centaur/vl/linttest/portcheck/check.rb
M books/centaur/vl/linttest/sameports/check.rb
M books/centaur/vl/linttest/shadowcheck/check.rb
M books/centaur/vl/linttest/translateoff/check.rb
M books/centaur/vl/linttest/trunc/check.rb
M books/centaur/vl/loader/lexer/strings.lisp
M books/centaur/vl/loader/lexer/tests.lisp
M books/centaur/vl/loader/lexer/top.lisp
M books/centaur/vl/loader/parser/udps.lisp
M books/centaur/vl/loader/preprocessor/tests.lisp
M books/centaur/vl/loader/preprocessor/top.lisp
M books/centaur/vl/loader/top.lisp
M books/centaur/vl/mlib/fmt.lisp
M books/centaur/vl/server/describe.lisp
M books/centaur/vl/transforms/unparam/top.lisp
M books/centaur/vl/util/sum-nats.lisp
M books/doc/top.lisp
M books/kestrel/utilities/applicability-conditions-tests.lisp
M books/kestrel/utilities/characters-tests.lisp
M books/kestrel/utilities/copy-def.lisp
M books/kestrel/utilities/defchoose-queries-tests.lisp
A books/kestrel/utilities/defthmr.lisp
M books/kestrel/utilities/defun-sk-queries-tests.lisp
M books/kestrel/utilities/fresh-names-tests.lisp
M books/kestrel/utilities/install-not-norm-event-tests.lisp
M books/kestrel/utilities/integers-from-to-tests.lisp
M books/kestrel/utilities/numbered-names-tests.lisp
M books/kestrel/utilities/strings-tests.lisp
M books/kestrel/utilities/terms-tests.lisp
M books/kestrel/utilities/testing-tests.lisp
M books/kestrel/utilities/testing.lisp
M books/kestrel/utilities/top.lisp
M books/kestrel/utilities/world-queries-tests.lisp
M books/meta/README
M books/misc/dft.lisp
A books/projects/simple-url-parser/parse-url.lisp
M books/projects/x86isa/machine/x86-other-non-det-raw.lsp
M books/projects/x86isa/tools/execution/exec-loaders/mach-o/mach-o-reader.lisp
M books/projects/x86isa/utils/decoding-utilities.lisp
A books/std/io/read-file-lines-no-newlines.lisp
M books/std/io/read-file-lines.lisp
M books/std/io/top.lisp
M books/system/doc/acl2-doc.lisp
M books/system/doc/render-doc-base.lisp
M books/xdoc/display.lisp
A books/xdoc/save-rendered.lisp
M defthm.lisp
M defuns.lisp
M doc.lisp
M other-events.lisp

Log Message:
-----------
Merge


Commit: 691db7e20a53697063306f6262902bb66f429b25
https://github.com/acl2/acl2/commit/691db7e20a53697063306f6262902bb66f429b25
Author: MattKaufmann <kauf...@cs.utexas.edu>
Date: 2016-10-01 (Sat, 01 Oct 2016)

Changed paths:
M books/projects/x86isa/proofs/dataCopy/dataCopy.lisp
A books/projects/x86isa/proofs/popcount/popcount-general.lisp
M books/projects/x86isa/proofs/popcount/popcount.lisp
M books/projects/x86isa/proofs/top.lisp

Log Message:
-----------
Merge pull request #649 from shigoel/cleanup

x86isa: Added a general version of the popcount theorem


Compare: https://github.com/acl2/acl2/compare/156985b17fc5...691db7e20a53

[GitHub]

Branch: refs/heads/master