Описание тега smt-lib
1
ответ
Есть ли в SMT-Lib оператор неравенства?
Я знаю, что могу утверждать неравенство с помощью простых (not (= a b)), но мне интересно, есть ли оператор, который делает это напрямую. Я перепробовал все, что приходило мне в голову, включая !=, <>, \= (это не разбирается), /=, =/=, neq и н…
23 апр '21 в 12:05
1
ответ
Вывести ограничения SMTLib на стандартный вывод в PySMT
У меня проблема с кодированием с использованием API-интерфейсов PySMT. На странице PySMT на GitHub показан пример использования любого SMTLib-совместимого решателя с PySMT. В нем говорится, что PySMT передаст проблему для решения в stdin. Но я не мо…
06 май '21 в 10:20
2
ответа
Как использовать кортежи в SMT-lib?
Я совершенно уверен, что можно будет описывать кортежи с использованием синтаксиса SMT-lib, особенно для решателя Z3. Однако я не могу найти способ сделать это. Я нашел только эту страницу документации , но не понимаю, как ее использовать в z3 -in. …
21 май '21 в 10:53
1
ответ
Регулярное выражение для интерпретации формата smtlib2
Я пытаюсь вычислить регулярное выражение, которое могло бы соответствовать результатам программы, которая выводит в формате smtlib. В основном мои данные имеют вид: (define-fun X_1 () Int 281) (define-fun X_71 () Int 104) (define-fun X_90 () Int 21)…
06 июн '21 в 20:19
1
ответ
Моделирование вложенных кортежей / последовательностей в z3
В настоящее время я создаю механизм символьного исполнения для небольшого подмножества Python. Самая сложная структура данных, поддерживаемая этим подмножеством, - это произвольно вложенные кортежи , то есть вы можете написать что-то вроде x = (1, 2…
24 июн '21 в 11:20
1
ответ
Почему smtlib/z3/cvc4 позволяет объявить одну и ту же константу более одного раза?
У меня есть вопрос о declare-const в smtlib. Например, В z3 / cvc4 следующая программа не сообщает об ошибке: C:\Users\Chansey>z3 -in (declare-const x Int) (declare-const x Bool) В справочнике smt-lib сказано, что (declare-fun f (s1 ... sn) s) ..…
18 авг '21 в 08:50
1
ответ
Можно ли в Z3 кодировать условные проверки Sat?
Предположим, у меня есть следующая проблема (которую я сделал тривиальной, чтобы упростить свой вопрос) ;; declare variables (declare-const X0 Int) (assert (>= X0 0)) (assert (<= X0 1)) (declare-const X1 Int) (assert (>= X1 0)) (assert (<…
18 авг '21 в 04:16
1
ответ
Можно ли в smtlib объявить сортировку функций?
Например, $ z3 -in (declare-fun f (Int Real) Int) (assert (= f f)) (check-sat) sat Хорошо. Однако я бы хотел квалифицировать это as? $ z3 -in (declare-fun f (Int Real) Int) (assert (= (as f ???) (as f ???))) (check-sat) sat Что я должен заполнить ??…
29 сен '21 в 16:42
1
ответ
параметрические функции в smtlib
Я понимаю, что есть способ объявить параметрические типы данных в SMTLIB. Есть ли способ определить функцию, которая принимает такой тип? Например, в стандартном документе есть: ( declare - datatypes ( ( Pair 2) ) ( ( par ( X Y ) ( ( pair ( first X …
12 ноя '21 в 05:48
0
ответов
3 кувшина с водой [закрыто]
Мне нужно решить загадку 3 кувшина с водой, и я очень потерялся. Емкость кувшинов 8, 5 и 3 литра. Вначале кувшин на 8 литров полон, а в конце кувшины на 8 и 5 литров должны иметь по 4 литра в каждом, а третий должен быть пуст. Решаю с помощью синтак…
20 дек '21 в 03:41
0
ответов
SMT-LIB2 синтаксический анализатор pysmt lib
У меня есть работа над pysmt lib в Python. Я буду работать над кодом SMT-LIB2. Вы можете увидеть код ниже. Я хочу спросить «как я могу получить значение переменных?». В коде я использую x1 как Bool, но не могу получить значение. Не могли бы вы помоч…
25 дек '21 в 17:38
1
ответ
Есть ли механизм шаблонов для smtlib2 (или z3)?
Мне было интересно, есть ли способ представить формулу smtlib2 в качестве шаблона. Например: (declare-fun b () (_ BitVec 16)) (declare-fun a () (_ BitVec 8)) (declare-fun c () (_ BitVec 32)) (assert (= c (bvor ((_ zero_extend 24) a) ((_ zero_extend …
15 фев '22 в 03:59
1
ответ
Как создать дополнительные ограничения из модели, полученной решателем в z3 Python API?
Как только у меня возникнет проблема с ограничением, я хотел бы посмотреть, выполнима ли она. На основе возвращенной модели (когда она установлена) я хотел бы добавить утверждения, а затем снова запустить решатель. Однако, похоже, я неправильно пони…
01 июн '22 в 21:35
1
ответ
Как я могу определить функцию в z3 Python API после появления нового стандарта SMT-LIB?
Новый стандарт SMT-LIB допускает команду определения функции в форме: (define-fun f ((x1 σ1) · · · (xn σn)) σ t) В спецификации уточняется, что это семантически эквивалентно (declare-fun f (σ1 · · · σn) σ) (assert (forall ((x1 σ1) · · · (xn σn)) (= …
27 апр '22 в 23:44
1
ответ
smtlib не отправляет электронное письмо на адрес электронной почты из списка столбцов кадра данных pandas
Дорогие У меня есть Code Connect to Oracle DB, получаю запрос как Daraframe и отправляю электронное письмо получателю, который существует в столбце Как я тестирую Когда я устанавливаю аргумент test_reciver на адрес электронной почты test_reciver Эле…
20 сен '22 в 11:56
1
ответ
Разбор SMTLIB с помощью Z3 C API без потери команд push, pop и check-sat
я используюZ3_parse_smtlib2_stringфункция из Z3 C API (через Haskell Z3 lib) для анализа файла SMTLIB и применения некоторых тактик для упрощения его содержимого, однако я заметил, что любойpush,popиcheck-satкоманды поглощаются этой функцией и не от…
27 июл '22 в 22:05
0
ответов
Теория массивов в Z3: (1) модель сложна для понимания, (2) не умею реализовывать функции и (3) разница с последовательностями
Следуя вопросу, опубликованному в статье Насколько выразительными могут быть массивы в Z3(Py)? Например , я выразил следующую формулу в Z3Py: Exists i::Integer s.t. (0<=i<|arr|) & (avg(arr)+t<arr[i]) Это означает: есть ли позицияi::0<…
20 сен '22 в 16:22
0
ответов
Поиск реальных решений проблемы происходит медленнее, чем ожидалось
Извините, это основной вопрос, я новичок в z3. Я написал программу для поиска действительного решения некоторого уравнения. Поскольку оно должно генерироваться для каждого уравнения, я не могу заранее сильно упростить уравнение. Но программа очень м…
30 ноя '22 в 22:34
1
ответ
Совместимы ли Int и Real как-то в SMT-LIB?
Оператор равенства в SMT-LIB обычно требует, что неудивительно, чтобы его операнды были одного типа. Например, это ошибка: (set-logic QF_LIRA) (declare-fun a () Bool) (declare-fun b () Real) (assert (= a b)) (check-sat) Однако я ожидал, что это тоже…
27 май '23 в 23:58
2
ответа
Как преобразовать модель SMT с оптимизацией с использованием библиотеки z3 в файл .smt2, распознаваемый различными решателями, такими как cvc4?
Я хочу преобразовать модель SMT, написанную на Python, с использованием библиотеки z3, в файл .smt2, чтобы получить файл, который можно запускать из разных решателей (например, cvc4-solver). Проблема в том, что моя модель выполняет оптимизацию, и пр…
20 май '23 в 14:17