CBMC
horn_encoding.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Horn-clause Encoding
4
5
Author: Daniel Kroening
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_GOTO_INSTRUMENT_HORN_ENCODING_H
13
#define CPROVER_GOTO_INSTRUMENT_HORN_ENCODING_H
14
15
#include <iosfwd>
16
17
class
goto_modelt
;
18
19
void
horn_encoding
(
20
const
goto_modelt
&,
21
std::ostream &out);
22
23
#endif
// CPROVER_GOTO_INSTRUMENT_HORN_ENCODING_H
goto_modelt
Definition:
goto_model.h:27
horn_encoding
void horn_encoding(const goto_modelt &, std::ostream &out)
Definition:
horn_encoding.cpp:1209
src
goto-instrument
horn_encoding.h
Generated by
1.9.1