Вопросы по теме 'smt'
Какая статистика указывает на эффективную работу 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
Почему результат запроса меняется, если прокомментировать промежуточный вызов `(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
Равенство констант в решателе Z3 SMT
Я использую решатель Z3 SMT от Microsoft и пытаюсь определить константы пользовательского вида. Кажется, что такие константы по умолчанию не являются неравными. Предположим, у вас есть следующая программа:
(declare-sort S 0)
(declare-const x...
3049 просмотров
schedule
22.06.2022
Поддерживает ли стандарт SMT-Lib комбинацию теорий?
Я знаю, что в нескольких работах пытаются разобраться с комбинацией теорий в SMT. Однако язык SMT-Lib 2.0 ( http://smtlib.cs.uiowa.edu/docs.html ) ничего не говорит об этом. Мой вопрос в том, поддерживает ли он это, и какие Solvers предлагают...
166 просмотров
schedule
09.01.2023
старая vs новая версия Z3
У меня есть экземпляр, который может быть очень эффективно решен старой версией Z3 (версия 2.18). Он возвращает SAT через несколько секунд. Однако когда я пробую его на текущей версии Z3 (версия 4.3.1). По прошествии 10 минут не возвращает никакого...
213 просмотров
schedule
29.04.2022
Haskell createProcess и чтение из Handle
когда я использую Haskell createProcess , мне нужно fork раньше, как если бы я использовал exec в c?
Из примеров, которые я видел, и того, что я пробовал, я не думаю, что делаю, но если я прочитаю из выходного дескриптора один раз, я получу...
1130 просмотров
schedule
15.09.2022
Задокументировано ли решение SMT в стиле DPLL(T) в z3 для линейной действительной арифметики?
Я пытаюсь придумать способы улучшить производительность z3 при решении моих задач. Мне известно о документе CAV'06 и технический отчет . Отличаются ли соответствующие части z3 v4.3.1 от того, что описано в этих документах, и если да, то чем?...
206 просмотров
schedule
06.08.2022
Преобразование объектов ast (или решателя) z3 C++ API в строку SMTLIB
Я играю с z3 и другими решателями SMT и хочу изучить случаи, когда другие решатели, такие как boolector, побеждают z3 и наоборот. Для этой цели мне нужен способ преобразования объявлений и утверждений в формат SMT-LIB2, который могут распознавать...
830 просмотров
schedule
31.07.2023
Как я могу написать длинное выражение smt-lib с квантором существования?
У меня есть следующее выражение
(declare-fun x00 () Real)
(declare-fun x01 () Real)
(declare-fun x10 () Real)
(declare-fun x11 () Real)
(declare-fun t0init () Real)
(declare-fun z0init0 () Real)
(declare-fun z0init1 () Real)
(assert (>= t0init...
236 просмотров
schedule
31.10.2022
muZ3: недетерминированный рекурсивный вызов
Есть ли способ выполнить недетерминированный рекурсивный вызов в спецификации отношения muZ3? В частности, я хочу перевести функцию, подобную следующей:
int foo(int x) {
...
if (*) y = foo(y);
...
}
в формат правила muZ3.
131 просмотров
schedule
14.04.2023
Как запускать вызовы SAT параллельно, используя привязки picosat haskell?
import Picosat
import Control.Applicative
main :: IO ()
main = do
dimacsList1 <- (read <$> getLine) :: IO [[Integer]]
dimacsList2 <- (read <$> getLine) :: IO [[Integer]]
res1 <- solve dimacsList1
res2 <- solve...
132 просмотров
schedule
18.05.2024
Отдельные значения массива в решателе z3 SMT
Некоторое время я пытался выполнить довольно простое требование: я объявил новый тип данных
(declare-datatypes () ((A (mk_A (key Int) (var1 Int) (var2 Int)))))
где key должен действовать как первичный ключ в базе данных, т. е. каждый...
679 просмотров
schedule
19.07.2022
z3py выдает ошибку парсера для действительного файла SMT2
1 (set-logic UFLIA)
2 (set-info :source | Simple list theorem |)
3 (set-info :smt-lib-version 2.0)
4 (set-info :category "crafted")
5 (set-info :status unsat)
6 (declare-sort List 0)
7 (declare-sort Elem 0)
8 (declare-fun cons (Elem...
768 просмотров
schedule
29.12.2022
Доступ к членам составных сортировок (типов данных) в SMT-LIBv2
Согласно разд. 3.9.3 из Язык и инструменты SMT-LIBv2: учебное пособие возможно чтобы объявить составную сортировку, подобную этой, в SMT-LIBv2:
(set-logic QF_UF)
(declare-sort Triple 3)
(declare-fun state () (Triple Bool Bool Bool))
Я...
139 просмотров
schedule
10.04.2022
При использовании Hyper Threading потоки одного физического ядра обмениваются через какой уровень кэша L1 / L2 / L3?
Позволяет ли Hyper Threading использовать L1-кеш для обмена данными между двумя потоками, которые выполняются одновременно на одном физическом ядре, но в двух виртуальных ядрах?
При условии, что оба принадлежат одному процессу, то есть в одном...
888 просмотров
schedule
23.07.2022
Битовые векторные операции Z3
Как использовать операции битового вектора «повторить» и «повернуть_влево»?
В общем, где я могу найти подробную документацию по операциям с битовыми векторами в формате сценариев SMT2, используемом Z3?
Все, что я нахожу, похоже, просто ведет к...
2258 просмотров
schedule
27.05.2023
z3py: Как правильно утверждать, что ограничение чего-то не существует?
Я хочу установить ограничение «что-то не должно существовать» в z3py. Я попытался использовать «Не (существует (...))». Простой пример таков. Я хочу найти задание для a и b, чтобы такого c не существовало.
from z3 import *
s = Solver()
a =...
377 просмотров
schedule
26.05.2022
z3, z3py: Могу ли я определить сортировку, включающую набор целых чисел?
Это дополнительный вопрос к моему предыдущему вопросу of-function">"Возможно ли существенно уменьшить пространство поиска Function" .
Я думаю, возможно ли определить сортировку, содержащую набор целых чисел, например, целые числа 1-10.
Моя...
772 просмотров
schedule
21.08.2022
Простое упражнение Z3, возвращающее неизвестное значение
Я начинаю использовать решатели SMT, и я практиковался с этой простой проблемой:
Exercise 5. Using Z3 at the restaurant:
(a) Encode the following menu choices into Z3 and determine what a customer could buy using exactly
$15.05
• Mixed fruit...
219 просмотров
schedule
15.09.2022
