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. .. contents:: Table of Contents :local: :depth: 2 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**: .. code-block:: bash python3 -m aria.cli.efsmt [options] **Arguments**: * ``file`` - EFSMT SMT-LIB2 file (``.smt2``) **Options**: .. list-table:: :header: "Option, Default, Description" :widths: 25, 60 ``--parser``, ``z3``, Parsing backend (z3 or sexpr) ``--theory``, ``auto``, Theory selection (auto, bool, bv, lira) ``--engine``, ``auto``, Solver engine (auto, z3, cegar, efbv-par, efbv-seq, eflira-par, eflira-seq) ``--bv-solver``, (from config), Backend for efbv-seq ``--forall-solver``, (from config), Binary solver for eflira-par ``--max-loops``, (default), Max iterations for CEGAR engines ``--timeout``, (default), Timeout in seconds for Z3-based checks ``--log-level``, ``INFO``, Logging level (DEBUG, INFO, WARNING, ERROR) **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**: .. code-block:: bash python3 -m aria.cli.fmldoc [options] **Commands**: #### ``translate`` - Translate between formats ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. code-block:: bash python3 -m aria.cli.fmldoc translate -i INPUT_FILE -o OUTPUT_FILE [options] **Options:** .. list-table:: :header: "Option, Description" :widths: 25, 60 ``-i, --input-file``, Input file (required) ``-o, --output-file``, Output file (required) ``--input-format``, Input format ``--output-format``, Output format ``--auto-detect``, Auto-detect formats from extensions #### ``validate`` - Validate file format ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. code-block:: bash python3 -m aria.cli.fmldoc validate -i INPUT_FILE [options] **Options:** .. list-table:: :header: "Option, Description" :widths: 25, 60 ``-i, --input-file``, Input file (required) ``-f, --format``, File format #### ``analyze`` - Analyze properties ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. code-block:: bash python3 -m aria.cli.fmldoc analyze -i INPUT_FILE [options] **Options:** .. list-table:: :header: "Option, Description" :widths: 25, 60 ``-i, --input-file``, Input file (required) ``-f, --format``, File format #### ``formats`` - List supported formats and translations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. code-block:: bash python3 -m aria.cli.fmldoc formats **Output:** * Validation and analysis formats currently supported * Implemented translation pairs #### ``batch`` - Batch process files ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. code-block:: bash python3 -m aria.cli.fmldoc batch -i INPUT_DIR -o OUTPUT_DIR [options] **Options:** .. list-table:: :header: "Option, Description" :widths: 25, 60 ``-i, --input-dir``, Input directory (required) ``-o, --output-dir``, Output directory (required) ``--input-format``, Input format ``--output-format``, Output format **Currently Supported Formats:** * DIMACS (``.cnf``): validate, analyze, translate to SMT-LIB2 * SMT-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**: .. code-block:: bash python3 -m aria.cli.mc [options] **Arguments**: * ``file`` - Formula file (``.smt2``, ``.cnf``, ``.dimacs``) **Options**: .. list-table:: :header: "Option, Default, Description" :widths: 25, 60 ``--theory``, ``auto``, Theory type (bool, bv, arith, auto) ``--method``, (auto), Counting method (theory-specific) ``--timeout``, (default), Timeout in seconds ``--log-level``, ``INFO``, Logging level (DEBUG, INFO, WARNING, ERROR) **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**: .. code-block:: bash python3 -m aria.cli.pyomt [options] **Arguments**: * ``file`` - Optimization problem file (``.smt2``) **Options**: .. list-table:: :header: "Option, Default, Description" :widths: 25, 60 ``--type``, ``omt``, Problem type (omt, maxsmt) ``--theory``, ``auto``, Theory type for OMT (bv, arith, auto) ``--engine``, ``qsmt``, Optimization engine (qsmt, maxsat, iter, z3py) ``--solver``, (auto), Solver name (engine-specific) ``--log-level``, ``INFO``, Logging level (DEBUG, INFO, WARNING, ERROR) **Problem Types:** * ``omt``: Optimization Modulo Theory * ``maxsmt``: 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**: .. code-block:: bash python3 -m aria.cli.maxsat [options] aria-maxsat [options] **Arguments**: * ``file`` - WCNF formula file (``.wcnf``, ``.cnf``) **Options**: .. list-table:: :header: "Option, Default, Description" :widths: 25, 60 ``--solver``, ``rc2``, MaxSAT engine (rc2, fm, lsu) ``--timeout``, (none), Timeout in seconds ``--print-model``, (off), Print optimal assignment ``--log-level``, ``WARNING``, Logging level **Output**: Prints ``cost: ``, 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**: .. code-block:: bash python3 -m aria.cli.unsat_core [options] aria-unsat-core [options] **Arguments**: * ``file`` - SMT-LIB2 formula file (``.smt2``) **Options**: .. list-table:: :header: "Option, Default, Description" :widths: 25, 60 ``--algorithm``, ``marco``, Algorithm (marco, musx, optux) ``--all-mus``, (off), Enumerate all minimal unsatisfiable subsets (MARCO only) ``--timeout``, (none), Timeout in seconds ``--no-formulas``, (off), Print only core indices, not assertion formulas 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**: .. code-block:: bash python3 -m aria.cli.allsmt [options] aria-allsmt [options] **Arguments**: * ``file`` - SMT-LIB2 formula file (``.smt2``) **Options**: .. list-table:: :header: "Option, Default, Description" :widths: 25, 60 ``--solver``, ``z3``, AllSMT backend (z3, pysmt, mathsat) ``--limit``, ``100``, Maximum number of models to enumerate ``--project``, (all vars), Comma-separated variable names to include ``--count-only``, (off), Print only the model count ``--verbose``, (off), Print each model in detail **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**: .. code-block:: bash python3 -m aria.cli.smt_server [options] **Options**: .. list-table:: :header: "Option, Default, Description" :widths: 25, 60 ``--input-pipe``, ``/tmp/smt_input``, Path to input pipe ``--output-pipe``, ``/tmp/smt_output``, Path to output pipe ``--log-level``, ``INFO``, Logging level (DEBUG, INFO, WARNING, ERROR, CRITICAL) **Supported Commands**: #### Basic SMT-LIB2 Commands ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. list-table:: :header: "Command, Description" :widths: 40, 60 ``declare-const ``, Declare constant (Int, Bool, Real) ``assert ``, Assert expression ``check-sat``, Check satisfiability ``get-model``, Get satisfying model ``get-value ...``, Get values of variables ``push``, Push new scope ``pop``, Pop scope ``exit``, Exit server #### Advanced Commands ~~~~~~~~~~~~~~~~~~~ .. list-table:: :header: "Command, Description" :widths: 40, 60 ``allsmt [:limit=] ...``, Enumerate all satisfying models ``unsat-core [:algorithm=] [:timeout=] [:enumerate-all]``, Compute UNSAT cores ``backbone [:algorithm=]``, Compute backbone literals ``count-models [:timeout=] [:approximate]``, Count satisfying models ``set-option