Barretenberg
The ZK-SNARK library at the core of Aztec
Loading...
Searching...
No Matches
Public Member Functions | Private Attributes | List of all members
AcirToSmtLoader Class Reference

Class for loading ACIR (Arithmetic Circuit Intermediate Representation) programs and converting them to SMT format. More...

#include <acir_loader.hpp>

Public Member Functions

 AcirToSmtLoader ()=delete
 
 AcirToSmtLoader (const AcirToSmtLoader &other)=delete
 
 AcirToSmtLoader (AcirToSmtLoader &&other)=delete
 
AcirToSmtLoader & operator= (const AcirToSmtLoader other)=delete
 
AcirToSmtLoader && operator= (AcirToSmtLoader &&other)=delete
 
 ~AcirToSmtLoader ()=default
 
 AcirToSmtLoader (std::string filename)
 Constructs loader from an ACIR program file.
 
acir_format::AcirFormat & get_constraint_systems ()
 Gets the constraint systems from the loaded ACIR program.
 
bb::UltraCircuitBuilder get_circuit_builder ()
 Creates a circuit builder for the loaded program.
 
smt_solver::Solver get_smt_solver ()
 Gets an SMT solver instance.
 
smt_circuit::UltraCircuit get_bitvec_smt_circuit (smt_solver::Solver *solver)
 Creates an SMT circuit for bitvector operations.
 
smt_circuit::UltraCircuit get_field_smt_circuit (smt_solver::Solver *solver)
 Creates an SMT circuit for field operations.
 
smt_circuit::UltraCircuit get_integer_smt_circuit (smt_solver::Solver *solver)
 Creates an SMT circuit for integer operations.
 
smt_circuit::CircuitSchema get_circuit_schema ()
 Gets the circuit schema from the loaded ACIR program.
 

Private Attributes

std::string instruction_name
 Name of the instruction/filename being processed.
 
std::vector< uint8_t > acir_program_buf
 Buffer containing the raw ACIR program data read from file.
 
acir_format::AcirFormat constraint_system
 The parsed constraint system from the ACIR program.
 
msgpack::sbuffer circuit_buf
 Buffer for circuit serialization using MessagePack.
 

Detailed Description

Class for loading ACIR (Arithmetic Circuit Intermediate Representation) programs and converting them to SMT format.

This class handles loading ACIR programs from files and provides functionality to:

  • Convert the ACIR program to various SMT circuit representations
  • Access the underlying constraint systems
  • Build circuits for verification

The loader reads an ACIR program file, creates constraint systems, and allows conversion to different SMT circuit types (bitvector, field, integer) for formal verification.

Definition at line 21 of file acir_loader.hpp.

Constructor & Destructor Documentation

◆ AcirToSmtLoader() [1/4]

AcirToSmtLoader::AcirToSmtLoader ( )
delete

◆ AcirToSmtLoader() [2/4]

AcirToSmtLoader::AcirToSmtLoader ( const AcirToSmtLoader &  other)
delete

◆ AcirToSmtLoader() [3/4]

AcirToSmtLoader::AcirToSmtLoader ( AcirToSmtLoader &&  other)
delete

◆ ~AcirToSmtLoader()

AcirToSmtLoader::~AcirToSmtLoader ( )
default

◆ AcirToSmtLoader() [4/4]

AcirToSmtLoader::AcirToSmtLoader ( std::string  filename)

Constructs loader from an ACIR program file.

Parameters
filenamePath to the ACIR program file to load

Reads the ACIR program from file, initializes the constraint system, and prepares the circuit buffer for later use.

Definition at line 29 of file acir_loader.cpp.

Member Function Documentation

◆ get_bitvec_smt_circuit()

smt_circuit::UltraCircuit AcirToSmtLoader::get_bitvec_smt_circuit ( smt_solver::Solver *  solver)

Creates an SMT circuit for bitvector operations.

Parameters
solverPointer to SMT solver to use
Returns
UltraCircuit configured for bitvector operations

Definition at line 59 of file acir_loader.cpp.

◆ get_circuit_builder()

bb::UltraCircuitBuilder AcirToSmtLoader::get_circuit_builder ( )

Creates a circuit builder for the loaded program.

Returns
UltraCircuitBuilder instance

Creates and returns a circuit builder with predefined variable names:

  • Variable 0 named "a"
  • Variable 1 named "b"
  • Variable 2 named "c"

Definition at line 37 of file acir_loader.cpp.

◆ get_circuit_schema()

smt_circuit::CircuitSchema AcirToSmtLoader::get_circuit_schema ( )

Gets the circuit schema from the loaded ACIR program.

Returns
CircuitSchema instance

Definition at line 54 of file acir_loader.cpp.

◆ get_constraint_systems()

acir_format::AcirFormat & AcirToSmtLoader::get_constraint_systems ( )
inline

Gets the constraint systems from the loaded ACIR program.

Returns
Reference to the ACIR format constraint systems

Definition at line 45 of file acir_loader.hpp.

◆ get_field_smt_circuit()

smt_circuit::UltraCircuit AcirToSmtLoader::get_field_smt_circuit ( smt_solver::Solver *  solver)

Creates an SMT circuit for field operations.

Parameters
solverPointer to SMT solver to use
Returns
UltraCircuit configured for field operations

Definition at line 65 of file acir_loader.cpp.

◆ get_integer_smt_circuit()

smt_circuit::UltraCircuit AcirToSmtLoader::get_integer_smt_circuit ( smt_solver::Solver *  solver)

Creates an SMT circuit for integer operations.

Parameters
solverPointer to SMT solver to use
Returns
UltraCircuit configured for integer operations

Definition at line 71 of file acir_loader.cpp.

◆ get_smt_solver()

smt_solver::Solver AcirToSmtLoader::get_smt_solver ( )

Gets an SMT solver instance.

Returns
Solver instance for SMT solving

Creates a solver configured with:

  • Circuit modulus from schema
  • Default solver configuration
  • Minimum bit width of 16
  • Maximum bit width of 240

Definition at line 46 of file acir_loader.cpp.

◆ operator=() [1/2]

AcirToSmtLoader && AcirToSmtLoader::operator= ( AcirToSmtLoader &&  other)
delete

◆ operator=() [2/2]

AcirToSmtLoader & AcirToSmtLoader::operator= ( const AcirToSmtLoader  other)
delete

Member Data Documentation

◆ acir_program_buf

std::vector<uint8_t> AcirToSmtLoader::acir_program_buf
private

Buffer containing the raw ACIR program data read from file.

Definition at line 99 of file acir_loader.hpp.

◆ circuit_buf

msgpack::sbuffer AcirToSmtLoader::circuit_buf
private

Buffer for circuit serialization using MessagePack.

Definition at line 101 of file acir_loader.hpp.

◆ constraint_system

acir_format::AcirFormat AcirToSmtLoader::constraint_system
private

The parsed constraint system from the ACIR program.

Definition at line 100 of file acir_loader.hpp.

◆ instruction_name

std::string AcirToSmtLoader::instruction_name
private

Name of the instruction/filename being processed.

Definition at line 98 of file acir_loader.hpp.

The documentation for this class was generated from the following files: