CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
search
decision_engine.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file decision_engine.h
4
*
5
* Author: Clark Barrett
6
*
7
* Created: Fri Jul 11 13:04:25 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
*/
19
/*****************************************************************************/
20
21
#ifndef _cvc3__search__decision_engine_h_
22
#define _cvc3__search__decision_engine_h_
23
24
#include "
statistics.h
"
25
#include "
search_fast.h
"
26
27
namespace
CVC3 {
28
29
class
DecisionEngine
{
30
31
/***************************************************************************/
32
/*!
33
*\defgroup DE Decision Engine
34
*\brief Decision Engine, used by Search Engine
35
*\ingroup SE
36
*@{
37
*/
38
/***************************************************************************/
39
40
protected
:
41
TheoryCore
*
d_core
;
//!< Pointer to core theory
42
SearchImplBase
*
d_se
;
//!< Pointer to search engine
43
44
//! List of currently active splitters
45
CDList<Expr>
d_splitters
;
46
47
//! Total number of splitters
48
StatCounter
d_splitterCount
;
49
50
ExprMap<Expr>
d_bestByExpr
;
51
52
//! Visited cache for findSplitterRec traversal.
53
/*! Must be emptied in every findSplitter() call. */
54
ExprMap<Expr>
d_visited
;
55
56
Expr
findSplitterRec
(
const
Expr
& e);
57
virtual
bool
isBetter
(
const
Expr
& e1,
const
Expr
& e2) = 0;
58
59
public
:
60
DecisionEngine
(
TheoryCore
* core,
SearchImplBase
* se);
61
virtual
~DecisionEngine
() { }
62
63
/*! @brief Finds a splitter inside a non const expression.
64
The expression passed in must not be a boolean constant,
65
otherwise a DebugAssert will occur. \return Null Expr if passed
66
in a Null Expr. */
67
virtual
Expr
findSplitter
(
const
Expr
& e) = 0;
68
69
//! Push context and record the splitter
70
void
pushDecision
(
Expr
splitter,
bool
whichCase=
true
);
71
//! Pop last decision (and context)
72
void
popDecision
();
73
//! Pop to given scope
74
void
popTo
(
int
dl);
75
76
//! Return the last known splitter.
77
Expr
lastSplitter
();
78
79
//! Search should call this when it derives 'false'
80
virtual
void
goalSatisfied
() = 0;
81
82
/*@}*/
// End of DE group
83
84
};
85
86
}
87
88
#endif
Generated on Thu Jul 19 2012 08:17:20 for CVC3 by
1.8.1.1