CVC3
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
search
decision_engine_dfs.cpp
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file decision_engine_dfs.cpp
4
* \brief Decision Engine
5
*
6
* Author: Clark Barrett
7
*
8
* Created: Sun Jul 13 22:44:55 2003
9
*
10
* <hr>
11
*
12
* License to use, copy, modify, sell and/or distribute this software
13
* and its documentation for any purpose is hereby granted without
14
* royalty, subject to the terms and conditions defined in the \ref
15
* LICENSE file provided with this distribution.
16
*
17
* <hr>
18
*
19
*/
20
/*****************************************************************************/
21
22
23
#include "
decision_engine_dfs.h
"
24
#include "
theory_core.h
"
25
#include "
search.h
"
26
27
28
using namespace
std;
29
using namespace
CVC3;
30
31
32
bool
DecisionEngineDFS::isBetter(
const
Expr
& e1,
const
Expr
& e2)
33
{
34
return
false
;
35
}
36
37
38
/*****************************************************************************/
39
/*!
40
* Function: DecisionEngineDFS::DecisionEngineDFS
41
*
42
* Author: Clark Barrett
43
*
44
* Created: Sun Jul 13 22:52:51 2003
45
*
46
* Constructor
47
*/
48
/*****************************************************************************/
49
DecisionEngineDFS::DecisionEngineDFS(
TheoryCore
* core,
SearchImplBase
* se)
50
:
DecisionEngine
(core, se)
51
{
52
}
53
54
55
/*****************************************************************************/
56
/*!
57
* Function: DecisionEngineDFS::findSplitter
58
*
59
* Author: Clark Barrett
60
*
61
* Created: Sun Jul 13 22:53:18 2003
62
*
63
* Main function to choose the next splitter.
64
* \return NULL if all known splitters are assigned.
65
*/
66
/*****************************************************************************/
67
Expr
DecisionEngineDFS::findSplitter
(
const
Expr
& e) {
68
TRACE
(
"splitters verbose"
,
"findSplitter("
, e,
") {"
);
69
Expr
splitter;
// Null by default
70
d_visited
.
clear
();
71
72
if
(!e.
isNull
()) {
73
splitter =
findSplitterRec
(e);
74
// It's OK not to find a splitter, since e may contain only "bad"
75
// splitters, according to d_se->isGoodSplitter(e)
76
77
// DebugAssert(!splitter.isNull(),
78
// "findSplitter: can't find splitter in non-literal: "
79
// + e.toString());
80
IF_DEBUG
(
if
(!splitter.
isNull
())
81
debugger.counter(
"splitters from decision engine"
)++;)
82
}
83
TRACE
(
"splitters verbose"
,
"findSplitter => "
, splitter,
" }"
);
84
return
splitter;
85
}
86
87
88
void
DecisionEngineDFS::goalSatisfied
()
89
{
90
}
Generated on Thu May 16 2013 13:25:13 for CVC3 by
1.8.2