smt

1зной

1ответ

Как определить перечисляемые типы в SMT-LIB для Z3

я ранее использовал API Z3 для определения перечисляемого типа как так let T = ctx.MkEnumSort("T", [| "a"; "b"; "c"|]) , который перечисляет элементы типа T как «а» «б» и «c» (и ничего больше). Одна

z3 smt 2014-09-16

---

2зной

1ответ

Можно ли моделировать ассоциативные массивы в z3?

Мне интересно, поддерживает ли z3 ассоциативные массивы (aka maps)? Если нет, то есть простой способ моделирования таких структур данных с использованием текущей версии z3?

z3 smt 2014-11-15

---

5зной

1ответ

Использование тактики Z3 QFNRA с типами данных: взаимодействие или вставка

В Non-linear arithmetic and uninterpreted functions Леонардо де Мора утверждает, что тактика qfnra-nlsat еще не полностью интегрирована с остальной частью Z3. Я думал, что ситуация изменилась через дв

z3 smt nonlinear-functions 2014-11-19

---

0зной

1ответ

Решение уравнений проекционной функции с использованием SMT в Z3

Я пытаюсь использовать Z3 для решения уравнений с участием неизвестных проекционных функций, чтобы найти правильную интерпретацию функций, удовлетворяющих уравнению. Так, например, для уравнения: snd

z3 smt algebraic-data-types theorem-proving unification 2014-10-01

---

0зной

1ответ

В SMT-LIB существует ли разница между массивом и функцией no-arg, которая возвращает массив?

Являются ли следующие два объявления/команды семантически идентичными на языке SMT-LIB? (declare-fun a1() (Array Index Element)) (declare-const a2 (Array Index Element)) С Z3 утверждение, применимо

arrays z3 smt 2014-10-09

---

3зной

2ответ

Почему Z3 говорит, что это уравнение не является выполнимым, когда у меня есть правильный ввод?

Учитывая простую операцию сдвига и XOR-, где «вход» является символическим: input = BitVec('input',32) feedback = 0x8049d30 shiftreg = input^feedback shiftreg = 0xffffffff & ((shiftreg << 8) | (shi

math z3 xor solver smt 2014-08-27

---

3зной

1ответ

Четкие значения массива в z3 SMT решатель

Я попытался вокруг некоторое время, чтобы получить довольно простое требование сделать: Я объявил новый тип данных (declare-datatypes() ((A (mk_A (key Int) (var1 Int) (var2 Int))))) где key должен дей

z3 smt 2014-08-29

---

3зной

1ответ

Удивляет поведение при попытке доказываем FORALL

Рассмотрим следующий SMT-LIB код: (set-option :auto_config false) (set-option :smt.mbqi false) ; (set-option :smt.case_split 3) (set-option :smt.qi.profile true) (declare-const x Int) (declare-

triggers z3 smt quantifiers 2014-09-02

---

1зной

1ответ

z3 "больше, чем" полностью упорядоченное отношение

Я хотел создать последовательность SMT, чтобы у меня было полное упорядочение, которое должно быть полным. Пример 1: a < b и b < c должны быть выполнимы Примера 2: a < b и c < d должен быть невыполним

z3 smt 2014-09-23

---