alpha148

ChangeLog

@@ -1,3 +1,13 @@
+2023-05-05  Steven Eker  <eker@pup>
+
+	* tests/ResolvedBugs/stripperCollectorSwitchMay2023.maude: added
+
+2023-05-03  Steven Eker  <eker@pup>
+
+	* tests/Corner/ACU_TreeVariableSubproblem.maude: added
+
+==================================Maude148===========================================
+
 2023-04-28  Steven Eker  <eker@pup>
 
 	* tests/ResolvedBugs/redBlackNGA_April2023.maude: added

NEWS

@@ -1,12 +1,26 @@
-Overview of Changes in alpha147
+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 dagnodes 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
-* optimizatons for ACU red-black matching
+* optimizations for ACU red-black matching
 
 Overview of Changes in alpha146 (2023-04-26)
 ============================================

configure

@@ -1,6 +1,6 @@
 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.
-# Generated by GNU Autoconf 2.69 for Maude alpha147.
+# Generated by GNU Autoconf 2.69 for Maude alpha148.
 #
 # Report bugs to <[email protected]>.
 #
@@ -580,8 +580,8 @@ MAKEFLAGS=
 # Identity of this package.
 PACKAGE_NAME='Maude'
 PACKAGE_TARNAME='maude'
-PACKAGE_VERSION='alpha147'
-PACKAGE_STRING='Maude alpha147'
+PACKAGE_VERSION='alpha148'
+PACKAGE_STRING='Maude alpha148'
 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 alpha147 to adapt to many kinds of systems.
+\`configure' configures Maude alpha148 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 alpha147:";;
+     short | recursive ) echo "Configuration of Maude alpha148:";;
    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 alpha147
+Maude configure alpha148
 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 alpha147, which was
+It was created by Maude $as_me alpha148, 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='alpha147'
+ VERSION='alpha148'
 
 
 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 alpha147, which was
+This file was extended by Maude $as_me alpha148, 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 alpha147
+Maude config.status alpha148
 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, alpha147, [[email protected]])
+AC_INIT(Maude, alpha148, [[email protected]])
 #
 #	Allow directory names that look like macros.
 #

doc/Makefile.am

@@ -15,4 +15,5 @@ EXTRA_DIST = \
 	alpha144.txt \
 	alpha145.txt \
 	alpha146.txt \
-	alpha147.txt
+	alpha147.txt \
+	alpha148.txt

doc/Makefile.in

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

doc/alpha148.txt

@@ -0,0 +1,86 @@
+Alpha 148 release notes
+========================
+
+Bug fixes
+==========
+
+(1) A bug in the new ACU matching code where the variables were sorted
+after the indices for ths stripper and collector variables for AC/ACU
+red-black matching had been stored, during compilation, invalidating them
+and causing missed matches. It's quite a tricky bug to demonstrate
+because the variables are also sorted before compilation as part of theory
+normalization.
+
+fmod FOO is
+  pr NAT .
+  sorts Set Elt .
+  subsort Elt < Set .
+var S : Set .
+var E : Elt .
+var N : Nat .
+  op dummy : Set -> Set .
+  eq dummy(S) = S .  *** needed to influence AC ordering
+
+  op z : -> Elt .
+  op p_ : Elt -> Elt .
+  op g : Nat Set -> Set .
+  eq g(s N, E) = f(g(N, p E), E) .
+
+  op f : Set Set -> Set [assoc comm] .
+  op h : Set -> Bool .
+  ceq h(f(S, E)) = true if E = z .
+endfm
+
+red h(g(7, z)) .  *** OK because argument list is too short to be red-black
+red h(g(8, z)) .  *** fails
+
+(2) A bug in the functional metalevel where metaSrewrite() did not
+transfer the rewrite count from the meta-operation to the top level
+context. Illustrated by this example from the test suite:
+
+red in META-LEVEL : metaSrewrite(
+mod 'INC is
+  protecting 'NAT .
+  sorts none .
+  none
+  none
+  none
+  none
+  rl 'N:Nat => 's_['N:Nat] [label('inc)] .
+endm, '0.Nat, ('inc[none]{empty}) *, breadthFirst, 8) .
+
+(3) A bug in the meta-interpreter where the rewrite count from the
+meta-computations performed on behalf of the srewriteTerm() message would
+only be transferred to the enclosing context if and when failure was seen.
+This resulting in the wrong number of rewrites being returned in
+srewroteTerm() messages other than the first, and in the noSuchResult()
+message. Also those rewrites were missing from the top level total if
+the computation did not proceed far enough that the noSuchResult() message
+was seen
+
+Other changes
+==============
+
+(1) ACU matching subproblems in the stripper-collector case when all
+solutions are required no longer caches solutions as it seems to be a net
+lose.
+
+(2) Fast handling for ACU matching subproblems in the stripper-collector
+case where the stripper and/or collector variable is already bound.
+
+(3) A smarter scheme for deciding when to allocate more dag nodes. This idea
+came from the observation that while not caching solutions in (1) saved
+time and memory for matching, it made the system slower overall because
+fewer dag nodes were needed and thus garbage collections were needed more
+frequently. 
+
+(4) If garbage collection reporting is turned on with
+  set show gc on .
+the number of the garbage collection is now shown and the other information
+is also given in megabytes.
+
+(5) There is a command line flag
+  -early-quit=N
+which causes Maude to quit abruptly after the Nth garbage collection. This
+is intended for developer use only, to assist in profiling long running
+examples.

src/ACU_Persistent/ACU_SlowIter.hh

@@ -2,7 +2,7 @@
 
     This file is part of the Maude 3 interpreter.
 
-    Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA.
+    Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA.
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -38,7 +38,8 @@ class ACU_SlowIter : public ACU_Stack
 public:
   ACU_SlowIter();
   ACU_SlowIter(const ACU_Tree& tree);
-
+  void reset(const ACU_Tree& tree);  // so we can reuse an existing ACU_SlowIter
+
   bool valid() const;
   DagNode* getDagNode() const;
   int getMultiplicity() const;
@@ -56,6 +57,13 @@ ACU_SlowIter::ACU_SlowIter(const ACU_Tree& tree)
   stackLeftmostPath(tree.root);
 }
 
+inline void
+ACU_SlowIter::reset(const ACU_Tree& tree)
+{
+  clear();
+  stackLeftmostPath(tree.root);
+}
+
 inline bool
 ACU_SlowIter::valid() const
 {

src/ACU_Persistent/ChangeLog

@@ -1,3 +1,9 @@
+2023-05-02  Steven Eker  <eker@pup>
+
+	* ACU_SlowIter.hh (ACU_SlowIter::reset): added
+
+===================================Maude148===========================================
+
 2019-07-01  Steven Eker  <eker@mu>
 
 	* ACU_RedBlackNode.hh: rewritten using new MemoryCell definition

src/ACU_Theory/ACU_LhsAutomaton.cc

@@ -131,34 +131,22 @@ ACU_LhsAutomaton::addTopVariable(const VariableTerm* variable,
 				 int multiplicity,
 				 bool willBeBound)
 {
-  int nrTopVariables = topVariables.length();
   Sort* s = variable->getSort();
   int bound = topSymbol->sortBound(s);
   bool takeIdentity = topSymbol->takeIdentity(s);
-  if (!willBeBound)
-    {
-      //
-      //	We don't expect the variable to be bound at match time before doing
-      //	a match with this automaton.
-      //
-      ++nrExpectedUnboundVariables;
-      if (multiplicity == 1)
-	{
-	  if (stripperIndex == NONE && !takeIdentity && bound == 1)
-	    stripperIndex = nrTopVariables;
-	  else if (collectorIndex == NONE && bound == UNBOUNDED)
-	    collectorIndex = nrTopVariables;
-	}
-    }
+
+  int nrTopVariables = topVariables.length();
   topVariables.expandBy(1);
   TopVariable& tv = topVariables[nrTopVariables];
   tv.index = variable->getIndex();
   tv.multiplicity = multiplicity;
   tv.sort = s;
   tv.upperBound = bound;
   tv.structure = topSymbol->sortStructure(s);
-  tv.takeIdentity = takeIdentity;
   tv.abstracted = 0;
+  tv.takeIdentity = takeIdentity;
+  tv.willBeBound = willBeBound;
+
   updateTotals(takeIdentity ? 0 : multiplicity,
 	       (bound == UNBOUNDED) ? UNBOUNDED : (bound * multiplicity));
 }
@@ -237,6 +225,10 @@ void
 ACU_LhsAutomaton::complete(MatchStrategy strategy,
 			   int nrIndependent)
 {
+  //
+  //	We need to sort variables before storing indices to variables.
+  //
+  sort(topVariables.begin(), topVariables.end(), topVariableLt);
   //
   //	For red-black greedy matching to be correct we require that
   //	(1) unbound top variables are quasi-linear and don't occur in the
@@ -260,6 +252,26 @@ ACU_LhsAutomaton::complete(MatchStrategy strategy,
   //
   if (treeMatchOK)
     {
+      Index nrVariables = topVariables.size();
+      for (Index i = 0; i < nrVariables; ++i)
+	{
+	  const TopVariable& tv = topVariables[i];
+	  if (!tv.willBeBound)
+	    {
+	      //
+	      //	We don't expect the variable to be bound at match time before doing
+	      //	a match with this automaton.
+	      //
+	      ++nrExpectedUnboundVariables;
+	      if (tv.multiplicity == 1)
+		{
+		  if (stripperIndex == NONE && !tv.takeIdentity && tv.upperBound == 1)
+		    stripperIndex = i;
+		  else if (collectorIndex == NONE && tv.upperBound == UNBOUNDED)
+		    collectorIndex = i;
+		}
+	    }
+	}
       if (strategy == LONE_VARIABLE || strategy == GREEDY)
 	treeMatchOK = collectorIndex != NONE || matchAtTop;
       else if (strategy == FULL)
@@ -286,11 +298,9 @@ ACU_LhsAutomaton::complete(MatchStrategy strategy,
       else
 	treeMatchOK = false;
     }
-
   matchStrategy = strategy;
   Assert(nrIndependent <= nonGroundAliens.length(), "too many independent");
   nrIndependentAliens = nrIndependent;
-  sort(topVariables.begin(), topVariables.end(), topVariableLt);
 }
 
 #ifdef DUMP

src/ACU_Theory/ACU_LhsAutomaton.hh

@@ -132,8 +132,9 @@ private:
     Sort* sort;
     int upperBound;
     AssociativeSymbol::Structure structure;
-    bool takeIdentity;
     LhsAutomaton* abstracted;	// automaton for abstracted term
+    bool takeIdentity;
+    bool willBeBound;  // will be bound at match time
     //
     //	Data storage for match-time use
     //
@@ -260,7 +261,7 @@ private:
   int maxPatternMultiplicity;  // must have at least on subject with >= this multiplicity
   int totalNonGroundAliensMultiplicity;
   int nrIndependentAliens;
-  int nrExpectedUnboundVariables;  // used at semicompile time only
+  int nrExpectedUnboundVariables;  // used at semicompile time only, for red-black case only
   LhsAutomaton* uniqueCollapseAutomaton;
   Vector<TopVariable> topVariables;
   Vector<GroundAlien> groundAliens;