Описание тега smt
Теории выполнимости по модулю (SMT) - это проблемы решения логических формул относительно комбинаций фоновых теорий, выраженных в классической логике первого порядка с равенством.
1
ответ
Может ли z3 прочитать выходной файл MathSAT как его входной файл?
Мне нужно провести несколько экспериментов с использованием z3 и mathsat. Я уже закончил эксперименты с mathsat. Написание входного файла для mathsat занимает много времени, и я не хочу снова записывать входные файлы для z3. Mathsat поддерживает соз…
04 янв '13 в 12:22
0
ответов
SMT Solver в ядре Linux
Есть ли способ вызвать решатель SMT, например, Yices или STP, из ядра Linux? Я хочу реализовать символический механизм выполнения и, следовательно, мне нужно решать ограничения во время выполнения. Заранее спасибо!
15 июн '14 в 10:57
1
ответ
Невозможно извлечь значение для Z3 EnumSort в z3py
В настоящее время я пытаюсь закодировать проблему в Z3, и я хочу смоделировать "трехуровневый" логический (то есть, логический с true, false а также unknown). Вот как я смоделировал это: #!/usr/bin/env python import z3 from collections import Ordere…
17 окт '17 в 12:41
1
ответ
Как выполнять SAT-вызовы параллельно, используя привязки haskell picosat?
import Picosat import Control.Applicative main :: IO () main = do dimacsList1 <- (read <$> getLine) :: IO [[Integer]] dimacsList2 <- (read <$> getLine) :: IO [[Integer]] res1 <- solve dimacsList1 res2 <- solve dimacsList2 put…
25 май '14 в 15:55
0
ответов
SMTPAuthenticationError: (535, "Ошибка аутентификации 5.0.0")
Я использую код Python для отправки электронного письма из моей учетной записи Hotmail. Код, который я использую: def initmail(): signin() ##if "gmail" in username: ## server = smtplib.SMTP('smtp.gmail.com', 587) ##if "hotmail" in username: server =…
30 янв '16 в 08:47
0
ответов
Моделирование вектора / массива фиксированного размера в Boogie
Я пытаюсь моделировать векторы фиксированной длины в буги. Каждый вектор с разным размером должен быть другого типа. Я попробовал два подхода, но у обоих есть особая проблема. Подход 1: Тип псевдонимов Определите псевдоним типа и некоторые аксиомы, …
26 июл '18 в 08:35
2
ответа
Распределение M экспериментов по N лабораториям при соблюдении ограничений
У меня следующая проблема: я должен выделить K экспериментов для N лабораторий, соблюдая при этом некоторые общие ограничения и некоторые конкретные. Основные из них: каждый эксперимент должен быть отнесен именно к R labs максимальное количество экс…
25 янв '19 в 14:26
2
ответа
Решение SAT с библиотекой haskell SBV: как создать предикат из проанализированной строки?
Я хочу разобрать String это изображает формулу высказывания, а затем найти все модели формулы высказывания с помощью решателя SAT. Теперь я могу разобрать пропозициональную формулу с пакетом hatt; увидеть testParse функция ниже. Я также могу запусти…
23 апр '14 в 02:55
1
ответ
Печать внутренних решающих формул в z3
Инструмент доказательства теорем z3 занимает много времени, чтобы решить формулу, с которой, я думаю, она сможет легко справиться. Чтобы лучше понять это и, возможно, оптимизировать мой ввод в z3, я хотел увидеть внутренние ограничения, которые z3 г…
27 окт '12 в 18:09
1
ответ
Упрощенное выражение: Z3 SMT Solver
Выполнение следующего запроса с помощью решателя Z3: (assert (exists ((c0_s Int) (c1_s Int) (c2_s Int)) (and (= (+ c0 c1 c2) 5) (>= c0 0) (>= c1 1) (>= c2 1) (= c0_s c0) (= c1_s (- c1 1)) (= c2_s (+ c2 1)) (= c2_s 3) (= (+ c0_s c1_s) 2) )) …
02 окт '15 в 10:07
1
ответ
Можно ли использовать iZ3 для извлечения симметричных интерполантов
Я хотел бы знать, как iZ3 может использоваться для извлечения симметричных интерполантов. Внутренне iZ3 использует FOCI, а FOCI имеет симметричное интерполяционное извлечение. FOCI не принимает формат smt. Поэтому я хотел бы знать, есть ли какой-либ…
22 янв '14 в 02:22
2
ответа
Поддерживает ли стандарт SMT-Lib сочетание теорий?
Я знаю, что несколько работ пытаются справиться с сочетанием теорий в SMT. Однако язык SMT-Lib 2.0 ( http://smtlib.cs.uiowa.edu/docs.html) ничего не говорит об этом. У меня вопрос, поддерживает ли он это, и что Солверс предлагает способность работат…
31 май '13 в 19:19
1
ответ
Как работает пошаговое решение в Z3?
У меня есть вопрос относительно того, как Z3 постепенно решает проблемы. Прочитав некоторые ответы здесь, я нашел следующее: Существует два способа использования Z3 для пошагового решения: один - режим push/pop(стек), другой - использование предполо…
07 май '13 в 14:46
1
ответ
Как представить константу с плавающей точкой (например, 1e307) в стандарте SMT-LIB?
В настоящее время я провожу некоторые эксперименты на Z3 и не имею представления представлять константу с плавающей запятой (например, 1e307) в SMT: (declare-const a Real) (assert (= a 1e+307)) (check-sat) Та же проблема произошла в теории FPA: (dec…
12 окт '15 в 08:58
1
ответ
Сокращение количества используемых предложений с использованием цели доказательства в Z3
Я экспериментирую с оптимизацией использования Z3 для доказательства фактов о теории первого порядка. В настоящее время я задаю теорию первого порядка в Python, обосновываю квантификаторы и отправляю все предложения вместе с отрицанием цели доказате…
21 дек '12 в 20:49
1
ответ
Устранение переменных в решателях SAT/SMT
В решении SMT/SAT, есть ли метод для определения не относящихся к делу переменных из формулы? т.е. те, которые могут иметь любое значение и не влиять на выполнимость формулы.
13 сен '12 в 22:08
1
ответ
Как определить количество решений данного экземпляра с помощью Mathsat
Mathsat поддерживает команду check-allsat и Z3 не поддерживает его. Пожалуйста, рассмотрите следующий пример: (declare-fun m () Bool) (declare-fun p () Bool) (declare-fun b () Bool) (declare-fun c () Bool) (declare-fun r () Bool) (declare-fun al () …
05 ноя '13 в 01:43
1
ответ
z3py: как проверить информацию трассировки при использовании z3 python api
Предположим, я хочу проверить информацию трассировки "random_split". я написал enable_trace("random_split") в моем скрипте Python, который использует Z3 Python API, но ничего не появляется. Интересно, как мне проверить информацию трассировки при исп…
24 ноя '15 в 16:31
2
ответа
SMT решатели для битовой векторной арифметики
Я планирую несколько экспериментов по символическому исполнению кода на языке C, используя готовый SMT-решатель, и задаюсь вопросом, какой решатель использовать; например, рассматривая участников конкурса SMT и принимая только системы с открытым исх…
07 июн '11 в 10:33
1
ответ
Определение функции в Z3 ее реализацией Java?
Вот что я пытаюсь сделать. Допустим, я хочу найти значение op используя Z3 (и его Java-привязку) в выражении, похожем на это: ((exists (op Int)) (= (foo op) 2) Поэтому я хочу вызвать функцию foo на op переменная и проверьте, для каких значений op бу…
22 май '16 в 13:38