CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
search
decision_engine_dfs.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file decision_engine_dfs.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_dfs_h_
22
#define _cvc3__search__decision_engine_dfs_h_
23
24
#include "
decision_engine.h
"
25
26
namespace
CVC3 {
27
28
/*****************************************************************************/
29
/*!
30
*\anchor de_dfs
31
*\class DecisionEngineDFS
32
*\brief Decision Engine for use with the Search Engine
33
*\ingroup DE
34
*
35
* Author: Clark Barrett
36
*
37
* Created: Fri Jul 11 16:34:22 2003
38
*
39
*/
40
/*****************************************************************************/
41
class
DecisionEngineDFS
:
public
DecisionEngine
{
42
43
protected
:
44
virtual
bool
isBetter
(
const
Expr
& e1,
const
Expr
& e2);
45
46
public
:
47
//! Constructor
48
DecisionEngineDFS
(
TheoryCore
* core,
SearchImplBase
* se);
49
virtual
~DecisionEngineDFS
() { }
50
51
/*! @brief Find the next splitter. \return Null Expr if no
52
splitter is found. */
53
virtual
Expr
findSplitter
(
const
Expr
& e);
54
55
//! Search should call this when it derives 'false'
56
virtual
void
goalSatisfied
();
57
58
};
59
60
}
61
62
#endif
Generated on Fri Aug 9 2013 10:34:40 for CVC3 by
1.8.4