Skip to main content

​
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

class CVCGenerator:
    def __init__(self, formula)

​
Parameters

​
formula
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

​
Instance Attributes

​
formula
str
The input first-order logic formula
​
tokens
list
Processed tokens representing the parsed formula structure

​
Methods

​
tokenize

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

@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

@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

@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

def generateCVCScript(finite_model_finding=False)
Generates complete CVC5 SMT-LIB script from the formula. Parameters:
​
finite_model_finding
bool
default:"False"
Enable finite model finding option in CVC5
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
from cvc import CVCGenerator

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

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

print(script)

​
Helper Classes

​
Sort

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

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

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: 
bound_variables = set()      # Variables bound by quantifiers
unbound_variables = {}       # Free variables and their sorts
predicate_to_sort_map = {}   # Predicate signatures
Global state is cleared on each CVCGenerator instantiation. Avoid creating multiple instances concurrently in multi-threaded contexts.

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

​
Helper Functions

​
isOperator

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

python cvc.py "<formula>"

python cvc.py "forall x (Cat(x) -> Animal(x))"

​
Integration Example

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)

​
Error Handling

The generator raises exceptions for:
The generator automatically normalizes operator syntax:
  • -> becomes =>
  • <-> and <=> become =
  • ForAll and ThereExists can be used instead of forall and exists

​
See Also

Build docs developers (and LLMs) love

Get started for freeTalk to us