Horn-clause Encoding. More...

#include "horn_encoding.h"
#include <util/c_types.h>
#include <util/exception_utils.h>
#include <util/format_expr.h>
#include <util/mathematical_expr.h>
#include <util/pointer_expr.h>
#include <util/prefix.h>
#include <util/replace_symbol.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <goto-programs/goto_model.h>
#include <solvers/smt2/smt2_conv.h>
#include <algorithm>
#include <ostream>
#include <unordered_set>

Include dependency graph for horn_encoding.cpp:

Go to the source code of this file.

Classes
class	state_typet

class	evaluate_exprt

class	update_state_exprt

class	allocate_exprt

class	encoding_targett

class	container_encoding_targett

class	smt2_encoding_targett

class	ascii_encoding_targett

class	state_encodingt

Functions
static mathematical_function_typet	state_predicate_type ()

static symbol_exprt	state_expr ()

const evaluate_exprt &	to_evaluate_expr (const exprt &expr)
	Cast an exprt to a evaluate_exprt. More...

evaluate_exprt &	to_evaluate_expr (exprt &expr)
	Cast an exprt to a evaluate_exprt. More...

const update_state_exprt &	to_update_state_expr (const exprt &expr)
	Cast an exprt to a update_state_exprt. More...

update_state_exprt &	to_update_state_expr (exprt &expr)
	Cast an exprt to a update_state_exprt. More...

const allocate_exprt &	to_allocate_expr (const exprt &expr)
	Cast an exprt to a allocate_exprt. More...

static void	operator<< (encoding_targett &target, exprt constraint)

static void	operator<< (encoding_targett &target, const container_encoding_targett &src)

static void	find_variables_rec (const exprt &src, std::unordered_set< symbol_exprt, irep_hash > &result)

static exprt	simplifying_not (exprt src)

void	state_encoding (const goto_modelt &goto_model, bool program_is_inlined, encoding_targett &dest)

std::unordered_set< symbol_exprt, irep_hash >	find_variables (const std::vector< exprt > &src)
	Returns the set of program variables (as identified by object_address expressions) in the given expression. More...

static typet	new_state_predicate_type (const binding_exprt::variablest &variables)

exprt	variable_encoding (exprt src, const binding_exprt::variablest &variables)

void	variable_encoding (std::vector< exprt > &constraints)

void	equality_propagation (std::vector< exprt > &constraints)

void	horn_encoding (const goto_modelt &goto_model, std::ostream &out)

Detailed Description

Horn-clause Encoding.

Definition in file horn_encoding.cpp.

Function Documentation

◆ equality_propagation()

void equality_propagation ( std::vector< exprt > & constraints )

Definition at line 1153 of file horn_encoding.cpp.

◆ find_variables()

std::unordered_set<symbol_exprt, irep_hash> find_variables ( const std::vector< exprt > & src )

Returns the set of program variables (as identified by object_address expressions) in the given expression.

Definition at line 1022 of file horn_encoding.cpp.

◆ find_variables_rec()

static void find_variables_rec	(	const exprt &	src,
		std::unordered_set< symbol_exprt, irep_hash > &	result
	)

static

Definition at line 325 of file horn_encoding.cpp.

◆ horn_encoding()

void horn_encoding	(	const goto_modelt &	goto_model,
		std::ostream &	out
	)

Definition at line 1209 of file horn_encoding.cpp.

◆ new_state_predicate_type()

static typet new_state_predicate_type ( const binding_exprt::variablest & variables )

static

Definition at line 1033 of file horn_encoding.cpp.

◆ operator<<() [1/2]

static void operator<<	(	encoding_targett &	target,
		const container_encoding_targett &	src
	)

inlinestatic

Definition at line 264 of file horn_encoding.cpp.

◆ operator<<() [2/2]

static void operator<<	(	encoding_targett &	target,
		exprt	constraint
	)

inlinestatic

Definition at line 259 of file horn_encoding.cpp.

◆ simplifying_not()

static exprt simplifying_not ( exprt src )

static

Definition at line 701 of file horn_encoding.cpp.

◆ state_encoding()

void state_encoding	(	const goto_modelt &	goto_model,
		bool	program_is_inlined,
		encoding_targett &	dest
	)

Definition at line 984 of file horn_encoding.cpp.

◆ state_expr()

static symbol_exprt state_expr ( )

inlinestatic

Definition at line 47 of file horn_encoding.cpp.

◆ state_predicate_type()

static mathematical_function_typet state_predicate_type ( )

inlinestatic

Definition at line 42 of file horn_encoding.cpp.

◆ to_allocate_expr()

const allocate_exprt& to_allocate_expr ( const exprt & expr )

inline

Cast an exprt to a allocate_exprt.

expr must be known to be allocate_exprt.

Parameters

expr	Source expression

Returns: Object of type allocate_exprt

Definition at line 206 of file horn_encoding.cpp.

◆ to_evaluate_expr() [1/2]

const evaluate_exprt& to_evaluate_expr ( const exprt & expr )

inline

Cast an exprt to a evaluate_exprt.

expr must be known to be evaluate_exprt.

Parameters

expr	Source expression

Returns: Object of type evaluate_exprt

Definition at line 88 of file horn_encoding.cpp.

◆ to_evaluate_expr() [2/2]

evaluate_exprt& to_evaluate_expr ( exprt & expr )

inline

Cast an exprt to a evaluate_exprt.

expr must be known to be evaluate_exprt.

Parameters

expr	Source expression

Returns: Object of type evaluate_exprt

Definition at line 97 of file horn_encoding.cpp.

◆ to_update_state_expr() [1/2]

const update_state_exprt& to_update_state_expr ( const exprt & expr )

inline

Cast an exprt to a update_state_exprt.

expr must be known to be update_state_exprt.

Parameters

expr	Source expression

Returns: Object of type update_state_exprt

Definition at line 147 of file horn_encoding.cpp.

◆ to_update_state_expr() [2/2]

update_state_exprt& to_update_state_expr ( exprt & expr )

inline

Cast an exprt to a update_state_exprt.

expr must be known to be update_state_exprt.

Parameters

expr	Source expression

Returns: Object of type update_state_exprt

Definition at line 156 of file horn_encoding.cpp.

◆ variable_encoding() [1/2]

exprt variable_encoding	(	exprt	src,
		const binding_exprt::variablest &	variables
	)

Definition at line 1042 of file horn_encoding.cpp.

◆ variable_encoding() [2/2]

void variable_encoding ( std::vector< exprt > & constraints )

Definition at line 1131 of file horn_encoding.cpp.

Classes

Functions

Detailed Description

Function Documentation

◆ equality_propagation()

◆ find_variables()

◆ find_variables_rec()

◆ horn_encoding()

◆ new_state_predicate_type()

◆ operator<<() [1/2]

◆ operator<<() [2/2]

◆ simplifying_not()

◆ state_encoding()

◆ state_expr()

◆ state_predicate_type()

◆ to_allocate_expr()

◆ to_evaluate_expr() [1/2]

◆ to_evaluate_expr() [2/2]

◆ to_update_state_expr() [1/2]

◆ to_update_state_expr() [2/2]

◆ variable_encoding() [1/2]

◆ variable_encoding() [2/2]