math/alt-ergo 2.5.4_2 FreeBSD

Automatic solver of mathematical formulas for program verification

System: FreeBSD
Repository: FreeBSD ports
Maintainer: [email protected]
License: CeCILL-C
Categories: math
Package size: 18202.1 KiB, 69855.4 KiB installed

Description

Alt-Ergo is an automatic theorem prover dedicated to program verification. Alt-Ergo is based on CC(X), a congruence closure algorithm parameterized by an equational theory X. Currently, CC(X) can be instantiated by the empty equational theory and by the linear arithmetics. Alt-Ergo contains also a home made SAT-solver and an instantiation mechanism.

Alt-Ergo is compact, safe, and modular. Each component is described by a small set of inference rules and is implemented as an Ocaml functor.

In the other systems

System

Port

Version

FreeBSD

math/alt-ergo

2.5.4_2

DragonFly

math/alt-ergo

2.5.4_2

Install

Binary package:

pkg install alt-ergo

From the ports tree:

cd /usr/ports/math/alt-ergo/ && make install clean

To depend on this port in another port's Makefile:

RUN_DEPENDS=	alt-ergo>0:math/alt-ergo

Packages

The version each package repository carries. “-” means the repository builds no package of it, “n/a” that there is no such repository.

Repository

aarch64

amd64

armv6

armv7

i386

FreeBSD:14:latest

2.5.4_2

FreeBSD:14:quarterly

2.5.4_2

n/a

2.5.4_2

FreeBSD:15:latest

2.5.4_2

n/a

2.5.4_2

FreeBSD:15:quarterly

2.5.4_2

n/a

FreeBSD:16:latest

2.5.4_2

n/a

FreeBSD:16:quarterly

n/a

Dependencies

As this port's Makefile names them.

Build 8

${LOCALBASE}/bin/menhir : devel/menhir
${LOCALBASE}/${OCAML_SITELIBDIR}/dolmen/META : devel/ocaml-dolmen
${LOCALBASE}/${OCAML_SITELIBDIR}/num/META : math/ocaml-num
${LOCALBASE}/${OCAML_SITELIBDIR}/ocplib-simplex/META : math/ocaml-ocplib-simplex
${LOCALBASE}/${OCAML_SITELIBDIR}/ppx_blob/META : devel/ocaml-ppx_blob
${LOCALBASE}/${OCAML_SITELIBDIR}/psmt2-frontend/META : devel/ocaml-psmt2-frontend
${LOCALBASE}/${OCAML_SITELIBDIR}/zarith/META : math/ocaml-zarith
${LOCALBASE}/${OCAML_SITELIBDIR}/zip/META : archivers/ocaml-zip

Library 1

libgmp.so : math/gmp

Runtime 7

${LOCALBASE}/${OCAML_SITELIBDIR}/dolmen/META : devel/ocaml-dolmen
${LOCALBASE}/${OCAML_SITELIBDIR}/num/META : math/ocaml-num
${LOCALBASE}/${OCAML_SITELIBDIR}/ocplib-simplex/META : math/ocaml-ocplib-simplex
${LOCALBASE}/${OCAML_SITELIBDIR}/ppx_blob/META : devel/ocaml-ppx_blob
${LOCALBASE}/${OCAML_SITELIBDIR}/psmt2-frontend/META : devel/ocaml-psmt2-frontend
${LOCALBASE}/${OCAML_SITELIBDIR}/zarith/META : math/ocaml-zarith
${LOCALBASE}/${OCAML_SITELIBDIR}/zip/META : archivers/ocaml-zip

The full lists below include those, and their dependencies in turn.

Build dependencies 60

Run dependencies 59

No port depends on this one.

Configuration

Options name: math_alt-ergo

Option

Default

Description

DOCS

off

Build and/or install documentation

MANPAGES

off

Build and/or install manual pages

USES: ocaml:dune
Service scripts: none

Files

Manual pages 1

alt-ergo(1)

pkg-plist 558

bin/alt-ergo
%%OCAML_SITELIBDIR%%/alt-ergo/META
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common.cmi
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common.cmt
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__AltErgoSites.cmi
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__AltErgoSites.cmt
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__Config.cmi
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__Config.cmt
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__Input_frontend.cmi
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__Input_frontend.cmt
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__Input_frontend.cmti
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__MyDynlink.cmi
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__MyDynlink.cmt
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__MyDynlink.cmti
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__Parse_command.cmi
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__Parse_command.cmt
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__Parse_command.cmti
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__Signals_profiling.cmi
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__Signals_profiling.cmt
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__Signals_profiling.cmti
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__Solving_loop.cmi
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__Solving_loop.cmt
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/.public_cmi/alt_ergo_common__Solving_loop.cmti
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/AltErgoSites.ml
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/alt_ergo_common.a
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/alt_ergo_common.cma
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/alt_ergo_common.cmx
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/alt_ergo_common.cmxa
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/alt_ergo_common.ml
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/alt_ergo_common__AltErgoSites.cmx
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/alt_ergo_common__Config.cmx
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/alt_ergo_common__Input_frontend.cmx
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/alt_ergo_common__MyDynlink.cmx
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/alt_ergo_common__Parse_command.cmx
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/alt_ergo_common__Signals_profiling.cmx
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/alt_ergo_common__Solving_loop.cmx
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/config.ml
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/input_frontend.ml
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/input_frontend.mli
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/myDynlink.ml
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/myDynlink.mli
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/parse_command.ml
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/parse_command.mli
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/signals_profiling.ml
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/signals_profiling.mli
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/solving_loop.ml
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/solving_loop.mli
%%OCAML_SITELIBDIR%%/alt-ergo/dune-package
%%OCAML_SITELIBDIR%%/alt-ergo/opam
%%OCAML_SITELIBDIR%%/alt-ergo/plugins/FmSimplexPlugin.cma
%%OCAML_SITELIBDIR%%/alt-ergo/plugins/FmSimplexPlugin.cmxs
%%OCAML_SITELIBDIR%%/alt-ergo/__private__/alt_ergo_common/alt_ergo_common.cmxs
%%OCAML_SITELIBDIR%%/alt-ergo-lib/AltErgoLib.a
%%OCAML_SITELIBDIR%%/alt-ergo-lib/AltErgoLib.cma
%%OCAML_SITELIBDIR%%/alt-ergo-lib/AltErgoLib.cmxa
%%OCAML_SITELIBDIR%%/alt-ergo-lib/META
%%OCAML_SITELIBDIR%%/alt-ergo-lib/__private__/alt_ergo_prelude/.public_cmi/prelude.cmi
%%OCAML_SITELIBDIR%%/alt-ergo-lib/__private__/alt_ergo_prelude/.public_cmi/prelude.cmt
%%OCAML_SITELIBDIR%%/alt-ergo-lib/__private__/alt_ergo_prelude/alt_ergo_prelude.a
%%OCAML_SITELIBDIR%%/alt-ergo-lib/__private__/alt_ergo_prelude/alt_ergo_prelude.cma
%%OCAML_SITELIBDIR%%/alt-ergo-lib/__private__/alt_ergo_prelude/alt_ergo_prelude.cmxa
%%OCAML_SITELIBDIR%%/alt-ergo-lib/__private__/alt_ergo_prelude/prelude.cmx
%%OCAML_SITELIBDIR%%/alt-ergo-lib/__private__/alt_ergo_prelude/prelude.ml
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib.cmi
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib.cmt
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib.cmx
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib.ml
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Ac.cmi
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Ac.cmt
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Ac.cmti
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Ac.cmx
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Adt.cmi
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Adt.cmt
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Adt.cmti
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Adt.cmx
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Adt_rel.cmi
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Adt_rel.cmt
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Adt_rel.cmti
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Adt_rel.cmx
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Arith.cmi
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Arith.cmt
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Arith.cmti
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Arith.cmx
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Arrays.cmi
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Arrays.cmt
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Arrays.cmti
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Arrays.cmx
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Arrays_rel.cmi
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Arrays_rel.cmt
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Arrays_rel.cmti
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Arrays_rel.cmx
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Bitv.cmi
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Bitv.cmt
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Bitv.cmti
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Bitv.cmx
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Bitv_rel.cmi
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Bitv_rel.cmt
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Bitv_rel.cmti
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Bitv_rel.cmx
%%OCAML_SITELIBDIR%%/alt-ergo-lib/altErgoLib__Ccx.cmi

The first 100 are listed.

distinfo 1

File

Size

SHA256

OCamlPro-alt-ergo-v2.5.4_GH0.tar.gz

3.055761e+06

397a76979e41cb7ded7fa617924a4ea18b3a6b9d3a7cb65de15314b5e0a86e4d

Commit history 0

No commits in the history this site was built from.