Skip to content
  • Alexandre Duret-Lutz's avatar
    Add trivial identities for &&, <>->, []-> and Boolean arguments. · a2da5184
    Alexandre Duret-Lutz authored
    * src/ltlast/binop.cc (EConcat, UConcat): Rewrite "{b}<>-> f"
    as "b && f", and rewrite "{b}[]->f" as "b->f".
    * src/ltlast/binop.hh (binop::instance): Document trivial
    identities for <>-> and []->.
    * src/ltlast/multop.cc (multop::instance): Rewrite "b1 & b2"
    as "b1 && b2" when b1 and b2 are Boolean.
    (multop::multop): Always disable is.boolean for AndNLM.
    * src/ltlast/multop.hh: Document the rewriting.
    * src/ltltest/equals.cc: Show the two formulas if the exit_code
    is 1, to help debugging.
    * src/ltltest/equals.test: Add more tests.
    * src/ltltest/kind.test: Adjust tests.
    a2da5184