Logic and Solving

This section combines the shared logical foundations, symbolic reasoning toolkits, and the main Boolean/SMT solving workflows. It is the place to look for core APIs, solver backends, and reusable reasoning infrastructure.

• Boolean Reasoning
  • Directory Structure
  • Usage Examples
  • Main API Entry Points
  • Key Dependencies
  • Notable Features
  • Size Statistics
• SMT Solving
  • Bit-Vectors, Floating Points, etc.
  • Linear Arithmetic
  • Strings
• SMT Solving for Finite Field
  • Overview
• Theory Reference: Finite Fields
  • Implementation
  • Usage Example
• References
• First-Order Logic (FOL)
  • Directory Structure
  • Module Purpose
  • Key Components
  • Algorithms Implemented
  • Usage Examples
  • Key Features
  • Size Statistics
  • Testing
  • Use Cases
  • Notable Design Decisions
• Utilities
  • Directory Structure
  • Module-Level Exports
  • Key Components
  • Usage Across Codebase
  • Design Patterns
  • Usage Examples
  • Key Features
  • Integration Points
  • Design Philosophy
  • Notes
  • Size Statistics
• SRK Symbolic Reasoning Kit
  • Overview
  • Subsystems
  • Getting Started
  • Working with SMT-LIB
  • Further Reading
• Unification
• Introduction
  • Key Features
• Components
  • Core Unification (aria/unification/core.py)
  • Pattern Matching (aria/unification/match.py)
  • Variables (aria/unification/variable.py)
  • Utilities (aria/unification/utils.py)
  • Type Dispatch (aria/unification/dispatch.py)
• Applications
• References
• AllSMT
  • Introduction
  • Related Work
  • References
• Backbone Computation
  • Introduction to Backbone Computation
  • Backbone Computation in Aria
  • Usage Example
  • Algorithm Details
  • Performance Considerations
  • References
• UNSAT Core Extraction
  • Introduction to UNSAT Core Extraction
  • UNSAT Core Extraction in Aria
  • Usage Example
  • Algorithm Selection
  • Advanced Features
  • References
• Optimization Modulo Theory
  • Introduction
  • OMT in Aria
  • References
• Knowledge Compilation
  • Introduction to Knowledge Compilation
  • Target Languages
  • Compilation Techniques
  • Applications
• Parallel SMT CDCL(T) Solving
  • CDCL(T)
  • Parallel CDCL(T)
  • How to Use