Skip to content

ltlsynt implement polarity and gequiv after decomposition too

Alexandre Duret-Lutz requested to merge adl/ltlsynt-polarized-decomposition into next
  • bin/ltlsynt.cc: Also simplify subformulas using polarity and global equivalence. Add support for --polarity=before-decompose and --global-equiv=before-decompose to restablish the previous behavior.
  • spot/tl/apcollect.hh, spot/tl/apcollect.cc (realizability_simplifier::merge_mapping): New method.
  • tests/core/ltlsynt.test: Add new test cases.

Merge request reports