Skip to content
  • Alexandre Duret-Lutz's avatar
    Introduce AndRat and OrRat operator. · 691119c1
    Alexandre Duret-Lutz authored
    It was a mistake to try to overload And/Or LTL operator for these when
    trivial simplification are performed.  The reason is so simple it is
    embarassing: And(f,1)=f is a trivial identity that should not be
    applied with AndRat.  E.g. AndRat(a;b, 1) is equal to 0, not a;b.
    
    * src/ltlast/multop.hh, src/ltlast/multop.cc: Add the AndRat and OrRat
    operators.
    * src/ltlparse/ltlparse.yy: Build them.
    * src/ltlvisit/mark.cc, src/ltlvisit/simplify.cc,
    src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc,
    src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc,
    src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc:
    Adjust all switches.
    691119c1