CLI Tools
The aria.cli module provides command-line interface tools for various automated reasoning tasks, including EFSMT solving, model counting, optimization (OMT/MaxSAT), UNSAT core and MUS computation, AllSMT model enumeration, and an enhanced SMT server with advanced features.
Directory Structure
``` cli/ ├── __init__.py (0 lines - empty) ├── efsmt.py Exists-Forall SMT solver ├── fmldoc.py Format conversion and validation ├── mc.py Model counting ├── pyomt.py OMT / MaxSMT optimization ├── maxsat.py MaxSAT (WCNF) solver ├── unsat_core.py UNSAT core / MUS / MSS ├── allsmt.py All satisfying models enumeration ├── smt_server.py Enhanced SMT server (IPC) ├── README.md CLI usage guide └── tests/
├── test_smt_server.py ├── test_cli_maxsat.py ├── test_cli_unsat_core.py └── test_cli_allsmt.py
No subdirectories - flat module structure with tests/ subdirectory.
CLI Tools Overview
### 1. efsmt.py - Exists-Forall SMT Solver
Purpose: Solve EFSMT (Exists-Forall Satisfiability Modulo Theories) problems using various algorithms.
Usage:
python3 -m aria.cli.efsmt <file> [options]
Arguments:
file- EFSMT SMT-LIB2 file (.smt2)
Options:
Features:
Automatic theory detection (Boolean, BitVector, LIRA)
Multiple solver engines (Z3, CEGAR, parallel EF-BV/LIRA)
Support for QF_BV, QF_LIRA, and Boolean theories
Configurable timeouts and logging
Theory Support:
Boolean: Pure SAT problems
BitVector: Quantifier-free bit-vector logic
LIRA: Linear Integer/Real Arithmetic
Auto: Auto-detect from problem content
### 2. fmldoc.py - Logic Constraint Format Utilities
Purpose: Translate, validate, and analyze supported logic constraint formats.
Usage:
python3 -m aria.cli.fmldoc <command> [options]
Commands:
#### translate - Translate between formats
python3 -m aria.cli.fmldoc translate -i INPUT_FILE -o OUTPUT_FILE [options]
Options:
#### validate - Validate file format
python3 -m aria.cli.fmldoc validate -i INPUT_FILE [options]
Options:
#### analyze - Analyze properties
python3 -m aria.cli.fmldoc analyze -i INPUT_FILE [options]
Options:
#### formats - List supported formats and translations
python3 -m aria.cli.fmldoc formats
Output:
Validation and analysis formats currently supported
Implemented translation pairs
#### batch - Batch process files
python3 -m aria.cli.fmldoc batch -i INPUT_DIR -o OUTPUT_DIR [options]
Options:
Currently Supported Formats:
DIMACS (
.cnf): validate, analyze, translate to SMT-LIB2SMT-LIB2 (
.smt2): validate, analyze
Currently Implemented Translation Pairs:
DIMACS -> SMT-LIB2
Global Options:
-v, --verbose: Verbose output-d, --debug: Debug output-h, --help: Show help message
### 3. mc.py - Model Counting Tool
Purpose: Count models of formulas in various theories (Boolean, QF_BV, Arithmetic).
Usage:
python3 -m aria.cli.mc <file> [options]
Arguments:
file- Formula file (.smt2,.cnf,.dimacs)
Options:
Features:
Automatic format detection (
.smt2,.cnf,.dimacs)Auto theory detection from content
Theory-specific counting methods: - Boolean: DIMACS parallel counting - BitVector: Enumeration and sampling - Arithmetic: LattE-based and enumeration-based
Output: Prints number of models to stdout
### 4. pyomt.py - Optimization Problems Solver
Purpose: Solve OMT (Optimization Modulo Theory) and MaxSMT problems.
Usage:
python3 -m aria.cli.pyomt <file> [options]
Arguments:
file- Optimization problem file (.smt2)
Options:
Problem Types:
omt: Optimization Modulo Theorymaxsmt: Maximum Satisfiability (not yet implemented)
Theory Support:
BitVector (
bv)Arithmetic (
arith)Auto (
auto- auto-detect from objective)
Engines:
qsmt: Quantified SMT (default: z3)maxsat: MaxSAT solver (default: FM)iter: Iterative search (default: z3-ls)z3py: Z3 Python API (default: z3py)
Default Solver Mapping:
qsmt → z3
maxsat → FM
iter → z3-ls
z3py → z3py
Note: MaxSMT support is not yet implemented in the CLI.
### 5. maxsat.py - MaxSAT Solver
Purpose: Solve (weighted partial) MaxSAT problems from WCNF files using RC2, FM, or LSU engines.
Usage:
python3 -m aria.cli.maxsat <file> [options]
aria-maxsat <file> [options]
Arguments:
file- WCNF formula file (.wcnf,.cnf)
Options:
Output: Prints cost: <n>, optional status, and with --print-model the satisfying literals.
### 6. unsat_core.py - UNSAT Core / MUS / MSS
Purpose: Compute one minimal unsatisfiable core or enumerate all MUSes from an SMT-LIB2 formula.
Usage:
python3 -m aria.cli.unsat_core <file> [options]
aria-unsat-core <file> [options]
Arguments:
file- SMT-LIB2 formula file (.smt2)
Options:
If the formula is satisfiable, the tool reports that and exits successfully. For unsatisfiable formulas, prints one or more cores (assertion indices and optionally the formulas).
### 7. allsmt.py - All Satisfying Models
Purpose: Enumerate all satisfying models of an SMT-LIB2 formula up to a configurable limit.
Usage:
python3 -m aria.cli.allsmt <file> [options]
aria-allsmt <file> [options]
Arguments:
file- SMT-LIB2 formula file (.smt2)
Options:
Output: Without --count-only, prints each model; with --count-only, a single line with the count.
### 8. smt_server.py - Enhanced SMT Server
Purpose: IPC-based SMT-LIB2 server with advanced aria features (AllSMT, UNSAT cores, backbone, model counting).
Usage:
python3 -m aria.cli.smt_server [options]
Options:
Supported Commands:
#### Basic SMT-LIB2 Commands
#### Advanced Commands
#### Configuration Options
Usage Example:
# Start server
python3 -m aria.cli.smt_server
# In another terminal, send commands
echo "declare-const x Int" > /tmp/smt_input
echo "assert (> x 0)" > /tmp/smt_input
echo "check-sat" > /tmp/smt_input
cat /tmp/smt_output # Read response
Advanced Features:
AllSMT: Model enumeration with limit support
UNSAT Cores: Computation using MARCO, MUSX, OPTUX algorithms
Backbone: Literal extraction from all models
Model Counting: Exact and approximate counting with timeout
Scope Management: Push/pop for incremental solving
Named Pipe IPC: Unix-style pipe communication
### 9. README.md - CLI Documentation
Comprehensive documentation in aria/cli/README.md covering:
All CLI tools (fmldoc, mc, pyomt, efsmt, maxsat, unsat_core, allsmt, smt_server)
Server architecture and IPC mechanisms
Complete command reference and options
Usage examples and testing
Testing
Run all CLI tests:
pytest aria/tests/test_cli_*.py -v
Per-tool tests:
test_cli_fmldoc.py- Format convertertest_cli_mc.py- Model countingtest_cli_efsmt.py- EFSMT solvertest_cli_pyomt.py- OMT solvertest_cli_maxsat.py- MaxSAT solvertest_cli_unsat_core.py- UNSAT core / MUStest_cli_allsmt.py- AllSMT enumerationtest_smt_server.py- SMT server (declare-const, assert, check-sat, get-model, AllSMT, UNSAT core, model counting, help)
Code Statistics
Documentation: aria/cli/README.md
Tests: test_cli_*.py, test_smt_server.py
Dependencies
Some tools require additional dependencies that may not be installed:
pysat: Required for EFSMT, MC, and pyomt tools
pysmt: Required for pyomt tool
Note: The help commands work even if dependencies are missing, showing the tool’s interface and options.
Main API Entry Points
All CLI tools can be invoked via Python module syntax:
python3 -m aria.cli.<tool_name> [options]
Where <tool_name> is one of:
efsmt- Exists-Forall SMT solverfmldoc- Format translator and validatormc- Model countingpyomt- OMT / MaxSMT optimization solvermaxsat- MaxSAT (WCNF) solver (RC2, FM, LSU)unsat_core- UNSAT core / MUS / MSS computationallsmt- Enumerate all satisfying modelssmt_server- SMT server (IPC)
Key Features
Modular Design: Each tool is a standalone Python module
Comprehensive CLI: Consistent argument parsing across all tools
Advanced Features: SMT server provides AllSMT, UNSAT cores, backbone, counting
Flexible Configuration: Multiple engines, theories, and algorithms per tool
Testing: SMT server has comprehensive test suite
Documentation: README.md provides detailed SMT server usage guide
Logging: Configurable logging levels for all tools
IPC Support: Named pipe communication for SMT server integration