Как получить конкретные значения из FuncInterp в Z3 Python? - PullRequest
Новая
       16

Как получить конкретные значения из FuncInterp в Z3 Python?

0 голосов
/ 08 апреля 2019

Я использовал Z3 Solver, чтобы проверить запрос и получить модель. Но некоторые переменные в модели - это FuncInterp, показанные в виде лямбда-функций. 

[v0 = Lambda(k!0, If(k!0 == 1, 4, 0)),
 v1 = Lambda(k!0,
                  If(k!0 == 1,
                     1,
                     If(k!0 == 3,
                        128,
                        If(k!0 == 2, 113, 0)))),
 v2 = Lambda(k!0, If(k!0 == 1, 1, 0)),
 v3 = Lambda(k!0,
                  If(k!0 == 1,
                     244,
                     If(k!0 == 3,
                        216,
                        If(k!0 == 2, 214, 198)))),
 v4 = Lambda(k!0,
                  If(k!0 == 3,
                     198,
                     If(k!0 == 1,
                        214,
                        If(k!0 == 2, 244, 215)))),
 v5 = K(BitVec(32), 80),
 v6 = K(BitVec(32), 194),
 v7 = K(BitVec(32), 80),
 v8 = K(BitVec(32), 80)]

Даже я пытался использовать z3.set_param('model_compress', False), как предложено в Как получить значение из лямбда-выражения? Они все еще как: 

[v0 = [0 -> 0, 1 -> 4, else -> 0],
 v1 = [0 -> 0,
       2 -> 113,
       3 -> 128,
       1 -> 1,
       else -> 0],
 v2 = [2 -> 0,
       0 -> 0,
       3 -> 0,
       1 -> 1,
       else -> 0],
 v3 = [0 -> 198,
       2 -> 214,
       3 -> 216,
       1 -> 244,
       else -> 198],
 v4 = [0 -> 215,
       2 -> 244,
       1 -> 214,
       3 -> 198,
       else -> 215],
 v5 = K(BitVec(32), 80),
 v6 = K(BitVec(32), 194),
 v7 = K(BitVec(32), 80),
 v8 = K(BitVec(32), 80),
 k!7 = [2 -> 0, 0 -> 0, 3 -> 0, 1 -> 1, else -> 0],
 k!4 = [0 -> 0, 1 -> 4, else -> 0],
 k!8 = [0 -> 215, 2 -> 244, 1 -> 214, 3 -> 198, else -> 215],
 k!5 = [0 -> 0, 2 -> 113, 3 -> 128, 1 -> 1, else -> 0],
 k!6 = [0 -> 198, 2 -> 214, 3 -> 216, 1 -> 244, else -> 198]]

У меня вопрос, как я могу получить постоянные / конкретные значения для этих FuncInterp?

Большое спасибо,

...