z3 - Отличная библиотека

z3

3зной

1ответ

Инвариантная индукция над роговыми предложениями с Z3py

В настоящее время я использую Z3py для вывода некоторых инвариантов, которые кодируются как совокупность роговых предложений, в то же время предоставляя шаблон для инварианта. Сначала я начинаю с прос

0зной

1ответ

Можно ли оценить время работы z3 или время работы алгоритма DPLL (T)? Даже худший случай

Я работаю над визуализацией прототипа microsoft z3. Интересно, можно ли оценить время работы z3 или алгоритм? Даже было бы здорово, если бы я мог получить худшее время работы. Кроме того, в z3 существ

-2зной

1ответ

Есть ли способ максимизировать сумму, используя минимальные записи из списка?

Я пытаюсь найти минимальное количество записей в списке или векторе, которые составляют максимальную сумму. Есть ли способ его найти? Я пытаюсь следующим образом, но не успех: D=[[Real('d%s%s' % (i+1,

3зной

2ответ

Z3, чтобы показать, что если a^3 = x * y * z, то 3a <= x + y + z

Я полный новичок с Z3 (начался сегодня). Пока это нравится. Отличный инструмент. К сожалению, синтаксис меня немного смущает. Я хочу доказать, что если: а^3 = х у г = т(с, х, у, г, т (0..1)) тогда: 3a

1зной

1ответ

Microsoft Z3 Dot Net API, Cloning Solver

Я хочу запустить мой z3-код на несколько потоков параллельно. В моей структуре программы я сначала инициализирую свой Z3-решатель всеми утверждениями, а затем попрошу удовлетворительное решение. Есть

3зной

2ответ

Выполнение get-model или unsat-core в зависимости от решения решателя

Интересно, есть ли возможность в сценарии SMT-LIB 2.0 получить доступ к последнему решению решающей задачи решателя (sat, unsat, ...). Например, следующий код: (set-option :produce-unsat-cores true)

2зной

1ответ

Существует ли теория для неинтерпретируемых функций (анализ конгруэнтности)?

У меня есть набор символических переменных: int a, b, c, d, e; Набор неизвестных функций, сдерживается целым рядом аксиом: f1(a, b) = f2(c, b) f1(d, e) = f1(e, d) f3(b, c, e) = f1(b, e) c = f1(a,