state_encoding.cpp File Reference

#include "state_encoding.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/mathematical_expr.h>
#include <util/pointer_expr.h>
#include <util/prefix.h>
#include <util/simplify_expr.h>
#include <util/std_code.h>
#include <goto-programs/goto_model.h>
#include "equality_propagation.h"
#include "instrument_contracts.h"
#include "sentinel_dll.h"
#include "solver.h"
#include "state.h"
#include "state_encoding_targets.h"
#include "variable_encoding.h"
#include <algorithm>
#include <iostream>

Include dependency graph for state_encoding.cpp:

Go to the source code of this file.

Classes
class	state_encodingt

Functions
static exprt	simplifying_not (exprt src)
void	state_encoding (const goto_modelt &goto_model, bool program_is_inlined, std::optional< irep_idt > contract, encoding_targett &dest)
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)
void	variable_encoding (const goto_modelt &goto_model, state_encoding_formatt state_encoding_format, std::ostream &out)
solver_resultt	state_encoding_solver (const goto_modelt &goto_model, bool program_is_inlined, std::optional< irep_idt > contract, const solver_optionst &solver_options)

Variables
std::set< irep_idt >	no_body_warnings

Function Documentation

simplifying_not()

static exprt simplifying_not ( exprt  src )

static

Definition at line 630 of file state_encoding.cpp.

state_encoding() [1/2]

void state_encoding	(	const goto_modelt &	goto_model,
		bool	program_is_inlined,
		std::optional< irep_idt >	contract,
		encoding_targett &	dest
	)

Definition at line 1116 of file state_encoding.cpp.

state_encoding() [2/2]

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.

Variable Documentation

no_body_warnings

std::set<irep_idt> no_body_warnings

Definition at line 645 of file state_encoding.cpp.