[acl2/acl2] cf21dc: aignet reasoning improvements

[GitHub]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: cf21dc39af22edbce6aa505d552a339e167cf913
https://github.com/acl2/acl2/commit/cf21dc39af22edbce6aa505d552a339e167cf913
Author: Sol Swords <ssw...@centtech.com>
Date: 2017-04-24 (Mon, 24 Apr 2017)

Changed paths:
M books/centaur/aig/aig-sat.lisp
M books/centaur/aignet/aig-cnf.lisp
M books/centaur/aignet/aiger.lisp
M books/centaur/aignet/aignet-absstobj.lisp
M books/centaur/aignet/aignet-logic-interface.lisp
M books/centaur/aignet/aignet-logic.lisp
M books/centaur/aignet/cnf.lisp
M books/centaur/aignet/construction.lisp
M books/centaur/aignet/copying.lisp
M books/centaur/aignet/eval.lisp
M books/centaur/aignet/from-hons-aig.lisp
M books/centaur/aignet/levels.lisp
M books/centaur/aignet/prune.lisp
M books/centaur/aignet/semantics.lisp
M books/centaur/aignet/top.lisp
R books/centaur/aignet/types.lisp
M books/centaur/aignet/vecsim.lisp
M books/centaur/gl/bfr-satlink.lisp
M books/centaur/misc/iter.lisp
M books/std/util/defenum.lisp

Log Message:
-----------
aignet reasoning improvements


Commit: fea9630277b6afded9fc50bbf2050e96e6da2854
https://github.com/acl2/acl2/commit/fea9630277b6afded9fc50bbf2050e96e6da2854
Author: Sol Swords <ssw...@centtech.com>
Date: 2017-04-24 (Mon, 24 Apr 2017)

Changed paths:
M axioms.lisp
M basis-a.lisp
M books/add-ons/hash-stobjs.lisp
M books/centaur/sv/svex/4vec.lisp
M books/clause-processors/SULFA/Makefile
M books/clause-processors/SULFA/books/sat/sat.lisp
A books/demos/register-invariant-risk-support.acl2
A books/demos/register-invariant-risk-support.lisp
A books/demos/register-invariant-risk.acl2
A books/demos/register-invariant-risk.lisp
R books/kestrel/utilities/applicability-conditions-tests.lisp
R books/kestrel/utilities/applicability-conditions.lisp
M books/kestrel/utilities/characters.lisp
A books/kestrel/utilities/doublets-tests.lisp
A books/kestrel/utilities/doublets.lisp
M books/kestrel/utilities/integers-from-to.lisp
A books/kestrel/utilities/named-formulas-tests.lisp
A books/kestrel/utilities/named-formulas.lisp
M books/kestrel/utilities/top.lisp
M books/misc/check-acl2-exports.lisp
A books/projects/fm9001/Makefile
A books/projects/fm9001/README
A books/projects/fm9001/acl2-customization.lsp
A books/projects/fm9001/alu-spec.lisp
A books/projects/fm9001/approx.lisp
A books/projects/fm9001/assoc-eq-value.lisp
A books/projects/fm9001/cert.acl2
A books/projects/fm9001/chip.lisp
A books/projects/fm9001/constants.lisp
A books/projects/fm9001/control-modules.lisp
A books/projects/fm9001/control.lisp
A books/projects/fm9001/core-alu.lisp
A books/projects/fm9001/de.lisp
A books/projects/fm9001/dual-port-ram.lisp
A books/projects/fm9001/expand-fm9001-macros.lisp
A books/projects/fm9001/expand-fm9001.lisp
A books/projects/fm9001/extend-immediate.lisp
A books/projects/fm9001/f-functions.lisp
A books/projects/fm9001/fast-zero.lisp
A books/projects/fm9001/final-reset.lisp
A books/projects/fm9001/flags.lisp
A books/projects/fm9001/fm9001-hardware.lisp
A books/projects/fm9001/fm9001-memory.lisp
A books/projects/fm9001/fm9001-spec.lisp
A books/projects/fm9001/hard-spec.lisp
A books/projects/fm9001/list-rewrites.lisp
A books/projects/fm9001/macros.lisp
A books/projects/fm9001/memory.lisp
A books/projects/fm9001/monotonicity-macros.lisp
A books/projects/fm9001/package.lsp
A books/projects/fm9001/pad-vectors.lisp
A books/projects/fm9001/pg-theory.lisp
A books/projects/fm9001/portcullis-constants.lsp
A books/projects/fm9001/portcullis.acl2
A books/projects/fm9001/portcullis.lisp
A books/projects/fm9001/post-alu.lisp
A books/projects/fm9001/pre-alu.lisp
A books/projects/fm9001/primitives.lisp
A books/projects/fm9001/primp-database.lisp
A books/projects/fm9001/proofs.lisp
A books/projects/fm9001/reg.lisp
A books/projects/fm9001/regfile.lisp
A books/projects/fm9001/store-resultp.lisp
A books/projects/fm9001/t-or-nor.lisp
A books/projects/fm9001/tree-number.lisp
A books/projects/fm9001/tv-alu-help.lisp
A books/projects/fm9001/tv-dec-pass.lisp
A books/projects/fm9001/tv-if.lisp
A books/projects/fm9001/unbound.lisp
A books/projects/fm9001/utils.lisp
A books/projects/fm9001/v-equal.lisp
A books/projects/fm9001/v-inc4.lisp
A books/projects/fm9001/vector-macros.lisp
A books/projects/fm9001/vector-module.lisp
M books/projects/x86isa/Makefile
M books/projects/x86isa/doc.lisp
M books/projects/x86isa/machine/instructions/x86-conditional-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-exchange-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-push-and-pop-instructions.lisp
M books/projects/x86isa/machine/x86-environment.lisp
M books/projects/x86isa/machine/x86-ia32e-segmentation.lisp
M books/projects/x86isa/machine/x86-rflags-spec.lisp
M books/projects/x86isa/machine/x86-top-level-memory.lisp
M books/projects/x86isa/proofs/utilities/general-memory-utils.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-top.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy-init.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy.lisp
M books/projects/x86isa/proofs/zeroCopy/non-marking-mode/zeroCopy.lisp
M books/projects/x86isa/utils/utilities.lisp
M books/rtl/rel11/lib/defs.lisp
M books/rtl/rel11/lib/float.lisp
M books/rtl/rel11/rel9-rtl-pkg/arithmetic/expo-proofs.lisp
M books/rtl/rel11/rel9-rtl-pkg/arithmetic/expo.lisp
M books/rtl/rel11/rel9-rtl-pkg/lib/add.lisp
M books/rtl/rel11/rel9-rtl-pkg/lib/bvecp-raw-helpers.lisp
M books/rtl/rel11/rel9-rtl-pkg/lib/float.lisp
M books/rtl/rel11/rel9-rtl-pkg/lib/round.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib1.delta1/bvecp-raw-helpers.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib1.delta1/float.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib1.delta1/round.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib1.delta2/float.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib1/bvecp-raw-helpers.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib1/float.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib1/round.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib2.delta1/bvecp-raw-helpers-proofs.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib2.delta1/bvecp-raw-helpers.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib2.delta1/float-new-proofs.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib2.delta1/float-new.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib2.delta1/float-proofs.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib2.delta1/float.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib2.delta1/round-new-proofs.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib2.delta1/round-new.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib2.delta1/round-proofs.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib2.delta1/round.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib2/bvecp-raw-helpers.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib2/float.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib2/round.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib3.delta2/bvecp-raw-helpers.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib3.delta2/float.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib3.delta2/round.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib3.delta3/round.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib3/bvecp-raw-helpers.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib3/float.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/lib3/round.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/away-proofs.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/away.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/bitn-proofs.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/bitn.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/bits-proofs.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/bits.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/bvecp-lemmas.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/drnd-original.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/encode.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/float.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/near+-proofs.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/near+.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/near-proofs.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/near.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/oddr-proofs.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/oddr.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/rnd.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/sticky-proofs.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/sticky.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/trunc-proofs.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/trunc.lisp
M books/rtl/rel11/support/definitions.lisp
M books/rtl/rel11/support/excps.lisp
M books/rtl/rel11/support/old-round.lisp
M books/rtl/rel11/support/sqrt.lisp
M books/rtl/rel11/support/verify-guards.lisp
M books/system/doc/acl2-doc.lisp
M books/workshops/2017/README
R books/workshops/2017/chau/fm9001/support/Makefile
R books/workshops/2017/chau/fm9001/support/README
R books/workshops/2017/chau/fm9001/support/acl2-customization.lsp
R books/workshops/2017/chau/fm9001/support/alu-spec.lisp
R books/workshops/2017/chau/fm9001/support/approx.lisp
R books/workshops/2017/chau/fm9001/support/assoc-eq-value.lisp
R books/workshops/2017/chau/fm9001/support/cert.acl2
R books/workshops/2017/chau/fm9001/support/chip.lisp
R books/workshops/2017/chau/fm9001/support/constants.lisp
R books/workshops/2017/chau/fm9001/support/control-modules.lisp
R books/workshops/2017/chau/fm9001/support/control.lisp
R books/workshops/2017/chau/fm9001/support/core-alu.lisp
R books/workshops/2017/chau/fm9001/support/de.lisp
R books/workshops/2017/chau/fm9001/support/dual-port-ram.lisp
R books/workshops/2017/chau/fm9001/support/expand-fm9001-macros.lisp
R books/workshops/2017/chau/fm9001/support/expand-fm9001.lisp
R books/workshops/2017/chau/fm9001/support/extend-immediate.lisp
R books/workshops/2017/chau/fm9001/support/f-functions.lisp
R books/workshops/2017/chau/fm9001/support/fast-zero.lisp
R books/workshops/2017/chau/fm9001/support/final-reset.lisp
R books/workshops/2017/chau/fm9001/support/flags.lisp
R books/workshops/2017/chau/fm9001/support/fm9001-hardware.lisp
R books/workshops/2017/chau/fm9001/support/fm9001-memory.lisp
R books/workshops/2017/chau/fm9001/support/fm9001-spec.lisp
R books/workshops/2017/chau/fm9001/support/hard-spec.lisp
R books/workshops/2017/chau/fm9001/support/list-rewrites.lisp
R books/workshops/2017/chau/fm9001/support/macros.lisp
R books/workshops/2017/chau/fm9001/support/memory.lisp
R books/workshops/2017/chau/fm9001/support/monotonicity-macros.lisp
R books/workshops/2017/chau/fm9001/support/package.lsp
R books/workshops/2017/chau/fm9001/support/pad-vectors.lisp
R books/workshops/2017/chau/fm9001/support/pg-theory.lisp
R books/workshops/2017/chau/fm9001/support/portcullis-constants.lsp
R books/workshops/2017/chau/fm9001/support/portcullis.acl2
R books/workshops/2017/chau/fm9001/support/portcullis.lisp
R books/workshops/2017/chau/fm9001/support/post-alu.lisp
R books/workshops/2017/chau/fm9001/support/pre-alu.lisp
R books/workshops/2017/chau/fm9001/support/primitives.lisp
R books/workshops/2017/chau/fm9001/support/primp-database.lisp
R books/workshops/2017/chau/fm9001/support/proofs.lisp
R books/workshops/2017/chau/fm9001/support/reg.lisp
R books/workshops/2017/chau/fm9001/support/regfile.lisp
R books/workshops/2017/chau/fm9001/support/store-resultp.lisp
R books/workshops/2017/chau/fm9001/support/t-or-nor.lisp
R books/workshops/2017/chau/fm9001/support/tree-number.lisp
R books/workshops/2017/chau/fm9001/support/tv-alu-help.lisp
R books/workshops/2017/chau/fm9001/support/tv-dec-pass.lisp
R books/workshops/2017/chau/fm9001/support/tv-if.lisp
R books/workshops/2017/chau/fm9001/support/unbound.lisp
R books/workshops/2017/chau/fm9001/support/utils.lisp
R books/workshops/2017/chau/fm9001/support/v-equal.lisp
R books/workshops/2017/chau/fm9001/support/v-inc4.lisp
R books/workshops/2017/chau/fm9001/support/vector-macros.lisp
R books/workshops/2017/chau/fm9001/support/vector-module.lisp
M defpkgs.lisp
M defuns.lisp
M doc.lisp
M other-events.lisp
M rewrite.lisp
M translate.lisp

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


Commit: 572c5a3cf9fe0b335dfcb0b979295f49c69356ba
https://github.com/acl2/acl2/commit/572c5a3cf9fe0b335dfcb0b979295f49c69356ba
Author: Sol Swords <ssw...@centtech.com>
Date: 2017-04-25 (Tue, 25 Apr 2017)

Changed paths:
M books/centaur/aig/faig-purebool-p.lisp

Log Message:
-----------
fix problem due to previous change


Commit: 108e664c7c6725bf3b0118089e76c34e55a1aa68
https://github.com/acl2/acl2/commit/108e664c7c6725bf3b0118089e76c34e55a1aa68
Author: Sol Swords <ssw...@centtech.com>
Date: 2017-04-25 (Tue, 25 Apr 2017)

Changed paths:
A books/kestrel/utilities/error-checking-tests.lisp
A books/kestrel/utilities/error-checking.lisp
M books/kestrel/utilities/top.lisp

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


Compare: https://github.com/acl2/acl2/compare/8be9c89ff871...108e664c7c67

[GitHub]

Branch: refs/heads/master