#
08d7a558 |
|
23-Oct-2014 |
Piotr Trojanek <piotr.trojanek@gmail.com> |
trailing newlines in *.{sml,sig} files from src/ removed Trailing newlines from SML files in src/ were rendered in HTML documentation.
|
#
177e6ef8 |
|
21-Dec-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get integer self-test to work with Poly/ML.
|
#
9d239a9d |
|
05-Jul-2007 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add a test case for Cooper's algorithm corresponding to the S E N D + M O R E ---------- M O N E Y puzzle. This causes it to break. Don't bother testing it with Omega as all the inequality constraints would force DNF normalisation to generate 2^28 clauses. (Hope to fix Cooper in the near future.)
|
#
0b822887 |
|
01-Oct-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
A fix for the bug reported in hol-info by Arthur van Leeuwen. Also extended the testing programs to be able to check goals (like the one he provided as an example). The problem is that his goal had an assumption where the non-presburger sub-term was in the scope of a universal quantifier. (If it was a existential then it could be pulled out, turned into a universal, stripped, allowing access to the non-presburger sub-term so that it could be generalised away.) The conversion still doesn't cope with this situation, but the tactics now won't attempt to include assumptions that look like that.
|
#
afad11b5 |
|
18-Feb-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Reorganised test programs so that regression suite is shared between omega and cooper tests. Also added useful Perl program for doing comparisons between test runs.
|
#
6ba3dbe7 |
|
20-Dec-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Removed last vestiges of push_exvar_to_bot, which exposed me to painful name-choice questions in marked fashion, and also added the 3-5 coins problem to my test suite. I'm still not entirely free of choice of name problems, and should probably switch back to the built-in EXISTS_OR_CONV in the meantime.
|
#
aea90a98 |
|
18-Dec-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Testing routine now needs to use DB.fetch.
|
#
48fa2c3b |
|
12-Oct-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixed a couple of bugs and added a problem that exhibited one of them to the regression test suite.
|
#
486741c8 |
|
04-Oct-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Moved a couple of useful functions into CooperSyntax (in fact, I think they are both useful enough to possibly make it into bool/; the functions are UNBETA_CONV and find_free_terms), and implemented handling of natural number DIV and MOD (along with test case demonstrating this).
|
#
a69b99a9 |
|
03-Oct-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Cooper's algorithm now updated to handle mod and div by constants (but only over the integers for the moment).
|
#
2d8edb6e |
|
01-Oct-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More tweaks and fiddles. The Pugh example now goes through in a reasonable length of time (same as SUNRISE problem, perhaps a 20-fold speed-up). Also added a couple of new theorems to integerTheory which will be the basis for extending COOPER_CONV to cope with division and modulus (as long as the divisor is a constant).
|
#
411a71d4 |
|
18-Sep-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Added a new problem to test suite (from paper by William Pugh about his Omega d.p.), but have left it commented out because it's a nasty pathological case, possibly indicating a bug, or perhaps just pointing to a really nasty case that Cooper's is doomed to perform badly on.
|
#
4ae3e9df |
|
14-Sep-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More reorganisation, mainly to remove listTheory as an ancestory wherever possible (it still persists as a necessary ancestor of CooperCore, but isn't used un-necessarily elsewhere). Also sped up phase5 of CooperCore some more.
|
#
99abe76d |
|
13-Sep-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Total reorganisation of Cooper code. Two ..Core modules can be swapped in and out of CooperShell to provide "shadow syntax" or my original implementation of the core phases of the algorithm. Code currently littered with profiler guff.
|
#
2f90b724 |
|
04-Sep-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
A new program to generate integer problems to be fed to Cooper's algorithm with larger coefficients than the problems generated by the existing genproblem program.
|
#
06c7e9ce |
|
24-Aug-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Added another problem to the standard regression test suite. It seems to take unacceptably long.
|
#
e1628e10 |
|
24-Aug-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
A slew of infrastructure for testing Cooper's algorithm. Useful for regression testing and efficiency experiments.
|