Вопросы по теме 'z3'
Какая статистика указывает на эффективную работу Z3?
Директива SMTLib2 (get-info all-statistics) отображает несколько чисел, например.
num. conflicts: 4
num. propagations: 0 (binary: 0)
num. qa. inst: 23
Чтобы протестировать различные аксиоматизации и кодировки, я хотел бы знать,...
857 просмотров
schedule
04.08.2023
Можно ли использовать Z3 для рассуждений о подстроках?
Я пытаюсь использовать Z3, чтобы рассуждать о подстроках, и столкнулся с некоторым неинтуитивным поведением. Z3 возвращает «sat», когда его просят определить, появляется ли «xy» внутри «xy», но возвращает «неизвестно», когда его спрашивают, находится...
1453 просмотров
schedule
27.05.2023
Присвоить значение битовому вектору (SMTLIB2, Z3)?
Я использую Z3 версии 3.0. Я хочу присвоить значение переменной битового вектора, как показано ниже. Но Z3 сообщает об ошибке «недопустимое приложение функции, несоответствие сортировки аргумента в позиции 2 в строке 3».
Кажется, моя константа...
1713 просмотров
schedule
21.11.2022
Как узнать, соответствует ли z3_ast предложению?
Я использую Z3 с C API. Можно ли узнать, соответствует ли данная переменная Z3_ast такому предложению, как or_b1_b2 ниже?
Z3_ast or_b1_b2 = mk_binary_or(c,mk_bool_var(c,"b1"),mk_bool_var(c,"b2"));
Спасибо
334 просмотров
schedule
01.09.2022
Тот же ввод, Z3 работает в Windows, но дает ошибки сегментации в Linux.
Я использую Z3 в качестве внутреннего решателя для проверки ограниченной программы. Я подаю одни и те же формулы на Z3 в разных операционных системах, Windows 7 X64 и SuSe 10.3 X64, оба Z3 версии 3.2.
Их ввод: run.z3 , он содержит вложенные...
202 просмотров
schedule
04.09.2022
Причина тайм-аута?
Я новичок в использовании Z3. Но я хочу понять, причина тайм-аута в следующей программе, введенной в Z3:
(declare-fun ADDR (Int) Int)
(declare-fun STAR (Int Int) Int)
(declare-fun VAR (Int Int) Int)
(declare-const error Int)
(assert (forall ((x...
286 просмотров
schedule
30.12.2022
Сортировочно-параметрические функции-обертки
Предполагая использование нескольких встроенных и определяемых пользователем сортировок Z3, например. Int, Bool, S1, S2, ..., есть ли способ написать общую функцию сортировки и распаковки, которая выполняет преобразование из сортировки A в сортировку...
170 просмотров
schedule
01.12.2022
алгебраические действительные числа: выполняет ли z3 округление при красивой печати?
Если я выдаю:
(set-option :pp-decimal true)
(set-option :pp-decimal-precision 10)
Делает ли Z3 какое-либо округление после 10-й цифры действительного числа? Или он просто обрезает оставшиеся цифры без округления?
366 просмотров
schedule
11.03.2024
Почему результат запроса меняется, если прокомментировать промежуточный вызов `(check-sat)`?
При отладке запроса UNSAT я заметил интересную разницу в статусе запроса. Структура запроса:
assert(...)
(push) ; commenting any of these two calls
(check-sat) ; makes the whole query UNSAT, otherwise it is SAT
assert(...)
(check-sat) ; SAT...
134 просмотров
schedule
18.04.2023
API Z3 ast_to_string() с вычитанием
Проблема довольно проста. Я утверждаю следующее утверждение в Z3, используя интерфейс C API.
(assert(>= (xA 1) (- (yB 0) period))))
Теперь иногда мне нужно проверить, какие утверждения были отправлены, и результат в SatSolver. Я делаю...
187 просмотров
schedule
13.04.2022
разрешима ли теория списка?
Мне интересно, разрешима ли теория списка z3? Кажется, что мы можем доказать только факты, которые не подтверждены, но не подтверждены с помощью теории, поэтому мне любопытно, разрешима ли она на самом деле. Спасибо за вашу помощь.
423 просмотров
schedule
08.03.2023
Обход Z3Context с помощью API z3.scala.dsl
Я использую инструмент scala^Z3 для небольшой библиотеки, которая (среди прочего) печатает ограничения Z3Context в латексном формате. Хотя можно пройтись по Z3AST и преобразовать выражения в латекс путем сравнения строк, было бы гораздо удобнее...
103 просмотров
schedule
22.04.2022
битвектор против целого числа в Z3
Я реализовал z3, используя фиксированную точку phi (Real, Real, Int, Int, Int, Int) и добавил некоторые правила в фиксированную точку. Это дало мне ответ, однако, когда я меняю тип Int на тип BitVector, он не может решить проблему и, наконец,...
866 просмотров
schedule
13.05.2023
Ошибка плагина теории Z3
Я создал собственный плагин теории, который на данный момент ничего не делает. Все обратные вызовы реализованы и зарегистрированы, но они просто возвращаются. Затем я считываю набор из declare-consts, declare-funs и asserts, используя...
195 просмотров
schedule
24.11.2022
Как переименовать переменную с помощью Z3?
учитывая выражение x'=x+1, я хочу переименовать x' в y. Как сделать с помощью z3?
434 просмотров
schedule
17.07.2023
Z3 вызывает недопустимый доступ к памяти с помощью JNA
Я использую Z3 C api в java с jna. Я часто получаю неверный доступ к памяти, но только с библиотеками windows (.dll) и mac os (.dylib). Этого не происходит, когда я использую linux one (.so).
Я временно решил эту проблему, никогда не вызывая...
957 просмотров
schedule
27.11.2022
как проверить, является ли const в z3 переменной или значением?
просто интересно в z3py , как мне проверить, является ли данное постоянное выражение переменной или значением? Например
x = Int('x')
x_ = IntVal(7)
ColorVal, (White,Black) = EnumSort("ColorVal",["While","Black"])
mycolor =...
2034 просмотров
schedule
16.01.2023
Z3 используя цели и тактику
Я использую Z3 с C-API. Я пытаюсь понять, как понять, как использовать тактику и цель в C-API. Проверял на примерах Z3, но не нашел подходящего.
У меня есть псевдокод C-API, как показано ниже:
contextId = mk_context();
solverId =...
1281 просмотров
schedule
13.08.2022
Как читать строки smtlib2 с помощью Z3 C++ API?
Я хочу создать объект expr из заданного файла SMTLIB2. Я вижу функцию Z3_parse_smtlib_string в примерах C. Есть ли для этого оболочка в классе expr ?
500 просмотров
schedule
09.06.2022
Равенство констант в решателе Z3 SMT
Я использую решатель Z3 SMT от Microsoft и пытаюсь определить константы пользовательского вида. Кажется, что такие константы по умолчанию не являются неравными. Предположим, у вас есть следующая программа:
(declare-sort S 0)
(declare-const x...
3049 просмотров
schedule
22.06.2022
