Loading...

Searching...

No Matches

Enumerations | Functions

state_encoding.h File Reference

State Encoding. More...

#include <util/irep.h>
#include "solver.h"
#include <iosfwd>
#include <optional>

+ Include dependency graph for state_encoding.h:

[フレーム]

+ This graph shows which files directly or indirectly include this file:

[フレーム]

Go to the source code of this file.

Enumerations

enum class state_encoding_formatt { ASCII , SMT2 }

Functions

void state_encoding (const goto_modelt &, state_encoding_formatt, bool program_is_inlined, std::optional< irep_idt > contract, std::ostream &out)

solver_resultt state_encoding_solver (const goto_modelt &, bool program_is_inlined, std::optional< irep_idt > contract, const solver_optionst &)

void variable_encoding (const goto_modelt &, state_encoding_formatt, std::ostream &out)

Detailed Description

State Encoding.

Definition in file state_encoding.h.

Enumeration Type Documentation

◆ state_encoding_formatt

enum class state_encoding_formatt

strong

Enumerator
ASCII
SMT2

Definition at line 24 of file state_encoding.h.

Function Documentation

◆ state_encoding()

void state_encoding ( const goto_modelt & goto_model,

state_encoding_formatt state_encoding_format,

bool program_is_inlined,

std::optional< irep_idt > contract,

std::ostream & out

)

Definition at line 1178 of file state_encoding.cpp.

◆ state_encoding_solver()

solver_resultt state_encoding_solver ( const goto_modelt & goto_model,

bool program_is_inlined,

std::optional< irep_idt > contract,

const solver_optionst & solver_options

)

Definition at line 1236 of file state_encoding.cpp.

◆ variable_encoding()

void variable_encoding ( const goto_modelt & goto_model,

state_encoding_formatt state_encoding_format,

std::ostream & out

)

Definition at line 1204 of file state_encoding.cpp.

src
cprover
state_encoding.h
Generated by doxygen 1.9.8