cprover
smt2_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_SMT2_SMT2_DEC_H
11
#define CPROVER_SOLVERS_SMT2_SMT2_DEC_H
12
13
#include <fstream>
14
15
#include "
smt2_conv.h
"
16
17
class
smt2_stringstreamt
18
{
19
protected
:
20
std::stringstream
stringstream
;
21
};
22
25
class
smt2_dect
:
protected
smt2_stringstreamt
,
public
smt2_convt
26
{
27
public
:
28
smt2_dect
(
29
const
namespacet
&_ns,
30
const
std::string &_benchmark,
31
const
std::string &_notes,
32
const
std::string &_logic,
33
solvert
_solver):
34
smt2_convt
(_ns, _benchmark, _notes, _logic, _solver,
stringstream
)
35
{
36
}
37
38
virtual
resultt
dec_solve
();
39
virtual
std::string
decision_procedure_text
()
const
;
40
41
// yes, we are incremental!
42
virtual
bool
has_set_assumptions
()
const
{
return
true
; }
43
44
protected
:
45
resultt
read_result
(std::istream &in);
46
};
47
48
#endif // CPROVER_SOLVERS_SMT2_SMT2_DEC_H
smt2_conv.h
smt2_dect::decision_procedure_text
virtual std::string decision_procedure_text() const
Definition:
smt2_dec.cpp:21
smt2_dect::has_set_assumptions
virtual bool has_set_assumptions() const
Definition:
smt2_dec.h:42
smt2_stringstreamt::stringstream
std::stringstream stringstream
Definition:
smt2_dec.h:20
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:93
smt2_dect::smt2_dect
smt2_dect(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver)
Definition:
smt2_dec.h:28
decision_proceduret::resultt
resultt
Definition:
decision_procedure.h:47
smt2_convt
Definition:
smt2_conv.h:32
smt2_dect::read_result
resultt read_result(std::istream &in)
Definition:
smt2_dec.cpp:131
smt2_dect
Decision procedure interface for various SMT 2.x solvers.
Definition:
smt2_dec.h:25
smt2_dect::dec_solve
virtual resultt dec_solve()
Definition:
smt2_dec.cpp:37
smt2_convt::solvert
solvert
Definition:
smt2_conv.h:35
smt2_stringstreamt
Definition:
smt2_dec.h:17
solvers
smt2
smt2_dec.h
Generated by
1.8.17