> ## Documentation Index
> Fetch the complete documentation index at: https://mintlify.com/lovishchopra/NL2FOL/llms.txt
> Use this file to discover all available pages before exploring further.

# FOL to SMT Conversion

> Convert first-order logic formulas to SMT-LIB format and run CVC4/CVC5 solver

## Overview

The `fol_to_cvc.py` script converts first-order logic formulas into SMT-LIB format and executes the CVC4 solver to check satisfiability. This determines whether logical arguments are valid or contain fallacies.

## How It Works

<Steps>
  <Step title="Load FOL Formulas">
    Reads the CSV file generated by `nl_to_fol.py` containing logical formulas.
  </Step>

  <Step title="Generate SMT Scripts">
    Uses the `CVCGenerator` class to convert FOL formulas to SMT-LIB format.
  </Step>

  <Step title="Run CVC4 Solver">
    Executes the SMT solver on each formula to check satisfiability.
  </Step>

  <Step title="Handle Unknown Results">
    If solver returns "unknown", retries with finite model finding enabled.
  </Step>

  <Step title="Interpret Results">
    Maps solver output to validity classification:

    * `unsat` = Valid argument
    * `sat`/`unknown` = Logical fallacy (LF)
  </Step>

  <Step title="Save Results">
    Outputs results to CSV with validity predictions.
  </Step>
</Steps>

## Command Usage

### Basic Command

```bash theme={null}
python3 src/fol_to_cvc.py <run_name>
```

### Parameters

<ParamField path="run_name" type="string" required>
  The name of the run from nl\_to\_fol.py. The script will:

  * Read from: `results/<run_name>.csv`
  * Create SMT files in: `results/<run_name>_smt/`
  * Save results to: `results/<run_name>_results.csv`
</ParamField>

## Example Usage

<CodeGroup>
  ```bash Basic Usage theme={null}
  python3 src/fol_to_cvc.py llama_experiment_1
  ```

  ```bash With Output Directory theme={null}
  # Creates results/llama_experiment_1_smt/ directory
  # with individual .smt2 and _out.txt files
  python3 src/fol_to_cvc.py llama_experiment_1
  ```
</CodeGroup>

## Prerequisites

<Warning>
  **CVC4 Solver Required**

  The script requires the CVC4 SMT solver binary (`./cvc4`) in the working directory.

  Download from: [https://github.com/CVC4/CVC4/releases](https://github.com/CVC4/CVC4/releases)

  Make executable:

  ```bash theme={null}
  chmod +x cvc4
  ```
</Warning>

## SMT-LIB Format

The FOL formulas are converted to SMT-LIB2 format. The system handles:

### Operator Conversions

| FOL Syntax    | SMT-LIB Syntax       |
| ------------- | -------------------- |
| `ForAll`      | `forall`             |
| `ThereExists` | `exists`             |
| `&`           | `and`                |
| `~`           | `not`                |
| `->`          | Implication operator |

### Example Conversion

**Input FOL:**

```
forall a (Human(a) -> Mortal(a))
```

**Output SMT-LIB:**

```smt2 theme={null}
(set-logic ALL)
(declare-sort Entity 0)
(declare-fun Human (Entity) Bool)
(declare-fun Mortal (Entity) Bool)

(assert (not 
  (forall ((a Entity))
    (=> (Human a) (Mortal a))
  )
))

(check-sat)
(get-model)
```

## Output Files

For each datapoint `i`, the script generates:

### SMT Files

**`results/<run_name>_smt/i.smt2`**
The SMT-LIB formatted formula file.

**`results/<run_name>_smt/i_out.txt`**
The solver output containing:

* First line: `sat`, `unsat`, or `unknown`
* Remaining lines: Counter-model (if sat)

### Results CSV

**`results/<run_name>_results.csv`**

Adds a `result` column to the original CSV:

* `Valid` - Formula is unsatisfiable (valid argument)
* `LF` - Formula is satisfiable or unknown (logical fallacy)
* Empty string - Processing error

## Finite Model Finding

When the solver returns `unknown`, the script automatically retries with finite model finding:

```python theme={null}
script = CVCGenerator(fol).generateCVCScript(
    finite_model_finding=True
)
```

This helps resolve formulas that are undecidable in the infinite domain.

<Note>
  Finite model finding can significantly increase solving time but improves coverage for complex formulas.
</Note>

## Understanding Results

### UNSAT (Valid Argument)

When the SMT solver returns `unsat`, it means:

* The negation of the formula is unsatisfiable
* No counter-example exists
* The original argument is logically valid

### SAT (Logical Fallacy)

When the SMT solver returns `sat`, it means:

* A counter-example exists
* The argument contains a logical fallacy
* The model shows why the implication doesn't hold

### Unknown

When the solver returns `unknown`:

* The formula is too complex for automatic decision
* Classified as potential fallacy (conservative approach)
* Retry with finite model finding may resolve

## Processing Flow

```mermaid theme={null}
graph TD
    A[Load CSV] --> B[Extract FOL Formula]
    B --> C[Generate SMT Script]
    C --> D[Run CVC4]
    D --> E{Result?}
    E -->|UNSAT| F[Mark as Valid]
    E -->|SAT| G[Mark as LF]
    E -->|UNKNOWN| H[Retry with FMF]
    H --> I{Result?}
    I -->|UNSAT| F
    I -->|SAT/UNKNOWN| G
    F --> J[Save to CSV]
    G --> J
```

## Performance Considerations

<Tip>
  **Processing Time**

  * Simple formulas: \< 1 second per formula
  * Complex formulas: 5-30 seconds
  * Formulas requiring FMF: 30-120 seconds

  Consider parallel processing for large datasets.
</Tip>

## Error Handling

The script includes comprehensive error handling:

```python theme={null}
try:
    # Generate and run SMT
    script = CVCGenerator(fol).generateCVCScript()
    # ...
except Exception as e:
    print("Cannot run this statement : {}".format(e))
    results.append("")  # Mark as error
    pass
```

Errors result in empty strings in the results column, which are excluded from evaluation metrics.

## CVCGenerator Class

The `CVCGenerator` class (from `cvc.py`) handles:

* FOL parsing
* SMT-LIB syntax generation
* Sort and function declarations
* Formula negation (for validity checking)

<Note>
  The solver checks the **negation** of the formula. If the negation is unsatisfiable, the original formula is valid.
</Note>

## Troubleshooting

### Common Issues

**CVC4 not found**

```bash theme={null}
# Ensure cvc4 binary is in current directory or PATH
ls -l ./cvc4
```

**Permission denied**

```bash theme={null}
chmod +x ./cvc4
```

**Directory not found**

```bash theme={null}
# Ensure SMT output directory exists
mkdir -p results/<run_name>_smt/
```

**Parsing errors**

* Check that FOL formulas are well-formed
* Verify all operators are properly converted
* Review `Logical Form 2` column for malformed expressions

## Alternative Solvers

While the script uses CVC4, you can adapt it for other SMT solvers:

**CVC5** (newer version)

```bash theme={null}
./cvc5 --lang smt2 results/<run_name>_smt/0.smt2
```

**Z3**

```bash theme={null}
z3 results/<run_name>_smt/0.smt2
```

<Warning>
  Different solvers may produce different results on undecidable formulas. CVC4 is recommended for consistency with the paper's results.
</Warning>

## Next Steps

After generating SMT results:

1. Interpret individual results with counter-examples using `interpret_smt_results.py`
2. Evaluate overall performance using `get_metrics.py`
3. Analyze error cases and improve FOL translation

See [Interpreting Results](/usage/interpretation) for detailed result analysis.