> ## 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.

# Interpreting SMT Results

> Understand and explain SMT solver outputs with LLM-generated interpretations

## Overview

The `interpret_smt_results.py` script analyzes SMT solver outputs and generates human-readable explanations for logical fallacies. It provides counter-examples when arguments are invalid.

## How It Works

<Steps>
  <Step title="Read SMT Output">
    Loads the solver output file containing SAT/UNSAT result and counter-model.
  </Step>

  <Step title="Parse Result">
    Determines if the formula is valid (UNSAT) or contains a fallacy (SAT).
  </Step>

  <Step title="Load Sentence Data">
    Reads the JSON file with claim, implication, entities, properties, and formula.
  </Step>

  <Step title="Generate Interpretation">
    Uses LLM to interpret the counter-model in natural language (for fallacies only).
  </Step>

  <Step title="Display Results">
    Prints the validity status and human-readable explanation.
  </Step>
</Steps>

## Command Usage

### Basic Command

```bash theme={null}
python3 src/interpret_smt_results.py <output_of_smt_file_path> <json_sentence_data_path>
```

### Parameters

<ParamField path="output_of_smt_file_path" type="string" required>
  Path to the SMT solver output file (e.g., `results/run_name_smt/0_out.txt`).

  This file should contain:

  * First line: `sat` or `unsat`
  * Subsequent lines: Counter-model (if SAT)
</ParamField>

<ParamField path="json_sentence_data_path" type="string" required>
  Path to JSON file containing the sentence analysis data.

  Required fields:

  * `Claim` - The extracted claim
  * `Implication` - The extracted implication
  * `Referring expressions` - Entity mappings
  * `Properties` - Property assignments
  * `Formula` - The FOL formula
</ParamField>

## Example Usage

<CodeGroup>
  ```bash Basic Example theme={null}
  python3 src/interpret_smt_results.py \
    results/experiment_1_smt/0_out.txt \
    results/experiment_1_data/0.json
  ```

  ```bash Multiple Files theme={null}
  # Interpret first 10 results
  for i in {0..9}; do
    python3 src/interpret_smt_results.py \
      results/experiment_1_smt/${i}_out.txt \
      results/experiment_1_data/${i}.json
  done
  ```
</CodeGroup>

## Input File Formats

### SMT Output File Format

**Valid Argument (UNSAT):**

```
unsat
```

**Logical Fallacy (SAT) with Counter-Model:**

```
sat
(model
  (define-fun Human ((x!0 Entity)) Bool
    (ite (= x!0 a) true false))
  (define-fun Mortal ((x!0 Entity)) Bool
    (ite (= x!0 a) false false))
)
```

### JSON Sentence Data Format

```json theme={null}
{
  "Claim": "All humans are mortal",
  "Implication": "Socrates is mortal",
  "Referring expressions": "humans, Socrates",
  "Properties": "Human(a), Mortal(a)",
  "Formula": "forall a (Human(a) -> Mortal(a))"
}
```

## Output Examples

### Valid Statement

```
The given statement is a valid statement
```

### Logical Fallacy with Interpretation

```
The given statement is a logical fallacy

Counter-example explanation:
The argument fails because it assumes all humans are mortal and 
that Socrates is human, but the model shows a case where Socrates 
could be human but not mortal. This violates the logical structure 
of the argument.

Specifically, the counter-model assigns:
- Human(Socrates) = true
- Mortal(Socrates) = false

This demonstrates that the implication does not necessarily follow 
from the claim.
```

## SMTResults Class

The interpretation logic is implemented in the `SMTResults` class:

```python theme={null}
class SMTResults:
    def __init__(self, output_file_path, sentence_data_path):
        # Parse SMT output
        with open(output_file_path, "r") as f:
            results = f.read() + "\n"
        
        sat_or_unsat, counter_model = results.split("\n", 1)
        
        if "unsat" in sat_or_unsat:
            self.formula_type = "valid statement"
            self.counter_example = None
        else:
            self.formula_type = "logical fallacy"
            # Generate LLM interpretation
            self.counter_example = self._generate_interpretation(
                sentence_data, counter_model
            )
```

## LLM-Based Interpretation

For logical fallacies, the system uses an LLM to generate natural language explanations:

<Steps>
  <Step title="Load Prompt Template">
    Reads `prompt_counter_example.txt` containing instructions for interpretation.
  </Step>

  <Step title="Format Prompt">
    Inserts claim, implication, entities, properties, formula, and counter-model.
  </Step>

  <Step title="Query LLM">
    Sends the prompt to the LLM (via `llm.py` helper).
  </Step>

  <Step title="Return Explanation">
    Returns human-readable explanation of why the argument fails.
  </Step>
</Steps>

## Prompt Template

The interpretation prompt (in `prompts/prompt_counter_example.txt`) typically includes:

```
Given the following logical argument:

Claim: {claim}
Implication: {implication}
Referring Expressions: {referring_expressions}
Properties: {properties}
Formula: {formula}

The SMT solver found a counter-model:
{counter_model}

Explain in natural language why this argument is fallacious 
and what the counter-model demonstrates.
```

<Tip>
  Customize the prompt template to adjust the style and detail level of interpretations.
</Tip>

## Usage Methods

### Programmatic Usage

```python theme={null}
from interpret_smt_results import SMTResults

# Create interpreter
results = SMTResults(
    output_file_path="results/exp_smt/0_out.txt",
    sentence_data_path="results/exp_data/0.json"
)

# Get results with interpretation
results.get_results(get_interpretation=True)

# Access properties
print(results.formula_type)      # "valid statement" or "logical fallacy"
print(results.counter_example)   # LLM-generated explanation (or None)
```

### Disable Interpretation

To check validity without generating explanations:

```python theme={null}
results.get_results(get_interpretation=False)
# Only prints: "The given statement is a logical fallacy"
```

<Note>
  Disabling interpretation speeds up batch processing but provides less insight into why arguments fail.
</Note>

## Counter-Model Analysis

The counter-model from the SMT solver shows:

**Function Definitions**: How predicates are interpreted

```smt2 theme={null}
(define-fun Wealthy ((x!0 Entity)) Bool
  (ite (= x!0 a) true false))
```

**Entity Assignments**: Which entities satisfy which properties

```
Wealthy(a) = true
Happy(a) = false
```

**Relationship Violations**: Where the implication breaks down

```
Claim asserts: Wealthy(a)
Implication requires: Happy(a)
Counter-model shows: Wealthy(a) ∧ ¬Happy(a)
```

## Understanding Fallacy Types

Common fallacy patterns revealed by counter-examples:

### Hasty Generalization

**Argument**: "Some wealthy people are happy, therefore all wealthy people are happy."

**Counter-model**: Shows a wealthy person who is not happy.

### False Cause

**Argument**: "A happened before B, therefore A caused B."

**Counter-model**: Shows A and B occurring without causal relationship.

### Composition Fallacy

**Argument**: "Each part has property P, therefore the whole has property P."

**Counter-model**: Shows parts with P but whole without P.

## Batch Processing

For processing multiple results:

```bash theme={null}
#!/bin/bash
# interpret_all.sh

RUN_NAME=$1
NUM_FILES=$2

for i in $(seq 0 $((NUM_FILES - 1))); do
  echo "Processing datapoint $i..."
  python3 src/interpret_smt_results.py \
    results/${RUN_NAME}_smt/${i}_out.txt \
    results/${RUN_NAME}_data/${i}.json \
    > results/${RUN_NAME}_interpretations/${i}.txt
done
```

## Error Handling

### Missing Files

```python theme={null}
try:
    results = SMTResults(output_path, data_path)
except FileNotFoundError as e:
    print(f"Error: File not found - {e}")
```

### Malformed Output

```python theme={null}
try:
    sat_or_unsat, counter_model = results.split("\n", 1)
except ValueError:
    print("Error: SMT output format incorrect")
```

### Invalid JSON

```python theme={null}
import json

try:
    with open(sentence_data_path) as f:
        data = json.load(f)
except json.JSONDecodeError:
    print("Error: Invalid JSON format")
```

## LLM Configuration

The `llm.py` helper module typically supports:

```python theme={null}
def get_llm_result(prompt, model_type='gpt-4o'):
    # OpenAI API call
    # or local model inference
    pass
```

Configure your LLM provider:

* Set API keys in environment variables
* Adjust model selection for cost/quality tradeoff
* Modify temperature for interpretation creativity

<Warning>
  LLM interpretations require API access (OpenAI) or local model setup. Ensure proper authentication and rate limiting.
</Warning>

## Visualization

Extend the script to generate visual representations:

```python theme={null}
import graphviz

def visualize_counter_model(counter_model):
    dot = graphviz.Digraph()
    # Parse counter_model and create graph
    # ...
    return dot
```

## Next Steps

After interpreting individual results:

1. Aggregate results across the dataset
2. Calculate evaluation metrics (accuracy, precision, recall, F1)
3. Analyze patterns in fallacy types
4. Refine FOL translation based on error analysis

See [Evaluation Metrics](/usage/evaluation) for performance analysis.