
18 Oct
2017
18 Oct
'17
2:31 p.m.
Hi Fanda, On Tue, Oct 17, 2017 at 4:27 PM, FrantiĊĦek Blahoudek <fandikb@gmail.com> wrote:
Hi,
I have found out that is_tt and is_ff does nt work as expected in Python. See the attached notebook for details.
formula::is_tt() and formula::is_ff() tests whether the formula (not the language) is tt or ff, but that isn't the case in your notebook, so it seems to be working as expected. class SPOT_API formula final { [...] /// Return the true constant. static formula tt() {...} /// Whether the formula is the true constant. bool is_tt() const {...} [...] For equivalence checks, see https://spot.lrde.epita.fr/tut04.html -- Alexandre Duret-Lutz