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

Improve aiger INF encoding

Browse source 
the encoding cna be simplified to produce less gates
when high or low is True.

* spot/twaalgos/aiger.cc: Here
* tests/python/_synthesis.ipynb: Test
This commit is contained in:
Philipp Schlehuber-Caissier 2022-09-21 17:27:58 +02:00
parent c1c874b1a5
commit c63c1796b9
2 changed files with 454 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

33
spot/twaalgos/aiger.cc
View file

@ -637,19 +637,44 @@ namespace spot
// De-morgan
// !(!v&low | v&high) = !(!v&low) & !(v&high)
// !v&low | v&high = !(!(!v&low) & !(v&high))
// note that if low or high are T
// we can simplify the formula
// given that low / high is T
// then !(!v&low) & !(v&high) can be simplified to
// !v&low | v&high = !v | high / low | v
// = !(v & !high) / !(!low & !v)
// The case when low / high is ⊥ is automatically treated
auto b_it = bdd2var_.find(b.id());
if (b_it != bdd2var_.end())
return b_it->second;
// todo
// unsigned v_var = bdd2var_.at(bdd_var(b));
unsigned v_var = bdd2var_.at(bdd_ithvar(bdd_var(b)).id());
unsigned b_branch_var[2] = {bdd2INFvar(bdd_low(b)),
bdd2INFvar(bdd_high(b))};
unsigned r = aig_not(aig_and(v_var, b_branch_var[1]));
unsigned l = aig_not(aig_and(aig_not(v_var), b_branch_var[0]));
unsigned l;
unsigned r;
if (b_branch_var[0] == aig_true())
{
// low == T
l = v_var;
r = aig_not(b_branch_var[1]);
}
else if (b_branch_var[1] == aig_true())
{
// high == T
l = aig_not(b_branch_var[0]);
r = aig_not(v_var);
}
else
{
// General case
r = aig_not(aig_and(v_var, b_branch_var[1]));
l = aig_not(aig_and(aig_not(v_var), b_branch_var[0]));
}
return aig_not(aig_and(l, r));
}