decision_engine_mbtf.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file decision_engine_mbtf.h
00004  * 
00005  * <hr>
00006  * Copyright (C) 2003 by the Board of Trustees of Leland Stanford
00007  * Junior University and by New York University. 
00008  *
00009  * License to use, copy, modify, sell and/or distribute this software
00010  * and its documentation for any purpose is hereby granted without
00011  * royalty, subject to the terms and conditions defined in the \ref
00012  * LICENSE file provided with this distribution.  In particular:
00013  *
00014  * - The above copyright notice and this permission notice must appear
00015  * in all copies of the software and related documentation.
00016  *
00017  * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
00018  * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
00019  * 
00020  * <hr>
00021  * 
00022  */
00023 /*****************************************************************************/
00024 
00025 #ifndef _cvcl__search__decision_engine_mbtf_h_
00026 #define _cvcl__search__decision_engine_mbtf_h_
00027 
00028 #include "decision_engine.h"
00029 
00030 namespace CVCL {
00031 
00032 class DecisionEngineMBTF : public DecisionEngine {
00033 
00034   class CacheEntry
00035   {
00036   public:
00037     Expr d_expr;
00038     int d_rank;
00039     int d_trust;
00040 
00041     CacheEntry() : d_rank(0), d_trust(0) {}
00042   };
00043 
00044   int d_startLevel;
00045   int d_bottomLevel;
00046   int d_topLevel;
00047   bool d_topLevelLock;
00048   int d_height;
00049 
00050   std::vector<CacheEntry> d_cache;
00051   ExprMap<int> d_index;
00052 
00053 protected:
00054   virtual bool isBetter(const Expr& e1, const Expr& e2);
00055 
00056 public:
00057   DecisionEngineMBTF(TheoryCore* core, SearchImplBase* se);
00058   virtual ~DecisionEngineMBTF() { }
00059 
00060   virtual Expr findSplitter(const Expr& e);
00061   virtual void goalSatisfied();
00062 };
00063 
00064 }
00065 
00066 #endif

Generated on Thu Apr 13 16:57:31 2006 for CVC Lite by  doxygen 1.4.4