CBMC: /home/runner/work/cbmc/cbmc/src/goto-instrument/horn_encoding.cpp File Reference

CBMC

Loading...

Searching...

No Matches

Classes | Functions

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 1152 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 1208 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.