[acl2/acl2] bd8dfc: the acc enum for range types now features a more i...

0 views
Skip to first unread message

GitHub

unread,
Jun 23, 2017, 5:10:37 PM6/23/17
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: bd8dfce43efc2b98fafb1bd8fe03ec0449fc5c29
https://github.com/acl2/acl2/commit/bd8dfce43efc2b98fafb1bd8fe03ec0449fc5c29
Author: Harsh Raju Chamarthi <harshraju...@ge.com>
Date: 2017-06-23 (Fri, 23 Jun 2017)

Changed paths:
M books/acl2s/defdata/builtin-combinators.lisp
M books/acl2s/defdata/defdata-util.lisp

Log Message:
-----------
the acc enum for range types now features a more involved sampling test data distribution


Commit: de95d76cc530ba204bbd841a08b8681a52ab90c6
https://github.com/acl2/acl2/commit/de95d76cc530ba204bbd841a08b8681a52ab90c6
Author: Harsh Raju Chamarthi <harshraju...@ge.com>
Date: 2017-06-23 (Fri, 23 Jun 2017)

Changed paths:
M books/acl2s/cgen/acl2s-parameter.lisp
M books/acl2s/cgen/top.lisp

Log Message:
-----------
By default use-fixers is disabled and also testing-enabled is not set in top, instead users have to manually enable it before using non-naive mode of cgen


Commit: e9e54825f182f3d68aa60736a63b8a255935a807
https://github.com/acl2/acl2/commit/e9e54825f182f3d68aa60736a63b8a255935a807
Author: Harsh Raju Chamarthi <harshraju...@ge.com>
Date: 2017-06-23 (Fri, 23 Jun 2017)

Changed paths:
M books/acl2s/cgen/build-enumcalls.lisp

Log Message:
-----------
only use per-thm or per-test? range inference is the computed range is a subtype of the original defdata range type


Commit: 95685d07e73b7b3de965bf6f5bc8cbe3d7246c98
https://github.com/acl2/acl2/commit/95685d07e73b7b3de965bf6f5bc8cbe3d7246c98
Author: David L. Rager <rag...@gmail.com>
Date: 2017-06-23 (Fri, 23 Jun 2017)

Changed paths:
M books/acl2s/cgen/acl2s-parameter.lisp
M books/acl2s/cgen/build-enumcalls.lisp
M books/acl2s/cgen/top.lisp
M books/acl2s/defdata/builtin-combinators.lisp
M books/acl2s/defdata/defdata-util.lisp

Log Message:
-----------
Merge pull request #745 from harshrc/master

Use a better sampling distribution for range types. Minor change in ACL2s defaults.


Compare: https://github.com/acl2/acl2/compare/57d4dd99b9af...95685d07e73b

GitHub

unread,
Jun 23, 2017, 5:46:43 PM6/23/17
to acl2-...@googlegroups.com
Branch: refs/heads/master
Reply all
Reply to author
Forward
0 new messages