#
91cc4cfb |
|
16-Jul-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix bug in integer d.p.s' handling of ODD/EVEN. Include test-case. Rewriting of ODD now uses |- ODD n <=> ?m. n = 2 * m + 1 rather than |- ODD n <=> ~(2 int_divides n) because in the latter, the elimination of natural number subtraction can't get to grips with the "isolated" argument n. Closes #437
|
#
3dcefcac |
|
12-Jan-2015 |
Michael Norrish <michael.norrish@nicta.com.au> |
Make the integer decision procedures handle maximum and minimum. This works for :num and :int. In both cases, the treatment is to expand with the definition of the relevant constant.
|
#
d1fe9497 |
|
12-Oct-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Bug-fix in integer self-tests. Bug was caused by change to Timer structure.
|
#
8f5e19cf |
|
11-Sep-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add a couple of test-cases. Mike2 used to cause the bug that I just fixed in Cooper's algorithm.
|
#
aa7a0a18 |
|
21-Jul-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Bug-fixes and test-cases from problems in src/rational.
|
#
2b2cd95c |
|
20-Jul-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add some pre-processing code so that the decision procedures can handle the Num constant, which coerces from integers to natural numbers. Changes to intSyntax include adding {mk,dest,is}_Num and also dest_absval.
|
#
42df0344 |
|
09-Jul-2007 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
I think this is a bug-fix. Now the SEND MORE MONEY test case takes four hours to raise an exception instead of just a minute. I've taken it out of the test cases list. I can't easily come up with a test case that proves this is a bug, but it seems plausible that it is. (Now I'm going to have to implement that "combine with DPLL d.p.")
|
#
e3ed4bac |
|
06-Jul-2007 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Send more money problem should require leading digits not to be zero. (Still breaks Cooper's.)
|
#
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.)
|
#
8264baed |
|
21-Feb-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement improved handling of integer div and mod, along lines already done for natural number operations. This allows Omega to prove John Matthew's example, recently posted to the Isabelle mailing list, in half a second. (Cooper seems to fail miserably.) Added this example (in four variants) to the test case suite.
|
#
59904d44 |
|
15-Nov-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Ahem, shouldn't try to write these things out from memory.
|
#
2e622ae0 |
|
15-Nov-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Another test case for Omega's new handling of MOD and DIV. From my work on netsem, a fact to do with sign-bits being zero (imagine 100000 being 2^31).
|
#
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.
|
#
00261c01 |
|
30-Oct-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Multiplication normalisation bug fixes, along with a couple of extra bugs picked up along the way recorded in the test cases.
|
#
118c2f99 |
|
30-Oct-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Introduce Alexey Gottsman's test case to the integer and natural number arithmetic decision procedures regression test suites. Now, selftests fail. Fixes forthcoming.
|
#
6914cde1 |
|
17-Aug-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
A fix for my "natural number goal" bug. (And a new test case for no particularly good reason.)
|
#
0e588bd5 |
|
16-Aug-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
The integer decision procedures don't handle natural number assumptions properly: the new goal added to the list here raises an exception.
|
#
d5033c3f |
|
23-Jun-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix for bug 964085 (to do with DIV/MOD expressions nested inside themselves). Also made the procedure cope with the presence of ?! quantifiers with scope over DIV/MOD expressions. Added test cases to demonstrate. Unfortunately, the example I chose in the bug report above produces a goal that takes too long to solve (the bug was in the production of the goal), so my exemplar of the bug in the regression test suite is instead (x MOD 2) MOD 2 = x MOD 2 which is rather less interesting.
|
#
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.
|
#
da4a7af8 |
|
07-May-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Added some test cases due originally to JRH (via Konrad) and discovered a bug in Cooper's handling of conditional expressions. Fixed the problem by making some code from IntDP_Munge visible.
|
#
588ec7a6 |
|
02-May-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixed a bug found by Mike. Problem stemmed from the routine that normalised multiplicative terms, which was supposed to do things like p * k * 2 --> 2 * (k * p). The code did this fine on natural number formulas, but was doing the wrong thing on integer formulas because a DEPTH_CONV of it would wrap non-multiplications in a multiplication by one. This multiplication by one was relied on elsewhere though, so the sum-normalisation routine needed tweaking as a result. In testing/ there are two new test cases, the natural number version worked before, but the integer one did not.
|
#
7a257bd3 |
|
07-Apr-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixed a bug in the normalisation routine; it wasn't handling the possibility that it might return ?x. F. New addition to test_cases is the example that tweaked this bug; thanks to Joe and Konrad for coming up with it.
|
#
5b7b7cf1 |
|
06-Mar-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Omega now passes all of its tests, and I claim it's probably now a reasonable approximation of a complete procedure for doing Preburger arithmetic. Aggressive preprocessing attempts to minimise DNF blowup, but the fact that EXISTS_OR_CONV can still consume over 10% of the procedure's running time basically sucks.
|
#
00262dd0 |
|
01-Mar-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
OMEGA_CONV is now "almost complete". There are just bugs to be ironed out. Changes are too many to document extensively. Some though: * OmegaMath has got a lot bigger, with OmegaEq being merged into it and also gaining some divisibility normalisation code. * couple of new test cases * decided against prenexing mixed quantifier problems.
|
#
88f99907 |
|
20-Feb-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Konrad found a bug: elimination of subtraction has to happen after DIV and MOD are eliminated so that terms of the form (x - y) DIV c are handled properly. Added a couple of test cases to demonstrate the bug in the old version.
|
#
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.
|