Global Parameters

The aria.global_params module provides centralized configuration management for the ARIA project. It handles SMT solver discovery, path management, and provides a singleton-based global configuration interface used throughout the codebase.

Directory Structure

` global_params/ ├── __init__.py                    (7 lines - module entry point) └── paths.py                       (206 lines - core implementation) `

No subdirectories - flat module structure.

Module Overview

### Centralized Configuration System

The global_params module implements a singleton pattern configuration manager that:

  1. Manages SMT solver paths and availability

  2. Provides project-wide constants for important directories

  3. Implements solver discovery (local binaries → system PATH)

  4. Offers consistent API for configuration access across the codebase

Usage Pattern: This module is imported in 21 files across the project for solver path resolution and configuration access.

Key Components

### 1. SolverConfig Class

A data class representing configuration for a single SMT solver.

Attributes:

### 2. SolverRegistry Metaclass

Implements the singleton pattern to ensure only one GlobalConfig instance exists:

  • Prevents duplicate initialization

  • Provides consistent access across the application

  • Thread-safe configuration management

### 3. GlobalConfig Class (Singleton)

The core configuration manager with comprehensive capabilities.

Managed Solvers (5 solvers total):

Path Properties:

  • PROJECT_ROOT - Root directory of ARIA project

  • BIN_SOLVERS_PATH - Path to binary executables (bin_solvers/)

  • BENCHMARKS_PATH - Path to benchmark files (benchmarks/)

Key Methods:

Solver Discovery Logic:

  1. First searches in local bin_solvers/ directory

  2. Falls back to system PATH

  3. Logs warnings for unavailable solvers

  4. Caches results for performance

Solver Configuration Details:

From get_smt_solvers_config():

### 4. Module-Level Exports

From __init__.py:

from aria.global_params import (
    global_config,      # GlobalConfig singleton instance
    SMT_SOLVERS_PATH,  # Dictionary of solver configurations
    PROJECT_ROOT,       # Path object pointing to project root
    BIN_SOLVERS_PATH,  # Path object to bin_solvers directory
    BENCHMARKS_PATH     # Path object to benchmarks directory
)

Usage Patterns Across Codebase

The module is imported in 21 files across the project, with common use cases:

### 1. Solver Path Retrieval (Most Common)

from aria.global_params import global_config

solver_path = global_config.get_solver_path("z3")

Used in: efbv_bin_solvers.py, mathsat_solver.py, cvc5_sygus_abduct.py, cvc5_interpolant.py, smtinterpol_interpolant.py, z3_plus_smtlib_solver.py, dimacs_counting.py, optimization/bin_solver.py, eflira_parallel.py

### 2. Availability Checking

from aria.global_params import global_config

if global_config.is_solver_available("sharp_sat"):
    # Use solver
    pass

Used in: test_bv_counting.py, test_bool_counting.py, test_sygus_inv.py, dimacs_counting.py

### 3. SMT Solver Configuration Dictionary

from aria.global_params import SMT_SOLVERS_PATH

z3_config = SMT_SOLVERS_PATH["z3"]
solver_bin = z3_config["path"] + " " + z3_config["args"]

Used in: pcdclt/solver.py, pcdclt/eval_smt.py, pcdclt/tests/test_solver.py, pcdclt/tests/test_process_cleanup.py

### 4. Benchmark Path Access

from aria.global_params import BENCHMARKS_PATH

cnf_path = BENCHMARKS_PATH / "dimacs" / "parity_5.cnf"

Used in: bool/features/sat_instance.py

Physical Directory Structure

``` bin_solvers/ # Solver binaries ├── z3 # 23.7 MB Z3 executable ├── cvc5 # 25.1 MB CVC5 executable ├── mathsat # 11.5 MB MathSAT executable └── sharpSAT # 1.2 MB SharpSAT executable

benchmarks/ # Test and evaluation benchmarks ├── abduction/ ├── dimacs/ ├── efmc/ │ ├── Boogie/ │ ├── BV/ │ ├── C/ │ ├── chc/ │ ├── INT/ │ ├── KSafety/ │ └── sygus-inv/ ├── fzn/ ├── qbf/ ├── smtlib2/ └── sygus-pbe/ ```

Domains Using Global Parameters

The module serves as a central hub for:

### SMT Solving aria/smt/pcdclt/ - Parallel CDCL(T) solver configuration**

  • Solver path resolution

  • Configuration dictionary access

### Quantifier Elimination aria/quant/efbv/, aria/quant/eflira/, aria/quant/qe/ - Multiple solver orchestration

  • Multiple solver integration

  • Custom path support

### Model Counting aria/counting/bool/ - SharpSAT integration

  • Solver availability checking

  • Model counter invocation

### Synthesis aria/synthesis/cvc5/ - SyGuS synthesis with CVC5

  • Solver path access

  • Binary management

### Abduction aria/abduction/ - Abductive reasoning

  • Solver orchestration

  • Multi-solver support

### Interpolation aria/interpolant/ - Interpolant generation

  • Multiple solver backends

  • Path configuration

### Boolean Reasoning aria/bool/features/ - SAT instance feature extraction

  • Benchmark path access

  • Feature computation infrastructure

Design Patterns

### 1. Singleton Pattern

Ensures single GlobalConfig instance via metaclass:

  • Benefits: - Consistent configuration across all imports - Prevents initialization conflicts - Efficient memory usage

### 2. Lazy Initialization

Solvers located on first access:

  • Reduces startup time

  • Only searches when needed

  • Caches results for performance

### 3. Fallback Strategy

Three-tier discovery:

  1. Local bin_solvers/ directory (preferred)

  2. System PATH (secondary)

  3. Unavailable (logged as warning)

### 4. Logging Integration

Uses Python logging for:

  • Unavailable solver warnings

  • Configuration errors

  • Debug information for troubleshooting

Documentation Quality

Strengths:

  • Comprehensive docstrings for all classes and methods

  • Clear parameter and return type documentation

  • Includes exception documentation

  • Explains design rationale (e.g., singleton pattern purpose)

Coverage:

  • All public methods have docstrings

  • Classes have descriptive summaries

  • Complex logic (solver discovery) is well documented

Recommendations for Enhancement

Based on the analysis, potential improvements include:

  1. Usage Examples - Add common usage patterns for each configuration method

  2. Version Documentation - Document expected solver versions/compatibility

  3. Troubleshooting Guide - Add section for solving common solver installation issues

  4. Environment Variable Support - Document environment variables for custom solver paths

  5. Download Script Documentation - Explain bin_solvers/download.py for initial solver setup

Integration Points

The module serves as the central hub for:

  1. Solver Orchestration: All external solver invocations route through this module

  2. Path Resolution: Standardizes project-wide path references

  3. Feature Testing: Test files check solver availability before running

  4. Parallel Processing: Used in multi-process contexts (singleton ensures consistency)

Key Features

  1. Singleton Management: Ensures single GlobalConfig instance

  2. Solver Discovery: Automatic path resolution with fallback strategy

  3. Path Management: Centralized project constants (PROJECT_ROOT, BIN_SOLVERS_PATH, BENCHMARKS_PATH)

  4. 5 Supported Solvers: Z3, CVC5, MathSAT, Yices2, SharpSAT

  5. 21 Integration Points: Used across SMT, quantifiers, synthesis, Boolean reasoning

  6. Thread-Safe: Singleton pattern with metaclass for concurrent access

  7. Logging Integration: Warnings and errors properly logged

  8. Extensible: Easy to add new solvers to configuration

Size Statistics

  • Total Python files: 2

  • Total Python lines: ~213

  • paths.py: 206 lines

  • __init__.py: 7 lines

  • Managed solvers: 5

  • Integration points: 21+