yices2 を Homebrew, apk, dnf, MacPorts, Nix, pacman でインストール

プロジェクトリンク

• ホームページ
• リポジトリ
• 上流ドキュメント
• パッケージマネージャページ

コマンドとエイリアス

• yices
• yices-sat
• yices-smt
• yices-smt2

プロジェクトの歴史

Yices comes from SRI International's Computer Science Laboratory and the formal-methods lineage around Bruno Dutertre and collaborators. The Yices web site says Yices 2 decides formulas over uninterpreted functions with equality, real and integer arithmetic, bitvectors, scalar types, and tuples, including linear and nonlinear arithmetic.

The documentation page anchors Yices 2 in the SMT research literature: the Yices 2.2 tool paper was presented at CAV 2014, while related technical background includes SMT tutorials, arithmetic-solver papers, MCSAT work, and applications to exists/forall problems and synthesis.

The GitHub repository was created in November 2014 and contains source, documentation, tests, and examples. Later release notes show continuing solver work: unsat cores and SMT-LIB 2.5 support in 2.6.0, bit-vector support and optional SAT backends in 2.6.2, interpolation and Kissat backend support in 2.6.4, arrays and thread-safety work in 2.6.5, and finite-field support in 2.7.0.

採用の歴史

Yices 2 is adopted in the formal-methods and verification world rather than as an end-user desktop CLI. Its official site documents installation with Homebrew on macOS and apt on Debian/Ubuntu via SRI's formal-methods PPA, and the repository provides examples plus multiple language bindings for embedding.

For package managers, Yices 2 matters because it is both a command suite and a native library. The README distinguishes executables, dynamic library, headers, source builds, optional MC-SAT support, and optional thread-safety builds.

使われ方

Typical CLI usage feeds SMT-LIB files to yices-smt2 and asks for satisfiability and models. The README includes examples for linear real arithmetic, bit-vectors, and nonlinear real arithmetic, all producing sat models.

Advanced users can embed the C API or use language bindings, build documentation, enable MC-SAT for nonlinear arithmetic and theory combination, run a portfolio script over hard SMT2 problems, or build a thread-safe library configuration when separate contexts are used per thread.

パッケージ好きにとっての重要性

Yices 2 is a heavyweight scientific package with a deceptively small command-line surface. Package maintainers care about it because optional solver backends, headers, libraries, bindings, documentation, and platform binaries all affect whether downstream verification tools can rely on the installed package.

It also illustrates a common formal-methods packaging pattern: research-grade solver, command-line frontends, C library, SMT-LIB compatibility, and cross-language bindings all distributed from one upstream.

タイムライン

• 2006: SRI-related linear-arithmetic solver papers form part of the technical background documented by Yices.
• 2014: Yices 2.2 tool paper presented at CAV and the public yices2 GitHub repository created.
• 2017-08: Yices 2.5.3 release synchronized with Debian packages.
• 2018-06: Yices 2.6.0 adds unsat cores and improved SMT-LIB 2.5 support.
• 2020-04: Yices 2.6.2 adds bit-vector support in MCSAT and optional SAT backends.
• 2021-10: Yices 2.6.4 stable release published.
• 2024-06: Yices 2.6.5 adds arrays support in MCSAT and thread-safety work.
• 2025-07: Yices 2.7.0 adds finite-field support and MCSAT improvements.

Related projects

• SMT-LIB: standard input language supported by Yices 2.
• libpoly and CUDD: optional dependencies documented for MC-SAT builds.
• CaDiCaL, CryptoMiniSAT, and Kissat: optional SAT backend families mentioned in release notes.
• SRI formal-methods tools: adjacent tools distributed by SRI's Computer Science Laboratory.

ソース

• https://api.github.com/repos/SRI-CSL/yices2 - repository creation date and project metadata.
• https://github.com/SRI-CSL/yices2 - README with examples, APIs, bindings, source-build options, MC-SAT, and thread-safety notes.
• https://github.com/SRI-CSL/yices2/releases - release history and feature notes.
• https://yices.csl.sri.com/ - official overview, supported theories, distribution channels, release information, and acknowledgements.
• https://yices.csl.sri.com/yices2-documentation.html - official documentation page and research background.