Welcome to aria’s Documentation!

Introduction

ARIA (Automated Reasoning Infrastructure & Applications) is a Python toolkit and research playground for automated reasoning. The repository combines libraries, CLI tools, and research prototypes across SAT/SMT solving, quantified reasoning, model counting, optimization, theorem proving, program verification, symbolic abstraction, and related experimentation.

Major user-facing areas include:

• aria.bool: SAT, MaxSAT, QBF, CNF simplification, and knowledge compilation

• aria.smt: SMT-oriented theory packages and solver utilities (including unification, fol)

• aria.utils.srk: symbolic reasoning infrastructure

• aria.quant: quantified reasoning, EFSMT, QE, CHC tooling, and prototypes

• aria.efmc: program verification frontends and engines

• aria.counting / aria.sampling / aria.prob: counting, sampling, and probabilistic reasoning

• aria.pyomt: optimization and MaxSMT/MaxSAT-oriented workflows

• aria.smt.fol: first-order logic theorem proving (Miniprover) - now in aria.smt.fol

• aria.util.translator / aria.cli: translators and command-line tools

• aria.volumn: volume computation for polytopes

Installing and using aria

Install from source:

git clone https://github.com/ZJU-PL/aria
cd aria
bash setup_local_env.sh
pip install -e .

For a faster local setup with uv:

uv venv
source .venv/bin/activate
uv pip install -e .

Common console commands after installation include:

• aria-fmldoc

• aria-mc

• aria-pyomt

• aria-efsmt

• aria-maxsat

• aria-unsat-core

• aria-allsmt

• aria-smt-server

• aria-efmc

• aria-efmc-efsmt

• aria-polyhorn

Documentation map

• getting-started: installation notes, quick reference, and tutorials

• logic-and-solving: core solver and reasoning packages

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

• quantified-reasoning: EFSMT, QE, and quantified workflows

• verification / abstraction: EFMC engines and abstraction-oriented pages

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

• cli-tools: command-line frontends and translator-oriented workflows

Contents:

• Getting Started
  • Tutorial
  • Quick Reference
  • Research Topics and Thesis Projects
  • 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
  • Modal Logic
  • Dissolve (Distributed SAT)
  • Three-Valued Logic
  • Prime Implicant / Implicate Enumeration
  • SAT Instance Feature Extraction
  • Boolean Analysis
  • CNF Simplification Framework
• Proofs and Explanations
  • Abductive Reasoning
  • Interpolant Generation
  • Interactive Theorem Proving (ITP)
• Quantified Reasoning
  • Playing wth Quantifiers
  • Exists-Forall SMT (EFSMT)
  • 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 Verification
  • Program Verification
  • PDR (Property-Directed Reachability)
  • SMT Tools
  • PolyHorn: Polynomial Horn Clause Solver
  • Houdini
  • K-Induction
  • K-Safety Verification
  • Ranking Functions
  • 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
  • Abstract Interpretation
• Counting, Sampling, and Probability
  • Model Counting
  • Model Sampling
  • Probabilistic Reasoning (aria/prob)
• Program Synthesis
  • Program Synthesis
  • Introduction
  • Components
  • Applications
  • References
• Logic Programming
  • Datalog
• LLM and ML
  • LLM Tools
  • Machine Learning Components
• CLI and Tools
  • CLI Tools
  • Translator Module
  • 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