decision_engine_mbtf.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file decision_engine_mbtf.h
00004  * 
00005  * <hr>
00006  *
00007  * License to use, copy, modify, sell and/or distribute this software
00008  * and its documentation for any purpose is hereby granted without
00009  * royalty, subject to the terms and conditions defined in the \ref
00010  * LICENSE file provided with this distribution.
00011  * 
00012  * <hr>
00013  * 
00014  */
00015 /*****************************************************************************/
00016 
00017 #ifndef _cvc3__search__decision_engine_mbtf_h_
00018 #define _cvc3__search__decision_engine_mbtf_h_
00019 
00020 #include "decision_engine.h"
00021 
00022 namespace CVC3 {
00023 
00024 class DecisionEngineMBTF : public DecisionEngine {
00025 
00026   class CacheEntry
00027   {
00028   public:
00029     Expr d_expr;
00030     int d_rank;
00031     int d_trust;
00032 
00033     CacheEntry() : d_rank(0), d_trust(0) {}
00034   };
00035 
00036   int d_startLevel;
00037   int d_bottomLevel;
00038   int d_topLevel;
00039   bool d_topLevelLock;
00040   int d_height;
00041 
00042   std::vector<CacheEntry> d_cache;
00043   ExprMap<int> d_index;
00044 
00045 protected:
00046   virtual bool isBetter(const Expr& e1, const Expr& e2);
00047 
00048 public:
00049   DecisionEngineMBTF(TheoryCore* core, SearchImplBase* se);
00050   virtual ~DecisionEngineMBTF() { }
00051 
00052   virtual Expr findSplitter(const Expr& e);
00053   virtual void goalSatisfied();
00054 };
00055 
00056 }
00057 
00058 #endif

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