cprover
Loading...
Searching...
No Matches
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< frametsetup_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< propertytfind_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.