alpha147

ChangeLog

@@ -1,3 +1,13 @@
+2023-04-28  Steven Eker  <eker@pup>
+
+	* tests/ResolvedBugs/redBlackNGA_April2023.maude: added
+
+	* tests/ResolvedBugs/redBlackTooFewSubjectsApril2023.maude: added
+
+	* tests/ResolvedBugs/redBlackNonLinearApril2023.maude: added
+
+===================================Maude147===========================================
+
 2023-04-13  Steven Eker  <eker@pup>
 
 	* tests/Corner/attributeOverparsing.maude: added latex examples
@@ -10,7 +20,7 @@
 
 	* tests/Corner/fakeParameterSort.maude: added
 
-===================================Maude144===========================================
+===================================Maude145===========================================
 
 2023-04-10  Steven Eker  <eker@pup>
 

INSTALL

@@ -132,7 +132,7 @@ tar xvf libtecla-1.6.3.tar.gz
 cd libtecla
 
 ./configure \
-CFLAGS="-fno-stack-protector -O3" \
+CFLAGS="-g -fno-stack-protector -O3" \
 --prefix=$OPTLIB
 
 make
@@ -155,7 +155,7 @@ autoconf
 --prefix=$OPTLIB \
 --with-static-gmp=$OPTLIB/lib/libgmp.a \
 --with-static-gmp-include-dir=$OPTLIB/include \
-CFLAGS="-fno-stack-protector -O3" \
+CFLAGS="-g -fno-stack-protector -O3" \
 LDFLAGS="-L$OPTLIB/lib" \
 CPPFLAGS="-I$OPTLIB/include"
 
@@ -183,7 +183,7 @@ cd Opt
 --with-yices2=yes \
 --with-cvc4=no \
 --enable-compiler \
-CXXFLAGS="-Wall -O3 -fno-stack-protector" \
+CXXFLAGS="-g -Wall -O3 -fno-stack-protector" \
 CPPFLAGS="-I$OPTLIB/include" \
 LDFLAGS="-L$OPTLIB/lib" \
 GMP_LIBS="$OPTLIB/lib/libgmpxx.a $OPTLIB/lib/libgmp.a"
@@ -357,7 +357,8 @@ make
 make check
 cd src/Main
 cp maude maude.darwin64
-strip maude.darwin64
+
+Note that stripping the binary on Macs seems to break libsigsegv for some reason.
 
 Check dependencies:
 

NEWS

@@ -1,3 +1,13 @@
+Overview of Changes in alpha147
+============================================
+* 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
+* optimizatons for ACU red-black matching
+
 Overview of Changes in alpha146 (2023-04-26)
 ============================================
 * overparsing for commands that end in on/off

configure

@@ -1,6 +1,6 @@
 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.
-# Generated by GNU Autoconf 2.69 for Maude alpha146.
+# Generated by GNU Autoconf 2.69 for Maude alpha147.
 #
 # Report bugs to <[email protected]>.
 #
@@ -580,8 +580,8 @@ MAKEFLAGS=
 # Identity of this package.
 PACKAGE_NAME='Maude'
 PACKAGE_TARNAME='maude'
-PACKAGE_VERSION='alpha146'
-PACKAGE_STRING='Maude alpha146'
+PACKAGE_VERSION='alpha147'
+PACKAGE_STRING='Maude alpha147'
 PACKAGE_BUGREPORT='[email protected]'
 PACKAGE_URL=''
 
@@ -1312,7 +1312,7 @@ if test "$ac_init_help" = "long"; then
   # Omit some internal or obsolete options to make the list less imposing.
   # This message is too long to be a string in the A/UX 3.1 sh.
   cat <<_ACEOF
-\`configure' configures Maude alpha146 to adapt to many kinds of systems.
+\`configure' configures Maude alpha147 to adapt to many kinds of systems.
 
 Usage: $0 [OPTION]... [VAR=VALUE]...
 
@@ -1383,7 +1383,7 @@ fi
 
 if test -n "$ac_init_help"; then
   case $ac_init_help in
-     short | recursive ) echo "Configuration of Maude alpha146:";;
+     short | recursive ) echo "Configuration of Maude alpha147:";;
    esac
   cat <<\_ACEOF
 
@@ -1490,7 +1490,7 @@ fi
 test -n "$ac_init_help" && exit $ac_status
 if $ac_init_version; then
   cat <<\_ACEOF
-Maude configure alpha146
+Maude configure alpha147
 generated by GNU Autoconf 2.69
 
 Copyright (C) 2012 Free Software Foundation, Inc.
@@ -2013,7 +2013,7 @@ cat >config.log <<_ACEOF
 This file contains any messages produced by compilers while
 running configure, to aid debugging if configure makes a mistake.
 
-It was created by Maude $as_me alpha146, which was
+It was created by Maude $as_me alpha147, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   $ $0 $@
@@ -2962,7 +2962,7 @@ fi
 
 # Define the identity of the package.
  PACKAGE='maude'
- VERSION='alpha146'
+ VERSION='alpha147'
 
 
 cat >>confdefs.h <<_ACEOF
@@ -6623,7 +6623,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1
 # report actual input values of CONFIG_FILES etc. instead of their
 # values after options handling.
 ac_log="
-This file was extended by Maude $as_me alpha146, which was
+This file was extended by Maude $as_me alpha147, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   CONFIG_FILES    = $CONFIG_FILES
@@ -6689,7 +6689,7 @@ _ACEOF
 cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
 ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`"
 ac_cs_version="\\
-Maude config.status alpha146
+Maude config.status alpha147
 configured by $0, generated by GNU Autoconf 2.69,
   with options \\"\$ac_cs_config\\"
 

configure.ac

@@ -3,7 +3,7 @@
 #
 #	Initialize autoconf stuff.
 #
-AC_INIT(Maude, alpha146, [[email protected]])
+AC_INIT(Maude, alpha147, [[email protected]])
 #
 #	Allow directory names that look like macros.
 #

doc/Makefile.am

@@ -14,4 +14,5 @@ EXTRA_DIST = \
 	alpha143.txt \
 	alpha144.txt \
 	alpha145.txt \
-	alpha146.txt
+	alpha146.txt \
+	alpha147.txt

doc/Makefile.in

@@ -246,7 +246,8 @@ EXTRA_DIST = \
 	alpha143.txt \
 	alpha144.txt \
 	alpha145.txt \
-	alpha146.txt
+	alpha146.txt \
+	alpha147.txt
 
 all: all-am
 

doc/alpha146.txt

@@ -1,7 +1,6 @@
 Alpha 146 release notes
 ========================
 
-
 Changes
 ========
 

doc/alpha147.txt

@@ -0,0 +1,139 @@
+Alpha 147 release notes
+========================
+
+Bug fixes
+==========
+
+(1) A bug in the new ACU optimized matching when a nonlinear variable
+could be used as a stripper variable by mistake producing wrong matches. For
+example:
+
+fmod FOO is
+  pr NAT .
+  sort  Set .
+  subsort Nat < Set .
+var N : Nat .
+  op f : Set Set -> Set [assoc comm] .
+  op g : Nat -> Set .
+  eq g(0) = 0 .
+  eq g(s N) = f(g(N), s N) .
+
+var S : Set .
+  op h : Set -> Set .
+  ceq h(f(N, N, S)) = S if N > 0 .
+endfm
+
+reduce in FOO : h(f(2, g(6))) .
+rewrites: 9 in 0ms cpu (0ms real) (~ rewrites/second)
+result Set: f(0, 1, 3, 4, 5, 6)
+*** correct
+
+reduce in FOO : h(f(2, g(7))) .
+rewrites: 11 in 0ms cpu (0ms real) (~ rewrites/second)
+result Set: f(0, 2, 2, 3, 4, 5, 6, 7)
+*** wrong
+
+Here once the AC argument list gets large enough (>= 8 distinct values) it
+is converted to a red-black tree and the new code runs for the conditional
+equation, even though N has multiplicity > 1 and in fact the pattern is
+treated as h(f(N, S)) so 1 is stripped from the argument list rather than 2.
+
+(2) A bug where the new ACU optimized matching did not deal with fewer than
+two subject subterms remaining. The following examples show crashes where
+only 1 or 0 subject subterms are remaining when the new code executes.
+
+fmod FOO is
+  pr NAT .
+  sort  Set .
+  subsort Nat < Set .
+var N : Nat .
+  op f : Set Set -> Set [assoc comm] .
+  op g : Nat -> Set .
+  eq g(0) = 0 .
+  eq g(s N) = f(g(N), s N) .
+
+var S : Set .
+  op h : Set -> Set .
+  ceq h(f(N, S)) = h(S) if N > 0 .
+  ceq h(f(0, N, S)) = 0 if N > 0 .
+endfm
+
+red h(f(g(7), 0)) .
+
+fmod FOO is
+  pr NAT .
+  sort  Set .
+  subsort Nat < Set .
+var N : Nat .
+  op f : Set Set -> Set [assoc comm] .
+  op g : Nat -> Set .
+  eq g(0) = 0 .
+  eq g(s N) = f(g(N), s N) .
+
+var S : Set .
+  op h : Set -> Set .
+  ceq h(f(N, S)) = h(S) if N > 0 .
+  ceq h(f(0, 0, N, S)) = 0 if N > 0 .
+endfm
+
+red h(f(g(7), 0)) .
+
+(3) A bug where the new ACU optimized matching was mistakenly used when there
+was a non-ground alien present. For example:
+
+fmod FOO is
+  pr NAT .
+  sort  Set .
+  subsort Nat < Set .
+var N : Nat .
+  op f : Set Set -> Set [assoc comm] .
+  op g : Nat -> Set .
+  eq g(0) = 0 .
+  eq g(s N) = f(g(N), s N) .
+
+var S : Set .
+var M : Nat .
+  op h : Set -> Set .
+  op i : Nat -> Nat .
+  ceq h(f(N, S, i(M))) = 0 if N > 0 .
+endfm
+
+reduce in FOO : h(g(7)) .
+rewrites: 8 in 0ms cpu (0ms real) (~ rewrites/second)
+result Set: h(f(0, 1, 2, 3, 4, 5, 6, 7))
+*** correct
+
+reduce in FOO : h(g(8)) .
+rewrites: 12 in 0ms cpu (0ms real) (~ rewrites/second)
+result Zero: 0
+*** wrong
+
+fmod FOO is
+  pr NAT .
+  sort  Set .
+  subsort Nat < Set .
+var N : Nat .
+  op f : Set Set -> Set [assoc comm] .
+  op g : Nat -> Set .
+  eq g(0) = 0 .
+  eq g(s N) = f(g(N), s N) .
+
+var S : Set .
+var M : Nat .
+  op h : Set -> Set .
+  op i : Nat -> Nat .
+  ceq h(f(N, S, i(M))) = M if N > 0 .
+endfm
+
+red h(g(8)) .
+*** crashes
+
+
+Other changes
+==============
+
+(1) Stripper and collector variables for AC/ACU red-black matching are recorded at
+compile time to avoid searching at match time.
+
+(2) AC/ACU red-black matching handles more cases that were previously handed to the
+(slow) backstop AC/ACU matching algorithm.

src/ACU_Theory/ACU_LazySubproblem.cc

@@ -50,9 +50,7 @@
 
 //	ACU theory class definitions
 #include "ACU_Symbol.hh"
-//#include "ACU_DagNode.hh"
 #include "ACU_TreeDagNode.hh"
-//#include "ACU_ExtensionInfo.hh"
 #include "ACU_LazySubproblem.hh"
 
 ACU_LazySubproblem::ACU_LazySubproblem(ACU_BaseDagNode* subject,