solver_types.cpp File Reference

Solver Types. More...

#include "solver_types.h"
#include <util/format_expr.h>
#include "free_symbols.h"
#include <iostream>
#include <set>

Include dependency graph for solver_types.cpp:

Go to the source code of this file.

Functions
frame_mapt	build_frame_map (const std::vector< framet > &frames)
std::vector< framet >	setup_frames (const std::vector< exprt > &constraints)
void	find_implications (const std::vector< exprt > &constraints, std::vector< framet > &frames)
frame_reft	find_frame (const frame_mapt &frame_map, const symbol_exprt &frame_symbol)
std::vector< propertyt >	find_properties (const std::vector< exprt > &constraints, const std::vector< framet > &frames)
exprt	property_predicate (const implies_exprt &src)
void	dump (const std::vector< framet > &frames, const propertyt &property, bool values, bool implications)

Detailed Description

Solver Types.

Definition in file solver_types.cpp.

Function Documentation

build_frame_map()

frame_mapt build_frame_map

(

const std::vector< framet > &

frames

)

Definition at line 63 of file solver_types.cpp.

dump()

void dump	(	const std::vector< framet > &	frames,
		const propertyt &	property,
		bool	values,
		bool	implications
	)

Definition at line 172 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.

property_predicate()

exprt property_predicate

(

const implies_exprt &

src

)

Definition at line 166 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.