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

Merge the syntactic implication code with ltl_simplifier.

So that we can latter use some combined optimizations.

* src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc: Integrate
the code from syntimpl.cc
* src/ltlvisit/syntimpl.hh, src/ltlvisit/syntimpl.cc: Delete.  All
code has been moved above.
* src/ltlvisit/Makefile.am: Adjust.
* src/ltltest/syntimpl.cc: Adjust code.
parent 3db13a6f
// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Dveloppement
// de l'Epita (LRDE).
// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
// Dveloppement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6
// (LIP6), dpartement Systmes Rpartis Coopratifs (SRC), Universit
// Pierre et Marie Curie.
......@@ -29,7 +29,7 @@
#include "ltlvisit/tunabbrev.hh"
#include "ltlvisit/dump.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/syntimpl.hh"
#include "ltlvisit/simplify.hh"
#include "ltlast/allnodes.hh"
#include "ltlvisit/nenoform.hh"
......@@ -67,8 +67,7 @@ main(int argc, char** argv)
std::string f2s = spot::ltl::to_string(f2);
int exit_return = 0;
spot::ltl::syntactic_implication_cache* c =
new spot::ltl::syntactic_implication_cache;
spot::ltl::ltl_simplifier* c = new spot::ltl::ltl_simplifier;
switch (opt)
{
......
......@@ -42,7 +42,6 @@ ltlvisit_HEADERS = \
reduce.hh \
simpfg.hh \
simplify.hh \
syntimpl.hh \
tostring.hh \
tunabbrev.hh
......@@ -63,6 +62,5 @@ libltlvisit_la_SOURCES = \
reduce.cc \
simpfg.cc \
simplify.cc \
syntimpl.cc \
tostring.cc \
tunabbrev.cc
......@@ -32,7 +32,6 @@
#include "tgba/bdddict.hh"
#include "ltlast/allnodes.hh"
#include "ltlast/visitor.hh"
#include "ltlvisit/syntimpl.hh"
#include "ltlvisit/contain.hh"
#include "ltlvisit/tostring.hh"
#include <cassert>
......@@ -42,6 +41,7 @@ namespace spot
namespace ltl
{
// The name of this class is public, but not its contents.
class ltl_simplifier_cache
{
......@@ -49,10 +49,11 @@ namespace spot
ptr_hash<formula> > f2f_map;
typedef Sgi::hash_map<const formula*, bdd,
ptr_hash<formula> > f2b_map;
typedef std::pair<const formula*, const formula*> pairf;
typedef std::map<pairf, bool> syntimpl_cache_t;
public:
bdd_dict dict;
ltl_simplifier_options options;
syntactic_implication_cache syntimpl;
language_containment_checker lcc;
~ltl_simplifier_cache()
......@@ -86,6 +87,16 @@ namespace spot
old->first->destroy();
}
}
{
syntimpl_cache_t::iterator i = syntimpl_.begin();
syntimpl_cache_t::iterator end = syntimpl_.end();
while (i != end)
{
syntimpl_cache_t::iterator old = i++;
old->first.first->destroy();
old->first.second->destroy();
}
}
dict_.unregister_all_my_variables(this);
}
......@@ -118,7 +129,7 @@ namespace spot
if (f == constant::true_instance())
result = bddtrue;
else if (f == constant::false_instance())
result = bddtrue;
result = bddfalse;
else
assert(!"Unsupported operator");
break;
......@@ -219,16 +230,7 @@ namespace spot
// Return true if f1 => f2 syntactically
bool
syntactic_implication(const formula* f1, const formula* f2)
{
// We cannot run syntactic_implication on SERE formulae,
// except on Boolean formulae.
if (f1->is_sere_formula() && !f1->is_boolean())
return false;
if (f2->is_sere_formula() && !f2->is_boolean())
return false;
return syntimpl.syntactic_implication(f1, f2);
}
syntactic_implication(const formula* f1, const formula* f2);
// Return true if f1 => f2
bool
......@@ -242,30 +244,7 @@ namespace spot
// If right==false, true if !f1 => f2, false otherwise.
// If right==true, true if f1 => !f2, false otherwise.
bool
syntactic_implication_neg(const formula* f1, const formula* f2,
bool right)
{
// We cannot run syntactic_implication_neg on SERE formulae,
// except on Boolean formulae.
if (f1->is_sere_formula() && !f1->is_boolean())
return false;
if (f2->is_sere_formula() && !f2->is_boolean())
return false;
trace << "[SIN] Does " << (right ? "(" : "!(")
<< to_string(f1) << ") implies "
<< (right ? "!(" : "(") << to_string(f2) << ") ?"
<< std::endl;
if (syntimpl.syntactic_implication_neg(f1, f2, right))
{
trace << "[SIN] Yes" << std::endl;
return true;
}
else
{
trace << "[SIN] No" << std::endl;
return false;
}
}
syntactic_implication_neg(const formula* f1, const formula* f2, bool right);
// Return true if f1 => !f2
bool contained_neg(const formula* f1, const formula* f2)
......@@ -350,11 +329,514 @@ namespace spot
f2b_map as_bdd_;
f2f_map simplified_;
f2f_map nenoform_;
syntimpl_cache_t syntimpl_;
};
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);