alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Compare Boolean LTL formulae using BDDs.

Browse source 
* src/ltlvisit/simplify.cc (syntactic_implication): Here.
This commit is contained in:
Alexandre Duret-Lutz 2011-10-12 11:06:26 +08:00
parent fea49630f6
commit c9a659c8d4
1 changed files with 17 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/ltlvisit/simplify.cc
View file

@ -2754,18 +2754,27 @@ namespace spot
bool result = false; bool result = false;
inf_left_recurse_visitor v1(f2, this); if (f1->is_boolean() && f2->is_boolean())
const_cast<formula*>(f1)->accept(v1);
if (v1.result())
{ {
result = true; bdd l = as_bdd(f1);
bdd r = as_bdd(f2);
result = ((l & r) == l);
} }
else else
{ {
inf_right_recurse_visitor v2(f1, this); inf_left_recurse_visitor v1(f2, this);
const_cast<formula*>(f2)->accept(v2); const_cast<formula*>(f1)->accept(v1);
if (v2.result()) if (v1.result())
result = true; {
result = true;
}
else
{
inf_right_recurse_visitor v2(f1, this);
const_cast<formula*>(f2)->accept(v2);
if (v2.result())
result = true;
}
} }
// Cache result // Cache result