ELINAplusplus

ELINA (ETH Library for Numerical Analysis) provides optimized numerical abstract domains for static analysis. This tree contains the native ELINA API and the following domains:

• Octagons
• Convex polyhedra
• Zones
• Boxes and zonotopes

The APRON compatibility layer and the neural-network verification components are intentionally not part of this build.

High-level APIs

The supported public interface is a stable C ABI with C++ and Python wrappers, following Z3's API layering:

#include <elina/elina.hpp>

elina::context ctx(elina::domain::octagon);
elina::environment env(ctx, {}, {"x", "y"});
elina::expr x(env.var("x"));
elina::expr y(env.var("y"));
auto state = env.top().assume(0 <= x, x <= 10).assign(y, x + 1);
auto bounds = state.bound(y);

API 2.0 covers the complete retained analysis surface: mathematical objects, tree and linear expressions, strict and modular constraints, lattice and transfer operations, safe widening, weak and conditional assignment, backward transfer, fixed-width integer operations, explicit dimension transforms, generators/rays, partitions, domain inspection, portable and native persistence, and direct domain conversion. Missing native algorithms use sound generic implementations and report precision loss. Domain-specific operations, such as octagon epsilon widening, report NONE on unrelated domains.

See the API guide, capability matrix, and migration guide. Implementation-level headers are available only through their module-qualified paths under include/elina.

Repository layout

include/elina/       Stable public C and C++ headers
  core/              Core engine headers matching lib/elina/core
  domains/           Domain headers matching lib/elina/domains
  linearize/         Linearization headers matching lib/elina/linearize
  support/           Support headers matching lib/elina/support
lib/elina/           Native library implementations, mirroring include/elina
  api/               Stable C ABI implementation
  core/              Core numerical objects and managers
  domains/           Octagon, polyhedra, zones, and zonotope engines
  linearize/         Expression linearization
  support/           Shared implementation utilities
bindings/python/     Python package and native-wheel build
abi/                 Stable C ABI symbol manifest
tests/               Tests organized by responsibility
  unit/              Focused component tests
  regression/        Engine bug regressions
  integration/       Public API and installed-package consumers
  scenarios/         Cross-domain semantic scenarios
  smoke/             Native domain smoke tests
  contracts/         ABI, generated-doc, and repository-layout contracts
examples/            C, C++, and Python examples
benchmarks/          Performance checks
tools/               Repository maintenance tools
  ci/                 Local/hosted build-and-test entry points
cmake/               Package configuration modules
docs/                API, capability, and migration documentation

The root CMake file contains project policy and installation only. Library, test, example, and benchmark targets are defined by their own subdirectories. Run tools/ci/build-and-test.sh for the same build, test, install, and downstream-consumer checks used by continuous integration.

Requirements

• C99 and C++17 compilers
• CMake 3.18 or newer
• GMP
• MPFR

On macOS with Homebrew:

brew install cmake gmp mpfr

On Debian or Ubuntu:

sudo apt install cmake build-essential libgmp-dev libmpfr-dev

Build and test

cmake -S . -B build -DCMAKE_BUILD_TYPE=Release
cmake --build build -j
ctest --test-dir build --output-on-failure

Shared libraries are built by default. Pass -DBUILD_SHARED_LIBS=OFF for static libraries. The scalar kernels are portable; x86 SIMD kernels can be enabled with -DELINA_ENABLE_SIMD=ON.

Install

cmake --install build --prefix /path/to/elina

The installation exports these CMake targets:

• ELINA::auxiliary
• ELINA::linearize
• ELINA::partitions
• ELINA::octagon
• ELINA::polyhedra
• ELINA::zones
• ELINA::zonotope
• ELINA::elina (recommended high-level C/C++ API)

A downstream CMake project can consume ELINA with:

find_package(ELINA 1.3 REQUIRED)
target_link_libraries(my_analysis PRIVATE ELINA::elina)

If ELINA was installed to a non-system prefix, add that prefix to CMAKE_PREFIX_PATH when configuring the downstream project.

The Python wrapper is packaged separately after installing the shared native library:

python -m pip install ./bindings/python

Set ELINA_LIBRARY_PATH when the installed library is outside the platform's normal loader search paths.

C clients use <elina/elina.h>; C++ clients use <elina/elina.hpp>.

License

ELINA is distributed under the GNU Lesser General Public License, version 3. See LICENSE.