inductiveness.cpp File Reference

Inductiveness. More...

#include "inductiveness.h"
#include <util/console.h>
#include <util/cout_message.h>
#include <util/format_expr.h>
#include <solvers/sat/satcheck.h>
#include "axioms.h"
#include "bv_pointers_wide.h"
#include "counterexample_found.h"
#include "propagate.h"
#include "solver.h"
#include <algorithm>
#include <iomanip>
#include <iostream>

Include dependency graph for inductiveness.cpp:

Go to the source code of this file.

Functions
bool	is_subsumed (const std::unordered_set< exprt, irep_hash > &a1, const std::unordered_set< exprt, irep_hash > &a2, const std::unordered_set< exprt, irep_hash > &a3, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, bool verbose, const namespacet &ns)
std::size_t	count_frame (const workt::patht &path, frame_reft f)
inductiveness_resultt	inductiveness_check (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)

Detailed Description

Inductiveness.

Definition in file inductiveness.cpp.

Function Documentation

count_frame()

std::size_t count_frame	(	const workt::patht &	path,
		frame_reft	f
	)

Definition at line 91 of file inductiveness.cpp.

inductiveness_check()

inductiveness_resultt inductiveness_check	(	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 98 of file inductiveness.cpp.

is_subsumed()

bool is_subsumed	(	const std::unordered_set< exprt, irep_hash > &	a1,
		const std::unordered_set< exprt, irep_hash > &	a2,
		const std::unordered_set< exprt, irep_hash > &	a3,
		const exprt &	b,
		const std::unordered_set< symbol_exprt, irep_hash > &	address_taken,
		bool	verbose,
		const namespacet &	ns
	)

Definition at line 30 of file inductiveness.cpp.