How to Compute Constant Bits in Bit Vector Formula?

[ChristianMoesl]

In the 2020 paper (section IV-B) they do not describe in detail how they compute "At", a precomputed ternary bit vector assignment for every node in the formula graph. They describe it on a high level: Bit Blasting is used to construct a AIG (And-Inverter-Graph) from the Bit Vector Formula. The graph is optimised greedily during construction. Constant Bits can then be inferred from the AIG and mapped back to the Word level to construct the ternary bit vectors.

They also mention a potential other method use propagation on a word level and some related work for that. This method seems more interesting to me, as the authors of the 2020 paper also say, that it could be faster.

For our first prototype I think we can effectively turn this constant bit optimisation off by computing a ternary bit vector assignment for every node, where every bit is in the "undetermined state" (*). And therefore we can ignore this problem for now.

Still I think it's good to keep it up here as an issue to start a discussion.

[ckirsch]

@ChristianMoesl you can always contact the authors and ask questions. Just cc me.

[ChristianMoesl]

@ckirsch Yeah right, I should definitely do that. Maybe this problem is also interesting for you @programLyrique ? This is for sure the biggest unsolved problem for our engine.

[programLyrique]

I'll have a look at it!

[AlexLoitzl]

In the paper they mention using bit-blasting and an And-Inverter-Graph for constant bit calculation. For future work they suggest calculating constant bits on the word level referencing two papers. One of those is Constraint Satisfaction over Bit-Vectors which one should read when considering implementing ternary vectors as many of the concepts seem to be adapted in the work of Aina and Matthias. They only give some examples and calculations for operators that are of interest to us, are missing. In Wombit the same concept was implemented and they have a github repo where one can see the implementations. Their work is based on the first paper,they extend and improve on it to build a working solver. I think with this information it should be possible to implement this on the word level.

[ckirsch]

This is a nice topic for a thesis, bachelor or master.