1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2011-2021 Laboratoire de Recherche et Developpement 3 // de l'Epita (LRDE). 4 // 5 // This file is part of Spot, a model checking library. 6 // 7 // Spot is free software; you can redistribute it and/or modify it 8 // under the terms of the GNU General Public License as published by 9 // the Free Software Foundation; either version 3 of the License, or 10 // (at your option) any later version. 11 // 12 // Spot is distributed in the hope that it will be useful, but WITHOUT 13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 15 // License for more details. 16 // 17 // You should have received a copy of the GNU General Public License 18 // along with this program. If not, see <http://www.gnu.org/licenses/>. 19 20 #include "config.h" 21 #include <iostream> 22 //#define TRACE 23 #ifdef TRACE 24 #define trace std::cerr 25 #else 26 #define trace while (0) std::cerr 27 #endif 28 29 #include <spot/tl/simplify.hh> 30 #include <spot/priv/robin_hood.hh> 31 #include <spot/tl/contain.hh> 32 #include <spot/tl/print.hh> 33 #include <spot/tl/snf.hh> 34 #include <spot/tl/length.hh> 35 #include <spot/twa/formula2bdd.hh> 36 #include <spot/misc/minato.hh> 37 #include <cassert> 38 #include <memory> 39 #include <unordered_set> 40 #include <map> 41 42 43 44 namespace spot 45 { 46 typedef std::vector<formula> vec; 47 48 // The name of this class is public, but not its contents. 49 class tl_simplifier_cache final 50 { 51 typedef robin_hood::unordered_map<formula, formula> f2f_map; 52 typedef robin_hood::unordered_map<formula, bdd> f2b_map; 53 typedef robin_hood::unordered_map<int, formula> b2f_map; 54 typedef std::pair<formula, formula> pairf; 55 typedef std::map<pairf, bool> syntimpl_cache_t; 56 public: 57 bdd_dict_ptr dict; 58 tl_simplifier_options options; 59 language_containment_checker lcc; 60 ~tl_simplifier_cache()61 ~tl_simplifier_cache() 62 { 63 dict->unregister_all_my_variables(this); 64 } 65 tl_simplifier_cache(const bdd_dict_ptr & d)66 tl_simplifier_cache(const bdd_dict_ptr& d) 67 : dict(d), lcc(d, true, true, false, false) 68 { 69 } 70 tl_simplifier_cache(const bdd_dict_ptr & d,const tl_simplifier_options & opt)71 tl_simplifier_cache(const bdd_dict_ptr& d, 72 const tl_simplifier_options& opt) 73 : dict(d), options(opt), 74 lcc(d, true, true, false, false, opt.containment_max_states) 75 { 76 options.containment_checks |= options.containment_checks_stronger; 77 options.event_univ |= options.favor_event_univ; 78 } 79 80 void print_stats(std::ostream & os) const81 print_stats(std::ostream& os) const 82 { 83 os << "simplified formulae: " << simplified_.size() << " entries\n" 84 << "negative normal form: " << nenoform_.size() << " entries\n" 85 << "syntactic implications: " << syntimpl_.size() << " entries\n" 86 << "boolean to bdd: " << as_bdd_.size() << " entries\n" 87 << "star normal form: " << snf_cache_.size() << " entries\n" 88 << "boolean isop: " << bool_isop_.size() << " entries\n" 89 << "as dnf: " << as_dnf_.size() << " entries\n" 90 << "as cnf: " << as_cnf_.size() << " entries\n"; 91 } 92 93 void clear_as_bdd_cache()94 clear_as_bdd_cache() 95 { 96 as_bdd_.clear(); 97 for (auto p: bdd_to_f_) 98 dict->unregister_variable(p.first, this); 99 bdd_to_f_.clear(); 100 } 101 102 // Convert a Boolean formula into a BDD for easier comparison. 103 bdd as_bdd(formula f)104 as_bdd(formula f) 105 { 106 // Lookup the result in case it has already been computed. 107 f2b_map::const_iterator it = as_bdd_.find(f); 108 if (it != as_bdd_.end()) 109 return it->second; 110 111 bdd result = bddfalse; 112 113 switch (f.kind()) 114 { 115 case op::tt: 116 result = bddtrue; 117 break; 118 case op::ff: 119 result = bddfalse; 120 break; 121 case op::ap: 122 result = bdd_ithvar(dict->register_proposition(f, this)); 123 break; 124 case op::Not: 125 result = !as_bdd(f[0]); 126 break; 127 case op::Xor: 128 { 129 bdd l = as_bdd(f[0]); 130 result = bdd_apply(l, as_bdd(f[1]), bddop_xor); 131 break; 132 } 133 case op::Implies: 134 { 135 bdd l = as_bdd(f[0]); 136 result = bdd_apply(l, as_bdd(f[1]), bddop_imp); 137 break; 138 } 139 case op::Equiv: 140 { 141 bdd l = as_bdd(f[0]); 142 result = bdd_apply(l, as_bdd(f[1]), bddop_biimp); 143 break; 144 } 145 case op::And: 146 { 147 result = bddtrue; 148 for (auto c: f) 149 result &= as_bdd(c); 150 break; 151 } 152 case op::Or: 153 { 154 result = bddfalse; 155 for (auto c: f) 156 result |= as_bdd(c); 157 break; 158 } 159 default: 160 { 161 unsigned var = dict->register_anonymous_variables(1, this); 162 bdd_to_f_[var] = f; 163 result = bdd_ithvar(var); 164 break; 165 } 166 } 167 168 // Cache the result before returning. 169 as_bdd_[f] = result; 170 return result; 171 } 172 as_xnf(formula f,bool cnf)173 formula as_xnf(formula f, bool cnf) 174 { 175 bdd in = as_bdd(f); 176 if (cnf) 177 in = !in; 178 minato_isop isop(in); 179 bdd cube; 180 vec clauses; 181 while ((cube = isop.next()) != bddfalse) 182 { 183 vec literals; 184 while (cube != bddtrue) 185 { 186 int var = bdd_var(cube); 187 const bdd_dict::bdd_info& i = dict->bdd_map[var]; 188 formula res; 189 if (i.type == bdd_dict::var) 190 { 191 res = i.f; 192 } 193 else 194 { 195 res = bdd_to_f_[var]; 196 assert(res); 197 } 198 bdd high = bdd_high(cube); 199 if (high == bddfalse) 200 { 201 if (!cnf) 202 res = formula::Not(res); 203 cube = bdd_low(cube); 204 } 205 else 206 { 207 if (cnf) 208 res = formula::Not(res); 209 // If bdd_low is not false, then cube was not a 210 // conjunction. 211 assert(bdd_low(cube) == bddfalse); 212 cube = high; 213 } 214 assert(cube != bddfalse); 215 literals.emplace_back(res); 216 } 217 if (cnf) 218 clauses.emplace_back(formula::Or(literals)); 219 else 220 clauses.emplace_back(formula::And(literals)); 221 } 222 if (cnf) 223 return formula::And(clauses); 224 else 225 return formula::Or(clauses); 226 } 227 as_dnf(formula f)228 formula as_dnf(formula f) 229 { 230 auto i = as_dnf_.find(f); 231 if (i != as_dnf_.end()) 232 return i->second; 233 formula r = as_xnf(f, false); 234 as_dnf_[f] = r; 235 return r; 236 } 237 as_cnf(formula f)238 formula as_cnf(formula f) 239 { 240 auto i = as_cnf_.find(f); 241 if (i != as_cnf_.end()) 242 return i->second; 243 formula r = as_xnf(f, true); 244 as_cnf_[f] = r; 245 return r; 246 } 247 248 249 250 formula lookup_nenoform(formula f)251 lookup_nenoform(formula f) 252 { 253 f2f_map::const_iterator i = nenoform_.find(f); 254 if (i == nenoform_.end()) 255 return nullptr; 256 return i->second; 257 } 258 259 void cache_nenoform(formula orig,formula nenoform)260 cache_nenoform(formula orig, formula nenoform) 261 { 262 nenoform_[orig] = nenoform; 263 } 264 265 // Return true iff the option set (syntactic implication 266 // or containment checks) allow to prove that f1 => f2. 267 bool implication(formula f1,formula f2)268 implication(formula f1, formula f2) 269 { 270 trace << "[->] does " << str_psl(f1) << " implies " 271 << str_psl(f2) << " ?" << std::endl; 272 if ((options.synt_impl && syntactic_implication(f1, f2)) 273 || (options.containment_checks && contained(f1, f2))) 274 { 275 trace << "[->] Yes" << std::endl; 276 return true; 277 } 278 trace << "[->] No" << std::endl; 279 return false; 280 } 281 282 // Return true if f1 => f2 syntactically 283 bool 284 syntactic_implication(formula f1, formula f2); 285 bool 286 syntactic_implication_aux(formula f1, formula f2); 287 288 // Return true if f1 => f2 289 bool contained(formula f1,formula f2)290 contained(formula f1, formula f2) 291 { 292 if (!f1.is_psl_formula() || !f2.is_psl_formula()) 293 return false; 294 return lcc.contained(f1, f2); 295 } 296 297 // If right==false, true if !f1 => f2, false otherwise. 298 // If right==true, true if f1 => !f2, false otherwise. 299 bool 300 syntactic_implication_neg(formula f1, formula f2, 301 bool right); 302 303 // Return true if f1 => !f2 contained_neg(formula f1,formula f2)304 bool contained_neg(formula f1, formula f2) 305 { 306 if (!f1.is_psl_formula() || !f2.is_psl_formula()) 307 return false; 308 trace << "[CN] Does (" << str_psl(f1) << ") imply !(" 309 << str_psl(f2) << ") ?" << std::endl; 310 if (lcc.contained_neg(f1, f2)) 311 { 312 trace << "[CN] Yes" << std::endl; 313 return true; 314 } 315 else 316 { 317 trace << "[CN] No" << std::endl; 318 return false; 319 } 320 } 321 322 // Return true if !f1 => f2 neg_contained(formula f1,formula f2)323 bool neg_contained(formula f1, formula f2) 324 { 325 if (!f1.is_psl_formula() || !f2.is_psl_formula()) 326 return false; 327 trace << "[NC] Does !(" << str_psl(f1) << ") imply (" 328 << str_psl(f2) << ") ?" << std::endl; 329 if (lcc.neg_contained(f1, f2)) 330 { 331 trace << "[NC] Yes" << std::endl; 332 return true; 333 } 334 else 335 { 336 trace << "[NC] No" << std::endl; 337 return false; 338 } 339 } 340 341 // Return true iff the option set (syntactic implication 342 // or containment checks) allow to prove that 343 // - !f1 => f2 (case where right=false) 344 // - f1 => !f2 (case where right=true) 345 bool implication_neg(formula f1,formula f2,bool right)346 implication_neg(formula f1, formula f2, bool right) 347 { 348 trace << "[IN] Does " << (right ? "(" : "!(") 349 << str_psl(f1) << ") imply " 350 << (right ? "!(" : "(") << str_psl(f2) << ") ?" 351 << std::endl; 352 if ((options.synt_impl && syntactic_implication_neg(f1, f2, right)) 353 || (options.containment_checks && right && contained_neg(f1, f2)) 354 || (options.containment_checks && !right && neg_contained(f1, f2))) 355 { 356 trace << "[IN] Yes" << std::endl; 357 return true; 358 } 359 else 360 { 361 trace << "[IN] No" << std::endl; 362 return false; 363 } 364 } 365 366 formula lookup_simplified(formula f)367 lookup_simplified(formula f) 368 { 369 f2f_map::const_iterator i = simplified_.find(f); 370 if (i == simplified_.end()) 371 return nullptr; 372 return i->second; 373 } 374 375 void cache_simplified(formula orig,formula simplified)376 cache_simplified(formula orig, formula simplified) 377 { 378 simplified_[orig] = simplified; 379 } 380 381 formula star_normal_form(formula f)382 star_normal_form(formula f) 383 { 384 return spot::star_normal_form(f, &snf_cache_); 385 } 386 387 formula star_normal_form_bounded(formula f)388 star_normal_form_bounded(formula f) 389 { 390 return spot::star_normal_form_bounded(f, &snfb_cache_); 391 } 392 393 394 formula boolean_to_isop(formula f)395 boolean_to_isop(formula f) 396 { 397 f2f_map::const_iterator it = bool_isop_.find(f); 398 if (it != bool_isop_.end()) 399 return it->second; 400 401 assert(f.is_boolean()); 402 formula res = bdd_to_formula(as_bdd(f), dict); 403 bool_isop_[f] = res; 404 return res; 405 } 406 407 private: 408 f2b_map as_bdd_; 409 b2f_map bdd_to_f_; 410 f2f_map simplified_; 411 f2f_map as_dnf_; 412 f2f_map as_cnf_; 413 f2f_map nenoform_; 414 syntimpl_cache_t syntimpl_; 415 snf_cache snf_cache_; 416 snf_cache snfb_cache_; 417 f2f_map bool_isop_; 418 }; 419 420 421 namespace 422 { 423 ////////////////////////////////////////////////////////////////////// 424 // 425 // NEGATIVE_NORMAL_FORM 426 // 427 ////////////////////////////////////////////////////////////////////// 428 429 formula 430 nenoform_rec(formula f, bool negated, tl_simplifier_cache* c, 431 bool deep); 432 equiv_or_xor(bool equiv,formula f1,formula f2,tl_simplifier_cache * c,bool deep)433 formula equiv_or_xor(bool equiv, formula f1, formula f2, 434 tl_simplifier_cache* c, bool deep) 435 { 436 auto rec = [c, deep](formula f, bool negated) 437 { 438 return nenoform_rec(f, negated, c, deep); 439 }; 440 441 if (equiv) 442 { 443 // Rewrite a<=>b as (a&b)|(!a&!b) 444 auto recurse_f1_false = rec(f1, false); 445 auto recurse_f2_false = rec(f2, false); 446 if (!deep && c->options.keep_top_xor) 447 return formula::Equiv(recurse_f1_false, recurse_f2_false); 448 auto recurse_f1_true = rec(f1, true); 449 auto recurse_f2_true = rec(f2, true); 450 auto left = formula::And({recurse_f1_false, recurse_f2_false}); 451 auto right = formula::And({recurse_f1_true, recurse_f2_true}); 452 return formula::Or({left, right}); 453 } 454 else 455 { 456 // Rewrite a^b as (a&!b)|(!a&b) 457 auto recurse_f1_false = rec(f1, false); 458 auto recurse_f2_false = rec(f2, false); 459 if (!deep && c->options.keep_top_xor) 460 return formula::Xor(recurse_f1_false, recurse_f2_false); 461 auto recurse_f1_true = rec(f1, true); 462 auto recurse_f2_true = rec(f2, true); 463 auto left = formula::And({recurse_f1_false, recurse_f2_true}); 464 auto right = formula::And({recurse_f1_true, recurse_f2_false}); 465 return formula::Or({left, right}); 466 } 467 } 468 469 // The deep argument indicate whether we are under a temporal 470 // operator (except X). 471 formula nenoform_rec(formula f,bool negated,tl_simplifier_cache * c,bool deep)472 nenoform_rec(formula f, bool negated, tl_simplifier_cache* c, 473 bool deep) 474 { 475 if (f.is(op::Not)) 476 { 477 negated = !negated; 478 f = f[0]; 479 } 480 481 formula key = f; 482 if (negated) 483 key = formula::Not(f); 484 formula result = c->lookup_nenoform(key); 485 if (result) 486 return result; 487 488 if (key.is_in_nenoform() 489 || (c->options.nenoform_stop_on_boolean && key.is_boolean())) 490 { 491 result = key; 492 } 493 else 494 { 495 auto rec = [c, &deep](formula f, bool neg) 496 { 497 return nenoform_rec(f, neg, c, deep); 498 }; 499 500 switch (op o = f.kind()) 501 { 502 case op::ff: 503 case op::tt: 504 // Negation of constants is taken care of in the 505 // constructor of unop::Not, so these cases should be 506 // caught by nenoform_recursively(). 507 assert(!negated); 508 result = f; 509 break; 510 case op::ap: 511 result = negated ? formula::Not(f) : f; 512 break; 513 case op::X: 514 case op::strong_X: 515 // Currently we don't distinguish between weak and 516 // strong semantics, so we treat the two operators 517 // identically. 518 // 519 // !Xa == X!a 520 // !X[!]a = X!a 521 result = formula::X(rec(f[0], negated)); 522 break; 523 case op::F: 524 // !Fa == G!a 525 deep = true; 526 result = formula::unop(negated ? op::G : op::F, 527 rec(f[0], negated)); 528 break; 529 case op::G: 530 // !Ga == F!a 531 deep = true; 532 result = formula::unop(negated ? op::F : op::G, 533 rec(f[0], negated)); 534 break; 535 case op::Closure: 536 deep = true; 537 result = formula::unop(negated ? 538 op::NegClosure : op::Closure, 539 rec(f[0], false)); 540 break; 541 case op::NegClosure: 542 case op::NegClosureMarked: 543 deep = true; 544 result = formula::unop(negated ? op::Closure : o, 545 rec(f[0], false)); 546 break; 547 548 case op::Implies: 549 if (negated) 550 // !(a => b) == a & !b 551 { 552 auto f2 = rec(f[1], true); 553 result = formula::And({rec(f[0], false), f2}); 554 } 555 else // a => b == !a | b 556 { 557 auto f2 = rec(f[1], false); 558 result = formula::Or({rec(f[0], true), f2}); 559 } 560 break; 561 case op::Xor: 562 { 563 // !(a ^ b) == a <=> b 564 result = equiv_or_xor(negated, f[0], f[1], c, deep); 565 break; 566 } 567 case op::Equiv: 568 { 569 // !(a <=> b) == a ^ b 570 result = equiv_or_xor(!negated, f[0], f[1], c, deep); 571 break; 572 } 573 case op::U: 574 { 575 deep = true; 576 // !(a U b) == !a R !b 577 auto f1 = rec(f[0], negated); 578 auto f2 = rec(f[1], negated); 579 result = formula::binop(negated ? op::R : op::U, f1, f2); 580 break; 581 } 582 case op::R: 583 { 584 deep = true; 585 // !(a R b) == !a U !b 586 auto f1 = rec(f[0], negated); 587 auto f2 = rec(f[1], negated); 588 result = formula::binop(negated ? op::U : op::R, f1, f2); 589 break; 590 } 591 case op::W: 592 { 593 deep = true; 594 // !(a W b) == !a M !b 595 auto f1 = rec(f[0], negated); 596 auto f2 = rec(f[1], negated); 597 result = formula::binop(negated ? op::M : op::W, f1, f2); 598 break; 599 } 600 case op::M: 601 { 602 deep = true; 603 // !(a M b) == !a W !b 604 auto f1 = rec(f[0], negated); 605 auto f2 = rec(f[1], negated); 606 result = formula::binop(negated ? op::W : op::M, f1, f2); 607 break; 608 } 609 case op::Or: 610 case op::And: 611 { 612 unsigned mos = f.size(); 613 vec v; 614 for (unsigned i = 0; i < mos; ++i) 615 v.emplace_back(rec(f[i], negated)); 616 op on = o; 617 if (negated) 618 on = o == op::Or ? op::And : op::Or; 619 result = formula::multop(on, v); 620 break; 621 } 622 case op::OrRat: 623 case op::AndRat: 624 case op::AndNLM: 625 case op::Concat: 626 case op::Fusion: 627 case op::Star: 628 case op::FStar: 629 case op::first_match: 630 // !(a*) etc. should never occur. 631 { 632 assert(!negated); 633 result = f.map([c, deep](formula f) 634 { 635 return nenoform_rec(f, false, c, deep); 636 }); 637 break; 638 } 639 case op::EConcat: 640 case op::EConcatMarked: 641 { 642 deep = true; 643 // !(a <>-> b) == a[]-> !b 644 auto f1 = f[0]; 645 auto f2 = f[1]; 646 result = formula::binop(negated ? op::UConcat : o, 647 rec(f1, false), rec(f2, negated)); 648 break; 649 } 650 case op::UConcat: 651 { 652 deep = true; 653 // !(a []-> b) == a<>-> !b 654 auto f1 = f[0]; 655 auto f2 = f[1]; 656 result = formula::binop(negated ? op::EConcat : op::UConcat, 657 rec(f1, false), rec(f2, negated)); 658 break; 659 } 660 case op::eword: 661 case op::Not: 662 SPOT_UNREACHABLE(); 663 } 664 } 665 666 c->cache_nenoform(key, result); 667 return result; 668 } 669 670 ////////////////////////////////////////////////////////////////////// 671 // 672 // SIMPLIFY_VISITOR 673 // 674 ////////////////////////////////////////////////////////////////////// 675 676 // Forward declaration. 677 formula 678 simplify_recursively(formula f, tl_simplifier_cache* c); 679 680 // X(a) R b or X(a) M b 681 // This returns a. 682 formula is_XRM(formula f)683 is_XRM(formula f) 684 { 685 if (!f.is(op::R, op::M)) 686 return nullptr; 687 auto left = f[0]; 688 if (!left.is(op::X)) 689 return nullptr; 690 return left[0]; 691 } 692 693 // X(a) W b or X(a) U b 694 // This returns a. 695 formula is_XWU(formula f)696 is_XWU(formula f) 697 { 698 if (!f.is(op::W, op::U)) 699 return nullptr; 700 auto left = f[0]; 701 if (!left.is(op::X)) 702 return nullptr; 703 return left[0]; 704 } 705 706 // b & X(b W a) or b & X(b U a) 707 // This returns (b W a) or (b U a). 708 formula is_bXbWU(formula f)709 is_bXbWU(formula f) 710 { 711 if (!f.is(op::And)) 712 return nullptr; 713 unsigned s = f.size(); 714 for (unsigned pos = 0; pos < s; ++pos) 715 { 716 auto p = f[pos]; 717 if (!(p.is(op::X))) 718 continue; 719 auto c = p[0]; 720 if (!c.is(op::U, op::W)) 721 continue; 722 formula b = f.all_but(pos); 723 if (b == c[0]) 724 return c; 725 } 726 return nullptr; 727 } 728 729 // b | X(b R a) or b | X(b M a) 730 // This returns (b R a) or (b M a). 731 formula is_bXbRM(formula f)732 is_bXbRM(formula f) 733 { 734 if (!f.is(op::Or)) 735 return nullptr; 736 unsigned s = f.size(); 737 for (unsigned pos = 0; pos < s; ++pos) 738 { 739 auto p = f[pos]; 740 if (!(p.is(op::X))) 741 continue; 742 auto c = p[0]; 743 if (!c.is(op::R, op::M)) 744 continue; 745 formula b = f.all_but(pos); 746 if (b == c[0]) 747 return c; 748 } 749 return nullptr; 750 } 751 752 formula unop_multop(op uop,op mop,vec v)753 unop_multop(op uop, op mop, vec v) 754 { 755 formula f = formula::unop(uop, formula::multop(mop, v)); 756 if (f.is(op::X) && f[0].is_ff()) 757 return formula::ff(); 758 return f; 759 } 760 761 formula unop_unop_multop(op uop1,op uop2,op mop,vec v)762 unop_unop_multop(op uop1, op uop2, op mop, vec v) 763 { 764 return formula::unop(uop1, unop_multop(uop2, mop, v)); 765 } 766 767 formula unop_unop(op uop1,op uop2,formula f)768 unop_unop(op uop1, op uop2, formula f) 769 { 770 return formula::unop(uop1, formula::unop(uop2, f)); 771 } 772 773 struct mospliter 774 { 775 enum what { Split_GF = (1 << 0), 776 Strip_GF = (1 << 1) | (1 << 0), 777 Split_FG = (1 << 2), 778 Strip_FG = (1 << 3) | (1 << 2), 779 Split_F = (1 << 4), 780 Strip_F = (1 << 5) | (1 << 4), 781 Split_G = (1 << 6), 782 Strip_G = (1 << 7) | (1 << 6), 783 Strip_X = (1 << 8), 784 Split_U_or_W = (1 << 9), 785 Split_R_or_M = (1 << 10), 786 Split_EventUniv = (1 << 11), 787 Split_Event = (1 << 12), 788 Split_Univ = (1 << 13), 789 Split_Bool = (1 << 14) 790 }; 791 792 private: mospliterspot::__anonc0ca6ab60111::mospliter793 mospliter(unsigned split, tl_simplifier_cache* cache) 794 : split_(split), c_(cache), 795 res_GF{(split_ & Split_GF) ? new vec : nullptr}, 796 res_FG{(split_ & Split_FG) ? new vec : nullptr}, 797 res_F{(split_ & Split_F) ? new vec : nullptr}, 798 res_G{(split_ & Split_G) ? new vec : nullptr}, 799 res_X{(split_ & Strip_X) ? new vec : nullptr}, 800 res_U_or_W{(split_ & Split_U_or_W) ? new vec : nullptr}, 801 res_R_or_M{(split_ & Split_R_or_M) ? new vec : nullptr}, 802 res_Event{(split_ & Split_Event) ? new vec : nullptr}, 803 res_Univ{(split_ & Split_Univ) ? new vec : nullptr}, 804 res_EventUniv{(split_ & Split_EventUniv) ? new vec : nullptr}, 805 res_Bool{(split_ & Split_Bool) ? new vec : nullptr}, 806 res_other{new vec} 807 { 808 } 809 810 public: mospliterspot::__anonc0ca6ab60111::mospliter811 mospliter(unsigned split, vec v, tl_simplifier_cache* cache) 812 : mospliter(split, cache) 813 { 814 for (auto f: v) 815 { 816 if (f) // skip null pointers left by previous simplifications 817 process(f); 818 } 819 } 820 mospliterspot::__anonc0ca6ab60111::mospliter821 mospliter(unsigned split, formula mo, 822 tl_simplifier_cache* cache) 823 : mospliter(split, cache) 824 { 825 unsigned mos = mo.size(); 826 for (unsigned i = 0; i < mos; ++i) 827 { 828 formula f = simplify_recursively(mo[i], cache); 829 process(f); 830 } 831 } 832 processspot::__anonc0ca6ab60111::mospliter833 void process(formula f) 834 { 835 bool e = f.is_eventual(); 836 bool u = f.is_universal(); 837 bool eu = res_EventUniv && e & u && c_->options.event_univ; 838 switch (f.kind()) 839 { 840 case op::X: 841 case op::strong_X: 842 if (res_X && !eu) 843 { 844 res_X->emplace_back(f[0]); 845 return; 846 } 847 break; 848 case op::F: 849 { 850 formula c = f[0]; 851 if (res_FG && u && c.is(op::G)) 852 { 853 res_FG->emplace_back(((split_ & Strip_FG) == Strip_FG 854 ? c[0] : f)); 855 return; 856 } 857 if (res_F && !eu) 858 { 859 res_F->emplace_back(((split_ & Strip_F) == Strip_F 860 ? c : f)); 861 return; 862 } 863 break; 864 } 865 case op::G: 866 { 867 formula c = f[0]; 868 if (res_GF && e && c.is(op::F)) 869 { 870 res_GF->emplace_back(((split_ & Strip_GF) == Strip_GF 871 ? c[0] : f)); 872 return; 873 } 874 if (res_G && !eu) 875 { 876 res_G->emplace_back(((split_ & Strip_G) == Strip_G 877 ? c : f)); 878 return; 879 } 880 break; 881 } 882 case op::U: 883 case op::W: 884 if (res_U_or_W) 885 { 886 res_U_or_W->emplace_back(f); 887 return; 888 } 889 break; 890 case op::R: 891 case op::M: 892 if (res_R_or_M) 893 { 894 res_R_or_M->emplace_back(f); 895 return; 896 } 897 break; 898 default: 899 if (res_Bool && f.is_boolean()) 900 { 901 res_Bool->emplace_back(f); 902 return; 903 } 904 break; 905 } 906 if (c_->options.event_univ) 907 { 908 if (res_EventUniv && e && u) 909 { 910 res_EventUniv->emplace_back(f); 911 return; 912 } 913 if (res_Event && e) 914 { 915 res_Event->emplace_back(f); 916 return; 917 } 918 if (res_Univ && u) 919 { 920 res_Univ->emplace_back(f); 921 return; 922 } 923 } 924 res_other->emplace_back(f); 925 } 926 927 unsigned split_; 928 tl_simplifier_cache* c_; 929 std::unique_ptr<vec> res_GF; 930 std::unique_ptr<vec> res_FG; 931 std::unique_ptr<vec> res_F; 932 std::unique_ptr<vec> res_G; 933 std::unique_ptr<vec> res_X; 934 std::unique_ptr<vec> res_U_or_W; 935 std::unique_ptr<vec> res_R_or_M; 936 std::unique_ptr<vec> res_Event; 937 std::unique_ptr<vec> res_Univ; 938 std::unique_ptr<vec> res_EventUniv; 939 std::unique_ptr<vec> res_Bool; 940 std::unique_ptr<vec> res_other; 941 }; 942 943 class simplify_visitor final 944 { 945 public: 946 simplify_visitor(tl_simplifier_cache * cache)947 simplify_visitor(tl_simplifier_cache* cache) 948 : c_(cache), opt_(cache->options) 949 { 950 } 951 952 // if !neg build c&X(c&X(...&X(tail))) with n occurences of c 953 // if neg build !c|X(!c|X(...|X(tail))). 954 formula dup_b_x_tail(bool neg,formula c,formula tail,unsigned n)955 dup_b_x_tail(bool neg, formula c, formula tail, unsigned n) 956 { 957 op mop; 958 if (neg) 959 { 960 c = formula::Not(c); 961 mop = op::Or; 962 } 963 else 964 { 965 mop = op::And; 966 } 967 while (n--) 968 tail = // b&X(tail) or !b|X(tail) 969 formula::multop(mop, {c, formula::X(tail)}); 970 return tail; 971 } 972 973 formula visit(formula f)974 visit(formula f) 975 { 976 formula result = f; 977 978 auto recurse = [this](formula f) 979 { 980 return simplify_recursively(f, c_); 981 }; 982 983 f = f.map(recurse); 984 985 switch (op o = f.kind()) 986 { 987 case op::ff: 988 case op::tt: 989 case op::eword: 990 case op::ap: 991 case op::Not: 992 case op::FStar: 993 return f; 994 case op::X: 995 case op::strong_X: 996 { 997 formula c = f[0]; 998 // The following rules are not trivial simplifications, 999 // because they are not true in LTLf. 1000 // X(0)=0 1001 // X[!](1)=1 1002 if (c.is_constant()) 1003 return c; 1004 // Xf = f if f is both eventual and universal. 1005 if (c.is_universal() && c.is_eventual()) 1006 { 1007 if (opt_.event_univ) 1008 return c; 1009 // If EventUniv simplification is disabled, use 1010 // only the following basic rewriting rules: 1011 // XGF(f) = GF(f) and XFG(f) = FG(f) 1012 // The former comes from Somenzi&Bloem (CAV'00). 1013 // It's not clear why they do not list the second. 1014 if (opt_.reduce_basics && 1015 (c.is({op::G, op::F}) || c.is({op::F, op::G}))) 1016 return c; 1017 } 1018 1019 // If Xa = a, keep only a. 1020 if (opt_.containment_checks_stronger 1021 && c_->lcc.equal(f, c)) 1022 return c; 1023 1024 // X(f1 & GF(f2)) = X(f1) & GF(f2) 1025 // X(f1 | GF(f2)) = X(f1) | GF(f2) 1026 // X(f1 & FG(f2)) = X(f1) & FG(f2) 1027 // X(f1 | FG(f2)) = X(f1) | FG(f2) 1028 // 1029 // The above usually make more sense when reversed (see 1030 // them in the And and Or rewritings), except when we 1031 // try to maximaze the size of subformula that do not 1032 // have EventUniv formulae. 1033 if (opt_.favor_event_univ) 1034 if (c.is(op::Or, op::And)) 1035 { 1036 mospliter s(mospliter::Split_EventUniv, c, c_); 1037 op oc = c.kind(); 1038 s.res_EventUniv-> 1039 emplace_back(unop_multop(op::X, oc, 1040 std::move(*s.res_other))); 1041 formula result = 1042 formula::multop(oc, 1043 std::move(*s.res_EventUniv)); 1044 if (result != f) 1045 result = recurse(result); 1046 return result; 1047 } 1048 return f; 1049 } 1050 case op::F: 1051 { 1052 formula c = f[0]; 1053 // If f is a pure eventuality formula then F(f)=f. 1054 if (opt_.event_univ && c.is_eventual()) 1055 return c; 1056 1057 auto g_in_f = [this](formula g, std::vector<formula>* to, 1058 std::vector<formula>* eventual = nullptr) 1059 { 1060 if (g[0].is(op::Or)) 1061 { 1062 mospliter s2(mospliter::Split_Univ | 1063 (eventual ? mospliter::Split_Event : 0), 1064 g[0], c_); 1065 for (formula e: *s2.res_Univ) 1066 to->push_back(e.is(op::X) ? e[0] : e); 1067 to->push_back 1068 (unop_multop(op::G, op::Or, 1069 std::move(*s2.res_other))); 1070 if (eventual) 1071 std::swap(*s2.res_Event, *eventual); 1072 } 1073 else 1074 { 1075 to->push_back(g); 1076 } 1077 }; 1078 1079 if (opt_.reduce_basics) 1080 { 1081 // F(a U b) = F(b) 1082 if (c.is(op::U)) 1083 return recurse(formula::F(c[1])); 1084 1085 // F(a M b) = F(a & b) 1086 if (c.is(op::M)) 1087 return recurse(unop_multop(op::F, op::And, 1088 {c[0], c[1]})); 1089 1090 // FX(a) = XF(a) 1091 // FXX(a) = XXF(a) ... 1092 // FXG(a) = XFG(a) = FG(a) ... 1093 if (c.is(op::X)) 1094 return recurse(unop_unop(op::X, op::F, c[0])); 1095 1096 // F(G(a | Gb)) = F(Ga | Gb) 1097 // F(G(a | Fb)) = FGa | GFb // opt_.favor_event_univ 1098 if (c.is({op::G, op::Or})) 1099 { 1100 std::vector<formula> toadd, eventual; 1101 g_in_f(c, &toadd, 1102 opt_.favor_event_univ ? &eventual : nullptr); 1103 formula res = unop_multop(op::F, op::Or, 1104 std::move(toadd)); 1105 if (!eventual.empty()) 1106 { 1107 formula ev = unop_multop(op::G, op::Or, 1108 std::move(eventual)); 1109 res = formula::Or({res, ev}); 1110 } 1111 if (res != f) 1112 return recurse(res); 1113 } 1114 1115 // F(G(a & Fb) = FGa & GFb // !opt_.reduce_size_strictly 1116 if (c.is({op::G, op::And}) && !opt_.reduce_size_strictly) 1117 { 1118 mospliter s2(mospliter::Split_Event, c[0], c_); 1119 for (formula& e: *s2.res_Event) 1120 while (e.is(op::X)) 1121 e = e[0]; 1122 formula fg = unop_unop_multop(op::F, op::G, op::And, 1123 std::move(*s2.res_other)); 1124 formula gf = unop_multop(op::G, op::And, 1125 std::move(*s2.res_Event)); 1126 formula res = formula::And({fg, gf}); 1127 if (res != f) 1128 return recurse(res); 1129 } 1130 1131 // FG(a) = FG(dnf(a)) if a is not Boolean 1132 // and contains some | above non-Boolean subformulas. 1133 if (c.is(op::G) && !c[0].is_boolean()) 1134 { 1135 formula m = c[0]; 1136 bool want_cnf = m.is(op::And); 1137 if (!want_cnf && m.is(op::Or)) 1138 for (auto cc : m) 1139 if (cc.is(op::And)) 1140 { 1141 want_cnf = true; 1142 break; 1143 } 1144 if (want_cnf && !opt_.reduce_size_strictly) 1145 m = c_->as_cnf(m); 1146 // FG(a & Xb) = FG(a & b) 1147 // FG(a & Gb) = FG(a & b) 1148 if (m.is(op::And)) 1149 m = m.map([](formula f) 1150 { 1151 if (f.is(op::X, op::G)) 1152 return f[0]; 1153 return f; 1154 }); 1155 if (c[0] != m) 1156 return recurse(unop_unop(op::F, op::G, m)); 1157 } 1158 } 1159 // if Fa => a, keep a. 1160 if (opt_.containment_checks_stronger 1161 && c_->lcc.contained(f, c)) 1162 return c; 1163 1164 // Disabled by default: 1165 // F(f1 & GF(f2)) = F(f1) & GF(f2) 1166 // 1167 // As is, these two formulae are translated into 1168 // equivalent Büchi automata so the rewriting is 1169 // useless. 1170 // 1171 // However when taken in a larger formula such 1172 // as F(f1 & GF(f2)) | F(a & GF(b)), this 1173 // rewriting used to produce (F(f1) & GF(f2)) | 1174 // (F(a) & GF(b)), missing the opportunity to 1175 // apply the F(E1)|F(E2) = F(E1|E2) rule which 1176 // really helps the translation. F((f1 & GF(f2)) 1177 // | (a & GF(b))) is indeed easier to translate. 1178 // 1179 // So we do not consider this rewriting rule by 1180 // default. However if favor_event_univ is set, 1181 // we want to move the GF out of the F. 1182 // 1183 // Also if this appears inside a G, we want to 1184 // reduce it: 1185 // GF(f1 & GF(f2)) = G(F(f1) & GF(f2)) 1186 // = G(F(f1) & F(f2)) 1187 // But this is handled by the G case. 1188 if (opt_.favor_event_univ) 1189 // F(f1&f2&FG(f3)&FG(f4)&f5&f6) = 1190 // F(f1&f2) & FG(f3&f4) & f5 & f6 1191 // if f5 and f6 are both eventual and universal. 1192 if (c.is(op::And)) 1193 { 1194 mospliter s(mospliter::Strip_FG | 1195 mospliter::Split_EventUniv, 1196 c, c_); 1197 s.res_EventUniv-> 1198 emplace_back(unop_multop(op::F, op::And, 1199 std::move(*s.res_other))); 1200 s.res_EventUniv-> 1201 emplace_back(unop_unop_multop(op::F, op::G, op::And, 1202 std::move(*s.res_FG))); 1203 formula res = 1204 formula::And(std::move(*s.res_EventUniv)); 1205 if (res != f) 1206 return recurse(res); 1207 } 1208 // If u3 and u4 are universal formulae and h is not: 1209 // F(f1 | f2 | Fu3 | u4 | FGg | Fh | Xu5 | G(f6 | Xu7 | u8)) 1210 // = F(f1 | f2 | u3 | u4 | Gg | h | u5 | Gf6 | u7 | u8) 1211 // or 1212 // F(f1 | f2 | Fu3 | u4 | FGg | Fh | Xu5) 1213 // = F(f1 | f2 | h) | F(u3 | u4 | Gg | u5 | Gf6 | u7 | u8) 1214 // depending on whether favor_event_univ is set. 1215 if (c.is(op::Or)) 1216 { 1217 int w = mospliter::Strip_F 1218 | mospliter::Strip_X | mospliter::Split_G; 1219 if (opt_.favor_event_univ) 1220 w |= mospliter::Split_Univ; 1221 mospliter s(w, c, c_); 1222 s.res_other->insert(s.res_other->end(), 1223 s.res_F->begin(), s.res_F->end()); 1224 for (formula f: *s.res_X) 1225 if (f.is_universal()) 1226 s.res_other->push_back(f); 1227 else 1228 s.res_other->push_back(formula::X(f)); 1229 std::vector<formula>* to = opt_.favor_event_univ ? 1230 s.res_Univ.get() : s.res_other.get(); 1231 for (formula g: *s.res_G) 1232 g_in_f(g, to); 1233 formula res = unop_multop(op::F, op::Or, 1234 std::move(*s.res_other)); 1235 if (s.res_Univ) 1236 { 1237 std::vector<formula> toadd; 1238 for (auto& g: *s.res_Univ) 1239 // Strip any F or X 1240 if (g.is(op::F, op::X)) 1241 g = g[0]; 1242 s.res_Univ->insert(s.res_Univ->end(), 1243 toadd.begin(), toadd.end()); 1244 formula fu = unop_multop(op::F, op::Or, 1245 std::move(*s.res_Univ)); 1246 res = formula::Or({res, fu}); 1247 } 1248 if (res != f) 1249 return recurse(res); 1250 } 1251 } 1252 return f; 1253 case op::G: 1254 { 1255 formula c = f[0]; 1256 // If f is a pure universality formula then G(f)=f. 1257 if (opt_.event_univ && c.is_universal()) 1258 return c; 1259 1260 auto f_in_g = [this](formula f, std::vector<formula>* to, 1261 std::vector<formula>* univ = nullptr) 1262 { 1263 if (f[0].is(op::And)) 1264 { 1265 mospliter s2(mospliter::Split_Event | 1266 (univ ? mospliter::Split_Univ : 0), 1267 f[0], c_); 1268 for (formula e: *s2.res_Event) 1269 to->push_back(e.is(op::X) ? e[0] : e); 1270 to->push_back 1271 (unop_multop(op::F, op::And, 1272 std::move(*s2.res_other))); 1273 if (univ) 1274 std::swap(*s2.res_Univ, *univ); 1275 } 1276 else 1277 { 1278 to->push_back(f); 1279 } 1280 }; 1281 1282 if (opt_.reduce_basics) 1283 { 1284 // G(a R b) = G(b) 1285 if (c.is(op::R)) 1286 return recurse(formula::G(c[1])); 1287 1288 // G(a W b) = G(a | b) 1289 if (c.is(op::W)) 1290 return recurse(unop_multop(op::G, op::Or, 1291 {c[0], c[1]})); 1292 1293 // GX(a) = XG(a) 1294 // GXX(a) = XXG(a) ... 1295 // GXF(a) = XGF(a) = GF(a) ... 1296 if (c.is(op::X)) 1297 return recurse(unop_unop(op::X, op::G, c[0])); 1298 1299 // G(F(a & Fb)) = G(Fa & Fb) 1300 // G(F(a & Gb)) = GFa & FGb // !opt_.reduce_size_strictly 1301 if (c.is({op::F, op::And})) 1302 { 1303 std::vector<formula> toadd, univ; 1304 f_in_g(c, &toadd, 1305 opt_.reduce_size_strictly ? nullptr : &univ); 1306 formula res = unop_multop(op::G, op::And, 1307 std::move(toadd)); 1308 if (!univ.empty()) 1309 { 1310 formula un = unop_multop(op::F, op::And, 1311 std::move(univ)); 1312 res = formula::And({res, un}); 1313 } 1314 if (res != f) 1315 return recurse(res); 1316 } 1317 1318 // G(F(a | Gb)) = GFa | FGb // opt_.favor_event_univ 1319 if (c.is({op::F, op::Or}) && opt_.favor_event_univ) 1320 { 1321 mospliter s2(mospliter::Split_Univ, c[0], c_); 1322 for (formula& u: *s2.res_Univ) 1323 while (u.is(op::X)) 1324 u = u[0]; 1325 formula gf = unop_unop_multop(op::G, op::F, op::Or, 1326 std::move(*s2.res_other)); 1327 formula fg = unop_multop(op::F, op::Or, 1328 std::move(*s2.res_Univ)); 1329 formula res = formula::Or({gf, fg}); 1330 if (res != f) 1331 return recurse(res); 1332 } 1333 1334 // G(f1|f2|GF(f3)|GF(f4)|f5|f6) = 1335 // G(f1|f2) | GF(f3|f4) | f5 | f6 1336 // if f5 and f6 are both eventual and universal. 1337 if (c.is(op::Or)) 1338 { 1339 mospliter s(mospliter::Strip_GF | 1340 mospliter::Split_EventUniv, 1341 c, c_); 1342 s.res_EventUniv-> 1343 emplace_back(unop_multop(op::G, op::Or, 1344 std::move(*s.res_other))); 1345 s.res_EventUniv-> 1346 emplace_back(unop_unop_multop(op::G, op::F, op::Or, 1347 std::move(*s.res_GF))); 1348 formula res = 1349 formula::Or(std::move(*s.res_EventUniv)); 1350 1351 if (res != f) 1352 return recurse(res); 1353 } 1354 // If e3 and e4 are eventual formulae and h is not: 1355 // G(f1 & f2 & Ge3 & e4 & GFg & Gh & Xe5 & F(f6 & Xe7 & e8)) 1356 // = G(f1 & f2 & e3 & e4 & Fg & h & e5 & Ff6 & e7 & e8) 1357 // or 1358 // G(f1 & f2 & Ge3 & e4 & GFg & Gh & Xe5 & F(f6 & Xe7 & e8)) 1359 // = G(f1 & f2 & h) & G(e3 & e4 & Fg & e5 & Ff6 & e7 & e8) 1360 // depending on whether favor_event_univ is set. 1361 else if (c.is(op::And)) 1362 { 1363 int w = mospliter::Strip_G | 1364 mospliter::Strip_X | mospliter::Split_F; 1365 if (opt_.favor_event_univ) 1366 w |= mospliter::Split_Event; 1367 mospliter s(w, c, c_); 1368 s.res_other->insert(s.res_other->end(), 1369 s.res_G->begin(), s.res_G->end()); 1370 for (formula f: *s.res_X) 1371 if (f.is_eventual()) 1372 s.res_other->push_back(f); 1373 else 1374 s.res_other->push_back(formula::X(f)); 1375 std::vector<formula>* to = opt_.favor_event_univ ? 1376 s.res_Event.get() : s.res_other.get(); 1377 for (formula f: *s.res_F) 1378 f_in_g(f, to); 1379 1380 formula res = unop_multop(op::G, op::And, 1381 std::move(*s.res_other)); 1382 if (s.res_Event) 1383 { 1384 std::vector<formula> toadd; 1385 // Strip any G or X 1386 for (auto& g: *s.res_Event) 1387 if (g.is(op::G, op::X)) 1388 { 1389 g = g[0]; 1390 } 1391 s.res_Event->insert(s.res_Event->end(), 1392 toadd.begin(), toadd.end()); 1393 formula ge = 1394 unop_multop(op::G, op::And, 1395 std::move(*s.res_Event)); 1396 res = formula::And({res, ge}); 1397 } 1398 if (res != f) 1399 return recurse(res); 1400 } 1401 1402 1403 // GF(a) = GF(dnf(a)) if a is not Boolean 1404 // and contains some | above non-Boolean subformulas. 1405 if (c.is(op::F) && !c[0].is_boolean()) 1406 { 1407 formula m = c[0]; 1408 bool want_dnf = m.is(op::Or); 1409 if (!want_dnf && m.is(op::And)) 1410 for (auto cc : m) 1411 if (cc.is(op::Or)) 1412 { 1413 want_dnf = true; 1414 break; 1415 } 1416 if (want_dnf && !opt_.reduce_size_strictly) 1417 m = c_->as_dnf(m); 1418 // GF(a | Xb) = GF(a | b) 1419 // GF(a | Fb) = GF(a | b) 1420 if (m.is(op::Or)) 1421 m = m.map([](formula f) 1422 { 1423 if (f.is(op::X, op::F)) 1424 return f[0]; 1425 return f; 1426 }); 1427 if (c[0] != m) 1428 return recurse(unop_unop(op::G, op::F, m)); 1429 } 1430 // GF(f1 & f2 & eu1 & eu2) = G(F(f1 & f2) & eu1 & eu2 1431 if (opt_.event_univ && c.is({op::F, op::And})) 1432 { 1433 mospliter s(mospliter::Split_EventUniv, 1434 c[0], c_); 1435 s.res_EventUniv-> 1436 emplace_back(unop_multop(op::F, op::And, 1437 std::move(*s.res_other))); 1438 formula res = 1439 formula::G(formula::And(std::move(*s.res_EventUniv))); 1440 if (res != f) 1441 return recurse(res); 1442 } 1443 } 1444 // if a => Ga, keep a. 1445 if (opt_.containment_checks_stronger 1446 && c_->lcc.contained(c, f)) 1447 return c; 1448 } 1449 return f; 1450 case op::Closure: 1451 case op::NegClosure: 1452 case op::NegClosureMarked: 1453 { 1454 formula c = f[0]; 1455 // {e[*]} = {e} 1456 // !{e[*]} = !{e} 1457 if (c.accepts_eword() && c.is(op::Star)) 1458 return recurse(formula::unop(o, c[0])); 1459 1460 if (!opt_.reduce_size_strictly) 1461 if (c.is(op::OrRat)) 1462 { 1463 // {a₁|a₂} = {a₁}| {a₂} 1464 // !{a₁|a₂} = !{a₁}&!{a₂} 1465 unsigned s = c.size(); 1466 vec v; 1467 for (unsigned n = 0; n < s; ++n) 1468 v.emplace_back(formula::unop(o, c[n])); 1469 return recurse(formula::multop(o == op::Closure 1470 ? op::Or : op::And, v)); 1471 } 1472 if (c.is(op::Concat)) 1473 { 1474 if (c.accepts_eword()) 1475 { 1476 if (opt_.reduce_size_strictly) 1477 return f; 1478 // If all terms accept the empty word, we have 1479 // {e₁;e₂;e₃} = {e₁}|{e₂}|{e₃} 1480 // !{e₁;e₂;e₃} = !{e₁}&!{e₂}&!{e₃} 1481 vec v; 1482 unsigned end = c.size(); 1483 v.reserve(end); 1484 for (unsigned i = 0; i < end; ++i) 1485 v.emplace_back(formula::unop(o, c[i])); 1486 return recurse(formula::multop(o == op::Closure ? 1487 op::Or : op::And, v)); 1488 } 1489 1490 // Some term does not accept the empty word. 1491 unsigned end = c.size() - 1; 1492 1493 // {r;1} = 1 if r accepts [*0], else {r} 1494 // !{r;1} = 0 if r accepts [*0], else !{r} 1495 if (c[end].is_tt()) 1496 { 1497 formula rest = c.all_but(end); 1498 if (rest.accepts_eword()) 1499 return o == op::Closure ? formula::tt() : formula::ff(); 1500 return recurse(formula::unop(o, rest)); 1501 } 1502 1503 // {b₁;b₂;e₁;f₁;e₂;f₂;e₂;e₃;e₄} 1504 // = b₁&X(b₂&X({e₁;f₁;e₂;f₂})) 1505 // !{b₁;b₂;e₁;f₁;e₂;f₂;e₂;e₃;e₄} 1506 // = !b₁|X(!b₂|X(!{e₁;f₁;e₂;f₂})) 1507 // if e denotes a term that accepts [*0] 1508 // and b denotes a Boolean formula. 1509 // 1510 // if reduce_size_strictly is set, we simply remove 1511 // the trailing e2;e3;e4. 1512 while (c[end].accepts_eword()) 1513 --end; 1514 unsigned start = 0; 1515 while (start <= end) 1516 { 1517 formula r = c[start]; 1518 if (r.is_boolean() && !opt_.reduce_size_strictly) 1519 ++start; 1520 else 1521 break; 1522 } 1523 unsigned s = end + 1 - start; 1524 if (s != c.size()) 1525 { 1526 bool doneg = o != op::Closure; 1527 formula tail; 1528 if (s > 0) 1529 { 1530 vec v; 1531 v.reserve(s); 1532 for (unsigned n = start; n <= end; ++n) 1533 v.emplace_back(c[n]); 1534 tail = formula::Concat(v); 1535 tail = formula::unop(o, tail); 1536 } 1537 else 1538 { 1539 tail = doneg ? formula::ff() : formula::tt(); 1540 } 1541 1542 for (unsigned n = start; n > 0;) 1543 { 1544 --n; 1545 formula e = c[n]; 1546 // {b;f} = b & X{f} 1547 // !{b;f} = !b | X!{f} 1548 if (e.is_boolean()) 1549 { 1550 tail = formula::X(tail); 1551 if (doneg) 1552 tail = formula::Or({formula::Not(e), tail}); 1553 else 1554 tail = formula::And({e, tail}); 1555 } 1556 } 1557 return recurse(tail); 1558 } 1559 1560 // {b[*i..j];c} = b&X(b&X(... b&X{b[*0..j-i];c})) 1561 // !{b[*i..j];c} = !b&X(!b&X(... !b&X!{b[*0..j-i];c})) 1562 if (!opt_.reduce_size_strictly) 1563 if (c[0].is(op::Star)) 1564 { 1565 formula s = c[0]; 1566 formula sc = s[0]; 1567 unsigned min = s.min(); 1568 if (sc.is_boolean() && min > 0) 1569 { 1570 unsigned max = s.max(); 1571 if (max != formula::unbounded()) 1572 max -= min; 1573 unsigned ss = c.size(); 1574 vec v; 1575 v.reserve(ss); 1576 v.emplace_back(formula::Star(sc, 0, max)); 1577 for (unsigned n = 1; n < ss; ++n) 1578 v.emplace_back(c[n]); 1579 formula tail = formula::Concat(v); 1580 tail = // {b[*0..j-i]} or !{b[*0..j-i]} 1581 formula::unop(o, tail); 1582 tail = 1583 dup_b_x_tail(o != op::Closure, 1584 sc, tail, min); 1585 return recurse(tail); 1586 } 1587 } 1588 } 1589 // {b[*i..j]} = b&X(b&X(... b)) with i occurences of b 1590 // !{b[*i..j]} = !b&X(!b&X(... !b)) 1591 if (!opt_.reduce_size_strictly) 1592 if (c.is(op::Star)) 1593 { 1594 formula cs = c[0]; 1595 if (cs.is_boolean()) 1596 { 1597 unsigned min = c.min(); 1598 assert(min > 0); 1599 formula tail; 1600 if (o == op::Closure) 1601 tail = dup_b_x_tail(false, cs, 1602 formula::tt(), min); 1603 else 1604 tail = dup_b_x_tail(true, cs, 1605 formula::ff(), min); 1606 return recurse(tail); 1607 } 1608 } 1609 return f; 1610 } 1611 case op::Xor: 1612 case op::Implies: 1613 case op::Equiv: 1614 case op::U: 1615 case op::R: 1616 case op::W: 1617 case op::M: 1618 case op::EConcat: 1619 case op::EConcatMarked: 1620 case op::UConcat: 1621 return visit_binop(f); 1622 case op::Or: 1623 case op::OrRat: 1624 case op::And: 1625 case op::AndRat: 1626 case op::AndNLM: 1627 case op::Concat: 1628 return visit_multop(f); 1629 case op::Fusion: 1630 return f; 1631 case op::Star: 1632 { 1633 if (!f.accepts_eword()) 1634 return f; 1635 formula h = f[0]; 1636 if (f.max() == 1 && h.accepts_eword()) 1637 return h; 1638 auto min = 0; 1639 if (f.max() == formula::unbounded()) 1640 { 1641 h = c_->star_normal_form(h); 1642 } 1643 else 1644 { 1645 h = c_->star_normal_form_bounded(h); 1646 if (h.accepts_eword()) 1647 min = 1; 1648 } 1649 return formula::Star(h, min, f.max()); 1650 } 1651 case op::first_match: 1652 { 1653 formula h = f[0]; 1654 if (h.is(op::Star)) 1655 { 1656 // first_match(b[*i..j]) = b[*i] 1657 // first_match(f[*i..j]) = first_match(f[*i]) 1658 unsigned m = h.min(); 1659 if (m < h.max()) 1660 { 1661 formula s = formula::Star(h[0], m, m); 1662 s = h[0].is_boolean() ? s : formula::first_match(s); 1663 return recurse(s); 1664 } 1665 } 1666 else if (h.is(op::FStar)) 1667 { 1668 // first_match(f[:*i..j]) = first_match(f[:*i]) 1669 unsigned m = h.min(); 1670 if (m < h.max()) 1671 { 1672 formula s = formula::FStar(h[0], m, m); 1673 return recurse(formula::first_match(s)); 1674 } 1675 } 1676 else if (h.is(op::Concat)) 1677 { 1678 // If b is Boolean and e accepts [*0], we have 1679 // 1. first_match(b;f) ≡ b;first_match(f) 1680 // 2. first_match(f;e) ≡ first_match(f) 1681 // 3. first_match(first_match(f);g) = 1682 // first_match(f);first_match(g) 1683 // 4. first_match(f;g[*i:j]) ≡ first_match(f;g[*i]) 1684 // 5. first_match(f;g[:*i..j]) = first_match(f;g[:*i]) 1685 // 6. first_match(b[*i:j];f) ≡ b[*i];first_match(b[*0:j-i];f) 1686 // Rules 1-3 can be repeated, so we will loop 1687 // to save the recursion and intermediate caching. 1688 1689 // Extract Boolean formulas at the beginning. 1690 int i = 0; 1691 int n = h.size(); 1692 while (i < n 1693 && (h[i].is_boolean() || h[i].is(op::first_match))) 1694 ++i; 1695 vec prefix; 1696 // +1 to append first_match(suffix), +1 to for rule 6. 1697 prefix.reserve(i + 2); 1698 for (int ii = 0; ii < i; ++ii) 1699 prefix.push_back(h[ii]); 1700 // Extract suffix, minus trailing formulas that accept [*0]. 1701 // "i" is the start of the suffix. 1702 do 1703 --n; 1704 while (i <= n && h[n].accepts_eword()); 1705 vec suffix; 1706 suffix.reserve(n + 1 - i); 1707 for (int ii = i; ii <= n; ++ii) 1708 suffix.push_back(h[ii]); 1709 // Rules 4-5 1710 if (!suffix.empty() && suffix.back().is(op::Star, op::FStar)) 1711 { 1712 formula s = suffix.back(); 1713 unsigned smin = s.min(); 1714 suffix.back() = formula::bunop(s.kind(), 1715 s[0], smin, smin); 1716 } 1717 // Rule 6 1718 if (!suffix.empty() && suffix.front().is(op::Star)) 1719 { 1720 formula s = suffix.front(); 1721 unsigned smin = s.min(); 1722 if (smin > 0 && s[0].is_boolean()) 1723 { 1724 prefix.push_back(formula::Star(s[0], smin, smin)); 1725 suffix.front() = 1726 formula::Star(s[0], 0, s.max() - smin); 1727 } 1728 } 1729 prefix.push_back(formula::first_match 1730 (formula::Concat(suffix))); 1731 formula res = formula::Concat(prefix); 1732 if (res != f) 1733 return recurse(res); 1734 } 1735 else if (h.is(op::Fusion)) 1736 { 1737 // 1. first_match(b:f) = b:first_match(f) if f rejects [*0] 1738 // (not implemented, because first_match will build a DFA 1739 // and limiting its choices is good) 1740 // 2. first_match(b[*i..j]:f) = 1741 // b[*i-1];first_match(b[*1..j-i+1]:f) if i>1 1742 if (h[0].is(op::Star)) 1743 { 1744 formula s = h[0]; 1745 unsigned smin = s.min(); 1746 if (smin > 1 && s[0].is_boolean()) 1747 { 1748 --smin; 1749 unsigned smax = s.max(); 1750 if (smax != formula::unbounded()) 1751 smax -= smin; 1752 formula s2 = formula::Star(s[0], 1, smax); 1753 formula in = formula::Fusion({s2, h.all_but(0)}); 1754 in = formula::first_match(in); 1755 formula s3 = formula::Star(s[0], smin, smin); 1756 return recurse(formula::Concat({s3, in})); 1757 } 1758 } 1759 // 3. first_match(first_match(f):g) = 1760 // first_match(f):first_match(1:g) 1761 if (h[0].is(op::first_match)) 1762 { 1763 formula rest = h.all_but(0); 1764 if (rest.accepts_eword()) 1765 rest = formula::Fusion({formula::tt(), rest}); 1766 rest = formula::first_match(rest); 1767 return recurse(formula::Fusion({h[0], rest})); 1768 } 1769 // 4. first_match(f:g[*i..j]) = first_match(f:g[*max(1,i)]) 1770 // 5. first_match(f:g[:*i..j]) = first_match(f:g[:*i]) 1771 unsigned last = h.size() - 1; 1772 formula tail = h[last]; 1773 if (tail.is(op::Star, op::FStar)) 1774 { 1775 unsigned smin = tail.min(); 1776 if (smin < tail.max()) 1777 { 1778 if (smin == 0 && tail.is(op::Star)) 1779 ++smin; 1780 formula s2 = 1781 formula::bunop(tail.kind(), tail[0], smin, smin); 1782 formula in = formula::Fusion({h.all_but(last), s2}); 1783 return recurse(formula::first_match(in)); 1784 } 1785 } 1786 } 1787 return f; 1788 } 1789 } 1790 SPOT_UNREACHABLE(); 1791 } 1792 reduce_sere_ltl(formula orig)1793 formula reduce_sere_ltl(formula orig) 1794 { 1795 op bindop = orig.kind(); 1796 formula a = orig[0]; 1797 formula b = orig[1]; 1798 1799 auto recurse = [this](formula f) 1800 { 1801 return simplify_recursively(f, c_); 1802 }; 1803 1804 // All this function is documented assuming bindop == 1805 // UConcat, but by changing the following variables it can 1806 // perform the rules for EConcat as well. 1807 op op_g; 1808 op op_w; 1809 op op_r; 1810 op op_and; 1811 bool doneg; 1812 if (bindop == op::UConcat) 1813 { 1814 op_g = op::G; 1815 op_w = op::W; 1816 op_r = op::R; 1817 op_and = op::And; 1818 doneg = true; 1819 } 1820 else // EConcat & EConcatMarked 1821 { 1822 op_g = op::F; 1823 op_w = op::M; 1824 op_r = op::U; 1825 op_and = op::Or; 1826 doneg = false; 1827 } 1828 1829 if (!opt_.reduce_basics) 1830 return orig; 1831 if (a.is(op::Star)) 1832 { 1833 // {[*]}[]->b = Gb 1834 if (a == formula::one_star()) 1835 return recurse(formula::unop(op_g, b)); 1836 1837 formula s = a[0]; 1838 unsigned min = a.min(); 1839 unsigned max = a.max(); 1840 // {s[*]}[]->b = b W !s if s is Boolean. 1841 // {s[+]}[]->b = b W !s if s is Boolean. 1842 if (s.is_boolean() && max == formula::unbounded() && min <= 1) 1843 { 1844 formula ns = doneg ? formula::Not(s) : s; 1845 // b W !s 1846 return recurse(formula::binop(op_w, b, ns)); 1847 } 1848 // {s[*0..j]}[]->b = {s[*1..j]}[]->b 1849 // {s[*0..j]}<>->b = {s[*1..j]}<>->b 1850 if (min == 0) 1851 return recurse(formula::binop(bindop, 1852 formula::Star(s, 1, max), b)); 1853 1854 if (opt_.reduce_size_strictly) 1855 return orig; 1856 // {s[*i..j]}[]->b = {s;s;...;s[*1..j-i+1]}[]->b 1857 // = {s}[]->X({s}[]->X(...[]->X({s[*1..j-i+1]}[]->b))) 1858 // if i>0 and s does not accept the empty word 1859 assert(min > 0); 1860 if (s.accepts_eword()) 1861 return orig; 1862 --min; 1863 if (max != formula::unbounded()) 1864 max -= min; // j-i+1 1865 // Don't rewrite s[1..]. 1866 if (min == 0) 1867 return orig; 1868 formula tail = // {s[*1..j-i]}[]->b 1869 formula::binop(bindop, formula::Star(s, 1, max), b); 1870 for (unsigned n = 0; n < min; ++n) 1871 tail = // {s}[]->X(tail) 1872 formula::binop(bindop, s, formula::X(tail)); 1873 return recurse(tail); 1874 } 1875 else if (a.is(op::Concat)) 1876 { 1877 unsigned s = a.size() - 1; 1878 formula last = a[s]; 1879 // {r;[*]}[]->b = {r}[]->Gb 1880 if (last == formula::one_star()) 1881 return recurse(formula::binop(bindop, a.all_but(s), 1882 formula::unop(op_g, b))); 1883 1884 formula first = a[0]; 1885 // {[*];r}[]->b = G({r}[]->b) 1886 if (first == formula::one_star()) 1887 return recurse(formula::unop(op_g, 1888 formula::binop(bindop, 1889 a.all_but(0), b))); 1890 1891 if (opt_.reduce_size_strictly) 1892 return orig; 1893 1894 // {r;s[*]}[]->b = {r}[]->(b & X(b W !s)) 1895 // if s is Boolean and r does not accept [*0]; 1896 if (last.is_Kleene_star()) // l = s[*] 1897 if (last[0].is_boolean()) 1898 { 1899 formula r = a.all_but(s); 1900 if (!r.accepts_eword()) 1901 { 1902 formula ns = // !s 1903 doneg ? formula::Not(last[0]) : last[0]; 1904 formula w = // b W !s 1905 formula::binop(op_w, b, ns); 1906 formula x = // X(b W !s) 1907 formula::X(w); 1908 formula d = // b & X(b W !s) 1909 formula::multop(op_and, {b, x}); 1910 // {r}[]->(b & X(b W !s)) 1911 return recurse(formula::binop(bindop, r, d)); 1912 } 1913 } 1914 // {s[*];r}[]->b = !s R ({r}[]->b) 1915 // if s is Boolean and r does not accept [*0]; 1916 if (first.is_Kleene_star()) 1917 if (first[0].is_boolean()) 1918 { 1919 formula r = a.all_but(0); 1920 if (!r.accepts_eword()) 1921 { 1922 formula ns = // !s 1923 doneg 1924 ? formula::Not(first[0]) 1925 : first[0]; 1926 formula u = // {r}[]->b 1927 formula::binop(bindop, r, b); 1928 // !s R ({r}[]->b) 1929 return recurse(formula::binop(op_r, ns, u)); 1930 } 1931 } 1932 1933 // {r₁;r₂;r₃}[]->b = {r₁}[]->X({r₂}[]->X({r₃}[]->b)) 1934 // if r₁, r₂, r₃ do not accept [*0]. 1935 if (!a.accepts_eword()) 1936 { 1937 unsigned count = 0; 1938 for (unsigned n = 0; n <= s; ++n) 1939 count += !a[n].accepts_eword(); 1940 assert(count > 0); 1941 if (count == 1) 1942 return orig; 1943 // Let e denote a term that accepts [*0] 1944 // and let f denote a term that do not. 1945 // A formula such as {e₁;f₁;e₂;e₃;f₂;e₄}[]->b 1946 // in which count==2 will be grouped 1947 // as follows: r₁ = e₁;f₁;e₂;e₃ 1948 // r₂ = f₂;e₄ 1949 // this way we have 1950 // {e₁;f₁;e₂;e₃;f₂;e₄}[]->b = {r₁;r₂;r₃}[]->b 1951 // where r₁ and r₂ do not accept [*0]. 1952 unsigned pos = s + 1; 1953 1954 // We compute the r formulas from the right 1955 // (i.e., r₂ before r₁.) 1956 vec r; 1957 do 1958 r.insert(r.begin(), a[--pos]); 1959 while (r.front().accepts_eword()); 1960 formula tail = // {r₂}[]->b 1961 formula::binop(bindop, formula::Concat(r), b); 1962 while (--count) 1963 { 1964 vec r; 1965 do 1966 r.insert(r.begin(), a[--pos]); 1967 while (r.front().accepts_eword()); 1968 // If it's the last block, take all leading 1969 // formulae as well. 1970 if (count == 1) 1971 while (pos > 0) 1972 { 1973 r.insert(r.begin(), a[--pos]); 1974 assert(r.front().accepts_eword()); 1975 } 1976 1977 tail = // X({r₂}[]->b) 1978 formula::X(tail); 1979 tail = // {r₁}[]->X({r₂}[]->b) 1980 formula::binop(bindop, formula::Concat(r), tail); 1981 } 1982 return recurse(tail); 1983 } 1984 } 1985 else if (opt_.reduce_size_strictly) 1986 { 1987 return orig; 1988 } 1989 else if (a.is(op::Fusion)) 1990 { 1991 // {r₁:r₂:r₃}[]->b = {r₁}[]->({r₂}[]->({r₃}[]->b)) 1992 unsigned s = a.size(); 1993 formula tail = b; 1994 do 1995 { 1996 --s; 1997 tail = formula::binop(bindop, a[s], tail); 1998 } 1999 while (s != 0); 2000 return recurse(tail); 2001 } 2002 else if (a.is(op::OrRat)) 2003 { 2004 // {r₁|r₂|r₃}[]->b = ({r₁}[]->b)&({r₂}[]->b)&({r₃}[]->b) 2005 unsigned s = a.size(); 2006 vec v; 2007 for (unsigned n = 0; n < s; ++n) 2008 // {r₁}[]->b 2009 v.emplace_back(formula::binop(bindop, a[n], b)); 2010 return recurse(formula::multop(op_and, v)); 2011 } 2012 return orig; 2013 } 2014 2015 formula visit_binop(formula bo)2016 visit_binop(formula bo) 2017 { 2018 auto recurse = [this](formula f) 2019 { 2020 return simplify_recursively(f, c_); 2021 }; 2022 op o = bo.kind(); 2023 formula b = bo[1]; 2024 if (opt_.event_univ) 2025 { 2026 trace << "bo: trying eventuniv rules" << std::endl; 2027 /* If b is a pure eventuality formula then a U b = b. 2028 If b is a pure universality formula a R b = b. */ 2029 if ((b.is_eventual() && bo.is(op::U)) 2030 || (b.is_universal() && bo.is(op::R))) 2031 return b; 2032 } 2033 2034 formula a = bo[0]; 2035 if (opt_.event_univ) 2036 { 2037 /* If a is a pure eventuality formula then a M b = a & b. 2038 If a is a pure universality formula a W b = a | b. */ 2039 if (a.is_eventual() && bo.is(op::M)) 2040 return recurse(formula::And({a, b})); 2041 if (a.is_universal() && bo.is(op::W)) 2042 return recurse(formula::Or({a, b})); 2043 2044 // (q R Xf) = X(q R f) 2045 // (q U Xf) = X(q U f) 2046 if (a.is_eventual() && a.is_universal() 2047 && bo.is(op::R, op::U) && b.is(op::X)) 2048 return recurse(formula::X(formula::binop(o, a, b[0]))); 2049 2050 // e₁ W e₂ = Ge₁ | e₂ 2051 // u₁ M u₂ = Fu₁ & u₂ 2052 // 2053 // The above formulas are actually true if e₁ and u₁ are 2054 // unconstrained, however there are many cases were such a 2055 // more generic reduction rule will actually produce more 2056 // states once the resulting formula is translated. 2057 if (!opt_.reduce_size_strictly) 2058 { 2059 if (bo.is(op::W) && a.is_eventual() && b.is_eventual()) 2060 return recurse(formula::Or({formula::G(a), b})); 2061 if (bo.is(op::M) && a.is_universal() && b.is_universal()) 2062 return recurse(formula::And({formula::F(a), b})); 2063 } 2064 2065 // In the following rewritings we assume that 2066 // - e is a pure eventuality 2067 // - u is purely universal 2068 // - q is purely universal pure eventuality 2069 // (a U (b|e)) = (a U b)|e 2070 // (a W (b|e)) = (a W b)|e 2071 // (a U (b&q)) = (a U b)&q 2072 // ((a&q) M b) = (a M b)&q 2073 // (a R (b&u)) = (a R b)&u 2074 // (a M (b&u)) = (a M b)&u 2075 if (opt_.favor_event_univ) 2076 { 2077 if (bo.is(op::U, op::W)) 2078 if (b.is(op::Or)) 2079 { 2080 mospliter s(mospliter::Split_Event, b, c_); 2081 formula b2 = formula::Or(std::move(*s.res_other)); 2082 if (b2 != b) 2083 { 2084 s.res_Event->emplace_back(formula::binop(o, a, b2)); 2085 return recurse 2086 (formula::Or(std::move(*s.res_Event))); 2087 } 2088 } 2089 if (bo.is(op::U)) 2090 if (b.is(op::And)) 2091 { 2092 mospliter s(mospliter::Split_EventUniv, b, c_); 2093 formula b2 = formula::And(std::move(*s.res_other)); 2094 if (b2 != b) 2095 { 2096 s.res_EventUniv->emplace_back(formula::binop(o, 2097 a, b2)); 2098 return recurse 2099 (formula::And(std::move(*s.res_EventUniv))); 2100 } 2101 } 2102 if (bo.is(op::M)) 2103 if (a.is(op::And)) 2104 { 2105 mospliter s(mospliter::Split_EventUniv, a, c_); 2106 formula a2 = formula::And(std::move(*s.res_other)); 2107 if (a2 != a) 2108 { 2109 s.res_EventUniv->emplace_back(formula::binop(o, 2110 a2, b)); 2111 return recurse 2112 (formula::And(std::move(*s.res_EventUniv))); 2113 } 2114 } 2115 if (bo.is(op::R, op::M)) 2116 if (b.is(op::And)) 2117 { 2118 mospliter s(mospliter::Split_Univ, b, c_); 2119 formula b2 = formula::And(std::move(*s.res_other)); 2120 if (b2 != b) 2121 { 2122 s.res_Univ->emplace_back(formula::binop(o, a, b2)); 2123 return recurse 2124 (formula::And(std::move(*s.res_Univ))); 2125 } 2126 } 2127 } 2128 trace << "bo: no eventuniv rule matched" << std::endl; 2129 } 2130 2131 // Inclusion-based rules 2132 if (opt_.synt_impl | opt_.containment_checks) 2133 { 2134 trace << "bo: trying inclusion-based rules" << std::endl; 2135 switch (o) 2136 { 2137 case op::Equiv: 2138 { 2139 if (c_->implication(a, b)) 2140 return recurse(formula::Implies(b, a)); 2141 if (c_->implication(b, a)) 2142 return recurse(formula::Implies(a, b)); 2143 break; 2144 } 2145 case op::Implies: 2146 { 2147 if (c_->implication(a, b)) 2148 return formula::tt(); 2149 break; 2150 } 2151 case op::Xor: 2152 { 2153 // if (!a)->b then a xor b = b->!a = a->!b 2154 if (c_->implication_neg(a, b, false)) 2155 { 2156 if (b.is(op::Not)) 2157 return recurse(formula::Implies(a, b[0])); 2158 return recurse(formula::Implies(b, formula::Not(a))); 2159 } 2160 // if a->!b then a xor b = (!b)->a = (!a)->b 2161 if (c_->implication_neg(a, b, true)) 2162 { 2163 if (b.is(op::Not)) 2164 return recurse(formula::Implies(b[0], a)); 2165 return recurse(formula::Implies(formula::Not(a), b)); 2166 } 2167 break; 2168 } 2169 case op::U: 2170 // if a => b, then a U b = b 2171 if (c_->implication(a, b)) 2172 { 2173 // but if also b => a, pick the smallest one. 2174 if ((length_boolone(a) < length_boolone(b)) 2175 && c_->implication(b, a)) 2176 return a; 2177 return b; 2178 } 2179 // if (a U b) => b, then a U b = b (for stronger containment) 2180 if (opt_.containment_checks_stronger 2181 && c_->contained(bo, b)) 2182 return b; 2183 // if !a => b, then a U b = Fb 2184 // if a eventual && b => a, then a U b = Fb 2185 if (c_->implication_neg(a, b, false) 2186 || (a.is_eventual() && c_->implication(b, a))) 2187 return recurse(formula::F(b)); 2188 // if a => b, then a U (b U c) = (b U c) 2189 // if a => b, then a U (b W c) = (b W c) 2190 if (b.is(op::U, op::W) && c_->implication(a, b[0])) 2191 return b; 2192 // if b => a, then a U (b U c) = (a U c) 2193 if (b.is(op::U) && c_->implication(b[0], a)) 2194 return recurse(formula::U(a, b[1])); 2195 // if a => c, then a U (b R (c U d)) = (b R (c U d)) 2196 // if a => c, then a U (b R (c W d)) = (b R (c W d)) 2197 // if a => c, then a U (b M (c U d)) = (b M (c U d)) 2198 // if a => c, then a U (b M (c W d)) = (b M (c W d)) 2199 if (b.is(op::R, op::M)) 2200 { 2201 auto c1 = b[1]; 2202 if (c1.is(op::U, op::W) && c_->implication(a, c1[0])) 2203 return b; 2204 } 2205 // if a => b, then (a U c) U b = c U b 2206 // if a => b, then (a W c) U b = c U b 2207 if (a.is(op::U, op::W) && c_->implication(a[0], b)) 2208 return recurse(formula::U(a[1], b)); 2209 // if c => b, then (a U c) U b = (a U c) | b 2210 if (a.is(op::U) && c_->implication(a[1], b)) 2211 return recurse(formula::Or({a, b})); 2212 // if g => h, then (f|g) U h = f U h 2213 if (a.is(op::Or)) 2214 { 2215 unsigned n = a.size(); 2216 for (unsigned child = 0; child < n; ++child) 2217 if (c_->implication(a[child], b)) 2218 return recurse(formula::U(a.all_but(child), b)); 2219 } 2220 // a U (b & e) = F(b & e) if !b => a 2221 if (b.is(op::And)) 2222 for (formula c: b) 2223 if (c.is_eventual()) 2224 { 2225 // We know there is one pure eventuality 2226 // formula but we might have more. So lets 2227 // extract everything else. 2228 vec rest; 2229 rest.reserve(c.size()); 2230 for (formula cc: b) 2231 if (!cc.is_eventual()) 2232 rest.emplace_back(cc); 2233 if (c_->implication_neg(formula::And(rest), a, false)) 2234 return recurse(formula::F(b)); 2235 break; 2236 } 2237 break; 2238 2239 case op::R: 2240 // if b => a, then a R b = b 2241 if (c_->implication(b, a)) 2242 { 2243 // but if also a => b, pick the smallest one. 2244 if ((length_boolone(a) < length_boolone(b)) 2245 && c_->implication(a, b)) 2246 return a; 2247 return b; 2248 } 2249 // if b => !a, then a R b = Gb 2250 // if a universal && a => b, then a R b = Gb 2251 if (c_->implication_neg(b, a, true) 2252 || (a.is_universal() && c_->implication(a, b))) 2253 return recurse(formula::G(b)); 2254 // if b => a, then a R (b R c) = b R c 2255 // if b => a, then a R (b M c) = b M c 2256 if (b.is(op::R, op::M) && c_->implication(b[0], a)) 2257 return b; 2258 // if a => b, then a R (b R c) = a R c 2259 if (b.is(op::R) && c_->implication(a, b[0])) 2260 return recurse(formula::R(a, b[1])); 2261 // if b => a, then (a R c) R b = c R b 2262 // if b => a, then (a M c) R b = c R b 2263 // if c => b, then (a R c) R b = (a & c) R b 2264 // if c => b, then (a M c) R b = (a & c) R b 2265 if (a.is(op::R, op::M)) 2266 { 2267 if (c_->implication(b, a[0])) 2268 return recurse(formula::R(a[1], b)); 2269 if (c_->implication(a[1], b)) 2270 { 2271 formula ac = formula::And({a[0], a[1]}); 2272 return recurse(formula::R(ac, b)); 2273 } 2274 } 2275 // if h => g, then (f&g) R h = f R h 2276 if (a.is(op::And)) 2277 { 2278 unsigned n = a.size(); 2279 for (unsigned child = 0; child < n; ++child) 2280 if (c_->implication(b, a[child])) 2281 return recurse(formula::R(a.all_but(child), b)); 2282 } 2283 // a R (b | u) = G(b | u) if b => !a 2284 if (b.is(op::Or)) 2285 for (formula c: b) 2286 if (c.is_universal()) 2287 { 2288 // We know there is one purely universal 2289 // formula but we might have more. So lets 2290 // extract everything else. 2291 vec rest; 2292 rest.reserve(c.size()); 2293 for (formula cc: b) 2294 if (!cc.is_universal()) 2295 rest.emplace_back(cc); 2296 if (c_->implication_neg(formula::Or(rest), a, true)) 2297 return recurse(formula::G(b)); 2298 break; 2299 } 2300 break; 2301 2302 case op::W: 2303 // if !a => b then a W b = 1 2304 if (c_->implication_neg(a, b, false)) 2305 return formula::tt(); 2306 // if a => b, then a W b = b 2307 if (c_->implication(a, b)) 2308 { 2309 // but if also b => a, pick the smallest one. 2310 if ((length_boolone(a) < length_boolone(b)) 2311 && c_->implication(b, a)) 2312 return a; 2313 return b; 2314 } 2315 2316 // if a W b => b, then a W b = b (for stronger containment) 2317 if (opt_.containment_checks_stronger 2318 && c_->contained(bo, b)) 2319 return b; 2320 // if a => b, then a W (b W c) = b W c 2321 // (Beware: even if a => b we do not have a W (b U c) = b U c) 2322 if (b.is(op::W) && c_->implication(a, b[0])) 2323 return b; 2324 // if b => a, then a W (b U c) = a W c 2325 // if b => a, then a W (b W c) = a W c 2326 if (b.is(op::U, op::W) && c_->implication(b[0], a)) 2327 return recurse(formula::W(a, b[1])); 2328 // if a => b, then (a U c) W b = c W b 2329 // if a => b, then (a W c) W b = c W b 2330 if (a.is(op::U, op::W) && c_->implication(a[0], b)) 2331 return recurse(formula::W(a[1], b)); 2332 // if c => b, then (a W c) W b = (a W c) | b 2333 // if c => b, then (a U c) W b = (a U c) | b 2334 if (a.is(op::U, op::W) && c_->implication(a[1], b)) 2335 return recurse(formula::Or({a, b})); 2336 // if g => h, then (f|g) W h = f M h 2337 if (a.is(op::Or)) 2338 { 2339 unsigned n = a.size(); 2340 for (unsigned child = 0; child < n; ++child) 2341 if (c_->implication(a[child], b)) 2342 return recurse(formula::W(a.all_but(child), b)); 2343 } 2344 break; 2345 2346 case op::M: 2347 // if b => !a, then a M b = 0 2348 if (c_->implication_neg(b, a, true)) 2349 return formula::ff(); 2350 // if b => a, then a M b = b 2351 if (c_->implication(b, a)) 2352 { 2353 // but if also a => b, pick the smallest one. 2354 if ((length_boolone(a) < length_boolone(b)) 2355 && c_->implication(a, b)) 2356 return a; 2357 return b; 2358 } 2359 // if b => a, then a M (b M c) = b M c 2360 if (b.is(op::M) && c_->implication(b[0], a)) 2361 return b; 2362 // if a => b, then a M (b M c) = a M c 2363 // if a => b, then a M (b R c) = a M c 2364 if (b.is(op::M, op::R) && c_->implication(a, b[0])) 2365 return recurse(formula::M(a, b[1])); 2366 // if b => a, then (a R c) M b = c M b 2367 // if b => a, then (a M c) M b = c M b 2368 if (a.is(op::R, op::M) && c_->implication(b, a[0])) 2369 return recurse(formula::M(a[1], b)); 2370 // if c => b, then (a M c) M b = (a & c) M b 2371 if (a.is(op::M) && c_->implication(a[1], b)) 2372 return 2373 recurse(formula::M(formula::And({a[0], a[1]}), 2374 b)); 2375 // if h => g, then (f&g) M h = f M h 2376 if (a.is(op::And)) 2377 { 2378 unsigned n = a.size(); 2379 for (unsigned child = 0; child < n; ++child) 2380 if (c_->implication(b, a[child])) 2381 return recurse(formula::M(a.all_but(child), b)); 2382 } 2383 break; 2384 2385 default: 2386 break; 2387 } 2388 trace << "bo: no inclusion-based rules matched" << std::endl; 2389 } 2390 2391 if (!opt_.reduce_basics) 2392 { 2393 trace << "bo: basic reductions disabled" << std::endl; 2394 return bo; 2395 } 2396 2397 trace << "bo: trying basic reductions" << std::endl; 2398 // Rewrite U,R,W,M as F or G when possible. 2399 // true U b == F(b) 2400 if (bo.is(op::U) && a.is_tt()) 2401 return recurse(formula::F(b)); 2402 // false R b == G(b) 2403 if (bo.is(op::R) && a.is_ff()) 2404 return recurse(formula::G(b)); 2405 // a W false == G(a) 2406 if (bo.is(op::W) && b.is_ff()) 2407 return recurse(formula::G(a)); 2408 // a M true == F(a) 2409 if (bo.is(op::M) && b.is_tt()) 2410 return recurse(formula::F(a)); 2411 2412 if (bo.is(op::W, op::M) || bo.is(op::U, op::R)) 2413 { 2414 // X(a) U X(b) = X(a U b) 2415 // X(a) R X(b) = X(a R b) 2416 // X(a) W X(b) = X(a W b) 2417 // X(a) M X(b) = X(a M b) 2418 if (a.is(op::X) && b.is(op::X)) 2419 return recurse(formula::X(formula::binop(o, 2420 a[0], b[0]))); 2421 2422 if (bo.is(op::U, op::W)) 2423 { 2424 // a U Ga = Ga 2425 // a W Ga = Ga 2426 if (b.is(op::G) && a == b[0]) 2427 return b; 2428 // a U (b | c | G(a)) = a W (b | c) 2429 // a W (b | c | G(a)) = a W (b | c) 2430 if (b.is(op::Or)) 2431 for (int i = 0, s = b.size(); i < s; ++i) 2432 { 2433 formula c = b[i]; 2434 if (c.is(op::G) && c[0] == a) 2435 return recurse(formula::W(a, b.all_but(i))); 2436 } 2437 // a U (b & a & c) == (b & c) M a 2438 // a W (b & a & c) == (b & c) R a 2439 if (b.is(op::And)) 2440 for (int i = 0, s = b.size(); i < s; ++i) 2441 if (b[i] == a) 2442 return recurse(formula::binop(o == op::U ? 2443 op::M : op::R, 2444 b.all_but(i), a)); 2445 // If b is Boolean: 2446 // (Xc) U b = b | X(b M c) 2447 // (Xc) W b = b | X(b R c) 2448 if (!opt_.reduce_size_strictly 2449 && a.is(op::X) && b.is_boolean()) 2450 { 2451 formula x = formula::X(formula::binop(o == op::U ? 2452 op::M : op::R, 2453 b, a[0])); 2454 return recurse(formula::Or({b, x})); 2455 } 2456 } 2457 else if (bo.is(op::M, op::R)) 2458 { 2459 // a R Fa = Fa 2460 // a M Fa = Fa 2461 if (b.is(op::F) && b[0] == a) 2462 return b; 2463 2464 // a R (b & c & F(a)) = a M (b & c) 2465 // a M (b & c & F(a)) = a M (b & c) 2466 if (b.is(op::And)) 2467 for (int i = 0, s = b.size(); i < s; ++i) 2468 { 2469 formula c = b[i]; 2470 if (c.is(op::F) && c[0] == a) 2471 return recurse(formula::M(a, b.all_but(i))); 2472 } 2473 // a M (b | a | c) == (b | c) U a 2474 // a R (b | a | c) == (b | c) W a 2475 if (b.is(op::Or)) 2476 for (int i = 0, s = b.size(); i < s; ++i) 2477 if (b[i] == a) 2478 return recurse(formula::binop(o == op::M ? 2479 op::U : op::W, 2480 b.all_but(i), a)); 2481 // If b is Boolean: 2482 // (Xc) R b = b & X(b W c) 2483 // (Xc) M b = b & X(b U c) 2484 if (!opt_.reduce_size_strictly 2485 && a.is(op::X) && b.is_boolean()) 2486 { 2487 formula x = 2488 formula::X(formula::binop(o == op::M ? op::U : op::W, 2489 b, a[0])); 2490 return recurse(formula::And({b, x})); 2491 } 2492 } 2493 } 2494 if (bo.is(op::UConcat) || bo.is(op::EConcat, op::EConcatMarked)) 2495 return reduce_sere_ltl(bo); 2496 return bo; 2497 } 2498 2499 formula visit_multop(formula mo)2500 visit_multop(formula mo) 2501 { 2502 auto recurse = [this](formula f) 2503 { 2504 return simplify_recursively(f, c_); 2505 }; 2506 2507 unsigned mos = mo.size(); 2508 2509 if ((opt_.synt_impl | opt_.containment_checks) 2510 && mo.is(op::Or, op::And)) 2511 { 2512 // Do not merge these two loops, as rewritings from the 2513 // second loop could prevent rewritings from the first one 2514 // to trigger. 2515 for (unsigned i = 0; i < mos; ++i) 2516 { 2517 formula fi = mo[i]; 2518 formula fo = mo.all_but(i); 2519 // if fi => !fo, then fi & fo = false 2520 // if fo => !fi, then fi & fo = false 2521 // if !fi => fo, then fi | fo = true 2522 // if !fo => fi, then fi | fo = true 2523 bool is_and = mo.is(op::And); 2524 if (c_->implication_neg(fi, fo, is_and) 2525 || c_->implication_neg(fo, fi, is_and)) 2526 return recurse(is_and ? formula::ff() : formula::tt()); 2527 } 2528 for (unsigned i = 0; i < mos; ++i) 2529 { 2530 formula fi = mo[i]; 2531 formula fo = mo.all_but(i); 2532 // if fi => fo, then fi | fo = fo 2533 // if fo => fi, then fi & fo = fo 2534 if ((mo.is(op::Or) && c_->implication(fi, fo)) 2535 || (mo.is(op::And) && c_->implication(fo, fi))) 2536 { 2537 // We are about to pick fo, but hold on! 2538 // Maybe we actually have fi <=> fo, in 2539 // which case we could decide to work on fi or fo. 2540 // 2541 // As a heuristic, let's return the smallest 2542 // subformula. So we only need to check this 2543 // other implication if fi is smaller than fo, 2544 // otherwise we don't care. 2545 if ((length_boolone(fi) < length_boolone(fo)) 2546 && ((mo.is(op::Or) && c_->implication(fo, fi)) 2547 || (mo.is(op::And) && c_->implication(fi, fo)))) 2548 return recurse(fi); 2549 else 2550 return recurse(fo); 2551 } 2552 } 2553 } 2554 2555 vec res; 2556 res.reserve(mos); 2557 for (auto f: mo) 2558 res.emplace_back(f); 2559 op o = mo.kind(); 2560 2561 // basics reduction do not concern Boolean formulas, 2562 // so don't waste time trying to apply them. 2563 if (opt_.reduce_basics && !mo.is_boolean()) 2564 { 2565 switch (o) 2566 { 2567 case op::And: 2568 assert(!mo.is_sere_formula()); 2569 { 2570 // a & X(G(a&b...) & c...) = Ga & X(G(b...) & c...) 2571 // a & (Xa W b) = b R a 2572 // a & (Xa U b) = b M a 2573 // a & (b | X(b R a)) = b R a 2574 // a & (b | X(b M a)) = b M a 2575 if (!mo.is_syntactic_stutter_invariant()) // Skip if no X. 2576 { 2577 typedef std::unordered_set<formula> fset_t; 2578 typedef robin_hood::unordered_node_map 2579 <formula, std::set<unsigned>> fmap_t; 2580 fset_t xgset; // XG(...) 2581 fset_t xset; // X(...) 2582 fmap_t wuset; // (X...)W(...) or (X...)U(...) 2583 2584 std::vector<bool> tokill(mos); 2585 2586 // Make a pass to search for subterms 2587 // of the form XGa or X(... & G(...&a&...) & ...) 2588 for (unsigned n = 0; n < mos; ++n) 2589 { 2590 if (!res[n]) 2591 continue; 2592 if (res[n].is_syntactic_stutter_invariant()) 2593 continue; 2594 2595 if (formula xarg = is_XWU(res[n])) 2596 { 2597 wuset[xarg].insert(n); 2598 continue; 2599 } 2600 2601 // Now we are looking for 2602 // - X(...) 2603 // - b | X(b R ...) 2604 // - b | X(b M ...) 2605 if (formula barg = is_bXbRM(res[n])) 2606 { 2607 wuset[barg[1]].insert(n); 2608 continue; 2609 } 2610 2611 if (!res[n].is(op::X)) 2612 continue; 2613 2614 formula c = res[n][0]; 2615 auto handle_G = [&xgset](formula c) 2616 { 2617 formula a2 = c[0]; 2618 if (a2.is(op::And)) 2619 for (auto c: a2) 2620 xgset.insert(c); 2621 else 2622 xgset.insert(a2); 2623 }; 2624 2625 if (c.is(op::G)) 2626 { 2627 handle_G(c); 2628 } 2629 else if (c.is(op::And)) 2630 { 2631 for (auto cc: c) 2632 if (cc.is(op::G)) 2633 handle_G(cc); 2634 else 2635 xset.insert(cc); 2636 } 2637 else 2638 { 2639 xset.insert(c); 2640 } 2641 res[n] = nullptr; 2642 } 2643 // Make a second pass to check if the "a" 2644 // terms can be used to simplify "Xa W b", 2645 // "Xa U b", "b | X(b R a)", or "b | X(b M a)". 2646 vec resorig(res); 2647 for (unsigned n = 0; n < mos; ++n) 2648 { 2649 formula x = resorig[n]; 2650 if (!x) 2651 continue; 2652 fmap_t::const_iterator gs = wuset.find(x); 2653 if (gs == wuset.end()) 2654 continue; 2655 2656 for (unsigned pos: gs->second) 2657 { 2658 formula wu = resorig[pos]; 2659 if (wu.is(op::W, op::U)) 2660 { 2661 // a & (Xa W b) = b R a 2662 // a & (Xa U b) = b M a 2663 op t = wu.is(op::U) ? op::M : op::R; 2664 assert(wu[0].is(op::X)); 2665 formula a = wu[0][0]; 2666 formula b = wu[1]; 2667 res[pos] = formula::binop(t, b, a); 2668 } 2669 else 2670 { 2671 // a & (b | X(b R a)) = b R a 2672 // a & (b | X(b M a)) = b M a 2673 wu = is_bXbRM(resorig[pos]); 2674 assert(wu); 2675 res[pos] = wu; 2676 } 2677 // Remember to kill "a". 2678 tokill[n] = true; 2679 } 2680 } 2681 2682 // Make third pass to search for terms 'a' 2683 // that also appears as 'XGa'. Replace them 2684 // by 'Ga' and delete XGa. 2685 for (unsigned n = 0; n < mos; ++n) 2686 { 2687 formula x = res[n]; 2688 if (!x) 2689 continue; 2690 fset_t::const_iterator g = xgset.find(x); 2691 if (g != xgset.end()) 2692 { 2693 // x can appear only once. 2694 formula gf = *g; 2695 xgset.erase(g); 2696 res[n] = formula::G(x); 2697 } 2698 else if (tokill[n]) 2699 { 2700 res[n] = nullptr; 2701 } 2702 } 2703 2704 vec xv; 2705 unsigned xgs = xgset.size(); 2706 xv.reserve(xset.size() + 1); 2707 if (xgs > 0) 2708 { 2709 vec xgv; 2710 xgv.reserve(xgs); 2711 for (auto f: xgset) 2712 xgv.emplace_back(f); 2713 xv.emplace_back(unop_multop(op::G, op::And, xgv)); 2714 } 2715 for (auto f: xset) 2716 xv.emplace_back(f); 2717 res.emplace_back(unop_multop(op::X, op::And, xv)); 2718 } 2719 2720 // Gather all operands by type. 2721 mospliter s(mospliter::Strip_X | 2722 mospliter::Strip_FG | 2723 mospliter::Strip_G | 2724 mospliter::Split_F | 2725 mospliter::Split_U_or_W | 2726 mospliter::Split_R_or_M | 2727 mospliter::Split_EventUniv, 2728 res, c_); 2729 2730 // FG(a) & FG(b) = FG(a & b) 2731 formula allFG = unop_unop_multop(op::F, op::G, op::And, 2732 std::move(*s.res_FG)); 2733 // Xa & Xb = X(a & b) 2734 // Xa & Xb & FG(c) = X(a & b & FG(c)) 2735 // For Universal&Eventual formulae f1...fn we also have: 2736 // Xa & Xb & f1...fn = X(a & b & f1...fn) 2737 if (!s.res_X->empty() && !opt_.favor_event_univ) 2738 { 2739 s.res_X->emplace_back(allFG); 2740 allFG = nullptr; 2741 s.res_X->insert(s.res_X->begin(), 2742 s.res_EventUniv->begin(), 2743 s.res_EventUniv->end()); 2744 } 2745 else 2746 // If f1...fn are event&univ formulae, with at least 2747 // one formula of the form G(...), 2748 // Rewrite g & f1...fn as g & G(f1..fn) while 2749 // stripping any leading G from f1...fn. 2750 // This gathers eventual&universal formulae 2751 // under the same term. 2752 { 2753 vec eu; 2754 bool seen_g = false; 2755 for (auto f: *s.res_EventUniv) 2756 if (f.is(op::G)) 2757 { 2758 seen_g = true; 2759 eu.emplace_back(f[0]); 2760 } 2761 else 2762 { 2763 eu.emplace_back(f); 2764 } 2765 if (seen_g) 2766 { 2767 eu.emplace_back(allFG); 2768 allFG = nullptr; 2769 formula andeu = formula::multop(op::And, eu); 2770 if (!opt_.favor_event_univ) 2771 s.res_G->emplace_back(andeu); 2772 else 2773 s.res_other->emplace_back(formula::G(andeu)); 2774 } 2775 else 2776 { 2777 s.res_other->insert(s.res_other->end(), 2778 eu.begin(), eu.end()); 2779 } 2780 } 2781 2782 // Xa & Xb & f1...fn = X(a & b & f1...fn) 2783 // is built at the end of this op::And case. 2784 // G(a) & G(b) = G(a & b) 2785 // is built at the end of this op::And case. 2786 2787 // The following three loops perform these rewritings: 2788 // (a U b) & (c U b) = (a & c) U b 2789 // (a U b) & (c W b) = (a & c) U b 2790 // (a W b) & (c W b) = (a & c) W b 2791 // (a R b) & (a R c) = a R (b & c) 2792 // (a R b) & (a M c) = a M (b & c) 2793 // (a M b) & (a M c) = a M (b & c) 2794 // F(a) & (a R b) = a M b 2795 // F(a) & (a M b) = a M b 2796 // F(b) & (a W b) = a U b 2797 // F(b) & (a U b) = a U b 2798 // F(c) & G(phi | e) = c M (phi | e) if c => !phi. 2799 typedef robin_hood::unordered_map<formula, 2800 vec::iterator> fmap_t; 2801 fmap_t uwmap; // associates "b" to "a U b" or "a W b" 2802 fmap_t rmmap; // associates "a" to "a R b" or "a M b" 2803 // (a U b) & (c U b) = (a & c) U b 2804 // (a U b) & (c W b) = (a & c) U b 2805 // (a W b) & (c W b) = (a & c) W b 2806 for (auto i = s.res_U_or_W->begin(); 2807 i != s.res_U_or_W->end(); ++i) 2808 { 2809 formula b = (*i)[1]; 2810 auto j = uwmap.find(b); 2811 if (j == uwmap.end()) 2812 { 2813 // First occurrence. 2814 uwmap[b] = i; 2815 continue; 2816 } 2817 // We already have one occurrence. Merge them. 2818 formula old = *j->second; 2819 op o = op::W; 2820 if (i->is(op::U) || old.is(op::U)) 2821 o = op::U; 2822 formula fst_arg = formula::And({old[0], (*i)[0]}); 2823 *j->second = formula::binop(o, fst_arg, b); 2824 assert(j->second->is(o)); 2825 *i = nullptr; 2826 } 2827 // (a R b) & (a R c) = a R (b & c) 2828 // (a R b) & (a M c) = a M (b & c) 2829 // (a M b) & (a M c) = a M (b & c) 2830 for (auto i = s.res_R_or_M->begin(); 2831 i != s.res_R_or_M->end(); ++i) 2832 { 2833 formula a = (*i)[0]; 2834 auto j = rmmap.find(a); 2835 if (j == rmmap.end()) 2836 { 2837 // First occurrence. 2838 rmmap[a] = i; 2839 continue; 2840 } 2841 // We already have one occurrence. Merge them. 2842 formula old = *j->second; 2843 op o = op::R; 2844 if (i->is(op::M) || old.is(op::M)) 2845 o = op::M; 2846 formula snd_arg = formula::And({old[1], (*i)[1]}); 2847 *j->second = formula::binop(o, a, snd_arg); 2848 assert(j->second->is(o)); 2849 *i = nullptr; 2850 } 2851 // F(b) & (a W b) = a U b 2852 // F(b) & (a U b) = a U b 2853 // F(a) & (a R b) = a M b 2854 // F(a) & (a M b) = a M b 2855 for (auto& f: *s.res_F) 2856 { 2857 bool superfluous = false; 2858 formula c = f[0]; 2859 2860 fmap_t::iterator j = uwmap.find(c); 2861 if (j != uwmap.end()) 2862 { 2863 superfluous = true; 2864 formula bo = *j->second; 2865 if (bo.is(op::W)) 2866 { 2867 *j->second = formula::U(bo[0], bo[1]); 2868 assert(j->second->is(op::U)); 2869 } 2870 } 2871 j = rmmap.find(c); 2872 if (j != rmmap.end()) 2873 { 2874 superfluous = true; 2875 formula bo = *j->second; 2876 if (bo.is(op::R)) 2877 { 2878 *j->second = formula::M(bo[0], bo[1]); 2879 assert(j->second->is(op::M)); 2880 } 2881 } 2882 if (opt_.synt_impl | opt_.containment_checks) 2883 { 2884 // if the input looks like o1|u1|u2|o2, 2885 // return o1 | o2. The input must have at 2886 // least on universal formula. 2887 auto extract_not_un = 2888 [&](formula f) { 2889 if (f.is(op::Or)) 2890 for (auto u: f) 2891 if (u.is_universal()) 2892 { 2893 vec phi; 2894 phi.reserve(f.size()); 2895 for (auto uu: f) 2896 if (!uu.is_universal()) 2897 phi.push_back(uu); 2898 return formula::Or(phi); 2899 } 2900 return formula(nullptr); 2901 }; 2902 2903 // F(c) & G(phi | e) = c M (phi | e) if c => !phi. 2904 for (auto in_g = s.res_G->begin(); 2905 in_g != s.res_G->end();) 2906 { 2907 if (formula phi = extract_not_un(*in_g)) 2908 if (c_->implication_neg(phi, c, true)) 2909 { 2910 s.res_other->push_back(formula::M(c, 2911 *in_g)); 2912 in_g = s.res_G->erase(in_g); 2913 superfluous = true; 2914 continue; 2915 } 2916 ++in_g; 2917 } 2918 } 2919 if (superfluous) 2920 f = nullptr; 2921 } 2922 2923 s.res_other->reserve(s.res_other->size() 2924 + s.res_F->size() 2925 + s.res_U_or_W->size() 2926 + s.res_R_or_M->size() 2927 + 3); 2928 s.res_other->insert(s.res_other->end(), 2929 s.res_F->begin(), 2930 s.res_F->end()); 2931 s.res_other->insert(s.res_other->end(), 2932 s.res_U_or_W->begin(), 2933 s.res_U_or_W->end()); 2934 s.res_other->insert(s.res_other->end(), 2935 s.res_R_or_M->begin(), 2936 s.res_R_or_M->end()); 2937 2938 // Those "G" formulae that are eventual can be 2939 // postponed inside the X term if there is one. 2940 // 2941 // In effect we rewrite 2942 // Xa&Xb&GFc&GFd&Ge as X(a&b&G(Fc&Fd))&Ge 2943 if (!s.res_X->empty() && !opt_.favor_event_univ) 2944 { 2945 vec event; 2946 for (auto& f: *s.res_G) 2947 if (f.is_eventual()) 2948 { 2949 event.emplace_back(f); 2950 f = nullptr; // Remove it from res_G. 2951 } 2952 s.res_X->emplace_back(unop_multop(op::G, op::And, 2953 std::move(event))); 2954 } 2955 2956 // G(a) & G(b) & ... = G(a & b & ...) 2957 formula allG = unop_multop(op::G, op::And, 2958 std::move(*s.res_G)); 2959 // Xa & Xb & ... = X(a & b & ...) 2960 formula allX = unop_multop(op::X, op::And, 2961 std::move(*s.res_X)); 2962 s.res_other->emplace_back(allX); 2963 s.res_other->emplace_back(allG); 2964 s.res_other->emplace_back(allFG); 2965 formula r = formula::And(std::move(*s.res_other)); 2966 // If we altered the formula in some way, process 2967 // it another time. 2968 if (r != mo) 2969 return recurse(r); 2970 return r; 2971 } 2972 case op::AndRat: 2973 { 2974 mospliter s(mospliter::Split_Bool, res, c_); 2975 if (!s.res_Bool->empty()) 2976 { 2977 // b1 & b2 & b3 = b1 ∧ b2 ∧ b3 2978 formula b = formula::And(std::move(*s.res_Bool)); 2979 2980 vec ares; 2981 for (auto& f: *s.res_other) 2982 switch (f.kind()) 2983 { 2984 case op::Star: 2985 // b && r[*i..j] = b & r if i<=1<=j 2986 // = 0 otherwise 2987 if (f.min() > 1 || f.max() < 1) 2988 return formula::ff(); 2989 ares.emplace_back(f[0]); 2990 f = nullptr; 2991 break; 2992 case op::Fusion: 2993 // b && {r1:..:rn} = b && r1 && .. && rn 2994 for (auto ri: f) 2995 ares.emplace_back(ri); 2996 f = nullptr; 2997 break; 2998 case op::Concat: 2999 // b && {r1;...;rn} = 3000 // - b && ri if there is only one ri 3001 // that does not accept [*0] 3002 // - b && (r1|...|rn) if all ri 3003 // do not accept [*0] 3004 // - 0 if more than one ri accept [*0] 3005 { 3006 formula ri = nullptr; 3007 unsigned nonempty = 0; 3008 unsigned rs = f.size(); 3009 for (unsigned j = 0; j < rs; ++j) 3010 { 3011 formula jf = f[j]; 3012 if (!jf.accepts_eword()) 3013 { 3014 ri = jf; 3015 ++nonempty; 3016 } 3017 } 3018 if (nonempty == 1) 3019 { 3020 ares.emplace_back(ri); 3021 } 3022 else if (nonempty == 0) 3023 { 3024 vec sum; 3025 for (auto j: f) 3026 sum.emplace_back(j); 3027 ares.emplace_back(formula::OrRat(sum)); 3028 } 3029 else 3030 { 3031 return formula::ff(); 3032 } 3033 f = nullptr; 3034 break; 3035 } 3036 default: 3037 ares.emplace_back(f); 3038 f = nullptr; 3039 break; 3040 } 3041 ares.emplace_back(b); 3042 auto r = formula::AndRat(std::move(ares)); 3043 // If we altered the formula in some way, process 3044 // it another time. 3045 if (r != mo) 3046 return recurse(r); 3047 return r; 3048 } 3049 // No Boolean as argument of &&. 3050 3051 // Look for occurrences of {b;r} or {b:r}. We have 3052 // {b1;r1}&&{b2;r2} = {b1&&b2};{r1&&r2} 3053 // head1 tail1 3054 // {b1:r1}&&{b2:r2} = {b1&&b2}:{r1&&r2} 3055 // head2 tail2 3056 vec head1; 3057 vec tail1; 3058 vec head2; 3059 vec tail2; 3060 for (auto& i: *s.res_other) 3061 { 3062 if (!i) 3063 continue; 3064 if (!i.is(op::Concat, op::Fusion)) 3065 continue; 3066 formula h = i[0]; 3067 if (!h.is_boolean()) 3068 continue; 3069 if (i.is(op::Concat)) 3070 { 3071 head1.emplace_back(h); 3072 tail1.emplace_back(i.all_but(0)); 3073 } 3074 else // op::Fusion 3075 { 3076 head2.emplace_back(h); 3077 tail2.emplace_back(i.all_but(0)); 3078 } 3079 i = nullptr; 3080 } 3081 if (!head1.empty()) 3082 { 3083 formula h = formula::And(std::move(head1)); 3084 formula t = formula::AndRat(std::move(tail1)); 3085 s.res_other->emplace_back(formula::Concat({h, t})); 3086 } 3087 if (!head2.empty()) 3088 { 3089 formula h = formula::And(std::move(head2)); 3090 formula t = formula::AndRat(std::move(tail2)); 3091 s.res_other->emplace_back(formula::Fusion({h, t})); 3092 } 3093 3094 // {r1;b1}&&{r2;b2} = {r1&&r2};{b1∧b2} 3095 // head3 tail3 3096 // {r1:b1}&&{r2:b2} = {r1&&r2}:{b1∧b2} 3097 // head4 tail4 3098 vec head3; 3099 vec tail3; 3100 vec head4; 3101 vec tail4; 3102 for (auto& i: *s.res_other) 3103 { 3104 if (!i) 3105 continue; 3106 if (!i.is(op::Concat, op::Fusion)) 3107 continue; 3108 unsigned s = i.size() - 1; 3109 formula t = i[s]; 3110 if (!t.is_boolean()) 3111 continue; 3112 if (i.is(op::Concat)) 3113 { 3114 tail3.emplace_back(t); 3115 head3.emplace_back(i.all_but(s)); 3116 } 3117 else // op::Fusion 3118 { 3119 tail4.emplace_back(t); 3120 head4.emplace_back(i.all_but(s)); 3121 } 3122 i = nullptr; 3123 } 3124 if (!head3.empty()) 3125 { 3126 formula h = formula::AndRat(std::move(head3)); 3127 formula t = formula::And(std::move(tail3)); 3128 s.res_other->emplace_back(formula::Concat({h, t})); 3129 } 3130 if (!head4.empty()) 3131 { 3132 formula h = formula::AndRat(std::move(head4)); 3133 formula t = formula::And(std::move(tail4)); 3134 s.res_other->emplace_back(formula::Fusion({h, t})); 3135 } 3136 3137 auto r = formula::AndRat(std::move(*s.res_other)); 3138 // If we altered the formula in some way, process 3139 // it another time. 3140 if (r != mo) 3141 return recurse(r); 3142 return r; 3143 } 3144 case op::Or: 3145 { 3146 // a | X(F(a) | c...) = Fa | X(c...) 3147 // a | (Xa R b) = b W a 3148 // a | (Xa M b) = b U a 3149 // a | (b & X(b W a)) = b W a 3150 // a | (b & X(b U a)) = b U a 3151 if (!mo.is_syntactic_stutter_invariant()) // Skip if no X 3152 { 3153 typedef std::unordered_set<formula> fset_t; 3154 typedef robin_hood::unordered_node_map 3155 <formula, std::set<unsigned>> fmap_t; 3156 fset_t xfset; // XF(...) 3157 fset_t xset; // X(...) 3158 fmap_t rmset; // (X...)R(...) or (X...)M(...) or 3159 // b & X(b W ...) or b & X(b U ...) 3160 3161 std::vector<bool> tokill(mos); 3162 3163 // Make a pass to search for subterms 3164 // of the form XFa or X(... | F(...|a|...) | ...) 3165 for (unsigned n = 0; n < mos; ++n) 3166 { 3167 if (!res[n]) 3168 continue; 3169 if (res[n].is_syntactic_stutter_invariant()) 3170 continue; 3171 3172 if (formula xarg = is_XRM(res[n])) 3173 { 3174 rmset[xarg].insert(n); 3175 continue; 3176 } 3177 3178 // Now we are looking for 3179 // - X(...) 3180 // - b & X(b W ...) 3181 // - b & X(b U ...) 3182 if (formula barg = is_bXbWU(res[n])) 3183 { 3184 rmset[barg[1]].insert(n); 3185 continue; 3186 } 3187 3188 if (!res[n].is(op::X)) 3189 continue; 3190 3191 formula c = res[n][0]; 3192 3193 auto handle_F = [&xfset](formula c) 3194 { 3195 formula a2 = c[0]; 3196 if (a2.is(op::Or)) 3197 for (auto c: a2) 3198 xfset.insert(c); 3199 else 3200 xfset.insert(a2); 3201 }; 3202 3203 if (c.is(op::F)) 3204 { 3205 handle_F(c); 3206 } 3207 else if (c.is(op::Or)) 3208 { 3209 for (auto cc: c) 3210 if (cc.is(op::F)) 3211 handle_F(cc); 3212 else 3213 xset.insert(cc); 3214 } 3215 else 3216 { 3217 xset.insert(c); 3218 } 3219 res[n] = nullptr; 3220 } 3221 // Make a second pass to check if we can 3222 // remove all instance of XF(a). 3223 unsigned allofthem = xfset.size(); 3224 vec resorig(res); 3225 for (unsigned n = 0; n < mos; ++n) 3226 { 3227 formula x = resorig[n]; 3228 if (!x) 3229 continue; 3230 fset_t::const_iterator f = xfset.find(x); 3231 if (f != xfset.end()) 3232 --allofthem; 3233 assert(allofthem != -1U); 3234 // At the same time, check if "a" can also 3235 // be used to simplify "Xa R b", "Xa M b". 3236 // "b & X(b W a)", or "b & X(b U a)". 3237 fmap_t::const_iterator gs = rmset.find(x); 3238 if (gs == rmset.end()) 3239 continue; 3240 for (unsigned pos: gs->second) 3241 { 3242 formula rm = resorig[pos]; 3243 if (rm.is(op::M, op::R)) 3244 { 3245 // a | (Xa R b) = b W a 3246 // a | (Xa M b) = b U a 3247 op t = rm.is(op::M) ? op::U : op::W; 3248 assert(rm[0].is(op::X)); 3249 formula a = rm[0][0]; 3250 formula b = rm[1]; 3251 res[pos] = formula::binop(t, b, a); 3252 } 3253 else 3254 { 3255 // a | (b & X(b W a)) = b W a 3256 // a | (b & X(b U a)) = b U a 3257 rm = is_bXbWU(resorig[pos]); 3258 assert(rm); 3259 res[pos] = rm; 3260 } 3261 // Remember to kill "a". 3262 tokill[n] = true; 3263 } 3264 } 3265 3266 // If we can remove all of them... 3267 if (allofthem == 0) 3268 // Make third pass to search for terms 'a' 3269 // that also appears as 'XFa'. Replace them 3270 // by 'Fa' and delete XFa. 3271 for (unsigned n = 0; n < mos; ++n) 3272 { 3273 formula x = res[n]; 3274 if (!x) 3275 continue; 3276 fset_t::const_iterator f = xfset.find(x); 3277 if (f != xfset.end()) 3278 { 3279 // x can appear only once. 3280 formula ff = *f; 3281 xfset.erase(f); 3282 res[n] = formula::F(x); 3283 // We don't need to kill "a" anymore. 3284 tokill[n] = false; 3285 } 3286 } 3287 // Kill any remaining "a", used to simplify Xa R b 3288 // or Xa M b. 3289 for (unsigned n = 0; n < mos; ++n) 3290 if (tokill[n] && res[n]) 3291 res[n] = nullptr; 3292 3293 // Now rebuild the formula that remains. 3294 vec xv; 3295 size_t xfs = xfset.size(); 3296 xv.reserve(xset.size() + 1); 3297 if (xfs > 0) 3298 { 3299 // Group all XF(a)|XF(b|c|...)|... as XF(a|b|c|...) 3300 vec xfv; 3301 xfv.reserve(xfs); 3302 for (auto f: xfset) 3303 xfv.emplace_back(f); 3304 xv.emplace_back(unop_multop(op::F, op::Or, xfv)); 3305 } 3306 // Also gather the remaining Xa | X(b|c) as X(b|c). 3307 for (auto f: xset) 3308 xv.emplace_back(f); 3309 res.emplace_back(unop_multop(op::X, op::Or, xv)); 3310 } 3311 3312 // Gather all operand by type. 3313 mospliter s(mospliter::Strip_X | 3314 mospliter::Strip_GF | 3315 mospliter::Strip_F | 3316 mospliter::Split_G | 3317 mospliter::Split_U_or_W | 3318 mospliter::Split_R_or_M | 3319 mospliter::Split_EventUniv, 3320 res, c_); 3321 // GF(a) | GF(b) = GF(a | b) 3322 formula allGF = unop_unop_multop(op::G, op::F, op::Or, 3323 std::move(*s.res_GF)); 3324 3325 bool eu_has_F = false; 3326 for (auto f: *s.res_EventUniv) 3327 if (f.is(op::F)) 3328 eu_has_F = true; 3329 3330 // Xa | Xb = X(a | b) 3331 // Xa | Xb | GF(c) = X(a | b | GF(c)) 3332 // For Universal&Eventual formula f1...fn we also have: 3333 // Xa | Xb | f1...fn = X(a | b | f1...fn) 3334 if (!s.res_X->empty() && !opt_.favor_event_univ) 3335 { 3336 s.res_X->emplace_back(allGF); 3337 allGF = nullptr; 3338 s.res_X->insert(s.res_X->end(), 3339 s.res_EventUniv->begin(), 3340 s.res_EventUniv->end()); 3341 } 3342 else if (!opt_.favor_event_univ 3343 && (!s.res_F->empty() || eu_has_F) 3344 && s.res_G->empty() 3345 && s.res_U_or_W->empty() 3346 && s.res_R_or_M->empty() 3347 && s.res_other->empty()) 3348 { 3349 // If there is no X but some F and only 3350 // eventual&universal formulae f1...fn|GF(c), do: 3351 // Fa|Fb|f1...fn|GF(c) = F(a|b|f1...fn|GF(c)) 3352 // 3353 // The reasoning here is that if we should 3354 // move f1...fn|GF(c) inside the "F" only 3355 // if it allows us to move all terms under F, 3356 // allowing a nice initial self-loop. 3357 // 3358 // For instance: 3359 // F(a|GFb) 3st.6tr. with initial self-loop 3360 // Fa|GFb 4st.8tr. without initial self-loop 3361 // 3362 // However, if other terms are presents they will 3363 // prevent the formation of a self-loop, and the 3364 // rewriting is unwelcome: 3365 // F(a|GFb)|Gc 5st.11tr. without initial self-loop 3366 // Fa|GFb|Gc 5st.10tr. without initial self-loop 3367 // (counting the number of "subtransitions" 3368 // or, degeneralizing the automaton amplifies 3369 // these differences) 3370 s.res_F->emplace_back(allGF); 3371 allGF = nullptr; 3372 for (auto f: *s.res_EventUniv) 3373 s.res_F->emplace_back(f.is(op::F) ? f[0] : f); 3374 } 3375 else if (opt_.favor_event_univ) 3376 { 3377 s.res_EventUniv->emplace_back(allGF); 3378 allGF = nullptr; 3379 bool seen_f = false; 3380 if (s.res_EventUniv->size() > 1) 3381 { 3382 // If some of the EventUniv formulas start 3383 // with an F, Gather them all under the 3384 // same F. Striping any leading F. 3385 for (auto& f: *s.res_EventUniv) 3386 if (f.is(op::F)) 3387 { 3388 seen_f = true; 3389 f = f[0]; 3390 } 3391 if (seen_f) 3392 { 3393 formula eu = 3394 unop_multop(op::F, op::Or, 3395 std::move(*s.res_EventUniv)); 3396 s.res_other->emplace_back(eu); 3397 } 3398 } 3399 if (!seen_f) 3400 s.res_other->insert(s.res_other->end(), 3401 s.res_EventUniv->begin(), 3402 s.res_EventUniv->end()); 3403 } 3404 else 3405 { 3406 for (auto f: *s.res_EventUniv) 3407 { 3408 if (f.is(op::F)) 3409 s.res_F->emplace_back(f[0]); 3410 else 3411 s.res_other->emplace_back(f); 3412 } 3413 } 3414 // Xa | Xb | f1...fn = X(a | b | f1...fn) 3415 // is built at the end of this multop::Or case. 3416 // F(a) | F(b) = F(a | b) 3417 // is built at the end of this multop::Or case. 3418 3419 // The following three loops perform these rewritings: 3420 // (a U b) | (a U c) = a U (b | c) 3421 // (a W b) | (a U c) = a W (b | c) 3422 // (a W b) | (a W c) = a W (b | c) 3423 // (a R b) | (c R b) = (a | c) R b 3424 // (a R b) | (c M b) = (a | c) R b 3425 // (a M b) | (c M b) = (a | c) M b 3426 // G(a) | (a U b) = a W b 3427 // G(a) | (a W b) = a W b 3428 // G(b) | (a R b) = a R b. 3429 // G(b) | (a M b) = a R b. 3430 // G(c) | F(phi & e) = c W (phi & e) if !c => phi. 3431 typedef robin_hood::unordered_map<formula, 3432 vec::iterator> fmap_t; 3433 fmap_t uwmap; // associates "a" to "a U b" or "a W b" 3434 fmap_t rmmap; // associates "b" to "a R b" or "a M b" 3435 // (a U b) | (a U c) = a U (b | c) 3436 // (a W b) | (a U c) = a W (b | c) 3437 // (a W b) | (a W c) = a W (b | c) 3438 for (auto i = s.res_U_or_W->begin(); 3439 i != s.res_U_or_W->end(); ++i) 3440 { 3441 formula a = (*i)[0]; 3442 auto j = uwmap.find(a); 3443 if (j == uwmap.end()) 3444 { 3445 // First occurrence. 3446 uwmap[a] = i; 3447 continue; 3448 } 3449 // We already have one occurrence. Merge them. 3450 formula old = *j->second; 3451 op o = op::U; 3452 if (i->is(op::W) || old.is(op::W)) 3453 o = op::W; 3454 formula snd_arg = formula::Or({old[1], (*i)[1]}); 3455 *j->second = formula::binop(o, a, snd_arg); 3456 assert(j->second->is(o)); 3457 *i = nullptr; 3458 } 3459 // (a R b) | (c R b) = (a | c) R b 3460 // (a R b) | (c M b) = (a | c) R b 3461 // (a M b) | (c M b) = (a | c) M b 3462 for (auto i = s.res_R_or_M->begin(); 3463 i != s.res_R_or_M->end(); ++i) 3464 { 3465 formula b = (*i)[1]; 3466 auto j = rmmap.find(b); 3467 if (j == rmmap.end()) 3468 { 3469 // First occurrence. 3470 rmmap[b] = i; 3471 continue; 3472 } 3473 // We already have one occurrence. Merge them. 3474 formula old = *j->second; 3475 op o = op::M; 3476 if (i->is(op::R) || old.is(op::R)) 3477 o = op::R; 3478 formula fst_arg = formula::Or({old[0], (*i)[0]}); 3479 *j->second = formula::binop(o, fst_arg, b); 3480 assert(j->second->is(o)); 3481 *i = nullptr; 3482 } 3483 // G(a) | (a U b) = a W b 3484 // G(a) | (a W b) = a W b 3485 // G(b) | (a R b) = a R b. 3486 // G(b) | (a M b) = a R b. 3487 for (auto& f: *s.res_G) 3488 { 3489 bool superfluous = false; 3490 formula c = f[0]; 3491 3492 fmap_t::iterator j = uwmap.find(c); 3493 if (j != uwmap.end()) 3494 { 3495 superfluous = true; 3496 formula bo = *j->second; 3497 if (bo.is(op::U)) 3498 { 3499 *j->second = formula::W(bo[0], bo[1]); 3500 assert(j->second->is(op::W)); 3501 } 3502 } 3503 j = rmmap.find(c); 3504 if (j != rmmap.end()) 3505 { 3506 superfluous = true; 3507 formula bo = *j->second; 3508 if (bo.is(op::M)) 3509 { 3510 *j->second = formula::R(bo[0], bo[1]); 3511 assert(j->second->is(op::R)); 3512 } 3513 } 3514 if (opt_.synt_impl | opt_.containment_checks) 3515 { 3516 // if the input looks like o1&e1&e2&o2, 3517 // return o1 & o2. The input must have at 3518 // least on eventual formula. 3519 auto extract_not_ev = 3520 [&](formula f) { 3521 if (f.is(op::And)) 3522 for (auto e: f) 3523 if (e.is_eventual()) 3524 { 3525 vec phi; 3526 phi.reserve(f.size()); 3527 for (auto ee: f) 3528 if (!ee.is_eventual()) 3529 phi.push_back(ee); 3530 return formula::And(phi); 3531 } 3532 return formula(nullptr); 3533 }; 3534 3535 // G(c) | F(phi & e) = c W (phi & e) if !c => phi. 3536 for (auto in_f = s.res_F->begin(); 3537 in_f != s.res_F->end();) 3538 { 3539 if (formula phi = extract_not_ev(*in_f)) 3540 if (c_->implication_neg(c, phi, false)) 3541 { 3542 s.res_other->push_back(formula::W(c, 3543 *in_f)); 3544 in_f = s.res_F->erase(in_f); 3545 superfluous = true; 3546 continue; 3547 } 3548 ++in_f; 3549 } 3550 } 3551 if (superfluous) 3552 f = nullptr; 3553 } 3554 3555 s.res_other->reserve(s.res_other->size() 3556 + s.res_G->size() 3557 + s.res_U_or_W->size() 3558 + s.res_R_or_M->size() 3559 + 3); 3560 s.res_other->insert(s.res_other->end(), 3561 s.res_G->begin(), 3562 s.res_G->end()); 3563 s.res_other->insert(s.res_other->end(), 3564 s.res_U_or_W->begin(), 3565 s.res_U_or_W->end()); 3566 s.res_other->insert(s.res_other->end(), 3567 s.res_R_or_M->begin(), 3568 s.res_R_or_M->end()); 3569 3570 // Those "F" formulae that are universal can be 3571 // postponed inside the X term if there is one. 3572 // 3573 // In effect we rewrite 3574 // Xa|Xb|FGc|FGd|Fe as X(a|b|F(Gc|Gd))|Fe 3575 if (!s.res_X->empty()) 3576 { 3577 vec univ; 3578 for (auto& f: *s.res_F) 3579 if (f.is_universal()) 3580 { 3581 univ.emplace_back(f); 3582 f = nullptr; // Remove it from res_F. 3583 } 3584 s.res_X->emplace_back(unop_multop(op::F, op::Or, 3585 std::move(univ))); 3586 } 3587 3588 // F(a) | F(b) | ... = F(a | b | ...) 3589 formula allF = unop_multop(op::F, op::Or, 3590 std::move(*s.res_F)); 3591 // Xa | Xb | ... = X(a | b | ...) 3592 formula allX = unop_multop(op::X, op::Or, 3593 std::move(*s.res_X)); 3594 s.res_other->emplace_back(allX); 3595 s.res_other->emplace_back(allF); 3596 s.res_other->emplace_back(allGF); 3597 formula r = formula::Or(std::move(*s.res_other)); 3598 // If we altered the formula in some way, process 3599 // it another time. 3600 if (r != mo) 3601 return recurse(r); 3602 return r; 3603 } 3604 case op::AndNLM: 3605 { 3606 mospliter s(mospliter::Split_Bool, res, c_); 3607 if (!s.res_Bool->empty()) 3608 { 3609 // b1 & b2 & b3 = b1 ∧ b2 ∧ b3 3610 formula b = formula::And(std::move(*s.res_Bool)); 3611 3612 // now we just consider b & rest 3613 formula rest = formula::AndNLM(std::move(*s.res_other)); 3614 3615 // We have b & rest = b : rest if rest does not 3616 // accept [*0]. Otherwise b & rest = b | (b : rest) 3617 // FIXME: It would be nice to remove [*0] from rest. 3618 formula r = nullptr; 3619 if (rest.accepts_eword()) 3620 { 3621 // The b & rest = b | (b : rest) rewriting 3622 // augment the size, so do that only when 3623 // explicitly requested. 3624 if (!opt_.reduce_size_strictly) 3625 return recurse(formula::OrRat 3626 ({b, formula::Fusion({b, rest})})); 3627 else 3628 return mo; 3629 } 3630 else 3631 { 3632 return recurse(formula::Fusion({b, rest})); 3633 } 3634 } 3635 // No Boolean as argument of &&. 3636 3637 // Look for occurrences of {b;r} or {b:r}. We have 3638 // {b1;r1}&{b2;r2} = {b1∧b2};{r1&r2} 3639 // head1 tail1 3640 // {b1:r1}&{b2:r2} = {b1∧b2}:{r1&r2} 3641 // head2 tail2 3642 // BEWARE: The second rule is correct only when 3643 // both r1 and r2 do not accept [*0]. 3644 3645 vec head1; 3646 vec tail1; 3647 vec head2; 3648 vec tail2; 3649 for (auto& i: *s.res_other) 3650 { 3651 if (!i) 3652 continue; 3653 if (!i.is(op::Concat, op::Fusion)) 3654 continue; 3655 formula h = i[0]; 3656 if (!h.is_boolean()) 3657 continue; 3658 if (i.is(op::Concat)) 3659 { 3660 head1.emplace_back(h); 3661 tail1.emplace_back(i.all_but(0)); 3662 } 3663 else // op::Fusion 3664 { 3665 formula t = i.all_but(0); 3666 if (t.accepts_eword()) 3667 continue; 3668 head2.emplace_back(h); 3669 tail2.emplace_back(t); 3670 } 3671 i = nullptr; 3672 } 3673 if (!head1.empty()) 3674 { 3675 formula h = formula::And(std::move(head1)); 3676 formula t = formula::AndNLM(std::move(tail1)); 3677 s.res_other->emplace_back(formula::Concat({h, t})); 3678 } 3679 if (!head2.empty()) 3680 { 3681 formula h = formula::And(std::move(head2)); 3682 formula t = formula::AndNLM(std::move(tail2)); 3683 s.res_other->emplace_back(formula::Fusion({h, t})); 3684 } 3685 3686 formula r = formula::AndNLM(std::move(*s.res_other)); 3687 // If we altered the formula in some way, process 3688 // it another time. 3689 if (r != mo) 3690 return recurse(r); 3691 return r; 3692 } 3693 case op::OrRat: 3694 case op::Concat: 3695 case op::Fusion: 3696 // FIXME: No simplifications yet. 3697 return mo; 3698 default: 3699 SPOT_UNIMPLEMENTED(); 3700 return nullptr; 3701 } 3702 SPOT_UNREACHABLE(); 3703 } 3704 return mo; 3705 } 3706 3707 protected: 3708 tl_simplifier_cache* c_; 3709 const tl_simplifier_options& opt_; 3710 }; 3711 3712 3713 formula simplify_recursively(formula f,tl_simplifier_cache * c)3714 simplify_recursively(formula f, 3715 tl_simplifier_cache* c) 3716 { 3717 #ifdef TRACE 3718 static int srec = 0; 3719 for (int i = srec; i; --i) 3720 trace << ' '; 3721 trace << "** simplify_recursively(" << str_psl(f) << ')'; 3722 #endif 3723 3724 formula result = c->lookup_simplified(f); 3725 if (result) 3726 { 3727 trace << " cached: " << str_psl(result) << std::endl; 3728 return result; 3729 } 3730 else 3731 { 3732 trace << " miss" << std::endl; 3733 } 3734 3735 #ifdef TRACE 3736 ++srec; 3737 #endif 3738 3739 if (f.is_boolean() && c->options.boolean_to_isop) 3740 { 3741 result = c->boolean_to_isop(f); 3742 } 3743 else 3744 { 3745 simplify_visitor v(c); 3746 result = v.visit(f); 3747 } 3748 3749 #ifdef TRACE 3750 --srec; 3751 for (int i = srec; i; --i) 3752 trace << ' '; 3753 trace << "** simplify_recursively(" << str_psl(f) << ") result: " 3754 << str_psl(result) << std::endl; 3755 #endif 3756 3757 c->cache_simplified(f, result); 3758 return result; 3759 } 3760 3761 } // anonymous namespace 3762 3763 ////////////////////////////////////////////////////////////////////// 3764 // tl_simplifier_cache 3765 3766 3767 // This implements the recursive rules for syntactic implication. 3768 // (To follow this code please look at the table given as an 3769 // appendix in the documentation for temporal logic operators.) 3770 inline 3771 bool syntactic_implication_aux(formula f,formula g)3772 tl_simplifier_cache::syntactic_implication_aux(formula f, formula g) 3773 { 3774 // We first process all lines from the table except the 3775 // first two, and then we process the first two as a fallback. 3776 // 3777 // However for Boolean formulas we skip the bottom lines 3778 // (keeping only the first one) to prevent them from being 3779 // further split. 3780 if (!f.is_boolean()) 3781 // Deal with all lines of the table except the first two. 3782 switch (f.kind()) 3783 { 3784 case op::X: 3785 case op::strong_X: 3786 if (g.is_eventual() && syntactic_implication(f[0], g)) 3787 return true; 3788 if (g.is(op::X, op::strong_X) && syntactic_implication(f[0], g[0])) 3789 return true; 3790 break; 3791 3792 case op::F: 3793 if (g.is_eventual() && syntactic_implication(f[0], g)) 3794 return true; 3795 break; 3796 3797 case op::G: 3798 if (g.is(op::U, op::R) && syntactic_implication(f[0], g[1])) 3799 return true; 3800 if (g.is(op::W) && (syntactic_implication(f[0], g[0]) 3801 || syntactic_implication(f[0], g[1]))) 3802 return true; 3803 if (g.is(op::M) && (syntactic_implication(f[0], g[0]) 3804 && syntactic_implication(f[0], g[1]))) 3805 return true; 3806 // First column. 3807 if (syntactic_implication(f[0], g)) 3808 return true; 3809 break; 3810 3811 case op::U: 3812 { 3813 formula f1 = f[0]; 3814 formula f2 = f[1]; 3815 if (g.is(op::U, op::W) 3816 && syntactic_implication(f1, g[0]) 3817 && syntactic_implication(f2, g[1])) 3818 return true; 3819 if (g.is(op::M, op::R) 3820 && syntactic_implication(f1, g[1]) 3821 && syntactic_implication(f2, g[0]) 3822 && syntactic_implication(f2, g[1])) 3823 return true; 3824 if (g.is(op::F) && syntactic_implication(f2, g[0])) 3825 return true; 3826 // First column. 3827 if (syntactic_implication(f1, g) && syntactic_implication(f2, g)) 3828 return true; 3829 break; 3830 } 3831 case op::W: 3832 { 3833 formula f1 = f[0]; 3834 formula f2 = f[1]; 3835 if (g.is(op::U) && (syntactic_implication(f1, g[1]) 3836 && syntactic_implication(f2, g[1]))) 3837 return true; 3838 if (g.is(op::W) && (syntactic_implication(f1, g[0]) 3839 && syntactic_implication(f2, g[1]))) 3840 return true; 3841 if (g.is(op::R) && (syntactic_implication(f1, g[1]) 3842 && syntactic_implication(f2, g[0]) 3843 && syntactic_implication(f2, g[1]))) 3844 return true; 3845 if (g.is(op::F) && (syntactic_implication(f1, g[0]) 3846 && syntactic_implication(f2, g[0]))) 3847 return true; 3848 // First column. 3849 if (syntactic_implication(f1, g) && syntactic_implication(f2, g)) 3850 return true; 3851 break; 3852 } 3853 case op::R: 3854 { 3855 formula f1 = f[0]; 3856 formula f2 = f[1]; 3857 if (g.is(op::W) && (syntactic_implication(f1, g[1]) 3858 && syntactic_implication(f2, g[0]))) 3859 return true; 3860 if (g.is(op::R) && (syntactic_implication(f1, g[0]) 3861 && syntactic_implication(f2, g[1]))) 3862 return true; 3863 if (g.is(op::M) && (syntactic_implication(f2, g[0]) 3864 && syntactic_implication(f2, g[1]))) 3865 return true; 3866 if (g.is(op::F) && syntactic_implication(f2, g[0])) 3867 return true; 3868 // First column. 3869 if (syntactic_implication(f2, g)) 3870 return true; 3871 break; 3872 } 3873 case op::M: 3874 { 3875 formula f1 = f[0]; 3876 formula f2 = f[1]; 3877 if (g.is(op::U, op::W) && (syntactic_implication(f1, g[1]) 3878 && syntactic_implication(f2, 3879 g[0]))) 3880 return true; 3881 if (g.is(op::R, op::M) && (syntactic_implication(f1, g[0]) 3882 && syntactic_implication(f2, 3883 g[1]))) 3884 return true; 3885 if (g.is(op::F) && (syntactic_implication(f1, g[0]) 3886 || syntactic_implication(f2, g[0]))) 3887 return true; 3888 // First column. 3889 if (syntactic_implication(f2, g)) 3890 return true; 3891 break; 3892 } 3893 case op::Or: 3894 { 3895 // If we are checking something like 3896 // (a | b | Xc) => g, 3897 // split it into 3898 // (a | b) => g 3899 // Xc => g 3900 unsigned i = 0; 3901 if (formula bops = f.boolean_operands(&i)) 3902 if (!syntactic_implication(bops, g)) 3903 break; 3904 bool b = true; 3905 unsigned fs = f.size(); 3906 for (; i < fs; ++i) 3907 if (!syntactic_implication(f[i], g)) 3908 { 3909 b = false; 3910 break; 3911 } 3912 if (b) 3913 return true; 3914 break; 3915 } 3916 case op::And: 3917 { 3918 // If we are checking something like 3919 // (a & b & Xc) => g, 3920 // split it into 3921 // (a & b) => g 3922 // Xc => g 3923 unsigned i = 0; 3924 if (formula bops = f.boolean_operands(&i)) 3925 if (syntactic_implication(bops, g)) 3926 return true; 3927 unsigned fs = f.size(); 3928 for (; i < fs; ++i) 3929 if (syntactic_implication(f[i], g)) 3930 return true; 3931 break; 3932 } 3933 default: 3934 break; 3935 } 3936 // First two lines of the table. 3937 // (Don't check equality, it has already be done.) 3938 if (!g.is_boolean()) 3939 switch (g.kind()) 3940 { 3941 case op::F: 3942 if (syntactic_implication(f, g[0])) 3943 return true; 3944 break; 3945 3946 case op::G: 3947 case op::X: 3948 case op::strong_X: 3949 if (f.is_universal() && syntactic_implication(f, g[0])) 3950 return true; 3951 break; 3952 3953 case op::U: 3954 case op::W: 3955 if (syntactic_implication(f, g[1])) 3956 return true; 3957 break; 3958 3959 case op::M: 3960 case op::R: 3961 if (syntactic_implication(f, g[0]) 3962 && syntactic_implication(f, g[1])) 3963 return true; 3964 break; 3965 3966 case op::And: 3967 { 3968 // If we are checking something like 3969 // f => (a & b & Xc), 3970 // split it into 3971 // f => (a & b) 3972 // f => Xc 3973 unsigned i = 0; 3974 if (formula bops = g.boolean_operands(&i)) 3975 if (!syntactic_implication(f, bops)) 3976 break; 3977 bool b = true; 3978 unsigned gs = g.size(); 3979 for (; i < gs; ++i) 3980 if (!syntactic_implication(f, g[i])) 3981 { 3982 b = false; 3983 break; 3984 } 3985 if (b) 3986 return true; 3987 break; 3988 } 3989 3990 case op::Or: 3991 { 3992 // If we are checking something like 3993 // f => (a | b | Xc), 3994 // split it into 3995 // f => (a | b) 3996 // f => Xc 3997 unsigned i = 0; 3998 if (formula bops = g.boolean_operands(&i)) 3999 if (syntactic_implication(f, bops)) 4000 return true; 4001 unsigned gs = g.size(); 4002 for (; i < gs; ++i) 4003 if (syntactic_implication(f, g[i])) 4004 return true; 4005 break; 4006 } 4007 default: 4008 break; 4009 } 4010 return false; 4011 } 4012 4013 // Return true if f => g syntactically 4014 bool syntactic_implication(formula f,formula g)4015 tl_simplifier_cache::syntactic_implication(formula f, 4016 formula g) 4017 { 4018 // We cannot run syntactic_implication on SERE formulae, 4019 // except on Boolean formulae. 4020 if (f.is_sere_formula() && !f.is_boolean()) 4021 return false; 4022 if (g.is_sere_formula() && !g.is_boolean()) 4023 return false; 4024 4025 if (f == g) 4026 return true; 4027 if (g.is_tt() || f.is_ff()) 4028 return true; 4029 if (g.is_ff() || f.is_tt()) 4030 return false; 4031 4032 // Often we compare a literal (an atomic_prop or its negation) 4033 // to another literal. The result is necessarily false. To be 4034 // true, the two literals would have to be equal, but we have 4035 // already checked that. 4036 if (f.is_literal() && g.is_literal()) 4037 return false; 4038 4039 // Cache lookup 4040 { 4041 pairf p(f, g); 4042 syntimpl_cache_t::const_iterator i = syntimpl_.find(p); 4043 if (i != syntimpl_.end()) 4044 return i->second; 4045 } 4046 4047 bool result; 4048 4049 if (f.is_boolean() && g.is_boolean()) 4050 { 4051 bdd l = as_bdd(f); 4052 result = bdd_implies(l, as_bdd(g)); 4053 } 4054 else 4055 { 4056 result = syntactic_implication_aux(f, g); 4057 } 4058 4059 // Cache result 4060 { 4061 pairf p(f, g); 4062 syntimpl_[p] = result; 4063 // std::cerr << str_psl(f) << (result ? " ==> " : " =/=> ") 4064 // << str_psl(g) << std::endl; 4065 } 4066 4067 return result; 4068 } 4069 4070 // If right==false, true if !f1 => f2, false otherwise. 4071 // If right==true, true if f1 => !f2, false otherwise. 4072 bool syntactic_implication_neg(formula f1,formula f2,bool right)4073 tl_simplifier_cache::syntactic_implication_neg(formula f1, 4074 formula f2, 4075 bool right) 4076 { 4077 // We cannot run syntactic_implication_neg on SERE formulae, 4078 // except on Boolean formulae. 4079 if (f1.is_sere_formula() && !f1.is_boolean()) 4080 return false; 4081 if (f2.is_sere_formula() && !f2.is_boolean()) 4082 return false; 4083 if (right) 4084 f2 = nenoform_rec(f2, true, this, false); 4085 else 4086 f1 = nenoform_rec(f1, true, this, false); 4087 return syntactic_implication(f1, f2); 4088 } 4089 4090 4091 ///////////////////////////////////////////////////////////////////// 4092 // tl_simplifier 4093 tl_simplifier(const bdd_dict_ptr & d)4094 tl_simplifier::tl_simplifier(const bdd_dict_ptr& d) 4095 { 4096 cache_ = new tl_simplifier_cache(d); 4097 } 4098 tl_simplifier(const tl_simplifier_options & opt,bdd_dict_ptr d)4099 tl_simplifier::tl_simplifier(const tl_simplifier_options& opt, 4100 bdd_dict_ptr d) 4101 { 4102 cache_ = new tl_simplifier_cache(d, opt); 4103 } 4104 ~tl_simplifier()4105 tl_simplifier::~tl_simplifier() 4106 { 4107 delete cache_; 4108 } 4109 4110 formula simplify(formula f)4111 tl_simplifier::simplify(formula f) 4112 { 4113 if (!f.is_in_nenoform()) 4114 f = negative_normal_form(f, false); 4115 return simplify_recursively(f, cache_); 4116 } 4117 4118 tl_simplifier_options& options()4119 tl_simplifier::options() 4120 { 4121 return cache_->options; 4122 } 4123 4124 formula negative_normal_form(formula f,bool negated)4125 tl_simplifier::negative_normal_form(formula f, bool negated) 4126 { 4127 return nenoform_rec(f, negated, cache_, false); 4128 } 4129 4130 bool syntactic_implication(formula f1,formula f2)4131 tl_simplifier::syntactic_implication(formula f1, formula f2) 4132 { 4133 return cache_->syntactic_implication(f1, f2); 4134 } 4135 4136 bool syntactic_implication_neg(formula f1,formula f2,bool right)4137 tl_simplifier::syntactic_implication_neg(formula f1, 4138 formula f2, bool right) 4139 { 4140 return cache_->syntactic_implication_neg(f1, f2, right); 4141 } 4142 4143 bool are_equivalent(formula f,formula g)4144 tl_simplifier::are_equivalent(formula f, formula g) 4145 { 4146 return cache_->lcc.equal(f, g); 4147 } 4148 4149 bool implication(formula f,formula g)4150 tl_simplifier::implication(formula f, formula g) 4151 { 4152 return cache_->lcc.contained(f, g); 4153 } 4154 4155 bdd as_bdd(formula f)4156 tl_simplifier::as_bdd(formula f) 4157 { 4158 return cache_->as_bdd(f); 4159 } 4160 4161 formula star_normal_form(formula f)4162 tl_simplifier::star_normal_form(formula f) 4163 { 4164 return cache_->star_normal_form(f); 4165 } 4166 4167 formula boolean_to_isop(formula f)4168 tl_simplifier::boolean_to_isop(formula f) 4169 { 4170 return cache_->boolean_to_isop(f); 4171 } 4172 4173 bdd_dict_ptr get_dict() const4174 tl_simplifier::get_dict() const 4175 { 4176 return cache_->dict; 4177 } 4178 4179 void print_stats(std::ostream & os) const4180 tl_simplifier::print_stats(std::ostream& os) const 4181 { 4182 cache_->print_stats(os); 4183 } 4184 4185 void clear_as_bdd_cache()4186 tl_simplifier::clear_as_bdd_cache() 4187 { 4188 cache_->clear_as_bdd_cache(); 4189 cache_->lcc.clear(); 4190 } 4191 4192 void clear_caches()4193 tl_simplifier::clear_caches() 4194 { 4195 tl_simplifier_cache* c = 4196 new tl_simplifier_cache(get_dict(), cache_->options); 4197 std::swap(c, cache_); 4198 delete c; 4199 } 4200 } 4201