z3py: получить условия ветвления из формулы z3 - PullRequest
Новая
       13

z3py: получить условия ветвления из формулы z3

0 голосов
/ 19 февраля 2020

Допустим, у меня есть программа z3py, подобная этой: 

import z3


a = z3.Int("a")
input_0 = z3.Int("input_0")
output = z3.Int("output")

some_formula = z3.If(a < input_0, 1, z3.If(a > 1, 4, 2))

s = z3.Solver()

s.add(output == some_formula)

s.check()
m = s.model()
print(m)

Есть ли для меня элегантный способ получить условия ветвления из some_formula? Так что получите список вроде [a < input_0, a > 1]. Это должно работать для сколь угодно глубокой вложенности выражений if.

Я знаю, что есть какой-то способ использования кубов, но я не могу получить более двух выражений куба. Я не уверен, как настроить решатель.

Моя конечная цель состоит в том, чтобы заставить решатель выдавать мне разные выходные данные в зависимости от ограничений, которые я выбираю * pop и 101. Ограничения - это набор условий, которые я вывел из этой формулы.

Ответы [ 2 ]

0 голосов
/ 19 февраля 2020

Хорошо, спасибо @alias! Я придумал пользовательскую версию, которая выполняет свою работу. Если кто-то знает более элегантный способ сделать это, пожалуйста, дайте мне знать. 

import z3


a = z3.Int("a")
input_0 = z3.Int("input_0")
output = z3.Int("output")

some_formula = z3.If(a < input_0, 1, z3.If(a > 1, 4, 2))
nested_formula = z3.If(some_formula == 1, 20, 10)

s = z3.Solver()

s.add(output == some_formula)

s.check()
m = s.model()
print(m)


def get_branch_conditions(z3_formula):
    conditions = []
    if z3.is_app_of(z3_formula, z3.Z3_OP_ITE):
        # the first child is usually the condition
        cond = z3_formula.children()[0]
        conditions.append(cond)
    for child in z3_formula.children():
        conditions.extend(get_branch_conditions(child))
    return conditions


conds = get_branch_conditions(some_formula)
print(conds)
conds = get_branch_conditions(nested_formula)
print(conds)
0 голосов
/ 19 февраля 2020

Вы можете распечатать кубы, используя: 

for cube in s.cube():
    print cube

Но это не поможет вам. Для вашего примера он печатает: 

[If(a + -1*input_0 >= 0, If(a <= 1, 2, 4), 1) == 1]
[Not(If(a + -1*input_0 >= 0, If(a <= 1, 2, 4), 1) == 1)]

, что не совсем то, что вы искали.

Самый простой способ go рассказать о вашей проблеме - это пройти прямо по AST формулы, и возьмите условия, когда вы идете по выражениям. Конечно, Z3 AST - довольно волосатый объект (каламбур!), Так что для этого потребуется немало программирования. Но чтение конструкторов (If, Var et c.) В этом файле поможет вам начать: https://z3prover.github.io/api/html/z3py_8py_source.html

...