CVC3  2.4.1
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 /*****************************************************************************/
42 
43 protected:
44  virtual bool isBetter(const Expr& e1, const Expr& e2);
45 
46 public:
47  //! Constructor
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