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

# SMT Solving

> Using SMT solvers to verify logical validity of first-order formulas

## What is SMT Solving?

SMT (Satisfiability Modulo Theories) solving is a technique for checking the satisfiability of logical formulas with respect to combinations of background theories. SMT solvers extend SAT (Boolean satisfiability) solvers by supporting reasoning about data types, arithmetic, arrays, and other structures.

<Info>
  The NL2FOL system uses SMT solvers to automatically verify whether a logical argument is valid or contains a fallacy.
</Info>

## Why Use SMT Solvers?

SMT solvers provide several advantages for logical verification:

<CardGroup cols={2}>
  <Card title="Automation" icon="robot">
    Automatically check validity without manual proof construction
  </Card>

  <Card title="Efficiency" icon="gauge-high">
    Modern solvers can handle complex formulas with many variables
  </Card>

  <Card title="Soundness" icon="shield-check">
    Guaranteed correct results based on formal logic
  </Card>

  <Card title="Completeness" icon="circle-check">
    Can determine SAT, UNSAT, or UNKNOWN for any formula
  </Card>
</CardGroup>

## From FOL to SMT-LIB

The NL2FOL system converts first-order logic formulas to **SMT-LIB format**, a standardized input language for SMT solvers.

### SMT-LIB Format

SMT-LIB uses S-expressions (similar to Lisp) to represent logical formulas:

```lisp theme={null}
(set-logic ALL)
(declare-fun IsTall (BoundSet) Bool)
(declare-fun LovesCheese (BoundSet) Bool)
(assert (not 
  (=> 
    (exists ((x BoundSet)) (and (IsTall x) (LovesCheese x)))
    (forall ((y BoundSet)) (=> (IsTall y) (LovesCheese y)))
  )
))
(check-sat)
```

## The CVCGenerator Class

The `CVCGenerator` class (`src/cvc.py`) handles the conversion from FOL to SMT-LIB format.

### Architecture

```python theme={null}
# From src/cvc.py:203-213
class CVCGenerator:
    def __init__(self, formula):
        bound_variables.clear()
        unbound_variables.clear()
        predicate_to_sort_map.clear()
        self.formula = formula
        self.tokens = self.tokenize()
```

### Key Components

<Accordion title="Tokenization">
  The first step is to break down the formula into tokens:

  ```python theme={null}
  # From src/cvc.py:214-231
  def tokenize(self):
      tokens = re.split(r'(\(|\)|\s|\bexists\b|\band\b|\bor\b|\bnot\b|\bforall\b|\->|<->|,|<=>|=>|=)', 
                       self.formula)
      result = []
      for token in tokens:
          if token not in ['', ' ']:
              if token == '->':
                  result.append("=>")
              elif token in ['<->', '<=>']:
                  result.append("=")
              else:
                  result.append(token)
      return CVCGenerator.process_tokens(result)
  ```

  This converts the formula string into a list of tokens, normalizing operators.
</Accordion>

<Accordion title="Operator Handling">
  The system defines an `Operator` class to manage logical operators:

  ```python theme={null}
  # From src/cvc.py:28-73
  class Operator:
      def __init__(self, operator):
          self.operator = operator
          self.quantifier = ("exists" in operator or "forall" in operator)
          self.arity = 1 if operator == "not" or self.quantifier else 2
          self.priority = Operator.priority_values(operator)
      
      @staticmethod
      def priority_values(op):
          if op == "not":
              return 5
          elif "exists" in op or "forall" in op:
              return 4
          elif op == "and":
              return 3
          elif op == "or":
              return 2
          elif op in ["=>", "="]:
              return 1
  ```

  **Operator Priorities**:

  1. `not` (highest)
  2. `exists`, `forall`
  3. `and`
  4. `or`
  5. `=>`, `=` (lowest)
</Accordion>

<Accordion title="Predicate Processing">
  Predicates are parsed recursively to handle nested structures:

  ```python theme={null}
  # From src/cvc.py:75-126
  class Predicate:
      def __init__(self, predicate_name):
          self.name = predicate_name
          self.terms = []
          self.prefix_form = []
          self.sort = []
      
      def set_terms(self, terms):
          i = 0
          n_parenthesis = 0
          running_tokens = []
          
          while i < len(terms):
              if terms[i] == ',':
                  if n_parenthesis == 0:
                      self.terms.append(CVCGenerator.process_tokens(running_tokens))
                      running_tokens = []
                  else:
                      running_tokens.append(terms[i])
              else:
                  if terms[i] == '(':
                      n_parenthesis += 1
                  elif terms[i] == ')':
                      n_parenthesis -= 1
                  running_tokens.append(terms[i])
              i += 1
          
          self.terms.append(CVCGenerator.process_tokens(running_tokens))
  ```

  This handles predicates with multiple arguments, including nested predicates.
</Accordion>

## Sort System

The sort system ensures type consistency across predicates.

### Sort Types

<CardGroup cols={3}>
  <Card title="BoundSet" icon="link">
    For variables bound by quantifiers (exists/forall)
  </Card>

  <Card title="UnboundSet" icon="circle">
    For free variables without quantifiers
  </Card>

  <Card title="Bool" icon="toggle-on">
    For boolean expressions and compound formulas
  </Card>
</CardGroup>

### Sort Inference

```python theme={null}
# From src/cvc.py:128-149
def find_sort(self):
    self.sort = []
    for term in self.terms:
        if len(term) == 1:
            # Single token - must be a variable
            if term[0] in bound_variables:
                self.sort.append(Sort("BoundSet"))
            else:
                if term[0] not in unbound_variables:
                    unbound_variables[term[0]] = Sort()
                self.sort.append(unbound_variables[term[0]])
        else:
            # Multiple tokens - boolean expression
            self.sort.append(Sort("Bool"))
    
    self.unify_sort()
```

### Sort Unification

The system ensures predicates are used consistently:

```python theme={null}
# From src/cvc.py:155-185
def unify_sort(self):
    if self.name not in predicate_to_sort_map:
        predicate_to_sort_map[self.name] = self.sort
    else:
        cur_sort = predicate_to_sort_map[self.name]
        if len(cur_sort) != len(self.sort):
            raise Exception("Sorts of {0} is not consistent.".format(self.name))
        for i in range(len(cur_sort)):
            cur_sort[i] = self.unify(cur_sort[i], self.sort[i])

def unify(self, sort1, sort2):
    sort1_sort = sort1.getSort() if sort1 else None
    sort2_sort = sort2.getSort() if sort2 else None
    
    if sort1_sort == sort2_sort:
        return sort1
    elif sort1_sort is None:
        sort1.setSort(sort2_sort)
        return sort2
    elif sort2_sort is None:
        sort2.setSort(sort1_sort)
        return sort1
    else:
        raise Exception("Sorts of {0} are not consistent".format(self.name))
```

<Note>
  If a predicate is used with inconsistent sorts (e.g., `IsTall(x)` where x is BoundSet in one place and UnboundSet in another), the system raises an exception.
</Note>

## Prefix Form Conversion

SMT-LIB uses prefix notation (operator before operands). The system converts infix to prefix:

### Algorithm

```python theme={null}
# From src/cvc.py:281-346
@staticmethod
def infixToPostfix(infix):
    if len(infix) == 1:
        return infix
    
    infix = ["("] + infix + [")"]
    op_stack = []
    output = []
    
    i = 0
    while i < len(infix):
        if infix[i] == "(":
            op_stack.append(infix[i])
        elif infix[i] == ")":
            while op_stack[-1] != "(":
                operator = op_stack.pop()
                if operator.quantifier:
                    bound_variables.remove(operator.quanified_variable)
                output.append(operator)
            op_stack.pop()
        elif isOperator(infix[i]):
            while op_stack[-1] != '(' and infix[i].getPriority() <= op_stack[-1].getPriority():
                operator = op_stack.pop()
                if operator.quantifier:
                    bound_variables.remove(operator.quanified_variable)
                output.append(operator)
            
            if infix[i].quantifier:
                op, variable = str(infix[i]).split(" ")
                op_stack.append(Operator(op + " ((" + variable + " BoundSet" + "))"))
                bound_variables.add(variable)
            else:
                op_stack.append(infix[i])
        else:
            output.append(infix[i])
        i += 1
    
    return output
```

### Parenthesization

```python theme={null}
# From src/cvc.py:348-383
@staticmethod
def generatePrefixFormula(tokens):
    infix = tokens[::-1]  # Reverse
    
    # Swap parentheses
    for i in range(len(infix)):
        if infix[i] == "(":
            infix[i] = ")"
        elif infix[i] == ")":
            infix[i] = "("
    
    reverse_postfix = CVCGenerator.infixToPostfix(infix)
    
    stack = []
    for token in reverse_postfix:
        if not isOperator(token):
            stack.append(token)
        else:
            arity = Operator.getOperatorArity(token)
            if arity == 1:
                operand = stack.pop()
                parenthesized_expr = "("+ str(token) + " " + str(operand) +")"
            else: 
                operand1 = stack.pop()
                operand2 = stack.pop()
                parenthesized_expr = "(" + str(token) + " " + str(operand1) + " " + str(operand2) + ")"
            stack.append(parenthesized_expr)
    
    return stack[0]
```

<Tip>
  The conversion works by:

  1. Reversing the infix formula
  2. Swapping parentheses
  3. Converting to postfix
  4. Building prefix expressions from the stack
</Tip>

## Generating the SMT Script

The final step produces a complete SMT-LIB script:

```python theme={null}
# From src/cvc.py:385-413
def generateCVCScript(self, finite_model_finding=False):
    # Initial declarations
    cvc_str = "(set-logic ALL)\n(set-option :produce-models true)\n"
    cvc_str += "(declare-sort BoundSet 0)\n(declare-sort UnboundSet 0)"
    
    if finite_model_finding:
        cvc_str += "\n(set-option :finite-model-find true)"
    
    prefix_formula = CVCGenerator.generatePrefixFormula(self.tokens)
    
    # Declare unbound variables
    for variable in unbound_variables:
        if not unbound_variables[variable].getSort():
            unbound_variables[variable].setSort("UnboundSet")
        cvc_str += "\n(declare-fun {0} () {1})".format(variable, unbound_variables[variable])
    
    # Declare predicates
    for predicate in predicate_to_sort_map:
        sort = " ".join([str(s) for s in predicate_to_sort_map[predicate]])
        cvc_str += "\n(declare-fun {0} ({1}) Bool)".format(predicate, sort)
    
    # Assert negation of the formula
    cvc_str += "\n(assert (not {0}))".format(prefix_formula)
    
    # Check satisfiability
    cvc_str += "\n(check-sat)\n(get-model)"
    return cvc_str
```

### Script Structure

<Accordion title="1. Logic Declaration">
  ```lisp theme={null}
  (set-logic ALL)
  (set-option :produce-models true)
  ```

  Sets the logic to ALL (supports all theories) and enables model generation.
</Accordion>

<Accordion title="2. Sort Declarations">
  ```lisp theme={null}
  (declare-sort BoundSet 0)
  (declare-sort UnboundSet 0)
  ```

  Declares custom sorts for bound and unbound variables.
</Accordion>

<Accordion title="3. Variable Declarations">
  ```lisp theme={null}
  (declare-fun a () UnboundSet)
  (declare-fun b () BoundSet)
  ```

  Declares free variables with their sorts.
</Accordion>

<Accordion title="4. Predicate Declarations">
  ```lisp theme={null}
  (declare-fun IsTall (BoundSet) Bool)
  (declare-fun LovesCheese (BoundSet) Bool)
  ```

  Declares predicates with their argument sorts and return type.
</Accordion>

<Accordion title="5. Assertion">
  ```lisp theme={null}
  (assert (not 
    (=> 
      (exists ((x BoundSet)) (and (IsTall x) (LovesCheese x)))
      (forall ((y BoundSet)) (=> (IsTall y) (LovesCheese y)))
    )
  ))
  ```

  Asserts the **negation** of the formula. If this is satisfiable, the original formula is invalid.
</Accordion>

<Accordion title="6. Satisfiability Check">
  ```lisp theme={null}
  (check-sat)
  (get-model)
  ```

  Checks if the assertion is satisfiable and requests a model if so.
</Accordion>

## Interpreting Results

SMT solvers return one of three results:

<CardGroup cols={3}>
  <Card title="SAT" icon="check">
    **Satisfiable**

    A model exists that satisfies the formula

    For negated fallacies: **FALLACY DETECTED**
  </Card>

  <Card title="UNSAT" icon="xmark">
    **Unsatisfiable**

    No model can satisfy the formula

    For negated fallacies: **VALID ARGUMENT**
  </Card>

  <Card title="UNKNOWN" icon="question">
    **Unknown**

    Solver couldn't determine result (timeout, complexity)

    May need different solver or simplification
  </Card>
</CardGroup>

### Example: Detecting a Fallacy

<Tip>
  Let's see how the solver detects a hasty generalization:
</Tip>

**Formula**: `exists x (IsTall(x) and LovesCheese(x)) -> forall y (IsTall(y) -> LovesCheese(y))`

**Negated**: `NOT(exists x (IsTall(x) and LovesCheese(x)) -> forall y (IsTall(y) -> LovesCheese(y)))`

This is equivalent to:

```
exists x (IsTall(x) and LovesCheese(x)) AND exists y (IsTall(y) and NOT(LovesCheese(y)))
```

**Interpretation**: There exists a tall person who loves cheese, AND there exists a tall person who doesn't love cheese.

**Result**: **SAT** - This is satisfiable! The model shows:

* x is tall and loves cheese
* y is tall and doesn't love cheese

Since the negation is SAT, the original formula is **invalid** → **FALLACY DETECTED**

## Finite Model Finding

For some formulas, the system enables finite model finding:

```python theme={null}
def generateCVCScript(self, finite_model_finding=False):
    cvc_str = "(set-logic ALL)\n(set-option :produce-models true)\n"
    cvc_str += "(declare-sort BoundSet 0)\n(declare-sort UnboundSet 0)"
    
    if finite_model_finding:
        cvc_str += "\n(set-option :finite-model-find true)"
```

<Info>
  Finite model finding restricts the solver to search only finite domains, which can improve performance for certain types of formulas.
</Info>

## Command-Line Usage

The CVC generator can be used directly from the command line:

```bash theme={null}
python cvc.py "exists x (IsTall(x) and LovesCheese(x)) -> forall y (IsTall(y) -> LovesCheese(y))"
```

```python theme={null}
# From src/cvc.py:415-423
if __name__ == "__main__":
    if len(sys.argv) != 2:
        print('Usage: python cvc.py "<fol>"')
        sys.exit(1)

    script = CVCGenerator(
        sys.argv[1].replace("ForAll", "forall")
                   .replace("ThereExists", "exists")
                   .replace("&", "and")
                   .replace("~", "not ")
    ).generateCVCScript()
    print(script)
```

## Integration with SMT Solvers

The generated SMT-LIB scripts can be used with various solvers:

<CardGroup cols={2}>
  <Card title="CVC5" icon="c">
    Modern SMT solver with excellent performance

    ```bash theme={null}
    cvc5 script.smt2
    ```
  </Card>

  <Card title="Z3" icon="z">
    Microsoft's powerful SMT solver

    ```bash theme={null}
    z3 script.smt2
    ```
  </Card>
</CardGroup>

<Note>
  While the module is named `cvc.py`, the SMT-LIB format it generates is compatible with any SMT-LIB 2.0 compliant solver, including Z3, CVC4, CVC5, and others.
</Note>

## Performance Considerations

### Complexity Factors

1. **Number of quantifiers**: More quantifiers increase search space
2. **Nesting depth**: Deeply nested formulas are harder to solve
3. **Number of predicates**: More predicates means more possible interpretations
4. **Domain size**: Larger domains (when specified) increase complexity

### Optimization Strategies

<Accordion title="Minimize Quantifier Alternation">
  Avoid alternating between exists and forall when possible, as this creates high complexity.
</Accordion>

<Accordion title="Use Finite Model Finding Selectively">
  Enable finite model finding for formulas where infinite domains are unnecessary.
</Accordion>

<Accordion title="Simplify Before Solving">
  Apply logical simplifications (e.g., removing double negations) before passing to solver.
</Accordion>

## Next Steps

<CardGroup cols={2}>
  <Card title="First-Order Logic" icon="function" href="/concepts/first-order-logic">
    Review FOL fundamentals and notation
  </Card>

  <Card title="Translation Pipeline" icon="diagram-project" href="/concepts/translation-pipeline">
    See how natural language becomes FOL
  </Card>

  <Card title="API Reference" icon="code" href="/api/cvc-generator">
    Use the CVCGenerator class
  </Card>

  <Card title="Quick Start" icon="rocket" href="/quickstart">
    Try the complete system
  </Card>
</CardGroup>