CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
search
decision_engine_caching.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file decision_engine_caching.h
4
*
5
* <hr>
6
*
7
* License to use, copy, modify, sell and/or distribute this software
8
* and its documentation for any purpose is hereby granted without
9
* royalty, subject to the terms and conditions defined in the \ref
10
* LICENSE file provided with this distribution.
11
*
12
* <hr>
13
*
14
*/
15
/*****************************************************************************/
16
17
#ifndef _cvc3__search__decision_engine_caching_h_
18
#define _cvc3__search__decision_engine_caching_h_
19
20
#include "
decision_engine.h
"
21
22
namespace
CVC3 {
23
24
class
DecisionEngineCaching
:
public
DecisionEngine
{
25
26
class
CacheEntry
27
{
28
public
:
29
Expr
d_expr
;
30
int
d_rank
;
31
int
d_trust
;
32
33
CacheEntry
() :
d_rank
(0),
d_trust
(0) {}
34
};
35
36
int
d_startLevel
;
37
int
d_bottomLevel
;
38
int
d_topLevel
;
39
bool
d_topLevelLock
;
40
int
d_height
;
41
42
std::vector<CacheEntry>
d_cache
;
43
ExprMap<int>
d_index
;
44
45
protected
:
46
virtual
bool
isBetter
(
const
Expr
& e1,
const
Expr
& e2);
47
48
public
:
49
DecisionEngineCaching
(
TheoryCore
* core,
SearchImplBase
* se);
50
virtual
~DecisionEngineCaching
() { }
51
52
virtual
Expr
findSplitter
(
const
Expr
& e);
53
virtual
void
goalSatisfied
();
54
};
55
56
}
57
58
#endif
Generated on Mon Aug 6 2012 09:40:03 for CVC3 by
1.8.1.1