search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
324 stars 63 forks source link

Lookup Table #192

Closed panicarada closed 2 years ago

panicarada commented 2 years ago

Is there a way to create a constant lookup table that can be accessed by a variable index? It is useful for representing nonlinear operation like S-boxes in cryptography.

panicarada commented 2 years ago

It can be done by b.Array(), we just need to initialize the array by sequentially writing

for i in range(n):
    arr = btor.Write(arr, i, f(i))