solver_types.h File Reference

Solver. More...

#include <util/mathematical_expr.h>
#include <util/std_expr.h>
#include <chrono>
#include <unordered_map>
#include <unordered_set>

Include dependency graph for solver_types.h:

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

Go to the source code of this file.

Classes
class	frame_reft
struct	framet
	Stack frames – these are used for function calls and for exceptions. More...
struct	framet::implicationt
class	propertyt
struct	propertyt::trace_updatet
struct	propertyt::trace_statet
struct	workt

Typedefs
using	frame_mapt = std::unordered_map< symbol_exprt, frame_reft, irep_hash >

Functions
frame_mapt	build_frame_map (const std::vector< framet > &frames)
frame_reft	find_frame (const frame_mapt &, const symbol_exprt &frame_symbol)
void	find_implications (const std::vector< exprt > &constraints, std::vector< framet > &)
std::vector< framet >	setup_frames (const std::vector< exprt > &constraints)
std::vector< propertyt >	find_properties (const std::vector< exprt > &constraints, const std::vector< framet > &)

Detailed Description

Solver.

Definition in file solver_types.h.

Typedef Documentation

frame_mapt

using frame_mapt = std::unordered_map<symbol_exprt, frame_reft, irep_hash>

Definition at line 38 of file solver_types.h.

Function Documentation

build_frame_map()

frame_mapt build_frame_map

(

const std::vector< framet > &

frames

)

Definition at line 63 of file solver_types.cpp.

find_frame()

frame_reft find_frame	(	const frame_mapt &	frame_map,
		const symbol_exprt &	frame_symbol
	)

Definition at line 124 of file solver_types.cpp.

find_implications()

void find_implications	(	const std::vector< exprt > &	constraints,
		std::vector< framet > &	frames
	)

Definition at line 91 of file solver_types.cpp.

find_properties()

std::vector<propertyt> find_properties	(	const std::vector< exprt > &	constraints,
		const std::vector< framet > &	frames
	)

Definition at line 134 of file solver_types.cpp.

setup_frames()

std::vector<framet> setup_frames

(

const std::vector< exprt > &

constraints

)

Definition at line 73 of file solver_types.cpp.