CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
vc_cmd.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file vc_cmd.h
4
*
5
* Author: Clark Barrett
6
*
7
* Created: Fri Dec 13 22:35:15 2002
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
*/
19
/*****************************************************************************/
20
21
#ifndef _cvc3__vc_cvc__vc_cmd_h_
22
#define _cvc3__vc_cvc__vc_cmd_h_
23
24
#include <string>
25
#include "
compat_hash_map.h
"
26
#include "
exception.h
"
27
#include "
queryresult.h
"
28
29
namespace
CVC3 {
30
31
class
ValidityChecker;
32
class
Parser;
33
class
Context;
34
class
Expr;
35
36
template
<
class
Data>
37
class
ExprMap;
38
39
class
VCCmd
{
40
ValidityChecker
*
d_vc
;
41
Parser
*
d_parser
;
42
// TODO: move state variables into validity checker.
43
typedef
std::hash_map<const char*, Context*>
CtxtMap
;
44
std::string
d_name_of_cur_ctxt
;
45
CtxtMap
d_map
;
46
bool
d_calledFromParser
;
47
48
//! Print the symbols in e, cache results
49
void
printSymbols
(
Expr
e,
ExprMap<bool>
& cache);
50
//! Take a parsed Expr and evaluate it
51
bool
evaluateCommand
(
const
Expr
& e);
52
// Fetch the next command and evaluate it. Return true if
53
// evaluation was successful, false otherwise. In especially bad
54
// cases an exception may be thrown.
55
bool
evaluateNext
();
56
void
findAxioms
(
const
Expr
& e,
ExprMap<bool>
& skolemAxioms,
57
ExprMap<bool>
& visited);
58
Expr
skolemizeAx
(
const
Expr
& e);
59
void
reportResult
(
QueryResult
qres,
bool
checkingValidity =
true
);
60
void
printModel
();
61
void
printCounterExample
();
62
63
public
:
64
VCCmd
(
ValidityChecker
*
vc
,
Parser
* parser,
bool
calledFromParser=
false
);
65
~VCCmd
();
66
67
// Main loop function
68
void
processCommands
();
69
};
70
71
}
72
73
#endif
Generated on Fri Aug 9 2013 10:34:46 for CVC3 by
1.8.4