Rewrite syntactic implication using a single function.
* src/ltlvisit/simplify.cc (inf_left_recurse_visitor, inf_right_recurse_visitor): Remove. (syntactic_implication, syntactic_implication_aux): Rewrite all rules for syntactic implication. (syntactic_implication_neg): Simplify.
This commit is contained in:
Alexandre Duret-Lutz
parent
7514cc15ee
commit
369ad87e50
1 changed files with 311 additions and 542 deletions
|
|
@ -231,6 +231,8 @@ namespace spot
|
||||||
// Return true if f1 => f2 syntactically
|
// Return true if f1 => f2 syntactically
|
||||||
bool
|
bool
|
||||||
syntactic_implication(const formula* f1, const formula* f2);
|
syntactic_implication(const formula* f1, const formula* f2);
|
||||||
|
bool
|
||||||
|
syntactic_implication_aux(const formula* f1, const formula* f2);
|
||||||
|
|
||||||
// Return true if f1 => f2
|
// Return true if f1 => f2
|
||||||
bool
|
bool
|
||||||
|
|
@ -336,508 +338,6 @@ namespace spot
|
||||||
|
|
||||||
namespace
|
namespace
|
||||||
{
|
{
|
||||||
// Check if f implies the visited formula.
|
|
||||||
class inf_right_recurse_visitor: public const_visitor
|
|
||||||
{
|
|
||||||
public:
|
|
||||||
|
|
||||||
inf_right_recurse_visitor(const formula *f,
|
|
||||||
ltl_simplifier_cache* c)
|
|
||||||
: result_(false), f(f), c(c)
|
|
||||||
{
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual
|
|
||||||
~inf_right_recurse_visitor()
|
|
||||||
{
|
|
||||||
}
|
|
||||||
|
|
||||||
int
|
|
||||||
result() const
|
|
||||||
{
|
|
||||||
return result_;
|
|
||||||
}
|
|
||||||
|
|
||||||
void
|
|
||||||
visit(const atomic_prop* ap)
|
|
||||||
{
|
|
||||||
if (f == ap)
|
|
||||||
result_ = true;
|
|
||||||
}
|
|
||||||
|
|
||||||
void
|
|
||||||
visit(const constant* c)
|
|
||||||
{
|
|
||||||
switch (c->val())
|
|
||||||
{
|
|
||||||
case constant::True:
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
case constant::False:
|
|
||||||
result_ = false;
|
|
||||||
return;
|
|
||||||
case constant::EmptyWord:
|
|
||||||
result_ = false;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void
|
|
||||||
visit(const bunop*)
|
|
||||||
{
|
|
||||||
}
|
|
||||||
|
|
||||||
void
|
|
||||||
visit(const unop* uo)
|
|
||||||
{
|
|
||||||
const formula* f1 = uo->child();
|
|
||||||
switch (uo->op())
|
|
||||||
{
|
|
||||||
case unop::Not:
|
|
||||||
// !f1 => !f1
|
|
||||||
if (uo == f)
|
|
||||||
{
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
// !a => !f1 if f1 => a
|
|
||||||
if (f->kind() == formula::UnOp)
|
|
||||||
{
|
|
||||||
const unop* op = static_cast<const unop*>(f);
|
|
||||||
if (op->op() == unop::Not)
|
|
||||||
result_ = c->syntactic_implication(f1, op->child());
|
|
||||||
}
|
|
||||||
return;
|
|
||||||
case unop::X:
|
|
||||||
{
|
|
||||||
if (f->kind() != formula::UnOp)
|
|
||||||
return;
|
|
||||||
const unop* op = static_cast<const unop*>(f);
|
|
||||||
if (op->op() == unop::X)
|
|
||||||
result_ = c->syntactic_implication(op->child(), f1);
|
|
||||||
}
|
|
||||||
return;
|
|
||||||
case unop::F:
|
|
||||||
// f => F(f1) if f => f1
|
|
||||||
result_ = c->syntactic_implication(f, f1);
|
|
||||||
return;
|
|
||||||
case unop::G:
|
|
||||||
/* G(a) = false R a */
|
|
||||||
if (c->syntactic_implication(f, constant::false_instance()))
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
case unop::Finish:
|
|
||||||
case unop::Closure:
|
|
||||||
case unop::NegClosure:
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
/* Unreachable code. */
|
|
||||||
assert(0);
|
|
||||||
}
|
|
||||||
|
|
||||||
void
|
|
||||||
visit(const binop* bo)
|
|
||||||
{
|
|
||||||
const formula* f1 = bo->first();
|
|
||||||
const formula* f2 = bo->second();
|
|
||||||
switch (bo->op())
|
|
||||||
{
|
|
||||||
case binop::Xor:
|
|
||||||
case binop::Equiv:
|
|
||||||
case binop::Implies:
|
|
||||||
case binop::UConcat:
|
|
||||||
case binop::EConcat:
|
|
||||||
case binop::EConcatMarked:
|
|
||||||
return;
|
|
||||||
case binop::U:
|
|
||||||
case binop::W:
|
|
||||||
if (c->syntactic_implication(f, f2))
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
case binop::R:
|
|
||||||
if (f->kind() == formula::BinOp)
|
|
||||||
{
|
|
||||||
const binop* fb = static_cast<const binop*>(f);
|
|
||||||
if (fb->op() == binop::R
|
|
||||||
&& c->syntactic_implication(fb->first(), f1)
|
|
||||||
&& c->syntactic_implication(fb->second(), f2))
|
|
||||||
{
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (f->kind() == formula::UnOp)
|
|
||||||
{
|
|
||||||
const unop* fu = static_cast<const unop*>(f);
|
|
||||||
if (fu->op() == unop::G
|
|
||||||
&& f1 == constant::false_instance()
|
|
||||||
&& c->syntactic_implication(fu->child(), f2))
|
|
||||||
{
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (c->syntactic_implication(f, f1)
|
|
||||||
&& c->syntactic_implication(f, f2))
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
case binop::M:
|
|
||||||
if (f->kind() == formula::BinOp)
|
|
||||||
{
|
|
||||||
const binop* fb = static_cast<const binop*>(f);
|
|
||||||
if (fb->op() == binop::M
|
|
||||||
&& c->syntactic_implication(fb->first(), f1)
|
|
||||||
&& c->syntactic_implication(fb->second(), f2))
|
|
||||||
{
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (f->kind() == formula::UnOp)
|
|
||||||
{
|
|
||||||
const unop* fu = static_cast<const unop*>(f);
|
|
||||||
if (fu->op() == unop::F
|
|
||||||
&& f2 == constant::true_instance()
|
|
||||||
&& c->syntactic_implication(fu->child(), f1))
|
|
||||||
{
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (c->syntactic_implication(f, f1)
|
|
||||||
&& c->syntactic_implication(f, f2))
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
/* Unreachable code. */
|
|
||||||
assert(0);
|
|
||||||
}
|
|
||||||
|
|
||||||
void
|
|
||||||
visit(const automatop*)
|
|
||||||
{
|
|
||||||
assert(0);
|
|
||||||
}
|
|
||||||
|
|
||||||
void
|
|
||||||
visit(const multop* mo)
|
|
||||||
{
|
|
||||||
multop::type op = mo->op();
|
|
||||||
unsigned mos = mo->size();
|
|
||||||
switch (op)
|
|
||||||
{
|
|
||||||
case multop::And:
|
|
||||||
for (unsigned i = 0; i < mos; ++i)
|
|
||||||
if (!c->syntactic_implication(f, mo->nth(i)))
|
|
||||||
return;
|
|
||||||
result_ = true;
|
|
||||||
break;
|
|
||||||
case multop::Or:
|
|
||||||
for (unsigned i = 0; i < mos && !result_; ++i)
|
|
||||||
if (c->syntactic_implication(f, mo->nth(i)))
|
|
||||||
result_ = true;
|
|
||||||
break;
|
|
||||||
case multop::Concat:
|
|
||||||
case multop::Fusion:
|
|
||||||
case multop::AndNLM:
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
protected:
|
|
||||||
bool result_; /* true if f < f1, false otherwise. */
|
|
||||||
const formula* f;
|
|
||||||
ltl_simplifier_cache* c;
|
|
||||||
};
|
|
||||||
|
|
||||||
/////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
// Check if the visited formula implies f.
|
|
||||||
class inf_left_recurse_visitor: public const_visitor
|
|
||||||
{
|
|
||||||
public:
|
|
||||||
|
|
||||||
inf_left_recurse_visitor(const formula *f,
|
|
||||||
ltl_simplifier_cache* c)
|
|
||||||
: result_(false), f(f), c(c)
|
|
||||||
{
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual
|
|
||||||
~inf_left_recurse_visitor()
|
|
||||||
{
|
|
||||||
}
|
|
||||||
|
|
||||||
bool
|
|
||||||
special_case(const binop* f2)
|
|
||||||
{
|
|
||||||
if (f->kind() != formula::BinOp)
|
|
||||||
return false;
|
|
||||||
const binop* fb = static_cast<const binop*>(f);
|
|
||||||
if (fb->op() == f2->op()
|
|
||||||
&& c->syntactic_implication(f2->first(), fb->first())
|
|
||||||
&& c->syntactic_implication(f2->second(), fb->second()))
|
|
||||||
return true;
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
|
|
||||||
bool
|
|
||||||
special_case_check(const formula* f2)
|
|
||||||
{
|
|
||||||
if (f2->kind() != formula::BinOp)
|
|
||||||
return false;
|
|
||||||
return special_case(static_cast<const binop*>(f2));
|
|
||||||
}
|
|
||||||
|
|
||||||
int
|
|
||||||
result() const
|
|
||||||
{
|
|
||||||
return result_;
|
|
||||||
}
|
|
||||||
|
|
||||||
void
|
|
||||||
visit(const atomic_prop* ap)
|
|
||||||
{
|
|
||||||
inf_right_recurse_visitor v(ap, c);
|
|
||||||
const_cast<formula*>(f)->accept(v);
|
|
||||||
result_ = v.result();
|
|
||||||
}
|
|
||||||
|
|
||||||
void
|
|
||||||
visit(const bunop*)
|
|
||||||
{
|
|
||||||
}
|
|
||||||
|
|
||||||
void
|
|
||||||
visit(const constant* cst)
|
|
||||||
{
|
|
||||||
inf_right_recurse_visitor v(cst, c);
|
|
||||||
switch (cst->val())
|
|
||||||
{
|
|
||||||
case constant::True:
|
|
||||||
const_cast<formula*>(f)->accept(v);
|
|
||||||
result_ = v.result();
|
|
||||||
return;
|
|
||||||
case constant::False:
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
case constant::EmptyWord:
|
|
||||||
result_ = true; // FIXME
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
/* Unreachable code. */
|
|
||||||
assert(0);
|
|
||||||
}
|
|
||||||
|
|
||||||
void
|
|
||||||
visit(const unop* uo)
|
|
||||||
{
|
|
||||||
const formula* f1 = uo->child();
|
|
||||||
inf_right_recurse_visitor v(uo, c);
|
|
||||||
switch (uo->op())
|
|
||||||
{
|
|
||||||
case unop::Not:
|
|
||||||
if (uo == f)
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
case unop::X:
|
|
||||||
if (f->kind() == formula::UnOp)
|
|
||||||
{
|
|
||||||
const unop* op = static_cast<const unop*>(f);
|
|
||||||
if (op->op() == unop::X)
|
|
||||||
result_ = c->syntactic_implication(f1, op->child());
|
|
||||||
}
|
|
||||||
return;
|
|
||||||
case unop::F:
|
|
||||||
{
|
|
||||||
/* F(a) = true U a */
|
|
||||||
const formula* tmp = binop::instance(binop::U,
|
|
||||||
constant::true_instance(),
|
|
||||||
f1->clone());
|
|
||||||
if (special_case_check(tmp))
|
|
||||||
{
|
|
||||||
result_ = true;
|
|
||||||
tmp->destroy();
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
if (c->syntactic_implication(tmp, f))
|
|
||||||
result_ = true;
|
|
||||||
tmp->destroy();
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
case unop::G:
|
|
||||||
{
|
|
||||||
/* G(a) = false R a */
|
|
||||||
const formula* tmp = binop::instance(binop::R,
|
|
||||||
constant::false_instance(),
|
|
||||||
f1->clone());
|
|
||||||
if (special_case_check(tmp))
|
|
||||||
{
|
|
||||||
result_ = true;
|
|
||||||
tmp->destroy();
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
if (c->syntactic_implication(tmp, f))
|
|
||||||
result_ = true;
|
|
||||||
tmp->destroy();
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
case unop::Finish:
|
|
||||||
case unop::Closure:
|
|
||||||
case unop::NegClosure:
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
/* Unreachable code. */
|
|
||||||
assert(0);
|
|
||||||
}
|
|
||||||
|
|
||||||
void
|
|
||||||
visit(const binop* bo)
|
|
||||||
{
|
|
||||||
if (special_case(bo))
|
|
||||||
{
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
|
|
||||||
const formula* f1 = bo->first();
|
|
||||||
const formula* f2 = bo->second();
|
|
||||||
switch (bo->op())
|
|
||||||
{
|
|
||||||
case binop::Xor:
|
|
||||||
case binop::Equiv:
|
|
||||||
case binop::Implies:
|
|
||||||
case binop::UConcat:
|
|
||||||
case binop::EConcat:
|
|
||||||
case binop::EConcatMarked:
|
|
||||||
return;
|
|
||||||
case binop::U:
|
|
||||||
/* (a < c) && (c < d) => a U b < c U d */
|
|
||||||
if (f->kind() == formula::BinOp)
|
|
||||||
{
|
|
||||||
const binop* fb = static_cast<const binop*>(f);
|
|
||||||
if (fb->op() == binop::U
|
|
||||||
&& c->syntactic_implication(f1, fb->first())
|
|
||||||
&& c->syntactic_implication(f2, fb->second()))
|
|
||||||
{
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (f->kind() == formula::UnOp)
|
|
||||||
{
|
|
||||||
const unop* fu = static_cast<const unop*>(f);
|
|
||||||
if (fu->op() == unop::F
|
|
||||||
&& f1 == constant::true_instance()
|
|
||||||
&& c->syntactic_implication(f2, fu->child()))
|
|
||||||
{
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (c->syntactic_implication(f1, f)
|
|
||||||
&& c->syntactic_implication(f2, f))
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
case binop::W:
|
|
||||||
/* (a < c) && (c < d) => a W b < c W d */
|
|
||||||
if (f->kind() == formula::BinOp)
|
|
||||||
{
|
|
||||||
const binop* fb = static_cast<const binop*>(f);
|
|
||||||
if (fb->op() == binop::W
|
|
||||||
&& c->syntactic_implication(f1, fb->first())
|
|
||||||
&& c->syntactic_implication(f2, fb->second()))
|
|
||||||
{
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (f->kind() == formula::UnOp)
|
|
||||||
{
|
|
||||||
const unop* fu = static_cast<const unop*>(f);
|
|
||||||
if (fu && fu->op() == unop::G
|
|
||||||
&& f2 == constant::false_instance()
|
|
||||||
&& c->syntactic_implication(f1, fu->child()))
|
|
||||||
{
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (c->syntactic_implication(f1, f)
|
|
||||||
&& c->syntactic_implication(f2, f))
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
case binop::R:
|
|
||||||
if (f->kind() == formula::UnOp)
|
|
||||||
{
|
|
||||||
const unop* fu = static_cast<const unop*>(f);
|
|
||||||
if (fu->op() == unop::G
|
|
||||||
&& f1 == constant::false_instance()
|
|
||||||
&& c->syntactic_implication(f2, fu->child()))
|
|
||||||
{
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (c->syntactic_implication(f2, f))
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
case binop::M:
|
|
||||||
if (f->kind() == formula::UnOp)
|
|
||||||
{
|
|
||||||
const unop* fu = static_cast<const unop*>(f);
|
|
||||||
if (fu->op() == unop::F
|
|
||||||
&& f2 == constant::true_instance()
|
|
||||||
&& c->syntactic_implication(f1, fu->child()))
|
|
||||||
{
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (c->syntactic_implication(f2, f))
|
|
||||||
result_ = true;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
/* Unreachable code. */
|
|
||||||
assert(0);
|
|
||||||
}
|
|
||||||
|
|
||||||
void
|
|
||||||
visit(const automatop*)
|
|
||||||
{
|
|
||||||
assert(0);
|
|
||||||
}
|
|
||||||
|
|
||||||
void
|
|
||||||
visit(const multop* mo)
|
|
||||||
{
|
|
||||||
multop::type op = mo->op();
|
|
||||||
unsigned mos = mo->size();
|
|
||||||
switch (op)
|
|
||||||
{
|
|
||||||
case multop::And:
|
|
||||||
for (unsigned i = 0; (i < mos) && !result_; ++i)
|
|
||||||
if (c->syntactic_implication(mo->nth(i), f))
|
|
||||||
result_ = true;
|
|
||||||
break;
|
|
||||||
case multop::Or:
|
|
||||||
for (unsigned i = 0; i < mos; ++i)
|
|
||||||
if (!c->syntactic_implication(mo->nth(i), f))
|
|
||||||
return;
|
|
||||||
result_ = true;
|
|
||||||
break;
|
|
||||||
case multop::Concat:
|
|
||||||
case multop::Fusion:
|
|
||||||
case multop::AndNLM:
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
protected:
|
|
||||||
bool result_; /* true if f1 < f, 1 otherwise. */
|
|
||||||
const formula* f;
|
|
||||||
ltl_simplifier_cache* c;
|
|
||||||
};
|
|
||||||
|
|
||||||
//////////////////////////////////////////////////////////////////////
|
//////////////////////////////////////////////////////////////////////
|
||||||
//
|
//
|
||||||
// NEGATIVE_NORMAL_FORM_VISITOR
|
// NEGATIVE_NORMAL_FORM_VISITOR
|
||||||
|
|
@ -2727,61 +2227,336 @@ namespace spot
|
||||||
// ltl_simplifier_cache
|
// ltl_simplifier_cache
|
||||||
|
|
||||||
|
|
||||||
// Return true if f1 => f2 syntactically
|
// This implements the recursive rules for syntactic implication.
|
||||||
|
// (To follow this code please look at the table given as an
|
||||||
|
// appendix in the documentation for temporal logic operators.)
|
||||||
|
inline
|
||||||
bool
|
bool
|
||||||
ltl_simplifier_cache::syntactic_implication(const formula* f1,
|
ltl_simplifier_cache::syntactic_implication_aux(const formula* f,
|
||||||
const formula* f2)
|
const formula* g)
|
||||||
|
{
|
||||||
|
formula::opkind fk = f->kind();
|
||||||
|
formula::opkind gk = g->kind();
|
||||||
|
|
||||||
|
// Deal with all lines except the first one.
|
||||||
|
switch (fk)
|
||||||
|
{
|
||||||
|
case formula::Constant:
|
||||||
|
case formula::AtomicProp:
|
||||||
|
case formula::BUnOp:
|
||||||
|
case formula::AutomatOp:
|
||||||
|
break;
|
||||||
|
|
||||||
|
case formula::UnOp:
|
||||||
|
{
|
||||||
|
const unop* f_ = down_cast<const unop*>(f);
|
||||||
|
unop::type fo = f_->op();
|
||||||
|
|
||||||
|
if (gk == formula::UnOp)
|
||||||
|
{
|
||||||
|
const unop* g_ = down_cast<const unop*>(g);
|
||||||
|
unop::type go = g_->op();
|
||||||
|
if (fo == unop::F)
|
||||||
|
{
|
||||||
|
if ((go == unop::F)
|
||||||
|
&& syntactic_implication(f_->child(), g_->child()))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else if (fo == unop::G)
|
||||||
|
{
|
||||||
|
if ((go == unop::G || go == unop::X)
|
||||||
|
&& syntactic_implication(f_->child(), g_->child()))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else if (fo == unop::X)
|
||||||
|
{
|
||||||
|
if ((go == unop::F || go == unop::X)
|
||||||
|
&& syntactic_implication(f_->child(), g_->child()))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else if (gk == formula::BinOp && fo == unop::G)
|
||||||
|
{
|
||||||
|
const binop* g_ = down_cast<const binop*>(g);
|
||||||
|
binop::type go = g_->op();
|
||||||
|
const formula* g1 = g_->first();
|
||||||
|
const formula* g2 = g_->second();
|
||||||
|
if ((go == binop::U || go == binop::R)
|
||||||
|
&& syntactic_implication(f_->child(), g2))
|
||||||
|
return true;
|
||||||
|
else if (go == binop::W
|
||||||
|
&& (syntactic_implication(f_->child(), g1)
|
||||||
|
|| syntactic_implication(f_->child(), g2)))
|
||||||
|
return true;
|
||||||
|
else if (go == binop::M
|
||||||
|
&& (syntactic_implication(f_->child(), g1)
|
||||||
|
&& syntactic_implication(f_->child(), g2)))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
// First column.
|
||||||
|
if (fo == unop::G && syntactic_implication(f_->child(), g))
|
||||||
|
return true;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
|
||||||
|
case formula::BinOp:
|
||||||
|
{
|
||||||
|
const binop* f_ = down_cast<const binop*>(f);
|
||||||
|
binop::type fo = f_->op();
|
||||||
|
const formula* f1 = f_->first();
|
||||||
|
const formula* f2 = f_->second();
|
||||||
|
|
||||||
|
if (gk == formula::UnOp)
|
||||||
|
{
|
||||||
|
const unop* g_ = down_cast<const unop*>(g);
|
||||||
|
unop::type go = g_->op();
|
||||||
|
if (go == unop::F)
|
||||||
|
{
|
||||||
|
if (fo == binop::U)
|
||||||
|
{
|
||||||
|
if (syntactic_implication(f2, g_->child()))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else if (fo == binop::W)
|
||||||
|
{
|
||||||
|
if (syntactic_implication(f1, g_->child())
|
||||||
|
&& syntactic_implication(f2, g_->child()))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else if (fo == binop::R)
|
||||||
|
{
|
||||||
|
if (syntactic_implication(f2, g_->child()))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else if (fo == binop::M)
|
||||||
|
{
|
||||||
|
if (syntactic_implication(f1, g_->child())
|
||||||
|
|| syntactic_implication(f2, g_->child()))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
else if (gk == formula::BinOp)
|
||||||
|
{
|
||||||
|
const binop* g_ = down_cast<const binop*>(g);
|
||||||
|
binop::type go = g_->op();
|
||||||
|
const formula* g1 = g_->first();
|
||||||
|
const formula* g2 = g_->second();
|
||||||
|
|
||||||
|
if ((fo == binop::U && (go == binop::U || go == binop::W))
|
||||||
|
|| (fo == binop::W && go == binop::W)
|
||||||
|
|| (fo == binop::R && go == binop::R)
|
||||||
|
|| (fo == binop::M && (go == binop::R || go == binop::M)))
|
||||||
|
{
|
||||||
|
if (syntactic_implication(f1, g1)
|
||||||
|
&& syntactic_implication(f2, g2))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else if (fo == binop::W && go == binop::U)
|
||||||
|
{
|
||||||
|
if (syntactic_implication(f1, g2)
|
||||||
|
&& syntactic_implication(f2, g2))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else if (fo == binop::R && go == binop::M)
|
||||||
|
{
|
||||||
|
if (syntactic_implication(f2, g1)
|
||||||
|
&& syntactic_implication(f2, g2))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else if ((fo == binop::U && (go == binop::R || go == binop::M))
|
||||||
|
|| (fo == binop::W && go == binop::R))
|
||||||
|
{
|
||||||
|
if (syntactic_implication(f1, g1)
|
||||||
|
&& syntactic_implication(f2, g1)
|
||||||
|
&& syntactic_implication(f2, g2))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else if ((fo == binop::M && (go == binop::U || go == binop::W))
|
||||||
|
|| (fo == binop::R && go == binop::W))
|
||||||
|
{
|
||||||
|
if (syntactic_implication(f1, g2)
|
||||||
|
&& syntactic_implication(f2, g1))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// First column.
|
||||||
|
if (fo == binop::U || fo == binop::W)
|
||||||
|
{
|
||||||
|
if (syntactic_implication(f1, g)
|
||||||
|
&& syntactic_implication(f2, g))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else if (fo == binop::R || fo == binop::M)
|
||||||
|
{
|
||||||
|
if (syntactic_implication(f2, g))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
case formula::MultOp:
|
||||||
|
{
|
||||||
|
const multop* f_ = down_cast<const multop*>(f);
|
||||||
|
multop::type fo = f_->op();
|
||||||
|
unsigned fs = f_->size();
|
||||||
|
|
||||||
|
// First column.
|
||||||
|
switch (fo)
|
||||||
|
{
|
||||||
|
case multop::Or:
|
||||||
|
{
|
||||||
|
bool b = true;
|
||||||
|
for (unsigned i = 0; i < fs; ++i)
|
||||||
|
if (!syntactic_implication(f_->nth(i), g))
|
||||||
|
{
|
||||||
|
b &= false;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
if (b)
|
||||||
|
return true;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
case multop::And:
|
||||||
|
{
|
||||||
|
for (unsigned i = 0; i < fs; ++i)
|
||||||
|
if (syntactic_implication(f_->nth(i), g))
|
||||||
|
return true;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
case multop::Concat:
|
||||||
|
case multop::Fusion:
|
||||||
|
case multop::AndNLM:
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// First line.
|
||||||
|
switch (gk)
|
||||||
|
{
|
||||||
|
case formula::Constant:
|
||||||
|
case formula::AtomicProp:
|
||||||
|
case formula::BUnOp:
|
||||||
|
case formula::AutomatOp:
|
||||||
|
break;
|
||||||
|
|
||||||
|
case formula::UnOp:
|
||||||
|
{
|
||||||
|
const unop* g_ = down_cast<const unop*>(g);
|
||||||
|
unop::type go = g_->op();
|
||||||
|
if (go == unop::F)
|
||||||
|
{
|
||||||
|
if (syntactic_implication(f, g_->child()))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
case formula::BinOp:
|
||||||
|
{
|
||||||
|
const binop* g_ = down_cast<const binop*>(g);
|
||||||
|
binop::type go = g_->op();
|
||||||
|
const formula* g1 = g_->first();
|
||||||
|
const formula* g2 = g_->second();
|
||||||
|
|
||||||
|
if (go == binop::U || go == binop::W)
|
||||||
|
{
|
||||||
|
if (syntactic_implication(f, g2))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else if (go == binop::M || go == binop::R)
|
||||||
|
{
|
||||||
|
if (syntactic_implication(f, g1)
|
||||||
|
&& syntactic_implication(f, g2))
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
case formula::MultOp:
|
||||||
|
{
|
||||||
|
const multop* g_ = down_cast<const multop*>(g);
|
||||||
|
multop::type go = g_->op();
|
||||||
|
unsigned gs = g_->size();
|
||||||
|
|
||||||
|
switch (go)
|
||||||
|
{
|
||||||
|
case multop::And:
|
||||||
|
{
|
||||||
|
bool b = true;
|
||||||
|
for (unsigned i = 0; i < gs; ++i)
|
||||||
|
if (!syntactic_implication(f, g_->nth(i)))
|
||||||
|
{
|
||||||
|
b &= false;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
if (b)
|
||||||
|
return true;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
case multop::Or:
|
||||||
|
{
|
||||||
|
for (unsigned i = 0; i < gs; ++i)
|
||||||
|
if (syntactic_implication(f, g_->nth(i)))
|
||||||
|
return true;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
case multop::Concat:
|
||||||
|
case multop::Fusion:
|
||||||
|
case multop::AndNLM:
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
|
||||||
|
// Return true if f => g syntactically
|
||||||
|
bool
|
||||||
|
ltl_simplifier_cache::syntactic_implication(const formula* f,
|
||||||
|
const formula* g)
|
||||||
{
|
{
|
||||||
// We cannot run syntactic_implication on SERE formulae,
|
// We cannot run syntactic_implication on SERE formulae,
|
||||||
// except on Boolean formulae.
|
// except on Boolean formulae.
|
||||||
if (f1->is_sere_formula() && !f1->is_boolean())
|
if (f->is_sere_formula() && !f->is_boolean())
|
||||||
return false;
|
return false;
|
||||||
if (f2->is_sere_formula() && !f2->is_boolean())
|
if (g->is_sere_formula() && !g->is_boolean())
|
||||||
return false;
|
return false;
|
||||||
|
|
||||||
if (f1 == f2)
|
if (f == g)
|
||||||
return true;
|
return true;
|
||||||
if (f2 == constant::true_instance()
|
if (g == constant::true_instance()
|
||||||
|| f1 == constant::false_instance())
|
|| f == constant::false_instance())
|
||||||
return true;
|
return true;
|
||||||
|
|
||||||
// Cache lookup
|
// Cache lookup
|
||||||
{
|
{
|
||||||
pairf p(f1, f2);
|
pairf p(f, g);
|
||||||
syntimpl_cache_t::const_iterator i = syntimpl_.find(p);
|
syntimpl_cache_t::const_iterator i = syntimpl_.find(p);
|
||||||
if (i != syntimpl_.end())
|
if (i != syntimpl_.end())
|
||||||
return i->second;
|
return i->second;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool result = false;
|
bool result;
|
||||||
|
|
||||||
if (f1->is_boolean() && f2->is_boolean())
|
if (f->is_boolean() && g->is_boolean())
|
||||||
{
|
{
|
||||||
bdd l = as_bdd(f1);
|
bdd l = as_bdd(f);
|
||||||
bdd r = as_bdd(f2);
|
bdd r = as_bdd(g);
|
||||||
result = ((l & r) == l);
|
result = ((l & r) == l);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
inf_left_recurse_visitor v1(f2, this);
|
result = syntactic_implication_aux(f, g);
|
||||||
const_cast<formula*>(f1)->accept(v1);
|
|
||||||
if (v1.result())
|
|
||||||
{
|
|
||||||
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
|
||||||
{
|
{
|
||||||
pairf p(f1->clone(), f2->clone());
|
pairf p(f->clone(), g->clone());
|
||||||
syntimpl_[p] = result;
|
syntimpl_[p] = result;
|
||||||
|
// std::cerr << to_string(f) << (result ? " ==> " : " =/=> ")
|
||||||
|
// << to_string(g) << std::endl;
|
||||||
}
|
}
|
||||||
|
|
||||||
return result;
|
return result;
|
||||||
|
|
@ -2801,22 +2576,16 @@ namespace spot
|
||||||
if (f2->is_sere_formula() && !f2->is_boolean())
|
if (f2->is_sere_formula() && !f2->is_boolean())
|
||||||
return false;
|
return false;
|
||||||
|
|
||||||
const formula* l = f1->clone();
|
|
||||||
const formula* r = f2->clone();
|
|
||||||
if (right)
|
if (right)
|
||||||
{
|
f2 = nenoform_recursively(f2, true, this);
|
||||||
const formula* old = r;
|
|
||||||
r = nenoform_recursively(r, true, this);
|
|
||||||
old->destroy();
|
|
||||||
}
|
|
||||||
else
|
else
|
||||||
{
|
f1 = nenoform_recursively(f1, true, this);
|
||||||
const formula* old = l;
|
|
||||||
l = nenoform_recursively(l, true, this);
|
|
||||||
old->destroy();
|
|
||||||
}
|
|
||||||
|
|
||||||
return syntactic_implication(l, r);
|
bool result = syntactic_implication(f1, f2);
|
||||||
|
|
||||||
|
(right ? f2 : f1)->destroy();
|
||||||
|
|
||||||
|
return result;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue