z3py: ошибка при попытке установить членство - PullRequest
Новая
       11

z3py: ошибка при попытке установить членство

1 голос
/ 28 апреля 2019

В Z3Py я хочу выразить, что значение одной (целочисленной) переменной должно быть среди множества допустимых значений. В этом случае E12 серия обычно используется для значений компонентов в электронике.

Мне удалось сделать это с помощью нескольких предложений Z3 Or (value == 12 || value == 15 || ...), но это кажется действительно уродливым и неэффективным. Каждый компонент моей системы получает около 80 ограничений, просто чтобы выразить это. Это, безусловно, затрудняет чтение сообщений об ошибках.

Когда я вместо этого пытаюсь использовать тип Set в Z3Py, он завершается с ошибкой сегмента. Код ниже воспроизводит это.

Это правильный способ использования наборов для этой цели? Есть ли другие чистые способы сделать то же самое? 


import z3
import pytest

e12_series = (1.0, 1.2, 1.5, 1.8, 2.2, 2.7, 3.3, 3.9, 4.7, 5.6, 6.8, 8.2, 10.0)

def e_values(start_decade=1, end_decade=6, series=e12_series):
    values = []
    for decade in range(start_decade, end_decade):
        values += [ int(v*10)*10**(decade-1) for v in series ]    

    return values

def value_in(value, valid):
    options = [ value == v for v in valid ]
    return z3.Or(options)

# Values to test with
E12_VALID=[
    120, 18e3,
]
E12_INVALID=[
    119, 19e3,
]

EXAMPLES = []
EXAMPLES += [ (True, v) for v in E12_VALID ]
EXAMPLES += [ (False, v) for v in E12_INVALID ]

@pytest.mark.parametrize('example', EXAMPLES)
def test_bruteforce(example):
    expect_valid, value = example 
    valid_values = e_values()

    s = z3.Solver()
    var = z3.IntVal(value)
    s.add(value_in(var, valid_values))
    satisfied = str(s.check()) == 'sat'
    assert satisfied == expect_valid, s

@pytest.mark.parametrize('example', EXAMPLES)
def test_set(example):
    expect_valid, value = example

    # create a set
    valid_values = e_values()
    e12 = z3.SetSort(z3.IntSort())
    for val in valid_values:
        z3.SetAdd(e12, val)

    s = z3.Solver()
    var = z3.IntVal(value)
    s.add(z3.IsMember(var, e12))
    satisfied = str(s.check()) == 'sat'
    assert satisfied == expect_valid, s

Запуск с pytest -v setmembers.py, вывод: 

platform linux -- Python 3.7.3, pytest-4.4.1, py-1.8.0, pluggy-0.9.0 -- /usr/bin/python
plugins: cov-2.6.1, hypothesis-4.17.0
collected 8 items                                                                                                                                                                                                                            

setmembers.py::test_bruteforce[example0] PASSED                                                                                                                                                                                        [ 12%]
setmembers.py::test_bruteforce[example1] PASSED                                                                                                                                                                                        [ 25%]
setmembers.py::test_bruteforce[example2] PASSED                                                                                                                                                                                        [ 37%]
setmembers.py::test_bruteforce[example3] PASSED                                                                                                                                                                                        [ 50%]
setmembers.py::test_set[example0] Segmentation fault (core dumped)

Использование python-z3 4.8.4-2 в Arch Linux

...