solver.cpp File Reference

Solver. More...

#include "solver.h"
#include <util/format_expr.h>
#include "address_taken.h"
#include "generalization.h"
#include "inductiveness.h"
#include "report_properties.h"
#include "report_traces.h"
#include "solver_progress.h"
#include "solver_types.h"
#include <iostream>

Include dependency graph for solver.cpp:

Go to the source code of this file.

Classes
class	take_time_resourcet

Functions
void	solver (std::vector< framet > &frames, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const solver_optionst &solver_options, const namespacet &ns, std::vector< propertyt > &properties, std::size_t property_index)
solver_resultt	solver (const std::vector< exprt > &constraints, const solver_optionst &solver_options, const namespacet &ns)

Detailed Description

Solver.

Definition in file solver.cpp.

Function Documentation

solver() [1/2]

solver_resultt solver	(	const std::vector< exprt > &	constraints,
		const solver_optionst &	solver_options,
		const namespacet &	ns
	)

Definition at line 107 of file solver.cpp.

solver() [2/2]

void solver	(	std::vector< framet > &	frames,
		const std::unordered_set< symbol_exprt, irep_hash > &	address_taken,
		const solver_optionst &	solver_options,
		const namespacet &	ns,
		std::vector< propertyt > &	properties,
		std::size_t	property_index
	)

Definition at line 44 of file solver.cpp.