Gentoo Packages

Search

Install

Install this package:

emerge -a sci-mathematics/yices2

If the package is masked, you can unmask it using the autounmask tool or standard emerge options:

autounmask sci-mathematics/yices2

Or alternatively:

emerge --autounmask-write -a sci-mathematics/yices2

Package Information

Description:

Yices 2 is an SMT solver that decides the satisfiability of formulas containing uninterpreted function symbols with equality, real and integer arithmetic, bitvectors, scalar types, and tuples. Yices 2 supports both linear and nonlinear arithmetic. Yices 2 can process input written in the SMT-LIB notation (both versions 2.0 and 1.2 are supported). Alternatively, you can write specifications using Yices 2's own specification language, which includes tuples and scalar types. You can also use Yices 2 as a library in your software.

Homepage:

https://github.com/SRI-CSL/yices2/

License:

GPL-3+

Versions

Metadata

Description

• Yices 2 is an SMT solver that decides the satisfiability of formulas containing uninterpreted function symbols with equality, real and integer arithmetic, bitvectors, scalar types, and tuples. Yices 2 supports both linear and nonlinear arithmetic. Yices 2 can process input written in the SMT-LIB notation (both versions 2.0 and 1.2 are supported). Alternatively, you can write specifications using Yices 2's own specification language, which includes tuples and scalar types. You can also use Yices 2 as a library in your software.

Maintainers

• Gentoo Mathematics Project (sci-mathematics@gentoo.org) - Type: project

Upstream

• Bugs: https://github.com/SRI-CSL/yices2/issues/
• Remote IDs:
  • github: SRI-CSL/yices2

<pkgmetadata>
	<maintainer type="project">
		<email>sci-mathematics@gentoo.org</email>
		<name>Gentoo Mathematics Project</name>
	</maintainer>
	<longdescription>
    Yices 2 is an SMT solver that decides the satisfiability of formulas
    containing uninterpreted function symbols with equality, real and integer
    arithmetic, bitvectors, scalar types, and tuples. Yices 2 supports both
    linear and nonlinear arithmetic. Yices 2 can process input written in the
    SMT-LIB notation (both versions 2.0 and 1.2 are supported). Alternatively,
    you can write specifications using Yices 2's own specification language,
    which includes tuples and scalar types. You can also use Yices 2 as a
    library in your software.
  </longdescription>
	<use>
		<flag name="mcsat">Enable support for MCSAT</flag>
	</use>
	<upstream>
		<bugs-to>https://github.com/SRI-CSL/yices2/issues/</bugs-to>
		<remote-id type="github">SRI-CSL/yices2</remote-id>
	</upstream>
</pkgmetadata>

Lint Warnings

• [Error] Missing md5-cache for ebuild yices2-2.6.5

USE Flags

Manage flags for this package: euse -i <flag> -p sci-mathematics/yices2 | euse -E <flag> -p sci-mathematics/yices2 | euse -D <flag> -p sci-mathematics/yices2

Manifest