horn_encoding.cpp File Reference

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.
evaluate_exprt &	to_evaluate_expr (exprt &expr)
	Cast an exprt to a evaluate_exprt.
const update_state_exprt &	to_update_state_expr (const exprt &expr)
	Cast an exprt to a update_state_exprt.
update_state_exprt &	to_update_state_expr (exprt &expr)
	Cast an exprt to a update_state_exprt.
const allocate_exprt &	to_allocate_expr (const exprt &expr)
	Cast an exprt to a allocate_exprt.
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.
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.