CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
parser.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file parser.h
4
*
5
* Author: Sergey Berezin
6
*
7
* Created: Wed Feb 5 11:46:57 2003
8
*
9
* <hr>
10
*
11
* License to use, copy, modify, sell and/or distribute this software
12
* and its documentation for any purpose is hereby granted without
13
* royalty, subject to the terms and conditions defined in the \ref
14
* LICENSE file provided with this distribution.
15
*
16
* <hr>
17
*
18
* The top-level API to the parser. At this level, it is simply a
19
* stream of commands (Expr's) terminated by an infinite sequence of
20
* Null Expr. It has a support to parse several different input
21
* languages (as many as we care to implement), and may take a file
22
* name, or an istream to read from (default: std::cin, or stdin).
23
* Using iostream means no more worries about whether to close files
24
* or not.
25
*/
26
/*****************************************************************************/
27
28
#ifndef _cvc3__parser_h_
29
#define _cvc3__parser_h_
30
31
#include "
exception.h
"
32
#include "
lang.h
"
33
34
namespace
CVC3 {
35
36
class
ValidityChecker;
37
class
Translator;
38
class
Expr;
39
40
// Internal parser state and other data
41
class
ParserData;
42
43
class
Parser
{
44
private
:
45
ParserData*
d_data
;
46
// Internal methods for constructing and destroying the actual parser
47
void
initParser
();
48
void
deleteParser
();
49
public
:
50
// Constructors
51
Parser
(
ValidityChecker
*
vc
,
Translator
* translator,
InputLanguage
lang,
52
// The 'interactive' flag is ignored when fileName != ""
53
bool
interactive =
true
,
54
const
std::string& fileName =
""
);
55
Parser
(
ValidityChecker
*
vc
,
Translator
* translator,
InputLanguage
lang, std::istream& is,
56
bool
interactive =
false
);
57
// Destructor
58
~Parser
();
59
// Read the next command.
60
Expr
next
();
61
// Check if we are done (end of input has been reached)
62
bool
done
()
const
;
63
// The same check can be done by using the class Parser's value as
64
// a Boolean
65
operator
bool()
const
{
return
done
(); }
66
void
printLocation
(std::ostream & out)
const
;
67
// Reset any local data that depends on validity checker
68
void
reset
();
69
};
// end of class Parser
70
71
// The global pointer to ParserTemp. Each instance of class Parser
72
// sets this pointer before any calls to the lexer. We do it this
73
// way because flex and bison use global vars, and we want each
74
// Parser object to appear independent.
75
class
ParserTemp;
76
extern
ParserTemp*
parserTemp
;
77
78
}
// end of namespace CVC3
79
80
#endif
CVC3::Parser::~Parser
~Parser()
CVC3::Expr
Data structure of expressions in CVC3.
Definition:
expr.h:133
CVC3::Parser::deleteParser
void deleteParser()
CVC3::Parser
Definition:
parser.h:43
CVC3::parserTemp
ParserTemp * parserTemp
CVC3::InputLanguage
InputLanguage
Different input languages.
Definition:
lang.h:30
lang.h
Definition of input and output languages to CVC3.
exception.h
CVC3::Parser::reset
void reset()
CVC3::Parser::next
Expr next()
CVC3::Parser::printLocation
void printLocation(std::ostream &out) const
vc
static ValidityChecker * vc
Definition:
main.cpp:51
CVC3::Translator
Definition:
translator.h:60
CVC3::ValidityChecker
Generic API for a validity checker.
Definition:
vc.h:92
CVC3::Parser::Parser
Parser(ValidityChecker *vc, Translator *translator, InputLanguage lang, bool interactive=true, const std::string &fileName="")
CVC3::Parser::d_data
ParserData * d_data
Definition:
parser.h:45
CVC3::Parser::done
bool done() const
CVC3::Parser::initParser
void initParser()
Generated on Mon Sep 15 2014 15:00:54 for CVC3 by
1.8.7