decision_engine_dfs.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file decision_engine_dfs.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_dfs_h_
00022 #define _cvc3__search__decision_engine_dfs_h_
00023 
00024 #include "decision_engine.h"
00025 
00026 namespace CVC3 {
00027 
00028 /*****************************************************************************/
00029 /*!
00030  *\anchor de_dfs
00031  *\class DecisionEngineDFS
00032  *\brief Decision Engine for use with the Search Engine
00033  *\ingroup DE
00034  *
00035  * Author: Clark Barrett
00036  *
00037  * Created: Fri Jul 11 16:34:22 2003
00038  *
00039  */
00040 /*****************************************************************************/
00041 class DecisionEngineDFS : public DecisionEngine {
00042 
00043 protected:
00044   virtual bool isBetter(const Expr& e1, const Expr& e2);
00045 
00046 public:
00047   //! Constructor
00048   DecisionEngineDFS(TheoryCore* core, SearchImplBase* se);
00049   virtual ~DecisionEngineDFS() { }
00050 
00051   /*! @brief Find the next splitter.  \return Null Expr if no
00052     splitter is found. */
00053   virtual Expr findSplitter(const Expr& e);
00054 
00055   //! Search should call this when it derives 'false'
00056   virtual void goalSatisfied();
00057 
00058 };
00059 
00060 }
00061 
00062 #endif

Generated on Wed Nov 18 16:13:29 2009 for CVC3 by  doxygen 1.5.2