enumerative_loop_contracts_synthesizer.cpp File Reference

Enumerative Loop Contracts Synthesizer. More...

#include "enumerative_loop_contracts_synthesizer.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/find_symbols.h>
#include <util/format_expr.h>
#include <util/pointer_predicates.h>
#include <util/prefix.h>
#include <util/replace_symbol.h>
#include <util/simplify_expr.h>
#include <analyses/local_may_alias.h>
#include <analyses/natural_loops.h>
#include <goto-instrument/contracts/cfg_info.h>
#include <goto-instrument/contracts/utils.h>
#include <goto-instrument/havoc_utils.h>
#include <goto-instrument/loop_utils.h>
#include "cegis_evaluator.h"
#include "expr_enumerator.h"

Include dependency graph for enumerative_loop_contracts_synthesizer.cpp:

Go to the source code of this file.

Functions
void	replace_tmp_post (exprt &dest, const std::unordered_map< exprt, exprt, irep_hash > &tmp_post_map)
std::vector< exprt >	construct_terminals (const std::set< symbol_exprt > &symbols)

Detailed Description

Enumerative Loop Contracts Synthesizer.

Definition in file enumerative_loop_contracts_synthesizer.cpp.

Function Documentation

construct_terminals()

std::vector< exprt > construct_terminals

(

const std::set< symbol_exprt > &

symbols

)

Definition at line 51 of file enumerative_loop_contracts_synthesizer.cpp.

replace_tmp_post()

void replace_tmp_post	(	exprt &	dest,
		const std::unordered_map< exprt, exprt, irep_hash > &	tmp_post_map
	)

Definition at line 34 of file enumerative_loop_contracts_synthesizer.cpp.