#
4888f523 |
|
15-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove eqtype declaration for term type
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files. This affects over 900 files and was done using emacs's delete-trailing-whitespace function in batch mode. Building the system with Poly/ML and Moscow ML seems to work, so I'm hoping these changes don't break anything. Please complain if they do!
|
#
f426d72b |
|
17-Apr-2008 |
Scott Owens <Scott.Owens@cl.cam.ac.uk> |
Removed Polyhash
|
#
e234dcdc |
|
23-Mar-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Got rid of QConv, and made all conversions do the "raise exception to indicate reflexivity" thing. (Also fixed bug in new implementation of ABS_CONV that attempted renaming on failure of conv, and not just failure of ABS.) Next step will be to rework the simplifier's implementation so that it also uses Conv.UNCHANGED, rather than in its own internal version of the same. This will let the simplifier play efficiently with others. May also assess making ABS_CONV not do renaming, and give the rewriter its own special traverser. This might make some things more efficient.
|
#
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.
|
#
a20eeb9e |
|
14-Mar-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Gave OmegaSymbolic a signature file to make it clearer what this module of the decision procedure does.
|
#
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.
|
#
f32f2816 |
|
04-Mar-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Omega now works on all of the test case, bar KXSDIV1, on which it blows up. Some investigation suggests that this is "just" an efficiency issue and not one of code correctness. With luck, I'll check in some efficiency changes tomorrow, and then I'll be done.
|
#
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.
|
#
8ebf18ee |
|
28-Feb-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Very close to a complete symbolic method.
|
#
091d31cc |
|
27-Feb-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Moved some theorems about; basic machinery is now in place to decide all problems with only one sort of quantifier (occasionally the out-of-the-logic approach breaks, and the symbolic approach is needed, even for all-one- quantifier problems).
|
#
dadcb8f7 |
|
26-Feb-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More fiddling (gradual progress) with symbolic implementation of Omega.
|
#
cec7c874 |
|
22-Feb-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More work on symbolic quantifier elimination.
|
#
2e985d5f |
|
21-Feb-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Moved some theorems into the theory file.
|
#
636b04b3 |
|
20-Feb-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Progress with symbolic form of Omega Test.
|
#
941ea164 |
|
15-Feb-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Initial thoughts on doing Omega the hard way, symbolically.
|