Вопросы по теме 'z3'
Поддерживает ли Z3 интерполяцию Крейга?
Может ли Z3 генерировать интерполянты Крейга (по крайней мере, для пропозициональной логики?). Я не нашел его в документации Z3.
673 просмотров
schedule
25.03.2024
Объявить символы, которые остаются действительными за пределами их области действия
В Z3 2.x была особенность (ну, скорее, ошибка), что объявления символов не выскакивали, например. следующий код принимается Z3 2.x:
(push)
(declare-fun x () Int)
; Assumptions made in this scope will be popped correctly
(pop)
(assert (= x x))...
115 просмотров
schedule
28.07.2023
Как объявить запись так, чтобы одно из ее полей было функцией
Я очень новичок в Z3, так что извините за глупые вопросы.
Я пытаюсь определить запись так, чтобы некоторые из ее полей были функциями. Я пробовал это:
(объявить типы данных (DOM RAN) ((PFun (mk-pfun (dom (DOM) Bool) (закон (DOM) RAN)))))
с...
171 просмотров
schedule
16.03.2023
Можно ли клонировать Z3_context?
Мне это нужно для пошагового решения в контексте символического выполнения (Кли). В точках ветвления символьных путей выполнения необходимо разделить контекст решателя на 2 части: с истинными и ложными условиями. Конечно, есть дорогой обходной путь...
487 просмотров
schedule
09.08.2022
Есть ли способ упростить условия пути
Например, в приведенном ниже коде условие пути будет x>0 && x+1>0 . Но поскольку x>0 подразумевает x+1>0 , есть ли способ в z3 или pex API получить только x>0 , а не оба.
if(x>0)
if(x+1>0)
//get path...
188 просмотров
schedule
22.03.2023
Можно ли найти оптимальное решение для булевой формулы с помощью решателей SMT?
У меня есть большая логическая формула для решения, из-за редактирования я должен вставить изображение здесь:
Кроме того, у меня уже есть функция area для измерения размера 4 целых чисел: area(c,d,e,f)=|c−d|×|e−f|
Я хотел бы сделать...
1636 просмотров
schedule
29.01.2023
Есть ли разница между версиями Z3 2.19 и 3.2 w.r.t. Синтаксис кода SMTLIB-2?
После установки Z3 V3.1 следующий код SMT-LIB не работает. В моей ранней версии (Z3 V2.19) было неплохо.
(define-fun getIP ((o0 Int) (o1 Int) (o2 Int) (o3 Int)) BitVec[32]
(bvor (bvshl (int2bv[32] o0) (int2bv[32] 24))
(bvshl...
209 просмотров
schedule
27.05.2023
Предупреждение: параметр INI отсутствует в Z3 3.2?
Согласно списку параметров INI должны быть логическим флагом WARNING, но установить его в Z3 3.2 (x64_mt) через
(set-option :WARNING false)
дает unsupported для обоих написаний WARNING и warning .
Документы устарели или я что-то не...
88 просмотров
schedule
06.12.2023
Определить верхнюю/нижнюю границу для переменных в произвольной пропозициональной формуле
Учитывая произвольную пропозициональную формулу PHI (линейные ограничения на некоторые переменные), как лучше всего определить (приблизительно) верхнюю и нижнюю границы для каждой переменной?
Некоторые переменные могут быть неограниченными. В этом...
2042 просмотров
schedule
13.11.2022
Может ли Z3 работать в инкрементальном режиме?
Я использую Z3 на формулах QFBV. Мне было интересно, может ли Z3 постепенно работать с такими формулами, как решатели SAT могут работать с логическими предложениями. В основном мне нужен способ реализовать следующий цикл:
F = initial QFBV...
598 просмотров
schedule
08.06.2022
z3: как преобразовать логическую сортировку в сортировку по битовому вектору
Я делаю символическую интерпретацию инструкций x86. Например, для инструкции cmp знак сравнения и равенство операндов хранятся в двух битах регистра eflags.
Вот мой код:
/* s1,s2 are source operands of sort bit-vector
* of 32 bits...
526 просмотров
schedule
24.03.2024
Можно ли отключить вывод промежуточных моделей?
Формула с кванторами содержит объявление trans функции. Z3 успешно находит модель и печатает ее. Но он также печатает модели для таких функций, как trans!1!4464 , trans!7!4463 .. которые нигде в модели не используются. Что это такое? Как я...
146 просмотров
schedule
28.04.2023
Эквивалентные формулы без квантификатора
Я хочу знать, может ли Z3 отображать эквивалентные формулы после исключения квантификатора.
Пример (существует k) (i x k) = 1 и k > 5 эквивалентен
i > 0 и 5 i - 1 ‹ 0.
Здесь квантор k исключен.
Это возможно?
Спасибо, Каустубх.
452 просмотров
schedule
25.04.2023
объявление функции в z3
Можно ли в z3 объявить функцию, которая принимает в качестве аргумента другую функцию? Например, это
(declare-fun foo ( ((Int) Bool) ) Int)
не совсем работает. Спасибо.
2695 просмотров
schedule
02.05.2023
перекрестное произведение в z3
Предоставляет ли z3 функцию перекрестного произведения для двух списков? Если нет, возможно ли определить его без использования функций более высокого порядка или с использованием предоставленных функций списка? У меня возникли проблемы с...
403 просмотров
schedule
20.06.2022
Не удается выполнить пример scala^z3 fibonacci
Я пытаюсь использовать Scala^Z3 в 64-разрядной версии MacOS со следующими настройками:
res0: String = Z3 4.0 (сборка 0, ред. 0), ScalaZ3 3.2.c (в разработке)
Теперь, когда я пытаюсь выполнить пример Фибоначчи с главной страницы ScalaZ3 , я...
378 просмотров
schedule
06.04.2023
Z3 реальная арифметика и статистика
Учитывая проблему, которая закодирована с использованием Z3-реалов, какая из статистики, которую производит Z3 /smt2 /st , может быть полезной, чтобы судить, есть ли у движка Reals "проблемы/много работы"?
В моем случае у меня есть две в основном...
669 просмотров
schedule
10.08.2023
Инструменты для исключения квантификаторов в линейной целочисленной арифметике
Существуют ли какие-либо другие доступные (и до сих пор поддерживаемые) инструменты SMT, которые выполняют исключение квантификаторов для линейной целочисленной арифметики помимо Z3?
Спасибо.
241 просмотров
schedule
17.06.2022
Различные способы аксиоматизации содержащей функции для списков Z3
Аксиоматизация операции contains в списках ( в Rise4Fun ) как
(declare-fun Seq.in ((List Int) Int) Bool)
(assert (forall ((e Int))
(not (Seq.in nil e))))
(assert (forall ((xs (List Int)) (e Int))
(iff
(not (= xs nil))
(=...
300 просмотров
schedule
26.04.2022
Символьные переменные в z3
Есть ли способ заставить решатель z3 выдавать «символические» решения? Например, для уравнения:
1+x=c
решение x=c-1, но z3 всегда выдает определенную модель, например [c = 0, x = -1] . Как «определить» c как символическую переменную?
401 просмотров
schedule
29.12.2023
