Welcome to aria’s Documentation!

Introduction

Aria is a comprehensive toolkit for automated reasoning and constraint solving. It provides implementations of various algorithms and tools for:

• Abductive Inference (aria/abduction) - Generate explanations for observations

• AllSMT (aria/allsmt) - Enumerate all satisfying models

• Backbone Computation (aria/backbone) - Extract forced assignments

• UNSAT Core Extraction (aria/unsat_core) - Identify minimal unsatisfiable subsets

• Quantifier Reasoning (aria/quant) - Handle exists-forall and quantified formulas

• Quantifier Elimination (aria/quant/qe) - Eliminate quantifiers from formulas

• Solution Sampling (aria/sampling) - Generate diverse solutions

• Model Counting (aria/counting) - Count satisfying assignments

• Optimization Modulo Theory (aria/optimization) - Solve optimization problems

• Interpolant Generation (aria/interpolant) - Generate Craig interpolants

• Symbolic Abstraction (aria/symabs) - Abstract state spaces

• Predicate Abstraction (aria/symabs/predicate_abstraction) - Abstract with predicates

• Monadic Abstraction (aria/monabs) - Monadic predicate abstraction

• Knowledge Compilation (aria/bool/knowledge_compiler) - Compile to tractable forms

• MaxSAT Solving (aria/bool/maxsat) - Solve maximum satisfiability problems

• QBF Solving - Quantified Boolean formula solving

• Finite Field Solving (aria/smt/ff) - SMT for Galois field constraints

• Interactive Theorem Proving (aria/itp) - Proof assistant framework

• Automata Operations (aria/automata) - Finite automata algorithms

• Program Synthesis (aria/synthesis) - Synthesize programs from specifications

• Context-Free Language Reachability (aria/cfl) - CFL solving algorithms

• Unification (aria/unification) - Term unification algorithms

• Translator (aria/translator) - Translate between different formats

• EFMC Verification (aria/efmc) - Program verification with invariant generation, termination analysis, and more

We welcome any feedback, issues, or suggestions for improvement. Please feel free to open an issue in our repository.

Installing and Using Aria

Install aria from source

git clone https://github.com/ZJU-PL/aria
virtualenv --python=python3 venv
source venv/bin/activate
cd aria
bash setup_local_env.sh
pip install -e .

The setup script will: - Create a Python virtual environment if it doesn’t exist - Activate the virtual environment and install the package and its dependencies (from pyproject.toml) - Download required solver binaries (CVC5, MathSAT, z3) - Run unit tests if available

Quick Start

from aria import *

# Example: Check satisfiability
formula = Bool(True)  # Simple tautology
result = smt_solve(formula)
print(f"Formula is {'satisfiable' if result else 'unsatisfiable'}")

Documentation Map

• getting-started: tutorials, quick reference, and topic overviews

• logic-and-solving: core logic APIs, solver stacks, SRK, and reusable reasoning infrastructure

• proofs and explanations: abduction, interpolation, and interactive theorem proving

• quantified-reasoning: quantified solving, quantifier elimination, and instantiation techniques

• abstraction / verification: program-analysis engines and verification workflows

• counting-probability: model counting, sampling, and probabilistic reasoning

Contents:

• Getting Started
  • Tutorial
  • Quick Reference
  • Research Topics and Thesis Projects
  • Playing wiht Program Verification with EFMC
• Logic and Solving
  • Boolean Reasoning
  • SMT Solving
  • SMT Solving for Finite Field
  • Theory Reference: Finite Fields
  • References
  • First-Order Logic (FOL)
  • Utilities
  • SRK Symbolic Reasoning Kit
  • Unification
  • Introduction
  • Components
  • Applications
  • References
  • AllSMT
  • Backbone Computation
  • UNSAT Core Extraction
  • Optimization Modulo Theory
  • Knowledge Compilation
  • Parallel SMT CDCL(T) Solving
• Proofs and Explanations
  • Abduction
  • Interpolant Generation
  • Interactive Theorem Proving (ITP)
• Quantified Reasoning
  • Playing wth Quantifiers
  • Quantifier Elimination (QE)
  • Quantifier Instantiation (QI)
• Automata and Languages
  • Automata
  • Introduction
  • Components
  • Applications
  • References
  • AALpy
  • Context-Free Language Reachability
  • Introduction
  • Components
  • Applications
  • References
  • CFL OBDD (Context-Free Language Ordered Binary Decision Diagrams)
• Verification
  • BDD-based Symbolic Model Checking
  • Program Verification
  • PolyHorn: Polynomial Horn Clause Solver
  • Houdini
  • K-induction
  • K-Safety Verification
  • Ranking Function Templates for Termination Verification
  • Danger Invariants
  • Linear Teamporal Logic
  • Symbolic Finite Automata
  • LLM4Inv: LLM-Guided Invariant Synthesis
• Abstraction
  • Symbolic Abstraction
  • Predicate Abstraction
  • Predicate Abstraction and CEGAR
  • Monadic Predicate Abstraction
  • Abstraction Interpretation
  • Widening
  • Making Abstraction Interpretation Complete
• Counting, Sampling, and Probability
  • Model Counting
  • Model Sampling
  • Probabilistic Reasoning (aria/prob)
• Program Synthesis
  • Program Synthesis
  • Introduction
  • Components
  • Applications
  • References
• LLM and ML
  • LLM Tools
• CLI and Tools
  • CLI Tools
  • Translator Module
  • Introduction
  • Components
  • Command-Line Interface (aria/cli/fmldoc.py)
  • Examples
  • Applications
  • References
  • Applications
  • Boogie Frontend for EFMC
  • C Frontend for EFMC
  • Constrained Horn Clauses (CHC) Tools
  • Verification Tools
• Global Parameters
  • Directory Structure
  • Module Overview
  • Key Components
  • Usage Patterns Across Codebase
  • Physical Directory Structure
  • Domains Using Global Parameters
  • Design Patterns
  • Documentation Quality
  • Recommendations for Enhancement
  • Integration Points
  • Key Features
  • Size Statistics