Это команда z3, которую можно запустить в бесплатном хостинг-провайдере OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
z3 - ультрасовременное средство доказательства теорем от Microsoft Research
СИНТАКСИС
z3 [кредита] [-file:] файл
ОПИСАНИЕ
Эта страница руководства кратко документирует z3 команда.
z3 Z3 - это ультрасовременное средство доказательства теорем от Microsoft Research. Его можно использовать для
проверить выполнимость логических формул по одной или нескольким теориям. Z3 предлагает
убедительно сочетаются с инструментами анализа и проверки программного обеспечения, поскольку несколько общих
программные конструкции отображаются непосредственно в поддерживаемых теориях.
вход формат
-смт Используйте синтаксический анализатор для входного формата SMT.
-смт2 Используйте синтаксический анализатор для входного формата SMT 2.
-дл Используйте синтаксический анализатор для входного формата журнала данных.
-димаки
Используйте синтаксический анализатор для входного формата DIMACS.
-журнал Используйте парсер для формата ввода журнала Z3.
-in Считайте формулу из стандартного ввода.
Прочее
-h | -?
Распечатывает информацию об использовании.
-версия
Печатает номер версии Z3.
-v: уровень
Будьте многословны, где уровень детализации.
-ну Отключить предупреждающие сообщения.
-p Отображение глобальных (и модульных) параметров Z3.
-pd Отображение описаний глобальных параметров (и модулей) Z3.
-pm: имя
Модуль дисплея Z3 параметры.
-pp: имя
Отобразить описание параметра Z3, если не указан, то все имена модулей
перечислены.
-- Предполагается, что все остальные аргументы являются частью имени входного файла. Этот вариант
позволяет Z3 читать файлы со странными именами, например: -foo.smt2.
Ресурсы
-T: тайм-аут
Установите время ожидания (в секундах).
-t: тайм-аут
Установите мягкий тайм-аут (в миллисекундах). Убивает только текущий запрос.
-память: мегабайты
Установите ограничение на потребление виртуальной памяти.
Результат
-st Показать статистику.
Параметр установка
Глобальные параметры и параметры модуля можно установить в командной строке. Используйте 'z3 -p' для полной
список глобальных и модульных параметров.
param_name = значение
Для настройки глобальных параметров.
module_name.param_name = значение
Для настройки параметров модуля.
Используйте z3 онлайн с помощью сервисов onworks.net
