diff --git a/ChangeLog b/ChangeLog index fed3d9fd..9f35dcd7 100755 --- a/ChangeLog +++ b/ChangeLog @@ -1,7 +1,28 @@ +2024-04-16 Steven Eker + + * tests/BuiltIn/stringOps.maude: added + +2024-04-08 Steven Eker + + * tests/Misc/initialEqualityPredicate.maude: added more examples + +2024-04-01 Steven Eker + + * INSTAL: remove refs to gmp-6.2.1 + + * tests/ResolvedBugs/stringToRatConversionMarch2024.maude: added + +2024-03-19 Steven Eker + + * INSTALL: update GMP section on the register x18 issue + +==================================Maude160=========================================== + 2024-03-19 Steven Eker * README.md: updated web links + 2024-03-13 Steven Eker * README.md: added Maude 3.4 details diff --git a/INSTALL b/INSTALL index b197f84b..5479241d 100755 --- a/INSTALL +++ b/INSTALL @@ -87,8 +87,8 @@ make install GMP --- curl -LJO https://gmplib.org/download/gmp/gmp-6.3.0.tar.xz -tar xvf gmp-6.2.1.tar.xz -cd gmp-6.2.1 +tar xvf gmp-6.3.0.tar.xz +cd gmp-6.3.0 mkdir Opt cd Opt @@ -240,9 +240,12 @@ make install GMP --- -curl -LJO https://gmplib.org/download/gmp/gmp-6.2.1.tar.xz -tar xvf gmp-6.2.1.tar.xz -cd gmp-6.2.1 +Note that 6.3.0 or later is needed for Apple silicon because of the +register x18 issue. + +curl -LJO https://gmplib.org/download/gmp/gmp-6.3.0.tar.xz +tar xvf gmp-6.3.0.tar.xz +cd gmp-6.3.0 mkdir HighSierra cd HighSierra diff --git a/NEWS b/NEWS index 04fd11d4..49cd5da1 100755 --- a/NEWS +++ b/NEWS @@ -1,7 +1,17 @@ +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 +* fixed loop mode LaTeX bug Overview of Changes in Maude 3.4 beta (alpha158) (2023-03-12) ============================================================= diff --git a/configure b/configure index 54cd8092..3e75c94e 100755 --- a/configure +++ b/configure @@ -1,6 +1,6 @@ #! /bin/sh # Guess values for system-dependent variables and create Makefiles. -# Generated by GNU Autoconf 2.69 for Maude 3.4. +# Generated by GNU Autoconf 2.69 for Maude alpha160. # # Report bugs to . # @@ -580,8 +580,8 @@ MAKEFLAGS= # Identity of this package. PACKAGE_NAME='Maude' PACKAGE_TARNAME='maude' -PACKAGE_VERSION='3.4' -PACKAGE_STRING='Maude 3.4' +PACKAGE_VERSION='alpha160' +PACKAGE_STRING='Maude alpha160' PACKAGE_BUGREPORT='maude-bugs@lists.cs.illinois.edu' 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 3.4 to adapt to many kinds of systems. +\`configure' configures Maude alpha160 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 3.4:";; + short | recursive ) echo "Configuration of Maude alpha160:";; 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 3.4 +Maude configure alpha160 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 3.4, which was +It was created by Maude $as_me alpha160, 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='3.4' + VERSION='alpha160' 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 3.4, which was +This file was extended by Maude $as_me alpha160, 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 3.4 +Maude config.status alpha160 configured by $0, generated by GNU Autoconf 2.69, with options \\"\$ac_cs_config\\" diff --git a/configure.ac b/configure.ac index 610c2d8b..554ea3be 100755 --- a/configure.ac +++ b/configure.ac @@ -3,7 +3,7 @@ # # Initialize autoconf stuff. # -AC_INIT(Maude, 3.4, [maude-bugs@lists.cs.illinois.edu]) +AC_INIT(Maude, alpha160, [maude-bugs@lists.cs.illinois.edu]) # # Allow directory names that look like macros. # diff --git a/doc/Makefile.am b/doc/Makefile.am index 547f3a06..0cd4d4a6 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -27,4 +27,5 @@ EXTRA_DIST = \ alpha156.txt \ alpha157.txt \ alpha158.txt \ - alpha159.txt + alpha159.txt \ + alpha160.txt diff --git a/doc/Makefile.in b/doc/Makefile.in index ebebd05c..a0b7f918 100644 --- a/doc/Makefile.in +++ b/doc/Makefile.in @@ -259,7 +259,8 @@ EXTRA_DIST = \ alpha156.txt \ alpha157.txt \ alpha158.txt \ - alpha159.txt + alpha159.txt \ + alpha160.txt all: all-am diff --git a/doc/alpha160.txt b/doc/alpha160.txt new file mode 100644 index 00000000..d50f6c5c --- /dev/null +++ b/doc/alpha160.txt @@ -0,0 +1,239 @@ +Alpha 160 release notes +======================== + +Bug fixes +========== + +(1) A bug reported by Carolyn where + op rat : String NzNat ~> Rat [special (...)] . +in fmod CONVERSION didn't handle strings where the first number was 0 +other than 0 itself: + +Maude> red rat("-0", 10) . +reduce in CONVERSION : rat("-0", 10) . +rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second) +result [Rat,FindResult]: rat("-0", 10) +Maude> +> red rat("0/1", 10) . +reduce in CONVERSION : rat("0/1", 10) . +rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second) +result [Rat,FindResult]: rat("0/1", 10) +Maude> +> red rat("-0/1", 10) . +reduce in CONVERSION : rat("-0/1", 10) . +rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second) +result [Rat,FindResult]: rat("-0/1", 10) + +(2) An issue where Maude couldn't be built on platforms where time_t +is 64-bits and long is 32-bits due to GMP not supporting long long. + +(3) A subtle bug where freshly allocated variables at the start of +a vu-narrow were not protected from the garbage collector during the +initial reduction of the start term with those renamed variables in +that case that they disappeared from the term being rewritten, leaving +a potential dangling pointer in the accumulated substitution (which +at this point is just a mapping from the original variables to the +fresh variables). The confluence of events needed to expose this bug +seem hard to arrange deliberately. + +(4) A bug where vu-narrow/fvu-narrow allowed unsafe names such as #1:Foo in +the intial state and/or goal, at both the object level and metalevel. + +mod FOO is + sort Foo . +endm + +vu-narrow #1:Foo =>* X:Foo . +vu-narrow X:Foo =>* #1:Foo . + +New feature +============ + +There is a new fmod STRING-OPS in the prelude which adds extra built-in +operators on characters and strings: + +fmod STRING-OPS is + protecting STRING . + op isControl : Char -> Bool [special (...)] . + op isPrintable : Char -> Bool [special (...)] . + op isWhiteSpace : Char -> Bool [special (...)] . + op isBlank : Char -> Bool [special (...)] . + op isGraphic : Char -> Bool [special (...)] . + op isPunctuation : Char -> Bool [special (...)] . + op isAlphanumeric : Char -> Bool [special (...)] . + op isAlphabetic : Char -> Bool [special (...)] . + op isUppercase : Char -> Bool [special (...)] . + op isLowercase : Char -> Bool [special (...)] . + op isDigit : Char -> Bool [special (...)] . + op isHexadecimalDigit : Char -> Bool [special (...)] . + + op startsWith : String String -> Bool [special (...)] . + op endsWith : String String -> Bool [special (...)] . + + op trimStart : String -> String [special (...)] . + op trimEnd : String -> String [special (...)] . + op trim : String -> String [special (...)] . +endfm + +The is*() functions follow the C++ standard. startsWith() and endWith() +check if the first string starts with (resp. ends with) the second +string. The trim*() functions remove white-space characters from +the start, end, or bothe ends of the string argument. +The reason for placing theses function in a new fmod it that it +is intended to extend it in future with operations that require +lists of strings. + +Other changes +============== + +(1) The operational semantics of the initial equality predicate now allow +more reductions. To illustrate the changes I use this running example: + +fmod FOO is + inc INITIAL-EQUALITY-PREDICATE . + sort Foo . + ops a b c 1 : -> Foo . + op __ : Foo Foo -> Foo [assoc] . + op _+_ : Foo Foo -> Foo [assoc comm] . + op s : Foo Foo -> Foo [comm] . + op f : Foo Foo -> Foo [assoc comm id: 1] . + ops g h p : Foo -> Foo . + var A B C D E W X Y Z : Foo . + eq p(X) = g(h(X)) . +endfm + +Internally Maude has the notion of a symbol f being stable if a term +headed by f cannot change its top symbol under instantiation and axioms. +In the current implementation, a symbol is stable unless it is a variable +or has collapse axioms (idem, id:). This could change in the future since +distributivity would make both of its function symbols unstable. + +A symbol f is equation-free if no equation can match a term with f on top. +This can be an complicated analysis due to collapse but is needed to index +equations under the symbols they might apply to and has existed in Maude +since collapse axioms were introduced. + +A symbol f is said to equationally-stable if it stable and equation-free. + +A term t = f(...) is said to be fixed if it is ground or f is equationally +stable. + +With these definitions the operation semantics of _.=._ change as follows: + +(a) Function symbols no longer need the the ctor attribute to participate +in simplifications. This is because f being equationally-stable makes f +a de facto constructor on all sorts where it is defined, regardless of +whether is has been declared that way. + +red g(X) .=. g(Y) . +reduce in FOO : g(X) .=. g(Y) . +rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second) +result Bool: X .=. Y + +(b) The comparison of a ground term with an unstable top symbol with a +nonground term having an equationally-stable top symbol returns false. + +red f(a, g(b), c) .=. h(X) . +reduce in FOO : h(X) .=. f(a, c, g(b)) . +rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second) +result Bool: false + +(c) A term is headed by an equationally-stable function symbol can never +be equal to a proper subterm. + +(d) For a commutative equationally-stable function symbol s, the case +where the same argument appears under each side and can be canceled in +is recognized. + +red s(g(X), Z) .=. s(Y, g(X)) . +reduce in FOO : s(Z, g(X)) .=. s(Y, g(X)) . +rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second) +result Bool: Z .=. Y + +(e) For an associative-commutative symbol _+_, if the top level terms are +unequal and are both nonground, we examine subterms in the flattened argument +lists; i.e. subterms headed by something other than _+_. Equal arguments on both +sides can be canceled. If one side fully cancels we can return false; otherwise +if one side onlyhas fixed subterms we can check if there are enough arguments to +pair up with the other side or return false. Then we can check for each fixed +subterm on the other side, there is something for it to pair with, or return +false. Finally if we had cancelations we can return the reduced initial equality. + +red g(A) + g(B) + g(C) .=. g(A) + B + h(C) . +reduce in FOO : g(A) + B + h(C) .=. g(A) + g(B) + g(C) . +rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second) +result Bool: false + +red g(A) + g(B) + g(C) .=. g(A) + B . +reduce in FOO : B + g(A) .=. g(A) + g(B) + g(C) . +rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second) +result Bool: B .=. g(B) + g(C) + +(f) For an associative symbol __, if the top level terms are unequal, and are +both nonground we examine subterms in the flattened argument lists; i.e. +subterms headed by something other than __. We attempt to decompose the argument +lists by pairing up fixed subterms at the beginning and end of the associative +argument lists. If we have a pair of fixed subterms with different symbols on +top we can return false. Once no more subterms can be paired off, we pretend +the remaining argument lists are associative-commutative and try to prove they +will always be unequal using the approach for associative-commutative argument +lists in (e) in which case we return false, since they must also always be +unequal modulo associativity. Finally we return the decomposed problem +as a conjunction. + +red g(A) (B) X h(A) Y h(C) .=. h(A) g(D) g(E) Z X h(A) . +reduce in FOO : g(A) B X h(A) Y h(C) .=. h(A) g(D) g(E) Z X h(A) . +rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second) +result Bool: false + +red g(A) X Y h(A) h(C) .=. g(D) g(E) g(D) X h(A) . +reduce in FOO : g(A) X Y h(A) h(C) .=. g(D) g(E) g(D) X h(A) . +rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second) +result Bool: false + +red g(A) g(B) X h(A) Y h(C) .=. g(D) g(E) Z X h(A) . +reduce in FOO : g(A) g(B) X h(A) Y h(C) .=. g(D) g(E) Z X h(A) . +rewrites: 4 in 0ms cpu (0ms real) (~ rewrites/second) +result Bool: E .=. B and A .=. C and A .=. D and Z X .=. X h(A) Y + +(2) The vu-narrow command now supports a disjunction of initial +states: + vu-narrow s1 \/ s2 \/ ... \/ sn =>* p . +The same four search types, =>1, =>+, =>*, =>! are supported. Unlike the +single initial state case, variables may not be shared between the +states and the pattern. Nor may variables be shared between states. +Essentially each initial state generates its own tree of descendents, but +states from one tree may subsume states from another tree if the fold +option is given; in fact one initial state may subsume another. If +a disjunction of initial states is given, the result information includes +the initial state from which the state that unified with the pattern was +narrowed. For example: + +mod FOO is + sort Foo . + ops a a2 b b2 f g : Foo -> Foo . +vars P Q R S T X : Foo . + rl a(f(X)) => a2(X) [narrowing] . + rl b(g(X)) => b2(X) [narrowing] . +endm + +vu-narrow a(P) \/ b(Q) =>* a2(R) . +vu-narrow in FOO : a(P) \/ b(Q) =>* a2(R) . + +Solution 1 +rewrites: 1 in 4ms cpu (1ms real) (250 rewrites/second) +state: a2(@1:Foo) +initial state: a(P) +accumulated substitution: +P --> f(@1:Foo) +variant unifier: +R --> %1:Foo +@1:Foo --> %1:Foo + +No more solutions. + +vu-narrow a(P) \/ b(Q) =>* a2(P) . +vu-narrow in FOO : a(P) \/ b(Q) =>* a2(P) . +Warning: sharing a variable P between initial state a(P) and goal a2(P) is not allowed when narrowing a disjunction of initial states. + +Currently this is only supported at the object level. diff --git a/src/BuiltIn/ChangeLog b/src/BuiltIn/ChangeLog index d1a5f951..f9947d24 100755 --- a/src/BuiltIn/ChangeLog +++ b/src/BuiltIn/ChangeLog @@ -1,3 +1,32 @@ +2024-04-16 Steven Eker + + * stringOpSymbol.cc (StringOpSymbol::attachData): use BIND_OP3() + (StringOpSymbol::getDataAttachments): use CODE_CASE3() + (StringOpSymbol::eqRewrite): use CODE3() + (StringOpSymbol::getDataAttachments): beginsWith -> startsWith + (StringOpSymbol::eqRewrite): beginsWith -> startsWith + (StringOpSymbol::eqRewrite): goto fail on bad string op + (StringOpSymbol::eqRewrite): static_cast before calling + isspace() + (StringOpSymbol::getDataAttachments): added character tests + (StringOpSymbol::eqRewrite): added character tests + +2024-04-15 Steven Eker + + * stringOpSymbol.cc (StringOpSymbol::eqRewrite): added trim + functions and reorganized switch statement + (StringOpSymbol::eqRewrite): use Rope::const_iterator rather than + operator[] to avoid O(n log n) time to trim ropes + (StringOpSymbol::eqRewrite): added beginsWith, endsWith + (StringOpSymbol::getDataAttachments): support new functions + +2024-03-29 Steven Eker + + * stringOpSymbol.cc (StringOpSymbol::ropeToNumber): allow things + like -0, 0/1, -0/2 + +===================================Maude160=========================================== + 2024-03-06 Steven Eker * divisionSymbol.cc (DivisionSymbol::isRat): (both versions) diff --git a/src/BuiltIn/stringOpSymbol.cc b/src/BuiltIn/stringOpSymbol.cc index 24a3d35c..1456be82 100755 --- a/src/BuiltIn/stringOpSymbol.cc +++ b/src/BuiltIn/stringOpSymbol.cc @@ -76,7 +76,7 @@ StringOpSymbol::attachData(const Vector& opDeclaration, const char* purpose, const Vector& data) { - BIND_OP(purpose, StringOpSymbol, op, data); + BIND_OP3(purpose, StringOpSymbol, op, data); return FreeSymbol::attachData(opDeclaration, purpose, data); } @@ -131,25 +131,44 @@ StringOpSymbol::getDataAttachments(const Vector& opDeclaration, const char*& d = data[nrDataAttachments][0]; switch (op) { - CODE_CASE(d, 'f', 'l', "float") - CODE_CASE(d, 'l', 'e', "length") - CODE_CASE(d, 'a', 's', "ascii") - CODE_CASE(d, 'u', 'p', "upperCase") - CODE_CASE(d, 'l', 'o', "lowerCase") + CODE_CASE3(d, 'f', 'l', 'o', "float") + CODE_CASE3(d, 'l', 'e', 'n', "length") + CODE_CASE3(d, 'a', 's', 'c', "ascii") + CODE_CASE3(d, 'u', 'p', 'p', "upperCase") + CODE_CASE3(d, 'l', 'o', 'w', "lowerCase") CODE_CASE(d, '+', 0, "+") CODE_CASE(d, '<', 0, "<") CODE_CASE(d, '<', '=', "<=") CODE_CASE(d, '>', 0, ">") CODE_CASE(d, '>', '=', ">=") - CODE_CASE(d, 'r', 'a', "rat") - CODE_CASE(d, 's', 'u', "substr") - CODE_CASE(d, 'f', 'i', "find") - CODE_CASE(d, 'r', 'f', "rfind") - CODE_CASE(d, 's', 't', "string") - CODE_CASE(d, 'd', 'e', "decFloat") - CODE_CASE(d, 'c', 'h', "char") + CODE_CASE3(d, 'r', 'a', 't', "rat") + CODE_CASE3(d, 's', 'u', 'b', "substr") + CODE_CASE3(d, 'f', 'i', 'n', "find") + CODE_CASE3(d, 'r', 'f', 'i', "rfind") + CODE_CASE3(d, 's', 't', 'r', "string") + CODE_CASE3(d, 'd', 'e', 'c', "decFloat") + CODE_CASE3(d, 'c', 'h', 'a', "char") + + CODE_CASE3(d, 'c', 'n', 't', "cntrl") + CODE_CASE3(d, 'p', 'r', 'i', "print") + CODE_CASE3(d, 's', 'p', 'a', "space") + CODE_CASE3(d, 'b', 'l', 'a', "blank") + CODE_CASE3(d, 'g', 'r', 'a', "graphic") + CODE_CASE3(d, 'p', 'u', 'n', "punct") + CODE_CASE3(d, 'a', 'l', 'n', "alnum") + CODE_CASE3(d, 'a', 'l', 'p', "alpha") + CODE_CASE3(d, 'i', 's', 'u', "isupper") + CODE_CASE3(d, 'i', 's', 'l', "islower") + CODE_CASE3(d, 'd', 'i', 'g', "digit") + CODE_CASE3(d, 'x', 'd', 'i', "xdigit") + + CODE_CASE3(d, 'l', 't', 'r', "ltrim") + CODE_CASE3(d, 'r', 't', 'r', "rtrim") + CODE_CASE3(d, 't', 'r', 'i', "trim") + CODE_CASE3(d, 's', 't', 'a', "startsWith") + CODE_CASE3(d, 'e', 'n', 'd', "endsWith") default: - CantHappen("bad string op"); + CantHappen("bad string op" << op); } FreeSymbol::getDataAttachments(opDeclaration, purposes, data); } @@ -217,46 +236,171 @@ StringOpSymbol::eqRewrite(DagNode* subject, RewritingContext& context) { case 1: { - mpz_class r; - switch (op) + if (trueTerm.getTerm() == nullptr) { - case CODE('f', 'l'): - { - bool error; - char* flStr = left.makeZeroTerminatedString(); - double fl = stringToDouble(flStr, error); - delete [] flStr; - - if (error) - goto fail; - return floatSymbol->rewriteToFloat(subject, context, fl); - } - case CODE('l', 'e'): // length - { - r = left.length(); - break; - } - case CODE('a', 's'): // acsii - { - if (left.length() != 1) + // + // Not a predicate. + // + mpz_class r; + switch (op) + { + case CODE3('f', 'l', 'o'): // float + { + bool error; + char* flStr = left.makeZeroTerminatedString(); + double fl = stringToDouble(flStr, error); + delete [] flStr; + + if (error) + goto fail; + return floatSymbol->rewriteToFloat(subject, context, fl); + } + case CODE3('l', 'e', 'n'): // length + { + return succSymbol->rewriteToNat(subject, context, left.length()); + } + case CODE3('a', 's', 'c'): // acsii + { + if (left.length() != 1) + goto fail; + unsigned char c = left[0]; + return succSymbol->rewriteToNat(subject, context, c); + } + case CODE3('u', 'p', 'p'): // upperCase + { + Rope result = upperCase(left); + return rewriteToString(subject, context, result); + } + case CODE3('l', 'o', 'w'): // lowerCase + { + Rope result = lowerCase(left); + return rewriteToString(subject, context, result); + } + case CODE3('l', 't', 'r'): // trimStart (left trim) + { + Index len = left.length(); + Rope::const_iterator j = left.begin(); + for (Index i = 0; i < len; ++i, ++j) + { + if (!isspace(static_cast(*j))) + return rewriteToString(subject, context, left.substr(i, len - i)); + } + break; + } + case CODE3('r', 't', 'r'): // trimEnd (right trim) + { + Rope::const_iterator j = left.end(); + for (Index i = left.length(); i > 0; --i) + { + --j; + if (!isspace(static_cast(*j))) + return rewriteToString(subject, context, left.substr(0, i)); + } + break; + } + case CODE3('t', 'r', 'i'): // trim + { + Index len = left.length(); + Rope::const_iterator j = left.begin(); + for (Index i = 0; i < len; ++i, ++j) + { + if (!isspace(static_cast(*j))) + { + Index nrCharsWanted = len - i; + for (Rope::const_iterator e = left.end() - 1; + nrCharsWanted > 1 && isspace(static_cast(*e)); + --nrCharsWanted, --e) + ; + return rewriteToString(subject, context, left.substr(i, nrCharsWanted)); + } + } + break; + } + default: + CantHappen("bad string op" << op); goto fail; - r = static_cast(left[0]); - break; - } - case CODE('u', 'p'): // upperCase - { - Rope result = upperCase(left); - return rewriteToString(subject, context, result); - } - case CODE('l', 'o'): // lowerCase - { - Rope result = lowerCase(left); - return rewriteToString(subject, context, result); - } - default: - CantHappen("bad string op"); + } + return rewriteToString(subject, context, Rope()); // empty rope + } + else + { + // + // Character predicate. + // + if (left.length() != 1) + goto fail; + unsigned char c = left[0]; + bool r; + switch (op) + { + case CODE3('c', 'n', 't'): + { + r = iscntrl(c); + break; + } + case CODE3('p', 'r', 'i'): + { + r = isprint(c); + break; + } + case CODE3('s', 'p', 'a'): + { + r = isspace(c); + break; + } + case CODE3('b', 'l', 'a'): + { + r = isblank(c); + break; + } + case CODE3('g', 'r', 'a'): + { + r = isgraph(c); + break; + } + case CODE3('p', 'u', 'n'): + { + r = ispunct(c); + break; + } + case CODE3('a', 'l', 'n'): + { + r = isalnum(c); + break; + } + case CODE3('a', 'l', 'p'): + { + r = isalpha(c); + break; + } + case CODE3('i', 's', 'u'): // to avoid clash with upperCase + { + r = isupper(c); + break; + } + case CODE3('i', 's', 'l'): // to avoid clash with lowerCase + { + r = islower(c); + break; + } + case CODE3('d', 'i', 'g'): + { + r = isdigit(c); + break; + } + case CODE3('x', 'd', 'i'): + { + r = isxdigit(c); + break; + } + default: + { + CantHappen("bad string op" << op); + goto fail; + } + } + return context.builtInReplace(subject, r ? trueTerm.getDag() : falseTerm.getDag()); } - return succSymbol->rewriteToNat(subject, context, r); } case 2: { @@ -274,26 +418,57 @@ StringOpSymbol::eqRewrite(DagNode* subject, RewritingContext& context) return rewriteToString(subject, context, t); } case '<': - r = left < right; - break; + { + r = left < right; + break; + } case '>': - r = left > right; - break; + { + r = left > right; + break; + } case CODE('<', '='): - r = left <= right; - break; + { + r = left <= right; + break; + } case CODE('>', '='): - r = left >= right; - break; + { + r = left >= right; + break; + } + case CODE3('s', 't', 'a'): // startsWith + case CODE3('e', 'n', 'd'): // endsWith + { + Index leftLen = left.length(); + Index rightLen = right.length(); + if (leftLen < rightLen) + r = false; + else + { + r = true; + Rope::const_iterator leftIter = (op == CODE3('s', 't', 'a')) ? left.begin() : left.begin() + (leftLen - rightLen); + Rope::const_iterator rightIter = right.begin(); + for (Index i = 0; i < rightLen; ++i, ++leftIter, ++rightIter) + { + if (*leftIter != *rightIter) + { + r = false; + break; + } + } + } + break; + } default: - CantHappen("bad string op"); - r = false; // avoid compiler warning + CantHappen("bad string op" << op); + goto fail; } Assert(trueTerm.getTerm() != 0 && falseTerm.getTerm() != 0, "null true/false for relational op"); return context.builtInReplace(subject, r ? trueTerm.getDag() : falseTerm.getDag()); } - else if (op == CODE('r', 'a')) + else if (op == CODE3('r', 'a', 't')) // rat { DebugAdvisory("StringOpSymbol::eqRewrite() entered rat case for " << subject); DagNode* a1 = d->getArgument(1); @@ -334,7 +509,7 @@ StringOpSymbol::eqRewrite(DagNode* subject, RewritingContext& context) { switch (op) { - case CODE('s', 'u'): // substr + case CODE3('s', 'u', 'b'): // substr { DagNode* a1 = d->getArgument(1); DagNode* a2 = d->getArgument(2); @@ -364,15 +539,15 @@ StringOpSymbol::eqRewrite(DagNode* subject, RewritingContext& context) int r; switch (op) { - case CODE('f', 'i'): // find + case CODE3('f', 'i', 'n'): // find r = fwdFind(left, pattern, index); break; - case CODE('r', 'f'): // rfind + case CODE3('r', 'f', 'i'): // rfind r = revFind(left, pattern, index); break; default: - CantHappen("bad string op"); - r = 0; // avoid compiler warning + CantHappen("bad string op" << op); + goto fail; } Assert(notFoundTerm.getTerm() != 0, "null notFound for find op"); if (r == NONE) @@ -388,12 +563,12 @@ StringOpSymbol::eqRewrite(DagNode* subject, RewritingContext& context) } else if (a0->symbol() == floatSymbol) { - if (nrArgs == 1 && op == CODE('s', 't')) + if (nrArgs == 1 && op == CODE3('s', 't', 'r')) // string { double fl = safeCast(FloatDagNode*, a0)->getValue(); return rewriteToString(subject, context, doubleToString(fl)); } - else if (nrArgs == 2 && op == CODE('d', 'e')) + else if (nrArgs == 2 && op == CODE3('d', 'e', 'c')) // decFloat { DagNode* a1 = d->getArgument(1); Assert(succSymbol != 0, "succSymbol undefined"); @@ -415,7 +590,7 @@ StringOpSymbol::eqRewrite(DagNode* subject, RewritingContext& context) } } } - else if (op == CODE('s', 't') && nrArgs == 2) + else if (op == CODE3('s', 't', 'r') && nrArgs == 2) { DagNode* a1 = d->getArgument(1); Assert(succSymbol != 0, "succSymbol undefined"); @@ -470,7 +645,7 @@ StringOpSymbol::eqRewrite(DagNode* subject, RewritingContext& context) { switch (op) { - case CODE('c', 'h'): // char + case CODE3('c', 'h', 'a'): // char { DagNode* a0 = d->getArgument(0); Assert(succSymbol != 0, "succSymbol undefined"); @@ -589,8 +764,10 @@ StringOpSymbol::ropeToNumber(const Rope& subject, ++i; } char c = subject[i]; - if (!isalnum(c) || (c == '0' && len > 1)) + if (!isalnum(c)) return false; + if (c == '0' && len > i + 1 && subject[i + 1] != '/') + return false; // we don't allow numbers starting with 0 except for things like 0, -0, -0/2 for (i++; i < len; i++) { char c = subject[i]; diff --git a/src/Core/ChangeLog b/src/Core/ChangeLog index 1b3f90c6..3d9dc0c5 100644 --- a/src/Core/ChangeLog +++ b/src/Core/ChangeLog @@ -1,3 +1,9 @@ +2024-04-26 Steven Eker + + * narrowingVariableInfo.hh (class NarrowingVariableInfo): make copyable + +===================================Maude160=========================================== + 2024-03-05 Steven Eker * argumentIterator.hh (ArgumentIterator::ArgumentIterator): take diff --git a/src/Core/narrowingVariableInfo.hh b/src/Core/narrowingVariableInfo.hh index f44100e4..9d6a5fe5 100644 --- a/src/Core/narrowingVariableInfo.hh +++ b/src/Core/narrowingVariableInfo.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2007 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 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 @@ -29,8 +29,6 @@ class NarrowingVariableInfo { - NO_COPYING(NarrowingVariableInfo); - public: NarrowingVariableInfo() {} diff --git a/src/FreeTheory/ChangeLog b/src/FreeTheory/ChangeLog index ed46c547..7e6f3ca1 100755 --- a/src/FreeTheory/ChangeLog +++ b/src/FreeTheory/ChangeLog @@ -1,3 +1,26 @@ +2024-03-20 Steven Eker + + * freeSymbol.cc (FreeSymbol::eqRewrite) + (FreeSymbol::computeBaseSort) + (FreeSymbol::normalizeAndComputeTrueSort) + (FreeSymbol::stackArguments, FreeSymbol::termify) + (FreeSymbol::computeGeneralizedSort) + (FreeSymbol::determineGround) + (FreeSymbol::computeGeneralizedSort2, FreeSymbol::makeCanonical) + (FreeSymbol::makeCanonicalCopy): use DagNode* const* + + * freeTerm.cc (FreeTerm::compareArguments) + (FreeTerm::partialCompareArguments): use DagNode* const* + + * freeDagNode.hh (FreeDagNode::argArray): split into const and + non-const versions + + * freeDagArgumentIterator.hh (class FreeDagArgumentIterator): use + pointer to constant point to DagNode + (FreeDagArgumentIterator::FreeDagArgumentIterator): updated + +===================================Maude160=========================================== + 2024-03-14 Steven Eker * freeTerm.cc (FreeTerm::compareArguments): (Term* version) diff --git a/src/FreeTheory/freeDagArgumentIterator.hh b/src/FreeTheory/freeDagArgumentIterator.hh index 1bbd3030..6aa19299 100755 --- a/src/FreeTheory/freeDagArgumentIterator.hh +++ b/src/FreeTheory/freeDagArgumentIterator.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-2024 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 @@ -29,19 +29,19 @@ class FreeDagArgumentIterator : public RawDagArgumentIterator { public: - FreeDagArgumentIterator(DagNode** first, int nrArgs); + FreeDagArgumentIterator(DagNode* const* first, int nrArgs); bool valid() const; DagNode* argument() const; void next(); private: - DagNode** position; + DagNode* const* position; int nrRemaining; }; inline -FreeDagArgumentIterator::FreeDagArgumentIterator(DagNode** first, int nrArgs) +FreeDagArgumentIterator::FreeDagArgumentIterator(DagNode* const* first, int nrArgs) { position = first; nrRemaining = nrArgs; diff --git a/src/FreeTheory/freeDagNode.cc b/src/FreeTheory/freeDagNode.cc index 5cc2d6f5..b82f7351 100755 --- a/src/FreeTheory/freeDagNode.cc +++ b/src/FreeTheory/freeDagNode.cc @@ -81,7 +81,7 @@ FreeDagNode::getHashValue() return hashCache[nrWords - 1].size; size_t hashValue = symbol()->getHashValue(); int nrArgs = symbol()->arity(); - DagNode** p = argArray(); + DagNode* const* p = argArray(); for (int i = 0; i < nrArgs; i++) hashValue = hash(hashValue, (*p++)->getHashValue()); if (nrArgs != nrWords) @@ -104,8 +104,8 @@ FreeDagNode::compareArguments(const DagNode* other) const const FreeDagNode* qd = static_cast(other); for (;;) { - DagNode** p = pd->argArray(); - DagNode** q = qd->argArray(); + DagNode* const* p = pd->argArray(); + DagNode* const* q = qd->argArray(); for (int i = nrArgs - 1; i > 0; --i, ++p, ++q) { @@ -142,7 +142,7 @@ FreeDagNode::markArguments() int nrArgs = symbol()->arity(); if (nrArgs != 0) { - DagNode** p = argArray(); + DagNode* const* p = argArray(); while (--nrArgs > 0) (*p++)->mark(); return *p; @@ -158,7 +158,7 @@ FreeDagNode::copyEagerUptoReduced2() int nrArgs = s->arity(); if (nrArgs != 0) { - DagNode** p = argArray(); + DagNode* const* p = argArray(); DagNode** q = n->argArray(); if (s->standardStrategy()) // everything is eager { @@ -182,7 +182,7 @@ FreeDagNode::copyAll2() int nrArgs = s->arity(); if (nrArgs != 0) { - DagNode** p = argArray(); + DagNode* const* p = argArray(); DagNode** q = n->argArray(); for (int i = nrArgs; i > 0; i--, p++, q++) *q = (*p)->copyAll(); @@ -194,7 +194,7 @@ void FreeDagNode::clearCopyPointers2() { int nrArgs = symbol()->arity(); - DagNode** p = argArray(); + DagNode* const* p = argArray(); for (int i = nrArgs; i > 0; i--, p++) (*p)->clearCopyPointers(); } @@ -207,7 +207,7 @@ FreeDagNode::overwriteWithClone(DagNode* old) int nrArgs = s->arity(); d->copySetRewritingFlags(this); d->setSortIndex(getSortIndex()); - DagNode** p = argArray(); + DagNode* const* p = argArray(); DagNode** q = d->argArray(); for (int i = nrArgs; i > 0; i--, p++, q++) *q = *p; @@ -221,7 +221,7 @@ FreeDagNode::makeClone() int nrArgs = s->arity(); d->copySetRewritingFlags(this); d->setSortIndex(getSortIndex()); - DagNode** p = argArray(); + DagNode* const* p = argArray(); DagNode** q = d->argArray(); for (int i = nrArgs; i > 0; i--, p++, q++) *q = *p; @@ -235,7 +235,7 @@ FreeDagNode::copyWithReplacement(int argIndex, DagNode* replacement) FreeDagNode* d = new FreeDagNode(s); int nrArgs = s->arity(); Assert(argIndex >= 0 && argIndex < nrArgs, "bad argIndex"); - DagNode** p = argArray(); + DagNode* const* p = argArray(); DagNode** q = d->argArray(); for (int i = 0; i < nrArgs; i++, p++, q++) *q = (i == argIndex) ? replacement : *p; @@ -259,7 +259,7 @@ FreeDagNode::copyWithReplacement(Vector& redexStack, "bad replacement arg index"); FreeDagNode* d = new FreeDagNode(s); - DagNode** p = argArray(); + DagNode* const* p = argArray(); DagNode** q = d->argArray(); int nextReplacementIndex = redexStack[first].argIndex(); for (int i = 0; i < nrArgs; i++, p++, q++) @@ -287,7 +287,7 @@ FreeDagNode::computeBaseSortForGroundSubterms(bool warnAboutUnimplemented) ReturnResult result = GROUND; Symbol* s = symbol(); int nrArgs = s->arity(); - DagNode** args = argArray(); + DagNode* const* args = argArray(); for (int i = 0; i < nrArgs; ++i) { ReturnResult r = args[i]->computeBaseSortForGroundSubterms(warnAboutUnimplemented); @@ -313,8 +313,8 @@ FreeDagNode::computeSolvedForm2(DagNode* rhs, { int nrArgs = s->arity(); Assert(nrArgs > 0, "we shouldn't be called on constants " << this); - DagNode** args = argArray(); - DagNode** rhsArgs = safeCast(FreeDagNode*, rhs)->argArray(); + DagNode* const* args = argArray(); + DagNode* const* rhsArgs = safeCast(FreeDagNode*, rhs)->argArray(); for (int i = 0; i < nrArgs; ++i) { if (!(args[i]->computeSolvedForm(rhsArgs[i], solution, pending))) @@ -363,7 +363,7 @@ FreeDagNode::purifyAndOccurCheck(DagNode* repVar, FreeSymbol* s = symbol(); int nrArgs = s->arity(); - DagNode** args = argArray(); + DagNode* const* args = argArray(); for (int i = 0; i < nrArgs; ++i) { DagNode* arg = args[i]; @@ -482,7 +482,7 @@ FreeDagNode::insertVariables2(NatSet& occurs) int i = symbol()->arity(); if (i > 0) { - for (DagNode** p = argArray(); i > 0; i--, p++) + for (DagNode* const* p = argArray(); i > 0; i--, p++) (*p)->insertVariables(occurs); } } @@ -495,7 +495,7 @@ FreeDagNode::instantiate2(const Substitution& substitution, bool maintainInvaria int nrArgs = s->arity(); Assert(nrArgs > 0, "we shouldn't be called on constants: " << this); - DagNode** args = argArray(); + DagNode* const* args = argArray(); for (int i = 0; i < nrArgs; ++i) { if (DagNode* n = args[i]->instantiate(substitution, maintainInvariants)) @@ -559,7 +559,7 @@ bool FreeDagNode::indexVariables2(NarrowingVariableInfo& indices, int baseIndex) { int nrArgs = symbol()->arity(); - DagNode** args = argArray(); + DagNode* const* args = argArray(); bool ground = true; for (int i = 0; i < nrArgs; ++i) { @@ -579,7 +579,7 @@ FreeDagNode::instantiateWithReplacement(const Substitution& substitution, FreeDagNode* d = new FreeDagNode(s); int nrArgs = s->arity(); Assert(argIndex >= 0 && argIndex < nrArgs, "bad argIndex"); - DagNode** p = argArray(); + DagNode* const* p = argArray(); DagNode** q = d->argArray(); for (int i = 0; i < nrArgs; i++) { @@ -607,7 +607,7 @@ FreeDagNode::instantiateWithCopies2(const Substitution& substitution, const Vect int nrArgs = s->arity(); Assert(nrArgs > 0, "we shouldn't be called on constants"); - DagNode** args = argArray(); + DagNode* const* args = argArray(); for (int i = 0; i < nrArgs; ++i) { DagNode* a = args[i]; diff --git a/src/FreeTheory/freeDagNode.hh b/src/FreeTheory/freeDagNode.hh index d5dc9d6e..196fba81 100755 --- a/src/FreeTheory/freeDagNode.hh +++ b/src/FreeTheory/freeDagNode.hh @@ -88,7 +88,8 @@ private: MemoryBlock::MachineWord hashCache[nrWords]; // so we can use the last word as a hash value if nrArgs != nrWords }; - DagNode** argArray() const; + DagNode* const* argArray() const; + DagNode** argArray(); DagNode* markArguments(); DagNode* copyEagerUptoReduced2(); DagNode* copyAll2(); @@ -208,10 +209,16 @@ FreeDagNode::FreeDagNode(Symbol* symbol, int /* dummy */, DagNode* a0, DagNode* } #endif -inline DagNode** +inline DagNode* const* FreeDagNode::argArray() const { - return needToCallDtor() ? external : const_cast(&(internal[0])); + return needToCallDtor() ? external : &(internal[0]); +} + +inline DagNode** +FreeDagNode::argArray() +{ + return needToCallDtor() ? external : &(internal[0]); } inline DagNode* diff --git a/src/FreeTheory/freeSymbol.cc b/src/FreeTheory/freeSymbol.cc index 4ca43384..d3738ab7 100755 --- a/src/FreeTheory/freeSymbol.cc +++ b/src/FreeTheory/freeSymbol.cc @@ -156,7 +156,7 @@ FreeSymbol::eqRewrite(DagNode* subject, RewritingContext& context) if (standardStrategy()) { int nrArgs = arity(); - DagNode** args = static_cast(subject)->argArray(); + DagNode* const* args = static_cast(subject)->argArray(); for (int i = nrArgs; i > 0; i--, args++) (*args)->reduce(context); return DISC_NET.applyReplace(subject, context); @@ -277,7 +277,7 @@ FreeSymbol::computeBaseSort(DagNode* subject) subject->setSortIndex(traverse(0, 0)); // HACK return; } - DagNode** args = static_cast(subject)->argArray(); + DagNode* const* args = static_cast(subject)->argArray(); int state = 0; for (int i = 0; i < nrArgs; i++) @@ -301,7 +301,7 @@ FreeSymbol::normalizeAndComputeTrueSort(DagNode* subject, RewritingContext& cont { Assert(this == subject->symbol(), "bad symbol"); int nrArgs = arity(); - DagNode** args = static_cast(subject)->argArray(); + DagNode* const* args = static_cast(subject)->argArray(); // // First make sure each of our subterms has a sort. // @@ -325,7 +325,7 @@ FreeSymbol::stackArguments(DagNode* subject, if (nrArgs != 0) { const NatSet& frozen = getFrozen(); - DagNode** args = static_cast(subject)->argArray(); + DagNode* const* args = static_cast(subject)->argArray(); for (int i = 0; i < nrArgs; i++) { DagNode* d = args[i]; @@ -340,7 +340,7 @@ FreeSymbol::termify(DagNode* dagNode) { int nrArgs = arity(); Vector args(nrArgs); - DagNode** dagNodeArgs = safeCast(FreeDagNode*, dagNode)->argArray(); + DagNode* const* dagNodeArgs = safeCast(FreeDagNode*, dagNode)->argArray(); for (int i = 0; i < nrArgs; i++) { DagNode* d = dagNodeArgs[i]; @@ -379,7 +379,7 @@ FreeSymbol::computeGeneralizedSort(const SortBdds& sortBdds, DebugAdvisory("getting sort function for " << this << " " << subject); const Vector& sortFunction = sortBdds.getSortFunction(this); - DagNode** args = safeCast(FreeDagNode*, subject)->argArray(); + DagNode* const* args = safeCast(FreeDagNode*, subject)->argArray(); int varCounter = 0; bddPair* argMap = bdd_newpair(); for (int i = 0; i < nrArgs; i++) @@ -407,7 +407,7 @@ bool FreeSymbol::determineGround(DagNode* dagNode) { Index nrArgs = arity(); - DagNode** args = safeCastNonNull(dagNode)->argArray(); + DagNode* const* args = safeCastNonNull(dagNode)->argArray(); for (Index i = 0; i < nrArgs; ++i) { if (!(args[i]->determineGround())) @@ -431,7 +431,7 @@ FreeSymbol::computeGeneralizedSort2(const SortBdds& sortBdds, // Gather the input BDDs for the generalized sorts of the arguments. // Vector inputBdds; - DagNode** args = safeCast(FreeDagNode*, subject)->argArray(); + DagNode* const* args = safeCast(FreeDagNode*, subject)->argArray(); for (int i = 0; i < nrArgs; i++) args[i]->computeGeneralizedSort2(sortBdds, realToBdd, inputBdds); // @@ -448,7 +448,7 @@ DagNode* FreeSymbol::makeCanonical(DagNode* original, HashConsSet* hcs) { int nrArgs = arity(); - DagNode** p = safeCast(FreeDagNode*, original)->argArray(); + DagNode* const* p = safeCast(FreeDagNode*, original)->argArray(); for (int i = 0; i < nrArgs; i++) { DagNode* d = p[i]; @@ -487,7 +487,7 @@ FreeSymbol::makeCanonicalCopy(DagNode* original, HashConsSet* hcs) DagNode** q = n->argArray(); int nrArgs = arity(); - DagNode** p = safeCast(FreeDagNode*, original)->argArray(); + DagNode* const* p = safeCast(FreeDagNode*, original)->argArray(); for (int i = 0; i < nrArgs; ++i, ++p, ++q) *q = hcs->getCanonical(hcs->insert(*p)); return n; diff --git a/src/FreeTheory/freeTerm.cc b/src/FreeTheory/freeTerm.cc index 7c4945e8..be7d3159 100755 --- a/src/FreeTheory/freeTerm.cc +++ b/src/FreeTheory/freeTerm.cc @@ -181,7 +181,7 @@ FreeTerm::compareArguments(const DagNode* other) const int nrArgs = other->symbol()->arity(); if (nrArgs != 0) { - DagNode** q = static_cast(other)->argArray(); + DagNode* const* q = static_cast(other)->argArray(); Vector::const_iterator p = argArray.begin(); for (;;) { @@ -204,7 +204,7 @@ FreeTerm::partialCompareArguments(const Substitution& partialSubstitution, DagNo int nrArgs = argArray.size(); if (nrArgs != 0) { - DagNode** da = safeCast(FreeDagNode*, other)->argArray(); + DagNode* const* da = safeCast(FreeDagNode*, other)->argArray(); for (Term* t : argArray) { int r = t->partialCompare(partialSubstitution, *da); diff --git a/src/Higher/ChangeLog b/src/Higher/ChangeLog index 6917ba94..e10ec3d0 100755 --- a/src/Higher/ChangeLog +++ b/src/Higher/ChangeLog @@ -1,3 +1,230 @@ +2024-05-02 Steven Eker + + * narrowingSequenceSearch3.cc: + (NarrowingSequenceSearch3::NarrowingSequenceSearch3): use new + handleInitialState() convention + + * narrowingSequenceSearch3.hh (class NarrowingSequenceSearch3): updated + decl for handleInitialState() + + * narrowingSequenceSearch3.cc + (NarrowingSequenceSearch3::NarrowingSequenceSearch3): fix bug where + empty startStates caused nrInitialStatesToTry to be wrong + (NarrowingSequenceSearch3::handleInitialState): check for unsafe + variable names here + + * narrowingSequenceSearch3.hh (NarrowingSequenceSearch3::problemOK): + added + + * narrowingSequenceSearch3.cc + (NarrowingSequenceSearch3::NarrowingSequenceSearch3): check for unsafe + variable names + + * narrowingSequenceSearch3.hh (class NarrowingSequenceSearch3): added data + member problemOkay + + * narrowingSequenceSearch3.cc + (NarrowingSequenceSearch3::NarrowingSequenceSearch3): check for + variables shared between initial states + (NarrowingSequenceSearch3::NarrowingSequenceSearch3): check for + variables shared between initial state and goal in term disjunction case + +2024-05-01 Steven Eker + + * narrowingSequenceSearch3.cc (NarrowingSequenceSearch3::findNextUnifier): + lockPath() -> lockPathToCurrentState() + + * narrowingFolder.hh (class NarrowingFolder): lockPath() -> + lockPathToCurrentState() + + * narrowingFolder.cc (NarrowingFolder::lockPath): becomes + lockPathToCurrentState() + + * narrowingSequenceSearch3.cc + (NarrowingSequenceSearch3::NarrowingSequenceSearch3): pass keepHistory + = true to stateCollection if KEEP_HISTORY | KEEP_PATHS + + * narrowingFolder.cc (NarrowingFolder::getNextSurvivingState): added + Assert()s that an unexplore state is neither locked nor subsumed + + * narrowingSequenceSearch3.cc + (NarrowingSequenceSearch3::findNextUnifier): if KEEP_PATHS then lock + the path of any state that unifies with goal + + * narrowingSequenceSearch3.hh (class NarrowingSequenceSearch3): + KEEP_FULL_HISTORY -> KEEP_PATH; added INVARIANT to enum Flags + (NarrowingSequenceSearch3::getVariantFlags): added + +2024-04-30 Steven Eker + + * narrowingSequenceSearch3.hh (class NarrowingSequenceSearch3): deleted + data member needToTryInitialState; added data member nrInitialStatesToTry + + * narrowingSequenceSearch3.cc + (NarrowingSequenceSearch3::findNextInterestingState): handle trying + multiple initial states + (NarrowingSequenceSearch3::NarrowingSequenceSearch3): initialize + nrInitialStatesToTry; don't initialize needToTryInitialState + + * narrowingFolder.hh (NarrowingFolder::exists): added + + * narrowingSequenceSearch3.hh (class NarrowingSequenceSearch3): added + comment that NONE is used to represent unbounded + +2024-04-29 Steven Eker + + * narrowingFolder.cc (NarrowingFolder::RetainedState::RetainedState): + don't initialized stuff that is initialized in the struct decl + (NarrowingFolder::insertState): mark locked states as subsumed rather + than deleting them + (NarrowingFolder::insertState): don't try to subsume the new state by + a state that itself is marked subsumed + (NarrowingFolder::insertState): don't try to subsume states that are + already marked as subsumed + (NarrowingFolder::cleanGraph): don't delete locked states even if + they have no descendents + (NarrowingFolder::cleanGraph): Assert() that we don't have a locked state + if we're not keeping history + (NarrowingFolder::lockPath): added + + * narrowingFolder.hh (class NarrowingFolder): added data member locked + to struct RetainedState + (class NarrowingFolder): reorganized struct RetainedState + + * narrowingSequenceSearch3.hh (class NarrowingSequenceSearch3): added + VFOLD and KEEP_FULL_HISTORY to enum Flags and renumbered + +2024-04-26 Steven Eker + + * narrowingSequenceSearch3.hh (class NarrowingSequenceSearch3): added + data member protectedSubstitution + + * narrowingSequenceSearch3.cc + (NarrowingSequenceSearch3::markReachableNodes): mark + protectedSubstitution + (NarrowingSequenceSearch3::NarrowingSequenceSearch3): clear + protectedSubstitution pointer; don't init startStates + (NarrowingSequenceSearch3::handleInitialState): use protectedSubsitution + to stop fresh variables from being garbage collected if they disappear + from initial state during rewriting + + * narrowingSequenceSearch3.hh + (NarrowingSequenceSearch3::getNrInitialStates): use initalStates + rather than startStates + (class NarrowingSequenceSearch3): added data member termDisjunction + (NarrowingSequenceSearch3::getStateInfo): check if we have a + termDisjunction + (NarrowingSequenceSearch3::getInitialVariableInfo): check if we have + a termDisjunction + + * narrowingSequenceSearch3.cc + (NarrowingSequenceSearch3::NarrowingSequenceSearch3): use + handleInitialState() + + * narrowingSequenceSearch3.hh (class NarrowingSequenceSearch3): added + decl for handleInitialState() + + * narrowingSequenceSearch3.cc + (NarrowingSequenceSearch3::handleInitialState): added + + * narrowingSequenceSearch3.hh (class NarrowingSequenceSearch3): added + struct InitialState and data member initialStates; deleted data member + startStates + +2024-04-25 Steven Eker + + * narrowingSequenceSearch3.cc + (NarrowingSequenceSearch3::NarrowingSequenceSearch3): only add + accumulated substitutions to initial states which survive + +2024-04-24 Steven Eker + + * narrowingSequenceSearch3.hh + (NarrowingSequenceSearch3::getNrInitialStates): added + + * narrowingFolder.hh (NarrowingFolder::getRootIndex): added + + * narrowingSequenceSearch3.hh (class NarrowingSequenceSearch3): updated + decl for getStateInfo() + (NarrowingSequenceSearch3::getStateInfo): fill out initialStateDag + + * narrowingSequenceSearch3.cc + (NarrowingSequenceSearch3::markReachableNodes): protect startStates + rather than original variables + + * narrowingSequenceSearch3.hh (class NarrowingSequenceSearch3): added + startStates data member + + * narrowingSequenceSearch3.cc + (NarrowingSequenceSearch3::NarrowingSequenceSearch3): save startStates + + * narrowingFolder.hh (class NarrowingFolder): made RetainedState::depth + const + (class NarrowingFolder): updated decl for RetainedState() + + * narrowingFolder.cc (NarrowingFolder::RetainedState::RetainedState): + take and fill out rootIndex and depth + (NarrowingFolder::insertState): pass rootIndex and depth to + RetainedState() + + * narrowingFolder.hh (class NarrowingFolder): added data member + rootIndex + +2024-04-23 Steven Eker + + * narrowingSequenceSearch3.cc + (NarrowingSequenceSearch3::markReachableNodes): added + + * narrowingSequenceSearch3.hh (class NarrowingSequenceSearch3): derive + from SimpleRootContainer + + * narrowingSequenceSearch3.cc + (NarrowingSequenceSearch3::NarrowingSequenceSearch3): put multiple + states in the stateCollection + +2024-04-22 Steven Eker + + * narrowingSequenceSearch3.hh (class NarrowingSequenceSearch3): + updated decl for ctor + + * narrowingSequenceSearch3.cc: take startStates argument + +2024-04-19 Steven Eker + + * narrowingFolder.hh: fix comment + (class NarrowingFolder): rearrange data members + +2024-03-21 Steven Eker + + * unificationProblem.cc (UnificationProblem::UnificationProblem): + use safeCastNonNull<> + (UnificationProblem::bindFreeVariables): use safeCastNonNull<> + (UnificationProblem::findOrderSortedUnifiers): use + safeCastNonNull<> (3 places) + + * temporalSymbol.cc (TemporalSymbol::copyAttachments): use + safeCastNonNull<> + + * satSolverSymbol.cc (SatSolverSymbol::copyAttachments): use + safeCastNonNull<> + (SatSolverSymbol::eqRewrite): use safeCastNonNull<> + + * rewriteConditionFragment.cc (RewriteConditionFragment::solve): + use safeCastNonNull<> + + * narrowingUnificationProblem.cc + (NarrowingUnificationProblem::variableIndexToSort): use + safeCastNonNull<> (2 places) + + * modelCheckerSymbol.cc (ModelCheckerSymbol::copyAttachments): + use safeCastNonNull<> + (ModelCheckerSymbol::eqRewrite): use safeCastNonNull<> + + * assignmentConditionFragment.cc (AssignmentConditionFragment::solve): + use safeCastNonNull<> + +===================================Maude160=========================================== + 2024-01-24 Steven Eker * narrowingSearchState.cc: OR in RESPECT_FROZEN to flags before diff --git a/src/Higher/assignmentConditionFragment.cc b/src/Higher/assignmentConditionFragment.cc index 7b5e2363..b3c222df 100644 --- a/src/Higher/assignmentConditionFragment.cc +++ b/src/Higher/assignmentConditionFragment.cc @@ -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-2024 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 @@ -144,7 +144,7 @@ AssignmentConditionFragment::solve(bool findFirst, } else { - AssignmentConditionState* cs = safeCast(AssignmentConditionState*, state.top()); + AssignmentConditionState* cs = safeCastNonNull(state.top()); if (cs->solve(false, solution)) return true; delete cs; diff --git a/src/Higher/modelCheckerSymbol.cc b/src/Higher/modelCheckerSymbol.cc index aad15c1e..3e7deb74 100644 --- a/src/Higher/modelCheckerSymbol.cc +++ b/src/Higher/modelCheckerSymbol.cc @@ -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-2024 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 @@ -110,7 +110,7 @@ ModelCheckerSymbol::attachTerm(const char* purpose, Term* term) void ModelCheckerSymbol::copyAttachments(Symbol* original, SymbolMap* map) { - ModelCheckerSymbol* orig = safeCast(ModelCheckerSymbol*, original); + ModelCheckerSymbol* orig = safeCastNonNull(original); COPY_SYMBOL(orig, satisfiesSymbol, map, Symbol*); COPY_SYMBOL(orig, qidSymbol, map, QuotedIdentifierSymbol*); COPY_SYMBOL(orig, unlabeledSymbol, map, Symbol*); @@ -241,7 +241,7 @@ ModelCheckerSymbol::eqRewrite(DagNode* subject, RewritingContext& context) // // Compute normalization of negated formula. // - FreeDagNode* d = safeCast(FreeDagNode*, subject); + FreeDagNode* d = safeCastNonNull(subject); RewritingContext* newContext = context.makeSubcontext(negate(d->getArgument(1))); newContext->reduce(); #ifdef TDEBUG diff --git a/src/Higher/narrowingFolder.cc b/src/Higher/narrowingFolder.cc index 328db1f7..7735f748 100644 --- a/src/Higher/narrowingFolder.cc +++ b/src/Higher/narrowingFolder.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 2017-2020 SRI International, Menlo Park, CA 94025, USA. + Copyright 2017-2024 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 @@ -100,7 +100,7 @@ NarrowingFolder::insertState(int index, DagNode* state, int parentIndex) // for (auto& i : mostGeneralSoFar) { - if (i.second->subsumes(state)) + if (!i.second->subsumed && i.second->subsumes(state)) { DebugAdvisory("new state " << index << " subsumed by " << i.first); Verbose("New state " << state << " subsumed by " << i.second->state); @@ -108,16 +108,21 @@ NarrowingFolder::insertState(int index, DagNode* state, int parentIndex) } } } + // + // Create a new retained state. + // DebugAdvisory("new state " << index << " added"); - RetainedState* newState = new RetainedState(state, parentIndex, fold); + int rootIndex = index; int depth = 0; if (parentIndex != NONE) { RetainedStateMap::const_iterator j = mostGeneralSoFar.find(parentIndex); Assert(j != mostGeneralSoFar.end(), "couldn't find state with index " << parentIndex); + rootIndex = j->second->rootIndex; depth = j->second->depth + 1; } - newState->depth = depth; + RetainedState* newState = new RetainedState(state, parentIndex, rootIndex, depth, fold); + if (fold) { // @@ -140,11 +145,10 @@ NarrowingFolder::insertState(int index, DagNode* state, int parentIndex) { RetainedStateMap::iterator next = i; ++next; - if (ancestors.find(i->first) == ancestors.end()) // can't mess with ancestors of new state + if (!i->second->subsumed && ancestors.find(i->first) == ancestors.end()) // can't mess with ancestors of new state { RetainedState* potentialVictim = i->second; - if (existingStatesSubsumed.find(potentialVictim->parentIndex) != - existingStatesSubsumed.end()) + if (existingStatesSubsumed.find(potentialVictim->parentIndex) != existingStatesSubsumed.end()) { // // Our parent was subsumed so we are also subsumed. @@ -154,8 +158,13 @@ NarrowingFolder::insertState(int index, DagNode* state, int parentIndex) " evicted descendent of an older state " << i->second->state << " by subsuming an ancestor."); existingStatesSubsumed.insert(i->first); - delete potentialVictim; - mostGeneralSoFar.erase(i); + if (potentialVictim->locked) + potentialVictim->subsumed = true; // can't delete this state because we might need it for a path + else + { + delete potentialVictim; + mostGeneralSoFar.erase(i); + } } else if (newState->subsumes(potentialVictim->state)) { @@ -163,11 +172,15 @@ NarrowingFolder::insertState(int index, DagNode* state, int parentIndex) // Direct subsumption by new state. // DebugAdvisory("new state evicted an older state " << i->first); - Verbose("New state " << state << " subsumed older state " << - i->second->state); + Verbose("New state " << state << " subsumed older state " << i->second->state); existingStatesSubsumed.insert(i->first); - delete potentialVictim; - mostGeneralSoFar.erase(i); + if (potentialVictim->locked) + potentialVictim->subsumed = true; // can't delete this state because we might need it for a path + else + { + delete potentialVictim; + mostGeneralSoFar.erase(i); + } } } i = next; @@ -177,7 +190,7 @@ NarrowingFolder::insertState(int index, DagNode* state, int parentIndex) { // // Since we're not folding, if we are keeping history we - // need to keep track of number of descendant to know when + // need to keep track of number of descendants to know when // a state will never appear in the history of a returned // state. // @@ -222,12 +235,19 @@ NarrowingFolder::getNextSurvivingState(DagNode*& nextState, int& nextStateVariableFamily, int& nextStateDepth) { + // + // We're done with the current state, so we might want to delete it. + // cleanGraph(); - RetainedStateMap::const_iterator nextStateIterator = - mostGeneralSoFar.upper_bound(currentStateIndex); + // + // Find the next state if there is one. + // + RetainedStateMap::const_iterator nextStateIterator = mostGeneralSoFar.upper_bound(currentStateIndex); if (nextStateIterator == mostGeneralSoFar.end()) return NONE; - + Assert(!nextStateIterator->second->locked, "unvisited state should not be locked"); + Assert(!nextStateIterator->second->subsumed, "unvisited state that is subsumed should have been deleted"); + currentStateIndex = nextStateIterator->first; nextState = nextStateIterator->second->state; nextStateAccumulatedSubstitution = nextStateIterator->second->accumulatedSubstitution; @@ -252,9 +272,10 @@ NarrowingFolder::cleanGraph() if (!keepHistory) { // - // Since we are not keeping history, we should not need the - // current state again since we are moving on to the next state. + // Since we are not keeping history and not folding we have no further need of a fully + // explored state. // + Assert(!stateIterator->second->locked, "shouldn't have locked states if not keeping history"); delete stateIterator->second; mostGeneralSoFar.erase(stateIterator); return; @@ -262,11 +283,13 @@ NarrowingFolder::cleanGraph() // // We are keeping history and so we need to determine whether the // current state and its ancestors sill appear on an active path. + // We do this by walking up to the root, until we find a state with existing descendents + // or which has been locked. // - while (stateIterator->second->nrDescendants == 0) + while (!stateIterator->second->locked && stateIterator->second->nrDescendants == 0) { // - // No desendant left in graph so we will never + // No descendent left in graph so we will never // be asked for this state on a path and can delete it. // int parentIndex = stateIterator->second->parentIndex; @@ -283,9 +306,30 @@ NarrowingFolder::cleanGraph() } } -NarrowingFolder::RetainedState::RetainedState(DagNode* state, int parentIndex, bool fold) +void +NarrowingFolder::lockPathToCurrentState() +{ + Assert(keepHistory, "can't lock path if not keeping history"); + // + // We lock all the states on the current path back to the root state, so that they are never deleted and + // are thus available for showing the complete path to this state at any point before our object is deleted. + // + RetainedStateMap::iterator stateIterator = mostGeneralSoFar.find(currentStateIndex); + while(!stateIterator->second->locked) + { + stateIterator->second->locked = true; + int parentIndex = stateIterator->second->parentIndex; + if (parentIndex == NONE) + break; + stateIterator = mostGeneralSoFar.find(parentIndex); + } +} + +NarrowingFolder::RetainedState::RetainedState(DagNode* state, int parentIndex, int rootIndex, int depth, bool fold) : state(state), - parentIndex(parentIndex) + parentIndex(parentIndex), + rootIndex(rootIndex), + depth(depth) { if (fold) { @@ -294,7 +338,7 @@ NarrowingFolder::RetainedState::RetainedState(DagNode* state, int parentIndex, b // Term* t = state->symbol()->termify(state); // - // Even thoug t should be in normal form we need to set hash values. + // Even though it should be in normal form we need to set hash values. // t = t->normalize(true); VariableInfo variableInfo; @@ -319,22 +363,6 @@ NarrowingFolder::RetainedState::RetainedState(DagNode* state, int parentIndex, b matchingAutomaton = 0; nrMatchingVariables = 0; } - // - // These will be filled out later. - // - variableFamily = NONE; - accumulatedSubstitution = 0; - // - // These will be filled out later if we're keeping the history. - // - rule = 0; - unifier = 0; - narrowingContext = 0; - narrowingPosition = 0; - // - // This may be updated if we are keeping the history and we aren't folding. - // - nrDescendants = 0; } NarrowingFolder::RetainedState::~RetainedState() diff --git a/src/Higher/narrowingFolder.hh b/src/Higher/narrowingFolder.hh index 6a1f3076..7883c78e 100644 --- a/src/Higher/narrowingFolder.hh +++ b/src/Higher/narrowingFolder.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 2017 SRI International, Menlo Park, CA 94025, USA. + Copyright 2017-2024 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 @@ -27,7 +27,7 @@ // // The caller gives each state an index, and for each new state, holds the // index of the parent state or NONE if it is the initial state of the narrowing -// search. A states index is required to be larger than that of its parent. +// search. A state's index is required to be larger than that of its parent. // When an existing state is ejected by the arrival of a new state that is more // general, all of its descendents are likewise ejected, just as if the search // that has already taken place had been pruned. @@ -62,6 +62,7 @@ public: DagNode*& state, int& variableFamily, Substitution*& accumulatedSubstitution) const; + int getRootIndex(int index) const; int getDepth(int index) const; void getHistory(int index, DagNode*& root, @@ -80,38 +81,53 @@ public: Substitution*& nextStateAccumulatedSubstitution, int& nextStateVariableFamily, int& nextStateDepth); + // + // Ensures all the states from the interesting state back to the root are never deleted. + // + void lockPathToCurrentState(); + // + // Check if a state we previously entered still exists. + // + bool exists(int index); private: struct RetainedState { - RetainedState(DagNode* state, int parentIndex, bool fold); + RetainedState(DagNode* state, int parentIndex, int rootIndex, int depth, bool fold); ~RetainedState(); bool subsumes(DagNode* state) const; DagNode* const state; - Substitution* accumulatedSubstitution; - const int parentIndex; - int variableFamily; - int depth; + const int parentIndex; // index of parent state + const int rootIndex; // index of root state + const int depth; // number of narrowing steps from root + int variableFamily = NONE; + Substitution* accumulatedSubstitution = nullptr; // // Only used for folding. // Term* stateTerm; LhsAutomaton* matchingAutomaton; - int nrMatchingVariables; // number of variables needed for matching; includes - // any abstraction variables + int nrMatchingVariables; // number of variables needed for matching; includes any abstraction variables // // Only used for history. // - Rule* rule; // rule used for narrowing step that created this state - DagNode* narrowingContext; - DagNode* narrowingPosition; // pointer into old state - Substitution* unifier; // variant unifier between parent state and rule lhs + Rule* rule = nullptr; // rule used for narrowing step that created this state + DagNode* narrowingContext = nullptr; + DagNode* narrowingPosition = nullptr; // pointer into old state + Substitution* unifier = nullptr; // variant unifier between parent state and rule lhs NarrowingVariableInfo variableInfo; // variable info for the parent state part of the unifier // // Only used for history if we are not folding. // - int nrDescendants; + int nrDescendants = 0; + // + // The state is locked against deletion by any of the clean up mechanisms, but if it is subsumed + // we don't want to consider it for subsuming a new state or being subsumed in the future. + // An unexplored state can never be locked, and thus is deleted if subsumed. + // + bool locked = false; + bool subsumed = false; }; typedef map RetainedStateMap; @@ -122,8 +138,8 @@ private: const bool fold; // we do folding to prune less general states const bool keepHistory; // we keep the history of how we arrived at each state - RetainedStateMap mostGeneralSoFar; int currentStateIndex; + RetainedStateMap mostGeneralSoFar; }; inline void @@ -164,6 +180,14 @@ NarrowingFolder::getDepth(int index) const return i->second->depth; } +inline int +NarrowingFolder::getRootIndex(int index) const +{ + RetainedStateMap::const_iterator i = mostGeneralSoFar.find(index); + Assert(i != mostGeneralSoFar.end(), "couldn't find state with index " << index); + return i->second->rootIndex; +} + inline void NarrowingFolder::getHistory(int index, DagNode*& root, @@ -190,4 +214,10 @@ NarrowingFolder::getHistory(int index, parentIndex = i->second->parentIndex; } +inline bool +NarrowingFolder::exists(int index) +{ + return mostGeneralSoFar.find(index)!= mostGeneralSoFar.end(); +} + #endif diff --git a/src/Higher/narrowingSequenceSearch3.cc b/src/Higher/narrowingSequenceSearch3.cc index ac10c125..c04f304c 100644 --- a/src/Higher/narrowingSequenceSearch3.cc +++ b/src/Higher/narrowingSequenceSearch3.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2020 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 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 @@ -51,7 +51,68 @@ #include "filteredVariantUnifierSearch.hh" #include "narrowingSequenceSearch3.hh" +bool +NarrowingSequenceSearch3::handleInitialState(DagNode* dagToNarrow, NarrowingVariableInfo& varInfo) +{ + // + // Index the variables in the state dag. + // + dagToNarrow->indexVariables(varInfo, 0); + // + // Build a renaming from these variable to fresh variables. + // + int nrVariables = varInfo.getNrVariables(); + Substitution* renamingSubstitution = new Substitution(nrVariables); + for (int i = 0; i < nrVariables; ++i) + { + VariableDagNode* v = varInfo.index2Variable(i); + if (freshVariableGenerator->variableNameConflict(v->id(), NONE)) + { + IssueWarning("unsafe variable name " << QUOTE((DagNode*) v) << " in initial state " << + QUOTE(dagToNarrow) << "."); + return false; + } + int name = freshVariableGenerator->getFreshVariableName(i, 0); // 0 indicates a #variable + VariableDagNode* nv = new VariableDagNode(v->symbol(), name, i); + renamingSubstitution->bind(i, nv); + } + // + // Protect the variable dagnodes we just made from the garbage collector in case they + // disappear from the reduced term. + // + protectedSubstitution = renamingSubstitution; + // + // Rename all the variables in the state + // + if (DagNode* renamedDagToNarrow = dagToNarrow->instantiate(*renamingSubstitution, false)) + dagToNarrow = renamedDagToNarrow; + // + // Reduce the state with equations. + // + RewritingContext* reduceContext = initial->makeSubcontext(dagToNarrow); + reduceContext->reduce(); + initial->transferCountFrom(*reduceContext); + protectedSubstitution = nullptr; + // + // Add the renamed and reduced state to the state collection, along with the + // renaming as its accumulated substitution. + // + int newStateIndex = ++counter; + bool survived = stateCollection.insertState(newStateIndex, reduceContext->root(), -1); + delete reduceContext; + if (survived) + stateCollection.addAccumulatedSubstitution(newStateIndex, 0, renamingSubstitution); + else + delete renamingSubstitution; + // + // If we cared about the renaming substitution, it is now protected by stateCollection. + // + protectedSubstitution = nullptr; + return true; +} + NarrowingSequenceSearch3::NarrowingSequenceSearch3(RewritingContext* initial, + const Vector& startStates, SearchType searchType, DagNode* goal, int maxDepth, @@ -59,37 +120,68 @@ NarrowingSequenceSearch3::NarrowingSequenceSearch3(RewritingContext* initial, int variantFlags) : initial(initial), goal(goal), + nrInitialStatesToTry((searchType == ANY_STEPS) ? (startStates.size() ? startStates.size() : 1) : 0), maxDepth((searchType == ONE_STEP) ? 1 : maxDepth), - needToTryInitialState(searchType == ANY_STEPS), normalFormNeeded(searchType == NORMAL_FORM), + termDisjunction(startStates.size() > 1), freshVariableGenerator(freshVariableGenerator), variantFlags(variantFlags), - stateCollection(variantFlags & FOLD, variantFlags & KEEP_HISTORY) + stateCollection(variantFlags & FOLD, variantFlags & (KEEP_HISTORY | KEEP_PATHS)) { incompleteFlag = false; - unificationProblem = 0; - stateBeingExpanded = 0; + problemOkay = false; + unificationProblem = nullptr; + stateBeingExpanded = nullptr; stateBeingExpandedIndex = NONE; stateBeingExpandedDepth = 0; expansionSuccessful = false; nextInterestingState = NONE; - counter = 0; + counter = -1; nrStatesExpanded = 0; + protectedSubstitution = nullptr; // - // Index variables occurring in the initial term and create a fresh - // #variable for each original variable and an accumulated substitution - // that maps fresh original variables to fresh variables. + // Index variables occurring in the startStates. // - DagNode* dagToNarrow = initial->root(); - dagToNarrow->indexVariables(initialVariableInfo, 0); - int nrInitialVariables = initialVariableInfo.getNrVariables(); - Substitution* accumulatedSubstitution = new Substitution(nrInitialVariables); - for (int i = 0; i < nrInitialVariables; ++i) + map seenVariables; + if (termDisjunction) { - Symbol* baseSymbol = initialVariableInfo.index2Variable(i)->symbol(); - int name = freshVariableGenerator->getFreshVariableName(i, 0); - VariableDagNode* v = new VariableDagNode(baseSymbol, name, i); - accumulatedSubstitution->bind(i, v); + Index nrInitialStates = startStates.size(); + initialStates.resize(nrInitialStates); + // + // First protect all startStates from garbage collection putting them in initialStates. + // + for (Index i = 0; i < nrInitialStates; ++i) + initialStates[i].state = startStates[i]; + // + // Then do the processing on each initial state which may call reduce() and the garbage collector. + // + for (Index i = 0; i < nrInitialStates; ++i) + { + InitialState& is = initialStates[i]; + if (!handleInitialState(is.state, is.varInfo)) + return; + // + // Check for illegal variable sharing. + // + int nrVariables = is.varInfo.getNrVariables(); + for (int j = 0; j < nrVariables; ++j) + { + DagNode* v = is.varInfo.index2Variable(j); + auto r = seenVariables.insert({v, i}); + if (!r.second) + { + IssueWarning("variable " << QUOTE(v) << " appears in both initial state " << + QUOTE(initialStates[r.first->second].state) << " and initial state " << + QUOTE(initialStates[i].state) << "."); + return; + } + } + } + } + else + { + if (!handleInitialState(initial->root(), initialVariableInfo)) + return; } // // HACK: this is so we can use instantiate which expects ground terms @@ -97,28 +189,34 @@ NarrowingSequenceSearch3::NarrowingSequenceSearch3(RewritingContext* initial, // //goal->computeTrueSort(*initial); // - // We also want to index goal variables so we can apply the accumulated + // We also want to index goal variables so we can apply the renaming // substitution, but we do not want to carry around the extra variables // since they cannot play a role in narrowing, as they don't occur in // the initial term. // goal->indexVariables(initialVariableInfo, 0); - // - // Reduction could lose variables. But initial variables will be protected - // from garbage collection by initial RewritingContext, and goal only - // variables will be protected by goal. - // - if (DagNode* renamedDagToNarrow = dagToNarrow->instantiate(*accumulatedSubstitution, false)) - dagToNarrow = renamedDagToNarrow; - RewritingContext* reduceContext = initial->makeSubcontext(dagToNarrow); - reduceContext->reduce(); - initial->transferCountFrom(*reduceContext); - // - // Create initial state in state collection. - // - (void) stateCollection.insertState(0, reduceContext->root(), -1); - stateCollection.addAccumulatedSubstitution(0, 0, accumulatedSubstitution); - delete reduceContext; + int nrVariables = initialVariableInfo.getNrVariables(); + for (int i = 0; i < nrVariables; ++i) + { + VariableDagNode* v = initialVariableInfo.index2Variable(i); + DagNode* d = v; + if (freshVariableGenerator->variableNameConflict(v->id(), NONE)) + { + IssueWarning("unsafe variable name " << QUOTE(d) << " in goal " << goal << "."); + return; + } + if (termDisjunction) + { + auto p = seenVariables.find(d); + if (p != seenVariables.end()) + { + IssueWarning("sharing a variable " << QUOTE(d) << " between initial state " << + QUOTE(initialStates[p->second].state) << " and goal " << + QUOTE(goal) << " is not allowed when narrowing a disjunction of initial states."); + return; + } + } + } // // Need to make internal symbol for variant unification with goal. // @@ -130,6 +228,8 @@ NarrowingSequenceSearch3::NarrowingSequenceSearch3(RewritingContext* initial, domain[0] = range; domain[1] = range; unificationPairSymbol = module->createInternalTupleSymbol(domain, range); + + problemOkay = true; } NarrowingSequenceSearch3::~NarrowingSequenceSearch3() @@ -140,12 +240,29 @@ NarrowingSequenceSearch3::~NarrowingSequenceSearch3() delete initial; } +void +NarrowingSequenceSearch3::markReachableNodes() +{ + // + // Protect start states in termDisjuction mode + // + //goal->mark; // maybe use this rather than DagRoot + for (InitialState& i : initialStates) + i.state->mark(); + if (protectedSubstitution) + { + int nrBindings = protectedSubstitution->nrFragileBindings(); + for (int i = 0; i < nrBindings; ++i) + protectedSubstitution->value(i)->mark(); + } +} + bool NarrowingSequenceSearch3::findNextUnifier() { for (;;) { - if (unificationProblem != 0) + if (unificationProblem != nullptr) { bool moreUnifiers = unificationProblem->findNextUnifier(); initial->transferCountFrom(*(unificationProblem->getContext())); @@ -153,14 +270,25 @@ NarrowingSequenceSearch3::findNextUnifier() incompleteFlag = true; if (moreUnifiers) { - currentUnifier = &(unificationProblem->getCurrentUnifier(nrFreeVariablesInUnifier, - variableFamilyInUnifier)); + currentUnifier = &(unificationProblem->getCurrentUnifier(nrFreeVariablesInUnifier, variableFamilyInUnifier)); + if (variantFlags & KEEP_PATHS) + { + // + // We keep the path to a state that unifies with the goal since the user + // can ask for such a path at any time. Otherwise a state will be deleted if it + // becomes subsumed (if we're folding) or after all of its next states have been + // generated. + // + stateCollection.lockPathToCurrentState(); + } return true; } delete unificationProblem; - unificationProblem = 0; + unificationProblem = nullptr; } - + // + // Get the next state and see if we can unify it with our goal. + // nextInterestingState = findNextInterestingState(); if (nextInterestingState == NONE) break; @@ -168,34 +296,39 @@ NarrowingSequenceSearch3::findNextUnifier() int variableFamily; Substitution* accumulatedSubstitution; stateCollection.getState(nextInterestingState, stateDag, variableFamily, accumulatedSubstitution); - // - // Because the goal dag might include some of the variables from the initial state - // we need to instantiate it. - // - DagNode* instantiatedGoal; - int nrInitialVariables = accumulatedSubstitution->nrFragileBindings(); - int totalNrVariables = initialVariableInfo.getNrVariables(); - if (totalNrVariables > nrInitialVariables) + + DagNode* goalDag = goal.getNode(); // no change under instantiation + if (!termDisjunction) { // - // Need to make a bigger substitution with extra variables zero'd out. + // Because the goal dag might include some of the variables from the initial state + // we need to instantiate it. // - Substitution bigger(totalNrVariables); - for (int i = 0; i < nrInitialVariables; ++i) - bigger.bind(i, accumulatedSubstitution->value(i)); - for (int i = nrInitialVariables; i < totalNrVariables; ++i) - bigger.bind(i, 0); - instantiatedGoal = goal.getNode()->instantiate(bigger, false); - } - else - instantiatedGoal = goal.getNode()->instantiate(*accumulatedSubstitution, false); - if (instantiatedGoal == 0) - instantiatedGoal = goal.getNode(); // no change under instantiation + DagNode* instantiatedGoal; + int nrInitialVariables = accumulatedSubstitution->nrFragileBindings(); + int totalNrVariables = initialVariableInfo.getNrVariables(); + if (totalNrVariables > nrInitialVariables) + { + // + // Need to make a bigger substitution with extra variables zero'd out. + // + Substitution bigger(totalNrVariables); + for (int i = 0; i < nrInitialVariables; ++i) + bigger.bind(i, accumulatedSubstitution->value(i)); + for (int i = nrInitialVariables; i < totalNrVariables; ++i) + bigger.bind(i, nullptr); + instantiatedGoal = goalDag->instantiate(bigger, false); + } + else + instantiatedGoal = goalDag->instantiate(*accumulatedSubstitution, false); + if (instantiatedGoal != nullptr) + goalDag = instantiatedGoal; + } // // Need to variant unify the narrrowed dag in this state with the goal dag. // Vector args(2); - args[0] = instantiatedGoal; + args[0] = goalDag; args[1] = stateDag; DagNode* pairDag = unificationPairSymbol->makeDagNode(args); RewritingContext* pairContext = initial->makeSubcontext(pairDag); @@ -219,16 +352,22 @@ NarrowingSequenceSearch3::findNextUnifier() int NarrowingSequenceSearch3::findNextInterestingState() { - if (needToTryInitialState) + // + // If we are a =>* search we need tor try surviving initial states before we start narrowing. + // + while (nrInitialStatesToTry > 0) { + --nrInitialStatesToTry; + int stateToTry = counter - nrInitialStatesToTry; // want to try 0,..., counter // - // Special case: return the initial state; only happens for =>* + // We want to know if stateToTry has been subsumed; but because we have not started narrowing, + // it can't be locked, and thus if it has been subsumed it will have been deleted. // - needToTryInitialState = false; // don't do this again - return 0; + if (stateCollection.exists(stateToTry)) + return stateToTry; } - if (stateBeingExpanded != 0) + if (stateBeingExpanded != nullptr) { tryToExpand: // @@ -243,7 +382,7 @@ NarrowingSequenceSearch3::findNextInterestingState() if (!success) { delete stateBeingExpanded; - stateBeingExpanded = 0; + stateBeingExpanded = nullptr; if (normalFormNeeded && !expansionSuccessful) { // @@ -261,7 +400,7 @@ NarrowingSequenceSearch3::findNextInterestingState() // in normal form. // delete stateBeingExpanded; - stateBeingExpanded = 0; + stateBeingExpanded = nullptr; break; } expansionSuccessful = true; // stateBeingExpanded can't be a normal form @@ -293,7 +432,7 @@ NarrowingSequenceSearch3::findNextInterestingState() RewritingContext* reduceContext = initial->makeSubcontext(newState); replacementContextProtector.setNode(replacementContext); // protect replacementContext from GC during reduce() reduceContext->reduce(); // can call GC - replacementContextProtector.setNode(0); // withdraw protection + replacementContextProtector.setNode(nullptr); // withdraw protection initial->transferCountFrom(*reduceContext); // // Does new state survive folding? diff --git a/src/Higher/narrowingSequenceSearch3.hh b/src/Higher/narrowingSequenceSearch3.hh index 6c090743..d08e3ee6 100644 --- a/src/Higher/narrowingSequenceSearch3.hh +++ b/src/Higher/narrowingSequenceSearch3.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 2017-2020 SRI International, Menlo Park, CA 94025, USA. + Copyright 2017-2024 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 @@ -29,8 +29,9 @@ #include "narrowingFolder.hh" #include "narrowingSearchState3.hh" #include "dagRoot.hh" +#include "rewritingContext.hh" -class NarrowingSequenceSearch3 : public SequenceSearch +class NarrowingSequenceSearch3 : public SequenceSearch, private SimpleRootContainer { NO_COPYING(NarrowingSequenceSearch3); @@ -40,17 +41,39 @@ public: // enum Flags { - FOLD = 0x2000, - KEEP_HISTORY = 0x4000, + // + // Fold using matching. + // + FOLD = 0x10000, + // + // Fold using variant subsumption (to be implemented). + // + VFOLD = 0x20000, + // + // Keep the history of the current path. States can still be deleted once they are no longer on the + // current path, have no live descendents, and aren't needed for folding. This is intended for the + // metalevel where one cannot revisit old results without redoing the whole computation. + // + KEEP_HISTORY = 0x40000, + // + // Keep the history of the path to every state (subsumed or otherwise) that provided a unifier with goal. + // Potentially very expensive in terms of memory. This is intended for the object level where the + // user can ask for the path to any state that yielded a unifier (to be implemented). + // + KEEP_PATHS = 0x80000, + // + // This flag is just maintained as state information for users + // + INVARIANT = 0x100000, }; - // - // We take responsibility for protecting goal and deleting initial and freshVariableGenerator. + // We take responsibility for protecting startStates and goal and deleting initial and freshVariableGenerator. // NarrowingSequenceSearch3(RewritingContext* initial, + const Vector& startStates, SearchType searchType, DagNode* goal, - int maxDepth, + int maxDepth, // NONE = unbounded FreshVariableGenerator* freshVariableGenerator, int variantFlags); ~NarrowingSequenceSearch3(); @@ -64,7 +87,10 @@ public: // // Get information about current state. // - void getStateInfo(DagNode*& stateDag, int& variableFamily, Substitution*& accumulatedSubstitution) const; + void getStateInfo(DagNode*& stateDag, + int& variableFamily, + DagNode*& initialStateDag, + Substitution*& accumulatedSubstitution) const; void getExtraStateInfo(int& index, int& depth) const; // // Get information about some state in the history. @@ -88,8 +114,22 @@ public: RewritingContext* getContext() const; bool isIncomplete() const; + int getNrInitialStates() const; + int getVariantFlags() const; + bool problemOK() const; private: + // + // If we have multiple state states, we need one of these structs for each such state. + // + struct InitialState + { + DagNode* state; + NarrowingVariableInfo varInfo; + }; + + bool handleInitialState(DagNode* dagToNarrow, NarrowingVariableInfo& varInfo); + void markReachableNodes(); int findNextInterestingState(); bool findNextNormalForm(); // @@ -97,11 +137,13 @@ private: // RewritingContext* initial; DagRoot goal; + int nrInitialStatesToTry; const int maxDepth; - bool needToTryInitialState; const bool normalFormNeeded; + const bool termDisjunction; FreshVariableGenerator* freshVariableGenerator; const int variantFlags; + Vector initialStates; NarrowingFolder stateCollection; // // Maps variables occurring in initial state which will be the @@ -109,6 +151,10 @@ private: // NarrowingVariableInfo initialVariableInfo; // + // Used to temporarily protect the range of a substitution from the garbage collector. + // + Substitution* protectedSubstitution; + // // Pairing symbol for variant unification of state vs pattern. // Symbol* unificationPairSymbol; @@ -132,8 +178,15 @@ private: int variableFamilyInUnifier; bool incompleteFlag; + bool problemOkay; }; +inline bool +NarrowingSequenceSearch3::problemOK() const +{ + return problemOkay; +} + inline const Vector* NarrowingSequenceSearch3::getUnifier() const { @@ -149,13 +202,18 @@ NarrowingSequenceSearch3::getUnifierVariableInfo() const inline const NarrowingVariableInfo& NarrowingSequenceSearch3::getInitialVariableInfo() const { - return initialVariableInfo; + return termDisjunction ? initialStates[stateCollection.getRootIndex(nextInterestingState)].varInfo : initialVariableInfo; } inline void -NarrowingSequenceSearch3::getStateInfo(DagNode*& stateDag, int& variableFamily, Substitution*& accumulatedSubstitution) const +NarrowingSequenceSearch3::getStateInfo(DagNode*& stateDag, + int& variableFamily, + DagNode*& initialStateDag, + Substitution*& accumulatedSubstitution) const { stateCollection.getState(nextInterestingState, stateDag, variableFamily, accumulatedSubstitution); + + initialStateDag = termDisjunction ? initialStates[stateCollection.getRootIndex(nextInterestingState)].state : initial->root(); } inline void @@ -210,4 +268,16 @@ NarrowingSequenceSearch3::isIncomplete() const return incompleteFlag; } +inline int +NarrowingSequenceSearch3::getNrInitialStates() const +{ + return termDisjunction ? initialStates.size() : 1; +} + +inline int +NarrowingSequenceSearch3::getVariantFlags() const +{ + return variantFlags; +} + #endif diff --git a/src/Higher/narrowingUnificationProblem.cc b/src/Higher/narrowingUnificationProblem.cc index dae0b8f5..b3ce999b 100755 --- a/src/Higher/narrowingUnificationProblem.cc +++ b/src/Higher/narrowingUnificationProblem.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2020 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 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 @@ -225,7 +225,7 @@ NarrowingUnificationProblem::variableIndexToSort(int index) // // Original PreEquation variable. // - return safeCast(VariableSymbol*, preEquation->index2Variable(index)->symbol())->getSort(); + return safeCastNonNull(preEquation->index2Variable(index)->symbol())->getSort(); } if (index < substitutionSize) { @@ -233,8 +233,7 @@ NarrowingUnificationProblem::variableIndexToSort(int index) // // Original dag variable. // - return safeCast(VariableSymbol*, - variableInfo.index2Variable(index - firstTargetSlot)->symbol())->getSort(); + return safeCastNonNull(variableInfo.index2Variable(index - firstTargetSlot)->symbol())->getSort(); } // // Fresh variable introduced by unification. diff --git a/src/Higher/rewriteConditionFragment.cc b/src/Higher/rewriteConditionFragment.cc index de10ccbd..839c6c92 100644 --- a/src/Higher/rewriteConditionFragment.cc +++ b/src/Higher/rewriteConditionFragment.cc @@ -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-2024 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 @@ -131,7 +131,7 @@ RewriteConditionFragment::solve(bool findFirst, } else { - RewriteConditionState* cs = safeCast(RewriteConditionState*, state.top()); + RewriteConditionState* cs = safeCastNonNull(state.top()); if (cs->solve(false, solution)) return true; delete cs; diff --git a/src/Higher/satSolverSymbol.cc b/src/Higher/satSolverSymbol.cc index 85d4bc35..8642e466 100644 --- a/src/Higher/satSolverSymbol.cc +++ b/src/Higher/satSolverSymbol.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 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 @@ -97,7 +97,7 @@ SatSolverSymbol::attachTerm(const char* purpose, Term* term) void SatSolverSymbol::copyAttachments(Symbol* original, SymbolMap* map) { - SatSolverSymbol* orig = safeCast(SatSolverSymbol*, original); + SatSolverSymbol* orig = safeCastNonNull(original); COPY_SYMBOL(orig, formulaListSymbol, map, Symbol*); COPY_SYMBOL(orig, nilFormulaListSymbol, map, Symbol*); COPY_SYMBOL(orig, modelSymbol, map, Symbol*); @@ -152,7 +152,7 @@ SatSolverSymbol::eqRewrite(DagNode* subject, RewritingContext& context) { Assert(this == subject->symbol(), "bad symbol"); - FreeDagNode* f = safeCast(FreeDagNode*, subject); + FreeDagNode* f = safeCastNonNull(subject); DagNode* formulaDag = f->getArgument(0); formulaDag->reduce(context); diff --git a/src/Higher/temporalSymbol.cc b/src/Higher/temporalSymbol.cc index 415c9935..9f459145 100644 --- a/src/Higher/temporalSymbol.cc +++ b/src/Higher/temporalSymbol.cc @@ -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-2024 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 @@ -88,7 +88,7 @@ TemporalSymbol::attachSymbol(const char* purpose, Symbol* symbol) void TemporalSymbol::copyAttachments(Symbol* original, SymbolMap* map) { - TemporalSymbol* orig = safeCast(TemporalSymbol*, original); + TemporalSymbol* orig = safeCastNonNull(original); COPY_SYMBOL(orig, trueSymbol, map, Symbol*); COPY_SYMBOL(orig, falseSymbol, map, Symbol*); COPY_SYMBOL(orig, notSymbol, map, Symbol*); diff --git a/src/Higher/unificationProblem.cc b/src/Higher/unificationProblem.cc index 0888db9e..231e959d 100755 --- a/src/Higher/unificationProblem.cc +++ b/src/Higher/unificationProblem.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 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 @@ -98,8 +98,7 @@ UnificationProblem::UnificationProblem(Vector& lhs, for (int i = 0; i < nrOriginalVariables; ++i) { Term* v = variableInfo.index2Variable(i); - if (freshVariableGenerator->variableNameConflict(safeCast(VariableTerm*, v)->id(), - incomingVariableFamily)) + if (freshVariableGenerator->variableNameConflict(safeCastNonNull(v)->id(), incomingVariableFamily)) { IssueWarning("unsafe variable name " << QUOTE(v) << " in unification problem."); return; @@ -284,7 +283,7 @@ UnificationProblem::bindFreeVariables() DebugInfo("newSortIndex = " << newSortIndex << " newSort = " << newSort); Symbol* baseVariableSymbol = freshVariableGenerator->getBaseVariableSymbol(newSort); - int variableName = safeCast(VariableDagNode*, variable)->id(); + int variableName = safeCastNonNull(variable)->id(); DagNode* newVariable = new VariableDagNode(baseVariableSymbol, variableName, fv); sortedSolution->bind(fv, newVariable); } @@ -330,7 +329,7 @@ UnificationProblem::findOrderSortedUnifiers() freeVariables.insert(i); realToBdd[i] = nextBddVariable; Sort* sort = (i < nrOriginalVariables) ? - safeCast(VariableSymbol*, variableInfo.index2Variable(i)->symbol())->getSort() : + safeCastNonNull(variableInfo.index2Variable(i)->symbol())->getSort() : unsortedSolution->getFreshVariableSort(i); nextBddVariable += sortBdds->getNrVariables(sort->component()->getIndexWithinModule()); //cout << "allocated bdds" << endl; @@ -367,7 +366,7 @@ UnificationProblem::findOrderSortedUnifiers() for (int i = 0; i < nrOriginalVariables; ++i) { DebugAdvisory("Considering variable " << variableInfo.index2Variable(i)); - Sort* sort = safeCast(VariableSymbol*, variableInfo.index2Variable(i)->symbol())->getSort(); + Sort* sort = safeCastNonNull(variableInfo.index2Variable(i)->symbol())->getSort(); Bdd leqRelation; DagNode* d = sortedSolution->value(i); if (d != 0) @@ -411,7 +410,7 @@ UnificationProblem::findOrderSortedUnifiers() for (int fv : freeVariables) { Sort* sort = (fv < nrOriginalVariables) ? - safeCast(VariableSymbol*, variableInfo.index2Variable(fv)->symbol())->getSort() : + safeCastNonNull(variableInfo.index2Variable(fv)->symbol())->getSort() : unsortedSolution->getFreshVariableSort(fv); int nrBddVariables = sortBdds->getNrVariables(sort->component()->getIndexWithinModule()); // diff --git a/src/Main/ChangeLog b/src/Main/ChangeLog index 2062da3c..a555775b 100755 --- a/src/Main/ChangeLog +++ b/src/Main/ChangeLog @@ -1,10 +1,26 @@ +2024-04-16 Steven Eker + + * prelude.maude: beginsWith hook to startsWith; added + character class tests to fmod STRING-OPS + +2024-04-15 Steven Eker + + * prelude.maude: added fmod STRING-OPS + +2024-04-12 Steven Eker + + * maude.sty: added \maudeDisjunction + use \backslash rather than \textbackslash in ASCII mode + +===================================Maude160=========================================== + 2024-03-11 Steven Eker * maude.sty: added \maudeShowSpace 2024-02-20 Steven Eker - * maude.sty: adjust the spacing around, and hieght of * in + * maude.sty: adjust the spacing around, and height of * in \maudeRenaming ===================================Maude157=========================================== diff --git a/src/Main/Makefile.am b/src/Main/Makefile.am index 52aa0ee7..47dced6e 100755 --- a/src/Main/Makefile.am +++ b/src/Main/Makefile.am @@ -29,6 +29,7 @@ maude_CPPFLAGS = \ -I$(top_srcdir)/src/3rdParty \ -I$(top_srcdir)/src/FullCompiler \ -I$(top_srcdir)/src/StrategyLanguage \ + -I$(top_srcdir)/src/Parser \ -I$(top_srcdir)/src/Mixfix maude_LDADD = \ diff --git a/src/Main/Makefile.in b/src/Main/Makefile.in index b180369c..873a2d7a 100644 --- a/src/Main/Makefile.in +++ b/src/Main/Makefile.in @@ -350,6 +350,7 @@ maude_CPPFLAGS = \ -I$(top_srcdir)/src/3rdParty \ -I$(top_srcdir)/src/FullCompiler \ -I$(top_srcdir)/src/StrategyLanguage \ + -I$(top_srcdir)/src/Parser \ -I$(top_srcdir)/src/Mixfix maude_LDADD = \ diff --git a/src/Main/maude.sty b/src/Main/maude.sty index 4b4343ce..17793dc4 100644 --- a/src/Main/maude.sty +++ b/src/Main/maude.sty @@ -21,7 +21,7 @@ % Version 3.4. % \NeedsTeXFormat{LaTeX2e} -\ProvidesPackage{maude}[2024/03/12 Package for Maude logs] +\ProvidesPackage{maude}[2024/04/12 Package for Maude logs] \RequirePackage{amssymb,extarrows,longtable,tabto,xcolor,verbatim,alltt,seqsplit} \RequirePackage[T1]{fontenc} % @@ -142,6 +142,7 @@ \newcommand{\maudeSummation}{\,+\,} % module summation \newcommand{\maudePartialFunction}{\rightsquigarrow} % for partial op decls \newcommand{\maudeConjunction}{\,\wedge\,} % for conjunctions in conditions +\newcommand{\maudeDisjunction}{\,\vee\,} % for disjunctions in search \newcommand{\maudeHasSort}{\,:\,} % for op, variable decls, mbs and sort test condition fragments \newcommand{\maudeVariableColon}{\textnormal{:}} % for forming var:sort names \newcommand{\maudeEquals}{\,=\,} % for eqs and equality condition fragments @@ -209,7 +210,8 @@ \renewcommand{\maudeFunction}{\maudeBigSpace\textnormal{-->}\maudeBigSpace} \renewcommand{\maudePartialFunction}{\textnormal{\maudeTilde >}\maudeBigSpace} \renewcommand{\maudeConstantDecl}{\maudeInterwordSpace :\maudeInterwordSpace\textnormal{-->}\maudeBigSpace} % needed to get the spacing right - \renewcommand{\maudeConjunction}{\maudeBigSpace/\textbackslash\maudeBigSpace} + \renewcommand{\maudeConjunction}{\maudeBigSpace/\backslash\maudeBigSpace} + \renewcommand{\maudeDisjunction}{\maudeBigSpace\backslash/\maudeBigSpace} \renewcommand{\maudeRewritesTo}{\maudeBigSpace\textnormal{=>}\maudeBigSpace} \renewcommand{\maudeMatch}{\,\textnormal{<=?}\,} \renewcommand{\maudeUnify}{\,\textnormal{=?}\,} diff --git a/src/Main/prelude.maude b/src/Main/prelude.maude index 15e9f8cc..17bde661 100644 --- a/src/Main/prelude.maude +++ b/src/Main/prelude.maude @@ -22,7 +22,7 @@ *** *** Maude interpreter standard prelude. -*** Version 3.4. +*** Version alpha160 *** *** Some of the overall structure is taken from the OBJ3 *** interpreter standard prelude. @@ -1569,6 +1569,91 @@ view Array{X :: TRIV, Y :: DEFAULT} from TRIV to ARRAY{X, Y} is sort Elt to Array{X,Y} . endv +fmod STRING-OPS is + protecting STRING . + op isControl : Char -> Bool + [special (id-hook StringOpSymbol (cntrl) + op-hook stringSymbol ( : ~> String) + term-hook trueTerm (true) + term-hook falseTerm (false))] . + op isPrintable : Char -> Bool + [special (id-hook StringOpSymbol (print) + op-hook stringSymbol ( : ~> String) + term-hook trueTerm (true) + term-hook falseTerm (false))] . + op isWhiteSpace : Char -> Bool + [special (id-hook StringOpSymbol (space) + op-hook stringSymbol ( : ~> String) + term-hook trueTerm (true) + term-hook falseTerm (false))] . + op isBlank : Char -> Bool + [special (id-hook StringOpSymbol (blank) + op-hook stringSymbol ( : ~> String) + term-hook trueTerm (true) + term-hook falseTerm (false))] . + op isGraphic : Char -> Bool + [special (id-hook StringOpSymbol (graph) + op-hook stringSymbol ( : ~> String) + term-hook trueTerm (true) + term-hook falseTerm (false))] . + op isPunctuation : Char -> Bool + [special (id-hook StringOpSymbol (punct) + op-hook stringSymbol ( : ~> String) + term-hook trueTerm (true) + term-hook falseTerm (false))] . + op isAlphanumeric : Char -> Bool + [special (id-hook StringOpSymbol (alnum) + op-hook stringSymbol ( : ~> String) + term-hook trueTerm (true) + term-hook falseTerm (false))] . + op isAlphabetic : Char -> Bool + [special (id-hook StringOpSymbol (alpha) + op-hook stringSymbol ( : ~> String) + term-hook trueTerm (true) + term-hook falseTerm (false))] . + op isUppercase : Char -> Bool + [special (id-hook StringOpSymbol (isupper) + op-hook stringSymbol ( : ~> String) + term-hook trueTerm (true) + term-hook falseTerm (false))] . + op isLowercase : Char -> Bool + [special (id-hook StringOpSymbol (islower) + op-hook stringSymbol ( : ~> String) + term-hook trueTerm (true) + term-hook falseTerm (false))] . + op isDigit : Char -> Bool + [special (id-hook StringOpSymbol (digit) + op-hook stringSymbol ( : ~> String) + term-hook trueTerm (true) + term-hook falseTerm (false))] . + op isHexadecimalDigit : Char -> Bool + [special (id-hook StringOpSymbol (xdigit) + op-hook stringSymbol ( : ~> String) + term-hook trueTerm (true) + term-hook falseTerm (false))] . + + op startsWith : String String -> Bool + [special (id-hook StringOpSymbol (startsWith) + op-hook stringSymbol ( : ~> String) + term-hook trueTerm (true) + term-hook falseTerm (false))] . + op endsWith : String String -> Bool + [special (id-hook StringOpSymbol (endsWith) + op-hook stringSymbol ( : ~> String) + term-hook trueTerm (true) + term-hook falseTerm (false))] . + + op trimStart : String -> String + [special (id-hook StringOpSymbol (ltrim) + op-hook stringSymbol ( : ~> String))] . + op trimEnd : String -> String + [special (id-hook StringOpSymbol (rtrim) + op-hook stringSymbol ( : ~> String))] . + op trim : String -> String + [special (id-hook StringOpSymbol (trim) + op-hook stringSymbol ( : ~> String))] . +endfm + *** *** Container instantiations on builtin data types needed by the metalevel. *** diff --git a/src/Meta/ChangeLog b/src/Meta/ChangeLog index b900e42e..3b86ecd8 100644 --- a/src/Meta/ChangeLog +++ b/src/Meta/ChangeLog @@ -1,3 +1,31 @@ +2024-05-02 Steven Eker + + * miNarrowSearch.cc (InterpreterManagerSymbol::makeNarrowingSequenceSearch3): + removed hack, now that we don't need non-empty startStates; check problemOK() + + * metaNewNarrow2.cc (MetaLevelOpSymbol::makeNarrowingSequenceSearch3): + removed hack, now that we don't need non-empty startStates; check problemOK() + +2024-04-24 Steven Eker + + * metaNewNarrow2.cc (MetaLevelOpSymbol::metaNarrowingSearch): pass + dummy argument to getStateInfo() + + * miNarrowSearch.cc (InterpreterManagerSymbol::getNarrowingSearchResult): + pass dummy argument to getStateInfo() + +2024-04-22 Steven Eker + + * miNarrowSearch.cc + (InterpreterManagerSymbol::makeNarrowingSequenceSearch3): pass + startStates to arrowingSequenceSearch3() + + * metaNewNarrow2.cc + (MetaLevelOpSymbol::makeNarrowingSequenceSearch3): pass + startStates to arrowingSequenceSearch3() + +===================================Maude160=========================================== + 2024-03-06 Steven Eker * metaUp.cc (MetaLevel::upQid): got rid of const_cast<> diff --git a/src/Meta/metaNewNarrow2.cc b/src/Meta/metaNewNarrow2.cc index 05ececf1..47e1ad03 100644 --- a/src/Meta/metaNewNarrow2.cc +++ b/src/Meta/metaNewNarrow2.cc @@ -50,12 +50,18 @@ MetaLevelOpSymbol::makeNarrowingSequenceSearch3(MetaModule* m, if (fold) variantFlags |= NarrowingSequenceSearch3::FOLD; - return new NarrowingSequenceSearch3(subjectContext, - searchType, - goal, - maxDepth, - new FreshVariableSource(m, 0), - variantFlags); + Vector startStates; + NarrowingSequenceSearch3* nss = new NarrowingSequenceSearch3(subjectContext, + startStates, + searchType, + goal, + maxDepth, + new FreshVariableSource(m, 0), + variantFlags); + if (nss->problemOK()) + return nss; + else + delete nss; } } return 0; @@ -123,8 +129,9 @@ MetaLevelOpSymbol::metaNarrowingSearch(FreeDagNode* subject, RewritingContext& c DagNode* stateDag; int stateVariableFamily; + DagNode* dummy; Substitution* accumulatedSubstitution; - state->getStateInfo(stateDag, stateVariableFamily, accumulatedSubstitution); + state->getStateInfo(stateDag, stateVariableFamily, dummy, accumulatedSubstitution); result = metaLevel->upNarrowingSearchResult(stateDag, *accumulatedSubstitution, diff --git a/src/Meta/miNarrowSearch.cc b/src/Meta/miNarrowSearch.cc index f8555491..0760d6ac 100644 --- a/src/Meta/miNarrowSearch.cc +++ b/src/Meta/miNarrowSearch.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 2020-2021 SRI International, Menlo Park, CA 94025, USA. + Copyright 2020-2024 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 @@ -50,12 +50,18 @@ InterpreterManagerSymbol::makeNarrowingSequenceSearch3(ImportModule* m, if (fold) variantFlags |= NarrowingSequenceSearch3::FOLD; - return new NarrowingSequenceSearch3(subjectContext, - searchType, - goal, - maxDepth, - new FreshVariableSource(m, 0), - variantFlags); + Vector startStates; + NarrowingSequenceSearch3* nss = new NarrowingSequenceSearch3(subjectContext, + startStates, + searchType, + goal, + maxDepth, + new FreshVariableSource(m, 0), + variantFlags); + if (nss->problemOK()) + return nss; + else + delete nss; } } return 0; @@ -215,9 +221,10 @@ InterpreterManagerSymbol::getNarrowingSearchResult(FreeDagNode* message, // DagNode* stateDag; int stateVariableFamily; + DagNode* dummy; Substitution* accumulatedSubstitution; - state->getStateInfo(stateDag, stateVariableFamily, accumulatedSubstitution); + state->getStateInfo(stateDag, stateVariableFamily, dummy, accumulatedSubstitution); args[3] = metaLevel->upDagNode(stateDag, m, qidMap, dagNodeMap); args[4] = metaLevel->upType(stateDag->getSort(), qidMap); args[5] = metaLevel->upSubstitution(*accumulatedSubstitution, diff --git a/src/Mixfix/ChangeLog b/src/Mixfix/ChangeLog index d4ee82aa..3b85cac7 100644 --- a/src/Mixfix/ChangeLog +++ b/src/Mixfix/ChangeLog @@ -1,3 +1,259 @@ +2024-05-02 Steven Eker + + * search.cc (Interpreter::search): delete terms and condition fragments + if term disjunction used with anything other than vu-narrow/fvu-narrow + (Interpreter::search): check problemOK() in NarrowingSequenceSearch3() + case + +2024-05-01 Steven Eker + + * narrowing.cc (Interpreter::doVuNarrowing): pass stateNr to + generateSolutionNr() + (Interpreter::doVuNarrowing): print out state number if we + have the KEEP_PATHS flag + + * maudeLatexBuffer.hh (class MaudeLatexBuffer): pass NONE by + default to stateNr argument of generateSolutionNr() + + * maudeLatexBuffer.cc (MaudeLatexBuffer::generateSolutionNr): handle + stateNr argument + + * top.yy: added KW_VFOLD, KW_INVARIANT + + * lexer.ll: added invariant, vfold + +2024-04-24 Steven Eker + + * narrowing.cc (Interpreter::doVuNarrowing): latex initial state + if there was more than one initial state + + * maudeLatexBuffer.hh (class MaudeLatexBuffer): updated decl for + generateState() + + * maudeLatexBuffer.cc (MaudeLatexBuffer::generateState): take a + message argument + + * narrowing.cc (Interpreter::doVuNarrowing): print out initial state + if there was more than one initial state + +2024-04-22 Steven Eker + + * search.cc (Interpreter::search): pass subjectDags to + NarrowingSequenceSearch3() + +2024-04-19 Steven Eker + + * commands.yy (search): fix comment + (command): code cleaning + +2024-04-12 Steven Eker + + * mixfixParser.hh (class MixfixParser): TERM_DISJUNCTION -> + MAKE_TERM_DISJUNCTION + + * maudeLatexBuffer.hh (class MaudeLatexBuffer): updated decl for + generateSearch() + + * search.cc (Interpreter::search): handle the syntax of disjuctions + of initial terms + + * latexCommand.cc (MaudeLatexBuffer::generateSearch): handle + disjuctions of subjects + + * makeGrammar.cc (MixfixModule::makeComponentProductions): use + term disjunction for the first half of search pair + + * mixfixParser.cc (MixfixParser::makeTermDisjunction): added + (MixfixParser::makeSearchCommand): use makeTermDisjunction() + +2024-04-11 Steven Eker + + * mixfixParser.hh (class MixfixParser): added TERM_DISJUNCTION to + enum SemanticActions + + * specialTokens.cc: added vee + + * makeGrammar.cc (MixfixModule::makeComponentProductions): added syntax + for term disjunctions + + * mixfixModule.hh (class MixfixModule): added TERM_DISJUNCTION_TYPE and + set COMPLEX_NUMBER_OF_TYPES = 6 + +2024-04-10 Steven Eker + + * mixfixModule.hh (MixfixModule::nonTerminal): use getNumberOfTypes() + + * makeGrammar.cc (MixfixModule::makeGrammar): use SIMPLE_NUMBER_OF_TYPES, + COMPLEX_NUMBER_OF_TYPES + + * mixfixModule.hh (class MixfixModule): split NUMBER_OF_TYPES into + SIMPLE_NUMBER_OF_TYPES and COMPLEX_NUMBER_OF_TYPES + + * mixfixParser.hh (class MixfixParser): updated decl for ctor + + * mixfixParser.cc (MixfixParser::MixfixParser): take and store + numberOfTypes + + * mixfixParser.hh (class MixfixParser): added data member numberOfTypes + (MixfixParser::getNumberOfTypes): added + + * mixfixModule.hh (MixfixModule::domainComponentIndex): moved here + (MixfixModule::nonTerminal): moved here (both versions) + + * search.cc (Interpreter::search): pass initial as a + Vector& rather than a Term*& + + * mixfixParser.hh (class MixfixParser): updated decl for + makeSearchCommand() + + * mixfixParser.cc (MixfixParser::makeSearchCommand): initial is now a + Vector& rather than a Term*& + + * mixfixModule.hh (class MixfixModule): updated decl for + parseSearchCommand() + + * doParse.cc (MixfixModule::parseSearchCommand): initial is now a + Vector& rather than a Term*& + + * makeGrammar.cc (MixfixModule::makeComplexProductions): added missing + comment for get variants syntax + +2024-04-05 Steven Eker + + * commutativeDecomposeEqualitySymbol.cc + (CommutativeDecomposeEqualitySymbol::acProvablyUnequal): return with + arguments correctly canceled + (CommutativeDecomposeEqualitySymbol::acDecompose): handle the case where + some arguments canceled + +2024-04-04 Steven Eker + + * commutativeDecomposeEqualitySymbol.cc + (CommutativeDecomposeEqualitySymbol::decompose): use acDecompose() + + * commutativeDecomposeEqualitySymbol.hh + (class CommutativeDecomposeEqualitySymbol): added decl for acDecompose() + + * commutativeDecomposeEqualitySymbol.cc + (CommutativeDecomposeEqualitySymbol::acDecompose): added + + * commutativeDecomposeEqualitySymbol.hh + (CommutativeDecomposeEqualitySymbol::makeMultisetFromArguments): + added + (class CommutativeDecomposeEqualitySymbol): made makeMultiset() + static + + * commutativeDecomposeEqualitySymbol.cc + (CommutativeDecomposeEqualitySymbol::acProvablyUnequal): + added pairing argument + +2024-04-03 Steven Eker + + * commutativeDecomposeEqualitySymbol.hh + (class CommutativeDecomposeEqualitySymbol): added decl for + equationallyStableOrGround() + + * commutativeDecomposeEqualitySymbol.cc + (CommutativeDecomposeEqualitySymbol::associativeDecompose): added + (CommutativeDecomposeEqualitySymbol::equationallyStableOrGround): added + + * commutativeDecomposeEqualitySymbol.hh + (class CommutativeDecomposeEqualitySymbol): added decl for + acProvablyUnequal() + + * commutativeDecomposeEqualitySymbol.cc + (CommutativeDecomposeEqualitySymbol::associativeDecompose): use + makeMultiset() rather than fillSet() + + * commutativeDecomposeEqualitySymbol.hh + (class CommutativeDecomposeEqualitySymbol): deleted decl for + fillSet() + + * commutativeDecomposeEqualitySymbol.cc + (CommutativeDecomposeEqualitySymbol::fillSet): deleted + + * commutativeDecomposeEqualitySymbol.hh + (CommutativeDecomposeEqualitySymbol::makeMultiset): added + +2024-04-02 Steven Eker + + * commutativeDecomposeEqualitySymbol.hh + (class CommutativeDecomposeEqualitySymbol): added decl for fillSet() + + * commutativeDecomposeEqualitySymbol.cc + (CommutativeDecomposeEqualitySymbol::fillSet): added + + * commutativeDecomposeEqualitySymbol.hh + (class CommutativeDecomposeEqualitySymbol): + added typedef DagNodeSet + +2024-03-29 Steven Eker + + * commutativeDecomposeEqualitySymbol.hh + (class CommutativeDecomposeEqualitySymbol): updated decl for + decompose() + + * commutativeDecomposeEqualitySymbol.cc + (CommutativeDecomposeEqualitySymbol::decompose) + (CommutativeDecomposeEqualitySymbol::associativeDecompose) + (CommutativeDecomposeEqualitySymbol::eqRewrite): use new + isEquationallyStable() conventions + (CommutativeDecomposeEqualitySymbol::decompose): don't take + MixfixModule* argument + (CommutativeDecomposeEqualitySymbol::eqRewrite): use new decompose + convention + + * commutativeDecomposeEqualitySymbol.hh + (slass CommutativeDecomposeEqualitySymbol): updated decl for + isEquationallyStable(); made it static + + * commutativeDecomposeEqualitySymbol.cc + (CommutativeDecomposeEqualitySymbol::decompose): use + associativeDecompose() + (CommutativeDecomposeEqualitySymbol::equationallyStable): don't + take MixfixModule; renamed to isEquationallyStable() + + * commutativeDecomposeEqualitySymbol.hh + (class CommutativeDecomposeEqualitySymbol): added decl for + associativeDecompose() + + * commutativeDecomposeEqualitySymbol.cc + (CommutativeDecomposeEqualitySymbol::associativeDecompose): + split off assoc code into new function + +2024-03-28 Steven Eker + + * commutativeDecomposeEqualitySymbol.cc + (CommutativeDecomposeEqualitySymbol::decompose): fixed + infinite loop bug + +2024-03-27 Steven Eker + + * commutativeDecomposeEqualitySymbol.cc + (CommutativeDecomposeEqualitySymbol::eqRewrite): rewritten + using equationalStable() + (CommutativeDecomposeEqualitySymbol::decompose): handle + associative case + + * commutativeDecomposeEqualitySymbol.hh + (class CommutativeDecomposeEqualitySymbol): added decl for + equationallyStable() + + * commutativeDecomposeEqualitySymbol.cc + (CommutativeDecomposeEqualitySymbol::equationallyStable): added + +2024-03-26 Steven Eker + + * commutativeDecomposeEqualitySymbol.cc + (CommutativeDecomposeEqualitySymbol::hasImmediateSubterm): + use DagArgumentIterator to work in the general case + (CommutativeDecomposeEqualitySymbol::decompose): check for + the existence of a conjunction symbol here + (CommutativeDecomposeEqualitySymbol::eqRewrite): don't check for + the existence of a conjunctionSymbol here + +===================================Maude160=========================================== + 2024-03-15 Steven Eker * maudeLatexBuffer.cc (MaudeLatexBuffer::generateBanner): tweak diff --git a/src/Mixfix/commands.yy b/src/Mixfix/commands.yy index 71c1b42e..69955529 100644 --- a/src/Mixfix/commands.yy +++ b/src/Mixfix/commands.yy @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 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 @@ -182,10 +182,7 @@ command : KW_SELECT { lexBubble(END_COMMAND, 1); } { lexerInitialMode(); if (interpreter.setCurrentModule(moduleExpr, 1)) - { - interpreter.search(lexerBubble, number, number2, - Interpreter::VU_NARROW, $1, variantOptions); - } + interpreter.search(lexerBubble, number, number2, Interpreter::VU_NARROW, $1, variantOptions); } | match { @@ -658,7 +655,7 @@ conceal : KW_CONCEAL { $$ = true; } | KW_REVEAL { $$ = false; } ; /* - * Return true if we should do a narrowing search. + * Return what sort of search we should do; vu-narrow is handle separately because it has two sets of options. */ search : KW_NARROW { $$ = Interpreter::NARROW; } | KW_XG_NARROW { $$ = Interpreter::XG_NARROW; } @@ -692,6 +689,9 @@ optionsList : option { $$ = $1; } ; option : KW_FOLD { $$ = NarrowingSequenceSearch3::FOLD; } + | KW_VFOLD { $$ = NarrowingSequenceSearch3::VFOLD; } + | KW_PATH { $$ = NarrowingSequenceSearch3::KEEP_PATHS; } + | KW_INVARIANT { $$ = NarrowingSequenceSearch3::INVARIANT; } ; importMode : KW_PROTECT { $$ = ImportModule::PROTECTING; } diff --git a/src/Mixfix/commutativeDecomposeEqualitySymbol.cc b/src/Mixfix/commutativeDecomposeEqualitySymbol.cc index a09c9f50..f42a9bf0 100644 --- a/src/Mixfix/commutativeDecomposeEqualitySymbol.cc +++ b/src/Mixfix/commutativeDecomposeEqualitySymbol.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 2023-2024 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 @@ -34,7 +34,8 @@ #include "core.hh" #include "freeTheory.hh" #include "CUI_Theory.hh" -#include "strategyLanguage.hh" +#include "AU_Theory.hh" +#include "ACU_Theory.hh" #include "mixfix.hh" // interface class definitions @@ -43,7 +44,7 @@ #include "term.hh" // core class definitions -#include "argumentIterator.hh" +#include "dagArgumentIterator.hh" #include "rewritingContext.hh" #include "symbolMap.hh" @@ -55,6 +56,12 @@ #include "CUI_Symbol.hh" #include "CUI_DagNode.hh" +// AU theory class definitions +#include "AU_Symbol.hh" + +// ACU theory class definitions +#include "ACU_Symbol.hh" + // S theory class definitions #include "S_Symbol.hh" #include "S_DagNode.hh" @@ -155,6 +162,15 @@ CommutativeDecomposeEqualitySymbol::reset() CUI_Symbol::reset(); // parents reset() tasks } +bool +CommutativeDecomposeEqualitySymbol::isEquationallyStable(Symbol* s) +{ + return s->isStable() && // can't disappear by instantiation and axioms + s->equationFree() && // can't equationally rewrite at the top + safeCastNonNull(s->getModule())->getSymbolType(s).getBasicType() == + SymbolType::STANDARD; // can't disappear by built-in rewriting +} + bool CommutativeDecomposeEqualitySymbol::eqRewrite(DagNode* subject, RewritingContext& context) { @@ -182,56 +198,42 @@ CommutativeDecomposeEqualitySymbol::eqRewrite(DagNode* subject, RewritingContext // Otherwise we consider the properties of the top symbols. // Symbol* ls = l->symbol(); - if (ls->isStable() && ls->equationFree() && ls->isConstructor(l)) + if (isEquationallyStable(ls)) { // - // Left symbol cannot change under axioms, cannot equationally rewrite, and is declared - // to be a constructor on the arguments it has. + // Left top symbol cannot change under instantiation and equational rewriting. // - MixfixModule* m = safeCastNonNull(ls->getModule()); - if (m->getSymbolType(ls).getBasicType() == SymbolType::STANDARD) + if (hasImmediateSubterm(l, r)) + return context.builtInReplace(subject, notEqualTerm.getDag()); + Symbol* rs = r->symbol(); + if (ls == rs) { // - // No special properties either. + // Consider decomposition. + // + if (DagNode* decomposition = decompose(l, r)) + return context.builtInReplace(subject, decomposition); + } + else + { // - // (by axioms since we've already ruled out equational rewriting and special properties but - // not a future axiom f(X, f(X, Y)) = f(X, Y) for example), then return not equal. + // Return not equal if the right-hand side symbol can't change under instantiation + // equational rewriting. // - if (hasImmediateSubterm(l, r)) + if (isEquationallyStable(rs) || rs->determineGround(r)) return context.builtInReplace(subject, notEqualTerm.getDag()); - Symbol* rs = r->symbol(); - if (ls == rs) - { - if (conjunctionSymbol) - { - // - // Consider decomposition. - // - if (DagNode* decomposition = decompose(m, l, r)) - return context.builtInReplace(subject, decomposition); - } - } - else - { - // - // Consider returning not equal. - // - if (rs->isStable() && rs->equationFree() && rs->isConstructor(r) && - m->getSymbolType(rs).getBasicType() == SymbolType::STANDARD) - return context.builtInReplace(subject, notEqualTerm.getDag()); - } } } else { Symbol* rs = r->symbol(); - if (rs->isStable() && rs->equationFree() && rs->isConstructor(r)) + if (isEquationallyStable(rs)) // thus rs != ls { // - // Check for the converse case where rs is inert and r has an immediate subterm l. + // Check for the converse case where rs is inert and either l is ground or + // r has an immediate subterm l. // - MixfixModule* m = safeCastNonNull(rs->getModule()); - if (m->getSymbolType(rs).getBasicType() == SymbolType::STANDARD && hasImmediateSubterm(r, l)) + if (ls->determineGround(l) || hasImmediateSubterm(r, l)) return context.builtInReplace(subject, notEqualTerm.getDag()); } } @@ -250,8 +252,19 @@ CommutativeDecomposeEqualitySymbol::domainSortAlwaysLeqThan(Sort* /* sort */, in return false; } +bool +CommutativeDecomposeEqualitySymbol::hasImmediateSubterm(DagNode* bigger, DagNode* smaller) +{ + for (DagArgumentIterator d(bigger); d.valid(); d.next()) + { + if (d.argument()->equal(smaller)) + return true; + } + return false; +} + DagNode* -CommutativeDecomposeEqualitySymbol::decompose(MixfixModule* m, DagNode* l, DagNode* r) +CommutativeDecomposeEqualitySymbol::decompose(DagNode* l, DagNode* r) { Symbol* topSymbol = l->symbol(); if (FreeSymbol* f = dynamic_cast(topSymbol)) @@ -259,21 +272,25 @@ CommutativeDecomposeEqualitySymbol::decompose(MixfixModule* m, DagNode* l, DagNo // // FreeSymbol case: decompose into a conjunction. // + MixfixModule* m = safeCastNonNull(getModule()); int polymorphIndex = m->getPolymorphIndex(this); // find our polymorph int arity = f->arity(); - FreeDagNode* left = safeCastNonNull(l); - FreeDagNode* right = safeCastNonNull(r); - Vector subterms(arity); - Vector pair(2); - for (int i = 0; i < arity; ++i) + if (arity == 1 || conjunctionSymbol != nullptr) { - int kindIndex = f->domainComponent(i)->getIndexWithinModule(); - Symbol* sibling = m->instantiatePolymorph(polymorphIndex, kindIndex); - pair[0] = left->getArgument(i); - pair[1] = right->getArgument(i); - subterms[i] = sibling->makeDagNode(pair); + FreeDagNode* left = safeCastNonNull(l); + FreeDagNode* right = safeCastNonNull(r); + Vector subterms(arity); + Vector pair(2); + for (int i = 0; i < arity; ++i) + { + int kindIndex = f->domainComponent(i)->getIndexWithinModule(); + Symbol* sibling = m->instantiatePolymorph(polymorphIndex, kindIndex); + pair[0] = left->getArgument(i); + pair[1] = right->getArgument(i); + subterms[i] = sibling->makeDagNode(pair); + } + return (arity == 1) ? subterms[0] : conjunctionSymbol->makeDagNode(subterms); } - return (arity == 1) ? subterms[0] : conjunctionSymbol->makeDagNode(subterms); } else if (S_Symbol* f = dynamic_cast(topSymbol)) { @@ -301,27 +318,57 @@ CommutativeDecomposeEqualitySymbol::decompose(MixfixModule* m, DagNode* l, DagNo } return makeDagNode(pair); } - else if (disjunctionSymbol) + else if (CUI_Symbol* f = dynamic_cast(topSymbol)) { // - // Having a defined disjunctionSymbol allow us to do more. + // Consider the commutative case. + // + MixfixModule* m = safeCastNonNull(getModule()); + int polymorphIndex = m->getPolymorphIndex(this); // find our polymorph + int kindIndex = f->domainComponent(0)->getIndexWithinModule(); + Symbol* sibling = m->instantiatePolymorph(polymorphIndex, kindIndex); + CUI_DagNode* left = safeCastNonNull(l); + CUI_DagNode* right = safeCastNonNull(r); + DagNode* l0 = left->getArgument(0); + DagNode* l1 = left->getArgument(1); + DagNode* r0 = right->getArgument(0); + DagNode* r1 = right->getArgument(1); + // + // Pick off 4 cases that don't need a disjunction of conjunctions. // - if (CUI_Symbol* f = dynamic_cast(topSymbol)) + Vector pair(2); + if (l0->equal(r0)) + { + pair[0] = l1; + pair[1] = r1; + return sibling->makeDagNode(pair); + } + if (l1->equal(r1)) + { + pair[0] = l0; + pair[1] = r0; + return sibling->makeDagNode(pair); + } + if (l0->equal(r1)) + { + pair[0] = l1; + pair[1] = r0; + return sibling->makeDagNode(pair); + } + if (l1->equal(r0)) + { + pair[0] = l0; + pair[1] = r1; + return sibling->makeDagNode(pair); + } + // + // Otherwise we need to decompose as a disjunction of conjunctions. + // + if (conjunctionSymbol != nullptr && disjunctionSymbol != nullptr) { - int polymorphIndex = m->getPolymorphIndex(this); // find our polymorph - int kindIndex = f->domainComponent(0)->getIndexWithinModule(); - Symbol* sibling = m->instantiatePolymorph(polymorphIndex, kindIndex); - CUI_DagNode* left = safeCastNonNull(l); - CUI_DagNode* right = safeCastNonNull(r); - DagNode* l0 = left->getArgument(0); - DagNode* l1 = left->getArgument(1); - DagNode* r0 = right->getArgument(0); - DagNode* r1 = right->getArgument(1); - Vector orArgs(2); Vector andArgs(2); - Vector pair(2); - + pair[0] = l0; pair[1] = r0; andArgs[0] = sibling->makeDagNode(pair); @@ -341,30 +388,313 @@ CommutativeDecomposeEqualitySymbol::decompose(MixfixModule* m, DagNode* l, DagNo return disjunctionSymbol->makeDagNode(orArgs); } } + else if (AU_Symbol* f = dynamic_cast(topSymbol)) + return associativeDecompose(f, l, r); + else if (ACU_Symbol* f = dynamic_cast(topSymbol)) + return acDecompose(f, l, r); + return 0; +} + +DagNode* +CommutativeDecomposeEqualitySymbol::associativeDecompose(AU_Symbol* f, DagNode* l, DagNode* r) +{ + // + // One or both sides of .=. could be in persistent form, so collect arguments + // in vectors. + // + Vector leftArgs; + for (DagArgumentIterator d(l); d.valid(); d.next()) + leftArgs.push_back(d.argument()); + Vector rightArgs; + for (DagArgumentIterator d(r); d.valid(); d.next()) + rightArgs.push_back(d.argument()); + // + // Try peeling matching arguments from the ends. + // + Vector leftPeels; + Vector rightPeels; + Index leftEnd = leftArgs.size(); + Index rightEnd = rightArgs.size(); + Index maxEnd = max(leftEnd, rightEnd); + Index startMarker = 0; + // + // Peel arguments from the start. + // + for (; startMarker < maxEnd; ++startMarker) + { + DagNode* leftArg = leftArgs[startMarker]; + DagNode* rightArg = rightArgs[startMarker]; + if (leftArg->equal(rightArg)) + continue; // can peel off these arguments + Symbol* ls = leftArg->symbol(); + Symbol* rs = rightArg->symbol(); + if (ls->determineGround(leftArg)) + { + if (rs->determineGround(rightArg)) + return notEqualTerm.getDag(); // unequal ground terms decompose to false + else if (!isEquationallyStable(rs)) + break; // can't peel arguments with a right argument that could change under substitution + } + else + { + if (!isEquationallyStable(ls)) + break; // can't peel arguments with a left argument that could change under substitution + if (!(isEquationallyStable(rs) || rs->determineGround(rightArg))) + break; // can't peel arguments with a right argument that could change under substitution + } + if (ls != rs) + return notEqualTerm.getDag(); // decompose to false + // + // A pair if distinct terms with the same equationally-stable symbol on top + // and at least one is non-ground. + // + leftPeels.push_back(leftArg); + rightPeels.push_back(rightArg); + } + // + // Peel arguments from the end. + // + for (--leftEnd, --rightEnd; leftEnd >= startMarker && rightEnd >= startMarker; --leftEnd, --rightEnd) + { + DagNode* leftArg = leftArgs[leftEnd]; + DagNode* rightArg = rightArgs[rightEnd]; + if (leftArg->equal(rightArg)) + continue; // can peel off these arguments + Symbol* ls = leftArg->symbol(); + Symbol* rs = rightArg->symbol(); + if (ls->determineGround(leftArg)) + { + if (rs->determineGround(rightArg)) + return notEqualTerm.getDag(); // unequal ground terms decompose to false + else if (!isEquationallyStable(rs)) + break; // can't peel arguments with a right argument that could change under substitution + } + else + { + if (!isEquationallyStable(ls)) + break; // can't peel arguments with a left argument that could change under substitution + if (!(isEquationallyStable(rs) || rs->determineGround(rightArg))) + break; // can't peel arguments with a right argument that could change under substitution + } + if (ls != rs) + return notEqualTerm.getDag(); // decompose to false + // + // A pair if distinct terms with the same equationally-stable symbol on top + // and at least one is non-ground. + // + leftPeels.push_back(leftArg); + rightPeels.push_back(rightArg); + } + // + // We've peeled all we can; what's left? + // + Index leftSideRemaining = leftEnd + 1 - startMarker; + Index rightSideRemaining = rightEnd + 1 - startMarker; + if ((leftSideRemaining == 0) != (rightSideRemaining == 0)) + return notEqualTerm.getDag(); // decompose to false + // + // See if we can prove not equal on the remainders by using the commutative axiom. + // + DagNodeMultiset leftMultiset = makeMultiset(leftArgs, startMarker, leftEnd); + DagNodeMultiset rightMultiset = makeMultiset(rightArgs, startMarker, rightEnd); + if (acProvablyUnequal(leftMultiset, rightMultiset)) + return notEqualTerm.getDag(); // decompose to false + Index leftSideTotal = leftArgs.size(); + if (leftSideRemaining == leftSideTotal) + return 0; // no progress - need to exit to avoid an infinite loop + // + // Make decomposition. + // + Index nrPeels = leftPeels.size(); + Index arity = nrPeels + (leftSideRemaining != 0); + // + // We must have some unresolved subterms since left and right terms compared unequal. + // + Assert(arity != 0, "0 arity from peeling unequal assoc terms"); + if (arity == 1 || conjunctionSymbol != nullptr) + { + Vector pair(2); + Vector andArgs(arity); + for (Index i = 0; i < nrPeels; ++i) + { + pair[0] = leftPeels[i]; + pair[1] = rightPeels[i]; + andArgs[i] = makeDagNode(pair); + } + if (leftSideRemaining != 0) + { + if (leftSideRemaining == 1) + pair[0] = leftArgs[startMarker]; + else + { + Vector args(leftSideRemaining); + for (Index i = 0; i < leftSideRemaining; ++i) + args[i] = leftArgs[startMarker + i]; + pair[0] = f->makeDagNode(args); + } + if (rightSideRemaining == 1) + pair[1] = rightArgs[startMarker]; + else + { + Vector args(rightSideRemaining); + for (Index i = 0; i < rightSideRemaining; ++i) + args[i] = rightArgs[startMarker + i]; + pair[1] = f->makeDagNode(args); + } + andArgs[nrPeels] = makeDagNode(pair); + } + return (arity == 1) ? andArgs[0] : conjunctionSymbol->makeDagNode(andArgs); + } + return 0; // can't do anything +} + + +DagNode* +CommutativeDecomposeEqualitySymbol::acDecompose(ACU_Symbol* f, DagNode* l, DagNode* r) +{ + DagNodeMultiset leftMultiset = makeMultisetFromArguments(l); + DagNodeMultiset rightMultiset = makeMultisetFromArguments(r); + Index nrLeftArgs = leftMultiset.size(); + // + // If acProvablyUnequal() can't prove unequal, it may still cancel some subterms. + // + if (acProvablyUnequal(leftMultiset, rightMultiset)) + return notEqualTerm.getDag(); // decompose to false + + Index leftSideRemaining = leftMultiset.size(); + if (leftSideRemaining < nrLeftArgs) + { + // + // acProvablyUnequal() did some cancelation. + // + Vector pair(2); + if (leftSideRemaining == 1) + pair[0] = *(leftMultiset.begin()); + else + { + Vector args(leftSideRemaining); + Index i = 0; + for (DagNode* d : leftMultiset) + args[i++] = d; + pair[0] = f->makeDagNode(args); + } + Index rightSideRemaining = rightMultiset.size(); + if (rightSideRemaining == 1) + pair[1] = *(rightMultiset.begin()); + else + { + Vector args(rightSideRemaining); + Index i = 0; + for (DagNode* d : rightMultiset) + args[i++] = d; + pair[1] = f->makeDagNode(args); + } + return makeDagNode(pair); + } return 0; } bool -CommutativeDecomposeEqualitySymbol::hasImmediateSubterm(DagNode* bigger, DagNode* smaller) +CommutativeDecomposeEqualitySymbol::acProvablyUnequal(DagNodeMultiset& leftMultiset, DagNodeMultiset& rightMultiset) { - if (FreeSymbol* f = dynamic_cast(bigger->symbol())) + // + // We try to prove that the left multiset of subterms can never be equal to the right + // set multiset of subterms, under stubstitution, axioms and equational rewriting. + // We return true if we have a proof, and false if we don't. + // As a side effect, we delete common subterms from the multisets. + // + // Start by deleting equal subterms from each side. We use the naive O(n . log m) approach + // but we could be smarter and do O(n + m). + // + for (auto l = leftMultiset.begin(); l != leftMultiset.end(); ) { - int arity = f->arity(); - FreeDagNode* b = safeCastNonNull(bigger); - for (int i = 0; i < arity; ++i) + auto r = rightMultiset.find(*l); + if (r != rightMultiset.end()) { - if (b->getArgument(i)->equal(smaller)) - return true; + auto t = l; + ++l; + leftMultiset.erase(t); + rightMultiset.erase(r); } + else + ++l; + } + if (leftMultiset.empty()) + return !rightMultiset.empty(); // if left side is empty and right side is not, we have our proof + if (rightMultiset.empty()) + return true; // if right side is empty and left side is not, we have our proof + // + // Both sides are nonempty. See if one side only contains subterms that are ground or headed by + // equationally-stable symbols. + // + bool swapMultisets = false; + bool tryPairingTopSymbols = false; + if (equationallyStableOrGround(rightMultiset)) + { + if (leftMultiset.size() > rightMultiset.size()) + return true; // proof by cardinality argument + swapMultisets = true; + tryPairingTopSymbols = true; // we can go through rightSet, trying to find something that can't be paired + } + if (equationallyStableOrGround(leftMultiset)) + { + if (leftMultiset.size() < rightMultiset.size()) + return true; // proof by cardinality argument + swapMultisets = false; + tryPairingTopSymbols = true; // we can go through rightSet, trying to find something that can't be paired } - else if (S_DagNode* b = dynamic_cast(bigger)) - return b->getArgument()->equal(smaller); - else if (CUI_DagNode* b = dynamic_cast(bigger)) + if (tryPairingTopSymbols) { + if (swapMultisets) + leftMultiset.swap(rightMultiset); // - // We know the top symbol of b is stable so it must only be cummutative. + // We know the leftMultiset only has subterms that can't change their top symbols by + // instantiation, axioms and equational rewriting. We now go throught rightMultiset and + // look for subterms with the same property that can be cancelled with leftMutliset subterms. + // If we ever fail to get a cancellation, we have a proof of inequality. // - return b->getArgument(0)->equal(smaller) || b->getArgument(1)->equal(smaller); + DagNodeMultiset leftCopy(leftMultiset); + for (DagNode* r : rightMultiset) + { + Symbol* rs = r->symbol(); + if (isEquationallyStable(rs) || rs->determineGround(r)) + { + // + // Can only equal something with rs on top. + // + for (DagNode* l : leftCopy) + { + if (l->symbol() == rs) + { + leftCopy.erase(l); + goto nextRightSubterm; + } + } + // + // There is nothing left in leftMultiset that could be equal to r so we have our proof. + // + return true; + nextRightSubterm: + ; + } + } + // + // Restore multisets to their canceled form. + // + if (swapMultisets) + leftMultiset.swap(rightMultiset); } return false; } + +bool +CommutativeDecomposeEqualitySymbol::equationallyStableOrGround(DagNodeMultiset& dagMultiset) +{ + for (DagNode* d : dagMultiset) + { + Symbol* s = d->symbol(); + if (!(isEquationallyStable(s) || s->determineGround(d))) + return false; + } + return true; +} diff --git a/src/Mixfix/commutativeDecomposeEqualitySymbol.hh b/src/Mixfix/commutativeDecomposeEqualitySymbol.hh index 305743e6..908d3d4c 100644 --- a/src/Mixfix/commutativeDecomposeEqualitySymbol.hh +++ b/src/Mixfix/commutativeDecomposeEqualitySymbol.hh @@ -26,6 +26,7 @@ // #ifndef _commutativeDecomposeEqualitySymbol_hh_ #define _commutativeDecomposeEqualitySymbol_hh_ +#include #include "CUI_Symbol.hh" #include "cachedDag.hh" @@ -55,8 +56,17 @@ public: bool domainSortAlwaysLeqThan(Sort* sort, int argNr); private: - DagNode* decompose(MixfixModule* m, DagNode* l, DagNode* r); + typedef multiset DagNodeMultiset; + + static bool isEquationallyStable(Symbol* s); static bool hasImmediateSubterm(DagNode* bigger, DagNode* smaller); + static DagNodeMultiset makeMultiset(const Vector& args, Index start, Index end); + static DagNodeMultiset makeMultisetFromArguments(DagNode* d); + DagNode* decompose(DagNode* l, DagNode* r); + DagNode* associativeDecompose(AU_Symbol* f, DagNode* l, DagNode* r); + DagNode* acDecompose(ACU_Symbol* f, DagNode* l, DagNode* r); + bool acProvablyUnequal(DagNodeMultiset& leftMultiset, DagNodeMultiset& rightMultiset); + bool equationallyStableOrGround(DagNodeMultiset& dagMultiset); Symbol* conjunctionSymbol; Symbol* disjunctionSymbol; @@ -64,4 +74,22 @@ private: CachedDag notEqualTerm; }; +inline CommutativeDecomposeEqualitySymbol::DagNodeMultiset +CommutativeDecomposeEqualitySymbol::makeMultiset(const Vector& args, Index start, Index end) +{ + DagNodeMultiset ms; + for (Index i = start; i <= end; ++i) + ms.insert(args[i]); + return ms; +} + +inline CommutativeDecomposeEqualitySymbol::DagNodeMultiset +CommutativeDecomposeEqualitySymbol::makeMultisetFromArguments(DagNode* d) +{ + DagNodeMultiset ms; + for (DagArgumentIterator i(d); i.valid(); i.next()) + ms.insert(i.argument()); + return ms; +} + #endif diff --git a/src/Mixfix/doParse.cc b/src/Mixfix/doParse.cc index bdec3e85..4ea0a2b0 100644 --- a/src/Mixfix/doParse.cc +++ b/src/Mixfix/doParse.cc @@ -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-2024 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 @@ -213,7 +213,7 @@ MixfixModule::parseUnifyCommand(const Vector& bubble, bool MixfixModule::parseSearchCommand(const Vector& bubble, - Term*& initial, + Vector& initial, int& searchType, Term*& target, Vector& condition) diff --git a/src/Mixfix/latexCommand.cc b/src/Mixfix/latexCommand.cc index 75e4c8ab..9a81d596 100644 --- a/src/Mixfix/latexCommand.cc +++ b/src/Mixfix/latexCommand.cc @@ -340,7 +340,7 @@ MaudeLatexBuffer::generateMatch(bool showCommand, void MaudeLatexBuffer::generateSearch(bool showCommand, Interpreter::SearchKind searchKind, - DagNode* subject, + const Vector& subjects, int searchType, Term* target, const Vector& condition, @@ -351,13 +351,13 @@ MaudeLatexBuffer::generateSearch(bool showCommand, { // // These commands are for the form: - // in : . + // in : . // static const char* searchKindName[] = { "search", "narrow", "xg-narrow", "smt-search", "vu-narrow", "fvu-narrow"}; static const char* searchTypeSymbol[] = { "=>1", "=>+", "=>*", "=>!", "=>#" }; static const char* searchTypeLatex[] = { "\\maudeOneStep", "\\maudeAtLeastOneStep", "\\maudeAnySteps", "\\maudeToNormalForm", "\\maudeToBranch"}; - Module* module = subject->symbol()->getModule(); + Module* module = subjects[0]->symbol()->getModule(); // // Print comment. // @@ -381,7 +381,14 @@ MaudeLatexBuffer::generateSearch(bool showCommand, output << "} "; } safeCastNonNull(module)->printModifiers(output, limit, depth); - commentDagNode(subject); + { + const char* sep = ""; + for (DagNode* d : subjects) + { + output << sep << d; + sep = " \\/ "; + } + } output << ' ' << searchTypeSymbol[searchType] << ' '; commentTerm(target); if (!condition.empty()) @@ -417,7 +424,15 @@ MaudeLatexBuffer::generateSearch(bool showCommand, output << "\\maudeRightBrace"; } generateModifiers(module, limit, depth); - MixfixModule::latexPrintDagNode(output, subject); + { + const char* sep = ""; + for (DagNode* d : subjects) + { + output << sep; + MixfixModule::latexPrintDagNode(output, d); + sep = "\\maudeDisjunction"; + } + } output << searchTypeLatex[searchType]; MixfixModule::latexPrettyPrint(output, target); diff --git a/src/Mixfix/latexResult.cc b/src/Mixfix/latexResult.cc index 5c756d20..a434ceb3 100644 --- a/src/Mixfix/latexResult.cc +++ b/src/Mixfix/latexResult.cc @@ -212,15 +212,15 @@ MaudeLatexBuffer::generateSmtResult(SMT_RewriteSequenceSearch* state, int stateNr = state->getCurrentStateNumber(); DagNode* d = state->getState(stateNr); -output << "\\par\\maudeResponse{state:}\n"; -MixfixModule::latexPrintDagNode(output, d); + output << "\\par\\maudeResponse{state:}\n"; + MixfixModule::latexPrintDagNode(output, d); generateSubstitution(*(state->getSubstitution()), *state, state->getSMT_VarIndices()); output << "\\par\\maudeResponse{where}\n"; - MixfixModule::latexPrintDagNode(output, state->getFinalConstraint()); + MixfixModule::latexPrintDagNode(output, state->getFinalConstraint()); } void diff --git a/src/Mixfix/lexer.ll b/src/Mixfix/lexer.ll index cbf0d8a6..5060604f 100644 --- a/src/Mixfix/lexer.ll +++ b/src/Mixfix/lexer.ll @@ -261,6 +261,8 @@ smt-search return KW_SMT_SEARCH; vu-narrow return KW_VU_NARROW; fvu-narrow return KW_FVU_NARROW; fold return KW_FOLD; +vfold return KW_VFOLD; +invariant return KW_INVARIANT; desugared return KW_DESUGARED; processed return KW_PROCESSED; hook|hooks return KW_HOOKS; diff --git a/src/Mixfix/makeGrammar.cc b/src/Mixfix/makeGrammar.cc index 05a5a88b..51f22bed 100644 --- a/src/Mixfix/makeGrammar.cc +++ b/src/Mixfix/makeGrammar.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 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 @@ -48,15 +48,17 @@ MixfixModule::makeGrammar(bool complexFlag) // fixed one-off: // -1,..., componentNonTerminalBase + 1 // per component: - // componentNonTerminalBase,..., componentNonTerminalBase - NUMBER_OF_TYPES * #components + 1 + // componentNonTerminalBase,..., componentNonTerminalBase - numberOfTypes * #components + 1 // on demand: - // componentNonTerminalBase - NUMBER_OF_TYPES * #components,... downwards + // componentNonTerminalBase - numberOfTypes * #components,... downwards // int componentNonTerminalBase = complexFlag ? COMPLEX_BASE : SIMPLE_BASE; - int nextNonTerminal = componentNonTerminalBase - NUMBER_OF_TYPES * getConnectedComponents().length() + 1; + int numberOfTypes = complexFlag ? COMPLEX_NUMBER_OF_TYPES : SIMPLE_NUMBER_OF_TYPES; + int nextNonTerminal = componentNonTerminalBase - numberOfTypes * getConnectedComponents().length() + 1; parser = new MixfixParser(*this, complexFlag, componentNonTerminalBase, + numberOfTypes, nextNonTerminal, 2 * getSymbols().size()); // very rough estimate of number of tokens DebugInfo("new parser = " << parser << " complexFlag = " << complexFlag << @@ -135,6 +137,13 @@ MixfixModule::makeComplexProductions() static Vector rhs(3); + // + // ::= =>1 + // ::= =>+ + // ::= =>* + // ::= =>! + // ::= =># + // rhs.resize(1); rhs[0] = arrowOne; parser->insertProduction(SEARCH_CONNECTIVE, rhs, 0, emptyGather, @@ -152,7 +161,9 @@ MixfixModule::makeComplexProductions() rhs[0] = arrowHash; parser->insertProduction(SEARCH_CONNECTIVE, rhs, 0, emptyGather, MixfixParser::NOP, RewriteSequenceSearch::BRANCH); - + // + // ::= + // rhs[0] = MATCH_PAIR; parser->insertProduction(MATCH_COMMAND, rhs, 0, gatherAny); // @@ -162,10 +173,19 @@ MixfixModule::makeComplexProductions() rhs[0] = UNIFY_PAIR; parser->insertProduction(UNIFY_COMMAND, rhs, 0, gatherAny); + // + // ::= + // rhs[0] = SEARCH_PAIR; parser->insertProduction(SEARCH_COMMAND, rhs, 0, gatherAny); + // + // ::= + // rhs[0] = TERM; parser->insertProduction(GET_VARIANTS_COMMAND, rhs, 0, gatherAny); + // + // ::= + // rhs[0] = UNIFY_COMMAND; parser->insertProduction(VARIANT_UNIFY_COMMAND, rhs, 0, gatherAny); // @@ -173,26 +193,30 @@ MixfixModule::makeComplexProductions() // rhs[0] = MULTI_MATCH_COMMAND; parser->insertProduction(VARIANT_MATCH_COMMAND, rhs, 0, gatherAny); - + // + // ::= s.t. + // ::= such that + // rhs[0] = suchThat; parser->insertProduction(SUCH_THAT, rhs, 0, emptyGather); - rhs.resize(2); rhs[0] = such; rhs[1] = that; parser->insertProduction(SUCH_THAT, rhs, 0, emptyGather); - + // + // ::= + // rhs.resize(3); rhs[0] = MATCH_PAIR; rhs[1] = SUCH_THAT; rhs[2] = CONDITION; - parser->insertProduction(MATCH_COMMAND, rhs, 0, gatherAnyAnyAny, - MixfixParser::CONDITIONAL_COMMAND); - + parser->insertProduction(MATCH_COMMAND, rhs, 0, gatherAnyAnyAny, MixfixParser::CONDITIONAL_COMMAND); + // + // ::= + // rhs[0] = SEARCH_PAIR; rhs[2] = RULE_CONDITION; - parser->insertProduction(SEARCH_COMMAND, rhs, 0, gatherAnyAnyAny, - MixfixParser::CONDITIONAL_COMMAND); + parser->insertProduction(SEARCH_COMMAND, rhs, 0, gatherAnyAnyAny, MixfixParser::CONDITIONAL_COMMAND); // // ::= /\ // @@ -208,13 +232,15 @@ MixfixModule::makeComplexProductions() rhs[2] = MULTI_MATCH_COMMAND; parser->insertProduction(MULTI_MATCH_COMMAND, rhs, 0, gatherAnyAny, MixfixParser::PAIR_LIST); + // + // ::= such that irreducible + // rhs.resize(4); rhs[0] = TERM; rhs[1] = SUCH_THAT; rhs[2] = TERM_LIST; rhs[3] = irreducible; - parser->insertProduction(GET_VARIANTS_COMMAND, rhs, 0, gatherAnyAnyAny, - MixfixParser::MAKE_TERM_LIST); + parser->insertProduction(GET_VARIANTS_COMMAND, rhs, 0, gatherAnyAnyAny, MixfixParser::MAKE_TERM_LIST); // // ::= irreducible // @@ -223,8 +249,7 @@ MixfixModule::makeComplexProductions() rhs[1] = SUCH_THAT; rhs[2] = TERM_LIST; rhs[3] = irreducible; - parser->insertProduction(VARIANT_UNIFY_COMMAND, rhs, 0, gatherAnyAnyAny, - MixfixParser::MAKE_TERM_LIST); + parser->insertProduction(VARIANT_UNIFY_COMMAND, rhs, 0, gatherAnyAnyAny, MixfixParser::MAKE_TERM_LIST); // // ::= irreducible // @@ -233,10 +258,11 @@ MixfixModule::makeComplexProductions() rhs[1] = SUCH_THAT; rhs[2] = TERM_LIST; rhs[3] = irreducible; - parser->insertProduction(VARIANT_MATCH_COMMAND, rhs, 0, gatherAnyAnyAny, - MixfixParser::MAKE_TERM_LIST); + parser->insertProduction(VARIANT_MATCH_COMMAND, rhs, 0, gatherAnyAnyAny, MixfixParser::MAKE_TERM_LIST); // // Hetrogeneous term lists. + // ::= + // ::= , // rhs.resize(1); rhs[0] = TERM; @@ -248,6 +274,8 @@ MixfixModule::makeComplexProductions() parser->insertProduction(TERM_LIST, rhs, PREFIX_GATHER, gatherPrefixPrefix, MixfixParser::MAKE_TERM_LIST); // // Substitutions. + // ::= + // ::= , // rhs.resize(1); rhs[0] = ASSIGNMENT; @@ -622,35 +650,26 @@ MixfixModule::makeAttributeProductions() parser->insertProduction(ATTRIBUTE, rhs, 0, gatherAny, MixfixParser::MAKE_LABEL_ATTRIBUTE); rhs[0] = metadata; rhs[1] = STRING_NT; - parser->insertProduction(ATTRIBUTE, rhs, 0, gatherAny, - MixfixParser::MAKE_METADATA_ATTRIBUTE); + parser->insertProduction(ATTRIBUTE, rhs, 0, gatherAny, MixfixParser::MAKE_METADATA_ATTRIBUTE); rhs[0] = print; rhs[1] = PRINT_LIST; - parser->insertProduction(ATTRIBUTE, rhs, 0, gatherAny, - MixfixParser::MAKE_PRINT_ATTRIBUTE); + parser->insertProduction(ATTRIBUTE, rhs, 0, gatherAny, MixfixParser::MAKE_PRINT_ATTRIBUTE); rhs.resize(1); - parser->insertProduction(ATTRIBUTE, rhs, 0, emptyGather, - MixfixParser::MAKE_PRINT_ATTRIBUTE); + parser->insertProduction(ATTRIBUTE, rhs, 0, emptyGather, MixfixParser::MAKE_PRINT_ATTRIBUTE); rhs[0] = nonexec; - parser->insertProduction(ATTRIBUTE, rhs, 0, emptyGather, - MixfixParser::MAKE_NONEXEC_ATTRIBUTE); + parser->insertProduction(ATTRIBUTE, rhs, 0, emptyGather, MixfixParser::MAKE_NONEXEC_ATTRIBUTE); rhs[0] = otherwise; - parser->insertProduction(ATTRIBUTE, rhs, 0, emptyGather, - MixfixParser::MAKE_OWISE_ATTRIBUTE); + parser->insertProduction(ATTRIBUTE, rhs, 0, emptyGather, MixfixParser::MAKE_OWISE_ATTRIBUTE); rhs[0] = owise; - parser->insertProduction(ATTRIBUTE, rhs, 0, emptyGather, - MixfixParser::MAKE_OWISE_ATTRIBUTE); + parser->insertProduction(ATTRIBUTE, rhs, 0, emptyGather, MixfixParser::MAKE_OWISE_ATTRIBUTE); rhs[0] = variant; - parser->insertProduction(ATTRIBUTE, rhs, 0, emptyGather, - MixfixParser::MAKE_VARIANT_ATTRIBUTE); + parser->insertProduction(ATTRIBUTE, rhs, 0, emptyGather, MixfixParser::MAKE_VARIANT_ATTRIBUTE); rhs[0] = narrowing; - parser->insertProduction(ATTRIBUTE, rhs, 0, emptyGather, - MixfixParser::MAKE_NARROWING_ATTRIBUTE); + parser->insertProduction(ATTRIBUTE, rhs, 0, emptyGather, MixfixParser::MAKE_NARROWING_ATTRIBUTE); rhs[0] = dnt; - parser->insertProduction(ATTRIBUTE, rhs, 0, emptyGather, - MixfixParser::MAKE_DNT_ATTRIBUTE); + parser->insertProduction(ATTRIBUTE, rhs, 0, emptyGather, MixfixParser::MAKE_DNT_ATTRIBUTE); // // Print items. // @@ -856,8 +875,8 @@ MixfixModule::makeComponentProductions() rhsList[1] = comma; const Vector& components = getConnectedComponents(); - int nrComponents = components.length(); - for (int i = 0; i < nrComponents; i++) + Index nrComponents = components.size(); + for (Index i = 0; i < nrComponents; ++i) { int termNt = nonTerminal(i, TERM_TYPE); int sortNt = nonTerminal(i, SORT_TYPE); @@ -962,17 +981,39 @@ MixfixModule::makeComponentProductions() if (parser->isComplex()) { // - // Syntax for match and search pairs, assignments: + // Syntax for term disjunctions: + // ::= + // ::= \/ + // + static Vector rhsDisjunct(3); + int termDisjunctionNt = nonTerminal(i, TERM_DISJUNCTION_TYPE); + rhsOne[0] = termNt; + parser->insertProduction(termDisjunctionNt, rhsOne, PREFIX_GATHER, gatherAny, MixfixParser::PASS_THRU); + rhsDisjunct[0] = termNt; + rhsDisjunct[1] = vee; + rhsDisjunct[2] = termDisjunctionNt; + parser->insertProduction(termDisjunctionNt, rhsDisjunct, PREFIX_GATHER, gatherPrefixPrefix, + MixfixParser::MAKE_TERM_DISJUNCTION); + // + // ::= + // + rhsPair[0] = termDisjunctionNt; + rhsPair[1] = SEARCH_CONNECTIVE; + parser->insertProduction(SEARCH_PAIR, rhsPair, 0, gatherAnyAnyAny); + // // ::= <=? - // ::= - // ::= <- // + rhsPair[0] = termNt; rhsPair[1] = matches; parser->insertProduction(MATCH_PAIR, rhsPair, 0, gatherAnyAny); + // + // ::= =? + // rhsPair[1] = unifies; parser->insertProduction(UNIFY_PAIR, rhsPair, 0, gatherAnyAny); - rhsPair[1] = SEARCH_CONNECTIVE; - parser->insertProduction(SEARCH_PAIR, rhsPair, 0, gatherAnyAnyAny); + // + // ::= <- + // rhsPair[1] = assignment; Vector gather(2); gather[0] = ASSIGNMENT_PREC; diff --git a/src/Mixfix/maudeLatexBuffer.cc b/src/Mixfix/maudeLatexBuffer.cc index 87e8db41..7704933f 100644 --- a/src/Mixfix/maudeLatexBuffer.cc +++ b/src/Mixfix/maudeLatexBuffer.cc @@ -157,11 +157,16 @@ MaudeLatexBuffer::generateModuleName(NamedEntity* module) } void -MaudeLatexBuffer::generateSolutionNr(int64_t solutionNr) +MaudeLatexBuffer::generateSolutionNr(int64_t solutionNr, int stateNr) { if (needNewline) output << "\\newline"; - output << "\\par\\maudeResponse{Solution }\\maudeNumber{" << solutionNr << "}\n"; + output << "\\par\\maudeResponse{Solution}\\maudeSpace\\maudeNumber{" << solutionNr << "}\n"; + if (stateNr != NONE) + { + output << "\\maudeSpace\\maudePunctuation{(}\\maudeResponse{state}\\maudeSpace\\maudeNumber{" << + stateNr << "}\\maudePunctuation{)}\n"; + } needNewline = true; } @@ -276,9 +281,11 @@ MaudeLatexBuffer::generateAdvisory(const char* message) } void -MaudeLatexBuffer::generateState(DagNode* stateDag) +MaudeLatexBuffer::generateState(DagNode* stateDag, const char* message) { - output << "\\par$\\maudeResponse{state:}\\maudeSpace"; + if (message == nullptr) + message = "state:"; + output << "\\par$\\maudeResponse{" << message << "}\\maudeSpace"; MixfixModule::latexPrintDagNode(output, stateDag); output << "$\n"; } diff --git a/src/Mixfix/maudeLatexBuffer.hh b/src/Mixfix/maudeLatexBuffer.hh index 50cedd13..f307a3b1 100644 --- a/src/Mixfix/maudeLatexBuffer.hh +++ b/src/Mixfix/maudeLatexBuffer.hh @@ -41,7 +41,7 @@ public: void generateBanner(const char* date, const char* time, time_t seconds); void generateHeading(const char* message); void generateModuleName(NamedEntity* module); - void generateState(DagNode* stateDag); + void generateState(DagNode* stateDag, const char* message = nullptr); // // Functions to start latex for commands. // @@ -86,7 +86,7 @@ public: void generateSearch(bool showCommand, Interpreter::SearchKind searchKind, - DagNode* subject, + const Vector& subjects, int searchType, Term* target, const Vector& condition, @@ -103,7 +103,7 @@ public: // // Functions to print results. // - void generateSolutionNr(int64_t solutionNr); + void generateSolutionNr(int64_t solutionNr, int stateNr = NONE); void generateStats(RewritingContext& context, int64_t cpuTime, int64_t realTime, diff --git a/src/Mixfix/mixfixModule.cc b/src/Mixfix/mixfixModule.cc index 3907a20e..fd3deca4 100644 --- a/src/Mixfix/mixfixModule.cc +++ b/src/Mixfix/mixfixModule.cc @@ -180,29 +180,6 @@ Vector MixfixModule::gatherPrefix(1); Vector MixfixModule::gatherPrefixPrefix(2); Vector MixfixModule::gatherAny0(2); -inline int -MixfixModule::domainComponentIndex(const Symbol* symbol, int argNr) -{ - return symbol->domainComponent(argNr)->getIndexWithinModule(); -} - -inline int -MixfixModule::nonTerminal(int componentIndex, NonTerminalType type) -{ - /* - DebugInfo("parser = " << parser << - " parser->isComplex() = " << parser->isComplex() << - " parser->getComponentNonTerminalBase() = " << parser->getComponentNonTerminalBase()); - */ - return parser->getComponentNonTerminalBase() - componentIndex * NUMBER_OF_TYPES - type; -} - -inline int -MixfixModule::nonTerminal(const Sort* sort, NonTerminalType type) -{ - return nonTerminal(sort->component()->getIndexWithinModule(), type); -} - // our stuff #include "latexCommon.cc" #include "latexTermPrint.cc" diff --git a/src/Mixfix/mixfixModule.hh b/src/Mixfix/mixfixModule.hh index 2d39a2a2..e6731aed 100644 --- a/src/Mixfix/mixfixModule.hh +++ b/src/Mixfix/mixfixModule.hh @@ -29,6 +29,7 @@ #include #include #include +#include "strategyLanguage.hh" #include "profileModule.hh" #include "metadataStore.hh" #include "sharedTokens.hh" @@ -40,6 +41,7 @@ #include "SMT_Info.hh" #include "SMT_NumberSymbol.hh" #include "statementTransformer.hh" +#include "mixfixParser.hh" class MixfixModule : public ProfileModule, public MetadataStore, protected SharedTokens { @@ -173,7 +175,7 @@ public: int& firstBad); void parseStatement(const Vector& bubble); bool parseSearchCommand(const Vector& bubble, - Term*& initial, + Vector& initial, int& searchType, Term*& target, Vector& condition); @@ -495,12 +497,16 @@ private: enum NonTerminalType { - NUMBER_OF_TYPES = 5, TERM_TYPE = 0, SORT_TYPE = 1, DOT_SORT_TYPE = 2, ASSOC_LIST_TYPE = 3, - SORT_LIST_TYPE = 4 + SORT_LIST_TYPE = 4, + SIMPLE_NUMBER_OF_TYPES = 5, + // + // In a complex parser, for each kind, we need a nonterminal for t1 \/ t2 \/ ... \/ tn + TERM_DISJUNCTION_TYPE = 5, + COMPLEX_NUMBER_OF_TYPES = 6, }; enum SMT_Status @@ -1342,4 +1348,22 @@ MixfixModule::latexString(int code) return latexString(Token::name(code)); } +inline int +MixfixModule::domainComponentIndex(const Symbol* symbol, int argNr) +{ + return symbol->domainComponent(argNr)->getIndexWithinModule(); +} + +inline int +MixfixModule::nonTerminal(int componentIndex, NonTerminalType type) +{ + return parser->getComponentNonTerminalBase() - componentIndex * parser->getNumberOfTypes() - type; +} + +inline int +MixfixModule::nonTerminal(const Sort* sort, NonTerminalType type) +{ + return nonTerminal(sort->component()->getIndexWithinModule(), type); +} + #endif diff --git a/src/Mixfix/mixfixParser.cc b/src/Mixfix/mixfixParser.cc index 01072140..cd6e448d 100644 --- a/src/Mixfix/mixfixParser.cc +++ b/src/Mixfix/mixfixParser.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 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 @@ -108,11 +108,13 @@ MixfixParser::MixfixParser(MixfixModule& client, bool complexFlag, int componentNonTerminalBase, + int numberOfTypes, int nextNonTerminalCode, int nrTokensGuess) : client(client), complexParser(complexFlag), componentNonTerminalBase(componentNonTerminalBase), + numberOfTypes(numberOfTypes), tokenSet(nrTokensGuess), specialTerminals(Token::LAST_PROPERTY) { @@ -367,7 +369,18 @@ MixfixParser::makeUnifyCommand(Vector& lhs, Vector& rhs) } void -MixfixParser::makeSearchCommand(Term*& initial, +MixfixParser::makeTermDisjunction(int node, Vector& terms) +{ + for (;; node = parser.getChild(node, 1)) + { + terms.push_back(makeTerm(parser.getChild(node, 0))); + if (actions[parser.getProductionNumber(node)].action != MAKE_TERM_DISJUNCTION) + break; + } +} + +void +MixfixParser::makeSearchCommand(Vector& initial, int& searchType, Term*& target, Vector& condition) @@ -375,7 +388,11 @@ MixfixParser::makeSearchCommand(Term*& initial, Assert(nrParses > 0, "no parses"); int node = ROOT_NODE; int searchPair = parser.getChild(node, 0); - initial = makeTerm(parser.getChild(searchPair, 0)); + + makeTermDisjunction(parser.getChild(searchPair, 0), initial); + + //initial.push_back(makeTerm(parser.getChild(searchPair, 0))); // FIXME + int arrowType = parser.getChild(searchPair, 1); searchType = actions[parser.getProductionNumber(arrowType)].data; target = makeTerm(parser.getChild(searchPair, 2)); diff --git a/src/Mixfix/mixfixParser.hh b/src/Mixfix/mixfixParser.hh index ce093822..c0b6b12b 100644 --- a/src/Mixfix/mixfixParser.hh +++ b/src/Mixfix/mixfixParser.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 1997-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 1997-2024 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 @@ -44,6 +44,7 @@ public: // MAKE_TERM, ASSOC_LIST, + MAKE_TERM_DISJUNCTION, // // Special kinds of terms. // @@ -133,6 +134,7 @@ public: MixfixParser(MixfixModule& client, bool complexFlag, int componentNonTerminalBase, + int numberOfTypes, int nextNonTerminalCode, int nrTokensGuess); ~MixfixParser(); @@ -174,7 +176,7 @@ public: Term*& subject, Vector& condition); void makeUnifyCommand(Vector& lhs, Vector& rhs); - void makeSearchCommand(Term*& initial, + void makeSearchCommand(Vector& initial, int& searchType, Term*& target, Vector& condition); @@ -194,6 +196,7 @@ public: bool isComplex() const; int getComponentNonTerminalBase() const; + int getNumberOfTypes() const; int getNrProductions() const; int getNrNonTerminals() const; int getNrTerminals() const; @@ -244,11 +247,13 @@ private: void makeStrategyList(int node, Vector& strategies); void appendUsingPair(int node, Vector& terms, Vector& strategies); void makeUsingList(int node, Vector& terms, Vector& strategies); + void makeTermDisjunction(int node, Vector& terms); int translateSpecialToken(int code); MixfixModule& client; const bool complexParser; const int componentNonTerminalBase; + const int numberOfTypes; int nextNonTerminal; Parser parser; // CFG parser Vector productionRhs; // to avoid creating a new Vector for each production insertion @@ -286,6 +291,12 @@ MixfixParser::getComponentNonTerminalBase() const return componentNonTerminalBase; } +inline int +MixfixParser::getNumberOfTypes() const +{ + return numberOfTypes; +} + inline int MixfixParser::getNrNonTerminals() const { diff --git a/src/Mixfix/narrowing.cc b/src/Mixfix/narrowing.cc index 408ae98e..dfc98210 100644 --- a/src/Mixfix/narrowing.cc +++ b/src/Mixfix/narrowing.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 2017-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 2017-2024 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 @@ -188,25 +188,38 @@ Interpreter::doVuNarrowing(Timer& timer, } ++solutionCount; - cout << "\nSolution " << solutionCount << "\n"; + cout << "\nSolution " << solutionCount; + int stateNr = NONE; + if (state->getVariantFlags() & NarrowingSequenceSearch3::KEEP_PATHS) + { + int dummy; + state->getExtraStateInfo(stateNr, dummy); + cout << " (state " << stateNr << ")"; + } + cout << "\n"; printStats(*context, prof, real, showTiming); DagNode* stateDag; int variableFamily; + DagNode* initialStateDag; Substitution* accumulatedSubstitution; - state->getStateInfo(stateDag, variableFamily, accumulatedSubstitution); + state->getStateInfo(stateDag, variableFamily, initialStateDag, accumulatedSubstitution); cout << "state: " << stateDag << endl; + if (state->getNrInitialStates() > 1) + cout << "initial state: " << initialStateDag << endl; cout << "accumulated substitution:" << endl; UserLevelRewritingContext::printSubstitution(*accumulatedSubstitution, state->getInitialVariableInfo()); cout << "variant unifier:" << endl; UserLevelRewritingContext::printSubstitution(*(state->getUnifier()), state->getUnifierVariableInfo()); if (latexBuffer) { - latexBuffer->generateSolutionNr(solutionCount); + latexBuffer->generateSolutionNr(solutionCount, stateNr); if (getFlag(SHOW_STATS)) latexBuffer->generateStats(*context, prof, real, showTiming, getFlag(SHOW_BREAKDOWN)); latexBuffer->generateState(stateDag); + if (state->getNrInitialStates() > 1) + latexBuffer->generateState(initialStateDag, "initial state:"); latexBuffer->generateHeading("accumulated substitution:"); latexBuffer->generateSubstitution(*accumulatedSubstitution, state->getInitialVariableInfo()); latexBuffer->generateHeading("variant unifier:"); diff --git a/src/Mixfix/search.cc b/src/Mixfix/search.cc index 9b988ca9..84ae94a2 100644 --- a/src/Mixfix/search.cc +++ b/src/Mixfix/search.cc @@ -121,25 +121,35 @@ Interpreter::search(const Vector& bubble, bool debug, int variantFlags) { + static const char* searchKindName[] = {"search", "narrow", "xg-narrow", "smt-search", "vu-narrow", "fvu-narrow"}; VisibleModule* fm = currentModule->getFlatModule(); - Term* initial; + Vector initial; int searchType; Term* target; Vector condition; if (!(fm->parseSearchCommand(bubble, initial, searchType, target, condition))) return; - + Index nrInitialTerms = initial.size(); + if (nrInitialTerms > 1 && !(searchKind == VU_NARROW || searchKind == FVU_NARROW)) + { + IssueWarning(*target << ": term disjunctions are not supported for " << searchKindName[searchKind] << "."); + for (Term* t : initial) + t->deepSelfDestruct(); + target->deepSelfDestruct(); + for (ConditionFragment* cf : condition) + delete cf; + return; + } if (!checkSearchRestrictions(searchKind, searchType, target, condition, fm)) { - initial->deepSelfDestruct(); + for (Term* t : initial) + t->deepSelfDestruct(); target->deepSelfDestruct(); for (ConditionFragment* cf : condition) delete cf; return; } - Pattern* pattern = (searchKind == VU_NARROW || - searchKind == FVU_NARROW || - searchKind == SMT_SEARCH) ? 0 : + Pattern* pattern = (searchKind == VU_NARROW || searchKind == FVU_NARROW || searchKind == SMT_SEARCH) ? 0 : new Pattern(target, false, condition); // // Regular seach cannot have unbound variables. @@ -149,20 +159,20 @@ Interpreter::search(const Vector& bubble, IssueWarning(*target << ": variable " << QUOTE(pattern->index2Variable(pattern->getUnboundVariables().min())) << " is used before it is bound in the condition of a search command.\n"); - initial->deepSelfDestruct(); + for (Term* t : initial) + t->deepSelfDestruct(); delete pattern; return; } - DagNode* subjectDag = makeDag(initial); + Vector subjectDags(nrInitialTerms); + for (Index i = 0; i < nrInitialTerms; ++i) + subjectDags[i] = makeDag(initial[i]); static const char* searchTypeSymbol[] = { "=>1", "=>+", "=>*", "=>!", "=>#" }; bool showCommand = getFlag(SHOW_COMMAND); if (showCommand) { - static const char* searchKindName[] = - { "search", "narrow", "xg-narrow", - "smt-search", "vu-narrow", "fvu-narrow"}; UserLevelRewritingContext::beginCommand(); if (debug) @@ -185,7 +195,13 @@ Interpreter::search(const Vector& bubble, cout << "} "; } printModifiers(limit, depth); - cout << subjectDag << ' ' << searchTypeSymbol[searchType] << ' ' << target; + const char* sep = ""; + for (DagNode* d : subjectDags) + { + cout << sep << d; + sep = " \\/ "; + } + cout << ' ' << searchTypeSymbol[searchType] << ' ' << target; if (!condition.empty()) { cout << " such that "; @@ -194,13 +210,13 @@ Interpreter::search(const Vector& bubble, cout << " ." << endl; if (xmlBuffer != 0) - xmlBuffer->generateSearch(subjectDag, pattern, searchTypeSymbol[searchType], limit, depth); // does this work for narrowing? + xmlBuffer->generateSearch(subjectDags[0], pattern, searchTypeSymbol[searchType], limit, depth); // does this work for narrowing? } if (latexBuffer != 0) { latexBuffer->generateSearch(showCommand, searchKind, - subjectDag, + subjectDags, searchType, target, condition, @@ -218,7 +234,7 @@ Interpreter::search(const Vector& bubble, if (searchKind == SEARCH) { RewriteSequenceSearch* state = - new RewriteSequenceSearch(new UserLevelRewritingContext(subjectDag), + new RewriteSequenceSearch(new UserLevelRewritingContext(subjectDags[0]), static_cast(searchType), pattern, depth); @@ -229,7 +245,7 @@ Interpreter::search(const Vector& bubble, { const SMT_Info& smtInfo = fm->getSMT_Info(); VariableGenerator* vg = new VariableGenerator(smtInfo); - RewritingContext* initial = new UserLevelRewritingContext(subjectDag); + RewritingContext* initial = new UserLevelRewritingContext(subjectDags[0]); // // SMT_RewriteSequenceSearch takes responsibility for deleting // vg and initial. @@ -258,19 +274,25 @@ Interpreter::search(const Vector& bubble, if (searchKind == FVU_NARROW) variantFlags |= NarrowingSequenceSearch3::FOLD; NarrowingSequenceSearch3* state = - new NarrowingSequenceSearch3(new UserLevelRewritingContext(subjectDag), + new NarrowingSequenceSearch3(new UserLevelRewritingContext(subjectDags[0]), + subjectDags, static_cast(searchType), // HACK goal, depth, new FreshVariableSource(fm), variantFlags); + if (!state->problemOK()) + { + delete state; // deletes initial and fresh variable source + return; + } Timer timer(getFlag(SHOW_TIMING)); doVuNarrowing(timer, fm, state, 0, limit); } else { NarrowingSequenceSearch* state = - new NarrowingSequenceSearch(new UserLevelRewritingContext(subjectDag), + new NarrowingSequenceSearch(new UserLevelRewritingContext(subjectDags[0]), static_cast(searchType), // HACK pattern, depth, diff --git a/src/Mixfix/specialTokens.cc b/src/Mixfix/specialTokens.cc index b65586a9..a1199149 100644 --- a/src/Mixfix/specialTokens.cc +++ b/src/Mixfix/specialTokens.cc @@ -128,7 +128,8 @@ MACRO(amatchrew, "amatchrew") MACRO(by, "by") MACRO(irreducible, "irreducible") - MACRO(ellipsis, "..."); + MACRO(ellipsis, "...") + MACRO(vee, "\\/") // // Special hook identifier tokens. // diff --git a/src/Mixfix/top.yy b/src/Mixfix/top.yy index 189f36a0..86c5e741 100644 --- a/src/Mixfix/top.yy +++ b/src/Mixfix/top.yy @@ -165,7 +165,8 @@ int yylex(YYSTYPE* lvalp); %token KW_NUMBER KW_RAT KW_COLOR KW_IMPLIED_STEP %token SIMPLE_NUMBER %token KW_PWD KW_CD KW_PUSHD KW_POPD KW_LS KW_LL KW_LOAD KW_SLOAD KW_QUIT -%token KW_EOF KW_TEST KW_SMT_SEARCH KW_VU_NARROW KW_FVU_NARROW KW_FOLD KW_DESUGARED KW_PROCESSED +%token KW_EOF KW_TEST KW_SMT_SEARCH KW_VU_NARROW KW_FVU_NARROW KW_FOLD KW_VFOLD KW_INVARIANT +%token KW_DESUGARED KW_PROCESSED /* * Start keywords: signal end of mixfix statement if following '.'. diff --git a/src/ObjectSystem/ChangeLog b/src/ObjectSystem/ChangeLog index f83a5cb7..9e00a583 100755 --- a/src/ObjectSystem/ChangeLog +++ b/src/ObjectSystem/ChangeLog @@ -1,3 +1,17 @@ +2024-04-10 Steven Eker + + * timeActions.cc (TimeManagerSymbol::getTimeSinceEpoch): use + double for tv_sec on platforms where long is less than 8 bytes + +2024-04-08 Steven Eker + + * timeActions.cc (TimeManagerSymbol::getTimeSinceEpoch): put + timeValue.tv_sec into an Index variable so that the mpz_class + constructor is defined for 32-bit targets; this will cause a + problem for 32-bit platforms in 2038 if they are still supported + +===================================Maude160=========================================== + 2024-01-22 Steven Eker * directoryActions.cc (DirectoryManagerSymbol::getDirectoryEntry): diff --git a/src/ObjectSystem/timeActions.cc b/src/ObjectSystem/timeActions.cc index 77395aa2..20071003 100644 --- a/src/ObjectSystem/timeActions.cc +++ b/src/ObjectSystem/timeActions.cc @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 2021-2023 SRI International, Menlo Park, CA 94025, USA. + Copyright 2021-2024 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 @@ -39,8 +39,16 @@ TimeManagerSymbol::getTimeSinceEpoch(FreeDagNode* message, ObjectSystemRewriting timespec timeValue; DebugSave(r, clock_gettime(CLOCK_REALTIME, &timeValue)); Assert(r == 0, "clock_gettime() failed: " << strerror(errno)); - - mpz_class nanoSeconds(timeValue.tv_sec); + // + // time_t is 64-bit since Linux kernel 5.6 but GMP doesn't yet have support + // for long long which is a problem on platforms where long is less than 8 bytes. + // +#if SIZEOF_LONG < 8 + double seconds = timeValue.tv_sec; +#else + long seconds = timeValue.tv_sec; +#endif + mpz_class nanoSeconds(seconds); nanoSeconds *= BILLION; nanoSeconds += timeValue.tv_nsec; diff --git a/src/Utility/ChangeLog b/src/Utility/ChangeLog index 0d444237..7a013e97 100644 --- a/src/Utility/ChangeLog +++ b/src/Utility/ChangeLog @@ -1,3 +1,16 @@ +2024-04-18 Steven Eker + + * rope.hh (Rope::const_iterator::operator[]): added + (Rope::const_iterator::operator->): added + +2024-04-17 Steven Eker + + * rope.hh (Rope::const_iterator::operator++): added post increment + version + (Rope::const_iterator::operator--): added post decrement version + +===================================Maude160=================================== + 2024-03-06 Steven Eker * pointerMap.cc (PointerMap::PointerMap, PointerMap::setMap): diff --git a/src/Utility/rope.hh b/src/Utility/rope.hh index 5883de15..a5437fd5 100644 --- a/src/Utility/rope.hh +++ b/src/Utility/rope.hh @@ -2,7 +2,7 @@ This file is part of the Maude 3 interpreter. - Copyright 2020 SRI International, Menlo Park, CA 94025, USA. + Copyright 2020-2024 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 @@ -173,17 +173,17 @@ public: bool operator==(const const_iterator& other) const; bool operator!=(const const_iterator& other) const; const_reference operator*() const; - //const_pointer operator->() const; + const_pointer operator->() const; // // Forward iterator stuff. // const_iterator& operator++(); - //const_iterator operator++(int); + const_iterator operator++(int); // // Bidirectional iterator stuff. // const_iterator& operator--(); - //const_iterator operator--(int); + const_iterator operator--(int); // // Random access iterator stuff. // @@ -192,7 +192,7 @@ public: const_iterator& operator-=(difference_type delta); const_iterator operator-(difference_type delta) const; difference_type operator-(const const_iterator& other) const; - //const_reference operator[](difference_type i) const; + const_reference operator[](difference_type n) const; bool operator<(const const_iterator& other) const; private: @@ -356,6 +356,41 @@ Rope::end() const return const_iterator(this); } +/* + * Rope::const_iterator + */ + +inline +Rope::const_iterator +Rope::const_iterator::operator++(int) +{ + const_iterator dup(*this); + operator++(); + return dup; +} + +inline +Rope::const_iterator +Rope::const_iterator::operator--(int) +{ + const_iterator dup(*this); + operator--(); + return dup; +} + +inline Rope::const_iterator::const_reference +Rope::const_iterator::operator[](difference_type n) const +{ + return *(operator+(n)); +} + +inline Rope::const_iterator::const_pointer +Rope::const_iterator::operator->() const +{ + Assert(index < END_MARKER, "trying to dereference an end iterator, index = " << index); + return &(stackPtr->ptr->leaf[index]); +} + inline Rope::const_iterator::difference_type Rope::const_iterator::operator-(const const_iterator& other) const { diff --git a/tests/BuiltIn/Makefile.am b/tests/BuiltIn/Makefile.am index cd81292c..3cf2f92f 100644 --- a/tests/BuiltIn/Makefile.am +++ b/tests/BuiltIn/Makefile.am @@ -3,20 +3,23 @@ TESTS = \ int \ rat \ string \ - counters + counters \ + stringOps MAUDE_FILES = \ nat.maude \ int.maude \ rat.maude \ string.maude \ - counters.maude + counters.maude \ + stringOps.maude RESULT_FILES = \ nat.expected \ int.expected \ rat.expected \ string.expected \ - counters.expected + counters.expected \ + stringOps.expected EXTRA_DIST = $(TESTS) $(MAUDE_FILES) $(RESULT_FILES) diff --git a/tests/BuiltIn/Makefile.in b/tests/BuiltIn/Makefile.in index 3b305053..c8427d30 100644 --- a/tests/BuiltIn/Makefile.in +++ b/tests/BuiltIn/Makefile.in @@ -440,21 +440,24 @@ TESTS = \ int \ rat \ string \ - counters + counters \ + stringOps MAUDE_FILES = \ nat.maude \ int.maude \ rat.maude \ string.maude \ - counters.maude + counters.maude \ + stringOps.maude RESULT_FILES = \ nat.expected \ int.expected \ rat.expected \ string.expected \ - counters.expected + counters.expected \ + stringOps.expected EXTRA_DIST = $(TESTS) $(MAUDE_FILES) $(RESULT_FILES) all: all-am @@ -673,6 +676,13 @@ counters.log: counters --log-file $$b.log --trs-file $$b.trs \ $(am__common_driver_flags) $(AM_LOG_DRIVER_FLAGS) $(LOG_DRIVER_FLAGS) -- $(LOG_COMPILE) \ "$$tst" $(AM_TESTS_FD_REDIRECT) +stringOps.log: stringOps + @p='stringOps'; \ + b='stringOps'; \ + $(am__check_pre) $(LOG_DRIVER) --test-name "$$f" \ + --log-file $$b.log --trs-file $$b.trs \ + $(am__common_driver_flags) $(AM_LOG_DRIVER_FLAGS) $(LOG_DRIVER_FLAGS) -- $(LOG_COMPILE) \ + "$$tst" $(AM_TESTS_FD_REDIRECT) .test.log: @p='$<'; \ $(am__set_b); \ diff --git a/tests/BuiltIn/stringOps b/tests/BuiltIn/stringOps new file mode 100755 index 00000000..829daee8 --- /dev/null +++ b/tests/BuiltIn/stringOps @@ -0,0 +1,10 @@ +#!/bin/sh + +MAUDE_LIB=$srcdir/../../src/Main +export MAUDE_LIB + +../../src/Main/maude \ + < $srcdir/stringOps.maude -no-banner -no-advise \ + > stringOps.out 2>&1 + +diff $srcdir/stringOps.expected stringOps.out > /dev/null 2>&1 diff --git a/tests/BuiltIn/stringOps.expected b/tests/BuiltIn/stringOps.expected new file mode 100644 index 00000000..8841c449 --- /dev/null +++ b/tests/BuiltIn/stringOps.expected @@ -0,0 +1,193 @@ +========================================== +reduce in STRING-OPS : isControl("\n") . +rewrites: 1 +result Bool: true +========================================== +reduce in STRING-OPS : isControl("a") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : isPrintable("a") . +rewrites: 1 +result Bool: true +========================================== +reduce in STRING-OPS : isPrintable("\n") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : isWhiteSpace("\n") . +rewrites: 1 +result Bool: true +========================================== +reduce in STRING-OPS : isWhiteSpace("2") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : isBlank("\t") . +rewrites: 1 +result Bool: true +========================================== +reduce in STRING-OPS : isBlank("\n") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : isGraphic("a") . +rewrites: 1 +result Bool: true +========================================== +reduce in STRING-OPS : isGraphic(" ") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : isPunctuation(";") . +rewrites: 1 +result Bool: true +========================================== +reduce in STRING-OPS : isPunctuation("a") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : isAlphanumeric("a") . +rewrites: 1 +result Bool: true +========================================== +reduce in STRING-OPS : isAlphanumeric("3") . +rewrites: 1 +result Bool: true +========================================== +reduce in STRING-OPS : isAlphanumeric("!") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : isAlphanumeric("\n") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : isAlphanumeric("word") . +rewrites: 0 +result [Bool]: isAlphanumeric("word") +========================================== +reduce in STRING-OPS : isAlphabetic("a") . +rewrites: 1 +result Bool: true +========================================== +reduce in STRING-OPS : isAlphabetic("3") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : isAlphabetic("!") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : isUppercase("a") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : isUppercase("A") . +rewrites: 1 +result Bool: true +========================================== +reduce in STRING-OPS : isUppercase("4") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : isLowercase("a") . +rewrites: 1 +result Bool: true +========================================== +reduce in STRING-OPS : isLowercase("A") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : isLowercase("4") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : isDigit("A") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : isDigit("4") . +rewrites: 1 +result Bool: true +========================================== +reduce in STRING-OPS : isHexadecimalDigit("A") . +rewrites: 1 +result Bool: true +========================================== +reduce in STRING-OPS : isHexadecimalDigit("4") . +rewrites: 1 +result Bool: true +========================================== +reduce in STRING-OPS : isHexadecimalDigit("G") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : startsWith("Foo foo", "Foo") . +rewrites: 1 +result Bool: true +========================================== +reduce in STRING-OPS : startsWith("Foo foo", "Bar") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : startsWith("Foo foo", "BarBarBar") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : endsWith("Foo foo", "foo") . +rewrites: 1 +result Bool: true +========================================== +reduce in STRING-OPS : endsWith("Foo foo", "Bar") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : endsWith("Foo foo", "BarBarBar") . +rewrites: 1 +result Bool: false +========================================== +reduce in STRING-OPS : trimStart(" \nFoo\n ") . +rewrites: 1 +result String: "Foo\n " +========================================== +reduce in STRING-OPS : trimStart("BarFoo\n ") . +rewrites: 1 +result String: "BarFoo\n " +========================================== +reduce in STRING-OPS : trimStart("\t\t \f\r \n ") . +rewrites: 1 +result String: "" +========================================== +reduce in STRING-OPS : trimEnd(" \nFoo\n ") . +rewrites: 1 +result String: " \nFoo" +========================================== +reduce in STRING-OPS : trimEnd(" \nFooBar") . +rewrites: 1 +result String: " \nFooBar" +========================================== +reduce in STRING-OPS : trimEnd("\t\t \f\r \n ") . +rewrites: 1 +result String: "" +========================================== +reduce in STRING-OPS : trim(" \nFoo\n ") . +rewrites: 1 +result String: "Foo" +========================================== +reduce in STRING-OPS : trim("Foo\n ") . +rewrites: 1 +result String: "Foo" +========================================== +reduce in STRING-OPS : trim(" \nFoo") . +rewrites: 1 +result String: "Foo" +========================================== +reduce in STRING-OPS : trim("FooBar") . +rewrites: 1 +result String: "FooBar" +========================================== +reduce in STRING-OPS : trim("\t\t \f\r \n ") . +rewrites: 1 +result String: "" +Bye. diff --git a/tests/BuiltIn/stringOps.maude b/tests/BuiltIn/stringOps.maude new file mode 100644 index 00000000..ea61c470 --- /dev/null +++ b/tests/BuiltIn/stringOps.maude @@ -0,0 +1,69 @@ +set show timing off . +set show advisories off . + +select STRING-OPS . + +red isControl("\n") . +red isControl("a") . + +red isPrintable("a") . +red isPrintable("\n") . + +red isWhiteSpace("\n") . +red isWhiteSpace("2") . + +red isBlank("\t") . +red isBlank("\n") . + +red isGraphic("a") . +red isGraphic(" ") . + +red isPunctuation(";") . +red isPunctuation("a") . + +red isAlphanumeric("a") . +red isAlphanumeric("3") . +red isAlphanumeric("!") . +red isAlphanumeric("\n") . +red isAlphanumeric("word") . + +red isAlphabetic("a") . +red isAlphabetic("3") . +red isAlphabetic("!") . + +red isUppercase("a") . +red isUppercase("A") . +red isUppercase("4") . + +red isLowercase("a") . +red isLowercase("A") . +red isLowercase("4") . + +red isDigit("A") . +red isDigit("4") . + +red isHexadecimalDigit("A") . +red isHexadecimalDigit("4") . +red isHexadecimalDigit("G") . + +red startsWith("Foo foo", "Foo") . +red startsWith("Foo foo", "Bar") . +red startsWith("Foo foo", "BarBarBar") . + +red endsWith("Foo foo", "foo") . +red endsWith("Foo foo", "Bar") . +red endsWith("Foo foo", "BarBarBar") . + +red trimStart(" \nFoo\n ") . +red trimStart("BarFoo\n ") . +red trimStart("\t\t \f\r \n ") . + +red trimEnd(" \nFoo\n ") . +red trimEnd(" \nFooBar") . +red trimEnd("\t\t \f\r \n ") . + +red trim(" \nFoo\n ") . +red trim("Foo\n ") . +red trim(" \nFoo") . +red trim("FooBar") . +red trim("\t\t \f\r \n ") . diff --git a/tests/Corner/badRenaming.expected b/tests/Corner/badRenaming.expected index 9ada9c99..822718ad 100644 --- a/tests/Corner/badRenaming.expected +++ b/tests/Corner/badRenaming.expected @@ -63,6 +63,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -228,6 +229,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -395,6 +397,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -562,6 +565,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -746,6 +750,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -929,6 +934,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -1098,6 +1104,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -1280,6 +1287,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -1462,6 +1470,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -1646,6 +1655,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -1830,6 +1840,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET diff --git a/tests/Corner/badView.expected b/tests/Corner/badView.expected index da59af96..78d17c16 100644 --- a/tests/Corner/badView.expected +++ b/tests/Corner/badView.expected @@ -158,6 +158,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -368,6 +369,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -580,6 +582,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -786,6 +789,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET diff --git a/tests/Corner/operatorNames.expected b/tests/Corner/operatorNames.expected index 67caa259..9b4875c7 100644 --- a/tests/Corner/operatorNames.expected +++ b/tests/Corner/operatorNames.expected @@ -82,6 +82,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET diff --git a/tests/Misc/initialEqualityPredicate.expected b/tests/Misc/initialEqualityPredicate.expected index ceea7246..b4f260d2 100644 --- a/tests/Misc/initialEqualityPredicate.expected +++ b/tests/Misc/initialEqualityPredicate.expected @@ -61,9 +61,8 @@ result Bool: A .=. X and B .=. Y xor A .=. Y and B .=. X xor A .=. X and A .=. Y and B .=. X and B .=. Y ========================================== reduce in DECOMPOSE : c(A, X) .=. c(X, Y) . -rewrites: 4 -result Bool: A .=. X and X .=. Y xor A .=. X and A .=. Y and X .=. Y xor A .=. - Y +rewrites: 1 +result Bool: A .=. Y ========================================== reduce in DECOMPOSE : c(Z, c(X, Y)) .=. c(X, Y) . rewrites: 1 @@ -76,4 +75,36 @@ result Bool: A .=. W and B .=. Z and C .=. X and Y .=. D reduce in DECOMPOSE : c(f(A, B), f(C, D)) .=. c(f(X, Y), g(W, Z)) . rewrites: 11 result Bool: false +========================================== +reduce in FOO : g(X) .=. g(Y) . +rewrites: 1 +result Bool: X .=. Y +========================================== +reduce in FOO : h(X) .=. f(a, c, g(b)) . +rewrites: 1 +result Bool: false +========================================== +reduce in FOO : s(Z, g(X)) .=. s(Y, g(X)) . +rewrites: 1 +result Bool: Z .=. Y +========================================== +reduce in FOO : g(A) + B + h(C) .=. g(A) + g(B) + g(C) . +rewrites: 1 +result Bool: false +========================================== +reduce in FOO : B + g(A) .=. g(A) + g(B) + g(C) . +rewrites: 1 +result Bool: B .=. g(B) + g(C) +========================================== +reduce in FOO : g(A) B X h(A) Y h(C) .=. h(A) g(D) g(E) Z X h(A) . +rewrites: 1 +result Bool: false +========================================== +reduce in FOO : g(A) X Y h(A) h(C) .=. g(D) g(E) g(D) X h(A) . +rewrites: 1 +result Bool: false +========================================== +reduce in FOO : g(A) g(B) X h(A) Y h(C) .=. g(D) g(E) Z X h(A) . +rewrites: 4 +result Bool: E .=. B and A .=. C and A .=. D and Z X .=. X h(A) Y Bye. diff --git a/tests/Misc/initialEqualityPredicate.maude b/tests/Misc/initialEqualityPredicate.maude index 7ad8a9bd..0f69a642 100644 --- a/tests/Misc/initialEqualityPredicate.maude +++ b/tests/Misc/initialEqualityPredicate.maude @@ -43,3 +43,35 @@ red c(c(X, Y), Z) .=. c(X, Y) . *** compound red c(f(X, Y), g(W, Z)) .=. c(g(A, B), f(C, D)) . red c(f(X, Y), g(W, Z)) .=. c(f(A, B), f(C, D)) . + + +fmod FOO is + inc INITIAL-EQUALITY-PREDICATE . + sort Foo . + ops a b c 1 : -> Foo . + op __ : Foo Foo -> Foo [assoc] . + op _+_ : Foo Foo -> Foo [assoc comm] . + op s : Foo Foo -> Foo [comm] . + op f : Foo Foo -> Foo [assoc comm id: 1] . + ops g h p : Foo -> Foo . + var A B C D E W X Y Z : Foo . + eq p(X) = g(h(X)) . +endfm + +*** ctor declaration not needed for decomposition +red g(X) .=. g(Y) . + +*** ground vs equationally-stable +red f(a, g(b), c) .=. h(X) . + +*** canceling under commutative +red s(g(X), Z) .=. s(Y, g(X)) . + +*** AC +red g(A) + g(B) + g(C) .=. g(A) + B + h(C) . +red g(A) + g(B) + g(C) .=. g(A) + B . + +*** associative +red g(A) (B) X h(A) Y h(C) .=. h(A) g(D) g(E) Z X h(A) . +red g(A) X Y h(A) h(C) .=. g(D) g(E) g(D) X h(A) . +red g(A) g(B) X h(A) Y h(C) .=. g(D) g(E) Z X h(A) . diff --git a/tests/Misc/parameterization.expected b/tests/Misc/parameterization.expected index b87453de..26e59437 100644 --- a/tests/Misc/parameterization.expected +++ b/tests/Misc/parameterization.expected @@ -581,6 +581,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -1290,6 +1291,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -2003,6 +2005,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -2309,6 +2312,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET diff --git a/tests/Misc/parameterizedView.expected b/tests/Misc/parameterizedView.expected index f7725275..618147a4 100644 --- a/tests/Misc/parameterizedView.expected +++ b/tests/Misc/parameterizedView.expected @@ -117,6 +117,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET diff --git a/tests/Misc/renaming.expected b/tests/Misc/renaming.expected index a07ed563..fdb373cf 100644 --- a/tests/Misc/renaming.expected +++ b/tests/Misc/renaming.expected @@ -298,6 +298,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET diff --git a/tests/ResolvedBugs/Makefile.am b/tests/ResolvedBugs/Makefile.am index 0c1aa0f3..737be82c 100644 --- a/tests/ResolvedBugs/Makefile.am +++ b/tests/ResolvedBugs/Makefile.am @@ -66,7 +66,8 @@ TESTS = \ redBlackNGA_April2023 \ stripperCollectorSwitchMay2023 \ filteredVariantUnifyJune2023 \ - conditionSideEffectInStrategyLanguageDecember2023 + conditionSideEffectInStrategyLanguageDecember2023 \ + stringToRatConversionMarch2024 MAUDE_FILES = \ CUIbug12-22-09.maude \ @@ -136,7 +137,8 @@ MAUDE_FILES = \ redBlackNGA_April2023.maude \ stripperCollectorSwitchMay2023.maude \ filteredVariantUnifyJune2023.maude \ - conditionSideEffectInStrategyLanguageDecember2023.maude + conditionSideEffectInStrategyLanguageDecember2023.maude \ + stringToRatConversionMarch2024.maude RESULT_FILES = \ @@ -207,7 +209,8 @@ RESULT_FILES = \ redBlackNGA_April2023.expected \ stripperCollectorSwitchMay2023.expected \ filteredVariantUnifyJune2023.expected \ - conditionSideEffectInStrategyLanguageDecember2023.expected + conditionSideEffectInStrategyLanguageDecember2023.expected \ + stringToRatConversionMarch2024.expected EXTRA_DIST = $(TESTS) $(MAUDE_FILES) $(RESULT_FILES) diff --git a/tests/ResolvedBugs/Makefile.in b/tests/ResolvedBugs/Makefile.in index 93e4d9be..72dffe6f 100644 --- a/tests/ResolvedBugs/Makefile.in +++ b/tests/ResolvedBugs/Makefile.in @@ -503,7 +503,8 @@ TESTS = \ redBlackNGA_April2023 \ stripperCollectorSwitchMay2023 \ filteredVariantUnifyJune2023 \ - conditionSideEffectInStrategyLanguageDecember2023 + conditionSideEffectInStrategyLanguageDecember2023 \ + stringToRatConversionMarch2024 MAUDE_FILES = \ CUIbug12-22-09.maude \ @@ -573,7 +574,8 @@ MAUDE_FILES = \ redBlackNGA_April2023.maude \ stripperCollectorSwitchMay2023.maude \ filteredVariantUnifyJune2023.maude \ - conditionSideEffectInStrategyLanguageDecember2023.maude + conditionSideEffectInStrategyLanguageDecember2023.maude \ + stringToRatConversionMarch2024.maude RESULT_FILES = \ CUIbug12-22-09.expected \ @@ -643,7 +645,8 @@ RESULT_FILES = \ redBlackNGA_April2023.expected \ stripperCollectorSwitchMay2023.expected \ filteredVariantUnifyJune2023.expected \ - conditionSideEffectInStrategyLanguageDecember2023.expected + conditionSideEffectInStrategyLanguageDecember2023.expected \ + stringToRatConversionMarch2024.expected EXTRA_DIST = $(TESTS) $(MAUDE_FILES) $(RESULT_FILES) all: all-am @@ -1303,6 +1306,13 @@ conditionSideEffectInStrategyLanguageDecember2023.log: conditionSideEffectInStra --log-file $$b.log --trs-file $$b.trs \ $(am__common_driver_flags) $(AM_LOG_DRIVER_FLAGS) $(LOG_DRIVER_FLAGS) -- $(LOG_COMPILE) \ "$$tst" $(AM_TESTS_FD_REDIRECT) +stringToRatConversionMarch2024.log: stringToRatConversionMarch2024 + @p='stringToRatConversionMarch2024'; \ + b='stringToRatConversionMarch2024'; \ + $(am__check_pre) $(LOG_DRIVER) --test-name "$$f" \ + --log-file $$b.log --trs-file $$b.trs \ + $(am__common_driver_flags) $(AM_LOG_DRIVER_FLAGS) $(LOG_DRIVER_FLAGS) -- $(LOG_COMPILE) \ + "$$tst" $(AM_TESTS_FD_REDIRECT) .test.log: @p='$<'; \ $(am__set_b); \ diff --git a/tests/ResolvedBugs/moduleOrphanedByViewFebruary2023.expected b/tests/ResolvedBugs/moduleOrphanedByViewFebruary2023.expected index 93703a20..d1ab6bbd 100644 --- a/tests/ResolvedBugs/moduleOrphanedByViewFebruary2023.expected +++ b/tests/ResolvedBugs/moduleOrphanedByViewFebruary2023.expected @@ -32,6 +32,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -185,6 +186,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET diff --git a/tests/ResolvedBugs/orphanedViewInstantiationFebruary2023.expected b/tests/ResolvedBugs/orphanedViewInstantiationFebruary2023.expected index 7202b391..9d3a095a 100644 --- a/tests/ResolvedBugs/orphanedViewInstantiationFebruary2023.expected +++ b/tests/ResolvedBugs/orphanedViewInstantiationFebruary2023.expected @@ -32,6 +32,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET @@ -225,6 +226,7 @@ fmod LIST* fmod SET* fmod MAP fmod ARRAY +fmod STRING-OPS fmod NAT-LIST fmod QID-LIST fmod QID-SET diff --git a/tests/ResolvedBugs/stringToRatConversionMarch2024 b/tests/ResolvedBugs/stringToRatConversionMarch2024 new file mode 100755 index 00000000..5b4fe9e1 --- /dev/null +++ b/tests/ResolvedBugs/stringToRatConversionMarch2024 @@ -0,0 +1,10 @@ +#!/bin/sh + +MAUDE_LIB=$srcdir/../../src/Main +export MAUDE_LIB + +../../src/Main/maude \ + < $srcdir/stringToRatConversionMarch2024.maude -no-banner -no-advise \ + > stringToRatConversionMarch2024.out 2>&1 + +diff $srcdir/stringToRatConversionMarch2024.expected stringToRatConversionMarch2024.out > /dev/null 2>&1 diff --git a/tests/ResolvedBugs/stringToRatConversionMarch2024.expected b/tests/ResolvedBugs/stringToRatConversionMarch2024.expected new file mode 100644 index 00000000..55ea0aaa --- /dev/null +++ b/tests/ResolvedBugs/stringToRatConversionMarch2024.expected @@ -0,0 +1,13 @@ +========================================== +reduce in CONVERSION : rat("-0", 10) . +rewrites: 1 +result Zero: 0 +========================================== +reduce in CONVERSION : rat("0/1", 10) . +rewrites: 1 +result Zero: 0 +========================================== +reduce in CONVERSION : rat("-0/1", 10) . +rewrites: 1 +result Zero: 0 +Bye. diff --git a/tests/ResolvedBugs/stringToRatConversionMarch2024.maude b/tests/ResolvedBugs/stringToRatConversionMarch2024.maude new file mode 100644 index 00000000..1a190c67 --- /dev/null +++ b/tests/ResolvedBugs/stringToRatConversionMarch2024.maude @@ -0,0 +1,14 @@ +set show timing off . +set show advisories off . + +*** +*** Test for bug where certain strings did not convert. +*** + +select CONVERSION . + +red rat("-0", 10) . + +red rat("0/1", 10) . + +red rat("-0/1", 10) .