state_encoding.h File Reference

State Encoding. More...

#include <util/irep.h>
#include "solver.h"
#include <iosfwd>
#include <optional>

Include dependency graph for state_encoding.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Enumerations
enum class	state_encoding_formatt { ASCII , SMT2 }

Functions
void	state_encoding (const goto_modelt &, state_encoding_formatt, bool program_is_inlined, std::optional< irep_idt > contract, std::ostream &out)
solver_resultt	state_encoding_solver (const goto_modelt &, bool program_is_inlined, std::optional< irep_idt > contract, const solver_optionst &)
void	variable_encoding (const goto_modelt &, state_encoding_formatt, std::ostream &out)

Detailed Description

State Encoding.

Definition in file state_encoding.h.

Enumeration Type Documentation

state_encoding_formatt

enum state_encoding_formatt

strong

Enumerator
ASCII
SMT2

Definition at line 24 of file state_encoding.h.

Function Documentation

state_encoding()

void state_encoding	(	const goto_modelt &	goto_model,
		state_encoding_formatt	state_encoding_format,
		bool	program_is_inlined,
		std::optional< irep_idt >	contract,
		std::ostream &	out
	)

Definition at line 1178 of file state_encoding.cpp.

state_encoding_solver()

solver_resultt state_encoding_solver	(	const goto_modelt &	goto_model,
		bool	program_is_inlined,
		std::optional< irep_idt >	contract,
		const solver_optionst &	solver_options
	)

Definition at line 1236 of file state_encoding.cpp.

variable_encoding()

void variable_encoding	(	const goto_modelt &	goto_model,
		state_encoding_formatt	state_encoding_format,
		std::ostream &	out
	)

Definition at line 1204 of file state_encoding.cpp.