Замена Z3 по лямбде не удалась - PullRequest
Новая
       15

Замена Z3 по лямбде не удалась

0 голосов
/ 12 марта 2019

Задача

Я пытаюсь сделать замену над телом выражения Lambda, но, похоже, оно вообще не подставляется.

Мотивация

Я пытался Select над Lambda, но это не разрешено в Z3.

Сломанный код

Я также попытался подставить переменную read, но она тоже не сработала. 

def test_select_over_lambdas_can_be_implemented():
    solver = Solver()
    read = BitVec('read', 8)
    fake_array = Lambda([read], read)
    print(fake_array)  # Lambda(read, read)
    print(fake_array.body())  # Var(0)
    new_select = substitute(
        fake_array.body(),
        [
            (Const("Var(0)", fake_array.var_sort(0)), BitVecVal(1, 8))
        ])
    print(new_select)  # Var(0) / substitution failed
    solver.add(new_select == 1)
    assert str(solver.check()) == "sat"  # Fails with answer "unknown"
...