Слияние кода завершено, страница обновится автоматически
Версия 4.next
Планируемые функции:
— sat.euf — новый CDCL-ядро для SMT-запросов. Расширяет механизм SAT с помощью плагинов решателя теории. Текущее состояние нестабильно, не хватает эффективного сопоставления.
— polysat — решение на уровне битовых векторов на уровне слов.
— Введение простых индукционных лемм для обработки ограниченного набора индуктивных доказательств.
Версия 4.11.0
Изменения:
— Удалены Z3_bool, Z3_TRUE, Z3_FALSE из API. Вместо них используются bool, true, false.
— z3++.h больше не включает , так как он не использовался.
— Добавлен solver.axioms2files: выводит аксиомы теории в файлы. Каждый файл должен быть неудовлетворительным.
— Добавлен solver.lemmas2console: выводит леммы на консоль.
— Удалён параметр smt.arith.dump_lemmas. Заменён на solver.axioms2files.
Версия 4.10.2
Исправления:
— Исправлена регрессия #6194, нарушающая рассуждения о модуле/остатке/делении.
— Исправлено управление областью действия пользовательского пропагатора для обратных вызовов равенства.
Версия 4.10.1
Исправление:
— Исправлена реализация mk_fresh в пользовательском пропагаторе для Python API.
Версия 4.10.0
Добавлены:
— API Z3_enable_concurrent_dec_ref, который устанавливается интерфейсами, использующими параллельный сборщик мусора для управления счётчиками ссылок. Эта функция интегрирована с привязками OCaml и исправляет регрессию, возникшую при переходе OCaml на параллельный GC. Использование этой функции для .Net и Java не интегрировано для этого выпуска. Они используют внешние очереди, которые излишне сложны.
— Предварительно объявленные объявления абстрактных типов данных в контексте, чтобы Z3_eval_smtlib2_string работал с примерами списков.
— Отладка Java-связывания для MacOS Arm64.
— Недостающие обработчики обратного вызова в тактиках для пользовательского пропагатора (спасибо Клеменсу Айзенхоферу).
— Настройка арифметического рассуждения Grobner для smt.arith.solver=6 (в настоящее время используется по умолчанию в большинстве случаев). Проверка согласованности по модулю умножения была обновлена следующим образом: — Полиномиальные равенства извлекаются из строк таблицы Simplex с использованием алгоритма конуса влияния. Ранее включались строки, где основные переменные были неограниченными. Согласно устаревшей реализации такие строки не включаются при построении полиномиальных уравнений. — Уравнения предварительно решаются, если они линейны и могут быть разделены на две группы: одна содержит одну переменную с нижней (верхней) границей, другая — более двух переменных с верхней (нижней) границами. Это позволяет избежать потери информации о границах во время завершения. — После (частичного) завершения выполните постоянное распространение для равенств вида x = 0. — После (частичного) завершения выполняйте факторизацию для факторов вида xyp = 0, где x — переменные, p — линейный.
Поддержка:
— Поддержка объявления алгебраических типов данных из интерфейса C++.
Версия 4.9.1
Исправлена ошибка:
— Выпуск исправления ошибок для обеспечения работы пакета npm.
Версия 4.9.0
Особенности:
— Собственные двоичные файлы M1 (Mac ARM64) и дистрибутив pypi. — Спасибо Изабель Гарсия Контрерас и Арье Гурфинкель за тестирование и исправления.
— API для инкрементального анализа утверждений. Описание функции приводится здесь в качестве примера: https://github.com/Z3Prover/z3/commit/815518dc026e900392bf0d08ed859e5ec42d1e43. Также обеспечивает инкрементность на уровне добавления утверждений к объекту решателя.
— Свёртка/отображение последовательностей: https://microsoft.github.io/z3guide/docs/guide/Sequences#map-and-fold. На данный момент эти функции доступны только через интерфейс SMTLIB2 (а не программный API). maxdiff/mindiff в массивах, скорее всего, будут устаревшими.
— Пользовательский пропагатор: — Добавление функций и обратных вызовов для внешнего контроля над ветвлением (спасибо Клеменсу Эйзенхоферу). — Функционирующий API dotnet для пользовательского пропагатора: https://github.com/Z3Prover/z3/blob/master/src/api/dotnet/UserPropagator.cs.
— Java Script API: — Доступны высокоуровневые объектные оболочки (спасибо Кевину Гиббонсу и Олафу Томалке).
— Тотализаторы и RC2: — Механизм MaxSAT теперь позволяет запускать RC2 с кодированием тотализатора. Тотализаторы включены по умолчанию, как показывают предварительные тесты. Данный фрагмент текста представляет собой описание различных версий программного обеспечения Z3.
В тексте описывается функционал, изменения и улучшения в каждой версии. Также упоминаются некоторые технические детали, связанные с использованием и настройкой программы.
Текст содержит примеры кода на языке SMTLib, который используется для взаимодействия с программой Z3.
Основной язык текста — английский.
— Incremental constraints during optimization set option opt.incremental = true:
— The interface Z3_optimize_register_model_eh allows to monitor incremental results during optimization. It is now possible to also add constraints to the optimization context during search. You have to set the option opt.incremental=true to be able to add constraints. The option disables some pre-processing functionality that removes variables from the constraints.
— fix breaking bug in python interface for user propagator pop; — integrate fixes to z3str3; — initial support for nested algebraic datatypes with sequences; — initiate map/fold operators on sequences — full integration for next releases; — initiate maxdiff/mindiff on arrays — full integration for next releases.
Examples:
(declare-sort Expr)
(declare-sort Var)
(declare-datatypes ((Stmt 0))
(((Assignment (lval Var) (rval Expr))
(If (cond Expr) (th Stmt) (el Stmt))
(Seq (stmts (Seq Stmt))))))
(declare-const s Stmt)
(declare-const t Stmt)
(assert ((_ is Seq) t))
(assert ((_ is Seq) s))
(assert (= s (seq.nth (stmts t) 2)))
(assert (>= (seq.len (stmts s)) 5))
(check-sat)
(get-model)
(assert (= s (Seq (seq.unit s))))
(check-sat)
— initial support for Darwin Arm64 (for M1, M2, .. users) thanks to zwimer and Anja Petkovi'c Komel for updates. Java is not yet supported, pypi native arm64 distributions are not yet supported. cmake dependency added to enable users to build for not-yet-supported platforms directly; specifically M1 seems to come up. — added functionality to user propagator decisions. Thanks to Clemens Eisenhofer. — added options for rc2 and maxres-bin to maxsat (note that there was no real difference measured from maxres on MaxSAT unweighted so default option is unchanged) — improved search for mutex constraints (at-most-1 constraints) among soft constraints for maxsat derived from approach used in rc2 sample. — multiple merges.
— elaborate user propagator API. Change id based scheme to expressions; — includes a Web Assembly ffi API thanks to Kevin Gibbons.
— fixes Antimirov derivatives for intersections and unions required required for solving non-emptiness constraints; — includes x86 dll in nuget package for Windows; — exposes additional user propagator functionality.
The release integrates various bug fixes and tuning.
Release provided to fix git tag discrepancy issues with 4.8.11.
— self-contained character theory, direct support for UTF8, Unicode character sets. Characters are by default unicode with an 18 bit range; — support for incremental any-time MaxSAT using the option opt.enable_lns. The API allows registering a callback function that is invoked on each incremental improvement to objectives.
— rewritten arithmetic solver replacing legacy arithmetic solver and on by default.
— New features: significant improvements to regular expression solving, expose user theory plugin. It is a leaner user theory plugin that was once available. It allows for registering callbacks that react to when bit-vector and Boolean variables receive fixed values. — Bug fixes: many. — Notes: the new arithmetic theory is turned on by default. It does introduce regressions on several scenarios, but has its own advantages. Users can turn on the old solver by. Настройка smt.arith.solver=2. В зависимости от обратной связи мы можем снова включить эту настройку по умолчанию обратно в smt.arith.solver=2.
Новые функции:
Примечания:
Новые требования:
Новые функции:
Используйте sat.acce=true, чтобы активировать полный набор методов обработки. По умолчанию пункты, которые «исключаются» с помощью acce, помечаются как леммы (избыточные) и удаляются сборщиком мусора, если их уровень сцепления высок.
Существенная переработка механизма рожка-разделителя.
Добавлены базовые функции для поддержки привязок Lambda.
Реализована модель сжатия для исключения локальных определений функций в моделях. Если встраивание не влечёт существенных накладных расходов, можно воспроизвести старое поведение, установив параметр верхнего уровня model_compress=false.
Интеграция нового решателя линейной целочисленной арифметики и смешанной линейной целочисленной арифметики от Льва Начмансона. Он включает несколько улучшений решения QF_LIA на основе:
— использования более качественного LP-движка, который уже является основой для QF_LRA; — включения разрезов на основе эрмитовой нормальной формы (благодаря подходам, описанным в «разрезах из доказательств» и «сокращении смеси»); — извлечения целочисленных решений из LP-решений путём выборочного ужесточения границ. Мы используем обобщение Бромбергера и Вайденбаха, которое позволяет избежать выборочных ужесточений границ (https://easychair.org/publications/paper/qGfG).
Решатель значительно эффективнее справляется с задачами категории QF_LIA и на данный момент может быть лучшим решением вашей проблемы. Новый решатель доступен только для избранных логик SMT-LIB. Они включают QF_LIA, QF_IDL и QF_UFLIA. В других теориях (пока) используется устаревший арифметический решатель. Вы можете включить новый решатель, установив параметр smt.arith.solver=6.
Удалённые функции:
— Интерполяционный API. — Механизм двойственности для ограниченных рожков-разделителей. — PDR-механизм для ограниченных рожков-разделителей. Функциональность механизма была включена в spacer в качестве одной из дополнительных стратегий. — Устаревающие API-функции были удалены из z3_api.h.
Версия 4.7.1
Новые требования:
— Использует stdbool и stdint как часть z3.
Новых функций нет.
Удалённых функций нет.
Это незначительное обновление перед серией запланированных крупных обновлений. Оно использует младшую версию 7, чтобы указать, что использование stdbool и stdint является критическим изменением для потребителей C-API.
Версия 4.6.0
Новые требования:
— Компилятор, поддерживающий C++11, для сборки Z3. — C++ API теперь требует C++11 или новее.
Новые функции (включая):
— Новый строковый решатель от Университета Ватерлоо. — Новый линейный вещественный арифметический решатель. — Изменённое поведение оптимизационных команд в интерфейсе командной строки SMT2. Значения целей больше не выводятся по умолчанию. Их можно получить, выполнив команду (get-objectives). Доступ к целям фронта Парето осуществляется путём выполнения нескольких вызовов (check-sat), пока он не вернёт unsat.
Удалённые функции:
— Поддержка SMT-LIB 1.x удалена.
Версия 4.5.0
Новые функции:
— Новые теории строк и последовательностей. — API поиска последствий «get-consequences» для вычисления набора последствий по модулю жёстких ограничений и набора предположений. Оптимизированные реализации предоставляются для конечных областей (QF_FD) и для большинства логик SMT. — Система сборки CMake (спасибо @delcypher). — Новые API-функции, включая доступ к утверждениям и анализ тестов SMT-LIB. — Обновлённый и улучшенный OCaml API (спасибо @martin-neuhaeusser). — Обновлённый и улучшенный Java API (спасибо @cheshire). — Новые средства ограничения ресурсов, позволяющие избежать недетерминированного поведения тайм-аута. Его можно включить из командной строки с помощью переключателя rlimit=. — Новая тактика упрощения и аккерманизации векторов битов (спасибо @MikolasJanota, @nunoplopes). — QSAT: новый решатель для выполнимости квантифицированных арифметических формул. См.: Bjorner, Janota: Playing with Quantified Satisfaction, LPAR 2016. Это новый решатель по умолчанию для логик LIA, LRA, NRA. Кроме того, его можно применять в качестве тактики для квантифицированных формул. Использование алгебраических типов данных
Использование алгебраических типов данных (но исключая подтермы селектора, поскольку Z3 не определяет семантику применения селектора к несоответствующему термину конструктора).
Специализированная логика QF_FD и связанный инкрементальный решатель
Специализированная логика QF_FD и связанный инкрементальный решатель (поддерживает push/pop). Область QF_FD включает битовые векторы, типы данных перечислений, используемые только в равенствах, и ограниченные целые числа: целые числа, используемые в задачах QF_FD, должны быть ограничены конечной границей.
Запросы в механизме фиксированной точки
Запросы в механизме фиксированной точки теперь являются функциональными символами, а не формулами со свободными переменными. Это делает ассоциацию свободных переменных в ответах однозначной. Чтобы эмулировать запросы над составными формулами, введите новый предикат, аргументы которого являются соответствующими свободными переменными в формуле, и добавьте правило, которое использует новый предикат в голове и формулу в теле.
Минимизация ядер unsat доступна как опция для ядер SAT и SMT.
Минимизация ядер unsat доступна в качестве опции для модулей SAT и SMT. Установив smt.core.minimize=true или sat.core.minimize=true, ядра, созданные этими модулями, минимизируются.
Исправлен ряд ошибок.
Версия 4.4.1
Этот выпуск знаменует переход на новую модель разветвления и извлечения GitHub; ветки unstable и contrib будут удалены, все новые вклады будут направляться непосредственно в основную ветку.
Исправлен ряд ошибок.
Добавлена новая функция: поддержка оптимизационных запросов. Язык команд SMT-LIB2 дополнен тремя командами (maximize ), (minimize <expr) и (assert-soft [:weight ] [:id ]). Программный API также содержит выделенный контекст для решения оптимизационных запросов. В статье Bjorner, Dung и Fleckenstein на TACAS 2015 описаны дополнительные детали, а онлайн-учебник на http://rise4fun.com/z3opt иллюстрирует некоторые варианты использования.
Версия 4.4.0
Новая функция: Поддержка теории чисел с плавающей точкой. Она представлена в виде логик (QF_FP и QF_FPBV), тактик (qffp и qffpbv), а также подключаемого модуля теории, который позволяет комбинировать теории. Z3 поддерживает официальное определение теории FP SMT (см. http://smtlib.cs.uiowa.edu/theories/FloatingPoint.smt2) в файлах SMT2, а также во всех API.
Новая функция: Стохастический локальный поисковый механизм для формул битовых векторов (см. тактику qfbv-sls). См. также: Froehlich, Biere, Wintersteiger, Hamadi: Stochastic Local Search for Satisfiability Modulo Theories, AAAI 2015.
Обновление: Этот выпуск включает совершенно новый API OCaml/ML, который гораздо лучше интегрирован с системой сборки и, надеюсь, проще в использовании, чем предыдущий.
Исправлено множество ошибок, о которых сообщили Марк Брокшмидт, Венкатеш-Прасад Ранганат, Энрик Карбонелл, Морган Детерс, Том Болл, Мальте Шверхофф, Амир Эбрахими, пользователи Codeplex rsas, clockish, Heizmann, susmitj, steimann и пользователи Stackoverflow user297886.
Версия 4.3.2
Предварительная поддержка теории чисел с плавающей запятой (тактики qffpa, qffpabv и логики QF_FPA, QF_FPABV).
Интерполяционные функции iZ3 теперь интегрированы в Z3.
Множество ошибок и несоответствий было исправлено и сообщено нам лично, по электронной почте или на Codeplex. Из тех, о которых у нас есть записи, мы хотели бы выразить нашу благодарность Владимиру Клебанову, Конраду Ямрозику, Нуно Лопесу, Карстену Рютцу, Эстебану Павесу, Томеру Вайсу, Илье Миронову, Габриэле Паганелли, Левенту Эркоку, Фабиану Эммесу, Дэвиду Коку, Этьену Кнауссу, Арлену Коксу, Мэтту Льюису, Карстену Отто, Полу Джексону, Дэвиду Моннио, Мартину Плюкеру, Жасмин Бланшетт, Жюлю Вийяру, Эндрю Гачеку, Джорджу Карпенкову, Йоргу Пфехлеру и Пабло Аледо, а также следующим пользователям Codeplex, которые либо сообщали об ошибках, либо участвовали в обсуждениях: xor88, parno, gario, Bauna, GManNickG, hanwentao, dinu09, fhowar, Cici, chinissai, barak_cohen, tvalentyn, krikunts, sukyoung, daramos, snedunuri, rajtendulkar, sonertari, nick8325, dvitek, amdragon, Beatgodes, dmonniaux, nickolai, DameNingen, mangpo, ttsiodras. Новые возможности инфраструктуры настройки параметров. Теперь можно задавать параметры для внутренних модулей Z3. Изменились названия некоторых параметров. Список новых параметров можно получить, выполнив команду z3 -p.
Добавлены функции get_version() и get_version_string() в Z3Py.
Поддержка FreeBSD. Z3 можно скомпилировать на FreeBSD с помощью g++.
Поддержка Python 3.x.
Возврат к (set-option :global-decls false) как к значению по умолчанию. В Z3 4.3.0 и Z3 4.3.1 этот параметр был установлен в true. Благодарим Жюльена Генри за сообщение об этой проблеме.
Добавлен каталог doc и скрипты для автоматического создания документации API.
Убрана зависимость от autoconf. Больше не нужно выполнять команды autoconf и ./configure для сборки Z3.
Исправлена ошибка в результате, возвращаемом Z3_solver_get_num_scopes. (Спасибо Герману Вентеру). Эта ошибка появилась в Z3 4.3.0.
Java-привязки. Чтобы включить их, необходимо использовать опцию --java при выполнении скрипта mk_make.py. Пример: python scripts/mk_make.py --java.
Исправлен сбой при анализе некорректных формул. Сбой появился при добавлении поддержки «арифметических приведений» в Z3 4.3.0.
В mk_make добавлена новая опция, позволяющая пользователям указывать, где будут установлены привязки Python (Z3Py). (Благодарим Деяна Йовановича за сообщение о проблеме).
Исправлен сбой, о котором сообщалось на сайте http://z3.codeplex.com/workitem/10.
Удалены вспомогательные константы, созданные тактикой nnf из моделей Z3.
Исправлена проблема в красивом принтере. Он не вводил кавычки для имён атрибутов, таких как |foo:10|.
Исправлена ошибка при использовании предположений (спасибо Филиппу Сутеру и Этьену Кнеуссу). Рассмотрим следующий пример: (assert F) (check-sat a) (check-sat) Если 'F' неудовлетворительно независимо от предположения 'a', и противоречие может быть обнаружено только путём выполнения распространения, то версия <= 4.3.1 может возвращать unsat sat вместо unsat unsat. Мы говорим «может», потому что у 'F' могут быть другие неудовлетворительные ядра.
Исправлена ошибка, о которой сообщалось на сайте https://stackoverflow.com/questions/13923316/unprintable-solver-model.
Исправлены таймеры в Linux и FreeBSD.
Исправлен сбой, о котором сообщалось на сайте http://z3.codeplex.com/workitem/11.
Исправлена ошибка, о которой сообщалось на сайте https://stackoverflow.com/questions/14307692/unknown-when-using-defs.
Ослаблена процедура check_logic. Теперь она автоматически принимает приведения (to_real), вводимые Z3. (Спасибо Полу Джексону). Это исправление для http://z3.codeplex.com/workitem/19.
Исправлено https://stackoverflow.com/questions/14524316/z3-4-3-get-complete-model.
Исправлены ошибки в C++ API (спасибо Андрею Куприянову).
Исправлена ошибка, о которой сообщалось на сайте http://z3.codeplex.com/workitem/23 (спасибо Полу Джексону).
Исправлена ошибка, о которой сообщалось на сайте https://stackoverflow.com/questions/15226944/segmentation-fault-in-z3 (спасибо Тяньхаю Лю).
Добавлена поддержка компиляции Z3 с использованием clang++ в Linux и OSX.
Добавлен отсутствующий параметр компиляции (-D _EXTERNAL_RELEASE) в режиме выпуска.
Исправлена ошибка во время построения модели, о которой сообщил Хайцман (http://z3.codeplex.com/workitem/5).
Примечание: мы пропустили версию 4.2 из-за ошибки при выпуске версии 4.1.2. Версия 4.1.2 была ошибочно помечена как 4.2. Спасибо Клоду Маршу за сообщение об этом. С этого момента мы также официально переходим на трёхзначную систему нумерации версий. Идея состоит в том, чтобы... Иметь более частые релизы, содержащие исправления ошибок.
Проведена реорганизация кодовой базы Z3, также появилась новая система сборки.
На всех платформах требуется установить Python 2.7.x.
В Windows можно выполнить сборку с помощью командной строки Visual Studio.
В Linux, OSX, Cygwin можно выполнить сборку, используя g++. См. README для инструкций по компиляции.
Убрана тактика mip. Она была основана на коде, который был удалён во время реорганизации кода.
Исправлены проблемы компиляции с clang/llvm. Большое спасибо Си Вану за то, что он нашёл проблему и предложил решение.
Теперь Z3 автоматически добавляет арифметические приведения типов: to_real и to_int. Опция (set-option :int-real-coercions false) отключает эту функцию. Если SMTLIB2_COMPLIANT=true в командной строке, то :int-real-coercions также устанавливается в значение false.
По умолчанию SMTLIB2_COMPLIANT имеет значение false. Используйте параметр командной строки SMTLIB2_COMPLIANT = true, чтобы включить его обратно.
Добавлены команды «make install-z3py» и «make uninstall-z3py» в Makefile.in.
Исправлен сбой/ошибка в упрощателе. Сбой происходил, когда использовалась опция «:sort-sums true».
Очищены примеры c++, maxsat, test_mapi.
Файлы RELEASE_NOTES перемещены в дистрибутив исходного кода.
Удалены ненужные файлы из дистрибутива исходного кода.
Из z3-prover.sln удалены ненужные режимы компиляции.
Z3 по умолчанию переключается на инкрементный решатель, когда объект Solver используется для решения многих запросов. В этой версии мы возвращаемся к тактической структуре, если инкрементный решатель возвращает «неизвестно».
Разрешены отрицательные числа во внешнем интерфейсе SMT 2.0. То есть парсер Z3 SMT 2.0 теперь принимает такие числа, как «-2». Больше не нужно кодировать их как «(- 2)». Парсер по-прежнему принимает -foo как символ. То есть это не сокращение для (- foo). Эта функция отключается, когда в командной строке установлено значение SMTLIB2_COMPLIANT = true.
Теперь Z3 можно скомпилировать внутри cygwin с помощью gcc.
Исправлена ошибка в генерации ядра неудовлетворительности.
Первый выпуск исходного кода (2 октября 2012 г.)
Исправлена ошибка в Z3Py. Метод, который создаёт приложения Z3, мог дать сбой, если один из аргументов необходимо было «привести» к правильному виду (спасибо Денису Юричеву).
Исправлена ошибка в теории типов данных (спасибо Айрату).
Исправлена ошибка в определении MkEmptySet и MkFullSet в .Net API.
При включённой автоматической конфигурации (AUTO_CONFIG = true) отображается предупреждающее сообщение и игнорируется параметр CASE_SPLIT = 3,4 или 5 (спасибо Тобиасу с StackOverflow).
Предикаты <, <=, > и >= стали цепочечными, как определено в стандарте SMT 2.0 (спасибо Маттиасу Вейлеру).
Добавлена поддержка чисел в научной нотации в Z3_ast Z3_mk_numeral(__in Z3_context c, __in Z3_string numeral, __in Z3_sort ty).
Новые встроенные символы в арифметической теории: pi, euler, sin, cos, tan, asin, acos, atan, sinh, cosh, tanh, asinh, acosh, atanh. Первые два являются константами, а остальные — унарными функциями. Эти символы недоступны, если указана логика SMT 2.0 (например, QF_LRA, QF_NRA, QF_LIA и т. д.), поскольку эти символы не определены в этих логиках. То есть новые символы доступны только в том случае, если логика не указана.
Версия 4.1
CodeContracts в .NET API (большое спасибо Франческо Логодзо). Пользователи теперь могут проверить, правильно ли они используют .NET API, с помощью Clousot.
Добавлена опция :error-behavior. По умолчанию используется continued-execution. Теперь пользователи могут заставить внешний интерфейс Z3 SMT 2.0 завершать работу всякий раз, когда сообщается об ошибке. Им просто нужно использовать команду (set-option: error-behavior immediate-exit).
Исправлена ошибка в устранении термина if-then-else (спасибо Артуру Неядомскому).
Исправлена ошибка в коде обнаружения логики различий (спасибо Деяну). - Исправлена ошибка в препроцессоре псевдобулевых выражений (спасибо Адриену Чемпиону).
Исправлена ошибка в правилах препроцессинга bvsmod (спасибо Деяну Йовановичу).
Исправлена ошибка в Tactic tseitin-cnf (спасибо Георгу Хофереку).
Добавлен недостающий шаг упрощения в nlsat.
Исправлена ошибка при построении модели для линейной вещественной арифметики (спасибо Марчелло Берсани).
Исправлена ошибка в препроцессоре, который устранял рациональные степени (например, (^ x (/ 1.0 2.0))), ошибка затрагивала только задачи, где знаменатель был чётным (спасибо Йоханнесу Эрикссону).
Исправлена ошибка в операции k-го корня в пакете алгебраических чисел. Результат был правильным, но результирующий полином мог быть неправильно помечен как минимальный и вызывать бесконечный цикл при операциях сравнения. (Спасибо Йоханнесу Эрикссону.)
Исправлена ошибка, влияющая на задачи, содержащие шаблоны с n-арными арифметическими выражениями, такими как (p (+ x y 2)). Эта ошибка была введена в Z3 4.0. (Спасибо Полу Джексону.)
Исправлен сбой при нехватке памяти.
Исправлен сбой, о котором сообщил Алекс Саммерс. Сбой происходил в сценариях, содержащих кванторы, и использующих булевы формулы внутри терминов.
Исправлен сбой в модуле MBQI (спасибо Стефану Фальке).
Исправлена ошибка в механизме E-matching. Он пропускал экземпляры мультипаттернов (спасибо Алексу Саммерсу).
Исправлена ошибка в симпатичном принтере Z3Py.
Модуль вывода шаблонов больше не генерирует предупреждающие сообщения по умолчанию. Этот модуль отвечал за создание сообщений типа: «ПРЕДУПРЕЖДЕНИЕ: не удалось найти шаблон для квантификатора (идентификатор квантификатора: k!199)». Опцию PI_WARNINGS=true можно использовать для включения этих предупреждающих сообщений.
В z3++.h добавлены отсутствующие операторы возврата (спасибо Дэниелу Нейдеру).
Убрана поддержка форматов ввода TPTP5 и Simplify.
Убрана поддержка формата ввода Z3 (низкоуровневого). Он всё ещё доступен в API.
Убрана поддержка входного формата «SMT 1.5» (также известного как файлы .smtc). Это был гибридный входной формат, реализованный во время разработки стандарта SMT 2.0. Пользователи должны перейти на формат SMT 2.0. Обратите внимание, что формат SMT 1.0 всё ещё доступен.
Тактика tseitin-cnf стала более «дружелюбной». Она автоматически применяет необходимые преобразования, чтобы устранить такие операторы, как and, distinct и т. д.
Реализован новый алгоритм PSC (главных субрезультантных коэффициентов). Это было одним из узких мест в новом решателе/тактике nlsat.
Z3 4.0 — это крупный релиз. Основные новые функции: — Новый C API, обратно совместимый, но некоторые методы помечены как устаревшие. В новом API многие решатели могут быть созданы в одном контексте. Также он включает поддержку пользовательских стратегий с использованием тактик. Кроме того, он предоставляет новый интерфейс для просмотра моделей.
— Тонкий слой C++ вокруг C API, иллюстрирующий, как использовать подсчёт ссылок объектов ast. Несколько примеров можно найти в каталоге examples/c++.
— Новый .NET API вместе с обновлённой версией устаревшего .NET API. Новый .NET API поддерживает новые функции, тактики, решатели, цели и интеграцию с подсчётом ссылок. Время жизни терминов и видов больше не требует дисциплины области видимости.
— Z3Py: Python-интерфейс для Z3. Охватывает все основные функции Z3 API.
— Решатель NLSAT для нелинейной арифметики.
— Алгоритм PDR в muZ.
— iZ3: интерполирующий пролог, построенный на основе Z3 (см. документацию iz3). iZ3 доступен только для Windows и Linux.
— Новая инфраструктура логирования. Логи Z3 используются для записи каждого вызова API Z3, выполненного вашим приложением. Если вы обнаружите ошибку, достаточно отправить журнал команде Z3. Следующие API были удалены: Z3_trace_to_file, Z3_trace_to_stderr, Z3_trace_to_stdout, Z3_trace_off. API: Z3_open_log, Z3_append_log и Z3_close_log больше не получают Z3_context. При создании журнала необходимо вызвать Z3_open_log перед любым... Другие вызовы функций Z3.
Новые логи содержат больше деталей. Однако у них есть два ограничения:
Z3 (для Linux и OSX) больше не зависит от GMP. Макросы обратной совместимости Z3 1.x определены в z3_v1.h. Если вы всё ещё используете их, вам необходимо явно включить этот файл. Исправлены все ошибки, о которых сообщалось на Stackoverflow.
Временно отключены следующие функции:
Эти две функции вернутся в будущих выпусках.
Вот список всех устаревших функций.
Это обновление исправляет проблемы, о которых сообщалось в версии 3.1. Добавлена поддержка цепных и правоассоциативных атрибутов. Исправлена генерация моделей для логики QBVF (также известной как UFBV). Теперь Z3 официально поддерживает логики BV и UFBV. По сути, это QF_BV и QF_UFBV с квантификаторами. Исправлена ошибка в командах eval и get-value. Спасибо Левенту Эркоку. Исправлена проблема с производительностью, которая влияла на VCC и Slayer. Спасибо Михалу Москалю. Исправлено измерение времени на Linux. Спасибо Айрату Халимову. Исправлена ошибка деструктивного разрешения равенства (DER=true). Исправлена ошибка оператора map в теории массивов. Спасибо Шазу Куадеру. Улучшены сценарии сборки OCaml для Windows. Спасибо Джошу Бердайну. Исправлен сбой в MBQI (когда использовались переменные Real). Исправлены ошибки в устранении кванторов. Спасибо Джошу Бердайну. Исправлен сбой при использовании недопустимого объявления типа данных. Исправлена ошибка в парсере SMT2. Исправлен сбой быстрой проверки для количественных формул. Спасибо Свену Джейкобсу. Исправлена ошибка упростителя bvsmod. Спасибо Тревору Хансену. Новые API: Z3_substitute и Z3_substitute_vars. Исправлен сбой в MBQI. Спасибо Деяну Йовановичу.
Это обновление исправляет проблемы, о которых сообщалось в версии 3.0. Исправлена ошибка генерации модели. Спасибо Арлену Коксу и Гордону Фрейзеру. Исправлена ошибка Z3_check_assumptions, из-за которой её нельзя было использовать между выполнимыми экземплярами. Спасибо Кристофу Ходеру. Исправлены две ошибки устранения кванторов. Спасибо Джошу Бердайну. Исправлены ошибки препроцессора. Исправлена проблема с производительностью в MBQI. Спасибо Кэтрин Столи. Улучшена стратегия для логики QBVF (также известная как UFBV). Добавлена поддержка отрицательных предположений в команде check-sat.
Полностью совместимый интерфейс SMT-LIB 2.0 (SMT2). Старый интерфейс по-прежнему доступен (параметр командной строки -smtc). Руководство Z3 описывает новый интерфейс. Параметрические индуктивные типы данных и параметрические пользовательские типы. Новый SAT-решатель. Z3 также может читать формулы ввода dimacs. Новый решатель Bitvector (QF_BV). Новый решатель доступен только при использовании нового интерфейса SMT2. Значительные улучшения производительности. Новый стек предварительной обработки. Улучшения производительности для линейной и нелинейной арифметики. Улучшения доступны только при использовании интерфейса SMT2. Добавлен API для анализа файлов SMT2. Исправлена ошибка AUTO_CONFIG=true. Спасибо Альберто Гриджио. Исправлена ошибка кэша упростителя Z3. Он не сбрасывался во время возврата. Спасибо Альберто Гриджио. Исправлено множество других ошибок, о которых сообщали пользователи. Улучшено создание экземпляров модели на основе квантификатора (MBQI). Новый решатель для квантифицированной логики битовых векторов (QBVF). Z3 проверяет указанную пользователем логику. TPTP. managed API.
Версия 2.8
Были добавлены следующие функции:
В этом выпуске исправлены следующие ошибки:
Версия 2.7
Были добавлены следующие функции:
В этом выпуске были исправлены следующие ошибки:
Версия 2.6
Этот выпуск исправляет несколько ошибок. Спасибо Марко Кяэрэмесу за сообщение об ошибке в сильном упростителе контекста и Джошу Бердайну.
Также этот выпуск представляет некоторые новые функции предварительной обработки:
Версия 2.5
Эта версия представляет следующие функции:
Он также исправляет ошибки, о которых сообщили Энрик Родригес Карбонелл, Нуно Лопес, Джош Бердайн, Итан Джексон, Роб Куигли и Лукас Кордейру.
Версия 2.4
Эта версия вводит следующие функции:
Предварительная поддержка SMT-LIB2.
Исправлены следующие ошибки:
Спасибо Михалу Москалю, Саше Бёме и Итану Джексону.
Этот выпуск представляет следующие функции:
утилиты цитирования F#. В выпуске есть новый каталог «utils». Он содержит утилиты, созданные на основе Z3. Основная из них — поддержка перевода цитируемых выражений F# в формулы Z3.
конфигурация QUANT_ARITH. Полное устранение квантификатора для линейной вещественной и линейной целочисленной арифметики. QUANT_ARITH=1 использует метод Ферранте/Раккоффа для вещественных чисел и метод Купера для целых чисел. QUANT_ARITH=2 использует метод Фурье-Моцкина для вещественных и тест Омега для целых чисел.
Исправлены следующие ошибки:
Благодарим Кателина Хритку, Николая Тиллмана и Сашу Бёме.
В этом выпуске исправлены незначительные ошибки. Введены некоторые дополнительные функции во внешнем интерфейсе SMT-LIB, чтобы упростить анализ новых операторов в теории массивов. Они описаны в \ref smtlibext.
Это релиз с исправлением ошибок. Большое спасибо Роберту Бруммайеру, Карине Паскаль, Франсуа Реми, Раджешу К. Кармани, Роберто Люблинерману и многим другим за их отзывы и отчёты об ошибках.
Вы можете оставить комментарий после Вход в систему
Неприемлемый контент может быть отображен здесь и не будет показан на странице. Вы можете проверить и изменить его с помощью соответствующей функции редактирования.
Если вы подтверждаете, что содержание не содержит непристойной лексики/перенаправления на рекламу/насилия/вульгарной порнографии/нарушений/пиратства/ложного/незначительного или незаконного контента, связанного с национальными законами и предписаниями, вы можете нажать «Отправить» для подачи апелляции, и мы обработаем ее как можно скорее.
Опубликовать ( 0 )