blob: 8f1032286833eb5b7817e29866c33beaf78485f1 (
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
|
/********************* -*- C++ -*- */
/** parser.h
** This file is part of the CVC4 prototype.
**
** The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
**/
#ifndef __CVC4_PARSER_H
#define __CVC4_PARSER_H
namespace CVC4 {
// In terms of abstraction, this is below (and provides services to)
// the main CVC4 binary and above (and requires the services of)
// ValidityChecker.
class Parser {
private:// maybe protected is better ?
ValidityChecker *d_vc;
public:
Parser(ValidityChecker* vc);
/**
* Process a file. Overridden in subclasses to support SMT-LIB
* format, CVC4 presentation language, etc. In subclasses, this
* function should parse terms, build Command objects, and pass them
* to dispatch().
*/
virtual Expr process(std::istream&) = 0;
/**
* Dispatch a command.
*/
void dispatch(const Command&);
};/* class Parser */
} /* CVC4 namespace */
#endif /* __CVC4_PARSER_H */
|
