SMT Tools

The smttools module provides interfaces to various SMT solvers and related utilities for handling SMT-LIB format formulas.

Architecture

efmc/smttools/
├── smtlib_solver.py    # SMT-LIB interactive process interface
├── sygus_solver.py     # SyGuS solver interface
├── pysmt_solver.py     # PySMT-based solver wrapper
├── mapped_blast.py     # Bit-blasting utilities
├── smt_exceptions.py   # Exception definitions
└── __init__.py         # Module exports

SMT-LIB Solver Interface

The smtlib_solver module provides an interactive interface to SMT solvers that support the SMT-LIB 2 format.

SmtlibProc

Main class for interacting with SMT-LIB compliant solvers.

from efmc.smttools.smtlib_solver import SmtlibProc

# Create solver interface
solver = SmtlibProc("z3 -smt2 -in")

# Start the solver process
solver.start()

# Send commands and get responses
solver.write("(set-logic QF_BV)")
response = solver.read()

# Check satisfiability
solver.write("(check-sat)")
response = solver.read()  # "sat", "unsat", or "unknown"

# Close the solver
solver.close()

Available Solvers

EFMC supports the following SMT solvers:

• Z3: Microsoft Research’s SMT solver

• CVC5: The SMT solver from Stanford AI Lab

• Yices2: SRI’s SMT solver

• Bitwuzla: The SMT solver for bit-vectors and arrays

• MathSAT: The MathSAT5 SMT solver

Example usage:

from efmc.smttools.smtlib_solver import SmtlibProc

# Use Z3
z3_solver = SmtlibProc("z3 -smt2 -in")

# Use CVC5
cvc5_solver = SmtlibProc("cvc5 --lang=smt2 --incremental")

# Use Bitwuzla
bitwuzla_solver = SmtlibProc("bitwuzla --sat")

SyGuS Solver Interface

The sygus_solver module provides support for Syntax-Guided Synthesis (SyGuS) problems.

from efmc.smttools.sygus_solver import SyGuSSolver

solver = SyGuSSolver()
solver.set_options([
    "--generate-synth-assumptions",
    "--cegqi-si-all"
])

# Submit synthesis problem
solver.write("(set-logic LIA)")
solver.write("(synth-fun f ((x Int)) Int)")

# Get solution
solution = solver.get_synth_solution()

PySMT Integration

The pysmt_solver module provides integration with PySMT, enabling solver-agnostic SMT solving.

from pysmt.shortcuts import Symbol, Int, GT, Plus
from efmc.smttools.pysmt_solver import PySMTZ3Solver

# Create solver
solver = PySMTZ3Solver()

# Create formula
x = Symbol("x", Int())
y = Symbol("y", Int())

formula = GT(Plus(x, y), Int(0))

# Solve
solver.add_assertion(formula)
result = solver.solve()

Mapped Blast

The mapped_blast module provides utilities for bit-blasting SMT formulas, converting them to CNF format.

from efmc.smttools.mapped_blast import BitBlaster

blaster = BitBlaster()
cnf = blaster.bv_to_cnf(bv_formula)
blaster.dump_cnf(cnf, "output.cnf")

Exception Handling

Custom exceptions for SMT-related errors:

from efmc.smttools.smt_exceptions import SolverError, SolverTimeout

try:
    result = solver.solve()
except SolverTimeout:
    print("Solver timed out")
except SolverError as e:
    print(f"Solver error: {e}")

Supported Logics

The following SMT logics are supported:

• QF_BV: Quantifier-free bit-vectors

• QF_UFBV: Unbounded bit-vectors

• QF_LIA: Quantifier-free linear integer arithmetic

• QF_LRA: Quantifier-free linear real arithmetic

• QF_NIA: Non-linear integer arithmetic

• QF_NRA: Non-linear real arithmetic

• QF_FP: Floating-point arithmetic

• QF_SLIA: String length integer arithmetic

API Reference

SMTLIB solver interface.

Partially modified from https://github.com/trailofbits/manticore TODO: allow the user to select different modes 1. Use the same process to first accept the whole formula, and then accept

multiple (check-sat-assuming) commands?

2. Every time, create a new process the solve each individual instance (including formulas and check-sat-assuming)

TODO: we need to consider three “incremental mode” 1. Every time build new assertions

• build new solver process + new assertions?

• reuse the solver process, but use reset command? (it seems that reset can affect the tactic)

2. Use push/pop

3. Use assumption literal

class efmc.smttools.smtlib_solver.SMTLIBSolver(solver_command: str, debug=False)

Bases: object

SMTLIB solver interface using external solver via subprocess.

assert_assertions(assertions: str)

Add new assertions

check_sat()

check sat

check_sat_assuming(assumptions: List[str])

Parameters:

assumptions – a list of assumption literal

FIXME: implement and test; figure out what should “assumptions” look like

check_sat_from_scratch(whole_fml: str)

Check the satisfiability of the current state :param whole_fml: should be a whole formula (with declaration,

assertions, and check-sat)

Returns:

whether current state is satisfiable or not.

check_sat_with_pushpop_scope(new_assertions: str)

Parameters:

new_assertions – is a tmp cnt

FIXME: implement and test

get_expr_values(expressions: List[str])

If satisfiable, fetch the values of expressions

get_unsat_core()

Get the unsat core. FIXME: implement and test

pop()

Recall the last pushed constraint store and state.

push()

Pushes and save the current constraint store and state.

reset()

Auxiliary method to reset the smtlib external solver to initial defaults TODO: Z3 and CVC5 supports the “reset” cmd. Maybe can use it

stop()

Stop the solver process.

class efmc.smttools.smtlib_solver.SmtlibProc(solver_command: str, debug=False)

Bases: object

Single SMTLIB interactive process.

clear_buffers()

is_started()

recv(wait=True)

Reads the response from the smtlib solver :param wait: a boolean that indicate to wait with a blocking call until the results are available. Otherwise, it returns None if the solver does not respond.

send(cmd: str)

Send a string to the solver. :param cmd: a SMTLIBv2 command (ex. (check-sat))

start()

Spawns POpen solver process

stop()

Stops the solver process by: - sending a SIGKILL signal, - waiting till the process terminates (so we don’t leave a zombie process)

SyGuS (Syntax-Guided Synthesis) solver implementation:

1. Build SyGuS instances (PBE and other constraints)

2. Call CVC5 to solve the SyGuS instances

3. Parse function definition from SyGuS result

4. Map the result to Z3py world

Supports synthesis for:

• Integer and Boolean functions

• Bit-vector functions

• String functions

efmc.smttools.sygus_solver.build_sygus_cnt(funcs: List[FuncDeclRef], cnts: List[BoolRef], variables: List[ExprRef], logic='ALL')

Translate specification (written with z3 expr) to SyGuS format

Parameters:

• funcs – a list of function to be synthesized

• cnts – a list of constraints

• variables – a list of variables

• logic – SMT logic to use (default: “ALL”)

Returns:

SyGuS problem as a string

efmc.smttools.sygus_solver.convert_bv_literal(literal: str) → str

Convert a bit-vector literal from SyGuS format to Z3 format.

Parameters:

literal – SyGuS bit-vector literal (e.g., “#b101”, “#x1A”)

Returns:

Z3-compatible bit-vector expression

efmc.smttools.sygus_solver.convert_string_literal(literal: str) → str

Convert a string literal from SyGuS format to Z3 format.

Parameters:

literal – SyGuS string literal

Returns:

Z3-compatible string expression

efmc.smttools.sygus_solver.convert_sygus_expr_to_z3(expr: str, var_dict: Dict[str, int], return_type: str) → str

Convert a SyGuS expression to a Z3 expression.

Parameters:

• expr – SyGuS expression

• var_dict – Dictionary mapping variable names to their indices in the variables list

• return_type – Return type of the expression

Returns:

Z3-compatible expression

efmc.smttools.sygus_solver.get_sort_sexpr(sort: SortRef) → str

Get the SyGuS-compatible S-expression for a Z3 sort.

Parameters:

sort – Z3 sort

Returns:

SyGuS-compatible S-expression for the sort

efmc.smttools.sygus_solver.parse_sygus_solution(cvc5_output: str) → Dict[str, Dict[str, str]]

Parse the output of CVC5 to extract the synthesized functions.

Parameters:

cvc5_output – CVC5 output as a string

Returns:

Dictionary mapping function names to their definitions

efmc.smttools.sygus_solver.replace_fun_with_synthesized_one(formula: ExprRef, func_to_rep: FuncDeclRef, func_def: ExprRef) → ExprRef

Replace an uninterpreted function with a concrete template in a formula.

This is a wrapper around replace_func_with_template for backward compatibility.

Parameters:

• formula – Z3 formula containing the uninterpreted function

• func_to_rep – Uninterpreted function to replace

• func_def – Template to replace the uninterpreted function with

Returns:

Modified formula with the uninterpreted function replaced by the template

efmc.smttools.sygus_solver.solve_sygus(sygus_problem: str, timeout: int = 60) → Optional[str]

Call CVC5 to solve a SyGuS problem.

Parameters:

• sygus_problem – SyGuS problem as a string

• timeout – Timeout in seconds (default: 60)

Returns:

CVC5 output as a string, or None if CVC5 fails or times out

efmc.smttools.sygus_solver.sygus_to_z3(func_name: str, func_def: Dict[str, str], variables: List[ExprRef]) → ExprRef

Convert a SyGuS function definition to a Z3 expression.

Parameters:

• func_name – Name of the function

• func_def – Function definition from parse_sygus_solution

• variables – List of Z3 variables to use in the expression

Returns:

Z3 expression representing the function

efmc.smttools.sygus_solver.synthesize_function(func: FuncDeclRef, constraints: List[BoolRef], variables: List[ExprRef], logic: str = 'ALL', timeout: int = 60, force_cvc5: bool = False) → Optional[ExprRef]

Synthesize a function using SyGuS.

Parameters:

• func – Function to synthesize

• constraints – Constraints the function must satisfy

• variables – Variables used in the constraints

• logic – SMT logic to use (default: “ALL”)

• timeout – Timeout in seconds (default: 60)

• force_cvc5 – If True, always try to use CVC5 even for common functions (default: False)

Returns:

Z3 expression representing the synthesized function, or None if synthesis fails

FIXME: the name of this file can be confusing

Augmenting Z3 using PySMT, e.g., interpolant generation APIs of this file: - to_pysmt_vars: Convert Z3 variables to PySMT variables - PySMTSolver.convert: Convert Z3 formula to PySMT formula - PySMTSolver.check_with_pysmt: Check satisfiability using PySMT solver - PySMTSolver.check_portfolio: Check satisfiability using multiple solvers - PySMTSolver.all_smt: Sample k models of a formula - PySMTSolver.binary_interpolant: Generate binary interpolant (Craig interpolant) - PySMTSolver.sequence_interpolant: Generate sequence interpolant - PySMTSolver.efsmt: Solve exists-forall formula (used by the template-based invariant inference engine)

class efmc.smttools.pysmt_solver.PySMTSolver(debug=False)

Bases: Solver

PySMT-based solver wrapper for Z3.

all_smt(keys: List[ExprRef], bound=5)

Sample k models

binary_interpolant(fml_a: BoolRef, fml_b: BoolRef, solver_name='z3', logic=None)

Binary interpolant

check_portfolio()

Use multiple solvers (in parallel?)

check_with_pysmt()

Check satisfiability using PySMT solver. TODO: build a Z3 model?

static convert(zf: ExprRef)

Convert Z3 formula to PySMT formula. FIXME: if we do not call “pysmt_vars = …”, z3 will report naming warning..

efsmt(evars: List[ExprRef], uvars: List[ExprRef], z3fml: ExprRef, logic=QF_BV, maxloops=None, esolver_name='z3', fsolver_name='z3', verbose=False, timeout=None)

Solves exists x. forall y. phi(x, y)

Parameters:

• evars – Existentially quantified variables

• uvars – Universally quantified variables

• z3fml – Z3 formula representing the constraint

• logic – The logic to use (default: QF_BV)

• maxloops – Maximum number of iterations (default: None, meaning no limit)

• esolver_name – Name of the solver to use for existential solving (default: “z3”)

• fsolver_name – Name of the solver to use for universal solving (default: “z3”)

• verbose – Whether to print debugging information (default: False)

• timeout – Maximum execution time in seconds (default: None, meaning no timeout)

Returns:

“sat”, “unsat”, or “unknown”

sequence_interpolant(formulas: List[ExprRef])

Sequence interpolant

efmc.smttools.pysmt_solver.test()

Test function for PySMTSolver.

efmc.smttools.pysmt_solver.to_pysmt_vars(z3vars: [<class 'z3.z3.ExprRef'>])

Convert a list of Z3 variables to PySMT variables. :param z3vars: A list of Z3 variables to be converted. :type z3vars: list of z3.ExprRef

Returns:

A list of PySMT variables corresponding to the input Z3 variables.

Return type:

list of pysmt.fnode.FNode

Raises:

NotImplementedError – If a variable type is not supported.

The function supports the following Z3 variable types:

• Integer

• Real

• Bit-Vector

• Boolean

This module contains functions for translating SMT2 formulas to CNF and DIMACS format.

It also keeps track of the mapping between bit-vector variables and their corresponding Boolean variables.

TODO: it seems that this file can be slow. We need to profile and optimize it.

efmc.smttools.mapped_blast.bitblast(formula: ExprRef)

Bit-blast a formula to CNF.

efmc.smttools.mapped_blast.collect_vars(exp, seen=None)

Collect all variables in an SMT2 formula. TODO: this can be slow?

efmc.smttools.mapped_blast.dimacs_visitor(exp, table)

Visit an SMT2 formula and return the DIMACS clauses.

efmc.smttools.mapped_blast.dimacs_visitor_numeric(exp, table)

Visit an SMT2 formula and return numeric DIMACS clauses.

efmc.smttools.mapped_blast.is_literal(exp: ExprRef)

Check if an expression is a literal (uninterpreted constant).

efmc.smttools.mapped_blast.map_bitvector(input_vars)

Map bit-vector variables to their corresponding Boolean variables.

efmc.smttools.mapped_blast.proj_id_last(var, n_proj_vars, n_vars)

Convert a projected variable ID to the original variable ID.

Parameters:

• var – The projected variable ID to convert.

• n_proj_vars – The number of projected variables.

• n_vars – The total number of variables.

efmc.smttools.mapped_blast.test_blast(input_file)

efmc.smttools.mapped_blast.to_dimacs(cnf, table, proj_last) → Tuple[List[str], List[str]]

Translate an SMT2 formula to a CNF.

efmc.smttools.mapped_blast.to_dimacs_numeric(cnf, table, proj_last)

Translate an SMT2 formula to numeric clauses.

efmc.smttools.mapped_blast.translate_smt2formula_to_cnf(formula: ExprRef) → Tuple[Dict[str, list], Dict[str, int], List[str], List[str]]

Translate an SMT2 formula to a CNF.

efmc.smttools.mapped_blast.translate_smt2formula_to_cnf_file(formula: ExprRef, output_file: str)

Translate an SMT2 formula to a CNF file.

efmc.smttools.mapped_blast.translate_smt2formula_to_numeric_clauses(formula: ExprRef) → Tuple[Dict[str, list], Dict[str, int], List[str], List[int]]

Translate an SMT2 formula to numeric clauses.

Custom exception hierarchy for SMT-related errors.

exception efmc.smttools.smt_exceptions.SMTError

Bases: Exception

Top level Exception object for custom exception hierarchy.

exception efmc.smttools.smt_exceptions.SmtlibError

Bases: SMTError

Exception for SMTLIB-related errors.

exception efmc.smttools.smt_exceptions.SolverError

Bases: SmtlibError

Exception for solver-related errors.