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

# CVCGenerator

> Parser and generator for CVC5 SMT solver input files

## Overview

The `CVCGenerator` class parses first-order logic formulas and generates CVC5-compatible SMT-LIB format files. It handles tokenization, operator precedence, predicate arity checking, and sort unification to ensure valid SMT solver input.

## Class Definition

```python theme={null}
class CVCGenerator:
    def __init__(self, formula)
```

### Parameters

<ParamField path="formula" type="str" required>
  First-order logic formula to convert to CVC5 format. Supports standard FOL syntax with:

  * Quantifiers: `exists`, `forall`
  * Operators: `and`, `or`, `not`, `->`, `<->`, `=>`, `<=>`
  * Predicates: Function notation like `P(x, y)`
  * Variables: Single lowercase letters or words
</ParamField>

## Instance Attributes

<ResponseField name="formula" type="str">
  The input first-order logic formula
</ResponseField>

<ResponseField name="tokens" type="list">
  Processed tokens representing the parsed formula structure
</ResponseField>

## Methods

### tokenize

```python theme={null}
def tokenize()
```

Tokenizes the input formula by splitting on operators, parentheses, and whitespace.

**Returns:** `list` - List of processed tokens

**Processing Steps:**

1. Split formula using regex on operators and punctuation
2. Remove empty tokens
3. Normalize operators (`->` → `=>`, `<->` → `=`)
4. Process tokens recursively to handle nested structures

### process\_tokens

```python theme={null}
@staticmethod
def process_tokens(tokens)
```

Processes a list of tokens to identify operators, predicates, and variables.

**Parameters:**

* `tokens` (list): Raw tokens to process

**Returns:** `list` - Processed tokens with Operator and Predicate objects

**Handles:**

* Quantifier identification and variable binding
* Predicate parsing with argument extraction
* Operator object creation

### generatePrefixFormula

```python theme={null}
@staticmethod
def generatePrefixFormula(tokens)
```

Converts infix formula tokens to prefix (Polish) notation for CVC5.

**Parameters:**

* `tokens` (list): Infix tokens to convert

**Returns:** `str` - Prefix notation formula with full parenthesization

**Algorithm:**

1. Reverse the infix expression
2. Convert to postfix using modified Shunting Yard algorithm
3. Reverse postfix to get prefix
4. Add parentheses for all operators

### infixToPostfix

```python theme={null}
@staticmethod
def infixToPostfix(infix)
```

Converts reversed infix expression to postfix using operator precedence.

**Parameters:**

* `infix` (list): Reversed infix tokens

**Returns:** `list` - Postfix token list

**Operator Precedence:**

* `not`: 5 (highest)
* `exists`, `forall`: 4
* `and`: 3
* `or`: 2
* `=>`, `=`: 1 (lowest)

### generateCVCScript

```python theme={null}
def generateCVCScript(finite_model_finding=False)
```

Generates complete CVC5 SMT-LIB script from the formula.

**Parameters:**

<ParamField path="finite_model_finding" type="bool" default="False">
  Enable finite model finding option in CVC5
</ParamField>

**Returns:** `str` - Complete SMT-LIB script ready for CVC5

**Generated Script Structure:**

1. Logic and options (`set-logic ALL`, `set-option :produce-models true`)
2. Sort declarations (`BoundSet`, `UnboundSet`)
3. Variable declarations
4. Predicate function declarations with arities
5. Assert statement with negated formula
6. Check-sat and get-model commands

<CodeGroup>
  ```python Example theme={null}
  from cvc import CVCGenerator

  # Create formula
  formula = "forall x (P(x) -> Q(x))"

  # Generate CVC script
  generator = CVCGenerator(formula)
  script = generator.generateCVCScript()

  print(script)
  ```

  ```smt-lib Output theme={null}
  (set-logic ALL)
  (set-option :produce-models true)
  (declare-sort BoundSet 0)
  (declare-sort UnboundSet 0)
  (declare-fun P (BoundSet) Bool)
  (declare-fun Q (BoundSet) Bool)
  (assert (not (forall ((x BoundSet)) (=> (P x) (Q x)))))
  (check-sat)
  (get-model)
  ```
</CodeGroup>

## Helper Classes

### Sort

```python theme={null}
class Sort:
    def __init__(self, sort=None)
```

Represents a sort (type) in the SMT solver.

**Attributes:**

* `sort` (str): Sort name (`"BoundSet"`, `"UnboundSet"`, or `"Bool"`)

**Methods:**

* `getSort()`: Returns the sort name
* `setSort(sort)`: Sets the sort name

### Operator

```python theme={null}
class Operator:
    def __init__(self, operator)
```

Represents a logical operator with metadata.

**Attributes:**

* `operator` (str): Operator string
* `quantifier` (bool): True if operator is `exists` or `forall`
* `arity` (int): Number of operands (1 for unary, 2 for binary)
* `priority` (int): Operator precedence value
* `quantified_variable` (str): Variable bound by quantifier (if applicable)

**Methods:**

* `getOperatorArity()`: Returns operator arity
* `getPriority()`: Returns operator precedence
* `priority_values(op)`: Static method returning precedence for operator string

### Predicate

```python theme={null}
class Predicate:
    def __init__(self, predicate_name)
```

Represents a predicate with its terms and sorts.

**Attributes:**

* `name` (str): Predicate name
* `terms` (list): List of argument terms (can be nested formulas)
* `prefix_form` (list): Prefix notation of each term
* `sort` (list\[Sort]): Sort of each argument

**Methods:**

* `set_terms(terms)`: Parse and set predicate terms
* `find_sort()`: Determine sorts for all terms
* `unify_sort()`: Ensure consistent sorts across predicate uses
* `unify(sort1, sort2)`: Unify two sort instances

## Global State

The module maintains global state during parsing:

```python theme={null}
bound_variables = set()      # Variables bound by quantifiers
unbound_variables = {}       # Free variables and their sorts
predicate_to_sort_map = {}   # Predicate signatures
```

<Warning>
  Global state is cleared on each `CVCGenerator` instantiation. Avoid creating multiple instances concurrently in multi-threaded contexts.
</Warning>

## Sort Unification

The generator automatically unifies sorts to ensure consistent predicate arities:

1. **Bound Variables**: Variables under quantifiers get `BoundSet` sort
2. **Free Variables**: Assigned `UnboundSet` or unified based on usage
3. **Predicate Arguments**: Must have consistent sorts across all uses
4. **Nested Formulas**: Arguments that are formulas get `Bool` sort

<CodeGroup>
  ```python Consistent Sorts theme={null}
  # Valid: P has consistent arity 1 with BoundSet
  formula = "exists x (P(x) and forall y (Q(y) -> P(y)))"
  generator = CVCGenerator(formula)
  script = generator.generateCVCScript()
  # P and Q both declared as (BoundSet) -> Bool
  ```

  ```python Inconsistent Sorts theme={null}
  # Invalid: Would raise exception if P used with different arities
  try:
      formula = "P(x) and P(x, y)"  # P has arity 1 and 2
      generator = CVCGenerator(formula)
  except Exception as e:
      print(f"Sort error: {e}")
      # Output: "Sorts of P is not consistent."
  ```
</CodeGroup>

## Helper Functions

### isOperator

```python theme={null}
def isOperator(op)
```

Checks if a token is a logical operator.

**Parameters:**

* `op`: Token to check

**Returns:** `bool` - True if token is an operator

**Recognized Operators:**

* `not`, `and`, `or`
* `->`, `<->`, `=>`, `<=>`, `=`
* `exists <var>`, `forall <var>`

## Command-Line Usage

```bash theme={null}
python cvc.py "<formula>"
```

<CodeGroup>
  ```bash Example theme={null}
  python cvc.py "forall x (Cat(x) -> Animal(x))"
  ```

  ```smt-lib Output theme={null}
  (set-logic ALL)
  (set-option :produce-models true)
  (declare-sort BoundSet 0)
  (declare-sort UnboundSet 0)
  (declare-fun Cat (BoundSet) Bool)
  (declare-fun Animal (BoundSet) Bool)
  (assert (not (forall ((x BoundSet)) (=> (Cat x) (Animal x)))))
  (check-sat)
  (get-model)
  ```
</CodeGroup>

## Integration Example

<CodeGroup>
  ```python Complete Pipeline theme={null}
  from nl_to_fol import NL2FOL
  from cvc import CVCGenerator
  import subprocess

  # Step 1: Convert NL to FOL
  sentence = "All birds can fly, so penguins can fly."
  nl2fol = NL2FOL(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 CVC script
  generator = CVCGenerator(fol_formula)
  cvc_script = generator.generateCVCScript(finite_model_finding=True)

  # Step 3: Write to file
  with open("formula.smt2", "w") as f:
      f.write(cvc_script)

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

  print("Solver output:", result.stdout)
  ```
</CodeGroup>

## Error Handling

The generator raises exceptions for:

<Expandable title="Sort Inconsistency">
  ```python theme={null}
  Exception: "Sorts of <predicate> is not consistent."
  ```

  Raised when a predicate is used with different arities or argument sorts.
</Expandable>

<Expandable title="Unbalanced Parentheses">
  May result in parsing errors or incorrect formulas. Ensure input formulas have balanced parentheses.
</Expandable>

<Note>
  The generator automatically normalizes operator syntax:

  * `->` becomes `=>`
  * `<->` and `<=>` become `=`
  * `ForAll` and `ThereExists` can be used instead of `forall` and `exists`
</Note>

## See Also

* [NL2FOL](/api/nl2fol) - Generate FOL formulas from natural language
* [SMTResults](/api/smt-results) - Interpret solver output
* [Helper Functions](/api/helpers) - String processing utilities