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
CVC3::VCCmd::printModel
void printModel()
Definition:
vc_cmd.cpp:157
CVC3::VCCmd::printCounterExample
void printCounterExample()
Definition:
vc_cmd.cpp:228
CVC3::VCCmd::evaluateCommand
bool evaluateCommand(const Expr &e)
Take a parsed Expr and evaluate it.
Definition:
vc_cmd.cpp:267
CVC3::Expr
Data structure of expressions in CVC3.
Definition:
expr.h:133
CVC3::QueryResult
QueryResult
Definition:
queryresult.h:32
CVC3::Parser
Definition:
parser.h:43
CVC3::VCCmd::d_vc
ValidityChecker * d_vc
Definition:
vc_cmd.h:40
CVC3::VCCmd::d_parser
Parser * d_parser
Definition:
vc_cmd.h:41
CVC3::VCCmd::findAxioms
void findAxioms(const Expr &e, ExprMap< bool > &skolemAxioms, ExprMap< bool > &visited)
Definition:
vc_cmd.cpp:41
queryresult.h
enumerated type for result of queries
exception.h
compat_hash_map.h
CVC3::VCCmd::CtxtMap
std::hash_map< const char *, Context * > CtxtMap
Definition:
vc_cmd.h:43
vc
static ValidityChecker * vc
Definition:
main.cpp:51
CVC3::VCCmd::d_name_of_cur_ctxt
std::string d_name_of_cur_ctxt
Definition:
vc_cmd.h:44
CVC3::VCCmd::~VCCmd
~VCCmd()
Definition:
vc_cmd.cpp:39
CVC3::VCCmd::processCommands
void processCommands()
Definition:
vc_cmd.cpp:944
CVC3::ExprMap< bool >
CVC3::ValidityChecker
Generic API for a validity checker.
Definition:
vc.h:92
Hash::hash_map< const char *, Context * >
CVC3::VCCmd::d_map
CtxtMap d_map
Definition:
vc_cmd.h:45
CVC3::VCCmd
Definition:
vc_cmd.h:39
CVC3::VCCmd::d_calledFromParser
bool d_calledFromParser
Definition:
vc_cmd.h:46
CVC3::VCCmd::reportResult
void reportResult(QueryResult qres, bool checkingValidity=true)
Definition:
vc_cmd.cpp:102
CVC3::VCCmd::printSymbols
void printSymbols(Expr e, ExprMap< bool > &cache)
Print the symbols in e, cache results.
Definition:
vc_cmd.cpp:188
CVC3::VCCmd::evaluateNext
bool evaluateNext()
Definition:
vc_cmd.cpp:73
CVC3
Definition:
expr.cpp:35
CVC3::VCCmd::skolemizeAx
Expr skolemizeAx(const Expr &e)
Definition:
vc_cmd.cpp:61
CVC3::VCCmd::VCCmd
VCCmd(ValidityChecker *vc, Parser *parser, bool calledFromParser=false)
Definition:
vc_cmd.cpp:32
Generated on Tue Jul 14 2015 20:56:44 for CVC3 by
1.8.9.1