Support for Bit Vectors #13
Conversation
|
Oh I see the issue with |
… add QF_BV to the supported logics
+ The TVAR type stores the string representation of the bitvector's size. Two bitvectors will unify if they have the same size. + More operations on bitvectors were added to BitVecComponents.ml and to Bitarray.ml.
|
In order to run benchmarks I have to remove line 9 of Simulator.ml. Also, I think the way I tried to parameterize the bit vector type is probably not that good since I use TVAR to store information for a string instead of another type. Maybe I should create another type which just parameterizes the length of a bit vector. |
|
Thanks, let me take a look at your current set of changes and then I can provide better feedback. |
There was a problem hiding this comment.
Thanks Adam.
The components file and Bitarray file look good. I have left some comments on the definitions of types and values. The main issue is that we are doing unnecessary Int <-> String conversions for the length (which is also expensive computationally).
I will take another pass once that's fixed.
… bit The unification routines try to match a BitVec of negative size to one of positive size. The negative size is treated as a variable, so all BitVecs of size -1 will be matched to the same length BitVec. There is still int to string conversions because the length is parsed as a string and the unification routines use an environment, env, of type (string * t).
|
Hi Adam, Thanks for all these changes. Please let me know when you want me to take another look at your changes. |
|
Hi Saswat, |
|
I ran into the same problem that you had here with core_extended. Did you ever find a solution to it? It seems like the issue is that the dune file for the bitarray module does not have the |
|
@adaminsky You're right. I just tried it again and there doesn't seem to be an easy way of using I would raise another bug report, but for now I think you should move all your additions to some other files ( |
Bitarray.ml is taken from v0.14.0 of core_extended and included into the extended BitarrayExt module. A bitvector benchmark is included adapted from [cegar2.sl](https://github.com/SyGuS-Org/benchmarks/blob/master/lib-nonconforming/Inv_Track/cegist-cav18/cegar2.sl) in the SyGuS benchmarks repository. This benchmark currently passes.
No description provided.