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

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

Example

from cvc import CVCGenerator

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

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

print(script)

(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)

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

Consistent Sorts

# 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

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

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>"

Example

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

(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)

Integration Example

Complete Pipeline

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:

Show Sort Inconsistency

Exception: "Sorts of <predicate> is not consistent."

Raised when a predicate is used with different arities or argument sorts.

Show Unbalanced Parentheses

May result in parsing errors or incorrect formulas. Ensure input formulas have balanced parentheses.

The generator automatically normalizes operator syntax:

• -> becomes =>
• <-> and <=> become =
• ForAll and ThereExists can be used instead of forall and exists

See Also

• NL2FOL - Generate FOL formulas from natural language
• SMTResults - Interpret solver output
• Helper Functions - String processing utilities