I would like to use redlog to perform symbolic quantification of formulas over bitvectors. The formulas I'm dealing with use normal arithmetic operations (+,-, and constant multiplication), bit-wise operations, and relational operators (=,<,>,...). All of this can in principle be encoded using Presburger arithmetics with congruence. For my application it is important that the resulting expression after quantification is as concise as possible (which is why I cannot use bit blasting). My preliminary experiments with Redlog look promising; however I noticed that the structure of the result depends on the encoding of the input formula.
Therefore I was wondering if the Redlog community has experience with this type of problems. Perhaps there are some publications or software that I could look at to get some ideas for efficient encoding of bitvectors?
Thanks!
Leonid
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Maybe the reference below is somewhat related. Are your Presburger variables machine integers or are you encoding abstract bitvectors into Presburger integer variables?
Thomas
@incollection{KarrenbergKosta:13a,
Author = {Karrenberg, Ralf and Ko\v sta, Marek and Sturm, Thomas},
Booktitle = {Frontiers of Combining Systems},
Editor = {Fontaine, Pascal and Ringeissen, Christophe and Schmidt, Renate A.},
Pages = {56-70},
Publisher = {Springer},
Series = {LNAI},
Title = {Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages},
Volume = {8152},
Year = {2013}}
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
I would like to use redlog to perform symbolic quantification of formulas over bitvectors. The formulas I'm dealing with use normal arithmetic operations (+,-, and constant multiplication), bit-wise operations, and relational operators (=,<,>,...). All of this can in principle be encoded using Presburger arithmetics with congruence. For my application it is important that the resulting expression after quantification is as concise as possible (which is why I cannot use bit blasting). My preliminary experiments with Redlog look promising; however I noticed that the structure of the result depends on the encoding of the input formula.
Therefore I was wondering if the Redlog community has experience with this type of problems. Perhaps there are some publications or software that I could look at to get some ideas for efficient encoding of bitvectors?
Thanks!
Leonid
Maybe the reference below is somewhat related. Are your Presburger variables machine integers or are you encoding abstract bitvectors into Presburger integer variables?
Thomas
@incollection{KarrenbergKosta:13a, Author = {Karrenberg, Ralf and Ko\v sta, Marek and Sturm, Thomas}, Booktitle = {Frontiers of Combining Systems}, Editor = {Fontaine, Pascal and Ringeissen, Christophe and Schmidt, Renate A.}, Pages = {56-70}, Publisher = {Springer}, Series = {LNAI}, Title = {Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages}, Volume = {8152}, Year = {2013}}