High-level facade for stabilizing SMT-LIB2 inputs. More...

#include <stabilizer_api.h>

Collaboration diagram for stabilizer::api::SMTStabilizer:

Public Member Functions
	SMTStabilizer (SMTStabilizerOptions options={})

const SMTStabilizerOptions &	options () const noexcept

void	set_options (const SMTStabilizerOptions &options) noexcept

std::string	apply_file (const std::string &file_path) const
	Apply the full pipeline to an SMT-LIB2 file.

std::string	apply_text (const std::string &smt2_text) const
	Apply the full pipeline to an SMT-LIB2 script provided as text.

Static Private Member Functions
static void	configure_parser (stabilizer::parser::Parser &parser, const SMTStabilizerOptions &options)

static std::string	run_pipeline (stabilizer::parser::Parser &parser, const SMTStabilizerOptions &options)

Private Attributes
SMTStabilizerOptions	d_options

Detailed Description

High-level facade for stabilizing SMT-LIB2 inputs.

The facade accepts either a file path or an SMT-LIB2 script string, runs the existing parser/node/kernel pipeline, and returns the normalized SMT2 text.

API-to-kernel boundary:

API methods validate input and instantiate parser state.
run_pipeline creates node::NodeManager, simplifies assertions, and then transfers control to kernel::Kernel::apply.
Kernel remains an internal implementation detail; only API options and stable return types are exposed to integrators.

Instances are cheap to copy and can be configured independently.

Definition at line 81 of file stabilizer_api.h.

Constructor & Destructor Documentation

◆ SMTStabilizer()

stabilizer::api::SMTStabilizer::SMTStabilizer ( SMTStabilizerOptions options = {} )

explicit

Definition at line 32 of file stabilizer_api.cpp.

Member Function Documentation

◆ apply_file()

std::string stabilizer::api::SMTStabilizer::apply_file ( const std::string & file_path ) const

Apply the full pipeline to an SMT-LIB2 file.

Parameters

file_path Path to an SMT-LIB2 input file.

Returns: Stabilized SMT2 text.

Exceptions

std::invalid_argument	if the path is empty.
std::runtime_error	if parsing or normalization fails.

Definition at line 57 of file stabilizer_api.cpp.

References d_options, stabilizer::parser::Parser::parse(), and run_pipeline().

Referenced by stabilizer_apply_file().

◆ apply_text()

std::string stabilizer::api::SMTStabilizer::apply_text ( const std::string & smt2_text ) const

Apply the full pipeline to an SMT-LIB2 script provided as text.

Parameters

smt2_text Full SMT-LIB2 input text.

Returns: Stabilized SMT2 text.

Exceptions

std::invalid_argument	if the text is empty.
std::runtime_error	if parsing or normalization fails.

Definition at line 67 of file stabilizer_api.cpp.

References d_options, stabilizer::parser::Parser::parseStr(), and run_pipeline().

Referenced by stabilizer_apply_text().

◆ configure_parser()

void stabilizer::api::SMTStabilizer::configure_parser	(	stabilizer::parser::Parser &	parser,
		const SMTStabilizerOptions &	options
	)

staticprivate

Configure parser-global options before pipeline execution.

Definition at line 38 of file stabilizer_api.cpp.

References stabilizer::api::SMTStabilizerOptions::get_rewrite(), stabilizer::parser::Parser::getOptions(), and options().

Referenced by run_pipeline().

◆ options()

const SMTStabilizerOptions & stabilizer::api::SMTStabilizer::options ( ) const

noexcept

Return the current API options.

Definition at line 34 of file stabilizer_api.cpp.

References d_options.

Referenced by configure_parser(), run_pipeline(), stabilizer_get_context_propagation(), stabilizer_get_rewrite(), and stabilizer_get_subgraph_pruning().

◆ run_pipeline()

std::string stabilizer::api::SMTStabilizer::run_pipeline	(	stabilizer::parser::Parser &	parser,
		const SMTStabilizerOptions &	options
	)

staticprivate

Run parser -> node manager -> kernel pipeline and serialize final output.

Definition at line 45 of file stabilizer_api.cpp.

References stabilizer::kernel::Kernel::apply(), configure_parser(), stabilizer::api::SMTStabilizerOptions::get_context_propagation(), stabilizer::api::SMTStabilizerOptions::get_subgraph_pruning(), and options().

Referenced by apply_file(), and apply_text().

◆ set_options()

void stabilizer::api::SMTStabilizer::set_options ( const SMTStabilizerOptions & options )

noexcept

Replace the current API options.

Definition at line 36 of file stabilizer_api.cpp.

Member Data Documentation

◆ d_options

SMTStabilizerOptions stabilizer::api::SMTStabilizer::d_options

private

Definition at line 109 of file stabilizer_api.h.

Referenced by apply_file(), apply_text(), and options().

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

src/api/stabilizer_api.h
src/api/stabilizer_api.cpp

Public Member Functions

Static Private Member Functions

Private Attributes