Utilities

The aria.utils module provides common helper functions, type definitions, exception handling, and utility classes used throughout the ARIA codebase. It serves as a foundation for all other modules, offering standardized interfaces for solvers, expressions, values, and file parsing.

Directory Structure

` utils/ ├── __init__.py                     (7 lines - main entry point) ├── types.py                         (Type definitions) ├── exceptions.py                    (Exception hierarchy) ├── (Other utility modules across utils/) └── (Various subdirectories for specialized utilities) `

Note: The utils module is distributed across multiple subdirectories. Key utilities are documented below.

Module-Level Exports

From __init__.py:

from aria.utils import (
    SExprParser,          # S-expression parser
    SolverResult,          # Unified solver result type
    RE_GET_EXPR_VALUE_ALL  # Regex pattern for extracting values
)

Key Components

### 1. Type Definitions (types.py)

Provides common type definitions used throughout ARIA.

Key Types:

  • SolverResult (enum): Unified solver result type - SAT: Formula is satisfiable - UNSAT: Formula is unsatisfiable - UNKNOWN: Solver couldn’t determine status - ERROR: Solver error occurred

  • OSType (enum): Operating system type for solver binaries

  • BinarySMTSolverType (enum): Types of binary SMT solvers

Usage Pattern:

from aria.utils.types import SolverResult

result = SolverResult.SAT
if result == SolverResult.SAT:
    print("Satisfiable")

### 2. Exception Hierarchy (exceptions.py)

Custom exception hierarchy for ARIA-specific errors.

Base Exception:

  • AriaException: Base exception class for all ARIA errors - Provides consistent error handling across modules - Supports chaining for error context

Usage Pattern:

from aria.utils.exceptions import AriaException

try:
    # Some aria operation
    pass
except AriaException as e:
    print(f"ARIA error: {e}")

### 3. S-Expression Parser (SExprParser)

Parses S-expression format commonly used in SMT-LIB and related formats.

Key Methods:

  • parse(string): Parse S-expression string into Python objects

  • Supports nested expressions

  • Handles quoted strings and special characters

Usage Pattern:

from aria.utils import SExprParser

parser = SExprParser()
parsed = parser.parse("(and x y z)")
# Returns nested Python structure

Use Cases:

  • SMT-LIB2 parsing: Read S-expressions from SMT-LIB format files

  • Formula parsing: Convert S-expression to internal representations

  • Communication protocols: Parse solver output in S-expression format

### 4. Solver Utilities

Various utilities for working with external solvers:

Common Patterns:

  • Binary solver execution and output parsing

  • Standardized error handling across different solver backends

  • File I/O for solver communication

  • Process management for parallel solver execution

### 5. Expression Utilities

Helpers for working with Z3 and SMT expressions:

Common Functions:

  • Variable extraction from formulas

  • Expression transformation and simplification

  • Type checking and validation

  • Substitution and evaluation utilities

Related Modules:

  • z3_expr_utils.py: Z3-specific expression utilities

  • z3_solver_utils.py: Z3 solver wrapper utilities

  • pysmt_solver.py: PySMT solver interface

### 6. Value Conversion

Utilities for converting between different value representations:

Use Cases:

  • Converting solver outputs to ARIA internal types

  • Handling different numeric representations (integers, bit-vectors, reals)

  • String/bytes parsing and conversion

Usage Across Codebase

The utils module is used extensively throughout ARIA in these domains:

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

  • Solver configuration access

  • Type checking

  • Process management

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

  • Binary solver invocation

  • Custom path configuration

  • Multi-solver coordination

### Model Counting aria/counting/bool/ - Boolean model counting

  • 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/ - Boolean logic operations

  • SAT solver wrappers

  • Expression utilities

### General Utilities Expression parsing, file I/O, process management

Design Patterns

### 1. Centralized Configuration

Utils provide standardized access to:

  • Solver paths and availability

  • Type definitions

  • Common interfaces

Benefits:

  • Consistency: Single source of truth for solver configuration

  • Maintainability: Changes propagate automatically

  • Testing: Easy to mock utilities for testing

### 2. Error Handling

Unified exception hierarchy:

  • AriaException base class

  • Specific exceptions can inherit from it

  • Consistent error catching across modules

### 3. Type Safety

Strong typing with enums:

  • SolverResult for clear status communication

  • OSType for platform-specific behavior

  • BinarySMTSolverType for solver categorization

### 4. Parser Utilities

SExprParser for S-expression parsing:

  • Standard format in SMT and logic communities

  • Robust parsing with error handling

  • Support for nested structures

Usage Examples

### Solver Result Type

from aria.utils.types import SolverResult

def solve_formula(formula):
    # ... solver logic ...
    return SolverResult.SAT

def check_result(result):
    if result == SolverResult.SAT:
        print("Formula is satisfiable")
    elif result == SolverResult.UNSAT:
        print("Formula is unsatisfiable")
    else:
        print("Unknown or error")

### Exception Handling

from aria.utils.exceptions import AriaException

def some_aria_function():
    try:
        # Operation that might fail
        result = perform_solver_call()
    except AriaException as e:
        print(f"ARIA operation failed: {e}")
        raise

### S-Expression Parsing

from aria.utils import SExprParser

# Parse S-expression
parser = SExprParser()
parsed = parser.parse("(define-fun my-fun (x) (ite (is-sat x) true false))")

# Access parsed structure
print(parsed)

Key Features

  1. Type Safety: Strong typing with enums for results and configurations

  2. Error Handling: Centralized exception hierarchy for consistent error management

  3. Parser Support: S-expression parser for SMT-LIB compatibility

  4. Solver Integration: Utilities for working with external solver binaries

  5. Expression Utilities: Helpers for expression manipulation and analysis

  6. Value Conversion: Standardized conversion between different representations

  7. Extensibility: Easy to add new utilities as needed

Integration Points

The utils module is imported in numerous files across ARIA:

  • SMT solving: aria/smt/pcdclt/

  • Quantifiers: aria/quant/efbv/, aria/quant/eflira/

  • Model counting: aria/counting/bool/

  • Synthesis: aria/synthesis/cvc5/

  • Abduction: aria/abduction/

  • Interpolation: aria/interpolant/

  • Boolean reasoning: aria/bool/

  • Testing: aria/tests/

Design Philosophy

“Utility First”: Provide small, focused, well-tested utilities that:

  1. Do one thing well - Each utility has a clear, single purpose

  2. Be reusable - Designed for use across multiple modules

  3. Stay simple - Avoid unnecessary complexity

  4. Document thoroughly - Clear docstrings explain purpose and usage

  5. Handle errors gracefully - Proper exception raising and catching

  6. Standardize interfaces - Consistent APIs for similar functionality

Notes

  • The utils module is the foundation upon which all other ARIA modules build

  • Changes to utils should be made carefully as they have wide-ranging effects

  • Priority is on correctness and reliability over performance

  • Documentation is essential due to the module’s foundational role

Size Statistics

  • Total documented components: 6+ (from analysis)

  • Type definitions: 3+ enums

  • Core utilities: SExprParser, exception hierarchy, solver wrappers

  • Integration points: 15+ modules across ARIA