blob: 00b90a703de9a9a943c49779733513e4d375606f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
|
/********************* */
/*! \file smt_globals.h
** \verbatim
** Original author: Tim King
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2015 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief SmtGlobals is a light container for psuedo-global datastructures
** that are set by the user.
**
** SmtGlobals is a light container for psuedo-global datastructures
** that are set by the user. These contain paramaters for infrequently
** used modes: Portfolio and Replay. There should be exactly one of these
** per SmtEngine with the same lifetime as the SmtEngine.
** A user directly passes these as pointers and is resonsible for cleaning up
** the memory.
**
** Basically, the problem this class is solving is that previously these were
** using smt_options.h and the Options class as globals for these same
** datastructures.
**
** This class is NOT a good long term solution, but is a reasonable stop gap.
**/
#include "cvc4_public.h"
#ifndef __CVC4__SMT__SMT_GLOBALS_H
#define __CVC4__SMT__SMT_GLOBALS_H
#include <iosfwd>
#include <string>
#include <utility>
#include "expr/expr_stream.h"
#include "options/option_exception.h"
#include "smt_util/lemma_input_channel.h"
#include "smt_util/lemma_output_channel.h"
namespace CVC4 {
/**
* SmtGlobals is a wrapper around 4 pointers:
* - getReplayLog()
* - getReplayStream()
* - getLemmaInputChannel()
* - getLemmaOutputChannel()
*
* The user can directly set these and is responsible for handling the
* memory for these. These datastructures are used for the Replay and Portfolio
* modes.
*/
class CVC4_PUBLIC SmtGlobals {
public:
/** Creates an empty SmtGlobals with all 4 pointers initially NULL. */
SmtGlobals();
~SmtGlobals();
/** This setsReplayLog based on --replay-log */
void parseReplayLog(std::string optarg) throw (OptionException);
void setReplayLog(std::ostream*);
std::ostream* getReplayLog() { return d_replayLog; }
void setReplayStream(ExprStream* stream);
ExprStream* getReplayStream() { return d_replayStream; }
void setLemmaInputChannel(LemmaInputChannel* in);
LemmaInputChannel* getLemmaInputChannel() { return d_lemmaInputChannel; }
void setLemmaOutputChannel(LemmaOutputChannel* out);
LemmaOutputChannel* getLemmaOutputChannel() { return d_lemmaOutputChannel; }
private:
// Disable copy constructor.
SmtGlobals(const SmtGlobals&) CVC4_UNDEFINED;
// Disable assignment operator.
SmtGlobals& operator=(const SmtGlobals&) CVC4_UNDEFINED;
static std::pair<bool, std::ostream*>
checkReplayLogFilename(std::string optarg) throw (OptionException);
/**
* d_gcReplayLog is true iff d_replayLog was allocated by parseReplayLog.
*/
bool d_gcReplayLog;
/** This captures the old options::replayLog .*/
std::ostream* d_replayLog;
/** This captures the old options::replayStream .*/
ExprStream* d_replayStream;
/** This captures the old options::lemmaInputChannel .*/
LemmaInputChannel* d_lemmaInputChannel;
/** This captures the old options::lemmaOutputChannel .*/
LemmaOutputChannel* d_lemmaOutputChannel;
}; /* class SmtGlobals */
} /* namespace CVC4 */
#endif /* __CVC4__SMT__SMT_GLOBALS_H */
|
