CVC3  2.4.1
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 
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
46 
47  //! Total number of splitters
49 
51 
52  //! Visited cache for findSplitterRec traversal.
53  /*! Must be emptied in every findSplitter() call. */
55 
56  Expr findSplitterRec(const Expr& e);
57  virtual bool isBetter(const Expr& e1, const Expr& e2) = 0;
58 
59 public:
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.
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