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

# SMTResults

> Interpreter for SMT solver results and counterexample generation

## Overview

The `SMTResults` class interprets the output from SMT solvers (like CVC5) to determine whether a first-order logic formula represents a valid statement or contains a logical fallacy. It also uses LLMs to generate human-readable counterexamples when fallacies are detected.

## Class Definition

```python theme={null}
class SMTResults:
    def __init__(self, output_file_path, sentence_data_path)
```

### Parameters

<ParamField path="output_file_path" type="str" required>
  Path to the SMT solver output file containing SAT/UNSAT result and model
</ParamField>

<ParamField path="sentence_data_path" type="str" required>
  Path to JSON file containing original sentence data with keys:

  * `Claim`: The claim portion of the sentence
  * `Implication`: The implication portion
  * `Referring expressions`: Entities identified
  * `Properties`: Properties of entities
  * `Formula`: The generated FOL formula
</ParamField>

## Instance Attributes

<ResponseField name="formula_type" type="str">
  Classification of the formula. Values:

  * `"valid statement"`: Formula is satisfiable (UNSAT in negated form)
  * `"logical fallacy"`: Formula is unsatisfiable (SAT in negated form)
</ResponseField>

<ResponseField name="counter_example" type="str | None">
  Human-readable counterexample generated by LLM (only for logical fallacies)
</ResponseField>

## How It Works

The SMT solver receives the **negation** of the original formula. The interpretation logic:

1. **UNSAT Result**: Negation is unsatisfiable → Original formula is valid
2. **SAT Result**: Negation is satisfiable → Original formula is invalid (fallacy)

<Note>
  When the solver returns SAT, it provides a model (counterexample) showing variable assignments that make the negated formula true, thereby disproving the original claim.
</Note>

## Methods

### get\_results

```python theme={null}
def get_results(get_interpretation=True)
```

Prints the interpretation of SMT results to stdout.

**Parameters:**

<ParamField path="get_interpretation" type="bool" default="True">
  Whether to print the counterexample explanation for fallacies
</ParamField>

**Output Format:**

```
The given statement is a <formula_type>
[If fallacy: <counter_example>]
```

<CodeGroup>
  ```python Example: Valid Statement theme={null}
  results = SMTResults("output.txt", "sentence_data.json")
  results.get_results()
  # Output: The given statement is a valid statement
  ```

  ```python Example: Logical Fallacy theme={null}
  results = SMTResults("output.txt", "sentence_data.json")
  results.get_results()
  # Output:
  # The given statement is a logical fallacy
  # Counterexample: The claim assumes all cats are animals,
  # but the implication incorrectly concludes that all animals
  # are cats. A dog is an animal but not a cat.
  ```
</CodeGroup>

## Input File Formats

### SMT Solver Output File

Expected format:

```
sat
(model
  (define-fun x () BoundSet @uc_BoundSet_0)
  (define-fun P ((x!0 BoundSet)) Bool (= x!0 @uc_BoundSet_0))
)
```

Or:

```
unsat
```

### Sentence Data JSON File

Required structure:

```json theme={null}
{
  "Claim": "All cats are animals",
  "Implication": "Therefore, all animals are cats",
  "Referring expressions": "cats, animals",
  "Properties": "Cat(x), Animal(x)",
  "Formula": "forall x (Cat(x) -> Animal(x)) -> forall y (Animal(y) -> Cat(y))"
}
```

## Counterexample Generation

When a fallacy is detected, the class:

1. Loads the original sentence data from JSON
2. Reads the prompt template from `prompt_counter_example.txt`
3. Formats the prompt with:
   * Original claim and implication
   * Referring expressions and properties
   * The FOL formula
   * The SMT solver's model (counterexample)
4. Sends to LLM via `get_llm_result()`
5. Stores the natural language explanation in `self.counter_example`

<Warning>
  The `get_llm_result()` function must be defined in `llm.py` module. Ensure this module is available and properly configured with API credentials.
</Warning>

## Complete Usage Example

<CodeGroup>
  ```python Full Pipeline theme={null}
  import json
  import subprocess
  from nl_to_fol import NL2FOL
  from cvc import CVCGenerator
  from interpret_smt_results import SMTResults

  # Step 1: Convert natural language to FOL
  sentence = "All politicians are corrupt. John is a politician. Therefore, everyone is corrupt."
  nl2fol = NL2FOL(
      sentence=sentence,
      model_type='gpt',
      pipeline=None,
      tokenizer=None,
      nli_model=nli_model,
      nli_tokenizer=nli_tokenizer
  )
  fol_formula, _ = nl2fol.convert_to_first_order_logic()

  # Step 2: Generate CVC5 script
  generator = CVCGenerator(fol_formula)
  cvc_script = generator.generateCVCScript()

  with open("formula.smt2", "w") as f:
      f.write(cvc_script)

  # Step 3: Run SMT solver
  result = subprocess.run(
      ["cvc5", "formula.smt2"],
      capture_output=True,
      text=True
  )

  with open("solver_output.txt", "w") as f:
      f.write(result.stdout)

  # Step 4: Save sentence data
  sentence_data = {
      "Claim": nl2fol.claim,
      "Implication": nl2fol.implication,
      "Referring expressions": nl2fol.claim_ref_exp,
      "Properties": nl2fol.claim_properties,
      "Formula": fol_formula
  }

  with open("sentence_data.json", "w") as f:
      json.dump(sentence_data, f)

  # Step 5: Interpret results
  results = SMTResults("solver_output.txt", "sentence_data.json")
  results.get_results()

  # Access results programmatically
  if results.formula_type == "logical fallacy":
      print(f"\nCounterexample:\n{results.counter_example}")
  ```
</CodeGroup>

## Command-Line Usage

```bash theme={null}
python interpret_smt_results.py <output_file> <sentence_data_json>
```

<CodeGroup>
  ```bash Example theme={null}
  python interpret_smt_results.py solver_output.txt sentence_data.json
  ```

  ```bash Output theme={null}
  The given statement is a logical fallacy
  The claim states that all politicians are corrupt, and John is a
  politician. However, the implication that everyone is corrupt does
  not follow. A counterexample would be: Mary is not a politician and
  is not corrupt, contradicting the conclusion that everyone is corrupt.
  ```
</CodeGroup>

## Error Handling

<Expandable title="File Not Found">
  If either input file doesn't exist, Python will raise `FileNotFoundError`:

  ```python theme={null}
  FileNotFoundError: [Errno 2] No such file or directory: 'output.txt'
  ```

  Ensure both files exist before creating `SMTResults` instance.
</Expandable>

<Expandable title="Invalid JSON Format">
  If `sentence_data.json` is malformed:

  ```python theme={null}
  json.decoder.JSONDecodeError: Expecting property name enclosed in double quotes
  ```

  Validate JSON structure matches expected format.
</Expandable>

<Expandable title="Missing JSON Keys">
  If required keys are missing from sentence data:

  ```python theme={null}
  KeyError: 'Claim'
  ```

  Ensure all required keys are present: `Claim`, `Implication`, `Referring expressions`, `Properties`, `Formula`.
</Expandable>

<Expandable title="Invalid Solver Output">
  If solver output doesn't start with "sat" or "unsat":

  ```python theme={null}
  ValueError: not enough values to unpack
  ```

  Verify the solver output file format is correct.
</Expandable>

## Integration with Evaluation

<CodeGroup>
  ```python Batch Evaluation theme={null}
  import pandas as pd
  from pathlib import Path

  def evaluate_dataset(results_dir):
      """
      Evaluate a batch of SMT results
      """
      results_dir = Path(results_dir)
      evaluations = []
      
      for output_file in results_dir.glob("*_output.txt"):
          # Find corresponding sentence data
          base_name = output_file.stem.replace("_output", "")
          json_file = results_dir / f"{base_name}_data.json"
          
          if not json_file.exists():
              continue
          
          # Interpret results
          results = SMTResults(str(output_file), str(json_file))
          
          evaluations.append({
              "file": base_name,
              "type": results.formula_type,
              "has_counterexample": results.counter_example is not None
          })
      
      return pd.DataFrame(evaluations)

  # Run evaluation
  df = evaluate_dataset("results/")
  print(df['type'].value_counts())
  ```
</CodeGroup>

## Dependencies

The module requires:

* `llm.py`: Must define `get_llm_result(prompt)` function
* `json`: Standard library for JSON parsing
* `sys`: Standard library for command-line arguments
* `prompt_counter_example.txt`: Prompt template file

<Note>
  Ensure `prompt_counter_example.txt` exists in the working directory with appropriate placeholders for claim, implication, referring expressions, properties, formula, and counter model.
</Note>

## See Also

* [NL2FOL](/api/nl2fol) - Generate FOL formulas from natural language
* [CVCGenerator](/api/cvc-generator) - Create SMT solver input files
* [Helper Functions](/api/helpers) - Utility functions for processing