cprover
cvc_dec.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module:
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
9
10
#ifndef CPROVER_SOLVERS_CVC_CVC_DEC_H
11
#define CPROVER_SOLVERS_CVC_CVC_DEC_H
12
13
#include <fstream>
14
15
#include "
cvc_conv.h
"
16
17
class
cvc_temp_filet
18
{
19
public
:
20
cvc_temp_filet
();
21
~cvc_temp_filet
();
22
23
protected
:
24
std::ofstream
temp_out
;
25
std::string
temp_out_filename
,
temp_result_filename
;
26
};
27
28
class
cvc_dect
:
protected
cvc_temp_filet
,
public
cvc_convt
29
{
30
public
:
31
explicit
cvc_dect
(
const
namespacet
&_ns):
cvc_convt
(_ns,
temp_out
)
32
{
33
}
34
35
virtual
resultt
dec_solve();
36
37
protected
:
38
resultt
read_cvcl_result();
39
void
read_assert(std::istream &in, std::string &line);
40
};
41
42
#endif // CPROVER_SOLVERS_CVC_CVC_DEC_H
cvc_conv.h
cvc_temp_filet::temp_result_filename
std::string temp_result_filename
Definition:
cvc_dec.h:25
cvc_temp_filet::temp_out
std::ofstream temp_out
Definition:
cvc_dec.h:24
decision_proceduret::resultt
resultt
Definition:
decision_procedure.h:45
cvc_temp_filet
Definition:
cvc_dec.h:17
cvc_convt
Definition:
cvc_conv.h:17
namespacet
TO_BE_DOCUMENTED.
Definition:
namespace.h:62
cvc_dect::cvc_dect
cvc_dect(const namespacet &_ns)
Definition:
cvc_dec.h:31
cvc_temp_filet::cvc_temp_filet
cvc_temp_filet()
Definition:
cvc_dec.cpp:32
cvc_dect
Definition:
cvc_dec.h:28
cvc_temp_filet::temp_out_filename
std::string temp_out_filename
Definition:
cvc_dec.h:25
cvc_temp_filet::~cvc_temp_filet
~cvc_temp_filet()
Definition:
cvc_dec.cpp:41
solvers
cvc
cvc_dec.h
Generated by
1.8.12