Эквивалент (утверждать (= 10)) в Z3Py - PullRequest
Новая
       13

Эквивалент (утверждать (= 10)) в Z3Py

0 голосов
/ 20 октября 2019

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

У меня есть рабочий код в стандарте SMT-LIB 2.0. Я рассмотрел примеры на основе Python для Z3, но не смог найти решение.

Примечание: я очень новичок в SMT Solvers, таких как Z3.

Я знаю, что мы можем просто написать (assert (= a 10)), используя стандарт SMT-LIB 2.0. Для Python я попробовал a = IntVal("10"). Я не уверен, что это то, что мне нужно.

Я хочу написать (assert (= a 10)) аналогичный код, используя Z3Py. Будем благодарны за любую помощь.

1 Ответ

2 голосов
/ 20 октября 2019

В z3py это будет просто: 

from z3 import *

s = Solver()

a = Int('a')

s.add(a == 10)

print s.check()
print s.model()

, который печатает: 

sat
[a = 10]

Назначение против равенства

Когда вы программируете в SMTLib или Z3pyлучше рассматривать равенство как сравнение, а не как задание. Когда вы говорите: 

(assert (= a 10))

в SMTLib, вы не назначаете что-либо на a. Все, что вы говорите, это то, что значение a должно сравниваться равным 10. На самом деле выражение (= a 10) имеет тип Bool, поэтому вы можете эквивалентно сказать: 

(assert (= true (= a 10)))

, что было бы избыточным, но оно иллюстрирует суть.

Путаница в том,Конечно, «сравнение на равенство» в SMTLib называется =, но в Python это ==;и что еще хуже, = имеет смысл в Python как присваивание;но это не значит, что ты пытаешься сказать. Если вы знакомы с функциональным программированием, подумайте о программах SMTLib / Z3Py как о совокупности переменных разных типов и утверждений об отношениях между ними.

Надеюсь, это поможет! Задавать конкретные вопросы всегда лучше, чем английская проза;не стесняйтесь размещать фрагменты кода, которые могут сбивать с толку.

...