Вопросы по теме 'smt'
Smtlib проблема с кодом
У меня есть следующий код
(set-logic QF_LIA)
(declare-fun w () Int)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (> x y))
(assert (> y z))
(push 1)
(assert (> z x))
(check-sat) ; unsat
(get-info...
173 просмотров
schedule
05.09.2021
Массивы и квантификатор
Я пытаюсь использовать массив и квантификатор в Z3, чтобы найти подстроку в заданном тексте.
Мой код следующий:
(declare-const a (Array Int Int))
(declare-const x Int)
;; a|A
(assert (or (= (select a 0) 61) (= (select a 0) 41)))
;; b|B
(assert...
461 просмотров
schedule
10.10.2021
Что лучше в SMT: добавить несколько утверждений или одно и?
Допустим, у меня есть два предложения, которые я хочу смоделировать в SMT, лучше добавить их как отдельные утверждения, например
(assert (> x y))
(assert (< y 2))
или добавить одно утверждение с оператором и, как это
(assert (and...
278 просмотров
schedule
18.10.2021
функция для получения полубайтов с использованием Z3 и теории битового вектора
Я пытаюсь немного узнать о z3 и теории битовых векторов. Я намерен создать функцию для получения полубайта из позиции битового вектора
Этот код возвращает кусочек:
(define-fun g_nibble(
(l ( _ BitVec 12))
(idx (Int))
) ( _ BitVec 4)...
318 просмотров
schedule
05.09.2021
Используйте Z3, чтобы определить сложность исключения квантора для BV-запросов
В настоящее время я использую Z3 C ++ API для решения запросов по битовым векторам. Некоторые запросы могут содержать квантификатор существования на верхнем уровне.
Часто исключение квантификатора является простым и может быть выполнено Z3 быстро....
129 просмотров
schedule
11.11.2021
Разница в выводе, когда решатель smtlib2 вызывается через z3 python api и непосредственно из исполняемого файла?
Я работаю с z3 python api. Когда я решаю ограничения с помощью z3 python api, решатель работает бесконечно, и никаких ошибок не возникает. Но когда одни и те же ограничения сбрасываются в виде формата smtlib2, а затем решаются с помощью исполняемого...
131 просмотров
schedule
15.09.2021
Использование define-fun-rec в SMT
В настоящее время я пытаюсь написать сценарий SMT с помощью define-fun-rec. Я тестировал как Z3, версия 4.4.2, так и CVC4, версия 1.4. Насколько я могу судить, это самые последние версии обеих, и обе поддерживают эту функцию *. Однако оба, похоже,...
915 просмотров
schedule
10.10.2021
как получить несколько решений для решателя z3 в примере формата smt2?
Как сгенерировать несколько моделей для формулы битового вектора с помощью решателя z3 в формате smt2?
При реализации кода IDEA для битового вектора создается одна модель.
Как сгенерировать все возможные модели для одного и того же, если он...
1408 просмотров
schedule
26.11.2021
Решение проблем удовлетворения ограничений в Sympy
Я пытаюсь решить несколько простых задач логической выполнимости в Sympy. Здесь я попытался решить ограничение, содержащее логический оператор Or :
from sympy import *
a,b = symbols("a b")
print(solve(Or(Eq(3, b*2), Eq(3, b*3))))
# In other...
1130 просмотров
schedule
26.09.2021
Решатель SMT с пользовательскими теориями?
Я собираюсь провести некоторую работу по проверке, в которой у меня есть регулярные древовидные грамматики в качестве базовой теории.
Z3 позволяет вам определять свои собственные вещи с помощью неинтерпретируемых функций, но это не всегда хорошо...
637 просмотров
schedule
17.09.2021
Частично интерпретируемый Const в z3
В z3 можно объявить полностью неинтерпретируемый const следующим образом:
(declare-const x Int)
Точно так же можно определить полностью интерпретируемый следующим образом:
(define-fun y () Int 3)
; y == 3
Учитывая алгебраический...
72 просмотров
schedule
24.09.2021
Извлечение фактов в движке регистрации данных Z3
Можно ли отозвать факты в движке регистрации данных Z3? Самое близкое, что я могу найти в документации, - это Z3_fixedpoint_update_rule , которую мне не удалось заставить работать так, как я хочу.
Я видел, как другие вопросы касаются отзыва с...
58 просмотров
schedule
24.09.2021
Список содержит функцию в Z3
Учитывая типичный тип данных списка:
(declare-datatypes (X)(
(Lst
(nil)
(insert
(head X)
(tail Lst)))))
Я пытаюсь создать функцию, которая возвращает, находится ли данный элемент в данном списке. Похоже, мне нужно...
251 просмотров
schedule
28.09.2021
Существуют ли подходы к руководству Z3, аналогичные ff-маркировке в CLP (FD)?
Это скорее признание моей неграмотности в области исследований в области решения, чем в отношении реального программирования; глядя на следующий канонический пример N-ферзей в Z3:
print('Solving N Queens for a {} by {} chess board'.format(n, n))
#...
54 просмотров
schedule
14.10.2021
Вывод NoneType из модели z3
Я использую MaxSMT, чтобы найти решение для набора мягких и жестких ограничений. При тайм-ауте 600 секунд выход модели, который я получаю от решающей программы, будет Nonetype для всех параметров. Я ожидал, что решатель предоставит мне неоптимальное...
68 просмотров
schedule
14.01.2022
(Под) оптимальный способ получить достоверную информацию о диапазоне при использовании ограничения SMT с Z3
Этот вопрос связан с моим предыдущим вопросом
Возможно ли получить достоверную информацию о диапазоне при использовании ограничения SMT с Z3?
Таким образом, кажется, что «эффективное» нахождение информации о максимальном диапазоне...
97 просмотров
schedule
04.03.2022
Как определить необъявленный тип в Z3 Solver
Я использую SMT Solver Z3 для устранения ограничений. Например:
(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (> a 10))
(assert (< (f a true) 100))
(check-sat)
// SAT
Однако как, если мы не знаем, какой тип переменной...
60 просмотров
schedule
08.03.2022
Как оптимизировать кусок кода в Z3? (связано с PI_NON_NESTED_ARITH_WEIGHT)
У меня есть код в z3 , который направлен на решение задача оптимизации для булевой формулы
(set-option :PI_NON_NESTED_ARITH_WEIGHT 1000000000)
(declare-const a0 Int) (assert (= a0 2))
(declare-const b0 Int) (assert (= b0 2))
(declare-const c0...
1179 просмотров
schedule
19.03.2022
Z3: Можно ли упростить только часть утверждений?
Я использую Java-API 64-разрядной версии Z3 версии 4.3.2 в Windows 7, а также 64-разрядную версию Java 7, но я не думаю, что Java необходима для ответа на этот вопрос.
Прямо сейчас я использую следующий код Java, чтобы упростить подмножество моих...
658 просмотров
schedule
28.03.2022
разница в кодировании одной и той же аксиомы
Мне интересно, в чем разница между этими двумя кодировками одной и той же аксиомы списка:
(define-sort T1 () Int)
(declare-fun list_length ( (List T1) ) Int)
(assert (forall ( (i T1) (l (List T1)) )
(ite (= l (as nil (List T1)))...
57 просмотров
schedule
05.04.2022
