Передача постоянных значений в функции через ограничения в Z3 - PullRequest
Новая
       9

Передача постоянных значений в функции через ограничения в Z3

0 голосов
/ 18 декабря 2018

Я заметил в Z3, что если я использую функцию в моих ограничениях для Солвера, то я не могу передать ей постоянное значение.

Например:

В функции ниже, gen() - это функция, которая принимает 2 входа.Первый вход - это BitVec (), который представляет строку длиной 10. Второй параметр функции gen () будет использоваться для некоторых вычислений в ней.Тем не менее, я заметил, что хотя я передаю постоянное значение в качестве второго параметра через ограничения, это значение отличается внутри функции, когда Z3 решает уравнение. 

from z3 import *

def gen(input, v):
    outer_counter = v

    for i in range(len(input)):


    return result

s = Solver()

input = [BitVec("input%s" % i, 8) for i in range(10)]

s.add(gen(input, 0) == 0xAABBCCDD)
s.add(gen(input, 1) == 0xABCDABCD)

Итак, есть ли способв Z3 вызывать функцию через ограничения, а также передавать ей фиксированное значение?

...