#
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.
|
#
f37b24c5 |
|
14-Nov-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement some improvements to the pre-processing of natural number goals such that OMEGA can now prove goals of the form (x MOD c + y MOD c) MOD c = (x + y) MOD c in reasonable time. Cooper can't, unfortunately, so the test case for the above (with c = 1001) is added to a new class of examples that are only tried for Omega.
|
#
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.
|
#
9551a737 |
|
22-Jan-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
New test case for Omega, and slight fiddle with Makefile.
|
#
99de871c |
|
21-Jan-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Extended C program for testing decision procedures so that it can be pointed at arbitrary executables; also made it cope with initialisation delays (it would kill programs that hadn't properly loaded if they took longer than the user-mandated delay to do so). Now it won't start interrupting programs until they've started producing some output.
|