decision_engine.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file decision_engine.h
00004  * 
00005  * Author: Clark Barrett
00006  * 
00007  * Created: Fri Jul 11 13:04:25 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 
00021 #ifndef _cvc3__search__decision_engine_h_
00022 #define _cvc3__search__decision_engine_h_
00023 
00024 #include "statistics.h"
00025 #include "search_fast.h"
00026 
00027 namespace CVC3 {
00028 
00029 class DecisionEngine {
00030 
00031   /***************************************************************************/
00032   /*!
00033    *\defgroup DE Decision Engine
00034    *\brief Decision Engine, used by Search Engine
00035    *\ingroup SE
00036    *@{
00037    */
00038   /***************************************************************************/
00039 
00040 protected:
00041   TheoryCore* d_core; //!< Pointer to core theory
00042   SearchImplBase* d_se; //!< Pointer to search engine
00043 
00044   //! List of currently active splitters
00045   CDList<Expr> d_splitters;
00046 
00047   //! Total number of splitters
00048   StatCounter d_splitterCount;
00049 
00050   ExprMap<Expr> d_bestByExpr;
00051 
00052   //! Visited cache for findSplitterRec traversal.  
00053   /*! Must be emptied in every findSplitter() call. */
00054   ExprMap<Expr> d_visited;
00055 
00056   Expr findSplitterRec(const Expr& e);
00057   virtual bool isBetter(const Expr& e1, const Expr& e2) = 0;
00058 
00059 public:
00060   DecisionEngine(TheoryCore* core, SearchImplBase* se);
00061   virtual ~DecisionEngine() { }
00062 
00063   /*! @brief Finds a splitter inside a non const expression.
00064       The expression passed in must not be a boolean constant,
00065       otherwise a DebugAssert will occur.  \return Null Expr if passed
00066       in a Null Expr. */
00067   virtual Expr findSplitter(const Expr& e) = 0;
00068 
00069   //! Push context and record the splitter
00070   void pushDecision(Expr splitter, bool whichCase=true);
00071   //! Pop last decision (and context)
00072   void popDecision();
00073   //! Pop to given scope
00074   void popTo(int dl);
00075 
00076   //! Return the last known splitter.
00077   Expr lastSplitter();
00078 
00079   //! Search should call this when it derives 'false'
00080   virtual void goalSatisfied() = 0;
00081 
00082   /*@}*/ // End of DE group
00083 
00084 };
00085 
00086 }
00087 
00088 #endif

Generated on Tue Jul 3 14:33:36 2007 for CVC3 by  doxygen 1.5.1