CODEWITHSUNDEEP
z3smt
user3146687
user3146687

Reputation: 389

Abstract (QFBV) bit vector theory to linear arithmetric (LIA)

My current project involves counting/approximating the number of models in a set of constraints expressed in bit vector arithmetic. The model space is usually very large so enumerative methods will not scale very well. For instance:

A = BitVec('A', 32)
B = BitVec('B', 32)
solver.add(A>B)

The solution space would be 0.5 * 2 ** (2 * 32), beyond the reach of conventional probabilistic and enumerative models. There are existing tools, that I was hoping to use, such as http://arxiv.org/pdf/1507.00142.pdf, but it only works for LIA.

I was wondering if there are existing methods, or APIs that allows for such as abstraction. Otherwise the other option appears to be to manually translate all the clauses into LIA (linear integer arithmetic).

Upvotes: 2

Views: 102

Answers (0)

Related Questions