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

formula: introduce one_plus(), and saturate predefined formulas

Browse source 
* spot/tl/formula.hh, spot/tl/formula.cc (one_plus): New.
(fnode): Add a saturated argument.
(tt_, ff_, eword_, one_plus, one_star): Create saturated node.
(destroy): Do not check for id() < 3.
This commit is contained in:
Alexandre Duret-Lutz 2022-12-08 11:51:07 +01:00
parent 4629d074ab
commit 8ed9e3381f
2 changed files with 44 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

21
spot/tl/formula.cc
View file

@ -660,6 +660,16 @@ namespace spot
switch (o)
{
case op::Star:
if (max == unbounded() && child == tt_)
{
// bypass normal construction: 1[*] and 1[+] are
// frequently used, so they are not reference counted.
if (min == 0)
return one_star();
if (min == 1)
return one_plus();
}
neutral = eword();
break;
case op::FStar:
@ -810,7 +820,7 @@ namespace spot
return tt();
// ![*0] = 1[+]
if (f->is_eword())
return bunop(op::Star, tt(), 1);
return one_plus();
auto fop = f->kind();
// "Not" is an involution.
@ -1138,10 +1148,11 @@ namespace spot
return id;
}
const fnode* fnode::ff_ = new fnode(op::ff, {});
const fnode* fnode::tt_ = new fnode(op::tt, {});
const fnode* fnode::ew_ = new fnode(op::eword, {});
const fnode* fnode::ff_ = new fnode(op::ff, {}, true);
const fnode* fnode::tt_ = new fnode(op::tt, {}, true);
const fnode* fnode::ew_ = new fnode(op::eword, {}, true);
const fnode* fnode::one_star_ = nullptr; // Only built when necessary.
const fnode* fnode::one_plus_ = nullptr; // Only built when necessary.
void fnode::setup_props(op o)
{
@ -1817,7 +1828,7 @@ namespace spot
{
unsigned cnt = 0;
for (auto i: m.uniq)
if (i->id() > 3 && i != one_star_)
if (!i->saturated_)
{
if (!cnt++)
std::cerr << "*** m.uniq is not empty ***\n";

37
spot/tl/formula.hh
View file

@ -149,7 +149,7 @@ namespace spot
{
if (SPOT_LIKELY(refs_))
--refs_;
else if (SPOT_LIKELY(id_ > 2) && SPOT_LIKELY(!saturated_))
else if (SPOT_LIKELY(!saturated_))
// last reference to a node that is not a constant
destroy_aux();
}
@ -351,10 +351,18 @@ namespace spot
static const fnode* one_star()
{
if (!one_star_)
one_star_ = bunop(op::Star, tt(), 0);
one_star_ = new fnode(op::Star, tt_, 0, unbounded(), true);
return one_star_;
}
/// \see formula::one_plus
static const fnode* one_plus()
{
if (!one_plus_)
one_plus_ = new fnode(op::Star, tt_, 1, unbounded(), true);
return one_plus_;
}
/// \see formula::ap_name
const std::string& ap_name() const;
@ -536,7 +544,7 @@ namespace spot
template<class iter>
fnode(op o, iter begin, iter end)
fnode(op o, iter begin, iter end, bool saturated = false)
// Clang has some optimization where is it able to combine the
// 4 movb initializing op_,min_,max_,saturated_ into a single
// movl. Also it can optimize the three byte-comparisons of
@ -551,7 +559,7 @@ namespace spot
#if __llvm__
min_(0), max_(0),
#endif
saturated_(0)
saturated_(saturated)
{
size_t s = std::distance(begin, end);
if (SPOT_UNLIKELY(s > (size_t) UINT16_MAX))
@ -563,13 +571,15 @@ namespace spot
setup_props(o);
}
fnode(op o, std::initializer_list<const fnode*> l)
: fnode(o, l.begin(), l.end())
fnode(op o, std::initializer_list<const fnode*> l,
bool saturated = false)
: fnode(o, l.begin(), l.end(), saturated)
{
}
fnode(op o, const fnode* f, uint8_t min, uint8_t max)
: op_(o), min_(min), max_(max), saturated_(0), size_(1)
fnode(op o, const fnode* f, uint8_t min, uint8_t max,
bool saturated = false)
: op_(o), min_(min), max_(max), saturated_(saturated), size_(1)
{
children[0] = f;
setup_props(o);
@ -579,6 +589,7 @@ namespace spot
static const fnode* tt_;
static const fnode* ew_;
static const fnode* one_star_;
static const fnode* one_plus_;
op op_; // operator
uint8_t min_; // range minimum (for star-like operators)
@ -1552,7 +1563,15 @@ namespace spot
/// \brief Return a copy of the formula 1[*].
static formula one_star()
{
return formula(fnode::one_star()->clone());
// no need to clone, 1[*] is not reference counted
return formula(fnode::one_star());
}
/// \brief Return a copy of the formula 1[+].
static formula one_plus()
{
// no need to clone, 1[+] is not reference counted
return formula(fnode::one_plus());
}
/// \brief Whether the formula is an atomic proposition or its