z3

2зной

2ответ

list concat in z3

Есть ли способ конкатцировать два списка в z3? Как и оператор @ в ML? Я думал об определении его сам, но я не думаю, что z3 поддерживает определения рекурсивных функций, т.е. define-fun concat ((List

z3 2012-05-06

---

3зной

1ответ

Является ли Z3 минимальным неудовлетворительным ядром до сих пор?

Я хочу знать, может ли Z3 теперь дать минимальное неосязаемое ядро. Или кто-то разработал хорошую поддержку для этого? Кто-нибудь знает это? спасибо.

z3 2012-05-11

---

1зной

1ответ

Использование аксиом для вычетов в z3

Я новый пользователь для Z3 и хочу, чтобы он использовал некоторые аксиомы и только эти аксиомы, чтобы уменьшить формулу до другой эквивалентной формулы в логике первого порядка. Пример: Используйте т

c# z3 2012-05-17

---

1зной

2ответ

cross product in z3

Предоставляет ли z3 функцию перекрестного произведения для двух списков? Если нет, то можно определить один без использования функций более высокого порядка или с помощью предоставленных функций списк

z3 2012-05-17

---

1зной

1ответ

Определение sort Seq

Я хотел бы знать, что такое определение sort Seq. Я не смог найти его определение в руководстве Z3 SMT 2.0. Я понял, что Seq уже определен, потому что я пытался определить сортировку Seq. Существуют л

z3 2012-05-17

---

1зной

1ответ

Новый API Z3 .NET для фиксированной точки

Поскольку Z3 выпустила новый .NET API, мне кажется, что API для фиксированной точки изменился. Однако я не могу найти подробные сведения о том, как использовать новый API. Кто-нибудь может мне что-то

.net z3 2012-05-18

---

3зной

1ответ

Нелинейные арифметические и неинтерпретируемые функции

(declare-const x Real) (declare-fun f (Real) Real) (assert (= (f 1.0) 0.0)) (assert (= (* x x) (* 1.0 1.0))) (check-sat) (get-model) У меня есть два независимых утверждения: один в нелинейных а

z3 2012-05-19

---