12016-05-18 Steven Eker <eker@install.csl.sri.com> 2 3 * ACU_UnificationSubproblem2.cc (addUnification): check for subtermIndex 4 != NONE 5 (setMultiplicity): check for variable bound to identity; this fixes 6 a bug introduced in Maude108 where classify assumes such things 7 have already canceled 8 9===================================Maude110=========================================== 10 112016-05-17 Steven Eker <eker@install.csl.sri.com> 12 13 * ACU_Symbol.cc (computeGeneralizedSort2): fixed nasty FMR bug 14 where we were appending a reference to the same Vector which 15 became stale if the append forced reallocation 16 172016-03-24 Steven Eker <eker@install.csl.sri.com> 18 19 * ACU_Symbol.cc (computeGeneralizedSort2): rewritten 20 212016-03-18 Steven Eker <eker@install.csl.sri.com> 22 23 * ACU_Symbol.cc (computeGeneralizedSort2): added 24 25===================================Maude110=========================================== 26 272015-08-07 Steven Eker <eker@ape.csl.sri.com> 28 29 * ACU_Symbol.cc (unificationPriority): make ACU have a lower 30 priority than AC 31 322015-07-31 Steven Eker <eker@ape.csl.sri.com> 33 34 * ACU_UnificationSubproblem2.cc (classify): handle ground aliens 35 specially 36 372015-07-30 Steven Eker <eker@ape.csl.sri.com> 38 39 * ACU_DagNode.cc (computeBaseSortForGroundSubterms): call 40 setGround() in the ground case 41 42===================================Maude108=========================================== 43 442014-06-20 Steven Eker <eker@ape.csl.sri.com> 45 46 * ACU_UnificationSubproblem2.cc (solve): added comment with new 47 insight into why solved forms must be unsolved 48 49===================================Maude104=========================================== 50 512013-02-28 Steven Eker <eker@ape.csl.sri.com> 52 53 * ACU_UnificationSubproblem2.cc (addUnification): call killCancelledSubterms() 54 55 * ACU_UnificationSubproblem2.hh (SimpleRootContainer): added decl 56 for killCancelledSubterms() 57 58 * ACU_UnificationSubproblem2.cc (killCancelledSubterms): added 59 602013-02-27 Steven Eker <eker@ape.csl.sri.com> 61 62 * ACU_UnificationSubproblem2.cc (ACU_UnificationSubproblem2): 63 removed pointless #ifndef 64 (addUnification): code cleaning 65 (markReachableNodes): code cleaning 66 (solve): fix performance bug where we were checking subterms 67 rather than unifications for emptiness to detect the degenerate 68 case 69 (markReachableNodes): protect preSolveSubstitution rather than 70 savedSubstitution since it will have a superset of bindings 71 722013-02-07 Steven Eker <eker@ape.csl.sri.com> 73 74 * ACU_UnificationSubproblem2.cc: only bind variables to dags which 75 are in our theory - leave everything else to 76 computeSolvedForm() - This is to fix a bug where we bind a variable 77 to itself, or form an occurs check problem in an alien theory 78 79===================================Maude96c=========================================== 80 812012-07-10 Steven Eker <eker@ape.csl.sri.com> 82 83 * ACU_BaseDagNode.hh (DagNode): update comment on ASSIGNMENT now 84 that we can have variables at the kind level, and thus we don't 85 guarentee non-error sort this NormalizationStatus 86 87===================================Maude96a=========================================== 88 892012-04-30 Steven Eker <eker@ape.csl.sri.com> 90 91 * ACU_Term.cc (ACU_Term): multiplicities version: fix Assert(), 92 now that we can have a single argument with multiplicity >= 2 93 942012-04-13 Steven Eker <eker@ape.csl.sri.com> 95 96 * ACU_DagNode.hh (ACU_BaseDagNode): updated decl for 97 instantiateWithReplacement(); added decl for 98 instantiateWithCopies2() 99 100 * ACU_DagNode.cc (instantiateWithReplacement): rewritten to 101 respect eager positions 102 (instantiateWithCopies2): added 103 1042012-03-30 Steven Eker <eker@ape.csl.sri.com> 105 106 * ACU_Symbol.cc (termify): code cleaning 107 1082012-03-29 Steven Eker <eker@ape.csl.sri.com> 109 110 * ACU_Symbol.hh (AssociativeSymbol): added decl for termify() 111 112 * ACU_Term.hh (Term): added decl for new ctor 113 114 * ACU_Term.cc (ACU_Term): added version that takes multiplicities 115 116 * ACU_Symbol.cc (termify): added 117 118===================================Maude96=========================================== 119 1202011-11-22 Steven Eker <eker@rho> 121 122 * ACU_UnificationSubproblem2.cc (ACU_UnificationSubproblem2::solve): use restoreFromClone() 123 to make sure that sort and dagnode information for variable created on the branch we are 124 backtracking get purged from our UnificationContext object (4 places) 125 126===================================Maude95c=========================================== 127 1282010-12-09 Steven Eker <eker@rho> 129 130 * ACU_Symbol.cc (ACU_Symbol::postOpDeclarationPass): don't call 131 rightIdentitySortCheck() since we are commutative 132 133===================================Maude95b=========================================== 134 1352010-10-19 Steven Eker <eker@rho> 136 137 * ACU_Symbol.cc (ACU_Symbol::makeCanonicalCopyEagerUptoReduced): 138 becomes makeCanonicalCopy() 139 140 * ACU_Symbol.hh (class ACU_Symbol): 141 makeCanonicalCopyEagerUptoReduced() -> makeCanonicalCopy() 142 143===================================Maude95a=========================================== 144 1452010-09-29 Steven Eker <eker@rho> 146 147 * ACU_Symbol.cc (ACU_Symbol::makeCanonicalCopyEagerUptoReduced): 148 simplifed now that we only get unreduced nodes; use 149 getCanonicalCopyEagerUptoReduced(); fix bug where we were not 150 copying flags and sort 151 152 * ACU_Symbol.hh (class ACU_Symbol): added decl for 153 makeCanonicalCopyEagerUptoReduced() 154 155 * ACU_Symbol.cc (ACU_Symbol::makeCanonicalCopyEagerUptoReduced): 156 added 157 (ACU_Symbol::makeCanonical): removed commment out tree->array 158 conversion 159 1602010-09-23 Steven Eker <eker@rho> 161 162 * ACU_LazySubproblem.cc (ACU_LazySubproblem::bindCollector): fix 163 bug where we weren't handling the case where our collector 164 variable had become bound by our stripper automaton 165 166 * ACU_LhsAutomaton.cc (ACU_LhsAutomaton::complete): fixed out of 167 date comment 168 1692010-09-10 Steven Eker <eker@rho> 170 171 * ACU_UnificationSubproblem2.cc 172 (ACU_UnificationSubproblem2::solve): don't exclude the null 173 solution in the unequal identity collapse case 174 1752010-09-09 Steven Eker <eker@rho> 176 177 * ACU_UnificationSubproblem2.cc 178 (ACU_UnificationSubproblem2::solve): check 179 hasUnequalLeftIdentityCollapse() and force generation of 180 non-maximal solutions when it is true 181 1822010-08-18 Steven Eker <eker@rho> 183 184 * ACU_UnificationSubproblem2.cc 185 (ACU_UnificationSubproblem2::nextSelectionWithIdentity): deleted 186 commented out old verions 187 188 * ACU_DagNode.cc (ACU_DagNode::nonVariableSize): deleted 189 190 * ACU_DagNode.hh (class ACU_DagNode): deleted decl for 191 nonVariableSize() 192 193===================================Maude95=========================================== 194 1952010-08-11 Steven Eker <eker@rho> 196 197 * ACU_DagNode.cc (ACU_DagNode::computeSolvedForm2): handle 198 unification agaist bound variable by unifying against variables 199 binding to avoid nontermination 200 2012010-08-04 Steven Eker <eker@rho> 202 203 * ACU_UnificationSubproblem2.cc 204 (ACU_UnificationSubproblem2::buildSolution): handle <oldvar> =? d 205 the old way when the representative variable of <oldvar> is bound 206 to avoid generating problems of the same size as we solve 207 (ACU_UnificationSubproblem2::addUnification): handle variable rhs 208 even when we don't have an identity 209 2102010-08-03 Steven Eker <eker@rho> 211 212 * ACU_DagNode.cc (ACU_DagNode::computeSolvedForm2): rewritten to 213 push problems of the form f(...) = X on the pending stack rather 214 than pass them to VariableDagNode::computeSolvedForm2() 215 216 * ACU_UnificationSubproblem2.hh (class 217 ACU_UnificationSubproblem2): updated decl for addUnification() 218 219 * ACU_UnificationSubproblem2.cc 220 (ACU_UnificationSubproblem2::addUnification): handle marked 221 argument 222 2232010-07-29 Steven Eker <eker@rho> 224 225 * ACU_UnificationSubproblem2.hh (class 226 ACU_UnificationSubproblem2): updated decl for classify(); 227 deleleted decl for isRestrictedSubterm(); updated decl for 228 unsolve(); updated decl for setMultiplicity() 229 (class ACU_UnificationSubproblem2): deleted data member 230 restrictedSubterms; added data member markedSubterms 231 232 * ACU_UnificationSubproblem2.cc 233 (ACU_UnificationSubproblem2::addUnification): take solution as 234 argument 235 (ACU_UnificationSubproblem2::addUnification): simplified; keep set 236 of indices for marked subterms 237 (ACU_UnificationSubproblem2::setMultiplicity): use representative 238 variable in a chain; return subterm index 239 (ACU_UnificationSubproblem2::unsolve): simplified; never fail - we 240 let Diophantine solver worry about pathological X = f(..., X,...) 241 case 242 (ACU_UnificationSubproblem2::solve): simplified using new 243 unsolve() symantics 244 (ACU_UnificationSubproblem2::classify): simplified - no longer 245 chase variable chains as we should only have representative 246 variables in our system 247 (ACU_UnificationSubproblem2::isRestrictedSubterm): deleted 248 249 * ACU_UnificationSubproblem2.hh (class 250 ACU_UnificationSubproblem2): updated decl for addUnification() 251 2522010-07-21 Steven Eker <eker@rho> 253 254 * ACU_UnificationSubproblem2.cc 255 (ACU_UnificationSubproblem2::buildAndSolveDiophantineSystem): 256 comment out the case where with fail because we only have one 257 Diophantine variable since even with no basis elements we can 258 still get a unifier 259 2602010-07-20 Steven Eker <eker@rho> 261 262 * ACU_UnificationSubproblem2.hh (class 263 ACU_UnificationSubproblem2): added decl for isRestrictedSubterm 264 265 * ACU_UnificationSubproblem2.cc 266 (ACU_UnificationSubproblem2::classify): use equal() rather than == 267 for checking for restricted subterms 268 (ACU_UnificationSubproblem2::isRestrictedSubterm): added 269 (ACU_UnificationSubproblem2::classify): rewritten using 270 isRestrictedSubterm() to ensure that variables can be restricted 271 2722010-07-19 Steven Eker <eker@rho> 273 274 * ACU_UnificationSubproblem2.cc 275 (ACU_UnificationSubproblem2::markReachableNodes): fix bug where we 276 were deleting maximalSelections here rather than in 277 ~ACU_UnificationSubproblem2() 278 2792010-07-09 Steven Eker <eker@rho> 280 281 * ACU_UnificationSubproblem2.cc 282 (ACU_UnificationSubproblem2::buildSolution): add an Assert to 283 detect trivial bounds violation 284 (ACU_UnificationSubproblem2::computeLegalSelections): use index 285 member of basis element rather than separately maintained index 286 which is incorrect 287 2882010-07-08 Steven Eker <eker@rho> 289 290 * ACU_UnificationSubproblem2.cc 291 (ACU_UnificationSubproblem2::solve): set maximalSelections 292 (ACU_UnificationSubproblem2::ACU_UnificationSubproblem2): clear 293 maximalSelections 294 295 * ACU_UnificationSubproblem2.hh (class 296 ACU_UnificationSubproblem2): added data member maximalSelections 297 298 * ACU_UnificationSubproblem2.cc 299 (ACU_UnificationSubproblem2::addUnification): use hasIdentity() 300 (ACU_UnificationSubproblem2::unsolve): use hasIdentity() 301 (ACU_UnificationSubproblem2::solve): use hasIdentity() 302 303 * ACU_DagNode.cc (ACU_DagNode::computeBaseSortForGroundSubterms): 304 removed commented out code 305 3062010-07-07 Steven Eker <eker@rho> 307 308 * ACU_UnificationSubproblem2.hh (class 309 ACU_UnificationSubproblem2): added decl for 310 computeLegalSelections() 311 312===================================Maude94a=========================================== 313 3142010-06-29 Steven Eker <eker@rho> 315 316 * ACU_Symbol.cc (ACU_Symbol::canResolveTheoryClash): added 317 318 * ACU_DagNode.cc (ACU_DagNode::computeSolvedForm2): try using 319 resolveTheoryClash() 320 3212010-06-25 Steven Eker <eker@rho> 322 323 * ACU_UnificationSubproblem2.cc 324 (ACU_UnificationSubproblem2::addUnification): handle the theory 325 clash case where the rhs is actually our identity 326 327 * ACU_DagNode.cc (ACU_DagNode::computeSolvedForm2): quick hack to 328 handle theory clashes asymetrically 329 330 * ACU_UnificationSubproblem2.hh (class 331 ACU_UnificationSubproblem2): added data member restrictedSubterms 332 333 * ACU_UnificationSubproblem2.cc 334 (ACU_UnificationSubproblem2::unsolve): handle X = f(..., X, ...) 335 case where collapse might be possible 336 (ACU_UnificationSubproblem2::addUnification): rewritten to handle 337 theory clash unifications 338 (ACU_UnificationSubproblem2::classify): handle restricted subterms 339 3402010-06-24 Steven Eker <eker@rho> 341 342 * ACU_UnificationSubproblem2.cc 343 (ACU_UnificationSubproblem2::buildAndSolveDiophantineSystem): 344 given each basis element a unique index 345 346 * ACU_UnificationSubproblem2.hh (class 347 ACU_UnificationSubproblem2): added index field to struct Entry 348 349 * ACU_UnificationSubproblem2.cc 350 (ACU_UnificationSubproblem2::nextSelectionWithIdentity): avoid 351 generating subsets of previous selections 352 353 * ACU_UnificationSubproblem2.hh (class 354 ACU_UnificationSubproblem2): added data member old 355 (class ACU_UnificationSubproblem2): added NatSetList typedef 356 (class ACU_UnificationSubproblem2): added date member selectionSet 357 358 * ACU_UnificationSubproblem2.cc 359 (ACU_UnificationSubproblem2::buildAndSolveDiophantineSystem): 360 change criteria for failing due to lack of coverage 361 362 * ACU_UnificationSubproblem2.hh (class 363 ACU_UnificationSubproblem2): added data member needToCover 364 365 * ACU_UnificationSubproblem2.cc: fill out needToCover 366 367 * ACU_UnificationSubproblem2.hh (class 368 ACU_UnificationSubproblem2): added decl for 369 nextSelectionWithIdentity() 370 371 * ACU_UnificationSubproblem2.cc 372 (ACU_UnificationSubproblem2::buildSolution): handle null 373 assignments by using getIdentityDag() 374 (ACU_UnificationSubproblem2::nextSelectionWithIdentity): added 375 (ACU_UnificationSubproblem2::solve): use 376 nextSelectionWithIdentity() in identity case 377 3782010-06-23 Steven Eker <eker@rho> 379 380 * ACU_UnificationSubproblem2.hh (class 381 ACU_UnificationSubproblem2): update decl for classify() 382 383 * ACU_UnificationSubproblem2.cc 384 (ACU_UnificationSubproblem2::classify): fixed bug where we were 385 not checking for unbound variable 386 (ACU_UnificationSubproblem2::classify): fixed bug where we assume 387 we could treat our own top symbol as a stable symbol, even though 388 in any combination of basis elements it could take multiple things 389 and not be forced to unify against a single specific thing 390 (ACU_UnificationSubproblem2::classify): pass canTakeIdentity flag 391 rather than needToCover flag; fix bug where we could have left 392 needToCover false even when there was no identity 393 (ACU_UnificationSubproblem2::buildAndSolveDiophantineSystem): use 394 new classify() semantics 395 3962010-06-22 Steven Eker <eker@rho> 397 398 * ACU_UnificationSubproblem2.cc 399 (ACU_UnificationSubproblem2::buildAndSolveDiophantineSystem): 400 rewritten using classify() to fix bug in basis element killing 401 code 402 403 * ACU_UnificationSubproblem2.hh (class 404 ACU_UnificationSubproblem2): added decl for classify() 405 406 * ACU_UnificationSubproblem2.cc 407 (ACU_UnificationSubproblem2::classify): added 408 4092010-06-07 Steven Eker <eker@rho> 410 411 * ACU_UnificationSubproblem2.cc 412 (ACU_UnificationSubproblem2::buildAndSolveDiophantineSystem): 413 added code to exclude basis elements that force unresolvable 414 theory clashes 415 4162010-05-21 Steven Eker <eker@rho> 417 418 * ACU_DagNode.cc (ACU_DagNode::computeBaseSortForGroundSubterms): 419 hack to allow unification to proceed on non-ground ACU dags 420 421===================================Maude94=========================================== 422 4232010-04-16 Steven Eker <eker@rho> 424 425 * ACU_LhsCompiler1.cc (ACU_Term::analyseConstraintPropagation): 426 code cleaning 427 4282010-04-15 Steven Eker <eker@rho> 429 430 * ACU_LhsCompiler2.cc 431 (ACU_Term::findConstraintPropagationSequence): minor code cleaning 432 4332010-04-14 Steven Eker <eker@rho> 434 435 * ACU_LhsCompiler2.cc 436 (ACU_Term::findConstraintPropagationSequence): amongst sequences 437 that bind uniquely the same number of variables, perfer the longer 438 sequence 439 440 * ACU_Term.hh (class ACU_Term): deleted decl for 441 addIndependentAliens() 442 443 * ACU_LhsCompiler2.cc (ACU_Term::compileAliensOnlyCase): code 444 cleaning 445 (ACU_Term::findConstraintPropagationSequence): rewritten to avoid 446 exponential blow up in more cases. 447 (ACU_Term::findConstraintPropagationSequence): allow current 448 forceable NGA to be pruned if we've already explored a path and 449 there is nothing to be gained by matching it now 450 (ACU_Term::compileAliensOnlyCase): don't call 451 addIndependentAliens() since we assume best sequence will already 452 contain all forceable NGAs 453 (ACU_Term::addIndependentAliens): deleted 454 455===================================Maude93a=========================================== 456 4572010-03-12 Steven Eker <eker@rho> 458 459 * ACU_RhsAutomaton.cc (ACU_RhsAutomaton::buildArguments): use 460 nrArguments 461 462 * ACU_Term.cc (ACU_Term::compileRhs2): rewritten to compile/build 463 larger subterms first, to avoid quadratic conflict arcs on clt's 464 example 465 466 * ACU_RhsAutomaton.cc (ACU_RhsAutomaton::close): set nrArguments 467 (ACU_RhsAutomaton::construct, ACU_RhsAutomaton::replace): use 468 nrArguments rather than arguments.size() to avoid checking for a 469 null Vector 470 471 * ACU_RhsAutomaton.hh (class ACU_RhsAutomaton): added date element 472 nrArguments 473 474===================================Maude93=========================================== 475 4762010-02-26 Steven Eker <eker@rho> 477 478 * ACU_DagOperations.cc (ACU_DagNode::binarySearch): removed 479 setOnLs()/setOnGeq() since it seems to be a pessimization (both 480 versions) 481 4822010-02-24 Steven Eker <eker@rho> 483 484 * ACU_Normalize.cc (ACU_DagNode::copyAndBinaryInsert): use new 485 binarySearch() convention 486 4872010-02-19 Steven Eker <eker@rho> 488 489 * ACU_DagNode.hh (class ACU_DagNode): updated decl for DagNode* 490 version of binarySearch() 491 492 * ACU_DagOperations.cc (ACU_DagNode::binarySearch): rewrote 493 DagNode* version 494 (ACU_DagNode::eliminateSubject): use new binarySearch() convention 495 496 * ACU_DagNode.hh (class ACU_DagNode): updated decl for Term* 497 version of binarySearch() 498 499 * ACU_GndLhsAutomaton.cc (ACU_GndLhsAutomaton::match): use new 500 binarySearch() convention 501 502 * ACU_Matcher.cc (ACU_LhsAutomaton::eliminateGroundAliens): use 503 new binarySearch() convention 504 505 * ACU_DagOperations.cc (ACU_DagNode::binarySearch): rewritten to 506 return position rather than pass it back through a reference argument 507 (ACU_DagNode::eliminateArgument): use new binarySearch semantics 508 5092010-02-18 Steven Eker <eker@rho> 510 511 * ACU_DagOperations.cc (ACU_DagNode::binarySearch): use unsigned 512 sum optimization in both versions 513 5142010-01-06 Steven Eker <eker@goo.csl.sri.com> 515 516 * ACU_Term.cc (compileRhs2): experiment code to check my 517 understanding of clt's extreme right nesting example 518 519===================================Maude92c=========================================== 520 5212009-12-09 Steven Eker <eker@goo.csl.sri.com> 522 523 * ACU_TreeDagNode.cc (makeCanonical): added 524 525 * ACU_Symbol.cc (makeCanonical): use 526 ACU_TreeDagNode::makeCanonical() 527 5282009-12-03 Steven Eker <eker@goo.csl.sri.com> 529 530 * ACU_Symbol.hh (class ACU_Symbol): added decl for makeCanonical() 531 532 * ACU_TreeDagNode.hh (class ACU_TreeDagNode): make ACU_Symbol a 533 friend 534 535 * ACU_Symbol.cc (makeCanonical): added 536 537===================================Maude92b=========================================== 538 5392008-12-22 Steven Eker <eker@goo.csl.sri.com> 540 541 * ACU_Symbol.cc (computeGeneralizedSort): new getSortFunction() 542 convention 543 5442008-12-19 Steven Eker <eker@goo.csl.sri.com> 545 546 * ACU_Subproblem.hh: derive from DelayedSubproblem 547 548===================================Maude92=========================================== 549 5502008-09-24 Steven Eker <eker@goo.csl.sri.com> 551 552 * ACU_Matcher.cc (fullMatch): fix bug where we weren't setting up 553 the extensionInfo in the new fast success case 554 5552008-09-23 Steven Eker <eker@goo.csl.sri.com> 556 557 * ACU_Matcher.cc (fullMatch): catch the case where we have no 558 patterns, one variable that can't take identity, one subject and 559 extension 560 (fullMatch): catch the same case where we can take identity but 561 we're not allowed to since there were only two things in the 562 subject 563 564===================================Maude91c=========================================== 565 5662008-09-11 Steven Eker <eker@goo.csl.sri.com> 567 568 * ACU_DagNode.cc (computeBaseSortForGroundSubterms): added default 569 case to avoid compiler warning 570 5712008-05-08 Steven Eker <eker@goo.csl.sri.com> 572 573 * ACU_UnificationSubproblem2.cc (buildAndSolveDiophantineSystem): 574 use IntSystem rather than MpzSystem 575 (buildAndSolveDiophantineSystem): use new IntSystem semantics to 576 avoid making a zero padded copy of each equation 577 578===================================Maude91a=========================================== 579 5802008-04-18 Steven Eker <eker@goo.csl.sri.com> 581 582 * ACU_Symbol.hh (class ACU_Symbol): added decl for unificationPriority() 583 584 * ACU_Symbol.cc (unificationPriority): added 585 586===================================Maude91=========================================== 587 5882008-03-23 Steven Eker <eker@goo.csl.sri.com> 589 590 * ACU_DagNode.hh (class ACU_DagNode): ACU_UnificationSubproblem, 591 ACU_UnificationWithExtensionSubproblem no longer friends 592 593 * ACU_UnificationWithExtensionSubproblem.cc: deleted 594 595 * ACU_UnificationWithExtensionSubproblem.hh: deleted 596 597 * ACU_UnificationWithExtensionSubproblem.cc: deleted 598 599 * ACU_UnificationWithExtensionSubproblem.hh: deleted 600 601 * ACU_Theory.hh: removed classes ACU_UnificationSubproblem, 602 ACU_UnificationWithUnificationSubproblem 603 604 * ACU_DagNode.hh (class ACU_DagNode): deleted commented out decl 605 for old version of computeSolvedForm2() 606 607 * ACU_DagNode.cc (computeSolvedForm2): deleted commented out old 608 version 609 610===================================Maude90a=========================================== 611 6122008-02-08 Steven Eker <eker@goo.csl.sri.com> 613 614 * ACU_UnificationSubproblem2.hh (class 615 ACU_UnificationSubproblem2): added date member 616 preSolveSubstitution; added decl for unsolve() 617 618 * ACU_UnificationSubproblem2.cc (solve): unsolve solved forms in 619 our theory 620 (unsolve): added 621 622 * ACU_DagNode.cc (computeSolvedForm2): Substitution -> 623 UnificationContext 624 625 * ACU_DagNode.hh (class ACU_DagNode): updated decl for 626 computeSolvedForm2() 627 6282008-02-05 Steven Eker <eker@goo.csl.sri.com> 629 630 * ACU_Symbol.cc (makeUnificationSubproblem): added 631 632 * ACU_Symbol.hh (class ACU_Symbol): added decl for 633 makeUnificationSubproblem() 634 635 * ACU_DagNode.hh (class ACU_DagNode): updated decl for computeSolvedForm2() 636 637 * ACU_DagNode.cc (computeSolvedForm2): rewritten 638 6392008-02-04 Steven Eker <eker@goo.csl.sri.com> 640 641 * ACU_UnificationSubproblem2.cc: created 642 643 * ACU_UnificationSubproblem2.hh: created 644 6452008-01-17 Steven Eker <eker@goo.csl.sri.com> 646 647 * ACU_UnificationSubproblem.cc (ACU_UnificationSubproblem): 648 initialize savedSubstitution with 0 entries rather than with a 649 single entry (that will end up being marked in GC) 650 651===================================Maude90=========================================== 652 6532007-11-20 Steven Eker <eker@goo.csl.sri.com> 654 655 * ACU_UnificationSubproblem.cc (ACU_UnificationSubproblem): 656 savedSubstitution needs to be at least size 1 in new Substitution 657 handling 658 (unificationSolve): fix bug by using clone() to restore old 659 substitution 660 6612007-11-07 Steven Eker <eker@goo.csl.sri.com> 662 663 * ACU_TreeDagNode.cc (indexVariables2): added 664 665 * ACU_TreeDagNode.hh (class ACU_TreeDagNode): added decl for 666 indexVariables2() 667 6682007-11-05 Steven Eker <eker@goo.csl.sri.com> 669 670 * ACU_DagNode.cc (indexVariables2, instantiateWithReplacement): added 671 (instantiate2): use isGround() rather than checking for an unknown 672 sort 673 (instantiate2): call setGround() 674 675 * ACU_DagNode.hh (class ACU_DagNode): added decl for 676 indexVariables2() and instantiateWithReplacement() 677 6782007-11-01 Steven Eker <eker@goo.csl.sri.com> 679 680 * ACU_DagNode.cc (instantiate2): updated 681 682 * ACU_DagNode.hh (class ACU_DagNode): updated decl for 683 instantiate2() 684 6852007-09-28 Steven Eker <eker@goo.csl.sri.com> 686 687 * ACU_UnificationSubproblem.cc (unificationSolve): replaced two 688 clone() calls with copy() calls since when we copy back a saved 689 substitution, both substitutions should have the same copy size 690 691===================================Maude89h=========================================== 692 6932007-08-24 Steven Eker <eker@goo.csl.sri.com> 694 695 * ACU_DagNode.cc (computeBaseSortForGroundSubterms): rewritten 696 697 * ACU_DagNode.hh (class ACU_DagNode): updated decl for 698 computeBaseSortForGroundSubterms() 699 700 * ACU_UnificationSubproblem.cc (unificationSolve): added comments 701 to indicate that fresh variables are deallocated when done with 702 7032007-08-23 Steven Eker <eker@goo.csl.sri.com> 704 705 * ACU_UnificationSubproblem.cc (buildSolution): use 706 sortAndUniquize() in place of dumbNormalizeAtTop() 707 708 * ACU_DagNode.cc (computeSolvedForm): becomes computeSolvedForm2() 709 710 * ACU_DagNode.hh (class ACU_DagNode): computeSolvedForm() -> 711 computeSolvedForm2() 712 7132007-08-21 Steven Eker <eker@goo.csl.sri.com> 714 715 * ACU_UnificationSubproblem.cc (initialize): simplify and comment 716 (initialize): fix nasty bug by clearing previous selections 717 7182007-08-17 Steven Eker <eker@goo.csl.sri.com> 719 720 * ACU_UnificationSubproblem.hh (class ACU_UnificationSubproblem): 721 update decl for addBasisElement() 722 723 * ACU_UnificationSubproblem.cc (addBasisElement): pass element by 724 reference; made assignment in if statement obvious 725 726===================================Maude89g=========================================== 727 7282007-08-09 Steven Eker <eker@goo.csl.sri.com> 729 730 * ACU_DagNode.hh (class ACU_DagNode): added decl for 731 dumbNormalizeAtTop() 732 733 * ACU_DagNode.cc (instantiate2): use dumbNormalizeAtTop() to avoid 734 getting a tree form 735 736 * ACU_UnificationSubproblem.cc (buildSolution): use 737 dumbNormalizeAtTop() to avoid getting a tree form 738 739 * ACU_Normalize.cc (dumbNormalizeAtTop): added 740 (normalizeAtTop): use dumbNormalizeAtTop() for general case 741 742 * ACU_UnificationSubproblem.cc (buildSolution): added Assert() to 743 protect against getting a tree form from normalizeAtTop() 744 745===================================Maude89f=========================================== 746 7472007-07-06 Steven Eker <eker@goo.csl.sri.com> 748 749 * ACU_DagNode.cc (computeSolvedForm): use 750 ACU_UnificationWithExtensionSubproblem() 751 752 * ACU_Theory.hh: added ACU_UnificationWithUnificationSubproblem 753 7542007-06-29 Steven Eker <eker@goo.csl.sri.com> 755 756 * ACU_UnificationWithExtensionSubproblem.cc (generateUnificationSubproblem) 757 (fillOutExtensionInfo, nextSelection): added 758 7592007-06-28 Steven Eker <eker@goo.csl.sri.com> 760 761 * ACU_UnificationWithExtensionSubproblem.cc: created 762 763 * ACU_UnificationWithExtensionSubproblem.hh: created 764 765 * ACU_DagNode.hh (class ACU_DagNode): updated decl for 766 computeSolvedForm() 767 768 * ACU_DagNode.cc (computeSolvedForm): added extensionInfo arg 769 770===================================Maude89c=========================================== 771 7722007-03-16 Steven Eker <eker@goo.csl.sri.com> 773 774 * ACU_Symbol.cc (computeGeneralizedSort): reuse bddPair between 775 iterations 776 7772007-03-15 Steven Eker <eker@goo.csl.sri.com> 778 779 * ACU_Symbol.cc (computeGeneralizedSort): pass realToBdd by ref 780 781 * ACU_Symbol.hh (class ACU_Symbol): fix decl for 782 computeGeneralizedSort() 783 784===================================Maude89a=========================================== 785 7862007-03-14 Steven Eker <eker@goo.csl.sri.com> 787 788 * ACU_UnificationSubproblem.hh (class ACU_UnificationSubproblem): 789 added decl for markReachableNodes() 790 791 * ACU_UnificationSubproblem.cc (markReachableNodes): added 792 793 * ACU_UnificationSubproblem.hh (class ACU_UnificationSubproblem): 794 derive from SimpleRootContainer 795 796 * ACU_UnificationSubproblem.cc (ACU_UnificationSubproblem): 797 initialize savedSubstitution 798 (unificationSolve): don't call deallocateFreshVariables(); restore 799 original substitution after we're done with selection 800 8012007-03-13 Steven Eker <eker@goo.csl.sri.com> 802 803 * ACU_Symbol.cc (computeGeneralizedSort): added 804 805 * ACU_Symbol.hh (class ACU_Symbol): added decl for 806 computeGeneralizedSort() 807 808 * ACU_DagNode.hh (class ACU_DagNode): added decl for 809 instantiate2() 810 811 * ACU_DagNode.cc (instantiate2): added 812 813 * ACU_UnificationSubproblem.cc (unificationSolve): keep a copy of 814 the solution and restore is each time we give up on the current 815 basis selection 816 817 * ACU_UnificationSubproblem.hh (class ACU_UnificationSubproblem): 818 added data member savedSubstitution 819 820 * ACU_UnificationSubproblem.cc (buildSolution): added 821 (unificationSolve): fix bug that we were clearing selection that 822 we needed for backtracking 823 824 * ACU_UnificationSubproblem.hh (class ACU_UnificationSubproblem): 825 added decl for buildSolution() 826 827 * ACU_DagNode.hh (class ACU_DagNode): ACU_UnificationSubproblem 828 becomes a friend 829 830 * ACU_Theory.hh: added class ACU_UnificationSubproblem 831 8322007-03-12 Steven Eker <eker@goo.csl.sri.com> 833 834 * ACU_DagNode.cc (computeSolvedForm): use coverable() check 835 836 * ACU_UnificationSubproblem.cc (coverable): added 837 838 * ACU_DagNode.cc (computeSolvedForm): use 839 ACU_UnificationSubproblem 840 841 * ACU_UnificationSubproblem.cc: created 842 843 * ACU_UnificationSubproblem.hh: created 844 8452007-03-09 Steven Eker <eker@goo.csl.sri.com> 846 847 * ACU_DagNode.cc (computeBaseSortForGroundSubterms): added 848 (computeSolvedForm): take car of upper bounds 849 850 * ACU_DagNode.hh (class ACU_DagNode): added decl for 851 computeBaseSortForGroundSubterms() 852 853 * ACU_DagNode.cc (nonVariableSize): added 854 (insertVariables2): added 855 (computeSolvedForm): added stub 856 857 * ACU_DagNode.hh (class ACU_DagNode): added decls for 858 computeSolvedForm(), nonVariableSize(), insertVariables2() 859 860===================================Maude89=========================================== 861 8622006-10-10 Steven Eker <eker@goo.csl.sri.com> 863 864 * ACU_DagNode.hh: added declaration for getACU_DagNode() to 865 appease gcc 4.1 866 867===================================Maude88b=========================================== 868 8692005-10-06 Steven Eker <eker@goo.csl.sri.com> 870 871 * ACU_Term.cc (deepCopy2): fix bug where we were testing s rather 872 than s2 for 0 873 874===================================Maude86c=========================================== 875 8762005-07-28 Steven Eker <eker@goo.csl.sri.com> 877 878 * ACU_Term.hh (class ACU_Term): updated decl for SymbolMap* 879 version of ctor 880 881 * ACU_Term.cc (deepCopy2): handle translation to a non-ACU_Symbol 882 (ACU_Term): force symbol arg to be a ACU_Symbol* 883 8842005-07-01 Steven Eker <eker@goo.csl.sri.com> 885 886 * ACU_Term.hh (class ACU_Term): updated decls for deepCopy2() and 887 SymbolMap* version of ctor 888 889 * ACU_Term.cc (deepCopy2): rewritten 890 (ACU_Term): (SymbolMap* version) rewritten 891 892===================================Maude86b=========================================== 893 8942003-08-28 Steven Eker <eker@goo.csl.sri.com> 895 896 * ACU_Symbol.hh (class ACU_Symbol): added decl for 897 rewriteAtTopNoOwise() 898 899 * ACU_Symbol.cc (complexStrategy): rewritten to use 900 rewriteAtTopNoOwise() for first 0 in semi-eager case 901 (memoStrategy): ditto 902 (rewriteAtTopNoOwise): added 903 904===================================Maude82=========================================== 905 9062003-07-31 Steven Eker <eker@goo.csl.sri.com> 907 908 * ACU_LazySubproblem.cc (bindCollector): fixed nasty bug where we 909 were binding local rather than solution 910 (solve): need to retract() after a successful assert() followed by 911 subproblem failure (2 places) 912 913===================================Maude81=========================================== 914 9152003-05-29 Steven Eker <eker@goo.csl.sri.com> 916 917 * ACU_TreeMatcher.cc (treeMatch): added extra Assert()s for FULL case 918 919 * ACU_LhsAutomaton.cc (addTopVariable): update nrExpectedUnboundVariables 920 (ACU_LhsAutomaton): clear nrExpectedUnboundVariables 921 (addTopVariable): fix bug where we were not checking that 922 multiplicity == 1 in order to set collectorSeen 923 924 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): data member 925 nrExpectedUnboundVariables 926 927 * ACU_LhsAutomaton.cc (complete): fix bug where we weren't 928 checking that single nga had multiplicity 1 before enabling 929 treeMatchOK in FULL case 930 931 * ACU_TreeMatcher.cc (treeMatch): check for only 1 thing left in 932 FULL case 933 934 * ACU_LazySubproblem.cc (ACU_LazySubproblem): call ctors for 935 matchTime and local 936 (bindCollector): use checkSort() 937 (bindCollector): added Assert() for empty tree 938 939 * ACU_LhsAutomaton.cc (complete): allow the use of tree matching 940 in some FULL cases 941 942 * ACU_LazySubproblem.cc (bindCollector): simplified as 943 collectorSort will never be 0 944 945 * ACU_TreeMatcher.cc (treeMatch): use ACU_LazySubproblem() 946 947 * ACU_LazySubproblem.hh (class ACU_LazySubproblem): added decl for 948 bindCollector() 949 (class ACU_LazySubproblem): replaced topSymbol with subject; 950 updated decls for bindCollector() and ctor 951 952 * ACU_LazySubproblem.cc (ACU_LazySubproblem): init topSymbol 953 954 * ACU_LazySubproblem.hh (class ACU_LazySubproblem): added data 955 member topSymbol; updated decl for ctor 956 957 * ACU_LazySubproblem.cc (ACU_LazySubproblem): remaining arg is now 958 a const ACU_Tree&; use copy() to initialize matchTime 959 (bindCollector): added 960 961 * ACU_LazySubproblem.hh (class ACU_LazySubproblem): data member 962 remaining becomes ACU_Tree; updated decl for ctor 963 9642003-05-19 Steven Eker <eker@goo.csl.sri.com> 965 966 * ACU_Normalize.cc (normalizeAtTop): use useTree() 967 (insertAlien): use useTree() 968 969 * ACU_Symbol.hh (class ACU_Symbol): updated decl for ACU_Symbol() 970 (useTree): added 971 972 * ACU_Symbol.cc (ACU_Symbol): initialize useTreeFlag 973 974 * ACU_Symbol.hh (class ACU_Symbol): added data member useTreeFlag 975 9762003-05-16 Steven Eker <eker@goo.csl.sri.com> 977 978 * ACU_Symbol.cc (stackArguments): rewritten; handle tree case; use 979 FOR_EACH_CONST() in ArgVec case 980 (ruleRewrite): use ruleFree(); don't use getACU_DagNode() 981 9822003-05-15 Steven Eker <eker@goo.csl.sri.com> 983 984 * ACU_Symbol.cc (reduceArgumentsAndNormalize): rewritten; now 985 return true for collapse and false owise 986 987 * ACU_Symbol.hh (class ACU_Symbol): added decls for normalize() 988 and copyReduceSubtermsAndNormalize() 989 990 * ACU_Symbol.cc (memoStrategy): rewritten 991 (normalize): added 992 (complexStrategy): simplified using normalize() 993 (memoStrategy): simplified using normalize() 994 (normalizeAndComputeTrueSort): simplified using normalize() 995 (copyAndReduceSubterms): rewritten 996 (copyAndReduceSubterms): becomes copyReduceSubtermsAndNormalize() 997 (memoStrategy): simplified using copyReduceSubtermsAndNormalize() 998 (complexStrategy): simplified using 999 copyReduceSubtermsAndNormalize() 1000 1001 * ACU_TreeDagNode.cc (treeToArgVec): pass ASSIGNMENT to 1002 ACU_DagNode() 1003 1004 * ACU_Symbol.cc (reduceArgumentsAndNormalize): use isFresh() 1005 (eqRewrite): use isFresh() 1006 (complexStrategy): use isFresh() 1007 (memoStrategy): use isFresh() (2 places) 1008 (normalizeAndComputeTrueSort): rewritten; only call 1009 computeTrueSort() on args and normalize if our normalization 1010 status is FRESH 1011 1012 * ACU_BaseDagNode.hh (isFresh): added 1013 1014 * ACU_Symbol.cc (computeBaseSort): use isTree() 1015 10162003-05-14 Steven Eker <eker@goo.csl.sri.com> 1017 1018 * ACU_ExtensionInfo.hh (useUnmatched): deleted 1019 (class ACU_ExtensionInfo): deleted decls for convertToUnmatched(0 1020 and useUnmatched() 1021 1022 * ACU_ExtensionInfo.cc (buildMatchedPortion): rewritten using 1023 iterators 1024 (convertToUnmatched): deleted 1025 1026 * ACU_DagNode.cc (partialReplace): need to set normalization 1027 status to FRESH 1028 1029 * ACU_TreeMatcher.cc (makeHighMultiplicityAssignment): use new 1030 ACU_DagNode() convention 1031 (tryToBindLastVariable): use new ACU_DagNode() convention 1032 (forcedLoneVariableCase): use new ACU_DagNode() convention 1033 1034 * ACU_Subproblem.cc (oneVariableCase): use new ACU_DagNode() 1035 convention 1036 (computeAssignment): use new ACU_DagNode() convention 1037 (solveVariables): don't call setNormalizationStatus() 1038 1039 * ACU_NonLinearLhsAutomaton.cc (match): use new ACU_DagNode() 1040 convention 1041 1042 * ACU_Matcher.cc (forcedLoneVariableCase): use new ACU_DagNode() 1043 convention 1044 1045 * ACU_ExtensionInfo.cc (buildUnmatchedPortion): use new 1046 ACU_DagNode() convention 1047 1048 * ACU_GreedyMatcher.cc (greedyPureMatch): use new ACU_DagNode() 1049 convention 1050 1051 * ACU_CollectorLhsAutomaton.cc (collect): use new ACU_DagNode() 1052 convention 1053 1054 * ACU_DagNode.hh (ACU_DagNode): take NormalizationStatus arg 1055 1056 * ACU_ExtensionInfo.cc (buildUnmatchedPortion): rewritten to 1057 handle tree case and use iterators 1058 1059 * ACU_ExtensionInfo.hh (getUnmatched): deleted 1060 1061 * ACU_MergeSort.cc (flattenSortAndUniquize): moved here 1062 1063 * ACU_Normalize.cc (copyAndBinaryInsert): moved here 1064 1065 * ACU_DagNode.hh (class ACU_DagNode): deleted decls for 1066 extensionNormalizeAtTop() and binaryInsert() 1067 1068 * ACU_DagNormalization.cc (extensionNormalizeAtTop): deleted 1069 (binaryInsert): deleted 1070 1071 * ACU_Symbol.cc (reduceArgumentsAndNormalize): removed EXTENSION 1072 case 1073 (complexStrategy): test for ACU_BaseDagNode::FRESH 1074 (memoStrategy): removed EXTENSION case 1075 1076 * ACU_BaseDagNode.hh (class ACU_BaseDagNode): deleted EXTENSION 1077 from enum NormalizationStatus 1078 1079 * ACU_DagNode.cc (partialReplace): simplified using 1080 buildUnmatchedPortion(); don't use EXTENSION normalization status 1081 (partialConstruct): simplified using buildUnmatchedPortion() 1082 1083 * ACU_ExtensionInfo.hh (class ACU_ExtensionInfo): added decl for 1084 buildUnmatchedPortion() 1085 1086 * ACU_ExtensionInfo.cc (buildUnmatchedPortion): added 1087 10882003-05-13 Steven Eker <eker@goo.csl.sri.com> 1089 1090 * ACU_TreeDagNode.cc (copyEagerUptoReduced2): avoid treeToArgVec() 1091 in the case that our symbol is not eager 1092 (clearCopyPointers2): changed CantHappen() to Assert() now that we 1093 handle non-eager copies ourself 1094 1095 * ACU_DagNode.cc (clearCopyPointers2): only need to clear copy 1096 pointer if we're eager - lazy argumnets don't get copied 1097 10982003-05-12 Steven Eker <eker@goo.csl.sri.com> 1099 1100 * ACU_Symbol.cc (eqRewrite): simplified 1101 (complexStrategy): rewritten to avoid converting from tree to 1102 argvec form unless we need to evaluate aour args 1103 1104 * ACU_TreeDagNode.cc (getHashValue): cache hash value 1105 1106 * ACU_TreeDagNode.hh (class ACU_TreeDagNode): deleted decl for 1107 treeComputeBaseSort() 1108 (class ACU_TreeDagNode): added data member hashCache 1109 1110 * ACU_TreeDagNode.cc (treeComputeBaseSort): deleted 1111 1112 * ACU_Symbol.cc (computeBaseSort): use ACU_Tree::computeBaseSort() 1113 1114 * ACU_TreeMatcher.cc (tryToBindLastVariable): use 1115 ACU_Tree::computeBaseSort() 1116 1117 * ACU_CollectorLhsAutomaton.cc (collect): (ACU_Tree version) 1118 simplified 1119 1120 * ACU_LhsAutomaton.cc (complete): removed SAT_MULT test and 1121 comment 1122 1123 * ACU_LhsCompiler0.cc (tryToMakeNonLinearLhsAutomaton): removed 1124 SAT_MULT test and comment 1125 1126 * ACU_NonLinearLhsAutomaton.cc (ACU_NonLinearLhsAutomaton): 1127 removed SAT_MULT part of Assert() 1128 1129 * ACU_TreeMatcher.cc (treeMatch): deleted SAT_MULT Assert() 1130 11312003-05-06 Steven Eker <eker@goo.csl.sri.com> 1132 1133 * ACU_DagOperations.cc (findFirstPotentialMatch): use 1134 Term::UNKNOWN 1135 11362003-05-05 Steven Eker <eker@goo.csl.sri.com> 1137 1138 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): redBlackMatch() -> 1139 treeMatch() 1140 1141 * ACU_TreeMatcher.cc (redBlackMatch): becomes treeMatch() 1142 1143 * ACU_Matcher.cc (match): redBlackOK -> treeMatchOK, 1144 redBlackMatch() -> treeMatch() 1145 1146 * ACU_LhsAutomaton.cc: redBlackOK -> treeMatchOK 1147 1148 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): redBlackOK -> 1149 treeMatchOK 1150 1151 * ACU_TreeMatcher.cc: remamed from ACU_RedBlackMatcher.cc 1152 1153 * ACU_RedBlackMatcher.cc (eliminateBoundVariables): use deleteMult() 1154 (makeHighMultiplicityAssignment): use class ACU_Tree 1155 (redBlackMatch): use getTree() 1156 (eliminateGroundAliens): use deleteMult() 1157 (eliminateGroundedOutAliens): use deleteMult() 1158 (greedyMatch): use deleteMult() 1159 (tryToBindVariable): use deleteMult() 1160 (tryToBindLastVariable): use deleteMult() 1161 (eliminateBoundVariables): use ACU_Tree::find() 1162 (eliminateGroundAliens): use ACU_Tree::find() 1163 (eliminateGroundedOutAliens): use 1164 ACU_Tree::findFirstPotentialMatch() 1165 (greedyMatch): use ACU_Tree::findFirstPotentialMatch() 1166 (tryToBindVariable): use ACU_Tree::findGeqMult() 1167 (tryToBindLastVariable): use getSoleDagNode() 1168 1169 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): current becomes an 1170 ACU_Tree 1171 1172 * ACU_GndLhsAutomaton.cc (match): use getTree() 1173 1174 * ACU_ExtensionInfo.cc (convertToUnmatched): use getTree() 1175 1176 * ACU_Term.cc (compareArguments): use getTree() 1177 1178 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): updated decl for 1179 makeHighMultiplicityAssignment() 1180 1181 * ACU_NGA_LhsAutomaton.cc (match): use getTree() 1182 1183 * ACU_NonLinearLhsAutomaton.cc (match): use getTree() 1184 1185 * ACU_VarLhsAutomaton.cc (match): use getTree() 1186 1187 * ACU_Flatten.cc (flattenSortAndUniquize): use getTree() 1188 1189 * ACU_Normalize.cc (normalizeAtTop): use class ACU_Tree 1190 1191 * ACU_FastMerge.cc (fastMerge): use getTree() (2 versions) 1192 1193 * ACU_DagNode.hh (class ACU_DagNode): replace struct Pair with a 1194 typedef from ACU_Pair 1195 1196 * ACU_Normalize.cc (insertAlien): use class ACU_Tree 1197 1198 * ACU_DagNode.cc (compareArguments): use getTree() 1199 1200 * ACU_Convert.cc: deleted 1201 1202 * ACU_DagNode.hh (class ACU_DagNode): deleted decls for 1203 makeTree(), pow2min1(), makeTree() 1204 1205 * ACU_BaseDagNode.cc (getSize): use getTree() 1206 1207 * ACU_TreeDagNode.cc (recComputeBaseSort): deleted 1208 (arguments): use tree data member 1209 (getHashValue): use tree data member 1210 (overwriteWithClone): use tree data member 1211 (makeClone): use tree data member 1212 (compareArguments): use tree data member 1213 (stackArguments): use tree data member 1214 (markArguments): use ACU_Tree::mark() 1215 (treeToArgVec): use tree data member 1216 1217 * ACU_TreeDagNode.hh (class ACU_TreeDagNode): use ACU_Tree data 1218 element 1219 (getRoot): becomes getTree() 1220 (class ACU_TreeDagNode): deleted decl for recComputeBaseSort() 1221 1222 * ACU_Symbol.hh (computeMultSortIndex): deleted 1223 (computeSortIndex): deleted 1224 1225===================================Maude80a=========================================== 1226 12272003-05-02 Steven Eker <eker@goo.csl.sri.com> 1228 1229 * ACU_Symbol.hh (class ACU_Symbol): added decl for rewriteAtTop() 1230 1231 * ACU_Symbol.cc (rewriteAtTop): added 1232 (eqRewrite): use rewriteAtTop() to avoid having an 1233 ACU_ExtensionInfo on our stack frame 1234 (eqRewrite): simplified; we no longer assume that if we have 1235 standard strategy and our subject was produced by an assignment 1236 that we cannot be equation free; mbs can prevent exact sort 1237 calculation and setting of reduced flag 1238 (reduceArgumentsAndNormalize): only remove identity in 1239 ACU_DagNode::EXTENSION case 1240 1241 * ACU_DagNode.cc (markArguments): avoid recursing on the first arg 1242 that shares our symbol 1243 12442003-05-01 Steven Eker <eker@goo.csl.sri.com> 1245 1246 * ACU_TreeDagNode.cc (overwriteWithClone): use 1247 copySetRewritingFlags() 1248 (makeClone): use copySetRewritingFlags() 1249 1250 * ACU_DagNode.cc (overwriteWithClone): use copySetRewritingFlags() 1251 and fastCopy() 1252 (makeClone): use copySetRewritingFlags() and fastCopy() 1253 12542003-04-30 Steven Eker <eker@goo.csl.sri.com> 1255 1256 * ACU_LhsCompiler3.cc (findLongestIncreasingSequence): added 1257 comment to explain why calling subsumes() is safe even in the 1258 presence of external agencies that can bind variables in the 1259 subsumer 1260 1261===================================Maude80=========================================== 1262 12632003-03-28 Steven Eker <eker@goo.csl.sri.com> 1264 1265 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): deleted decl for 1266 copyMultiplicity() 1267 1268 * ACU_Matcher.cc (fullMatch): call addSubjects() here 1269 (aliensOnlyMatch): call addSubjects() here 1270 (buildBipartiteGraph): don't call addSubjects() here 1271 (aliensOnlyMatch): check for trivial graph 1272 (match): expand copyMultiplicity() here since it's only called 1273 from this one place 1274 (copyMultiplicity): deleted 1275 12762003-03-27 Steven Eker <eker@goo.csl.sri.com> 1277 1278 * ACU_Matcher.cc (fullMatch): check for trivial bipartite graph 1279 12802003-03-26 Steven Eker <eker@goo.csl.sri.com> 1281 1282 * ACU_Subproblem.hh (noPatterns): added 1283 1284 * ACU_Matcher.cc (forcedLoneVariableCase): now handle identity 1285 case here; no longer local_inline 1286 (match): don't handle lone variable identity case here 1287 1288 * ACU_RedBlackMatcher.cc (forcedLoneVariableCase): code cleaning 1289 1290 * ACU_Theory.hh: deleted fwd decl for class 1291 ACU_AlienAlienLhsAutomaton 1292 1293 * ACU_DagNode.hh (class ACU_DagNode): deleted decl for 1294 findFirstOccurrence() 1295 1296 * ACU_DagOperations.cc (findFirstOccurrence): deleted 1297 1298 * ACU_Term.hh (class ACU_Term): deleted decl for 1299 tryToMakeAlienAlienLhsAutomaton() 1300 1301 * ACU_LhsCompiler0.cc (tryToMakeAlienAlienLhsAutomaton): deleted 1302 (tryToMakeSpecialCaseAutomaton): don't call 1303 tryToMakeAlienAlienLhsAutomaton() 1304 1305 * ACU_AlienAlienLhsAutomaton.cc: deleted 1306 1307 * ACU_AlienAlienLhsAutomaton.hh: deleted 1308 1309 * ACU_Matcher.cc (buildBipartiteGraph): new ACU_Subproblem() 1310 convention to get arround the probelm that currentMultipplicities 1311 can change 1312 1313 * ACU_DagNode.cc (matchVariableWithExtension): new 1314 ACU_Subproblem() convention 1315 1316 * ACU_Subproblem.hh (class ACU_Subproblem): added decl for 1317 addSubjects(); updated decl for ctor 1318 1319 * ACU_Subproblem.cc (addSubjects): added 1320 (ACU_Subproblem): don't set currentMultiplicity here 1321 1322 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): updated decl for 1323 buildBipartiteGraph() 1324 1325 * ACU_Matcher.cc (buildBipartiteGraph): take SubproblemAccumulator 1326 arg 1327 (fullMatch): new buildBipartiteGraph() convention 1328 (aliensOnlyMatch): new buildBipartiteGraph() convention 1329 1330 * ACU_Subproblem.hh (class ACU_Subproblem): added decl for 1331 removePatternNode() 1332 1333 * ACU_Subproblem.cc (removePatternNode): added 1334 1335 * ACU_Matcher.cc (buildBipartiteGraph): force patterns that only 1336 have a single edge 1337 13382003-03-25 Steven Eker <eker@goo.csl.sri.com> 1339 1340 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): updated decls for 1341 forcedLoneVariableCase(), greedyPureMatch(), 1342 tryToBindLastVariable(), tryToBindVariable(), greedyMatch(), 1343 eliminateGroundedOutAliens(), eliminateGroundAliens(), 1344 eliminateBoundVariables() 1345 1346 * ACU_RedBlackMatcher.cc (eliminateBoundVariables): simplified 1347 argument list 1348 (eliminateGroundAliens): simplified argument list 1349 (eliminateGroundedOutAliens): simplified argument list 1350 (greedyMatch): simplified argument list 1351 (greedyMatch): simpified call to greedyPureMatch() 1352 (tryToBindVariable): simplified argument list 1353 (makeHighMultiplicityAssignment): current -> root so we don't 1354 confuse arg with data member 1355 (tryToBindLastVariable): simplified argument list 1356 (greedyPureMatch): simplified argument list 1357 (greedyPureMatch): simplified calls to tryToBindLastVariable() and 1358 tryToBindVariable() 1359 (redBlackMatch): assignto data members rather than local variables 1360 for current and matchedMultiplicity 1361 (redBlackMatch): simplified calls to eliminateBoundVariables(), 1362 eliminateGroundAliens(), eliminateGroundedOutAliens(), 1363 forcedLoneVariableCase() and greedyMatch() 1364 (forcedLoneVariableCase): simplified argument list 1365 1366 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): added decl for 1367 red-black version of forcedLoneVariableCase() 1368 (class ACU_LhsAutomaton): added data members current, 1369 nrUnboundVariables and matchedMultiplicity so we don't have to 1370 drag these values around as arguments at match time 1371 1372 * ACU_RedBlackMatcher.cc (forcedLoneVariableCase): added red-black 1373 version 1374 (redBlackMatch): use forcedLoneVariableCase() 1375 1376 * ACU_Matcher.cc (match): pass returnedSubproblem arg to 1377 redBlackMatch() 1378 1379 * ACU_RedBlackMatcher.cc (redBlackMatch): now take 1380 returnedSubproblem arg 1381 13822003-03-24 Steven Eker <eker@goo.csl.sri.com> 1383 1384 * ACU_AlienAlienLhsAutomaton.cc (match): use safeCast() 1385 1386 * ACU_ExtensionInfo.cc (copy): use safeCast() 1387 1388 * ACU_Matcher.cc (match): use safeCast() 1389 1390 * ACU_Term.cc (normalizeAliensAndFlatten): use safeCast() (3 1391 places) 1392 1393 * ACU_DagNode.cc (partialReplace): use safeCast() 1394 (partialConstruct): use safeCast() 1395 (matchVariableWithExtension): use safeCast() 1396 1397 * ACU_NonLinearLhsAutomaton.cc (match): use safeCast() (2 places) 1398 1399 * ACU_GndLhsAutomaton.cc (ACU_GndLhsAutomaton): don't initialize 1400 trueFailure 1401 (match): test extensionInfo == 0 rather than trueFailure 1402 (dump): don't dump trueFailure 1403 1404 * ACU_GndLhsAutomaton.hh (class ACU_GndLhsAutomaton): deleted data 1405 member trueFailure 1406 1407 * ACU_CollectorLhsAutomaton.cc (ACU_CollectorLhsAutomaton): added 1408 Assert to check for sort constraint freeness 1409 (collect): don't check for sort constraint freeness (both 1410 versions) 1411 (collect): use getUniqueSortIndex() (both versions) 1412 1413 * ACU_LhsCompiler0.cc (tryToMakeCollectorLhsAutomaton): require 1414 that top symbol be sort constraint free 1415 14162003-03-21 Steven Eker <eker@goo.csl.sri.com> 1417 1418 * ACU_Term.hh (class ACU_Term): added decl for 1419 tryToMakeSpecialCaseAutomaton() 1420 1421 * ACU_LhsCompiler0.cc (tryToMakeSpecialCaseAutomaton): added 1422 (compileLhs2): simplified using tryToMakeSpecialCaseAutomaton() 1423 1424 * ACU_NGA_LhsAutomaton.cc (match): call setValidAfterMatch() 1425 1426 * ACU_VarLhsAutomaton.cc (match): call setValidAfterMatch() 1427 1428 * ACU_GndLhsAutomaton.cc (match): call setValidAfterMatch() 1429 1430 * ACU_TreeDagNode.hh (ACU_TreeDagNode): added Assert() to check 1431 that we don't make an ACU_TreeDagNode with single argument 1432 1433 * ACU_NonLinearLhsAutomaton.cc (match): fixed symmetric bug 1434 (dump): dump pureSort 1435 (match): deleted superfluous setValidAfterMatch() 1436 1437 * ACU_RedBlackMatcher.cc (greedyPureMatch): fixed bug where we 1438 were creating ACU node with single argument when setting extension 1439 1440 * ACU_NonLinearLhsAutomaton.cc (match): restructured 1441 14422003-03-20 Steven Eker <eker@goo.csl.sri.com> 1443 1444 * ACU_Term.hh (class ACU_Term): updated decl for 1445 tryToMakeNonLinearLhsAutomaton() 1446 1447 * ACU_LhsCompiler0.cc (tryToMakeNonLinearLhsAutomaton): don't take 1448 matchAtTop arg since now it must be true 1449 (tryToMakeNonLinearLhsAutomaton): allow LIMIT_SORT, check that 1450 multiplicity <= SAT_MULT; new ACU_NonLinearLhsAutomaton() calling 1451 convention 1452 (compileLhs2): use new tryToMakeNonLinearLhsAutomaton() convention 1453 1454 * ACU_NonLinearLhsAutomaton.cc (match): check getMaxMult() here so 1455 that we can return false if there is no subject with enough 1456 multiplicity 1457 1458 * ACU_NonLinearLhsAutomaton.hh (class ACU_NonLinearLhsAutomaton): 1459 updated decl for ctor 1460 1461 * ACU_NonLinearLhsAutomaton.cc (ACU_NonLinearLhsAutomaton): don't 1462 take matchAtTop (must be true) or collapsePossible (must be false) 1463 1464 * ACU_NonLinearLhsAutomaton.hh (class ACU_NonLinearLhsAutomaton): 1465 deleted data members topSymbol and matched; added data member 1466 pureSort 1467 (class ACU_NonLinearLhsAutomaton): deleted decl for treeMatch() 1468 1469 * ACU_NonLinearLhsAutomaton.cc (match): use 1470 makeHighMultiplicityAssignment() rather than treeMatch() 1471 (match): deleted non-extension case; this will now be handled in 1472 the general greedy matcher 1473 (dump): don't dump topSymbol 1474 (match): use getSymbol rather than topSymbol 1475 (ACU_NonLinearLhsAutomaton): init pureSort; allow LIMIT_SORT 1476 (ACU_NonLinearLhsAutomaton): don't init topSymbol 1477 (treeMatch): deleted 1478 1479 * ACU_Subproblem.cc (~ACU_Subproblem): use FOR_EACH_CONST 1480 (solveVariables): use FOR_EACH_CONST 1481 1482 * ACU_RedBlackMatcher.cc (greedyMatch): new convention for 1483 greedyPureMatch() 1484 1485 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): updated decl for 1486 greedyPureMatch(); made makeHighMultiplicityAssignment() protected 1487 1488 * ACU_RedBlackMatcher.cc (greedyPureMatch): return bool now that 1489 we no longer try to make a distiction between true failure and 1490 UNDECIDED 1491 1492 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): updated decls for 1493 decidePhase1FailureMode() and decidePhase2FailureMode() 1494 1495 * ACU_GreedyMatcher.cc (decidePhase1FailureMode): rewritten 1496 (greedyPureMatch): use new decidePhase1FailureMode() convention 1497 (decidePhase2FailureMode): simplified to avoid nasty bug where a 1498 unit variable could be given a lower sort subject when it actually 1499 needs a higher sort subject in order for the match to succeed and 1500 we could end up returning false when a match is really possible 1501 (greedyPureMatch): use new decidePhase2FailureMode() convention 1502 15032003-03-19 Steven Eker <eker@goo.csl.sri.com> 1504 1505 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): added decls for 1506 decidePhase1FailureMode() and decidePhase2FailureMode() 1507 1508 * ACU_GreedyMatcher.cc (decidePhase1FailureMode): added 1509 (decidePhase2FailureMode): added 1510 (greedyPureMatch): use decidePhase1FailureMode() and 1511 decidePhase2FailureMode() 1512 1513 * ACU_Matcher.cc (match): don't pass returnUndecidedOnFail arg to 1514 greedyPureMatch() 1515 1516 * ACU_GreedyMatcher.cc (greedyMatch): don't pass 1517 returnUndecidedOnFail arg to greedyPureMatch() 1518 1519 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): updated decl for 1520 greedyPureMatch() 1521 1522 * ACU_GreedyMatcher.cc (greedyPureMatch): don't take 1523 returnUndecidedOnFail since greedyMatch() already checks for true 1524 and wasted effort is slight and rare 1525 1526 * ACU_Matcher.cc (eliminateGroundAliens): use FOR_EACH_CONST 1527 (eliminateGroundedOutAliens): use FOR_EACH_CONST 1528 (eliminateGroundedOutAliens): rewritten to be almost symmetric 1529 with red-black version 1530 (computeTotalMultiplicity): use FOR_EACH_CONST 1531 (copyMultiplicity): use FOR_EACH_CONST 1532 (fullMatch): use FOR_EACH_CONST 1533 (handleElementVariables): use FOR_EACH_CONST 1534 1535 * ACU_GreedyMatcher.cc (greedyMatch): rewritten to be mostly 1536 symmetric with red-black version 1537 1538 * ACU_LhsAutomaton.cc (dump): dump redBlackOK and collectorSeen 1539 1540 * ACU_LhsCompiler3.cc (compileGreedyAndFullCases): new complete() 1541 convention 1542 1543 * ACU_LhsCompiler2.cc (compileAliensOnlyCase): new complete() 1544 convention 1545 1546 * ACU_LhsCompiler1.cc (compileLhs3): new complete() convention 1547 1548 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): updated decl for 1549 complete() 1550 1551 * ACU_LhsAutomaton.cc (ACU_LhsAutomaton): init collectorSeen 1552 (addTopVariable): update collectorSeen 1553 (complete): new redBlackOK calculation 1554 1555 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): updated decl for 1556 addTopVariable() 1557 (class ACU_LhsAutomaton): added data member collectorSeen 1558 1559 * ACU_LhsCompiler1.cc (compileLhs3): use new addTopVariable() 1560 convention 1561 1562 * ACU_LhsAutomaton.cc (ACU_LhsAutomaton): init redBlackOK = true 1563 (addAbstractionVariable): falsify redBlackOK 1564 (addGroundedOutAlien): falsify redBlackOK if alien unstable 1565 (addNonGroundAlien): falsify redBlackOK if alien unstable 1566 15672003-03-18 Steven Eker <eker@goo.csl.sri.com> 1568 1569 * ACU_LhsCompiler3.cc (compileGreedyAndFullCases): use new 1570 complete() convention 1571 1572 * ACU_LhsCompiler2.cc (compileAliensOnlyCase): use new complete() 1573 convention 1574 1575 * ACU_LhsCompiler1.cc (compileLhs3): use new complete() convention 1576 1577 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): updated decl for 1578 complete() 1579 1580 * ACU_LhsAutomaton.cc (complete): take redBlackPossible arg; we 1581 can't rely on strategy == LONE_VARIABLE beacuse of variable 1582 abstraction 1583 1584 * ACU_LhsCompiler1.cc (compileLhs3): use empty() rather than 1585 length() == 0 1586 15872003-03-17 Steven Eker <eker@goo.csl.sri.com> 1588 1589 * ACU_TreeDagNode.cc (recComputeBaseSort): fixed nasty bug where 1590 we were using getLeft() twice instead of getRight() and computing 1591 the wrong sort 1592 1593 * ACU_LhsAutomaton.cc (ACU_LhsAutomaton): don't set redBlackOK 1594 here 1595 (complete): set redBlackOK here 1596 1597 * ACU_RedBlackMatcher.cc (redBlackMatch): call greedyMatch() 1598 15992003-03-12 Steven Eker <eker@goo.csl.sri.com> 1600 1601 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): added decl for 1602 makeHighMultiplicityAssignment() 1603 (class ACU_LhsAutomaton): added data member matched 1604 1605 * ACU_RedBlackMatcher.cc (makeHighMultiplicityAssignment): added 1606 (tryToBindLastVariable): added high multiplicity cases 1607 16082003-03-11 Steven Eker <eker@goo.csl.sri.com> 1609 1610 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): added decl for 1611 tryToBindLastVariable() 1612 1613 * ACU_RedBlackMatcher.cc (tryToBindLastVariable): added 1614 1615 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): updated decls for 1616 eliminateBoundVariables(), eliminateGroundAliens(), 1617 eliminateGroundedOutAliens() and greedyMatch(); added decl for 1618 tryToBindVariable() 1619 (class ACU_LhsAutomaton): updated decl for greedyPureMatch() 1620 1621 * ACU_RedBlackMatcher.cc (eliminateBoundVariables): update 1622 matchedMultiplicity 1623 (eliminateGroundAliens): update matchedMultiplicity 1624 (greedyMatch): update matchedMultiplicity 1625 (tryToBindVariable): added 1626 1627 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): added decls for 1628 red-black versions of greedyPureMatch() and greedyMatch(); updated 1629 decl for eliminateBoundVariables() 1630 1631 * ACU_RedBlackMatcher.cc (greedyMatch): added red-black version 1632 (eliminateBoundVariables): keep track of number of unbound 1633 variables rather than making a linked list of them. 1634 (eliminateBoundVariables): use iterators 1635 (eliminateBoundVariables): use FOR_EACH_CONST() macro 1636 (eliminateGroundAliens): use FOR_EACH_CONST() macro 1637 (eliminateGroundedOutAliens): use FOR_EACH_CONST() macro 1638 (greedyPureMatch): added red-black version 1639 16402003-03-10 Steven Eker <eker@goo.csl.sri.com> 1641 1642 * ACU_Matcher.cc (eliminateGroundAliens): use iterators 1643 (eliminateGroundedOutAliens): use iterators 1644 (eliminateGroundedOutAliens): rearrange tests; now only look at 1645 multiplicity after we have a match; if current multiplicity is too 1646 small we can rewturn false since ground out alien must match a 1647 unique subject subterm 1648 1649 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): added decls for 1650 red-black versions of eliminateBoundVariables(), 1651 eliminateGroundAliens() and eliminateGroundedOutAliens() 1652 1653 * ACU_RedBlackMatcher.cc (eliminateBoundVariables): added 1654 red-black version 1655 (eliminateGroundAliens): added red-black version 1656 (eliminateGroundedOutAliens): added red-black version 1657 1658 * ACU_LhsAutomaton.cc (ACU_LhsAutomaton): initialize redBlackOK 1659 1660 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): added decl for 1661 redBlackMatch() 1662 1663 * ACU_RedBlackMatcher.cc (redBlackMatch): added stub 1664 1665 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): added data member 1666 redBlackOK 1667 1668 * ACU_Matcher.cc (match): use redBlackOK and redBlackMatch() 1669 16702003-03-07 Steven Eker <eker@goo.csl.sri.com> 1671 1672 * ACU_NGA_LhsAutomaton.hh (class ACU_NGA_LhsAutomaton): delete 1673 data memeber trueFailure 1674 1675 * ACU_NGA_LhsAutomaton.cc (ACU_NGA_LhsAutomaton): added Assert()s 1676 to check to stripper term is non-ground and stable 1677 (match): do full match if collect() fails; this fixes a nasty bug 1678 where we tried to continue but collect() has destroyed the 1679 iterator 1680 (ACU_NGA_LhsAutomaton): don't initialize trueFailure 1681 1682 * ACU_VarLhsAutomaton.cc (ACU_VarLhsAutomaton): allow trueFailure 1683 if stripper variable has pure sort 1684 1685 * ACU_LhsCompiler0.cc (tryToMakeCollectorLhsAutomaton): no longer 1686 require stripper variable to have unit or pure sort 1687 1688 * ACU_VarLhsAutomaton.cc (match): do full match if collect() 1689 fails; this fixes a nasty bug where we tried to continue but 1690 collect() has destroyed the iterator 1691 (ACU_VarLhsAutomaton): changed definition of trueFailure to take 1692 account of the fact that failures due to collect() never test 1693 trueFailure 1694 (ACU_VarLhsAutomaton): added Assert() to check that stripper 1695 variable can't take identity 1696 1697 * ACU_LhsCompiler0.cc (tryToMakeCollectorLhsAutomaton): chnage 1698 requirement on collect variable to have unbounded sort rather than 1699 pure or limit sort. The is a wweaker condition that is now allowed 1700 because we gave up on the fast sort computation trick. 1701 1702 * ACU_GndLhsAutomaton.cc (ACU_GndLhsAutomaton): added Assert() to 1703 check that stripper term is ground 1704 1705 * ACU_CollectorLhsAutomaton.cc (ACU_CollectorLhsAutomaton): added 1706 Assert() to check that collector has unbounded sort 1707 1708 * ACU_NGA_LhsAutomaton.hh (class ACU_NGA_LhsAutomaton): deleted 1709 data member local 1710 1711 * ACU_NGA_LhsAutomaton.cc (match): use getLocal() 1712 (ACU_NGA_LhsAutomaton): don't initialize local 1713 1714 * ACU_LhsAutomaton.hh (getLocal): added 1715 (getLocal2): added 1716 1717 * ACU_NGA_LhsAutomaton.hh (class ACU_NGA_LhsAutomaton): deleted 1718 data members topSymbol and collapsePossible; added data member 1719 trueFailure 1720 1721 * ACU_NGA_LhsAutomaton.cc (match): use getSymbol() 1722 (match): use getCollapsePossible() 1723 (dump): don't dump topSymbol or collapsePossible 1724 (ACU_NGA_LhsAutomaton): don't initialize topSymbol or 1725 collapsePossible; initialize trueFailure 1726 (match): reorganized search loops using trueFailure 1727 17282003-03-06 Steven Eker <eker@goo.csl.sri.com> 1729 1730 * ACU_NGA_LhsAutomaton.cc (match): use new collapse() convention 1731 1732 * ACU_GndLhsAutomaton.cc (ACU_GndLhsAutomaton): initialize 1733 trueFailure 1734 (match): use trueFailure 1735 (dump): dump trueFailure 1736 1737 * ACU_GndLhsAutomaton.hh (class ACU_GndLhsAutomaton): added data 1738 member trueFailure 1739 1740 * ACU_VarLhsAutomaton.cc (match): rewrote argVec case 1741 (dump): dump trueFailure 1742 1743 * ACU_VarLhsAutomaton.hh (class ACU_VarLhsAutomaton): added data 1744 member trueFailure 1745 1746 * ACU_VarLhsAutomaton.cc (ACU_VarLhsAutomaton): don't initialize 1747 topSymbol or collapsePossible 1748 (dump): don't dump topSymbol or collapsePossible 1749 (match): use use getSymbol() and getCollapsePossible(); use new 1750 collapse() convention 1751 (match): fixed bug where we were returing false even though 1752 assigning multiple things to stripper, or putting stuff in 1753 extension or applying a membership might have produced a match. 1754 (ACU_VarLhsAutomaton): initialize trueFailure 1755 1756 * ACU_VarLhsAutomaton.hh (class ACU_VarLhsAutomaton): deleted data 1757 members topSymbol and collapsePossible 1758 1759 * ACU_GndLhsAutomaton.cc (match): use new collapse() convention 1760 1761 * ACU_CollectorLhsAutomaton.hh (collapse): use getSymbol() 1762 (class ACU_CollectorLhsAutomaton): updated decl for collapse() 1763 1764 * ACU_GndLhsAutomaton.cc (ACU_GndLhsAutomaton): don't initialize 1765 topSymbol or collapsePossible 1766 (dump): don't dump topSymbol or collapsePossible 1767 (match): fixed bug where we assumed red-black collect failing 1768 implied no match, where as some of teh suff might have been put in 1769 the extension 1770 (match): use getSymbol() (two places) and getCollapsePossible() 1771 1772 * ACU_GndLhsAutomaton.hh (class ACU_GndLhsAutomaton): deleted data 1773 members topSymbol and collapsePossible 1774 1775 * ACU_LhsAutomaton.hh (getSymbol): added 1776 (getCollapsePossible): added 1777 1778 * ACU_CollectorLhsAutomaton.cc (collect): major simplification; we 1779 no longer try to do sort check as we build, instead we use 1780 argVecComputeBaseSort() afterwards; this can lose in the case that 1781 we are not in an error free component (argVecComputeBaseSort() has 1782 to look at each arg) and we are not reduced (didn't need to have 1783 th exact base sort); but it simplifies things greatly 1784 (ACU_CollectorLhsAutomaton): swich of sort checks for kind 1785 variables 1786 17872003-03-05 Steven Eker <eker@goo.csl.sri.com> 1788 1789 * ACU_Symbol.cc (computeBaseSort): complete rewrite using 1790 argVecComputeBaseSort(); this fixes a nasty bug where we assumed 1791 that ACU_DagNodes with getNormalizationStatus() == ASSIGNMENT 1792 could not be in the error sort - no longer true since we allowed 1793 variables at the kind level 1794 1795 * ACU_DagNode.cc (argVecComputeBaseSort): unroll first iteration 1796 of standand case loop to move initial case branch out of loop 1797 1798 * ACU_DagNode.hh (class ACU_DagNode): added decl for 1799 argVecComputeBaseSort() 1800 1801 * ACU_DagNode.cc (argVecComputeBaseSort): added 1802 1803 * ACU_TreeDagNode.hh (class ACU_TreeDagNode): deleted decl for 1804 makeDelete(); updated decl for treeComputeBaseSort() 1805 1806 * ACU_Symbol.cc (computeBaseSort): use new treeComputeBaseSort() 1807 convention 1808 1809 * ACU_TreeDagNode.cc (treeComputeBaseSort): return index of 1810 computed sort rather than calling setSortIndex() 1811 (makeDelete): deleted 1812 1813 * ACU_CollectorLhsAutomaton.cc (collect): (tree version) use 1814 treeComputeBaseSort(); don't use makeDelete(); use setSortIndex(); 1815 don't use repudiateSortInfo() 1816 1817 * ACU_Symbol.cc (computeBaseSort): use treeComputeBaseSort() 1818 1819 * ACU_TreeDagNode.hh (class ACU_TreeDagNode): updated decls for 1820 recComputeBaseSort() and treeComputeBaseSort() 1821 1822 * ACU_TreeDagNode.cc (computeBaseSort): computeMultBaseSort() -> 1823 computeMultSortIndex(); computeBaseSort() -> computeSortIndex() (2 1824 places) 1825 (computeBaseSort): becomes recComputeBaseSort() 1826 (computeBaseSort): treeComputeBaseSort() 1827 1828 * ACU_NonLinearLhsAutomaton.cc (treeMatch): computeMultBaseSort() 1829 -> computeMultSortIndex() (2 places) 1830 1831 * ACU_Symbol.hh (computeBaseSort): renamed to computeSortIndex() 1832 to avoid confusion 1833 (computeMultBaseSort): renamed to computeMultSortIndex() for the 1834 sake on consistancy 1835 1836 * ACU_TreeDagNode.cc (computeBaseSort): use new 1837 computeMultBaseSort() calling convention 1838 1839 * ACU_NonLinearLhsAutomaton.cc (treeMatch): use new 1840 computeMultBaseSort() calling convention (2 places) 1841 1842 * ACU_Symbol.hh (computeMultBaseSort): rewritten 1843 (class ACU_Symbol): updated decl for computeMultBaseSort() 1844 18452003-03-04 Steven Eker <eker@goo.csl.sri.com> 1846 1847 * ACU_Term.hh (class ACU_Term): updated decl for 1848 tryToMakeAlienAlienLhsAutomaton() 1849 1850 * ACU_LhsCompiler0.cc (compileLhs2): use new alien-alien automata 1851 convention 1852 (tryToMakeAlienAlienLhsAutomaton): use new 1853 ACU_AlienAlienLhsAutomaton() convention 1854 1855 * ACU_AlienAlienLhsAutomaton.cc (ACU_AlienAlienLhsAutomaton): call 1856 ACU_LhsAutomaton() 1857 (match): call ACU_LhsAutomation::match() instead of fullMatch() 1858 (dump): call ACU_LhsAutomaton::dump() rather than 1859 HeuristicLhsAutomaton::dump() 1860 1861 * ACU_AlienAlienLhsAutomaton.hh: derive from ACU_LhsAutomaton 1862 rather than HeuristicLhsAutomaton; updated decl for ctor 1863 1864 * ACU_CollectorLhsAutomaton.cc (dump): call 1865 ACU_LhsAutomaton::dump() rather than HeuristicLhsAutomaton::dump() 1866 1867 * ACU_LhsCompiler0.cc (tryToMakeCollectorLhsAutomaton): use new 1868 ACU_GndLhsAutomaton() convention 1869 (tryToMakeCollectorLhsAutomaton): use new ACU_VarLhsAutomaton() 1870 convention 1871 (tryToMakeCollectorLhsAutomaton): use new ACU_NGA_LhsAutomaton() 1872 convention 1873 (compileLhs2): use new compilation conventions for collector 1874 automata 1875 1876 * ACU_NGA_LhsAutomaton.cc (ACU_NGA_LhsAutomaton): use new 1877 ACU_CollectorLhsAutomaton() convention 1878 (match): call ACU_LhsAutomation::match() instead of fullMatch() (3 1879 places) 1880 1881 * ACU_NGA_LhsAutomaton.hh (class ACU_NGA_LhsAutomaton): updated 1882 decl for ctor 1883 1884 * ACU_VarLhsAutomaton.cc (ACU_VarLhsAutomaton): use new 1885 ACU_CollectorLhsAutomaton() convention 1886 (match): call ACU_LhsAutomation::match() instead of fullMatch() (2 1887 places) 1888 1889 * ACU_VarLhsAutomaton.hh (class ACU_VarLhsAutomaton): updated decl 1890 for ctor 1891 1892 * ACU_GndLhsAutomaton.cc (ACU_GndLhsAutomaton): use new 1893 ACU_CollectorLhsAutomaton() convention 1894 (match): call ACU_LhsAutomation::match() instead of fullMatch() 1895 1896 * ACU_GndLhsAutomaton.hh (class ACU_GndLhsAutomaton): updated decl 1897 for ctor 1898 1899 * ACU_CollectorLhsAutomaton.cc (ACU_CollectorLhsAutomaton): call 1900 ACU_LhsAutomaton() 1901 1902 * ACU_CollectorLhsAutomaton.hh (class ACU_CollectorLhsAutomaton): 1903 derive from ACU_LhsAutomaton rather than HeuristicLhsAutomaton; 1904 updated decl for ctor 1905 19062003-03-03 Steven Eker <eker@goo.csl.sri.com> 1907 1908 * ACU_LhsCompiler0.cc (compileLhs2): use new 1909 ACU_NonLinearLhsAutomaton convention 1910 (tryToMakeNonLinearLhsAutomaton): use new 1911 ACU_NonLinearLhsAutomaton convention 1912 1913 * ACU_NonLinearLhsAutomaton.cc (ACU_NonLinearLhsAutomaton): call 1914 ACU_LhsAutomaton() 1915 (treeMatch): call ACU_LhsAutomaton::match() instead of fullMatch() 1916 (match): call ACU_LhsAutomaton::match() instead of fullMatch() 1917 (dump): call instead ACU_LhsAutomaton::dump() of 1918 HeuristicLhsAutomaton::dump() 1919 1920 * ACU_NonLinearLhsAutomaton.hh (class ACU_NonLinearLhsAutomaton): 1921 derive from ACU_LhsAutomaton rather than HeuristicLhsAutomaton 1922 (class ACU_NonLinearLhsAutomaton): updated decl for ctor 1923 1924 * ACU_LhsCompiler1.cc (compileLhs3): don't return automaton 1925 1926 * ACU_Term.hh (class ACU_Term): updated decl for compileLhs3() 1927 1928 * ACU_LhsCompiler1.cc (compileLhs3): take ACU_LhsAutomaton rather 1929 than creating it 1930 1931 * ACU_LhsCompiler0.cc (compileLhs2): create ACU_LhsAutomaton; 1932 use new compileLhs3() convention 1933 1934 * ACU_LhsCompiler1.cc (compileLhs3): use new ACU_LhsAutomaton() 1935 convention 1936 1937 * ACU_LhsAutomaton.cc (ACU_LhsAutomaton): clear 1938 uniqueCollapseAutomaton rather than setting it 1939 1940 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): updated decl for 1941 ctor; added decl for addUniqueCollapseAutomaton() 1942 (addUniqueCollapseAutomaton): added 1943 19442003-02-25 Steven Eker <eker@goo.csl.sri.com> 1945 1946 * ACU_VarLhsAutomaton.cc: removed #pragma 1947 (match): updated Assert() 1948 1949 * ACU_VarLhsAutomaton.hh: removed #pragma 1950 1951 * ACU_TreeDagNode.cc (computeBaseSort): updated Assert() 1952 (treeToArgVec): updated Assert() 1953 1954 * ACU_TreeDagArgumentIterator.cc (argument): updated Assert() 1955 (next): updated Assert() 1956 1957 * ACU_Term.cc: removed #pragma 1958 (Term): updated Assert() 1959 (normalizeAliensAndFlatten): updated Assert() 1960 (compareArguments): updated Assert()s (both versions) 1961 (insertAbstractionVariables): updated DebugAdvisoryCheck() 1962 1963 * ACU_Term.hh: removed #pragma 1964 1965 * ACU_Symbol.cc: removed #pragma 1966 (makeDagNode): updated Assert() 1967 (computeBaseSort): updated Assert()s 1968 (normalizeAndComputeTrueSort): updated Assert() 1969 1970 * ACU_Symbol.hh: removed #pragma 1971 1972 * ACU_Subproblem.cc: removed #pragma 1973 1974 * ACU_Subproblem.hh: removed #pragma 1975 1976 * ACU_RhsAutomaton.cc: removed #pragma 1977 (buildArguments): updated Assert()s 1978 1979 * ACU_RhsAutomaton.hh: removed #pragma 1980 1981 * ACU_NonLinearLhsAutomaton.cc: removed #pragma 1982 (ACU_NonLinearLhsAutomaton): updated Assert() 1983 (fillOutExtensionInfo): updated Assert() 1984 (treeMatch): updated Assert()s 1985 (match): updated Assert()s 1986 1987 * ACU_NonLinearLhsAutomaton.hh: removed #pragma 1988 1989 * ACU_NGA_LhsAutomaton.cc: removed #pragma 1990 (match): updated Assert() 1991 1992 * ACU_NGA_LhsAutomaton.hh: removed #pragma 1993 1994 * ACU_MergeSort.cc (mergeSortAndUniquize): updated Assert() 1995 1996 * ACU_Matcher.cc (eliminateGroundedOutAliens): updated Assert() 1997 (forcedLoneVariableCase): updated Assert()s 1998 (match): updated Assert()s 1999 2000 * ACU_LhsCompiler3.cc (findGreedySequence): updated Assert() 2001 2002 * ACU_LhsCompiler2.cc (compileAliensOnlyCase): updated Assert()s 2003 (findConstraintPropagationSequence): updated Assert() 2004 2005 * ACU_LhsCompiler1.cc (compileLhs3): updated Assert() 2006 2007 * ACU_LhsAutomaton.cc: removed #pragma 2008 (complete): updated Assert() 2009 2010 * ACU_LhsAutomaton.hh: removed #pragma 2011 2012 * ACU_GreedyMatcher.cc (greedyPureMatch): updated Assert()s 2013 2014 * ACU_GndLhsAutomaton.cc: removed #pragma 2015 (match): updated Assert() 2016 2017 * ACU_GndLhsAutomaton.hh: removed #pragma 2018 2019 * ACU_ExtensionInfo.cc (buildMatchedPortion): updated Assert()s 2020 (convertToUnmatched): updated Assert()s 2021 2022 * ACU_ExtensionInfo.hh (useUnmatched): updated Assert() 2023 2024 * ACU_DagOperations.cc (findFirstOccurrence): updated Assert() 2025 (findFirstPotentialMatch): updated Assert() 2026 (binarySearch): updated Assert() (both versions) 2027 2028 * ACU_DagNormalization.cc (extensionNormalizeAtTop): updated Assert() 2029 2030 * ACU_DagNode.cc: removed #pragma 2031 (compareArguments): updated Assert()s 2032 (markArguments): updated Assert() 2033 (copyWithReplacement): updated Assert() 2034 (partialReplace): updated Assert()s 2035 (partialConstruct): updated Assert() 2036 2037 * ACU_DagNode.hh: removed #pragma 2038 2039 * ACU_DagArgumentIterator.cc: removed #pragma 2040 (argument): updated Assert() 2041 (next): updated Assert() 2042 2043 * ACU_DagArgumentIterator.hh: removed #pragma 2044 2045 * ACU_CollectorLhsAutomaton.cc: removed #pragma 2046 (collect): updated Assert()s 2047 2048 * ACU_CollectorLhsAutomaton.hh: removed #pragma 2049 2050 * ACU_CollapseMatcher.cc (uniqueCollapseMatch): updated Assert()s 2051 (multiwayCollapseMatch): updated Assert()s 2052 2053 * ACU_ArgumentIterator.cc: removed #pragma 2054 (argument): updated Assert() 2055 (next): updated Assert() 2056 2057 * ACU_ArgumentIterator.hh: removed #pragma 2058 2059 * ACU_AlienAlienLhsAutomaton.cc: removed #pragma 2060 2061 * ACU_AlienAlienLhsAutomaton.hh: removed #pragma 2062 2063===================================Maude79=========================================== 2064 20652003-02-20 Steven Eker <eker@goo.csl.sri.com> 2066 2067 * ACU_Flatten.cc (flattenSortAndUniquize): use fastCopy(); handle 2068 ACU_TreeDagNode* case; don't bother trying to combine flattened in 2069 argument list with current run 2070 (flattenSortAndUniquize): can't use fastCopy() after all - need to 2071 multiply by multiplicity 2072 (flattenSortAndUniquize): removed optimize involving d+1 as it 2073 fails due to strict iterator checking 2074 2075 * ACU_DagNormalization.cc (copyAndBinaryInsert): don't treat 2076 nrSourceArgs > 1 as a special case 2077 (extensionNormalizeAtTop): fixed longstanding performance bug 2078 where we were copying an argArray rather than taking its reference 2079 (extensionNormalizeAtTop): handle ACU_TreeDagNode* case 2080 20812003-02-13 Steven Eker <eker@goo.csl.sri.com> 2082 2083 * ACU_Convert.cc (makeTree): don't use fast version of 2084 ACU_RedBlackNode() since we don't have the maxMult value to hand 2085 20862003-02-12 Steven Eker <eker@goo.csl.sri.com> 2087 2088 * ACU_Flatten.cc (flattenSortAndUniquize): moved here 2089 2090 * ACU_MergeSort.cc (mergeSortAndUniquize): moved here 2091 (sortAndUniquize): moved here 2092 2093 * ACU_Convert.cc (makeTree): added optional code for checking 2094 red-black property 2095 2096 * ACU_ExtensionInfo.cc (convertToUnmatched): reimplemented to 2097 handle unmatched dag root case 2098 20992003-02-11 Steven Eker <eker@goo.csl.sri.com> 2100 2101 * ACU_ExtensionInfo.cc (copy): reimplemented to handle unmatched 2102 dag root case 2103 (makeClone): reimplemented to handle unmatched dag root case 2104 (buildMatchedPortion): reimplemented to handle ACU_TreeDagNode 2105 case 2106 2107 * ACU_DagNode.hh (class ACU_DagNode): deleted decl for 2108 makeExtensionInfo() 2109 2110 * ACU_DagNode.cc (makeExtensionInfo): deleted 2111 2112 * ACU_TreeDagNode.hh (class ACU_TreeDagNode): deleted decl for 2113 makeExtensionInfo() 2114 2115 * ACU_TreeDagNode.cc (makeExtensionInfo): deleted 2116 2117 * ACU_BaseDagNode.hh (class ACU_BaseDagNode): added decl for 2118 makeExtensionInfo() 2119 2120 * ACU_BaseDagNode.cc (makeExtensionInfo): added 2121 2122 * ACU_TreeDagNode.cc (partialConstruct): reimplemented without 2123 using treeToArgVec() 2124 2125 * ACU_TreeDagNode.hh (class ACU_TreeDagNode): deleted decls for 2126 argVecToTree(), overwriteWithInsert() and makeTree() 2127 2128 * ACU_TreeDagNode.cc (argVecToTree): deleted 2129 (pow2min1): deleted 2130 (makeTree): deleted 2131 (overwriteWithInsert): deleted 2132 2133 * ACU_NewNormalize.cc: deleted 2134 2135 * ACU_Normalize.cc (insertAlien): use makeTree() in place of 2136 argVecToTree() (2 places) 2137 (insertAlien): use consInsert() in place of overwriteWithInsert() 2138 (normalizeAtTop): use makeTree() in place of argVecToTree() 2139 (normalizeAtTop): removed alternative merge case code 2140 2141 * ACU_DagNode.hh (class ACU_DagNode): added decl for makeTree() 2142 (both versions) and pow2min1() 2143 2144 * ACU_Convert.cc: created 2145 2146 * ACU_Normalize.cc (insertAlien): use CONVERT_THRESHOLD 2147 (insertAlien): fixed bug in alterate code when we fall below the 2148 threshold 2149 2150 * ACU_DagNode.hh (class ACU_DagNode): added MERGE_THRESHOLD to 2151 enum Sizes; THRESHOLD -> CONVERT_THRESHOLD 2152 2153 * ACU_Normalize.cc (normalizeAtTop): use MERGE_THRESHOLD 2154 21552003-02-10 Steven Eker <eker@goo.csl.sri.com> 2156 2157 * ACU_Normalize.cc (normalizeAtTop): don't convert back to 2158 re-black ofer merging two red-black trees 2159 2160 * ACU_NonLinearLhsAutomaton.cc (treeMatch): 2161 setNormalizationStatus(ACU_DagNode::ASSIGNMENT) now that we are 2162 extract hi mult arguments in order 2163 21642003-02-07 Steven Eker <eker@goo.csl.sri.com> 2165 2166 * ACU_DagNode.hh (class ACU_DagNode): added ctor decl for Pair 2167 (Pair): added 2168 (Pair): added default ctor 2169 2170 * ACU_NonLinearLhsAutomaton.hh (class ACU_NonLinearLhsAutomaton): 2171 added data member matched 2172 2173 * ACU_NonLinearLhsAutomaton.cc (treeMatch): rewritten 2174 (match): use treeMatch() 2175 21762003-02-06 Steven Eker <eker@goo.csl.sri.com> 2177 2178 * ACU_NonLinearLhsAutomaton.hh (class ACU_NonLinearLhsAutomaton): 2179 added decl for treeMatch() 2180 2181 * ACU_NonLinearLhsAutomaton.cc (treeMatch): added 2182 21832003-02-05 Steven Eker <eker@goo.csl.sri.com> 2184 2185 * ACU_TreeDagNode.cc (partialReplace): simplified using new 2186 ACU_Extension interface 2187 2188 * ACU_NonLinearLhsAutomaton.cc (match): use new ACU_Extension 2189 interface 2190 2191 * ACU_ExtensionInfo.hh (clearMatched): deleted 2192 (addMatched): deleted 2193 (getMatched): deleted 2194 (clear): set unmatched to 0 rather than clearing matched 2195 (reset): set unmatched to 0 rather than clearing matched 2196 (class ACU_ExtensionInfo): deleted data member matched; added data 2197 member unmatched 2198 (setUnmatched): added DagNode* version 2199 (getUnmatched): added DagNode* version 2200 (useUnmatched): use unmatched 2201 22022003-02-04 Steven Eker <eker@goo.csl.sri.com> 2203 2204 * ACU_Symbol.cc: (complexStrategy): use new normalizeAtTop() (2 2205 places) 2206 (reduceArgumentsAndNormalize): use new normalizeAtTop() 2207 (eqRewrite): use new normalizeAtTop() 2208 (memoStrategy): use new normalizeAtTop() (3 places) 2209 (normalizeAndComputeTrueSort): use new normalizeAtTop() 2210 2211 * ACU_DagNode.hh (class ACU_DagNode): added THRESHHOLD to enum Sizes 2212 2213 * ACU_TreeDagNode.hh (class ACU_TreeDagNode): made ctor public 2214 2215 * ACU_Normalize.cc (normalizeAtTop): reimplemented 2216 (insertAlien): added 2217 22182003-02-03 Steven Eker <eker@goo.csl.sri.com> 2219 2220 * ACU_Normalize.cc: created 2221 2222 * ACU_DagNode.hh (fastCopy): moved here 2223 (fastCopy): added ACU_FastIter version 2224 (class ACU_DagNode): added decls for additional versions of fastMerge() 2225 2226 * ACU_FastMerge.cc: created 2227 2228 * ACU_TreeDagNode.cc (markArguments): rewritten to do a preorder 2229 traversal, ignoring marked red-black nodes 2230 (partialReplace): added replacement == matched arg heuristic 2231 22322003-01-31 Steven Eker <eker@goo.csl.sri.com> 2233 2234 * ACU_NewNormalize.cc (normalizeAtTop): fixed stupid brace bug in 2235 two red-black tree case 2236 2237 * ACU_NonLinearLhsAutomaton.cc (match): fixed bug where we weren't 2238 dealing with the case that we matched everything 2239 2240 * ACU_TreeDagNode.cc (partialReplace): fixed bug where we were not 2241 testing r->getMultiplicity() against 1 2242 2243 * ACU_NewNormalize.cc (normalizeAtTop): added code for two 2244 red-black trees case 2245 2246 * ACU_Term.cc (analyseCollapses): becomes analyseCollapses2() 2247 2248 * ACU_Term.hh (class ACU_Term): analyseCollapses() -> 2249 analyseCollapses2() 2250 2251 * ACU_TreeDagArgumentIterator.cc: moved here 2252 2253 * ACU_TreeDagArgumentIterator.hh: moved here 2254 2255 * ACU_TreeDagNode.cc: moved here 2256 2257 * ACU_TreeDagNode.hh: moved here 2258 2259 * ACU_Theory.hh: added fwd decls for ACU_TreeDagNode and 2260 ACU_TreeDagArgumentIterator 2261 22622003-01-30 Steven Eker <eker@goo.csl.sri.com> 2263 2264 * ACU_CollectorLhsAutomaton.cc (collect): ACU_SlowIter -> 2265 ACU_Stack 2266 2267 * ACU_CollectorLhsAutomaton.hh (class ACU_CollectorLhsAutomaton): 2268 ACU_SlowIter -> ACU_Stack 2269 2270 * ACU_NGA_LhsAutomaton.cc (match): use 2271 ACU_RedBlackNode::findFirstPotentialMatch rather than 2272 ACU_TreeDagNode::findFirstPotentialMatch 2273 22742003-01-29 Steven Eker <eker@goo.csl.sri.com> 2275 2276 * ACU_VarLhsAutomaton.cc (match): getArgument() -> getDagNode() 2277 2278 * ACU_Term.cc (compareArguments): getArgument() -> getDagNode() 2279 2280 * ACU_NonLinearLhsAutomaton.cc (match): getArgument() -> 2281 getDagNode() 2282 2283 * ACU_NGA_LhsAutomaton.cc (match): getArgument() -> getDagNode() 2284 (2 places) 2285 2286 * ACU_DagNode.cc (compareArguments): getArgument() -> getDagNode() 2287 22882003-01-28 Steven Eker <eker@goo.csl.sri.com> 2289 2290 * ACU_ExtensionInfo.hh (class ACU_ExtensionInfo): added decl for 2291 convertToUnmatched() 2292 2293 * ACU_ExtensionInfo.cc (convertToUnmatched): added 2294 2295 * ACU_ExtensionInfo.hh (useUnmatched): added 2296 2297 * ACU_NewNormalize.cc (normalizeAtTop): use isTree() (2 places) 2298 2299 * ACU_DagNode.cc (getACU_DagNode): use isTree() 2300 2301 * ACU_NonLinearLhsAutomaton.cc (match): added red-black case 2302 23032003-01-27 Steven Eker <eker@goo.csl.sri.com> 2304 2305 * ACU_VarLhsAutomaton.cc (match): added red-black case 2306 2307 * ACU_GndLhsAutomaton.cc (match): added red-black case 2308 2309 * ACU_NGA_LhsAutomaton.cc (match): fixed if nesting bug; it hadn't 2310 bitten because collect() seldom return false; 2311 2312 * ACU_Symbol.cc (eqRewrite): use isTree() 2313 2314 * ACU_NGA_LhsAutomaton.cc (match): use isTree() 2315 2316 * ACU_ExtensionInfo.hh (clear): use getSize() 2317 (reset): use getSize() 2318 (clearMatched): added 2319 2320 * ACU_BaseDagNode.cc: created 2321 2322 * ACU_ExtensionInfo.hh (ACU_ExtensionInfo): take ACU_BaseDagNode* 2323 (class ACU_ExtensionInfo): added struct Matched and data member 2324 matched 2325 23262003-01-23 Steven Eker <eker@goo.csl.sri.com> 2327 2328 * ACU_DagNode.cc (compareArguments): rewritten to use left to 2329 right comparison and handle ACU_TreeDagNodes 2330 2331 * ACU_Term.cc (compareArguments): (DagNode* version) rewritten to 2332 use left to right comparison and handle ACU_TreeDagNodes 2333 (compareArguments): (Term*) rewritten to use iterators and left to 2334 right comparison 2335 23362003-01-22 Steven Eker <eker@goo.csl.sri.com> 2337 2338 * ACU_BaseDagNode.hh (isTree): added 2339 23402003-01-14 Steven Eker <eker@goo.csl.sri.com> 2341 2342 * ACU_Symbol.cc (eqRewrite): fixed casting bug in tree case 2343 23442003-01-13 Steven Eker <eker@goo.csl.sri.com> 2345 2346 * ACU_Symbol.hh (computeBaseSort): added 2347 (computeMultBaseSort): added 2348 2349 * ACU_ExtensionInfo.hh (ACU_ExtensionInfo): added ACU_TreeDagNode* 2350 version 2351 2352 * ACU_Symbol.cc (eqRewrite): handle TREE case 2353 2354 * ACU_CollectorLhsAutomaton.cc (collect): added ACU_TreeDagNode* 2355 version 2356 23572003-01-12 Steven Eker <eker@goo.csl.sri.com> 2358 2359 * ACU_NGA_LhsAutomaton.cc (match): added support for 2360 ACU_TreeDagNodes 2361 2362 * ACU_CollectorLhsAutomaton.hh (class ACU_CollectorLhsAutomaton): 2363 added decl for ACU_TreeDagNode* version of collect 2364 23652003-01-10 Steven Eker <eker@goo.csl.sri.com> 2366 2367 * ACU_Symbol.cc (eqRewrite): rewritten to use new normalizeAtTop() 2368 2369 * ACU_DagNode.hh (class ACU_DagNode): added decl for new version 2370 of normalizeAtTop() 2371 2372 * ACU_NewNormalize.cc: created 2373 2374 * ACU_DagNode.cc (getACU_DagNode): made into a global function 2375 2376 * ACU_DagNode.hh (class ACU_DagNode): made getACU_DagNode() a 2377 friend function rather than a static member function 2378 2379 * ACU_VarLhsAutomaton.cc (match): used getACU_DagNode() 2380 2381 * ACU_Term.cc (compareArguments): used getACU_DagNode() + 2382 const_cast<DagNode*>() 2383 2384 * ACU_Subproblem.cc (solveVariables): used getACU_DagNode() 2385 2386 * ACU_NonLinearLhsAutomaton.cc (match): used getACU_DagNode() 2387 2388 * ACU_NGA_LhsAutomaton.cc (match): used getACU_DagNode() 2389 2390 * ACU_Matcher.cc (match): used getACU_DagNode() 2391 2392 * ACU_GndLhsAutomaton.cc (match): used getACU_DagNode() 2393 2394 * ACU_AlienAlienLhsAutomaton.cc (match): used getACU_DagNode() 2395 2396 * ACU_Term.hh (symbol): replaced static_cast<ACU_Symbol>() with 2397 safeCast() 2398 2399 * ACU_Symbol.cc (ruleRewrite): used getACU_DagNode() 2400 (reduceArgumentsAndNormalize): used getACU_DagNode() 2401 (eqRewrite): used getACU_DagNode() 2402 (complexStrategy): used getACU_DagNode() 2403 (memoStrategy): used getACU_DagNode() 2404 (computeBaseSort): used getACU_DagNode() 2405 (normalizeAndComputeTrueSort): used getACU_DagNode() 2406 (stackArguments): used getACU_DagNode() 2407 2408 * ACU_DagNormalization.cc (flattenSortAndUniquize): used 2409 getACU_DagNode() 2410 (normalizeAtTop): used getACU_DagNode() in many places 2411 (extensionNormalizeAtTop): used getACU_DagNode() 2412 2413 * ACU_DagOperations.cc (eliminateSubject): use getACU_DagNode() 2414 rather than static_cast<ACU_DagNode*> 2415 2416 * ACU_DagNode.cc (compareArguments): handle TREE case 2417 2418 * ACU_DagNode.hh (class ACU_DagNode): added decl for 2419 getACU_DagNode() 2420 2421 * ACU_DagNode.cc (getACU_DagNode): added 2422 24232003-01-08 Steven Eker <eker@goo.csl.sri.com> 2424 2425 * ACU_Symbol.cc (eqRewrite): added crude hack to see if we can 2426 convert to re-black form and back 2427 2428 * ACU_DagNode.hh (class ACU_DagNode): made ACU_TreeDagNode a friend 2429 2430 * ACU_Theory.hh: added ACU_BaseDagNode; 2431 2432 * ACU_DagNode.cc (~ACU_DagNode): deleted 2433 2434 * ACU_DagNode.hh (class ACU_DagNode): rewritten, deriving from 2435 ACU_BaseDagNode 2436 2437 * ACU_BaseDagNode.hh: created 2438 24392003-01-07 Steven Eker <eker@goo.csl.sri.com> 2440 2441 * ACU_LhsCompiler0.cc (tryToMakeCollectorLhsAutomaton): use new 2442 ACU_NGA_LhsAutomaton() convention 2443 2444 * ACU_NGA_LhsAutomaton.cc (ACU_NGA_LhsAutomaton): replaced 2445 stripperTopSymbol with stripperTerm 2446 (match): rewritten using stripperTerm 2447 (dump): sump stripperTerm 2448 2449 * ACU_NGA_LhsAutomaton.hh (class ACU_NGA_LhsAutomaton): replaced 2450 stripperTopSymbol with stripperTerm 2451 (class ACU_NGA_LhsAutomaton): updated decl for 2452 ACU_NGA_LhsAutomaton() 2453 2454 * ACU_GreedyMatcher.cc (greedyMatch): use partialCompare() and 2455 findFirstPotentialMatch() 2456 2457 * ACU_Matcher.cc (eliminateGroundedOutAliens): use 2458 partialCompare() and findFirstPotentialMatch() 2459 (aliensOnlyMatch): use partialCompare() and 2460 findFirstPotentialMatch() 2461 (buildBipartiteGraph): use partialCompare() and 2462 findFirstPotentialMatch() 2463 2464 * ACU_LhsAutomaton.cc (addGroundedOutAlien): assign to term rather 2465 than topSymbol 2466 (addNonGroundAlien): assign to term rather than topSymbol 2467 2468 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): term replaces 2469 topSymbol in struct NonGroundAlien 2470 2471 * ACU_DagOperations.cc (findFirstPotentialMatch): added 2472 2473===================================Maude78================================================== 2474 24752003-01-02 Steven Eker <eker@goo.csl.sri.com> 2476 2477 * ACU_Term.hh (class ACU_Term): updated decl for 2478 tryToMakeCollectorLhsAutomaton() 2479 2480 * ACU_LhsCompiler0.cc (compileLhs2): use new 2481 tryToMakeCollectorLhsAutomaton() calling convention 2482 (tryToMakeCollectorLhsAutomaton): Allow collector variable to 2483 occur in context and/or condition as long as stripper is a ground 2484 term and we have no extension. This is ok because the ground term 2485 must strip exactly one occurence of itself from subject with the 2486 rest of the subject providing a unique binding for the collector 2487 24882002-12-20 Steven Eker <eker@goo.csl.sri.com> 2489 2490 * ACU_CollectorLhsAutomaton.cc (collect): optimized no sort check 2491 case 2492 (collect): optimized sort check case 2493 24942002-12-19 Steven Eker <eker@goo.csl.sri.com> 2495 2496 * ACU_DagOperations.cc (binarySearch): (Term* version): use 2497 setOnLs(), setOnGeq() 2498 24992002-12-17 Steven Eker <eker@goo.csl.sri.com> 2500 2501 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): added decl for 2502 handleElementVariables() 2503 2504 * ACU_Matcher.cc (handleElementVariables): added 2505 (fullMatch): use handleElementVariables() 2506 (buildBipartiteGraph): don't handle element variables here 2507 2508 * ACU_DagNormalization.cc (copyAndBinaryInsert): rewritten using 2509 resizeWithoutPreservation() 2510 (fastMerge): rewritten using resizeWithoutPreservation() 2511 25122002-12-16 Steven Eker <eker@goo.csl.sri.com> 2513 2514 * ACU_DagNormalization.cc (copyAndBinaryInsert): use fastCopy() in 2515 place of STL copy() (3 places) 2516 (fastMerge): use use fastCopy() in place of STL copy() (2 places) 2517 2518 * ACU_DagNode.hh (class ACU_DagNode): added decl for fastCopy() 2519 2520 * ACU_DagNormalization.cc (fastCopy): added 2521 2522 * ACU_DagNode.cc (markArguments): rewritten to avoid seperate 2523 iteration count 2524 25252002-11-22 Steven Eker <eker@goo.csl.sri.com> 2526 2527 * ACU_Subproblem.hh (class ACU_Subproblem): added decl for 2528 noVariableCase(); updated decl for oneVariableCase() 2529 2530 * ACU_Subproblem.cc (noVariableCase): added 2531 (oneVariableCase): generalized to handle the case where there may 2532 be multiple varibales but only one is unbound 2533 (extractDiophantineSystem): rewritten to handle a number of 2534 special cases efficiently 2535 2536 * ACU_Matcher.cc (buildBipartiteGraph): use new addEdge() calling 2537 convention 2538 (buildBipartiteGraph): use new addEdge() calling convention 2539 2540 * ACU_Subproblem.hh (class ACU_Subproblem): updated decl for 2541 addEdge() 2542 2543 * ACU_Subproblem.cc (addEdge): take difference rather than global 2544 and local bindings 2545 25462002-11-21 Steven Eker <eker@goo.csl.sri.com> 2547 2548 * ACU_Matcher.cc (buildBipartiteGraph): fixed bug we introduced by 2549 checking for matchable outside of the right scope 2550 2551 * ACU_Subproblem.hh (class ACU_Subproblem): updated decl for 2552 addPatternNode() 2553 2554 * ACU_Subproblem.cc (addPatternNode): return index to created 2555 pattern node 2556 2557 * ACU_Matcher.cc (buildBipartiteGraph): treat unbound variables 2558 that take exactly one subject as non-ground aliens 2559 (fullMatch): don't treat unbound variables that take exactly one 2560 subject as top variables 2561 25622002-11-20 Steven Eker <eker@goo.csl.sri.com> 2563 2564 * ACU_DagNode.cc (matchVariableWithExtension): now check & use 2565 sort bound 2566 25672002-11-19 Steven Eker <eker@goo.csl.sri.com> 2568 2569 * ACU_Subproblem.cc (oneVariableCase): partly optimized using 2570 iterators 2571 2572 * ACU_DagNormalization.cc (copyAndBinaryInsert): rewritten using 2573 iterators and copy() algorithm template 2574 (copyAndBinaryInsert): put back missing expandBy() 2575 (fastMerge):rewritten using iterators and copy() algorithm 2576 template 2577 2578 * ACU_NonLinearLhsAutomaton.hh (class ACU_NonLinearLhsAutomaton): 2579 updated decl for fillOutExtensionInfo() 2580 2581 * ACU_NonLinearLhsAutomaton.cc (match): rewritten using iterators 2582 to replace CONST_ARG_VEC_HACK() 2583 (fillOutExtensionInfo): pass chosen as a const 2584 ArgVec<ACU_DagNode::Pair>::const_iterator 2585 (match): new fillOutExtensionInfo() calling convention 2586 25872002-11-18 Steven Eker <eker@goo.csl.sri.com> 2588 2589 * ACU_DagOperations.cc (findFirstOccurrence): replaced 2590 CONST_ARG_VEC_HACK() with const_iterator 2591 (binarySearch): (both versions) replaced CONST_ARG_VEC_HACK() with 2592 const_iterator 2593 2594 * ACU_Matcher.cc (multiplicityChecks): rewritten using 2595 const_iterator in place of CONST_ARG_VEC_HACK() 2596 2597 * ACU_NonLinearLhsAutomaton.cc (fillOutExtensionInfo): rewritten 2598 using const_iterator in place of CONST_ARG_VEC_HACK() 2599 2600 * ACU_DagNode.cc (compareArguments): need to iterate backwards for 2601 consistancy 2602 2603 * ACU_RhsAutomaton.cc (buildArguments): rewritten using iterator 2604 in place of ARG_VEC_HACK() 2605 2606 * ACU_DagNode.cc (compareArguments): rewritten using 2607 iterators in place of CONST_ARG_VEC_HACK()s 2608 (partialReplace): rewritten using 2609 CONST_ARG_VEC_HACK()/ARG_VEC_HACK() 2610 2611 * ACU_CollectorLhsAutomaton.cc (collect): rewritten using 2612 itterators in place of CONST_ARG_VEC_HACK()/ARG_VEC_HACK() 2613 2614===================================Maude77================================================== 2615 26162002-11-07 Steven Eker <eker@goo.csl.sri.com> 2617 2618 * ACU_Subproblem.cc (solveVariables): 2619 DagNode::okToCollectGarbage() -> MemoryCell::okToCollectGarbage() 2620 26212002-11-06 Steven Eker <eker@goo.csl.sri.com> 2622 2623 * ACU_Subproblem.cc (oneVariableCase): try using set() rather 2624 than Pair(); on sparc this saves 1 ld instruction in loop - wins 2625 under quantify but loses in actual run - must be a sparc 2626 scheduling problem 2627 2628 * ACU_DagNode.hh (Pair): deleted as it loses 2629 (set): added 2630 2631 * ACU_Subproblem.cc (oneVariableCase): use ACU_DagNode::Pair() to 2632 see if enables g++ to generate better code 2633 2634 * ACU_DagNode.hh (Pair): added 2635 2636 * ACU_Subproblem.hh (class ACU_Subproblem): added decl for 2637 oneVariableCase() and updated decl for extractDiophantineSystem() 2638 2639 * ACU_Subproblem.cc (oneVariableCase): added 2640 (extractDiophantineSystem): use oneVariableCase(); take 2641 RewritingContext& since we need to pass it to oneVariableCase() 2642 26432002-11-05 Steven Eker <eker@goo.csl.sri.com> 2644 2645 * ACU_Subproblem.cc (extractDiophantineSystem): deleted 2646 excessively cute trivial case code; if we have no subjects but can 2647 succeed by binding unbound variables to the identity, do the 2648 binding here rather than in solveVariables() 2649 (solveVariables): don't do identity binding in null system case; 2650 code reorganized to share unbinding loop 2651 (extractDiophantineSystem): use clear() 2652 2653 * ACU_Matcher.cc (multiplicityChecks): replaced VECTOR_HACK() with 2654 Vector<int>::iterator 2655 2656 * ACU_RhsAutomaton.cc (buildArguments): replaced 2657 CONST_VECTOR_HACK() with Vector<Argument>::const_iterator 2658 26592002-10-28 Steven Eker <eker@goo.csl.sri.com> 2660 2661 * ACU_LhsCompiler0.cc (compileLhs2): added DebugAdvisory() for 2662 when we fail to produce heuristic ACU automaton 2663 26642002-10-16 Steven Eker <eker@goo.csl.sri.com> 2665 2666 * ACU_Symbol.hh (class ACU_Symbol): postInterSymbolPass() -> 2667 postOpDeclarationPass() 2668 2669 * ACU_Symbol.cc (postInterSymbolPass): becomes 2670 postOpDeclarationPass() since sort tables arem't computed at 2671 postInterSymbolPass time 2672 26732002-10-07 Steven Eker <eker@goo.csl.sri.com> 2674 2675 * ACU_DagNode.cc (copyWithReplacement): complex version: rewritten 2676 to fix a serious bug where we were relying on unstackable flags to 2677 figure out when args had been stacked and needed 2678 replacement. Since unstackable flags can be set after stacking 2679 this approach fails badly, corrupting the dag node 2680 26812002-10-04 Steven Eker <eker@goo.csl.sri.com> 2682 2683 * ACU_DagNode.hh (class ACU_DagNode): updated decl for the more 2684 complex copyWithReplacement() 2685 2686 * ACU_DagNode.cc (copyWithReplacement): rewritten to handle 2687 situation where only some args are stacked. 2688 2689 * ACU_Symbol.cc (stackArguments): we no longer stack all 2690 arguments; if we have frozen arguments we don't stack anything; 2691 otherwise we stack only those arguments that have not been flagged 2692 as unstackable 2693 26942002-10-03 Steven Eker <eker@goo.csl.sri.com> 2695 2696 * ACU_DagNode.hh (class ACU_DagNode): updated decl for 2697 stackArguments() 2698 2699 * ACU_DagNode.cc (stackArguments): handle respectFrozen argument 2700 2701===================================Maude76================================================== 2702 27032002-08-02 Steven Eker <eker@goo.csl.sri.com> 2704 2705 * ACU_Term.cc (compileRhs2): added code to flag last use of each 2706 source 2707 27082002-07-24 Steven Eker <eker@goo.csl.sri.com> 2709 2710 * ACU_LhsCompiler3.cc (findLongestIncreasingSequence): same as 2711 below 2712 2713 * ACU_LhsCompiler0.cc (tryToMakeAlienAlienLhsAutomaton): pass 2714 sameVariableSet = true to calls of subsumes() since both subterms 2715 are from the same pattern 2716 2717===================================Maude74================================================== 2718 27192002-05-13 Steven Eker <eker@goo.csl.sri.com> 2720 2721 * ACU_Symbol.hh (class ACU_Symbol): added decl for multiplicities 2722 version of makeDagNode() 2723 2724 * ACU_Symbol.cc (makeDagNode): added multiplicities version; this 2725 is so that derived symbol classes can build new AC_DagNodes from 2726 old ones with reasonable efficiency 2727 27282002-05-10 Steven Eker <eker@goo.csl.sri.com> 2729 2730 * ACU_Symbol.hh (class ACU_Symbol): added decl for 2731 reduceArgumentsAndNormalize() 2732 (class ACU_Symbol): added defaults for strategy and memo args 2733 2734 * ACU_Symbol.cc (reduceArgumentsAndNormalize): added; this is a 2735 special purpose function the all ACU builtin symbols to get an ACU 2736 dag in normal form 2737 2738===================================Maude72================================================== 2739 27402002-03-11 Steven Eker <eker@goo.csl.sri.com> 2741 2742 * ACU_Term.cc: deleted explicit template instantiation 2743 2744 * ACU_Subproblem.cc: deleted explicit template instantiation 2745 2746 * ACU_RhsAutomaton.cc: deleted explicit template instantiation 2747 2748 * ACU_DagNode.cc: deleted explicit template instantiation 2749 2750 * ACU_LhsAutomaton.cc: deleted explicit template instantiations 2751 2752===================================Maude71================================================== 2753 27542001-12-10 Steven Eker <eker@goo.csl.sri.com> 2755 2756 * ACU_DagNode.hh (class ACU_DagNode): made class 2757 ACU_DagArgumentIterator a friend 2758 2759 * ACU_Term.hh (class ACU_Term): made class ACU_ArgumentIterator a 2760 friend 2761 2762===================================Maude69================================================== 2763 27642001-04-03 Steven Eker <eker@goo.csl.sri.com> 2765 2766 * ACU_DagNode.hh (class ACU_DagNode): added decl for 2767 Vector<RedexPosition> version of copyWithReplacement() 2768 2769 * ACU_DagNode.cc (copyWithReplacement): added 2770 (Vector<RedexPosition> version) 2771 2772===================================Engine66================================================== 2773 27742001-03-08 Steven Eker <eker@goo.csl.sri.com> 2775 2776 * ACU_Symbol.hh (class ACU_Symbol): added decl for 2777 stackArguments() 2778 2779 * ACU_Symbol.cc (stackArguments): added 2780 2781===================================Engine65================================================== 2782 27832001-01-26 Steven Eker <eker@goo.csl.sri.com> 2784 2785 * ACU_DagNode.hh (class ACU_DagNode): updated decl for 2786 markArguments() and made it private 2787 2788 * ACU_DagNode.cc (markArguments): rewritten with new semantics 2789 2790===================================Engine64================================================== 2791 27922000-08-02 Steven Eker <eker@goo.csl.sri.com> 2793 2794 * ACU_DagNode.cc (matchVariableWithExtension): don't pass 2795 inErrorSort arg to ACU_Subproblem() 2796 2797 * ACU_Subproblem.cc (ACU_Subproblem): no longer take inErrorSort 2798 arg 2799 (dump): don't dump inErrorSort data member 2800 (solveVariables): don't test inErrorSort (2 places) 2801 2802 * ACU_Subproblem.hh (class ACU_Subproblem): ctor decl no longer 2803 has inErrorSort flag 2804 (class ACU_Subproblem): deleted data member inErrorSort 2805 2806 * ACU_Matcher.cc (buildBipartiteGraph): don't pass inErrorSort 2807 flag to ACU_Subproblem() 2808 2809 * ACU_LhsAutomaton.cc (ACU_LhsAutomaton): don't take inErrorSort 2810 arg 2811 (dump): don't dump inErrorSort data member 2812 2813 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): deleted data 2814 member inErrorSort 2815 (class ACU_LhsAutomaton): updared ctor decl 2816 2817 * ACU_LhsCompiler1.cc (compileLhs3): no longer care if pattern is 2818 in error sort; don't pass inErrorSort flags to ACU_LhsAutomaton() 2819 2820 * ACU_LhsCompiler0.cc (compileLhs2): no longer care if pattern is 2821 in error sort 2822 (tryToMakeNonLinearLhsAutomaton): no longer care if pattern is 2823 in error sort 2824 2825 * ACU_Symbol.cc (complexStrategy): greatly simplified now that we 2826 no longer treat last strategy zero specially when term is in the 2827 error sort 2828 (memoStrategy): ditto 2829 2830 * ACU_DagNode.hh (class ACU_DagNode): assumption "our sort 2831 (which may not be known) is not the error sort." for the 2832 ASSIGNMENT case is no longer true 2833 28342000-07-31 Steven Eker <eker@goo.csl.sri.com> 2835 2836 * ACU_Symbol.cc (computeBaseSort): don't handle union sorts 2837 2838===================================Engine61================================================== 2839 28402000-07-28 Steven Eker <eker@goo.csl.sri.com> 2841 2842 * ACU_RhsAutomaton.cc (remapIndices): added 2843 2844 * ACU_RhsAutomaton.hh (class ACU_RhsAutomaton): added decl for 2845 remapIndices() 2846 28472000-07-26 Steven Eker <eker@goo.csl.sri.com> 2848 2849 * ACU_LhsCompiler1.cc (compileLhs3): use 2850 getNrProtectedVariables() instead of nrVariables() 2851 2852 * ACU_LhsCompiler0.cc (tryToMakeAlienAlienLhsAutomaton): use 2853 getNrProtectedVariables() instead of nrVariables() 2854 (tryToMakeCollectorLhsAutomaton): use getNrProtectedVariables() 2855 instead of nrVariables() 2856 2857 * ACU_Term.cc (insertAbstractionVariables): use 2858 makeProtectedVariable() instead of makeAbstractionVariable() 2859 (compileRhs2): use makeConstructionIndex() instead of 2860 allocateIndex() 2861 28622000-07-25 Steven Eker <eker@goo.csl.sri.com> 2863 2864 * ACU_Term.cc (findAvailableTerms): don't insert ground terms into 2865 availableTerms since we can't do left->right sharing on them 2866 2867 * ACU_LhsAutomaton.cc (dump): cast Bool member before print so 2868 they don't print out as chars 2869 2870 * ACU_RhsAutomaton.cc (construct): don't call buildAliens() 2871 (replace): don't call buildAliens() 2872 (dump): don't call RhsAutomaton::dump() 2873 2874 * ACU_Term.hh (class ACU_Term): deleted decl for compileRhs() 2875 2876 * ACU_Term.cc (compileRhs): deleted 2877 2878===================================Engine60================================================== 2879 28802000-07-18 Steven Eker <eker@goo.csl.sri.com> 2881 2882 * ACU_LhsCompiler0.cc (tryToMakeNonLinearLhsAutomaton): use 2883 getConditionVariables() 2884 (tryToMakeCollectorLhsAutomaton): use getConditionVariables() 2885 2886 * ACU_LhsCompiler1.cc (compileLhs3): use getConditionVariables() 2887 28882000-07-12 Steven Eker <eker@goo.csl.sri.com> 2889 2890 * ACU_Term.cc (compileRhs2): call addRhsAutomaton() 2891 28922000-07-11 Steven Eker <eker@goo.csl.sri.com> 2893 2894 * ACU_Term.cc (findAvailableTerms): added 2895 (compileRhs2): added 2896 2897 * ACU_Term.hh (class ACU_Term): added declarations for 2898 findAvailableTerms() and compileRhs2() 2899 2900===================================Engine59================================================== 2901 2902 29032000-07-05 Steven Eker <eker@goo.csl.sri.com> 2904 2905 * ACU_LhsCompiler0.cc (compileLhs2): call to compileLhs2() becomes 2906 call to compileLhs3() 2907 2908 * ACU_LhsCompiler1.cc (compileLhs2): becomes compileLhs3() 2909 2910 * ACU_Term.hh (class ACU_Term): old compileLhs2() -> compileLhs3() 2911 2912 * ACU_LhsCompiler0.cc (compileLhs): becomes compileLhs2() 2913 2914 * ACU_Term.hh (class ACU_Term): compileLhs() -> compileLhs2() 2915 29162000-06-23 Steven Eker <eker@goo.csl.sri.com> 2917 2918 * ACU_Term.cc (compileRhs): modifiedIndex() -> getModifiedIndex() 2919 2920 * ACU_VarLhsAutomaton.cc (ACU_VarLhsAutomaton): index() -> 2921 getIndex() 2922 (ACU_VarLhsAutomaton): lookupSort() -> getSort() 2923 2924 * ACU_LhsCompiler1.cc (analyseConstraintPropagation): index() -> 2925 getIndex() 2926 (compileLhs2): index() -> getIndex() 2927 2928 * ACU_LhsCompiler0.cc (tryToMakeCollectorLhsAutomaton): index() -> 2929 getIndex() 2930 (tryToMakeNonLinearLhsAutomaton): index() -> getIndex() 2931 (tryToMakeNonLinearLhsAutomaton): lookupSort() -> getSort() 2932 (tryToMakeCollectorLhsAutomaton): lookupSort() -> getSort() 2933 2934 * ACU_LhsAutomaton.cc (addTopVariable): lookupSort() -> getSort() 2935 (addTopVariable): index() -> getIndex() 2936 2937 * ACU_CollectorLhsAutomaton.cc (ACU_CollectorLhsAutomaton): 2938 index() -> getIndex() 2939 (ACU_CollectorLhsAutomaton): lookupSort() -> getSort() 2940 2941===================================Engine58================================================== 2942 29432000-03-17 Steven Eker <eker@goo.csl.sri.com> 2944 2945 * ACU_VarLhsAutomaton.hh (class ACU_VarLhsAutomaton): use 2946 NO_COPYING() macro; ifdef'd dump() decl 2947 2948 * ACU_Term.cc (dump): ifdef'd 2949 2950 * ACU_Term.hh (class ACU_Term): use NO_COPYING() macro; ifdef'd 2951 dump() decl 2952 2953 * ACU_Subproblem.cc (dump): ifdef'd 2954 2955 * ACU_Subproblem.hh (class ACU_Subproblem): use NO_COPYING() 2956 macro; ifdef'd dump() decl 2957 2958 * ACU_RhsAutomaton.cc (dump): ifdef'd 2959 2960 * ACU_RhsAutomaton.hh (class ACU_RhsAutomaton): use NO_COPYING() 2961 macro; ifdef'd dump() decl 2962 2963 * ACU_NonLinearLhsAutomaton.cc (dump): ifdef'd 2964 2965 * ACU_NonLinearLhsAutomaton.hh (class ACU_NonLinearLhsAutomaton): 2966 use NO_COPYING() macro; ifdef'd dump() decl 2967 2968 * ACU_NGA_LhsAutomaton.cc (dump): ifdef'd 2969 2970 * ACU_NGA_LhsAutomaton.hh (class ACU_NGA_LhsAutomaton): use 2971 NO_COPYING() macro; ifdef'd dump() decl 2972 2973 * ACU_LhsAutomaton.cc (dump): ifdef'd 2974 2975 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): use NO_COPYING() 2976 macro; ifdef'd dump() decl 2977 2978 * ACU_GndLhsAutomaton.cc (dump): ifdef'd 2979 2980 * ACU_GndLhsAutomaton.hh (class ACU_GndLhsAutomaton): use 2981 NO_COPYING() macro; ifdef'd dump() decl 2982 2983 * ACU_CollectorLhsAutomaton.cc (dump): ifdef'd 2984 2985 * ACU_CollectorLhsAutomaton.hh (class ACU_CollectorLhsAutomaton): 2986 use NO_COPYING() macro; ifdef'd dump() decl 2987 2988 * ACU_AlienAlienLhsAutomaton.cc (dump): ifdef'd 2989 2990 * ACU_AlienAlienLhsAutomaton.hh (class 2991 ACU_AlienAlienLhsAutomaton): use NO_COPYING() macro; ifdef'd 2992 dump() decl 2993 2994 * ACU_Symbol.cc (complexStrategy): AdvisoryCheck() -> IssueAdvisory() 2995 (memoStrategy): AdvisoryCheck() -> IssueAdvisory() 2996 29972000-03-13 Steven Eker <eker@goo.csl.sri.com> 2998 2999 * ACU_NonLinearLhsAutomaton.cc (match): fixed nasty bug: 3000 if (nrArgs == 1 || args[0].multiplicity == fastMult) should be 3001 if (nrArgs == 1 && args[0].multiplicity == fastMult) 3002 3003===================================Engine56================================================== 3004 30052000-01-31 Steven Eker <eker@goo.csl.sri.com> 3006 3007 * ACU_Subproblem.cc (solveVariables): allow collection of garbage 3008 in fail case to avoid build up of failed solutions 3009 3010===================================Engine54================================================== 3011 30121999-11-03 Steven Eker <eker@goo.csl.sri.com> 3013 3014 * ACU_Symbol.hh (class ACU_Symbol): added decl for memoStrategy() 3015 3016 * ACU_Symbol.cc (memoStrategy): added 3017 (complexStrategy): simplified using revised MemoTable 3018 (memoStrategy): simplified using revised MemoTable 3019 30201999-11-01 Steven Eker <eker@goo.csl.sri.com> 3021 3022 * ACU_Symbol.cc (eqRewrite): use standardStrategy() 3023 30241999-10-29 Steven Eker <eker@goo.csl.sri.com> 3025 3026 * ACU_Symbol.cc (ACU_Symbol): use new AssociativeSymbol 3027 conventions 3028 3029===================================Engine53================================================== 3030 30311999-10-26 Steven Eker <eker@goo.csl.sri.com> 3032 3033 * ACU_LhsCompiler1.cc (analyseConstraintPropagation): 3034 VariableTerm::dynamicCast() -> dynamic_cast<VariableTerm*>() 3035 (compileLhs2): VariableTerm::dynamicCast() -> 3036 dynamic_cast<VariableTerm*>() 3037 3038 * ACU_LhsCompiler0.cc (tryToMakeNonLinearLhsAutomaton): 3039 VariableTerm::dynamicCast() -> dynamic_cast<VariableTerm*>() 3040 (tryToMakeCollectorLhsAutomaton): VariableTerm::dynamicCast() -> 3041 dynamic_cast<VariableTerm*>() (*2) 3042 3043 * ACU_Term.cc (compileRhs): VariableTerm::dynamicCast() -> 3044 dynamic_cast<VariableTerm*>() 3045 (insertAbstractionVariables): VariableTerm::dynamicCast() -> 3046 dynamic_cast<VariableTerm*>() 3047 3048 * ACU_Symbol.cc (ACU_Symbol): added memoFlag arg 3049 3050 * ACU_Symbol.hh (class ACU_Symbol): added memoFlag arg to ctor 3051 decl 3052 30531999-10-19 Steven Eker <eker@goo.csl.sri.com> 3054 3055 * ACU_DagNode.cc (getHashValue): added 3056 3057 * ACU_DagNode.hh (class ACU_DagNode): added decl for 3058 getHashValue() 3059 3060===================================Engine52================================================== 3061 30621999-08-02 Steven Eker <eker@goo.csl.sri.com> 3063 3064 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): decl for 3065 topVariableCompare() replaced by decl for topVariableLt() 3066 3067 * ACU_LhsAutomaton.cc (complete): use STL sort function 3068 (topVariableCompare): becomes topVariableLt() 3069 3070 * ACU_Term.hh (class ACU_Term): decl for pairCompare() replaced by 3071 decl for pairLt() 3072 3073 * ACU_Term.cc (normalize): use STL sort function 3074 (pairCompare): becomes pairLt() 3075 30761999-06-08 Steven Eker <eker@goo.csl.sri.com> 3077 3078 * ACU_Symbol.hh (class ACU_Symbol): added decl for complexStrategy() 3079 3080 * ACU_Symbol.cc (complexStrategy): added, taking guts from eqRewrite() 3081 (eqRewrite): rewritten using complexStrategy() 3082 3083 * ACU_NonLinearLhsAutomaton.cc (match): CONST_ARG_VEC_HACK 3084 (fillOutExtensionInfo): CONST_ARG_VEC_HACK 3085 (match): fastMult hack - register copy of multiplicity to avoid 3086 reloading after writes to memory 3087 3088 * ACU_VarLhsAutomaton.cc (match): very minor optimization using 3089 temporary to hold pointer to (potentially) stripped term 3090 3091 * ACU_DagOperations.cc (eliminateSubject): updated calling 3092 convention for binarySearch() (2 places) 3093 (eliminateArgument): updated calling convention for binarySearch() 3094 3095 * ACU_DagNormalization.cc (copyAndBinaryInsert): updated calling 3096 convention for binarySearch() 3097 (binaryInsert): updated calling convention for binarySearch() 3098 3099 * ACU_GndLhsAutomaton.cc (match): updated calling convention for 3100 binarySearch() 3101 3102 * ACU_NGA_LhsAutomaton.cc (match): updated calling 3103 convention for findFirstOccurrence() 3104 3105 * ACU_Matcher.cc (eliminateGroundedOutAliens): updated calling 3106 convention for findFirstOccurrence() 3107 (aliensOnlyMatch): updated calling convention for 3108 findFirstOccurrence() 3109 (buildBipartiteGraph): updated calling convention for 3110 findFirstOccurrence() 3111 (eliminateGroundAliens): updated calling convention for 3112 binarySearch() 3113 3114 * ACU_GreedyMatcher.cc (greedyMatch): updated calling convention 3115 for findFirstOccurrence() 3116 3117 * ACU_AlienAlienLhsAutomaton.cc (match): updated calling convention 3118 for findFirstOccurrence() (2 places) 3119 3120 * ACU_DagNode.hh (class ACU_DagNode): updated decls for 3121 findFirstOccurrence() and binarySearch (both versions) 3122 3123 * ACU_DagOperations.cc (findFirstOccurrence): made into member 3124 function; use CONST_ARG_VEC_HACK() 3125 (binarySearch): (both versions): made into member function; use 3126 CONST_ARG_VEC_HACK() 3127 31281999-06-07 Steven Eker <eker@goo.csl.sri.com> 3129 3130 * ACU_CollectorLhsAutomaton.cc (collect): simplified the case 3131 where there's only one unstripped arg and no new ACU_DagNode is 3132 needed 3133 (collect): loses so try another rearrangement 3134 (collect): yet another rearrangement 3135 (collect): 4th attempt 3136 (collect): 5th attempt 3137 31381999-06-03 Steven Eker <eker@goo.csl.sri.com> 3139 3140 * ACU_DagNormalization.cc (fastMerge): take ACU_DagNode* 3141 rather than ArgVec<Pair>& for both args 3142 (normalizeAtTop): updated calling convention for fastMerge() 3143 (flattenSortAndUniquize): fixed bug that we introduced, since we 3144 were originally calling mergeSortAndUniquize() on newArray rather 3145 than argArray; now swap them before the call. 3146 3147 * ACU_DagNode.hh (class ACU_DagNode): updated 3148 copyAndBinaryInsert() decl 3149 3150 * ACU_DagNormalization.cc (copyAndBinaryInsert): take ACU_DagNode* 3151 rather than ArgVec<Pair>& as 1st arg 3152 (normalizeAtTop): pass ACU_DagNode* rather than ArgVec<Pair> to 3153 copyAndBinaryInsert() (2 places) 3154 3155 * ACU_DagNode.hh (class ACU_DagNode): updated decl for 3156 mergeSortAndUniquize() 3157 3158 * ACU_DagNormalization.cc (mergeSortAndUniquize): get rid of 3159 runs arg and use runsBuffer directly 3160 (sortAndUniquize): don't pass runsBuffer to mergeSortAndUniquize() 3161 (flattenSortAndUniquize): don't pass runsBuffer to 3162 mergeSortAndUniquize() 3163 (extensionNormalizeAtTop): don't pass runsBuffer to 3164 mergeSortAndUniquize() 3165 3166 * ACU_DagNode.hh (class ACU_DagNode): updated decl for 3167 mergeSortAndUniquize(), no longer static 3168 3169 * ACU_DagNormalization.cc (mergeSortAndUniquize): removed argArray 3170 arg; now going to be a member function 3171 (sortAndUniquize): call mergeSortAndUniquize() like a member 3172 function 3173 (flattenSortAndUniquize): call mergeSortAndUniquize() like a member 3174 function 3175 (extensionNormalizeAtTop): call mergeSortAndUniquize() like a member 3176 function 3177 31781999-06-01 Steven Eker <eker@goo.csl.sri.com> 3179 3180 * ACU_DagNode.hh (class ACU_DagNode): update decl for binaryInsert() 3181 3182 * ACU_DagNormalization.cc (binaryInsert): moved here as it its 3183 only used for normalization 3184 (binaryInsert): first arg deleted; made non-static 3185 (extensionNormalizeAtTop): use new binaryInsert() calling convention 3186 3187 * ACU_DagNode.cc (partialReplace): added ARG_VEC_HACK 3188 (partialReplace): changed for() loop into do-while loop 3189 3190 * ACU_CollectorLhsAutomaton.cc (collect): replaced SPEED_HACK with 3191 CONST_ARG_VEC_HACK and ARG_VEC_HACK for cleaness 3192 3193 * ACU_DagNode.cc (compareArguments): replaced SPEED_HACK with 3194 CONST_ARG_VEC_HACKs for cleaness 3195 (markArguments): replaced SPEED_HACK with CONST_ARG_VEC_HACK for 3196 cleaness 3197 (markArguments): converted for() loop into do-while since we 3198 always have at least 1 arg 3199 3200 * ACU_Matcher.cc (multiplicityChecks): replaced SPEED_HACKs with 3201 CONST_ARG_VEC_HACK and VECTOR_HACK for cleaness 3202 3203 * ACU_RhsAutomaton.cc (buildArguments): replaced SPEED_HACK with 3204 ARG_VEC_HACK and CONST_VECTOR_HACK for cleaness 3205 3206 * ACU_DagNormalization.cc (fastMerge): add heursitic to try and 3207 avoid full merge 3208 (fastMerge): removed previous heursitic as it seems to lose on 3209 average 3210 3211 * ACU_DagNode.hh (class ACU_DagNode): added decl for fastMerge() 3212 3213 * ACU_DagNormalization.cc (fastMerge): added 3214 (normalizeAtTop): call fastMerge() 3215 3216 * ACU_DagNode.hh (class ACU_DagNode): updated decls for 3217 binarySearch() (both versions) and copyAndBinaryInsert() 3218 3219 * ACU_DagNormalization.cc (copyAndBinaryInsert): use ARG_VEC_HACKs 3220 3221 * ACU_DagOperations.cc (binarySearch): (both versions) made first 3222 arg const 3223 3224 * ACU_DagNormalization.cc (normalizeAtTop): fix bug where we were 3225 using copyAndBinaryInsert() even when the arg to be flattened in 3226 had arity > 1 3227 (copyAndBinaryInsert): make first arg const 3228 32291999-05-28 Steven Eker <eker@goo.csl.sri.com> 3230 3231 * ACU_DagNormalization.cc (copyAndBinaryInsert): fixed bug; we 3232 were searching in argArray rarther than source 3233 (normalizeAtTop): rearranged if statements to favor common cases 3234 3235 * ACU_DagNode.hh (class ACU_DagNode): added decl for copyAndBinaryInsert() 3236 3237 * ACU_DagNormalization.cc (fastNormalizeAtTop): added 3238 (copyAndBinaryInsert): added 3239 (flattenSortAndUniquize): no longer local inline 3240 (sortAndUniquize): no longer local inline 3241 (normalizeAtTop): incorporate fastNormalizeAtTop() 3242 (fastNormalizeAtTop): deleted 3243 32441999-05-16 Steven Eker <eker@goo.csl.sri.com> 3245 3246 * ACU_DagNode.cc (markArguments): added SPEED_HACK 3247 3248 * ACU_AlienAlienLhsAutomaton.cc: find first occurence of second 3249 symbol before entering outermost loop 3250 3251 * ACU_CollectorLhsAutomaton.cc (ACU_CollectorLhsAutomaton): set 3252 noSortChecks flag if the collector variable has a sort that is the 3253 unique maximal sort in an error free component 3254 (ACU_CollectorLhsAutomaton): indicate "sort checks off" by setting 3255 collectorSort to 0 3256 (collect): handle "sort checks off" in the 3 cases with superfast 3257 loops in the main case 3258 (dump): handle "sort checks off" 3259 32601999-05-13 Steven Eker <eker@goo.csl.sri.com> 3261 3262 * ACU_DagNode.cc (makeClone): copy theory byte 3263 (overwriteWithClone): copy theory byte 3264 32651999-05-12 Steven Eker <eker@goo.csl.sri.com> 3266 3267 * ACU_Symbol.hh (class ACU_Symbol): computeTrueSort() -> 3268 normalizeAndComputeTrueSort() 3269 3270 * ACU_Symbol.cc (computeTrueSort): become 3271 normalizeAndComputeTrueSort() 3272 (normalizeAndComputeTrueSort): use fastComputeTrueSort() 3273 32741999-05-11 Steven Eker <eker@goo.csl.sri.com> 3275 3276 * ACU_RhsAutomaton.cc (buildArguments): made local_inline 3277 (buildArguments): added SPEED_HACK 3278 3279===================================Engine49================================================== 3280 32811999-04-18 Steven Eker <eker@goo.csl.sri.com> 3282 3283 * Unmade previous chnage in all files due to huge number of 3284 functions that should have been in-lined but weren't (ans not 3285 reported either!) length(), expandTo(), contractTo() 3286 32871999-03-14 Steven Eker <eker@goo.csl.sri.com> 3288 3289 * ACU_Subproblem.cc: try commenting out template decls 3290 3291 * ACU_LhsAutomaton.cc: try commenting out template decls 3292 3293 * ACU_RhsAutomaton.cc: try commenting out template decls 3294 3295 * ACU_DagNode.cc: try commenting out template decls 3296 3297 * ACU_Term.cc: try commenting out template decls 3298 3299===================================Maude 1.0.2 released======================================= 3300===================================Maude 1.0.1 released======================================= 3301 33021999-02-18 Steven Eker <eker@goo.csl.sri.com> 3303 3304 * ACU_RhsAutomaton.cc (buildArguments): for() changed to 3305 do-while() 3306 3307===================================VectorExperiment========================================== 3308 33091999-01-19 Steven Eker <eker@goo.csl.sri.com> 3310 3311 * ACU_LhsCompiler0.cc (tryToMakeAlienAlienLhsAutomaton): fixed 3312 nasty long running bug where we were not dealing correctly with 3313 UNDECIDED from Term::subsumes() 3314 33151999-01-16 Steven Eker <eker@goo.csl.sri.com> 3316 3317 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): changed 3318 matchAtTop, inErrorSort and collapsePossible to Bool to save memory 3319 (class ACU_LhsAutomaton): changed matchStrategy to Byte to save memory 3320 3321 * ACU_Term.hh (class ACU_Term): made 3322 Pair::abstractionVariableIndex a short to save memory 3323 3324===================================Engine46================================================== 3325 3326Tue Dec 8 10:48:45 1998 Steven Eker <eker@lilac.csl.sri.com> 3327 3328 * ACU_Term.cc (Term): fixed nasty bug where we were not copying 3329 multiplicity correctly 3330 3331===================================Engine44================================================== 3332 3333Fri Nov 6 15:30:44 1998 Steven Eker <eker@lilac.csl.sri.com> 3334 3335 * ACU_Term.cc (deepCopy): -> deepCopy2() 3336 3337 * ACU_Term.hh (class ACU_Term): deepCopy() -> deepCopy2() 3338 3339===================================Engine43================================================== 3340 3341Wed Oct 28 14:41:53 1998 Steven Eker <eker@lilac.csl.sri.com> 3342 3343 * ACU_AlienAlienLhsAutomaton.cc (match): fixed nasty bug in 3344 extension setting code: e->setUnmatched(i, m); becomes 3345 e->setUnmatched(k, m); 3346 3347Thu Oct 8 13:41:45 1998 Steven Eker <eker@lilac.csl.sri.com> 3348 3349 * ACU_Term.cc (compareArguments): (DagNode* version) added 3350 const_cast 3351 (compareArguments): (DagNode* version) removed const_cast, added 3352 const 3353 (compareArguments): (Term* version) added const 3354 3355 * ACU_Term.hh: added #include "ACU_Symbol.hh" so that we can down 3356 cast everwhere in symbol() 3357 3358Fri Oct 2 11:20:43 1998 Steven Eker <eker@lilac.csl.sri.com> 3359 3360 * ACU_Matcher.cc (multiplicityChecks): added SPEED_HACKS 3361 (multiplicityChecks): rewritten; simpler and much faster in the 3362 maxPatternMultiplicity > 1 fail case at the cost of being slightly 3363 slower (or maybe not?) in the success case. When 3364 maxPatternMultiplicity > 1 failure seems to be _much_ more 3365 likely. 3366 3367===================================Engine41================================================== 3368 3369Tue Sep 22 14:52:16 1998 Steven Eker <eker@lilac.csl.sri.com> 3370 3371 * ACU_Symbol.cc (computeBaseSort): use lastIndex heuristic in 3372 uniform sort structure case 3373 3374 * ACU_CollectorLhsAutomaton.cc (collect): put collectorSort 3375 pointer into local variable to avoid reload; Use lastIndex 3376 heuristic to try and avoid sort comparisons; use leq(int, Sort*) 3377 instead of DagNode::Sort* where neccessary 3378 3379Fri Sep 18 11:28:08 1998 Steven Eker <eker@lilac.csl.sri.com> 3380 3381 * ACU_DagNode.cc (overwriteWithClone): use setSortIndex() 3382 (makeClone): use setSortIndex() 3383 3384 * ACU_Symbol.cc (computeBaseSort): rewritten using setSortIndex(), 3385 DagNode::leq(), traverse() and lookupSortIndex() 3386 3387Thu Sep 17 18:17:18 1998 Steven Eker <eker@lilac.csl.sri.com> 3388 3389 * ACU_VarLhsAutomaton.cc (match): use DagNode::leq() (2 places) 3390 3391 * ACU_NonLinearLhsAutomaton.cc (match): use DagNode::leq() (5 3392 places) 3393 3394 * ACU_Matcher.cc (forcedLoneVariableCase): use DagNode::leq() 3395 3396 * ACU_GreedyMatcher.cc (greedyPureMatch): use DagNode::leq() (2 3397 places) 3398 (greedyPureMatch): use leq(Sort*,Sort*) 3399 3400 * ACU_CollectorLhsAutomaton.cc (collect): use DagNode::leq() (5 3401 places) 3402 3403Fri Sep 11 17:26:33 1998 Steven Eker <eker@lilac.csl.sri.com> 3404 3405 * ACU_Subproblem.cc (solveVariables): use new checkSort() convention 3406 3407 * ACU_Matcher.cc (forcedLoneVariableCase): use new checkSort() 3408 convention 3409 3410 * ACU_Symbol.cc (computeBaseSort): use <=(DagNode*,Sort&) (1 place) 3411 3412 * ACU_VarLhsAutomaton.cc (match): use <=(DagNode*,Sort&) (2 3413 places) 3414 3415 * ACU_NonLinearLhsAutomaton.cc (match): use <=(DagNode*,Sort&) 3416 (5 places) 3417 3418 * ACU_DagNode.cc (matchVariableWithExtension): pass sort rather 3419 than code to addTopVariable() 3420 3421 * ACU_Matcher.cc (forcedLoneVariableCase): use <=(DagNode*,Sort&) 3422 (fullMatch): pass sort rather than code to addTopVariable() 3423 3424 * ACU_GreedyMatcher.cc (greedyPureMatch): use <=(DagNode*,Sort&) 3425 (2 places) and <=(Sort&,Sort&) 3426 3427 * ACU_CollectorLhsAutomaton.cc (collect): use <=(DagNode*,Sort&) 3428 (5 places) 3429 3430 * ACU_Subproblem.cc (addTopVariable): store sort rather than sortCode 3431 (solveVariables): temporary hack: pass sort->code() to checkSort() 3432 (dump): sort rather than sortCode 3433 3434 * ACU_Subproblem.hh (class ACU_Subproblem): struct TopVariable now 3435 has sort rather than sortCode; addTopVariable() decl updated 3436 3437Wed Sep 9 11:52:44 1998 Steven Eker <eker@lilac.csl.sri.com> 3438 3439 * ACU_Symbol.cc (compileOpDeclarations): call 3440 commutativeSortCompletion() before Symbol::compileOpDeclarations() 3441 due to new implementation 3442 3443===================================Engine40================================================== 3444 3445Mon Jul 20 19:35:25 1998 Steven Eker <eker@lilac.csl.sri.com> 3446 3447 * ACU_Term.hh (class ACU_Term): added decl for new ctor 3448 3449 * ACU_Term.cc (deepCopy): added 3450 (ACU_Term): added new ctor 3451 3452 * ACU_Term.hh (class ACU_Term): added decl for deepCopy() 3453 3454===================================Engine39================================================== 3455 3456Wed Jun 10 11:57:08 1998 Steven Eker <eker@lilac.csl.sri.com> 3457 3458 * ACU_Symbol.cc (postInterSymbolPass): added to do identity stuff 3459 (compileOpDeclarations): don't do identity stuff here anymore 3460 3461 * ACU_Term.hh (class ACU_Term): updated 3462 normalizeAliensAndFlatten() and normalize() decls 3463 3464 * ACU_Term.cc: IntSet -> NatSet 3465 (normalize): go back to getIdentity(); set changed flag if 3466 normalization made any changes to term; clear changed otherwise 3467 (normalizeAliensAndFlatten): return flag to say wether we changed term 3468 3469 * ACU_LhsCompiler3.cc: IntSet -> NatSet 3470 3471 * ACU_LhsCompiler2.cc: IntSet -> NatSet 3472 3473 * ACU_LhsCompiler1.cc: IntSet -> NatSet 3474 3475 * ACU_LhsCompiler0.cc: IntSet -> NatSet 3476 3477 * ACU_Term.hh: IntSet -> NatSet 3478 3479===================================Engine38================================================== 3480 3481Wed Jun 3 16:29:33 1998 Steven Eker <eker@lilac.csl.sri.com> 3482 3483 * ACU_Term.cc (normalize): use earlyGetIdentity() 3484 3485===================================Engine37================================================== 3486 3487Fri Mar 6 17:22:37 1998 Steven Eker <eker@lilac.csl.sri.com> 3488 3489 * ACU_DagOperations.cc (eliminateSubject): fixed nasty bug - test 3490 should be identity != 0 && identity->equal(target) and we had || 3491 3492Tue Feb 24 11:10:10 1998 Steven Eker <eker@lilac.csl.sri.com> 3493 3494 * ACU_Matcher.cc (eliminateBoundVariables): simplify now that 3495 eliminateSubject() handle identity 3496 3497 * ACU_DagOperations.cc (eliminateSubject): handle identity; this 3498 fixes a serious bug in ACU_Subproblem::extractDiophantineSystem() 3499 which assumed we were 3500 3501 * ACU_Subproblem.cc (dump): added 3502 (dump): dump local bindings 3503 (solveVariables): fixed serious bug - in the trivial Diophantine 3504 system case where findFirst is false we must unbind any variables 3505 we bound to the identity the first time around before returning false. 3506 3507 * ACU_Subproblem.hh (class ACU_Subproblem): added decl for dump() 3508 3509Fri Feb 20 17:27:13 1998 Steven Eker <eker@lilac.csl.sri.com> 3510 3511 * ACU_DagNode.cc (stackArguments): only stack arguments that are 3512 not flagged as unstackable 3513 3514===================================Engine36================================================== 3515 3516Sat Feb 14 14:45:02 1998 Steven Eker <eker@lilac.csl.sri.com> 3517 3518 * ACU_LhsAutomaton.cc (ACU_LhsAutomaton): need to delete 3519 uniqueCollapseAutomaton and abstraction automata 3520 3521Thu Feb 12 17:50:45 1998 Steven Eker <eker@lilac.csl.sri.com> 3522 3523 * ACU_NGA_LhsAutomaton.cc (~ACU_NGA_LhsAutomaton): added 3524 3525 * ACU_NGA_LhsAutomaton.hh (class ACU_NGA_LhsAutomaton): added decl 3526 for ~ACU_NGA_LhsAutomaton() 3527 3528 * ACU_AlienAlienLhsAutomaton.cc (~ACU_AlienAlienLhsAutomaton): add 3529 3530 * ACU_AlienAlienLhsAutomaton.hh (class 3531 ACU_AlienAlienLhsAutomaton): added decl for 3532 ~ACU_AlienAlienLhsAutomaton() 3533 3534 * ACU_LhsAutomaton.cc (ACU_LhsAutomaton): added 3535 3536 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): added decl for 3537 ~ACU_LhsAutomaton() 3538 3539Wed Feb 11 16:46:29 1998 Steven Eker <eker@lilac.csl.sri.com> 3540 3541 * ACU_VarLhsAutomaton.cc (match): compare() != 0 replaced by 3542 !equal() 3543 3544 * ACU_Term.cc (normalize): compare() == 0 replaced by equal() (2 3545 places) 3546 3547 * ACU_Matcher.cc (eliminateBoundVariables): compare() != 0 3548 replaced by !equal() 3549 3550 * ACU_GndLhsAutomaton.cc (match): compare() != 0 replaced by 3551 !equal() 3552 3553 * ACU_CollapseMatcher.cc (uniqueCollapseMatch): compare() != 0 3554 replaced by !equal() 3555 (multiwayCollapseMatch): compare() != 0 replaced by !equal() 3556 (multiwayCollapseMatch): compare() == 0 replaced by equal() (2 3557 places) 3558 3559 * ACU_NGA_LhsAutomaton.cc (match): use delete rather than 3560 calling deepSelfDestruct() 3561 3562 * ACU_Matcher.cc (buildBipartiteGraph): use delete rather than 3563 calling deepSelfDestruct() 3564 3565 * ACU_GreedyMatcher.cc (greedyMatch): use delete rather than 3566 calling deepSelfDestruct() 3567 3568 * ACU_AlienAlienLhsAutomaton.cc (match): use delete rather than 3569 calling deepSelfDestruct() 3570 3571 * ACU_Subproblem.hh (class ACU_Subproblem): deleted decl for 3572 deepSelfDestruct() 3573 3574 * ACU_Subproblem.cc (deepSelfDestruct): deleted 3575 (~ACU_Subproblem): inserted bulk of code from old 3576 deepSelfDestruct(); use delete rather than calling 3577 deepSelfDestruct() 3578 3579===================================Engine35================================================== 3580 3581Fri Jan 16 18:19:12 1998 Steven Eker <eker@lilac.csl.sri.com> 3582 3583 * ACU_Term.cc (insertAbstractionVariables): changed 3584 AdvisoryCheck() to DebugAdvisoryCheck() 3585 3586Wed Dec 24 15:34:20 1997 Steven Eker <eker@lilac.csl.sri.com> 3587 3588 * ACU_LhsAutomaton.cc (dump): dump uniqueCollapseAutomaton if it exists 3589 3590Tue Dec 23 12:38:55 1997 Steven Eker <eker@lilac.csl.sri.com> 3591 3592 * ACU_LhsAutomaton.cc (dump): don't try to print name of an 3593 abstraction variable 3594 3595 * ACU_LhsCompiler1.cc (compileLhs2): use greedySafe() 3596 3597 * ACU_LhsCompiler0.cc (tryToMakeAlienAlienLhsAutomaton): use greedySafe() 3598 (tryToMakeCollectorLhsAutomaton): use greedySafe() 3599 3600Thu Dec 18 18:01:52 1997 Steven Eker <eker@lilac.csl.sri.com> 3601 3602 * ACU_LhsAutomaton.cc (addTopVariable): use Term::takeIdentity() 3603 3604 * ACU_LhsCompiler0.cc (tryToMakeNonLinearLhsAutomaton): use 3605 Term::takeIdentity() 3606 (tryToMakeCollectorLhsAutomaton): use Term::takeIdentity() 3607 3608Wed Dec 17 12:03:01 1997 Steven Eker <eker@lilac.csl.sri.com> 3609 3610 * ACU_NonLinearLhsAutomaton.cc (match): check to see that we 3611 actually have a match before allocating ACU_DagNode in non ext 3612 case; the space for the ACU_DagNode can be very big and this case 3613 is likely to fail. 3614 3615 * ACU_NonLinearLhsAutomaton.hh (class ACU_NonLinearLhsAutomaton): 3616 made varIndex, multiplicity, varSort, unitSort const 3617 3618Tue Dec 16 11:52:36 1997 Steven Eker <eker@lilac.csl.sri.com> 3619 3620 * ACU_Term.hh (class ACU_Term): added decl for tryToMakeNonLinearLhsAutomaton() 3621 3622 * ACU_LhsCompiler0.cc (compileLhs): major rewrite and simplification 3623 (tryToMakeNonLinearLhsAutomaton): added 3624 3625 * ACU_NonLinearLhsAutomaton.cc (match): handle case where variable 3626 is bound 3627 (dump): call HeuristicLhsAutomaton::dump() 3628 3629 * ACU_NonLinearLhsAutomaton.hh (class ACU_NonLinearLhsAutomaton): 3630 derive from HeuristicLhsAutomaton 3631 3632 * ACU_AlienAlienLhsAutomaton.cc (complete): deleted 3633 (match): use fullMatch() 3634 (dump): call HeuristicLhsAutomaton::dump() 3635 3636 * ACU_AlienAlienLhsAutomaton.hh (class 3637 ACU_AlienAlienLhsAutomaton): derive from HeuristicLhsAutomaton; 3638 deleted decl for complete(); data member fullAutomaton; 3639 3640 * ACU_CollectorLhsAutomaton.cc (dump): call HeuristicLhsAutomaton::dump() 3641 (complete): deleted 3642 3643 * ACU_CollectorLhsAutomaton.hh (class ACU_CollectorLhsAutomaton): 3644 derive from HeuristicLhsAutomaton 3645 (class ACU_CollectorLhsAutomaton): deleted decls for complete() 3646 and fullMatch() 3647 (fullMatch): deleted 3648 (class ACU_CollectorLhsAutomaton): deleted data member fullAutomaton 3649 3650 * ACU_LhsCompiler0.cc (compileLhs): insert index of variable into 3651 boundUniquely when making a ACU_NonLinearLhsAutomaton 3652 3653 * ACU_NonLinearLhsAutomaton.cc (match): fixed bug where we were 3654 forgetting to increment p when building new ACU_DagNode 3655 3656 * ACU_LhsCompiler0.cc (compileLhs): added code to make 3657 ACU_NonLinearLhsAutomaton where appropriate 3658 3659Mon Dec 15 18:54:20 1997 Steven Eker <eker@lilac.csl.sri.com> 3660 3661 * ACU_NonLinearLhsAutomaton.cc: created 3662 3663 * ACU_NonLinearLhsAutomaton.hh (class ACU_NonLinearLhsAutomaton): 3664 created 3665 3666===================================Engine34================================================== 3667 3668Thu Dec 11 18:24:11 1997 Steven Eker <eker@lilac.csl.sri.com> 3669 3670 * ACU_Subproblem.cc (solveVariables): check that we actually have 3671 a sort before calling d->setReduced() since d->checkSort() is not 3672 guarenteed to leave a sort behind (in the presence of sort constraints). 3673 3674Fri Dec 5 11:23:05 1997 Steven Eker <eker@lilac.csl.sri.com> 3675 3676 * ACU_DagOperations.cc (eliminateArgument): code cleaning 3677 3678 * ACU_Symbol.cc (eqRewrite): optimized use of nrArgs 3679 (compileOpDeclarations): only call leftIdentitySortCheck() and 3680 rightIdentitySortCheck() if we actually have an identity 3681 3682 * ACU_Symbol.hh (class ACU_Symbol): deleted utilityBuffer static 3683 class member decl 3684 3685 * ACU_Symbol.cc (finalizeSortInfo): deleted 3686 (compileOpDeclarations): call leftIdentitySortCheck() and 3687 rightIdentitySortCheck() 3688 deleted utilityBuffer static class member 3689 (computeBaseSort): use local static sortIndexBuffer in place of 3690 utilityBuffer 3691 3692 * ACU_Symbol.hh (class ACU_Symbol): deleted finalizeSortInfo() decl 3693 3694Thu Dec 4 12:52:46 1997 Steven Eker <eker@lilac.csl.sri.com> 3695 3696 * ACU_Term.cc (compareArguments): compare multiplicity before 3697 actaul argument (dagNode version) 3698 (compareArguments): compare multiplicity before 3699 actaul argument (term version) 3700 3701 * ACU_DagNode.cc (compareArguments): compare multiplicity before 3702 actaul argument; this may avoid comparison of argument in some cases. 3703 3704 * ACU_Symbol.cc (ACU_Symbol): deleted inert arg 3705 3706 * ACU_Symbol.hh (class ACU_Symbol): deleted inert 3707 arg from ctor decl 3708 3709Tue Dec 2 16:40:08 1997 Steven Eker <eker@lilac.csl.sri.com> 3710 3711 * ACU_Symbol.cc (copyAndReduceSubterms): use DagNode::copyAndReduce() 3712 3713Mon Dec 1 11:33:38 1997 Steven Eker <eker@lilac.csl.sri.com> 3714 3715 * ACU_Symbol.cc (eqRewrite): use getPermuteStrategy() (*3) 3716 3717 * ACU_Term.cc (markEagerArguments): use getPermuteStrategy() 3718 (findEagerVariables): use getPermuteStrategy() 3719 3720 * ACU_Symbol.cc (ACU_Symbol): PermuteSymbol -> AssociativeSymbol 3721 (eqRewrite): PermuteSymbol -> AssociativeSymbol (*3) 3722 3723 * ACU_Term.cc (findEagerVariables): PermuteSymbol -> BinarySymbol (*3) 3724 (markEagerArguments): PermuteSymbol -> BinarySymbol 3725 3726 * ACU_LhsCompiler0.cc (tryToMakeCollectorLhsAutomaton): PermuteSymbol -> 3727 AssociativeSymbol (*2) 3728 3729 * ACU_LhsAutomaton.cc (addAbstractionVariable): PermuteSymbol -> 3730 AssociativeSymbol 3731 3732 * ACU_GreedyMatcher.cc (greedyPureMatch): PermuteSymbol -> 3733 AssociativeSymbol (*4) 3734 3735 * ACU_DagOperations.cc (eliminateArgument): use getPermuteStrategy() 3736 3737 * ACU_DagNode.cc (copyEagerUptoReduced2): use getPermuteStrategy() 3738 3739 * ACU_Symbol.hh (class ACU_Symbol): PermuteSymbol -> 3740 AssociativeSymbol 3741 3742 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): PermuteSymbol -> 3743 AssociativeSymbol 3744 3745Mon Nov 24 11:09:15 1997 Steven Eker <eker@lilac.csl.sri.com> 3746 3747 * ACU_AlienAlienLhsAutomaton.cc (dump): implemented 3748 3749 * ACU_DagNode.hh (class ACU_DagNode): ACU_FastLhsAutomaton no 3750 longer exists and hence is no longer a friend 3751 3752 * ACU_RhsAutomaton.cc (buildAliens): deleted 3753 (dump): implemented 3754 3755 * ACU_RhsAutomaton.hh (class ACU_RhsAutomaton): deleted aliens 3756 data member 3757 (addAlien): deleted 3758 3759 * ACU_Term.hh (class ACU_Term): updated member function declarations 3760 3761 * ACU_LhsCompiler0.cc (compileLhs): rewrutten 3762 (tryToMakeFastAutomation2): renamed to 3763 tryToMakeAlienAlienLhsAutomaton() 3764 (tryToMakeFastAutomaton): renamed to 3765 tryToMakeCollectorLhsAutomaton() 3766 (tryToMakeCollectorLhsAutomaton): rewrittten to use new derived classes 3767 3768 * ACU_GndLhsAutomaton.cc: created 3769 3770 * ACU_GndLhsAutomaton.hh (class ACU_GndLhsAutomaton): created 3771 3772 * ACU_DagNode.hh (class ACU_DagNode): ACU_VarLhsAutomaton becomes 3773 a friend 3774 (class ACU_DagNode): ACU_GndLhsAutomaton becomes a friend 3775 3776 * ACU_VarLhsAutomaton.hh (class ACU_VarLhsAutomaton): created 3777 3778 * ACU_VarLhsAutomaton.cc: created 3779 3780 * ACU_DagNode.hh (class ACU_DagNode): ACU_NGA_LhsAutomaton becomes 3781 a friend 3782 3783 * ACU_CollectorLhsAutomaton.cc (complete): added 3784 (dump): now dump fullAutomaton 3785 3786 * ACU_CollectorLhsAutomaton.hh (fullMatch): added 3787 3788 * ACU_NGA_LhsAutomaton.hh (class ACU_NGA_LhsAutomaton): created 3789 3790 * ACU_NGA_LhsAutomaton.cc: created 3791 3792Sun Nov 23 17:27:37 1997 Steven Eker <eker@lilac.csl.sri.com> 3793 3794 * ACU_DagNode.hh (class ACU_DagNode): ACU_CollectorLhsAutomaton 3795 becomes a friend 3796 3797 * ACU_FastLhsAutomaton.cc (dump): rewritten as a temporary hack 3798 9this class will soon be split 3 ways) 3799 3800 * ACU_FastLhsAutomaton.hh (class ACU_FastLhsAutomaton): updated 3801 dump() decl 3802 3803 * ACU_AlienAlienLhsAutomaton.hh (class 3804 ACU_AlienAlienLhsAutomaton): updated dump() decl 3805 3806 * ACU_LhsAutomaton.cc (dump): rewritten 3807 3808 * ACU_RhsAutomaton.hh (class ACU_RhsAutomaton): updated dump() decl 3809 3810 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): updated dump() decl 3811 3812 * ACU_CollectorLhsAutomaton.cc: created from ACU_FastLhsAutomaton.cc 3813 3814 * ACU_CollectorLhsAutomaton.hh: created from 3815 ACU_FastLhsAutomaton.hh 3816 3817===================================Engine33================================================== 3818 3819Fri Nov 21 14:28:50 1997 Steven Eker <eker@lilac.csl.sri.com> 3820 3821 * ACU_DagNormalization.cc (extensionNormalizeAtTop): added 3822 3823 * ACU_Symbol.cc (eqRewrite): have special handling for case when 3824 normalizationStatus == ACU_DagNode::EXTENSION 3825 3826 * ACU_DagNode.cc (partialReplace): use setNormalizationStatus() 3827 3828 * ACU_Subproblem.cc (solveVariables): use setNormalizationStatus() 3829 3830 * ACU_GreedyMatcher.cc (greedyPureMatch): use setNormalizationStatus() 3831 3832 * ACU_Matcher.cc (forcedLoneVariableCase): use setNormalizationStatus() 3833 3834 * ACU_FastLhsAutomaton.cc (collect): use setNormalizationStatus() 3835 3836 * ACU_DagNode.hh (ACU_DagNode): set theory byte to 0 3837 3838 * ACU_Symbol.cc (computeBaseSort): use getNormalizationStatus() 3839 (eqRewrite): use getNormalizationStatus() (3 times) 3840 3841 * ACU_DagNode.hh (clearShortCircuit): deleted 3842 (setShortCircuit): deleted 3843 (getShortCircuit): deleted 3844 (getNormalizationStatus): added 3845 (setNormalizationStatus): added 3846 3847 * ACU_DagNode.cc (partialReplace): made and unmade change to 3848 remove implicit flattening. The advantage of not implicitly 3849 flattening is that we don't mix sorted reduced stuff with unsorted 3850 undeduced stuff and thereby defeat are fast normalization. The 3851 problem is that we need an extra dag node, more match attempts and 3852 the new "not in error sort" semantics of the shortCircuit flag in 3853 unsafe here since the extension part could be in the error sort. 3854 3855Thu Nov 20 11:58:34 1997 Steven Eker <eker@lilac.csl.sri.com> 3856 3857 * ACU_ExtensionInfo.hh (reset): added; allows extensionInfo to be 3858 prepared for use without wasting time clearing it. 3859 3860 * ACU_AlienAlienLhsAutomaton.cc (match): put automata pointers into 3861 local variable to avoid gcc generating register reloads after 3862 function calls. Use ACU_ExtensionInfo::reset(). 3863 3864 * ACU_LhsCompiler0.cc (tryToMakeFastAutomation2): fixed bug where 3865 we were compile same t1 twice and t2 not at all 3866 3867 * ACU_AlienAlienLhsAutomaton.cc (match): handle cases where 3868 first/second symbol does not occcur in subject 3869 (match): fixed bug where we using wrong local substitution in 2nd match 3870 3871 * ACU_LhsCompiler0.cc (tryToMakeFastAutomation2): added missing 3872 return for AlienAlien case 3873 3874 * ACU_DagNode.hh (class ACU_DagNode): class 3875 ACU_AlienAlienLhsAutomaton becomes a friend 3876 3877 * ACU_AlienAlienLhsAutomaton.hh (class ACU_AlienAlienLhsAutomaton): created 3878 3879 * ACU_AlienAlienLhsAutomaton.cc (ACU_AlienAlienLhsAutomaton): created 3880 3881Tue Nov 18 18:25:08 1997 Steven Eker <eker@lilac.csl.sri.com> 3882 3883 * ACU_Term.cc (dump): added 3884 (dumpArguments): deleted 3885 3886 * ACU_Term.hh (class ACU_Term): dumpArguments() decl becomes dump() 3887 3888 * ACU_Term.cc (dumpArguments): removed const; pass variableInfo by 3889 ref; switch varableInfo, indentLevel args 3890 3891 * ACU_Term.hh (class ACU_Term): dumpArguments() decl now passes 3892 variableInfo by ref; removed const; switch varableInfo, 3893 indentLevel args 3894 3895Mon Nov 17 11:07:23 1997 Steven Eker <eker@lilac.csl.sri.com> 3896 3897 * ACU_Subproblem.cc (computeAssignment): don't pass shortCircuit 3898 argument to ACU_DagNode() 3899 (solveVariables): setShortCircuit() 3900 3901 * ACU_Matcher.cc (forcedLoneVariableCase): call setShortCircuit() 3902 3903 * ACU_GreedyMatcher.cc (greedyPureMatch): call setShortCircuit() 3904 3905 * ACU_FastLhsAutomaton.cc (collect): call setShortCircuit() 3906 3907 * ACU_Symbol.cc (eqRewrite): use getShortCircuit() (three places) 3908 3909 * ACU_DagNode.cc (partialReplace): call clearShortCircuit() 3910 3911 * ACU_DagNode.hh (class ACU_DagNode): removed shortCircuit arg from 3912 ctor 3913 (class ACU_DagNode): added decls for getShortCircuit() and 3914 setShortCircuit() and clearShortCircuit() 3915 (class ACU_DagNode): deleted shortCircuit data member 3916 (ACU_DagNode): non longer intialize shortCircuit 3917 (setShortCircuit): added 3918 (getShortCircuit): added 3919 (clearShortCircuit): added 3920 3921Fri Nov 14 10:20:07 1997 Steven Eker <eker@lilac.csl.sri.com> 3922 3923 * ACU_LhsAutomaton.cc (dump): dump collapsePossible 3924 3925 * ACU_FastLhsAutomaton.cc (collect): added speed hack 3926 (dump): implemented 3927 3928 * ACU_LhsCompiler0.cc: don't use fast automaton if we're in error 3929 sort and we have extension 3930 3931 * ACU_FastLhsAutomaton.cc (collect): hand optimized 3932 3933 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): all todays changes 3934 unmade as they made things slower 3935 3936 * ACU_Matcher.cc: all todays changes unmade as they made things slower 3937 3938 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): data memeber 3939 totalMultiplicity deleted 3940 (class ACU_LhsAutomaton): updated multiplicityChecks() decl 3941 3942 * ACU_Matcher.cc (multiplicityChecks): rewritten; first case now 3943 just does copying without multiplicity checks in the case where 3944 they will all trvially succeed. Second case now has early failure 3945 when totalSubjectMultiplicity > totalUpperBound 3946 (multiplicityChecks): rewritten; now sets extensionInfo upperBound 3947 (match): pass extensionInfo to multiplicityChecks(); don't set 3948 extensionInfo upperBound 3949 3950 * ACU_FastLhsAutomaton.cc (ACU_FastLhsAutomaton): changed 3951 stripperTopSymbol to stripperSymbol to avoid confusion with data member 3952 (match): make sure we actually bind stripper variable 3953 (match): bind collector variable in local rather than solution so 3954 it does not get overwritten when we copy local into solution 3955 3956 * ACU_LhsCompiler0.cc (tryToMakeFastAutomation): pass 3957 !(collapseSymbols().empty()) for collapsePossible (2 places) 3958 3959Thu Nov 13 16:11:00 1997 Steven Eker <eker@lilac.csl.sri.com> 3960 3961 * ACU_LhsCompiler0.cc: created 3962 3963 * ACU_Term.hh (class ACU_Term): added decl for compileLhs2() 3964 3965 * ACU_LhsCompiler1.cc (compileLhs2): created from old 3966 compileLhs(); now returns ACU_LhsAutomaton* 3967 3968 * ACU_DagNode.hh (class ACU_DagNode): ACU_FastLhsAutomaton becomes 3969 a friend 3970 3971 * ACU_FastLhsAutomaton.hh (class ACU_FastLhsAutomaton): created 3972 3973 * ACU_FastLhsAutomaton.cc: created 3974 3975===================================Engine32================================================== 3976 3977Fri Oct 31 16:56:23 1997 Steven Eker <eker@lilac.csl.sri.com> 3978 3979 * ACU_CollapseMatcher.cc (multiwayCollapseMatch): removed buggy 3980 optimization where we were binding variables to identity in 3981 solution after they had been considered for match against whole 3982 subject; the problem is that solution gets returned to caller with 3983 these not always correct bindings 3984 (multiwayCollapseMatch): make use of the faxt that all variables 3985 with multiplicity > 1 will be bound to dentity once we reach the 3986 disjuction loop; use DisjunctiveSubproblemAccumulator to simplify code. 3987 (multiwayCollapseMatch): eliminated first flag by using empty() 3988 3989Wed Oct 29 10:30:51 1997 Steven Eker <eker@lilac.csl.sri.com> 3990 3991 * ACU_DagNode.cc (matchVariableWithExtension): call 3992 extensionInfo->setValidAfterMatch(false) 3993 3994 * ACU_CollapseMatcher.cc (multiwayCollapseMatch): don't call 3995 extensionInfo->clear() 3996 (multiwayCollapseMatch): use extensionInfo->validAfterMatch() 3997 (multiwayCollapseMatch): use 3998 extensionInfo->setValidAfterMatch(false) in place of extensionInfo->clear() 3999 (multiwayCollapseMatch): in the case where the subject is our 4000 identity we fix a bug by checking for extension info and calling 4001 extensionInfo->setValidAfterMatch(true) and 4002 extensionInfo->setMatchedWhole(true) if so. Previously we didn't 4003 worry about extension with the result that it was never set, 4004 allowing an uninitialized data read in partialConstruct() for example. 4005 (multiwayCollapseMatch): non viable variable that are unbound are 4006 bound to identity at the outset (that is unbound variables that 4007 have multiplicity > 1). The case where nrViableVariables == 0 4008 contained a bug since we could still get a match if extension was 4009 present. The case where nrViableVariables == 1 clean up now we 4010 know that all other variables are bound to identity. 4011 4012 * ACU_Subproblem.cc (fillOutExtensionInfo): use setMatchedWhole() 4013 in place of setWholeFlag() (2 places) 4014 (solveVariables): use setMatchedWhole() in place of setWholeFlag() 4015 4016 * ACU_GreedyMatcher.cc (greedyPureMatch): call 4017 setValidAfterMatch(true) if we fill out the extension info 4018 4019 * ACU_Matcher.cc (fullMatch): call setValidAfterMatch(false) since 4020 extension info will not be valid until solve phase 4021 4022 * ACU_ExtensionInfo.cc (makeClone): use setValidAfterMatch(), 4023 validAfterMatch() and setMatchedWhole() 4024 (copy): use setValidAfterMatch(), 4025 validAfterMatch() and setMatchedWhole() 4026 4027Tue Oct 28 10:19:21 1997 Steven Eker <eker@lilac.csl.sri.com> 4028 4029 * ACU_CollapseMatcher.cc (multiwayCollapseMatch): clear extension 4030 information if it exists before each call to matchVariable; only 4031 save extensionInfo in SubproblemDisjunction in the case where it 4032 is valid (regardless of whether subproblem == 0 because we can 4033 have the case where extensionInfo is valid but subproblem != 0); 4034 Before exiting with true we clear any old extension info that 4035 might exist be cause it will now be invalid (having been saved on 4036 one of the disjuction paths it cannot be globally valid). 4037 4038Mon Oct 27 11:43:56 1997 Steven Eker <eker@lilac.csl.sri.com> 4039 4040 * ACU_CollapseMatcher.cc (multiwayCollapseMatch): save 4041 extensionInfo in SubproblemDisjunction in the case where subproblem == 0 4042 4043 * ACU_ExtensionInfo.hh (class ACU_ExtensionInfo): subject made non 4044 const in order to do copy() 4045 4046 * ACU_ExtensionInfo.cc (makeClone): added 4047 (copy): added 4048 4049 * ACU_ExtensionInfo.hh (class ACU_ExtensionInfo): added decls for 4050 makeClone() and copy() 4051 4052Fri Oct 24 13:07:30 1997 Steven Eker <eker@lilac.csl.sri.com> 4053 4054 * ACU_Subproblem.cc (solveVariables): use 4055 ExtensionInfo::buildMatchedPortion() and DagNode::inErrorSort() 4056 instead of matchedPortionOK(); call fillOutExtensionInfo() first 4057 (matchedPortionOK): deleted 4058 4059 * ACU_Subproblem.hh (class ACU_Subproblem): deleted decl for 4060 matchedPortionOK(); 4061 4062 * ACU_CollapseMatcher.cc (multiwayCollapseMatch): use 4063 EqualitySubproblem instead of ExclusionSubproblem 4064 4065 * ACU_DagNode.hh (class ACU_DagNode): class ACU_ExtensionInfo is 4066 now a friend 4067 4068 * ACU_Symbol.cc (ruleRewrite): switched to new ACU_ExtensionInfo convention 4069 (eqRewrite): switched to new ACU_ExtensionInfo convention (3 places) 4070 4071 * ACU_DagNode.cc (makeExtensionInfo): switched to new 4072 ACU_ExtensionInfo convention 4073 4074 * ACU_Theory.cc: deleted 4075 4076 * ACU_ExtensionInfo.cc: created 4077 4078 * ACU_ExtensionInfo.hh (ACU_ExtensionInfo): ctor now takes subject 4079 rather than nrArgs; added decl for buildMatchedPortion() 4080 (clear): use subject data member 4081 (ACU_ExtensionInfo): store subject arg in data member 4082 4083Tue Oct 21 12:23:04 1997 Steven Eker <eker@lilac.csl.sri.com> 4084 4085 * ACU_CollapseMatcher.cc (multiwayCollapseMatch): add exclusion 4086 subproblems to eliminate duplicate solutions in the case that the 4087 subject matches out identity with extension. 4088 4089 * ACU_Term.cc (dagify2): switched to new convention 4090 4091 * ACU_Term.hh (class ACU_Term): switched dagify2() decl to new convention 4092 4093Wed Oct 15 17:17:16 1997 Steven Eker <eker@lilac.csl.sri.com> 4094 4095 * ACU_Subproblem.cc (solveVariables): use BinarySymbol::getIdentityDag() 4096 (2 places) 4097 (solveVariables): delete identityDag local variable 4098 4099 * ACU_GreedyMatcher.cc (greedyPureMatch): use BinarySymbol::getIdentityDag() 4100 (greedyPureMatch): delete identityDag local variable 4101 4102 * ACU_Matcher.cc (match): use BinarySymbol::getIdentityDag() 4103 4104 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): delete identityDag 4105 arg from bindUnboundVariablesToIdentity() 4106 4107 * ACU_CollapseMatcher.cc (uniqueCollapseMatch): use BinarySymbol::getIdentityDag() 4108 (bindUnboundVariablesToIdentity): use 4109 BinarySymbol::getIdentityDag(); remove identityDag arg 4110 (multiwayCollapseMatch): use BinarySymbol::getIdentityDag() 4111 4112 * ACU_LhsCompiler1.cc (analyseConstraintPropagation): use VariableTerm::dynamicCast() 4113 (compileLhs): use VariableTerm::dynamicCast() 4114 4115 * ACU_Term.cc (mightCollapseToOurSymbol): deleted 4116 (mightMatchOurIdentity): deleted 4117 (analyseCollapses): use BinarySymbol::mightMatchOurIdentity() 4118 (insertAbstractionVariables): use BinarySymbol::mightMatchOurIdentity() 4119 (insertAbstractionVariables): use PermuteSymbol::mightCollapseToOurSymbol() 4120 (compileRhs): use VariableTerm::dynamicCast() 4121 (insertAbstractionVariables): use VariableTerm::dynamicCast() 4122 4123 * ACU_Term.hh (class ACU_Term): deleted decls for 4124 mightCollapseToOurSymbol() and mightMatchOurIdentity() 4125 4126 * ACU_Symbol.cc (~ACU_Symbol): deleted 4127 (compileOpDeclarations): use BinarySymbol::processIdentity() 4128 (eqRewrite): use getIdentity() (2 places) 4129 (computeTrueSort): use getIdentity() 4130 4131 * ACU_Symbol.hh (class ACU_Symbol): delete dtor decl 4132 4133 * ACU_Symbol.cc (ACU_Symbol): rewritten to use new PermuteSymbol conventions 4134 4135 * ACU_Symbol.hh (class ACU_Symbol): removed constructor arg from 4136 ctor; deleted decls for getIdentity() and makeIdentityDag(); 4137 (class ACU_Symbol): deleted identity, identityAutomaton and 4138 identitySubstitution data members 4139 (getIdentity): deleted 4140 (makeIdentityDag): deleted 4141 4142Mon Oct 13 10:36:57 1997 Steven Eker <eker@lilac.csl.sri.com> 4143 4144 * ACU_Term.cc (mightCollapseToOurSymbol): added 4145 (mightMatchOurIdentity): added 4146 (analyseCollapses): added 4147 (insertAbstractionVariables): added 4148 (determineCollapseSymbols): deleted 4149 4150 * ACU_Term.hh (class ACU_Term): added decls for analyseCollapses() 4151 and insertAbstractionVariables(); delete decl for determineCollapseSymbols() 4152 4153 * ACU_LhsAutomaton.cc (dump): index2Symbol() -> index2Variable() 4154 4155 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): VariableIndex -> VariableInfo 4156 4157 * ACU_LhsAutomaton.cc (dump): VariableIndex -> VariableInfo 4158 4159 * ACU_Term.cc (dumpArguments): VariableIndex -> VariableInfo 4160 (determineCollapseSymbols): VariableIndex -> VariableInfo 4161 (dumpArguments): VariableIndex -> VariableInfo 4162 4163 * ACU_Term.hh (class ACU_Term): VariableIndex -> VariableInfo 4164 4165 * ACU_Symbol.cc (compileOpDeclarations): VariableIndex -> 4166 VariableInfo 4167 4168===================================Engine30================================================== 4169 4170Tue Oct 7 15:32:51 1997 Steven Eker <eker@lilac.csl.sri.com> 4171 4172 * ACU_Symbol.hh (class ACU_Symbol): added decl for makeDagNode() 4173 4174 * ACU_Symbol.cc (makeDagNode): added 4175 4176Fri Oct 3 19:26:11 1997 Steven Eker <eker@lilac.csl.sri.com> 4177 4178 * ACU_Symbol.cc (compileOpDeclarations): DataSet -> TermSet 4179 4180 * ACU_Term.cc (compileRhs): DataSet -> TermSet 4181 (dagify2): DataSet -> TermSet 4182 4183 * ACU_Term.hh (class ACU_Term): DataSet -> TermSet 4184 4185===================================Engine29================================================== 4186 4187Thu Oct 2 17:43:48 1997 Steven Eker <eker@lilac.csl.sri.com> 4188 4189 * ACU_Symbol.cc (compileOpDeclarations): pass DataSet to compileRhs() 4190 4191 * ACU_Term.hh (class ACU_Term): updated compileRhs() decl 4192 4193 * ACU_Term.cc (compileRhs): adapted to use DataSet& compiled 4194 4195Tue Sep 30 12:18:57 1997 Steven Eker <eker@lilac.csl.sri.com> 4196 4197 * ACU_Term.hh (class ACU_Term): dagify() decl changed to dagify2() 4198 4199 * ACU_Term.cc (normalize): now compute hash values 4200 (dagify2): adapted from dagify() 4201 4202Thu Sep 25 16:38:20 1997 Steven Eker <eker@lilac.csl.sri.com> 4203 4204 * ACU_Term.cc (determineCollapseSymbols): use getOpDeclarations() 4205 4206 * ACU_Symbol.cc (specificRewrite): deleted 4207 4208 * ACU_Symbol.hh (class ACU_Symbol): deleted decl for 4209 specificRewrite() 4210 4211===================================Engine28================================================== 4212 4213Mon Aug 25 12:11:34 1997 Steven Eker <eker@lilac.csl.sri.com> 4214 4215 * ACU_Symbol.cc (eqRewrite): fixed a bug where we could collapse 4216 to an unreduced subterm and stop rewriting at this node. We now 4217 return true in this case to force rewriting to continue. 4218 4219Tue Aug 19 15:27:21 1997 Steven Eker <eker@lilac.csl.sri.com> 4220 4221 * ACU_DagNode.hh (nrArgs): added 4222 (getArgument): added 4223 (getMultiplicity): added 4224 (class ACU_DagNode): added decl for nrArgs(), getArgument(int i), 4225 getMultiplicity(int i). This provide a fast interface to the 4226 argument list for non ACU_Theory code that is ACU_Theory aware 4227 (maybe classes derived from ACU_Symbol). 4228 4229Fri Jul 25 18:04:23 1997 Steven Eker <eker@lilac.csl.sri.com> 4230 4231 * ACU_DagNode.cc (partialReplace): removed Assert(getSortIndex() == 4232 Sort::SORT_UNKNOWN, cerr << "shouldn't have valid sort"); since if 4233 node was original created by matcher it may well have valid sort 4234 4235Thu Jul 24 11:20:50 1997 Steven Eker <eker@lilac.csl.sri.com> 4236 4237 * ACU_GreedyMatcher.cc (greedyPureMatch): optimized vector 4238 accesses for assignment building 4239 (greedyPureMatch): optimized inner loop for assigning unassigned subjects 4240 4241 * ACU_Subproblem.cc (computeAssignment): pass shortCircuit = 4242 true to ACU_DagNode() 4243 4244 * ACU_GreedyMatcher.cc (greedyPureMatch): pass shortCircuit = 4245 true to ACU_DagNode() 4246 4247 * ACU_Matcher.cc (forcedLoneVariableCase): pass shortCircuit = 4248 true to ACU_DagNode() 4249 4250 * ACU_Symbol.cc (eqRewrite): added s->eliminateArgument(identity) 4251 calls after new normalizeAtTop() calls 4252 (eqRewrite): rewritten from scatch to make use of short circuit 4253 4254 * ACU_DagNode.cc (partialReplace): clear shortCircuit flag 4255 4256 * ACU_DagNode.hh (ACU_DagNode): set shortCircuit flag 4257 4258 * ACU_Symbol.cc (eqRewrite): added normalizeAtTop() calls after 4259 sort computation for LAZY and SEMI_EAGER cases; this fixes a bug 4260 introduced by just-in-time normalization 4261 4262 * ACU_DagNode.hh (class ACU_DagNode): added shortCircuit data 4263 member; the idea is to set this when an ACU_DagNode is created in 4264 the matcher cut down need for normalization checking 4265 4266Wed Jul 23 11:50:27 1997 Steven Eker <eker@lilac.csl.sri.com> 4267 4268 * ACU_DagNode.cc (partialReplace): added call to repudiateSortInfo() 4269 4270 * ACU_Term.cc (normalize): added full flag 4271 (normalize): don't call normalizeAliensAndFlatten() if full = false 4272 (normalizeAliensAndFlatten): pass full = true to normalize() 4273 4274 * ACU_Term.hh (class ACU_Term): added full flag to normalize 4275 4276 * ACU_Symbol.cc (ACU_Symbol): pass full = true to normalize() 4277 (compileOpDeclarations): deleted superfluous normalization call 4278 4279Mon Jul 21 10:24:23 1997 Steven Eker <eker@lilac.csl.sri.com> 4280 4281 * ACU_RhsAutomaton.hh (class ACU_RhsAutomaton): updated 4282 buildArguments() decl 4283 4284 * ACU_RhsAutomaton.cc (buildArguments): take argArray rather than node 4285 4286 * ACU_Symbol.cc (computeTrueSort): now do normalization 4287 4288 * ACU_DagNode.hh (class ACU_DagNode): deleted 4289 normalizeEagerUptoReduced2() and nonEagerInsert() decls 4290 4291 * ACU_DagNode.cc (normalizeEagerUptoReduced2): deleted 4292 (partialReplace): no longer attempt to normalize node 4293 (partialConstruct): no longer attempt to normalize node 4294 (copyWithReplacement): no longer attempt to normalize node 4295 (nonEagerInsert): deleted 4296 4297 * ACU_Term.cc (compileRhs): no longer pass normalize flag to ACU_RhsAutomaton 4298 (compileRhs): no longer pass term to addArgument() 4299 4300 * ACU_RhsAutomaton.cc (ACU_RhsAutomaton): no longer initialize simpleCtor 4301 (buildArguments): no longer check for reduced args or return bool 4302 (construct): greatly simplified; no longer attempt normalization 4303 under any circumstance 4304 (replace): greatly simplified; no longer attempt normalization 4305 under any circumstance 4306 4307 * ACU_RhsAutomaton.hh (class ACU_RhsAutomaton): removed simpleCtor 4308 member 4309 (class ACU_RhsAutomaton): changed buildArguments() decl 4310 4311===================================Engine26b================================================== 4312 4313Fri Jul 18 16:11:45 1997 Steven Eker <eker@lilac.csl.sri.com> 4314 4315 * ACU_RhsAutomaton.hh (class ACU_RhsAutomaton): (26) updated to 4316 agree with all the changes below 4317 4318 * ACU_RhsAutomaton.cc (ACU_RhsAutomaton): (26b) stripped stable stuff; 4319 deleted normalize arg 4320 (addArgument): (26b) all stable stuff removed; term arg removed 4321 (close): (26b) all stable stuff removed 4322 (calculateFlattening): (26b) all stable stuff removed 4323 (normalizeBuildArguments): (26b) deleted 4324 (buildArguments): (26b) created from old fastBuildArguments) 4325 (calculateFlattening): (26b) deleted 4326 (buildArguments): (26b) now return allReducedFlag 4327 (tryToSetReducedFlag): (26b) deleted 4328 (allArgumentsReduced): (26b) deleted 4329 (replace): (26b) rewritten 4330 (construct): (26b) rewritten 4331 4332 * ACU_RhsAutomaton.hh (class ACU_RhsAutomaton): (26b) stripped 4333 stable stuff 4334 (class ACU_RhsAutomaton): (26b) stripped normalize flag 4335 (class ACU_RhsAutomaton): (26b) removed normalize arg from ctor 4336 4337 * ACU_DagNode.cc (normalizeEagerUpToReduced2): added 4338 (nonEagerInsert): use normalizeEagerUpToReduced() 4339 4340 * ACU_DagNode.hh (class ACU_DagNode): added decl for 4341 normalizeEagerUpToReduced2() 4342 4343Thu Jul 17 10:38:22 1997 Steven Eker <eker@lilac.csl.sri.com> 4344 4345 * ACU_DagNode.hh (class ACU_DagNode): added decl for nonEagerInsert() 4346 4347 * ACU_DagNode.cc (nonEagerInsert): added 4348 (partialReplace): rewritten using nonEagerInsert() 4349 (partialConstruct): rewritten using nonEagerInsert() 4350 (copyWithReplacement): rewritten using nonEagerInsert() 4351 4352 * ACU_RhsAutomaton.cc (addArgument): changed criteria for stable 4353 arg; must 4354 (1) be stable term; 4355 (2) not have our top symbol on top (+NEW*) 4356 (3) not have our identity's top symbol on top (*NEW*) 4357 (4) have a top symbol greater than that of last stable arg 4358 Condition (2) is necessary since we will no longer flatten rhs in 4359 eager context. Condition (3) allows us to restrict search for 4360 identity to case where we have unstable args. 4361 (normalizeBuildArguments): code for removing identity elements 4362 pushed into unstable case 4363 4364 * ACU_Term.cc (compileRhs): calculate and pass normalize flag to 4365 ACU_RhsAutomaton() 4366 4367 * ACU_RhsAutomaton.hh (class ACU_RhsAutomaton): runs -> runsBuffer 4368 (class ACU_RhsAutomaton): added and changed memebr function decls 4369 to agree with all the recent changes in ACU_RhsAutomaton.cc 4370 4371 * ACU_RhsAutomaton.cc (normalizeBuildArguments): created from old 4372 buildArguments(); now do identity elimination 4373 (close): runs renamed to runsBuffer 4374 (replace): rewritten from scratch to be like new construct() 4375 (ACU_RhsAutomaton): initialize normalize flag 4376 4377Wed Jul 16 11:41:48 1997 Steven Eker <eker@lilac.csl.sri.com> 4378 4379 * ACU_RhsAutomaton.cc (construct): fixed bug where we were 4380 applying tryToSetReducedFlag() to a non ACU dagnode produced by 4381 eliminateArgument(identity) 4382 (replace): fix bug similar to above 4383 (construct): rewritten from scratch to handle building dagNode in 4384 normalized or denormalized form depending on the circumstances 4385 (buildAliens): now much simpler; return void 4386 (allArgumentsReduced): added 4387 (calculateFlattening): added 4388 (fastBuildArguments): added 4389 (tryToSetReducedFlag): simplified 4390 4391Tue Jul 15 15:33:28 1997 Steven Eker <eker@lilac.csl.sri.com> 4392 4393 * ACU_RhsAutomaton.cc (ACU_RhsAutomaton): simpleCtor 4394 initialization simplified 4395 4396 * ACU_Symbol.cc (ACU_Symbol): added inert arg 4397 (eqRewrite): inert() call replaced by equationFree() call 4398 4399 * ACU_Symbol.hh (class ACU_Symbol): added inert arg to ctor 4400 4401=====================================Engine26================================================= 4402 4403Mon Jul 14 10:48:39 1997 Steven Eker <eker@lilac.csl.sri.com> 4404 4405 * ACU_DagNode.hh (class ACU_DagNode): changed decl for 4406 sortAndUniquize(); tidied private function decls 4407 4408 * ACU_DagNormalization.cc (sortAndUniquize): code cleaned; make 4409 non-static; arg deleted; made local_inline 4410 (flattenSortAndUniquize): made local_inline 4411 (normalizeAtTop): deleted arg from sortAndUniquize() call 4412 4413Fri Jul 11 12:01:09 1997 Steven Eker <eker@lilac.csl.sri.com> 4414 4415 * ACU_DagNode.hh (class ACU_DagNode): added decl for flattenSortAndUniquize() 4416 4417 * ACU_DagNormalization.cc: created 4418 (normalizeAtTop): optimized; now use flattenSortAndUniquize() 4419 (flattenSortAndUniquize): added 4420 4421 * ACU_DagOperations.cc: created 4422 4423 * ACU_DagNode.cc: ACU specific functions split off into 4424 ACU_DagNormalization.cc and ACU_DagOperations.cc 4425 4426Wed Jul 9 10:53:22 1997 Steven Eker <eker@lilac.csl.sri.com> 4427 4428 * ACU_RhsAutomaton.hh (class ACU_RhsAutomaton): added decl for 4429 tryToSetReducedFlag() 4430 4431 * ACU_RhsAutomaton.cc (topSymbol): initialize simpleCtor 4432 (tryToSetReducedFlag): added 4433 4434 * ACU_RhsAutomaton.hh (class ACU_RhsAutomaton): simpleStor flag added 4435 4436 * ACU_Subproblem.cc (computeAssignment): added comment to note the 4437 fact that assigments are built in normal form 4438 (solveVariables): added topSymbol and buildReducedNodes local 4439 variables; now set reduced flags on nodes with our top symbol if 4440 the subject is reduced. 4441 4442 * ACU_Matcher.cc (forcedLoneVariableCase): set reduced flag on 4443 created ACU dag node if subject is reduced and new dag node has 4444 its true sort after sort checkSort() 4445 4446 * ACU_GreedyMatcher.cc (greedyPureMatch): if the subject is 4447 reduced and the top symbol is sort constraint free when we build 4448 assignments using the top symbols we compute their true sort 4449 (which is equal to their base sort) and set the reduced flag. This 4450 avoid unnecessary future normalization and matching attempts at 4451 the cost of a small matching overhead and having the matcher no 4452 longer oblivious to reduced flags and sort constraints. Ideally 4453 this optimization should only be done for assignments to variables 4454 that are "useful"; i.e. that appear in the rhs or condition. At 4455 some point we should add a "useful" flag to TopVariable or maybe a 4456 more sophisticated mechanism that would allow optimization of solutions. 4457 4458Tue Jul 1 10:19:58 1997 Steven Eker <eker@lilac.csl.sri.com> 4459 4460 * ACU_DagNode.cc (compareArguments): use modified multiset ordering 4461 4462 * ACU_Term.cc (compareArguments): use modified multiset ordering 4463 (compareArguments): use modified multiset ordering 4464 4465 * ACU_DagNode.cc (sortAndUniquize): switched two tests on "r" 4466 because we now sort in ascending order 4467 (mergeSortAndUniquize): switched two tests on "r" 4468 because we now sort in ascending order 4469 (findFirstOccurrence): switched test on "r" because we now 4470 sort in ascending order 4471 (binarySearch): switched test on "r" because we now 4472 sort in ascending order (DagNode* version) 4473 (binarySearch): switched test on "r" because we now 4474 sort in ascending order (Term* version) 4475 4476Mon Jun 30 16:28:11 1997 Steven Eker <eker@lilac.csl.sri.com> 4477 4478 * ACU_DagNode.cc (compareArguments): rewritten to do multiset ordering under the 4479 assumption that args are sorted in ascending order 4480 4481 * ACU_RhsAutomaton.cc (buildArguments): changed comparison to r > 4482 0 now that we want to swap args into ascending order 4483 (addArgument): changed test for adding new stable arg to < 0 since 4484 stable args will now be in ascending order of symbols 4485 4486 * ACU_Term.cc (pairCompare): use ascending rather than descending 4487 order to sort ACU arg list 4488 (compareArguments): rewritten to do multiset ordering under the 4489 assumption that args are sorted in ascending order (Term* version) 4490 (compareArguments): rewritten to do multiset ordering under the 4491 assumption that args are sorted in ascending order (DagNode* version) 4492 4493Fri Jun 27 15:50:27 1997 Steven Eker <eker@lilac.csl.sri.com> 4494 4495 * ACU_DagNode.hh (class ACU_DagNode): copyEagerUptoReduced2() and 4496 clearCopyPointers2() made private 4497 4498 * ACU_DagNode.cc (eliminateArgument): use copyReducible() 4499 rather than copyUptoEager(); we weren't calling 4500 clearCopyPointers() which was a serious but subtle bug. 4501 (copyWithReplacement): use copyReducible() 4502 rather than copyUptoEager(); we weren't calling 4503 clearCopyPointers() 4504 (partialReplace): use copyReducible() 4505 rather than copyUptoEager(); we weren't calling 4506 clearCopyPointers() 4507 (partialConstruct): use copyReducible() 4508 rather than copyUptoEager(); we weren't calling 4509 clearCopyPointers() 4510 4511 * ACU_Symbol.cc (copyAndReduceSubterms): use copyReducible() 4512 rather than copyUptoEager() and clearCopyPointers(); 4513 4514Wed Jun 25 15:15:12 1997 Steven Eker <eker@lilac.csl.sri.com> 4515 4516 * ACU_Symbol.cc: added #include "variable.hh" 4517 4518Tue Jun 24 15:53:31 1997 Steven Eker <eker@lilac.csl.sri.com> 4519 4520 * ACU_LhsAutomaton.cc (addTopVariable): changed Variable* 4521 to VariableTerm* 4522 4523 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): changed Variable* 4524 to VariableTerm* in addTopVariable() decl 4525 4526 * ACU_Term.cc: added #include "variable.hh" 4527 4528 * ACU_LhsCompiler1.cc (analyseConstraintPropagation): use VariableTerm::downCast() 4529 (compileLhs): use VariableTerm::downCast() 4530 4531 * ACU_Term.cc (compileRhs): use VariableTerm::downCast() 4532 4533Thu Jun 19 10:38:03 1997 Steven Eker <eker@lilac.csl.sri.com> 4534 4535 * ACU_Symbol.cc: deleted #include "unionFind.hh" 4536 4537Tue Jun 17 16:40:13 1997 Steven Eker <eker@lilac.csl.sri.com> 4538 4539 * ACU_Symbol.cc (compileOpDeclarations): no longer do the assoc 4540 stuff here 4541 4542 * ACU_Symbol.hh (class ACU_Symbol): deleted compileEquations() decl 4543 4544 * ACU_Symbol.cc (finalizeSortInfo): added 4545 (compileEquations): deleted 4546 4547 * ACU_Symbol.hh (class ACU_Symbol): added decl for finalizeSortInfo() 4548 4549Wed Jun 11 10:35:22 1997 Steven Eker <eker@lilac.csl.sri.com> 4550 4551 * ACU_LhsCompiler1.cc (analyseConstraintPropagation): use 4552 willGroundOutMatch() 4553 (compileLhs): use willGroundOutMatch() 4554 4555 * ACU_LhsCompiler2.cc (findConstraintPropagationSequence): use 4556 willGroundOutMatch() 4557 4558Tue Jun 10 10:24:35 1997 Steven Eker <eker@lilac.csl.sri.com> 4559 4560 * ACU_LhsCompiler2.cc (findConstraintPropagationSequence): don't 4561 add in grounded out aliens unless they also "honor ground out match". 4562 4563Fri Jun 6 18:32:04 1997 Steven Eker <eker@lilac.csl.sri.com> 4564 4565 * ACU_Term.hh (class ACU_Term): deleted addSubsumedAliens() decl 4566 4567 * ACU_LhsCompiler2.cc (compileAliensOnlyCase): removed call to 4568 addSubsumedAliens(); We cannot safely add subsumed aliens for the 4569 following reason: Even though the subsumed alien will not steal 4570 the only match for its subsuming alien (unless there is no overall 4571 match) it could take the wrong match if there is a subproblem; and 4572 we would not discover this until the solve phase when it is too 4573 late. We could make the use of this optimization conditional on 4574 there being no subproblem at match time but this complicates what is 4575 a very minor infrequently usable optimization beyond its utility - 4576 so we ditch it altogether. 4577 (addSubsumedAliens): deleted 4578 4579 * ACU_DagNode.hh (class ACU_DagNode): added 4580 matchVariableWithExtension() decl 4581 4582 * ACU_Symbol.hh (class ACU_Symbol): deleted 4583 matchVariableWithExtension() decl 4584 4585 * ACU_DagNode.cc (matchVariableWithExtension): added 4586 4587 * ACU_Symbol.cc (matchVariableWithExtension): deleted 4588 4589Thu Jun 5 11:48:46 1997 Steven Eker <eker@lilac.csl.sri.com> 4590 4591 * ACU_DagNode.cc (copyEagerUptoReduced2): adapted from old 4592 copyEagerUptoReduced() 4593 (clearCopyPointers2): adapted from old clearCopyPointers() 4594 4595 * ACU_DagNode.hh (class ACU_DagNode): decls for 4596 clearCopyPointers() and copyEagerUptoReduced() changed 4597 4598 * ACU_Subproblem.cc (solveVariables): don't pass context in call 4599 to computeAssignment() 4600 4601 * ACU_Subproblem.hh (class ACU_Subproblem): updated 4602 computeAssignment() decl 4603 4604 * ACU_Subproblem.cc (computeAssignment): no longer compute sort of 4605 returned DagNode 4606 (solveVariables): use inErrorSort() rather than 4607 computeTrueSortWhilePreservingContext() 4608 (solveVariables): use checkSort() now that assignment is no longer 4609 guarenteed to have a sort 4610 (computeAssignment): removed context arg as no longer needed 4611 4612 * ACU_Symbol.cc (ACU_Symbol): don't pass stable arg to Symbol; in 4613 fact we were aleays passing true which was a bug! 4614 4615==============================Engine24==================================== 4616 4617Tue Jun 3 17:01:31 1997 Steven Eker <eker@lilac.csl.sri.com> 4618 4619 * ACU_CollapseMatcher.cc (uniqueCollapseMatch): now cope with 4620 abstraction variables 4621 (multiwayCollapseMatch): removed error check for matching identity 4622 at top because such a match may ultimately fail due to abstraction 4623 subproblems and is therefore not necessarily illegal. 4624 (collapseMatch): handle abstraction variables in multiway collapse 4625 case 4626 4627Mon Jun 2 11:16:05 1997 Steven Eker <eker@lilac.csl.sri.com> 4628 4629 * ACU_Symbol.cc (compileOpDeclarations): move identity code here 4630 because we need sorts to be done before we can do collapse analysis 4631 4632 * ACU_LhsAutomaton.cc (dump): handle abstraction variables 4633 4634 * ACU_Matcher.cc (match): Assert in wrong place 4635 4636 * ACU_Term.cc (determineCollapseSymbols): fixed bug where we had 4637 wrong test for setting p.collapseToOurSymbol 4638 4639 * ACU_LhsAutomaton.cc (addAbstractionVariable): fixed bug where we 4640 were assigning tv.upperBound to itself rather than initializing it 4641 from upperBound arg 4642 4643 * ACU_Matcher.cc (fullMatch): pass nrVariables arg to 4644 VariableAbstractionSubproblem() 4645 4646Fri May 30 11:56:07 1997 Steven Eker <eker@lilac.csl.sri.com> 4647 4648 * ACU_LhsCompiler1.cc (compileLhs): check abstractionVariableIndex 4649 against NONE rather than 0 4650 4651 * ACU_Matcher.cc (match): handle the variable only case 4652 case where the last unbound variable is an abstraction variable 4653 and there is nothing to bind it to except identity 4654 (forcedLoneVariableCase): rewritten to deal with abstraction variables 4655 (fullMatch): deal with abstraction variables 4656 4657 * ACU_LhsCompiler1.cc (compileLhs): rewritten to 4658 handle abstractionVariable and honorsGroundOutMatch() 4659 4660 * ACU_LhsAutomaton.cc (addTopVariable): set abstracted to 0 4661 4662 * ACU_LhsCompiler1.cc (analyseConstraintPropagation): rewritten to 4663 handle abstractionVariable and honorsGroundOutMatch() 4664 4665 * ACU_LhsAutomaton.cc (addAbstractionVariable): added 4666 4667 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): added abstracted 4668 field to struct TopVariable 4669 (class ACU_LhsAutomaton): added decl for addAbstractionVariable() 4670 4671Thu May 29 16:57:27 1997 Steven Eker <eker@lilac.csl.sri.com> 4672 4673 * ACU_Term.cc (determineCollapseSymbols): major rewrite to set 4674 honorsGroundOutMatch and collapseToOurSymbol and matchOurIdentity flags 4675 (dumpArguments): print collapseToOurSymbol and matchOurIdentity 4676 4677 * ACU_Term.hh (class ACU_Term): added collapseToOurSymbol and 4678 matchOurIdentity to struct Pair 4679 4680Wed May 28 11:29:39 1997 Steven Eker <eker@lilac.csl.sri.com> 4681 4682 * ACU_Subproblem.cc (deepSelfDestruct): fixed long standing memory 4683 leak where we were deleting rather than deepSelfDestruct()ing edge 4684 subproblems 4685 4686 * ACU_CollapseMatcher.cc (multiwayCollapseMatch): pass identityDag 4687 arg to bindUnboundVariablesToIdentity() 4688 (bindUnboundVariablesToIdentity): added identityDag arg 4689 4690 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): added identityDag 4691 arg to bindUnboundVariablesToIdentity() 4692 4693 * ACU_LhsAutomaton.cc: added include for SubproblemDisjunction 4694 4695 * ACU_CollapseMatcher.cc (multiwayCollapseMatch): now use 4696 SubproblemDisjunction rather than ACU_CollapseSubproblem 4697 4698Tue May 27 11:19:03 1997 Steven Eker <eker@lilac.csl.sri.com> 4699 4700 * ACU_CollapseMatcher.cc (multiwayCollapseMatch): considerably 4701 simplified using DagNode::matchVariable() 4702 4703Fri May 23 14:18:00 1997 Steven Eker <eker@lilac.csl.sri.com> 4704 4705 * ACU_CollapseSubproblem.cc: created 4706 4707 * ACU_CollapseMatcher.cc (multiwayCollapseMatch): general case added 4708 4709 * ACU_CollapseSubproblem.hh (class ACU_CollapseSubproblem): created 4710 4711 * ACU_CollapseMatcher.cc (uniqueCollapseMatch): code cleaning; 4712 vi eliminated 4713 (bindUnboundVariablesToIdentity): added 4714 (multiwayCollapseMatch): implemented 1 bound variable, identity 4715 subject, 0 viable variables and 1 viable variable cases 4716 4717Thu May 22 10:48:52 1997 Steven Eker <eker@lilac.csl.sri.com> 4718 4719 * ACU_Matcher.cc (match): Don't do matchAtTop assertion until 4720 we've established that the subject actualy has our symbol on top 4721 since an alien (e.g. free) symbol may not have extension. 4722 4723 * ACU_LhsCompiler1.cc (compileLhs): fixed bug where 4724 we were using !empty rather than !empty() to decide whether 4725 collapse possible 4726 (compileLhs): uniqueCollapseAutomaton must be passed our 4727 matchAtTop flag to ensure matching with extension is performed if 4728 necessary. 4729 4730 * ACU_CollapseMatcher.cc (multiwayCollapseMatch): added 4731 (uniqueCollapseMatch): added 4732 4733Wed May 21 15:19:01 1997 Steven Eker <eker@lilac.csl.sri.com> 4734 4735 * ACU_LhsAutomaton.cc (ACU_LhsAutomaton): initialize 4736 uniqueCollapseAutomaton 4737 4738 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): add 4739 uniqueCollapseAutomaton arg to ctor decl 4740 4741 * ACU_LhsCompiler1.cc (compileLhs): pass flag saying whether we 4742 could collapse to ACU_LhsAutomaton() 4743 (compileLhs): compute uniqueCollapseAutomaton if needed 4744 4745 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): add 4746 collapsePosible arg to ctor decl 4747 4748 * ACU_LhsAutomaton.cc (ACU_LhsAutomaton): initialize collapse 4749 possible flag 4750 4751 * ACU_Term.cc (determineCollapseSymbols): need to insert 4752 abstraction variables for subterms that can't collapse but which 4753 have our identity as their top symbol and are non-ground. 4754 (determineCollapseSymbols): non longer assume that a subterm might 4755 match the idenitity element because it has the same top symbol as 4756 the identity element - check to see also that it is non-ground. 4757 4758Tue May 20 16:24:31 1997 Steven Eker <eker@lilac.csl.sri.com> 4759 4760 * ACU_Term.cc (dumpArguments): added 4761 4762 * ACU_Term.hh (class ACU_Term): added decl for dumpArguments() 4763 4764 * ACU_Matcher.cc (match): temporarily comment out unfinished 4765 collapse code so we can test variable abstraction 4766 4767 * ACU_Term.cc (determineCollapseSymbols): rewritten to do 4768 selective variable abstraction 4769 4770Mon May 19 10:48:23 1997 Steven Eker <eker@lilac.csl.sri.com> 4771 4772 * ACU_Term.cc (determineCollapseSymbols): now fill out 4773 uniqueCollapseSubtermIndex and abstractionVariableIndex 4774 4775 * ACU_Term.hh (class ACU_Term): added uniqueCollapseSubtermIndex 4776 (class ACU_Term): added abstractionVariableIndex to Pair (no 4777 longer really a pair! If this works out we will rename it to Triple. 4778 4779Fri May 16 11:38:36 1997 Steven Eker <eker@lilac.csl.sri.com> 4780 4781 * ACU_CollapseMatcher.cc: created 4782 4783 * ACU_Matcher.cc (match): added call to collapseMatch() in the 4784 case where top symbol mis-matches and collapsePossible 4785 4786 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): added 4787 collapsePossible flag and uniqueCollapseAutomaton pointer 4788 4789 * ACU_Term.cc (compileRhs): pass Term* rather than Symbol* for 4790 first arg of addArgument() 4791 4792 * ACU_RhsAutomaton.hh (class ACU_RhsAutomaton): change decl for 4793 addArgument() 4794 4795 * ACU_RhsAutomaton.cc (addArgument): rewritten to use se 4796 Term::stable() rather than Symbol::stable(). First arg is now a Term* 4797 4798 * ACU_LhsAutomaton.cc (addGroundedOutAlien): use Term::stable() 4799 rather than Symbol::stable() 4800 (addNonGroundAlien): use Term::stable() rather than Symbol::stable() 4801 4802Wed May 14 15:42:04 1997 Steven Eker <eker@lilac.csl.sri.com> 4803 4804 * ACU_Term.cc (analyseCollapses): deleted 4805 4806 * ACU_Term.hh (class ACU_Term): deleted analyseCollapses() decl 4807 4808 * ACU_Term.cc (determineCollapseSymbols): added 4809 4810 * ACU_Term.hh (class ACU_Term): added decl for determineCollapseSymbols() 4811 4812 * ACU_Symbol.cc (eqRewrite): changed comment on repudiate call now 4813 that inErrorSort() can leave sort info behind 4814 4815Tue May 13 10:29:27 1997 Steven Eker <eker@lilac.csl.sri.com> 4816 4817 * ACU_LhsAutomaton.cc: comment out #include "sortCheckSubproblem.hh" 4818 4819 * ACU_Matcher.cc (forcedLoneVariableCase): use 4820 DagNode::checkSort() to simplify code 4821 4822Fri May 9 15:55:04 1997 Steven Eker <eker@lilac.csl.sri.com> 4823 4824 * ACU_Term.cc (analyseCollapses): fixed bug where we need to check 4825 multiplicity against 1 in order to return early 4826 4827Wed May 7 16:46:17 1997 Steven Eker <eker@lilac.csl.sri.com> 4828 4829 * ACU_Term.cc (analyseCollapses): added 4830 4831Thu Apr 10 16:16:03 1997 Steven Eker <eker@lilac.csl.sri.com> 4832 4833 * ACU_Matcher.cc (forcedLoneVariableCase): must repudiateSort() in 4834 the case where the base sort is not small enough and 4835 the top symbol is not sort constraint free as the 4836 base sort we calculated may not be the true sort and will inhibit 4837 the calculation of the true sort during the solution of the sort 4838 check subprblem. 4839 4840Wed Apr 2 16:54:05 1997 Steven Eker <eker@lilac.csl.sri.com> 4841 4842 * ACU_Subproblem.cc (solveVariables): when solving a trivial 4843 system with extension, use extensionInfo->setWholeFlag(true) 4844 rather than extensionInfo->clear() (trying to fix UMR: 4845 Uninitialized memory read reported by purify). 4846 4847Fri Mar 28 16:51:53 1997 Steven Eker <eker@lilac.csl.sri.com> 4848 4849 * ACU_DagNode.hh (class ACU_DagNode): decl for makeExtensionInfo() 4850 added 4851 4852 * ACU_DagNode.cc (makeExtensionInfo): added 4853 4854Wed Mar 26 11:02:46 1997 Steven Eker <eker@lilac.csl.sri.com> 4855 4856 * ACU_Matcher.cc (buildBipartiteGraph): rewritten to use findFirstOccurrence() 4857 (aliensOnlyMatch): rewritten to use findFirstOccurrence() 4858 (eliminateGroundedOutAliens): rewritten to use findFirstOccurrence() 4859 4860 * ACU_GreedyMatcher.cc (greedyMatch): test top symbol before multiplicity 4861 4862Tue Mar 25 12:17:05 1997 Steven Eker <eker@lilac.csl.sri.com> 4863 4864 * ACU_GreedyMatcher.cc (greedyMatch): rewritten to use findFirstOccurrence() 4865 4866 * ACU_DagNode.hh (class ACU_DagNode): added decl for 4867 findFirstOccurrence() 4868 4869 * ACU_DagNode.cc (findFirstOccurrence): added 4870 4871 * ACU_Subproblem.cc (computeAssignment): initialized col to avoid 4872 spurious uninit warning from g++ 4873 4874 * ACU_LhsCompiler3.cc (compileGreedyAndFullCases): pass term in 4875 addNonGroundAlien() call 4876 4877 * ACU_LhsCompiler2.cc (compileAliensOnlyCase): pass term in 4878 addNonGroundAlien() calls 4879 4880 * ACU_LhsCompiler1.cc (compileLhs): pass term in 4881 addGroundedOutAlien() call 4882 4883 * ACU_LhsAutomaton.cc (addGroundedOutAlien): store topSymbol if 4884 stable, 0 otherwise 4885 (addNonGroundAlien): store topSymbol if stable, 0 otherwise 4886 4887 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): added topSymbol field 4888 to NonGroundAlien struct; added Term* alien arg to 4889 addGroundedOutAlien() and addNonGroundAlien() 4890 4891 * ACU_GreedyMatcher.cc (greedyPureMatch): new condition for 4892 choosing between false and UNDECIDED when we can't find a variable 4893 to assign some subject to in phase 2. 4894 4895Fri Mar 21 18:54:28 1997 Steven Eker <eker@lilac.csl.sri.com> 4896 4897 * ACU_GreedyMatcher.cc (greedyPureMatch): new technique for 4898 calculating failure mode in phase 1. 4899 (greedyMatch): call greedyPureMatch with extra arg 4900 4901 * ACU_Matcher.cc (match): call greedyPureMatch with extra arg 4902 4903Thu Mar 20 16:05:15 1997 Steven Eker <eker@lilac.csl.sri.com> 4904 4905 * ACU_Matcher.cc (multiplicityChecks): split off case where 4906 maxPatternMultiplicity = 1 4907 4908 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): extensionInfo 4909 removed from multiplicityChecks and totalMultiplicity added as 4910 data member; the aim is to save the totalSubjectMultiplicity so we 4911 don't have to mess with extensionInfo until it is clear that it is 4912 needed. (After checking with quantify) 4913 4914Tue Mar 18 16:07:47 1997 Steven Eker <eker@lilac.csl.sri.com> 4915 4916 * ACU_Symbol.cc (matchVariableWithExtension): set extensionInfo 4917 upperBound to avoid crashing when trying to build diophantine system 4918 4919Wed Feb 19 16:08:49 1997 Steven Eker <eker@lilac.csl.sri.com> 4920 4921 * ACU_LhsCompiler3.cc (findFullSequence): remember to expand 4922 sequenece before putting stuff in it. 4923 4924Thu Feb 13 10:41:49 1997 Steven Eker <eker@lilac.csl.sri.com> 4925 4926 * ACU_LhsCompiler1.cc (compileLhs): greedy = !inErrorSort 4927 4928Wed Feb 12 16:11:35 1997 Steven Eker <eker@lilac.csl.sri.com> 4929 4930 * ACU_GreedyMatcher.cc (greedyPureMatch): make sure we don't 4931 assign to much to extension 4932 4933 * ACU_Subproblem.cc (extractDiophantineSystem): use extensionInfo 4934 upper bound to bound extension row in diophantine system 4935 4936 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): amended 4937 multiplicityChecks() decl 4938 4939 * ACU_ExtensionInfo.hh (setUpperBound): added 4940 (getUpperBound): added 4941 4942 * ACU_Matcher.cc (match): pass extensionInfo to 4943 multiplicityChecks(); test extensionInfo rather than matchAtTop 4944 (multiplicityChecks): set upper bound on size of extension if necessary 4945 4946 * ACU_Subproblem.hh (class ACU_Subproblem): identityDag deleted 4947 4948 * ACU_Subproblem.cc (solveVariables): added code to bind variables 4949 to idenity in the case where ther are unbound variables and no system 4950 (solveVariables): handle the case where the sort of the dag node 4951 reeturn by computeAssignment() is unknown; this can only be the 4952 identity case 4953 (solveVariables): unbinding code simplified 4954 (extractDiophantineSystem): handle case where there are no 4955 unused subjects but all variables case take the identity by 4956 keeping track of nrNonIdentityVariables 4957 (computeAssignment): don't bother computing the sort of the 4958 identity dag since our lower bound condition guarentees that the 4959 variable can take the identity element 4960 (computeAssignment): return 0 in identity case 4961 (solveVariables): handle case where 0 is returned from computeAssignment() 4962 4963Fri Feb 7 14:49:35 1997 Steven Eker <eker@lilac.csl.sri.com> 4964 4965 * ACU_Term.cc (findEagerVariables): static_cast removed for symbol() 4966 (markEagerArguments): static_cast removed for symbol() 4967 4968 * ACU_DagNode.cc (copyEagerUptoReduced): static_cast removed for symbol() 4969 (overwriteWithClone): static_cast removed for symbol() 4970 (makeClone): static_cast removed for symbol() 4971 (copyWithReplacement): static_cast removed for symbol() 4972 (partialReplace): static_cast removed for symbol() 4973 (partialConstruct): static_cast removed for symbol() 4974 (eliminateArgument): static_cast removed for symbol() 4975 4976 * ACU_DagNode.hh (symbol): added 4977 4978 * ACU_Subproblem.hh (class ACU_Subproblem): identityDag pointer added 4979 4980 * ACU_Subproblem.cc (addEdge): optimized 4981 (addTopVariable): optimized 4982 (extractDiophantineSystem): optimized 4983 (solveVariables): zero out idenity dag pointer since the identity 4984 element that it may point to may get garbage collected before in 4985 can be used 4986 (computeAssignment): handle identity case 4987 4988 * ACU_Matcher.cc (fullMatch): pass 0 as lower bound for variables 4989 that can take identity 4990 4991 * ACU_LhsCompiler1.cc (compileLhs): set error sort flag only if we 4992 are matching with extension. Prevent compiling with greedy 4993 strategy if we are in the error sort flag is set. 4994 This fixes a bug because the ACU 4995 greedy matcher does not do sort check for matched part. 4996 4997Thu Feb 6 16:46:16 1997 Steven Eker <eker@lilac.csl.sri.com> 4998 4999 * ACU_GreedyMatcher.cc (greedyMatch): simplified 5000 (greedyPureMatch): deal with identity in first phase by allowing a 5001 variable with takeIdentity set to have no firstSubject if none can 5002 be found. 5003 (greedyPureMatch): in 3rd phase deal with variables that were 5004 assigned nothing by binding them to identity dag 5005 5006Wed Feb 5 11:57:26 1997 Steven Eker <eker@lilac.csl.sri.com> 5007 5008 * ACU_Symbol.cc (ACU_Symbol): zero identityAutomaton and 5009 identitySubstitution. Handle no identity case. 5010 5011 * ACU_Symbol.hh (makeIdentityDag): added 5012 5013 * ACU_Symbol.cc (compileEquations): added code to compile a 5014 rhsAutomaton for our identity element. Handle no identity case 5015 5016 * ACU_GreedyMatcher.cc: created 5017 5018 * ACU_Matcher.cc (multiplicityChecks): totalPatternMultiplicity -> 5019 totalLowerBound 5020 (eliminateBoundVariables): handle the case where a top variable is 5021 bound to our identity 5022 (match): recognize and handle special case of one variable which 5023 can take identity vs no subjects (no extension case) 5024 5025Tue Feb 4 12:18:37 1997 Steven Eker <eker@lilac.csl.sri.com> 5026 5027 * ACU_LhsAutomaton.cc (updateTotals): totalPatternMultiplicity -> 5028 totalLowerBound 5029 (addTopVariable): fill out takeIdentity field and take it into 5030 account when updating totals 5031 (dump): output takeIdenity field 5032 5033 * ACU_LhsAutomaton.hh (class ACU_LhsAutomaton): takeIdentity field 5034 added to struct TopVariable 5035 (class ACU_LhsAutomaton): totalPatternMultiplicity -> 5036 totalLowerBound (since identity may result in some pattern 5037 variables not being counted) 5038 5039 * ACU_LhsCompiler3.cc (findFullSequence): use weakConstraintPropogation() 5040 5041 * ACU_LhsCompiler2.cc (compileAliensOnlyCase): use weakConstraintPropogation() 5042 5043 * ACU_LhsCompiler1.cc (weakConstraintPropogation): added 5044 5045 * ACU_LhsCompiler3.cc (compileGreedyAndFullCases): simplified 5046 using findFullSequence() 5047 (findFullSequence): added 5048 5049Fri Jan 31 17:07:29 1997 Steven Eker <eker@lilac.csl.sri.com> 5050 5051 * ACU_LhsCompiler3.cc (compileGreedyAndFullCases): removed greedy 5052 argument; code cleaning 5053 (lengthCompare): deleted 5054 (findGreedySequence): no longer deal with fully independent aliens 5055 first as I can't see any justification for doing so 5056 (findIndependentSets): no longer sort independent sets by length 5057 (can't think of any justification). 5058 5059 * ACU_LhsCompiler1.cc (compileLhs): compileGreedyAndFullCases() no 5060 longer takes greedy argument 5061 5062 * ACU_LhsCompiler2.cc (compileAliensOnlyCase): code cleaning 5063 5064 * ACU_LhsCompiler1.cc (compileLhs): code cleaning; make sure 5065 subproblemLikely is false in lone variable case 5066 5067Thu Jan 30 16:17:56 1997 Steven Eker <eker@lilac.csl.sri.com> 5068 5069 * ACU_LhsCompiler3.cc: created 5070 (compileGreedyAndFullCases): added 5071 5072 * ACU_Term.hh (symbol): added 5073 5074 * ACU_LhsCompiler2.cc: created 5075 (compileAliensOnlyCase): added 5076 5077Mon Jan 27 10:59:41 1997 Steven Eker <eker@lilac.csl.sri.com> 5078 5079 * ACU_LhsAutomaton.hh: created 5080 5081 * ACU_LhsAutomaton.cc: created 5082 5083 * ACU_Matcher.cc: created 5084 5085Thu Jan 16 18:17:11 1997 Steven Eker <eker@lilac.csl.sri.com> 5086 5087 * ACU_RhsAutomaton.hh (class ACU_RhsAutomaton): topSymbol is 5088 ACU_Symbol* rather that Symbol* 5089 5090 * ACU_RhsAutomaton.cc (construct): added call to eliminate identity 5091 elements 5092 (replace): added call to eliminate identity elements 5093 (ACU_RhsAutomaton): take ACU_Symbol* rather that Symbol* 5094 5095Mon Jan 13 12:53:38 1997 Steven Eker <eker@lilac.csl.sri.com> 5096 5097 * ACU_RhsAutomaton.hh: created 5098 5099Fri Jan 10 11:15:42 1997 Steven Eker <eker@lilac.csl.sri.com> 5100 5101 * ACU_Term.cc: created 5102 (normalize): now delete idenity elements, collapsing to subterm 5103 where necessary 5104 5105 * ACU_DagNode.hh (class ACU_DagNode): enum NormalizationResult 5106 removed; declaration for eliminateArgument() added 5107 5108 * ACU_DagNode.cc (copyWithReplacement): handle case where collapse 5109 is avoided because single remaining argument has multiplicity > 1 5110 (partialReplace): handle case where collapse 5111 is avoided because single remaining argument has multiplicity > 1 5112 (partialConstruct): handle case where collapse 5113 is avoided because single remaining argument has multiplicity > 1 5114 (eliminateArgument): added to handle the removal of identity elements 5115 5116Thu Jan 9 15:40:11 1997 Steven Eker <eker@lilac.csl.sri.com> 5117 5118 * ACU_DagNode.cc: created 5119 (overwriteWithClone): fixed serious bug where we were copying sort 5120 of overwritten node rather than overwriting node 5121 (mergeSortAndUniquize): old commented out flip code removed 5122 (eliminateSubject): unnecessary ACU_DagNode::'s removed 5123 (partialConstruct): handle case where replacement it the identity element 5124 (partialReplace): handle case where replacement it the identity element 5125 (copyWithReplacement): handle case where replacement it the identity element 5126 5127Wed Jan 8 10:26:06 1997 Steven Eker <eker@lilac.csl.sri.com> 5128 5129 * ACU_Symbol.cc (eqRewrite): now cope with the possibility that 5130 whenever we normalize at top it is possible that we could collpase 5131 out of the current theory 5132 (computeBaseSort): added uniform sort code optimization; 5133 simplified uniform sort code computation by passing vectors of 5134 sort codes rather thhan vectors of vectors of int 5135 5136 * ACU_DagNode.hh (class ACU_DagNode): added enum NormalizationResult 5137 5138 * ACU_Symbol.cc: created 5139 (~ACU_Symbol): added 5140 (compileEquations): added as a hack to process identity element 5141 after all other op decl processing has been done. 5142 (ACU_Symbol): do normalization here to avoid problem of later 5143 identities that could possibly depend on this one. 5144 5145 * ACU_DagArgumentIterator.cc: created 5146 5147 * ACU_ArgumentIterator.hh (class ACU_ArgumentIterator): created 5148 5149 * ACU_DagArgumentIterator.hh (class ACU_DagArgumentIterator): created 5150 5151 * ACU_ArgumentIterator.cc: created 5152 5153 * ACU_ExtensionInfo.hh (class ACU_ExtensionInfo): created 5154 5155 * ACU_Theory.cc: created 5156 5157 * ACU_Theory.hh: created 5158 5159 * ACU_Term.hh (class ACU_Term): created 5160 5161 * ACU_Symbol.hh (getIdentity): added 5162 5163 * ACU_DagNode.hh (class ACU_DagNode): created 5164 5165 * ACU_Symbol.hh (class ACU_Symbol): created 5166 5167