-
Notifications
You must be signed in to change notification settings - Fork 10
/
NEWS
executable file
·1289 lines (1149 loc) · 51.6 KB
/
NEWS
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
Overview of Changes in Maude 3.5 beta (alpha163) (2023-06-07)
=============================================================
* rat() conversion operator is more tolerant of leading zeros
Overview of Changes in alpha162 (2023-05-30)
============================================
* fixed typo where sets of states were show as conjunctons rather
than disjunctions
* vfold option for vu-narrow
Overview of Changes in alpha161 (2023-05-17)
============================================
* reading from the stdin steam now supports continuation lines
* path option for vu-narrow
* show most general states .
* show frontier states .
* a state may now subsume its ancestors in vu-narrow
Overview of Changes in alpha160 (2023-05-02)
============================================
* initial equality operator handles more cases
* fixed bug in rat() string to rational conversion operator
* extra built-in operators on characters and strings
* fixed build issue on 32-bit platforms
* fixed potential memory corruption in vu-narrow
* check for unsafe variable names in vu-narrow
* allow term disjunctions in vu-narrow at the object level
Overview of Changes in Maude 3.4 (alpha159) (2023-03-19)
========================================================
* set print latex on/off command
* fixed loop mode LaTeX bug
Overview of Changes in Maude 3.4 beta (alpha158) (2023-03-12)
=============================================================
* fixed bug where LaTeX for op names in declarations, renamings
and views sometimes used the wrong font
* comments in LaTeX no longer use the comment environment
* fixed bug where the strategy part of an srewrite command was
omitted in the LaTeX comment
* fixed bug where show desugared omitted local op declarations
that overloaded imported operators
* changed the LaTeX vertical spacing
* fixed bug where color generated by a format attribute could
run in the following text in LaTeX output
* fixed bug where a newline generated by a format attribute
reset the color to black in LaTeX output
Overview of Changes in alpha157 (2024-02-27)
============================================
* fixed bug where debugging information was being printed to
stderr when generating the LaTeX for a structured constant; this
also caused a crash on Macs
* mismatched parentheses in operators now generates a warning
* fixed crash in LaTeX generating code for strange constant names
* bound on exponents and left shifts increased to ULONG_MAX
* many changes to the way operator names are printed to fix
various pathological cases and make the output look prettier
* various LaTeX tweaks
Overview of Changes in alpha156 (2024-01-29)
============================================
* LaTeX support for more commands and features
* big numbers, strings, qids and unparsed tokens are now broken
across multiple lines in LaTeX to avoid an "Overfull \hbox"
* fixed bug where bad LaTeX was generated by show mod for
certain characters in metadata
* added =># search type
* fixed bug where srewrite could miss a rewrite due to a side-effect
from a condition
* equations with both variant and nonexec attributes produce
an advisory and are no longer used for variant narrowing
* in/load/sload no longer attempt to read non-regular files
* increased line length and history size with Tecla
* the narrow command now respects frozen positions
Overview of Changes in alpha155 (2023-12-12)
============================================
* fixed bug in LaTeX output for format attribute
* fixed missing space in LaTeX output between format and
metadata attributes
* fixed bad LaTeX for dags with print color on
* latex attribute supported
* fixed bug where LaTeX for structured constants didn't
support the format attribute
* fixed bug where format s and i commands didn't work at the
start of a LaTeX line
* fixed CVC4 bindings for latest version
Overview of Changes in alpha154 (2023-11-30)
============================================
* conventions for printing spaces around unparsed tokens made
uniform
* fixed bug where set print const with sorts on . did not work
for built-in constants in terms
* new with-sorts PrintOption constant
* added metaPrintToString() descent function
* added printToString() message
* metaPrettyPrint() descent function supports concealed
argument lists via an extra argument
* printTerm() message supports concealed argument lists via an
extra argument
* concealed argument lists support for printing terms in modules
* fixed bug where color for terms in modules produced bad LaTeX
* fixed bug in LaTeX for disambiguation of iter operators
Overview of Changes in alpha153 (2023-11-07)
============================================
* smarter sort disambiguation for printing statements and
operator identities
* set print label attribute on/off .
* refinements to show module output
* ASCII option for maude.sty LaTeX package
* fixed various bugs in LaTeX output
* LaTeX support for more commands
* set clear module caches on/off .
* set print hooks on/off .
* space printed after comma by default in mixfix syntax
* portal attribute and enforcement of portal requirement
* uniform order for operator attributes
* _|=_ in model checker is now partial
* set print combine vars on/off .
* new line breaking rules for LaTeX output
* backquotes removed in LaTeX output for op-hooks
Overview of Changes in alpha152 (2023-10-02)
============================================
* more LaTeX support
* fixed bug in the LaTeX printing of view instantiations
* fixed bug in LaTeX printing of one strategy
* fixed bug in LaTeX printing of srew/dsrew commands
* fixed a termination bug in filtered variant unify
* optimizations to semi-compilation of free theory equations
* fixed compile time error for 32-bits targets
* updated config.guess
Overview of Changes in alpha151 (2023-08-11)
============================================
* fmod INITIAL-EQUALITY-PREDICATE added to prelude
* more LaTeX support
* fixed bug where debug modifier wasn't being printed
* fixed break deselect, trace deselect, trace include, print reveal bugs
* fixed LaTeX timing bugs
Overview of Changes in alpha150 (2023-07-21)
============================================
* added set show resources command
* intial support for LaTeX
* fixed bug in free theory discrimination nets for huge
number of patterns
* fixed bug in free theory discrimination nets for large
patterns
Overview of Changes in alpha149 (2023-05-12)
============================================
* added pseudo-random number generator objects
Overview of Changes in alpha148 (2023-05-05)
============================================
* fixed a bug in compilation of ACU patterns introduced by the
last alpha that caused matches to be missed
* fixed a bug in thew functional meta-level where rewrite count
from metaSrewrite() was lost
* more optimizations for ACU red-black matching
* smarter scheme for deciding how many dag nodes the memory manager
should allocate
* fixed a bug in the rewrite count values returned by the
meta-interpeter in response to the srewriteTerm() message
* more information shown in garbage collection reporting
* -early-quit=N flag for developer use
Overview of Changes in alpha147 (2023-04-28)
============================================
* fixed bug in new ACU matching code where stripper variable
was not required to have multiplicity 1
* fixed bug in new ACU matching code where it didn't handle
0 or 1 subject arguments left
* fixed bug in new ACU matching code where it could be used
even if a non-ground alien was present
* optimizations for ACU red-black matching
Overview of Changes in alpha146 (2023-04-26)
============================================
* overparsing for commands that end in on/off
* optimizations for AC/ACU matching
* optimizations for token handling
Overview of Changes in Maude 3.3.1 (alpha145) (2023-04-13)
==========================================================
* fixed a bug where internal error and stack overflow messages
didn't appear on Macs by not stripping Mac binary
* overparsing for attributes with missing information in operator
declarations and mappings
Overview of Changes in alpha144 (2023-04-10)
============================================
* fixed a bug where special symbols other than strings that
started with " were not recognized.
* fixed a bug where renamings that mapped parameterized constants
were not being correctly instantiated
* fixed a bug where operators with the same name but different
arities could confuse renamings generated to instantiate modules
* fixed a bug where a change of parameter was not supported for
parameterized polymorphic constants
* fixed a large family of bugs where identifiers that looked
like parameters but which were not ("pseudo parameters") could
clash with actual parameters by enforcing new constraints
* fixed a bug where a constant from a parameter theory that
looked like a parameterized constant was being treated as such
for various operations
* different message for self-check failure
Overview of Changes in Maude 3.3 (alpha143) (2023-03-22)
========================================================
* overparsing for omitting -> in constant mapping removed due
to ambiguity
* various gcc/clang warnings fixed
* show path states command now shows rule labels
* fixed a subtle bug with narrowing with variant unification in
the presence of irreducibility constraints
* fixed a bug where certain debugging information was printing
in the debug build even without the -debug flag
* added set generate-by command
* optimization for free theory dag nodes
Overview of Changes in Maude 3.3 beta (alpha142) (2023-03-03)
=============================================================
* show path states command
* fixed bug where generated-by was not recognized as the and of the
previous mixfix statement
* fixed bug where orphaned view instantiations were not being purged
* fixed bug where replacing a view did not immediately purged an
modules that became orphaned as a result
* heurstics for giving detailed explanations of runaway statements
* fixed bug where parameterized constants were printed without
parentheses in an ops declaration
* more overparsing
Overview of Changes in alpha141 (2023-02-24)
============================================
* fixed bug in parsing of oths
* fixed statement transformation depending on memory allocator issue
* -debug flag for debug build
* fixed bad printing of renamings in module names
* fixed op to term mapping in theory-view crash
* support pconst in op to term mappings
* sanity checks for class attributes
* fixed bug where auto OO includes were ignored by upModule()
* modules/views/commands cannot span files
Overview of Changes in alpha140 (2023-02-14)
============================================
* fixed bug where no warning was given for duplicate iter attribute
* pconst attribute for constants
* parameterized constants
* generated-by importation mode
* show processed view command
* classes can be parameterized
* object-oriented theories
* object-oriented mappings in views
* fixed bug where []s around bound parameter were shown in imported
module name with show desugared
Overview of Changes in alpha139 (2023-02-02)
============================================
* syntactic sugar for empty attribute set in object constructor
* changed reporting of syntax errors in sort and subset declarations
* fixed bug where automatic imports were included in meta-theories
* getClass() added to CONFIGURATION
* allow "from" as a sort name
* fixed spurious advisory where a specific renaming did not capture
an operator from a parameter
* identity sort/op mappings quietly dropped during renaming
canonicalization
* advisory if all the variables in the pattern of a := condition
fragment are bound before matching
* fixed bug where advisory about a specific strat renaming affecting
a theory parameter printed 0 rather than the strat name
* prettier printing of _,_ for attribute sets
* first attempt at supporting omods and OO mappings in renamings
* fixed bug where a view from T importing M to M was not allowed
* fixed a related bug where a misleading warning was given for
theory-views that implicitly mapped a sort from module to the
target theory
Overview of Changes in 3.2.2 (alpha138) (2022-12-22)
====================================================
* fixed bug where multiple instantiations (say via a theory-view)
was generating bad internal names for sorts
* fixed bug where the first sort in a kind printed by show mod
was including backquotes
* show desugared is now a documented feature
* desugar omod to mod, oth to th
* fixed bug where filtered variant unify crashed in the degenerate
case where there were no variables
* fixed issue where SIGSTKSZ is no longer guaranteed to be a
compile-time constant in glibc
* fixed issue with fileTest failing in environments when first
user file handle is something other than 3
Overview of Changes in Maude 3.2.1 (alpha137b) (2022-02-21)
===========================================================
* use filtered variant unification for unifying with goal when filter
flag is passed to vu-narrow
Overview of Changes in Maude 3.2 (alpha137a) (2022-02-07)
=========================================================
* updated comments to 3.2
Overview of Changes in Maude 3.2 beta (alpha137) (2022-01-28)
=============================================================
* fixed bug in the Yices bindings where constraints were being
asserted twice
* fixed bug in the prelude where projection functions didn't work for
parameterized meta-modules
* fixed bug in the handling of extension information for iter symbols
* fixed bug in loop mode where it would try to continue using state left
over from some incompatible command
Overview of Changes in alpha136 (2021-06-08)
============================================
* file API supports makeLink() message
* experimental directory API
* -assoc-unif-depth= to control A/AU unification search
Overview of Changes in alpha135 (2021-04-09)
============================================
* second control-C within a second now returns to command line
* fixed bug in deleteTimer() which would cause a later crash
* empty line is treated as implicit step command in debugger
* getLine() is now nonblocking
* changed semantics of stopTimer()
* standard streams now accept bad messages and return streamError()
Overview of Changes in alpha134 (2021-03-08)
============================================
* experimental time API
Overview of Changes in alpha133 (2021-02-25)
============================================
* fixed bugs in the processing of strategies in parameterized views
* fixed bug where irredundant prefix was echoed
* fixed bug where waiting on multiple file descriptors could ignore
some of them on platforms using pselect() such as Mac
* constraint propagation gets more A/AU unification cases
* two optimizations to reduce the number of redundant AU-unifiers
* meta-interpreters running in the orginal process now have the
same error semantics as meta-interpreters running in new processes
* file API has new error semantics
* missing start op-hook added to file.maude
* removeFile() message added to file.maude
* fixed a bug where irredundant unification was ignoring the
last variable in each subsumption check
* removed destructive generation of order-sorted unifiers because
it breaks irredundant unification (which assume unifiers can
be retained) and generates denormalized unifiers anyway
Overview of Changes in alpha132-32 (2020-12-14)
===============================================
* fixed GMP/long long int issue on 32-bit machines
Overview of Changes in alpha132 (2020-12-11)
============================================
* fixed bugs where non-unary iter symbols caused breakage
in regular and polymorphic cases
* fixed bugs where bad sorts for iter symbols caused breakage
in regular and polymorphics cases
* fixed bug where comm, idem and id: attributes were ignored
if iter attribute seen
* fixed bug where flattened prefix syntax wasn't accepted
for polymorphic associative operators
* fixed bug where f^n(...) syntax wasn't accepted for
polymorphic iter operators
* fixed bug for ! strategy
* support meta-interpreters in separate processes
* new options for vu-narrow
Overview of Changes in Maude 3.1 (alpha131a) (2020-10-12)
=========================================================
* changed messages for ^C seen during suspension
* some clang warnings fixed
Overview of Changes in Maude 3.1 beta (alpha131) (2020-10-05)
=============================================================
* fixed occurs-check bug in unification modulo U and CU
* optimizations for unification modulo U and CU
* fixed memory leak when trying to use file handle while
file handling is disabled
* optimization for merging variables during unification which
merges towards the smaller sort
* two control-C events without intervening rewrites to abort
while suspended on external event
* variant narrowing based commands no longer report number of
rewrites and no unifiers/variants/matchers if there is a problem
Overview of Changes in alpha130 (2020-09-22)
============================================
* fixed memory leak in filtered variant unify
* fixed variable check bug in filtered variant unify
* fixed bug in the meta-printing of strategies
* support VariantOptionsSet for descent functions and
meta-interpreter messages that use variant unification
* fixed a bug in unification modulo identity where the theory
purification code assumed the operator was also commutative
Overview of Changes in alpha129 (2020-09-09)
============================================
* verbose mode now flags sort decreasing axioms
* command line options for enabling dangerous feautures
* added irredundant unification
* receiving on a socket which closed for writing at the other
end returns the empty string the first time rather than closing
the socket
* irred is an abreviation for irredundant on the command line
* fixed stray space when echoing variant unify command
* fixed memory leak affecting erroneous case of unification
descent functions
* added filtered variant unification
* added variant matching
Overview of Changes in alpha128a (2020-07-06)
=============================================
* strategy definitions now support nonexec attribute
* fixed bug in metaParseStrategy() and all operator declaration
* fixed bug where simple and complex parsers could get
out of sync with the auxiliary information leading to crashes
* experimental support for processes as external objects
* fixed bug where signals such as ^C could be ignored when sockets
were used due to a race condition
* fixed bug where sockets only supported half duplex operation
* fixed bug where Maude could be terminated by SIGPIPE
* -no-execute command line option
* write half of a socket can now be shutdown
* fixed error in -help message
* fixed bug in C/U/Ul/Ur unification code that overwrote
previous variable -> variable binds and produced non-unifiers
* fixed bug where a collapse-up situation was not being
warned about because the declaration used a kind
* fixed bug in the sort analysis phase which could cause lost
ACU unifiers
* fixed bug in unifier subsumption check that causes silent
memory corruption
* fixed symmetric bug in variant subsumption check
* handling of order-sorting in elementary A unification now
takes systems of equations into account
* experimental support for associative-identity unification
Overview of Changes in alpha128 (2020-03-09)
============================================
* fixed bug where ascent functions were allowed to proceed
on bad modules, resulting in an internal error
* fixed bug where illegal use of built-in variable names
in variant equations and narrowing rules wasn't being
detecting in the functional metalevel
* more sophisticated handling of order-sorting in
elementary A unification
* cleaner handling of ^C in unify and match commands
* do clear memo command now takes an optional module
* extra functions defined in META-LEVEL
* fixed socket close bug
Overview of Changes in Maude 3.0 (alpha127a)
============================================
* commented out unused code/data structures
* increase default number of BDD variables to 100
* updated comments
Overview of Changes in Maude 3.0 beta 1 (alpha127)
==================================================
* fixed memory leak in file writing code
* support ll as alias for ls -l
* many compiler warnings fixed
Overview of Changes in alpha126
===============================
* fixed memory leak in failed view instantiation
* fixed bug in profiling of condition fragments
* fixed bug when comment ended by EOF
* Rubén Rafael Rubio Cuéllar's extensions to the strategy
language and fuctional reflection of the strategy language
integrated
* Strategy language supported by meta-interpreter
* -erewrite-loop-mode command line option
* set print constants with sorts option
* bubbles only disallow excluded tokens outside of parens
* new variable family based descent functions
* metaParse()/metaPretty() support variable aliases
* symmetric change in meta-interpreter
Overview of Changes in alpha123
===============================
* fixed a bug in module instantiation introduced by the
redesigned module system
* kludged around a bug in BuDDy
Overview of Changes in alpha121
===============================
* fixed a bug where module sums were commuted
* fixed a memory leak with module expression syntax errors
* fixed a bug where number of sorts from a parameter theory
was incorrectly recorded if the module had no regular imports
* fixed symmetric bug with operators from a parameter theory
* fixed symmetric bug with polymorphic operators from a parameter theory
* fixed bug where user declared sort with parameter sort name
could confuse module system
* summing modules with bound parameters is now supported
* parameterization of views is now supported
* weird situation with overloaded polymorphic operators that
could cause crash now disallowed
* fixed recursive view bug
Overview of Changes in alpha120
===============================
* fixed memory leak in normalizeTerm() message
* fixed double counting of initial eq rewrites and mb
application in metaApply()/metaXapply()
* added rule application to the meta-interpreter
* added single step narrowing with variant unification
to the meta-interpreter
* added narrowing search with variant unification, with
and without path, to the meta-interpreter
* Overview of Changes in alpha119
================================
* smart load "sload" directive
* more sort computation messages added to the meta-interpreter
* unification and disjoint unification added to the meta-interpreter
* fixed fake rewrites from object-message rewriting that
were visible in trace/break/profile
* variant generation added to the meta-interpreter
* fixed mb/eq double counting bugs in metaMatch()/metaXmatch()
and getMatch()/getXmatch()
* variant unifier generation added to the meta-interpreter
* fixed memory leak in metaGetVariant()
* pretty printing added to the meta-interpreter
* parsing added to the meta-interpreter
* fixed physical vs nominal argument index stacking bugs
Overview of Changes in alpha118
===============================
* getSearchResult()/getSearchResultAndPath() messages added to
meta-interpreter
* -show-pid command line option
* SIGINFO (SIGUSR1 on Linux) now works immediately when blocked
on sockets rather then waiting for next rewrite
* fixed memory leaks in metaXmatch()
* getMatch()/getXmatch() messages added to meta-interpreter
* upperCase()/lowerCase() functions added to fmod STRING
* sort computation messages added to the meta-interpreter
Overview of Changes in alpha117
===============================
* fixed syntax error location bug in new parser
* fixed show view bug
* fixed symmetric upView() bug
* fixed showModule bug in the meta-interpreter where imports
and parameters were omitted
* fixed hang when doing an abort from erewrite
* fixed crash caused by object-message rewriting with the
set clear rules off command
* fixed bug where rewriteTerm()/frewriteTerm() in the
meta-interpreter did not reset next rule pointers
* fixed a bug where modules cached by the metalevel functional
metalevel would be incorrectly used by by the meta-interpreter
* fixed bug where using the functional metalevel from within
the meta-interpreter would pull imports from object level
interpreter
* fixed bug where using the ascent functions from within
the meta-interpreter would pull modules from object level
interpreter
* added insertView and showView messages to meta-interpreter
* meta-interpreter now supports erewriteTerm message
* erewrite will check for external events even when internal
rewrites are possible
* fixed memory leak triggered by bad unify command
* loop-mode/pipe edge case reverted to old behavior for IOP
* status report in response to SIGINFO (SIGUSR1 on Linux)
Overview of Changes in alpha116
===============================
* fixed bug in ctor calculations for associative operators;
enforce new ctor consistancy for such operators
* fixed related bugs in unifier filtering, variant folding
and narrowing folding wrt the handing of abstraction
variables
* new mixfix parser based on Leo's algorithm fixes many
bubble related bugs
Overview of Changes in alpha115
===============================
* fixed bug where show mod command output empty parentheses
* fixed bug where maude wouldn't compile without SMT support
* support for file i/o
* support for standard streams
* support for lexical level QidList <-> String conversion
* no prompting when stdin redirect to read from file
* sort Bound and op unbounded have their own fmod
Overview of Changes in alpha114
===============================
* more sanity checks at object level and meta level
* pretty printer smarter about iterated operator disambiguation
* fixed bug where narrowing attribute was not being printed
if it was a rule's only attribute
* support for Yices2 as the SMT solver backend
* fixed bug in CVC4 bindings where passing something other than
a positive integer constant for the second argument to divisible
produced a crash
* asserting nonlinear stuff in CVC4 now produces unknown rather
that a crash
Overview of Changes in alpha113
===============================
* redesigned/extended vu narrowing functionality
Overview of Changes in alpha112b
================================
* fixed bug in AU instantiation code introduced by
optimizations in alpha111b
* fixed memory corruption bug in class VariantUnificationProblem
where the garbage collector runs before object fully initialized
Overview of Changes in alpha112a
================================
* support for debug, cont, debug cont in vu-narrow
* support for debug, cont, debug cont, incompleteness and
printing state and timing information in narrow
* support for cont/debug cont in variant unify
* support for cont/debug cont in get variants
* support for debug and debug cont in srewite
* support for debug, cont, debug cont and printing
printing state and timing information in smt-search
* support for debug and debug cont in search
* fixed longstanding family of related performance bugs
in the ACU matchers
* added bound element variable ACU stripper-collector automaton
* added early failure optimization for ACU_LazySubproblem
Overview of Changes in alpha112
===============================
* fixed a longstanding bug in the comparison of NatSets that
amongst other things broke the LTL -> VWAA conversion in the
model checker
Overview of Changes in alpha111b
================================
* optimized handling of stacks of states in conditions
* optimized construction of free right hand sides
* fixed bug where 0 step rewrites module SMT could return
unsatisfiable constraints
* fixed bug where bindings were being shared between eager and
lazy places in both regular narrowing and variant narrowing
* fixed bug where narrowing steps and equational rewrites
weren't being counted in metaNarrow()
* vu-narrow command added
* metaNarrowingSearch() descent function added
* fixed bug where illegally parameterizing a module by a
parameterized module caused a crash
Overview of Changes in alpha111a
================================
* fixed bug where variables occuring only in a irreducibility
constraint could cause a crash
* fixed bug where irreducibility constraint could be ignored
* better handled of contexts for metaNarrowingApply()
* require that variables that only occur in irreducibility
constraint meet safety criteria
Overview of Changes in alpha111
===============================
* fixed bug where an ambiguity in a term-hook caused crash in
sort computation because module isn't semi-compiled at this point
* new narrowing descent function
* one of the old narrowing descent functions now supports
incompleteness
Overview of Changes in Maude 2.7.1 (alpha110b)
==============================================
* fixed typos and copyright date
* minor configuation fixes
Overview of Changes in alpha110a
================================
* fixed bug in ACU unification that was introduced in alpha108
Overview of Changes in alpha110
===============================
* reorganization of unification sort computations
* added -print-to-stderr flag
* added cycle detection and depth bounds to PIG-PUG
* fixed some uninitialized memory reads in SMT code
Overview of Changes in alpha109
===============================
* new metalevel interface for variant narrowing
* large number of finite variant examples from Jose Meseuger added
to the test suite
Overview of Changes in alpha108a
================================
* fixed bug in variant narrowing where ground terms caused substitution size
mismatch and memory corruption during subsumption check
* replacement rope library avoids build problems on Mac
Overview of Changes in alpha108
===============================
* new associative unification algorithm based on PIG-PUG
* unification infrastructure support for incomplete algorithms
* fixed bug in metaGetIrredundantVariant()
* fixed bug in variant narrowing where collapse terms were being narrowed
with variant equations from the wrong kind
Overview of Changes in alpha107
===============================
* fixed bug where asking for the same variant or variant unify twice in
succession from the metalevel resulted in memory corruption
Overview of Changes in alpha106
===============================
* improvements to linear associative unification integration
* fixed bug in SequenceAssignment code (low level associative unification code)
Overview of Changes in alpha105
===============================
* experimental support for multi-step search modulo SMT
Overview of Changes in alpha104
===============================
* fixed duplicate advisories about missing sorts
* fixed missing echoing bug for commands with 2 optional arguments
* fixed caching bug for descent functions
* experimental support for 1-step rewriting modulo SMT
Overview of Changes in alpha103
===============================
* 0/1 is now a valid Rat constant
* advisory printed when downTerm() fails because of kind clash
* experimental support for calling CVC4
* fixed bug where metaPrettyPrint() was failing to generate needed
disambiguation for built-in data types
Overview of Changes in alpha102
===============================
* experimental support for linear associative unification
Overview of Changes in Maude 2.7 (alpha101)
===========================================
* fixed bug with debug text being output during rewriting
* MVM now supports _==_ and _=/=_
* incementalized (up to layer level) variant narrowing and unification
* --always-advise flag
Overview of Changes in alpha100a
================================
* dlmalloc removed (already disabled on most platforms)
* MVM now supports non-linear variables
* fixed bug with debug text being output during variant narrowing
* (binary) Mac version now compiled with Mac Ports toolchain which
resolves several issues caused by Apple gcc and flex bugs, including
hanging on an end-of-file inside a comment
* code cleaning to remove unused code and avoid many compiler warnings
Overview of Changes in Maude alpha100 (source trees 97, 98, 99 abandoned)
=========================================================================
* added crude Maude VM based interpreter (sreduce)
Overview of Changes in Maude alpha96c
=====================================
* added unification support for CU, U, Ul and Ur theories
* fixed two related bugs where unifying a variable against a variable
generating an implicit renaming caused an in-theory occurs check issue
leading to non-termination
* fixed a bug in the AC/ACU unification code where binding a variable to an alien
subterm caused a variety effects including missing unifiers and nontermination
* performance fixes for AC/ACU unification where subterms cancel
* fixed a GC bug in AC/ACU unification
* fixed a bug where printing the empty QID in loop mode caused an out-of-bounds
memory read
* fixed a bug in the free theory semi-compilation of variant equation left hand sides
Overview of Changes in Maude alpha96b
=====================================
* fixed bug in variant narrowing of ground terms
* fixed memory corruption bug in sockets
* the print attribute now flushes its output
* fixed a long standing bug where sockets could appear to be dropped on Mac
Overview of Changes in Maude alpha96a
=====================================
* hack to allow building 64-bit binaries under Darwin
* fixed bug in metaGenerateVariant() with singleton substitutions
* fixed variable name clash bug in narrowing
* support for irreducibility constraints in variant narrowing
* support for variant unification
Overview of Changes in Maude alpha96
====================================
* fixed bug in narrowing where unifiers were being eagerly rewritten in place
* fixed bug in narrowing caused by abstraction variables
* fixed bug in pretty printing of equation attributes
* fixed fresh variable clash bug in narrowing
* first attempt at supporting variant narrowing
Overview of Changes in Maude alpha95c
=====================================
* fixed a bug where stale information about fresh variables was not
being cleaned up when backing out of a unification branch that
generated those variables
* a bug where the socket write code was using memory might have been
deallocated
* patched around apparent weirdness in rope::c_str()
Overview of Changes in Maude 2.6 (alpha95b)
===========================================
* fixed a bug in the profiler provoked by condition fragments in a
command or descent function invocation
* more overparsing
* avoid unnecessary right id sort checking for commutative symbols
Overview of Changes in Maude alpha95a
=====================================
* fixed sort bug with new memo mechanism
* added MAUDE_META_MODULE_CACHE_SIZE environment variable
Overview of Changes in Maude alpha95
====================================
* fixed bug where tokens starting in . that followed a . that might
have, but didn't terminate a statement or command were having their
initial . split off
* handle collapse down cases in order sorted unification
* hash consing used for srewrite
* fixed a bug in the ACU matcher where bad solutions could be
generated by the lazy red-black algorithm for certain nonlinear
patterns
* fixed a bug in the module system where errors in modules constructed
for module expressions could cause a crash
* memo attribute reimplemented using hash consing
* a memory corruption bug in the compilation of variant equations whose
left hand side is headed by a free function symbol
Overview of Changes in Maude alpha94a
=====================================
* fixed bug where downTerm() could return terms in the wrong kind
* changed handling of operator names that are a single special
character
* implemented compound cycle breaking for unification
* optimizations for ACU unification
* changed handling of variable bindings for unification
Overview of Changes in Maude alpha94
====================================
* fixed bug where hash consing wasn't being used for model checking
after all.
* fixed bug where empty sort declaration crashed show module command
* fixed bug where op->op mapping in a theory-view could be ignored if
followed by an op->term mapping in another view
* fixed bug in upView() where op->term mappings were not being lifted
to the metalevel correctly.
* fixed potential bug in garbage collection of dags produced by
unification if rewriting takes place between the generation of two
unifiers
* partial implementation of ACU unification.
Overview of Changes in Maude 2.5 (alpha93d2)
============================================
* BOOL-OPS split off BOOL in prelude
Overview of Changes in Maude alpha93d
=====================================
* fixed bug where fail term attachments to polymorphs cause crash
* fixed bug where flattened meta-modules produced by upModule() still
had parameters
Overview of Changes in Maude alpha93c
=====================================
* fixed bug where upView was producing bad metaViews
Overview of Changes in Maude alpha93b
=====================================
* fixed bug in handing of metaRenamings
Overview of Changes in Maude alpha93a
=====================================
* changed AC constraint propagation algorithm to reduce the risk of
exponential blow up at semi-compile time
* changed free theory constraint propagation algorithm to reduce the
risk of exponential blow up at semi-compile time
Overview of Changes in Maude alpha93
====================================
* fixed performance bug with huge AC/ACU right hand sides
* fixed symmetric performace bug in A/AU theory
* fixed a A/AU rewriting with extension bug
* graceful recovery from tabs in string literals
* optimizations for construction of rhs instances
* bug where single token op names containing a string part were
considered to have mixfix syntax
* unification code cleanup and potential bug fixed
Overview of Changes in Maude alpha92c
=====================================
* fixed metaPrettyPrint() bug in assoc, with paren case
* tail recusion elimination for dag node comparison
* various low level optimizations
Overview of Changes in Maude alpha92b
=====================================
* fixed failure to GC in rules only search
* fixed unstackable flag bug in CUI theory
* first attempt at hash consing for search/model checking
* unrewritable/unstackable optimization for search/model checking
Overview of Changes in Maude alpha92a
=====================================
* fixed BDD variable bug introduced by lazy computation of symbol sort
calculation BDDs in alpha92
* fixed bug where free, fresh variables were not constrained to have a
valid sort
* partly fixed a performance bug in constraint propagaion analysis
phase of pattern compilation
* partial support for strat in metalevel builtins
Overview of Changes in Maude alpha92
====================================
* fixed a bug in unification sort calculations on polymorphic symbols
* if_then_else_fi now uses generic sort mechanism and can give
preregularity warnings
* fixed module reparsing bug
* fixed CUI matcher bug
* fixed pending unification stack bug
* added rewrite condition fragments to search command
* fixed instantiation by theory-view bug
* added meta-view syntax and upView() operator
* first attempt at meta-interpreter
Overview of Changes in Maude 2.4 (alpha91d)
===========================================
* fixed AU term normalization bug
Overview of Changes in Maude alpha91c
=====================================
* Special case optimization for AC/ACU matching with extension
Overview of Changes in Maude alpha91b
=====================================
* Removed extranous debugging print statement
Overview of Changes in Maude alpha91a
=====================================
* Now solve diophantine equations over ints rather than mpzs for
unification
* Extended unify command to handle systems
* Added print attribute
* Fixed Diophantine solver bug for results over 2^31 - 1
* Install .maude files in the data directory
* Fixed free theory discrimination net subsumption bug
* Fixed gcc4 incompatibilities
* Outlawed overloading operations from a parameter theory
* Fixed longstanding stdout/stderr synchonization bugs
Overview of Changes in Maude alpha91
====================================
* fixed bug where natSystemSolve() would lose hooks during importation
* fixed bug where unify command was not cleaning up after bad
unification problem
Overview of Changes in Maude alpha90a
=====================================
* added stack overflow handling using libsigsegv
* semi-compilation of right hand sides optimized for huge right hand
sides
* construnction of free theory discrimination nets optimized for large
numbers of equations
Overview of Changes in Maude alpha90
====================================
* new unification combination scheme to avoid AC cycling bug
* C unification is smarter about avoiding redundant unifiers
* reorganized surface syntax parser to allow deeply nested terms
* more overparsing
Overview of Changes in Maude alpha89j (not released)
====================================================
* fixed bug that cause solved form subproblems to be lost in
commutative unification
* added single redex per state narrowing option
Overview of Changes in Maude alpha89i
=====================================
* fixed two bugs which caused narrowing structures not to be deleted
* allow multiple calls to cached desent functions with same arguments
to be efficient in most cases
* added another narrowing descent function
Overview of Changes in Maude alpha89h
=====================================
* crude support for narrowing
* fixed bug with condition fragment collapses during processing
* fixed memory leak in AU term collapses