Commit c2335edb authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Remove the negative_normal_form call from reduce().

* src/ltlvisit/simplify.cc (ltl_simplifier::simplify):
Convert in negative normal form if needed.
* src/ltlvisit/reduce.cc (reduce): Do not call
negative_normal_form().
parent 1087c623
......@@ -27,7 +27,6 @@
#include "lunabbrev.hh"
#include "simpfg.hh"
#include "nenoform.hh"
#include "simplify.hh"
namespace spot
......@@ -68,10 +67,6 @@ namespace spot
f1 = unabbreviate_logic(f);
f2 = simplify_f_g(f1);
f1->destroy();
f1 = negative_normal_form(f2);
f2->destroy();
f2 = f1;
f = simplifier.simplify(f2);
f2->destroy();
}
......
......@@ -2222,7 +2222,13 @@ namespace spot
formula*
ltl_simplifier::simplify(const formula* f)
{
return const_cast<formula*>(simplify_recursively(f, cache_));
formula* neno = 0;
if (!f->is_in_nenoform())
f = neno = negative_normal_form(f);
formula* res = const_cast<formula*>(simplify_recursively(f, cache_));
if (neno)
neno->destroy();
return res;
}
formula*
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment