Translator Module

Introduction

The translator module (aria/translator) provides format conversion utilities for various logic constraint representations. It enables translation between different formats used in automated reasoning, including DIMACS, QDIMACS, SMT-LIB2, SyGuS, and others.

Key Features

  • DIMACS to SMT-LIB2: Convert CNF formulas to SMT2 format

  • QDIMACS to SMT-LIB2: Convert quantified Boolean formulas to SMT2 format

  • SMT-LIB2 to C: Generate C code from SMT formulas

  • SMT-LIB2 to SymPy: Convert SMT formulas to SymPy expressions

  • SyGuS to SMT-LIB2: Convert SyGuS synthesis instances to SMT2

  • WCNF to Z3: Convert weighted CNF to Z3 optimizer instances

  • CNF to Linear Programming: Convert CNF to LP format

  • FlatZinc to OMT: Convert FlatZinc to Optimization Modulo Theory formats

Components

DIMACS to SMT-LIB2 (aria/translator/dimacs2smt.py)

Converts DIMACS CNF files to SMT-LIB2 format. Supports both command-line usage and programmatic API.

Command-line usage:

python -m aria.translator.dimacs2smt input.cnf -o output.smt2 -l QF_UF

Programmatic usage:

from aria.translator import dimacs2smt

output_path = dimacs2smt.convert_dimacs_to_smt2(
    input_path="input.cnf",
    output_path="output.smt2",
    logic="QF_UF",
    var_prefix="v_"
)

Features: * Supports QF_UF and QF_BV logics * Customizable variable name prefixes * Preserves comments from DIMACS files * Handles empty clauses gracefully

QDIMACS to SMT-LIB2 (aria/translator/qbf2smt.py)

Converts QDIMACS (quantified Boolean formula) files to SMT-LIB2 format using UFBV logic. Uses bit-vector variables to compactly encode multiple Boolean variables.

Command-line usage:

python -m aria.translator.qbf2smt input.qdimacs

Features: * Converts quantifier prefixes (forall/exists) to SMT quantifiers * Uses bit-vectors for efficient encoding * Preserves quantifier structure * Outputs UFBV logic compatible with SMT solvers

Example:

The translator converts QDIMACS quantifier blocks like:

a 1 2 0
e 3 4 0

To SMT-LIB2 quantifiers:

(forall ((vec1 (_ BitVec 2)))
(exists ((vec2 (_ BitVec 2)))
...

CNF to SMT-LIB2 (aria/translator/cnf2smt.py)

Converts CNF formulas to Z3 expressions and SMT-LIB2 format. Provides parsing utilities for DIMACS strings and files.

Usage:

from aria.translator import cnf2smt
import z3

# Parse DIMACS file to Z3 expression
formula = cnf2smt.dimacs_to_z3("input.cnf")

# Check satisfiability
solver = z3.Solver()
solver.add(formula)
result = solver.check()

Functions: * parse_dimacs(filename): Parse DIMACS file, returns (num_vars, num_clauses, clauses) * parse_dimacs_string(dimacs_str): Parse DIMACS string * dimacs_to_z3(filename): Convert DIMACS file to Z3 expression * dimacs_string_to_z3(dimacs_str): Convert DIMACS string to Z3 expression * int_clauses_to_z3(clauses): Convert integer clause list to Z3 expression

CNF to Linear Programming (aria/translator/cnf2lp.py)

Converts CNF formulas to linear programming (LP) format, useful for logic programming applications.

Usage:

from aria.translator import cnf2lp

cnf2lp.cnf2lp("input.cnf", "output.lp")

Output format:

Each clause is converted to an LP rule:

p1 | p2 :- p3, p4.

Where positive literals appear in the head and negative literals in the body.

SMT-LIB2 to C (aria/translator/smt2c.py)

Generates C code from SMT-LIB2 formulas, useful for model counting and solution enumeration.

Usage:

python -m aria.translator.smt2c input.smt2 -o output.c

Features: * Generates C code for model counting * Supports bit-vector operations * Includes modulo arithmetic helper functions * Can generate SAT checking code

SMT-LIB2 to SymPy (aria/translator/smt2sympy.py)

Converts SMT-LIB2 formulas to SymPy symbolic expressions for symbolic manipulation and analysis.

Usage:

from aria.translator import smt2sympy

sympy_expr = smt2sympy.translate(smt_formula)

Features: * Preserves formula structure * Enables symbolic computation with SymPy * Supports arithmetic and Boolean operations

SyGuS to SMT-LIB2 (aria/translator/sygus2smt.py)

Converts SyGuS (Syntax-Guided Synthesis) instances to SMT-LIB2 format for use with SMT solvers.

Usage:

python -m aria.translator.sygus2smt --file input.sl

Conversion process: * Replaces synth-fun with declare-fun * Converts declare-var to declare-const * Transforms constraint to assert * Replaces check-synth with check-sat * Handles BitVec type annotations

Weighted CNF to Z3 (aria/translator/wcnf2z3.py)

Converts weighted CNF (WCNF) files to Z3 Optimize instances for partial weighted MaxSAT solving.

Usage:

from aria.translator import wcnf2z3
from z3 import *

opt, soft_constraints = wcnf2z3.construct_z3_optimizer(open("input.wcnf"))
result = opt.check()

Features: * Distinguishes hard and soft constraints * Uses Z3’s soft constraint API * Preserves clause weights * Supports partial MaxSAT instances

WCNF format: * Hard constraints have weight equal to top * Soft constraints have weight less than top * Format: p wcnf <vars> <clauses> <top>

FlatZinc to OMT (aria/translator/fzn2omt/)

Converts FlatZinc constraint programming instances to Optimization Modulo Theory (OMT) formats for various solvers.

Supported solvers: * Z3 (fzn2z3.py): Converts to Z3 optimization format * CVC4 (fzn2cvc4.py): Converts to CVC4 OMT format * OptiMathSAT (fzn2optimathsat.py): Converts to OptiMathSAT format

Common utilities (common.py): * Shared parsing and conversion functions * Constraint mapping utilities * Variable declaration helpers

Model conversion (smt2model2fzn.py): * Converts SMT2 model output back to FlatZinc format * Useful for round-trip conversions

Command-Line Interface (aria/cli/fmldoc.py)

A unified command-line interface for format translation with auto-detection capabilities.

Translate command:

aria-fmldoc translate -i input.cnf -o output.smt2 --input-format dimacs --output-format smtlib2

Auto-detect formats:

aria-fmldoc translate -i input.cnf -o output.smt2 --auto-detect

Supported format pairs:

  • dimacs → smtlib2

  • dimacs → lp

  • dimacs → sympy

  • qdimacs → smtlib2

  • sygus → smtlib2

  • smtlib2 → c

  • smtlib2 → sympy

  • wcnf → smtlib2

Other commands:

  • validate: Validate file format correctness

  • analyze: Analyze constraint properties (variable counts, clause counts, etc.)

  • batch: Batch process multiple files

Format detection:

The CLI can auto-detect formats from file extensions:

  • .cnf → dimacs

  • .qdimacs → qdimacs

  • .smt2 → smtlib2

  • .sy → sygus

  • .lp → lp

  • .fzn → fzn

Examples

Converting DIMACS to SMT-LIB2

from aria.translator import dimacs2smt

# Convert DIMACS CNF to SMT2
dimacs2smt.convert_dimacs_to_smt2(
    "formula.cnf",
    "formula.smt2",
    logic="QF_UF"
)

Converting QDIMACS to SMT-LIB2

from aria.translator import qbf2smt
import sys

# Convert QDIMACS file
qbf2smt.parse("formula.qdimacs")

Using CNF to Z3 conversion

from aria.translator import cnf2smt
import z3

# Load CNF and check satisfiability
formula = cnf2smt.dimacs_to_z3("instance.cnf")
solver = z3.Solver()
solver.add(formula)

if solver.check() == z3.sat:
    model = solver.model()
    print("Satisfiable:", model)

Weighted MaxSAT with Z3

from aria.translator import wcnf2z3
from z3 import *

# Load weighted CNF
with open("instance.wcnf") as f:
    opt, soft = wcnf2z3.construct_z3_optimizer(f)

# Solve MaxSAT
if opt.check() == sat:
    model = opt.model()
    print("Optimal solution found")

Applications

  • Format interoperability: Convert between different constraint formats

  • Solver integration: Prepare inputs for various SMT and SAT solvers

  • Model counting: Generate C code for efficient model enumeration

  • Symbolic analysis: Convert to SymPy for symbolic manipulation

  • Synthesis: Convert SyGuS instances for SMT-based synthesis

  • Optimization: Convert weighted constraints for MaxSAT solving

  • Constraint programming: Bridge between FlatZinc and OMT solvers

References