Вопросы по теме 'z3py'
Как решить проблему лжецов / правдивых с помощью Z3Py и Z3 SMT-LIB
Пример проблемы:
Предположим, что лжецы всегда говорят неправду, а правдивые всегда говорят правду. Далее предположим, что Эми, Боб, Кэл, Дэн, Эрни и Фрэнсис - каждый либо лжец, либо рассказчик правды.
Amy says, “Bob is a liar.”
Bob says, “Cal...
285 просмотров
schedule
26.07.2022
Какую форму ввода принимает решатель z3 smt? Как использовать файл для чтения уравнения, которое необходимо решить?
from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
try:
f = open("read.txt","r")
try:
str = f.read()
length = len(str)
s.add(str)
finally:
f.close()
except IOError:
pass
Я написал приведенный...
1920 просмотров
schedule
25.12.2022
Проверьте переполнение с помощью Z3
Я новичок в Z3 и проверял онлайн-учебник по Python.
Затем я подумал, что могу проверить поведение переполнения в BitVecs.
Я написал этот код:
x = BitVec('x', 3)
y = Int('y')
solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1)))
и я...
989 просмотров
schedule
25.03.2024
Можно ли получить окончательную формулу CNF от Z3?
Вот моя простая кодировка. Я хотел бы получить окончательную логическую CNF, в которой представлены все эти ограничения. Есть ли в решателе Z3 возможность получить окончательную логическую CNF?
x = Int('x')
y = Int('y')
c1 = And(x >= 1, x...
1378 просмотров
schedule
29.03.2022
Как я могу решить ограничение минимизации в Z3?
Может ли кто-нибудь сказать мне, как я могу реализовать задачу минимизации целых чисел, подобную приведенной ниже, с помощью Z3py? Как я могу определить для всех утверждений? Здесь все переменные int sort.
Есть ли в Z3 специальный решатель...
1446 просмотров
schedule
10.06.2023
z3py: предположения из (check-sat) утверждения
Есть ли способ передать предположения из (check-sat ...) утверждения формулы SMT2 в решатель?
Рассмотрим следующий пример формулы, хранящейся в ex.smt2:
# cat ex.smt2
(declare-fun p () Bool)
(assert (not p))
(check-sat p)
Как и ожидалось,...
227 просмотров
schedule
22.03.2023
как преобразовать выражение z3py в формат smtlib 2
Мой вопрос связан с: Z3: преобразовать выражение Z3py в SMT-LIB2?
Я пытаюсь преобразовать выражение z3py из в формат smtlib2. используя следующий скрипт, но после преобразования, когда я передаю результат на z3 или любой другой SMT, я получаю:...
1220 просмотров
schedule
12.08.2022
z3.prove намного быстрее, чем решатель и проверка
Я использую последний основной код z3 от Codeplex, помеченный как v4.3.1.
Мне нужна такая функция, как prove , которая имеет полезное возвращаемое значение и не печатает. Итак, я написал то, что казалось очевидным:
def prove2(claim):
s =...
545 просмотров
schedule
17.09.2023
Упрощение выражения с использованием переменных в конечной области
Тактика ctx-solver-simplify работает только для логических переменных, поэтому как мне поступить с переменными в конечной области (например, какую тактику использовать)? Например, если z может принимать только 3 значения 0,1,2 , то как упростить...
133 просмотров
schedule
25.04.2024
Производительность решателя z3 SMT на разных платформах
У меня есть логические проблемы, написанные с использованием z3py. Я запускаю их как на своем ПК (intel core i5 + 8 ГБ ОЗУ), так и на кластере (32 процессора AMD Operaton 6320 + 500 ГБ ОЗУ). Нет большой разницы во времени выполнения, и иногда...
640 просмотров
schedule
22.03.2023
как решить уравнение вместо того, чтобы давать одну модель в z3
Это может не выходить за рамки z3, я знаю, что в Z3 мы можем упростить выражение, но мне интересно, может ли z3 решить уравнение вместо того, чтобы давать модель.
Например, я хочу, чтобы следующее уравнение всегда было верным для любого значения a....
295 просмотров
schedule
01.02.2022
Как отобразить конкретное ограничение unsat, а не все ядро (Z3, Python)
Как я могу перечислить только конкретные результаты ограничений из моего ненасыщенного ядра? У меня много условий, и печать всего ядра не печатает все. Я читал, что это можно сделать с помощью команд assert_and_track и unsat_core. Я нашел несколько...
804 просмотров
schedule
22.01.2024
Почему создание объектов И / ИЛИ в Z3py занимает больше времени, чем ожидалось?
Я использую Z3py, где мне нужно создать тысячи объектов And () и Or () для подачи в Z3 Solver. Кажется, что большую часть времени уходит на создание этих объектов (добавление их в решатель и их решение происходит намного быстрее). В крайнем случае...
131 просмотров
schedule
01.02.2023
Неявная и явная количественная оценка существования в формулах SMT
Учитывая следующий код:
from z3 import *
a,b,c = BitVecs('a b c', 32)
f1 = Exists([a, b, c], And(a + b == c, a < b, c == 1337))
f2 = And(a + b == c, a < b, c == 1337)
prove(f1 == f2)
Я бы предположил, что в этом примере z3 неявно...
202 просмотров
schedule
04.08.2023
z3 и z3PY дают разные результаты
Когда я пробовал следовать в z3, у меня был таймаут результата
(set-option :smt.mbqi true)
(declare-fun R(Int) Int)
(declare-fun Q(Int) Int)
(declare-var X Int)
(declare-var Y Int)
(declare-const k Int)
(assert (>= X 0))
(assert (> Y 0))...
90 просмотров
schedule
07.02.2022
Объявление неинтерпретируемых полиадных функций с помощью Z3Py
Используя Z3Py, я пытаюсь написать функцию decl_func(fname, arity) , которая принимает два аргумента: fname , имя объявляемой функции, и arity , ее количество аргументов, и возвращает соответствующую (не интерпретируемую) функцию Z3 над целыми...
59 просмотров
schedule
21.03.2022
Примеры z3py не работают на macOS
Я не могу заставить работать ни один из примеров z3py. Мне удалось успешно установить его, следуя инструкциям из README на github. Я успешно обновил свой путь Python, чтобы он указывал на соответствующий каталог. Кроме того, мне удалось успешно...
1485 просмотров
schedule
03.06.2022
Ограничение K-вне-N в Z3Py
Я использую привязки Python для программы доказательства теорем Z3 (Z3Py). У меня есть N логических переменных, x1, .., xN. Я хочу выразить ограничение, согласно которому ровно K из N из них должны быть истинными. Как я могу это сделать в Z3Py?...
2001 просмотров
schedule
19.05.2023
Какие дополнительные аксиомы нам нужно добавить, чтобы Z3 мог проверять выполнимость программ с повторениями?
Как мы знаем , Z3 имеет ограничения с рецидивами. Есть ли способ получить результат для следующей программы? какое дополнительное уравнение поможет z3 получить результат?
from z3 import *...
326 просмотров
schedule
23.07.2023
Оцените BitVec в Z3Py
Я изучаю Z3 и возможно мой вопрос не актуален, так что наберитесь терпения.
Предположим, у меня есть следующее:
c1, c2 = z3.BitVec('c1', 32), z3.BitVec('c2', 32)
c1 = c1 + c1
c2 = c2 + c2
c2 = c2 + c1
c1 = c1 + c2
e1 = z3.simplify(c1)
e2 =...
286 просмотров
schedule
09.04.2024
