decision_engine_dfs.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file decision_engine_dfs.cpp
00004  * \brief Decision Engine
00005  * 
00006  * Author: Clark Barrett
00007  * 
00008  * Created: Sun Jul 13 22:44:55 2003
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  * 
00019  */
00020 /*****************************************************************************/
00021 
00022 
00023 #include "decision_engine_dfs.h"
00024 #include "theory_core.h"
00025 #include "search.h"
00026 
00027 
00028 using namespace std;
00029 using namespace CVC3;
00030 
00031 
00032 bool DecisionEngineDFS::isBetter(const Expr& e1, const Expr& e2)
00033 {
00034   return false;
00035 }
00036 
00037 
00038 /*****************************************************************************/
00039 /*!
00040  * Function: DecisionEngineDFS::DecisionEngineDFS
00041  *
00042  * Author: Clark Barrett
00043  *
00044  * Created: Sun Jul 13 22:52:51 2003
00045  *
00046  * Constructor
00047  */
00048 /*****************************************************************************/
00049 DecisionEngineDFS::DecisionEngineDFS(TheoryCore* core, SearchImplBase* se)
00050   : DecisionEngine(core, se)
00051 {
00052 }
00053 
00054 
00055 /*****************************************************************************/
00056 /*!
00057  * Function: DecisionEngineDFS::findSplitter
00058  *
00059  * Author: Clark Barrett
00060  *
00061  * Created: Sun Jul 13 22:53:18 2003
00062  *
00063  * Main function to choose the next splitter.
00064  * \return NULL if all known splitters are assigned.
00065  */
00066 /*****************************************************************************/
00067 Expr DecisionEngineDFS::findSplitter(const Expr& e) {
00068   TRACE("splitters verbose", "findSplitter(", e, ") {");
00069   Expr splitter; // Null by default
00070   d_visited.clear();
00071 
00072   if (!e.isNull()) {
00073     splitter = findSplitterRec(e);
00074     // It's OK not to find a splitter, since e may contain only "bad"
00075     // splitters, according to d_se->isGoodSplitter(e)
00076 
00077 //     DebugAssert(!splitter.isNull(),
00078 //    "findSplitter: can't find splitter in non-literal: "
00079 //    + e.toString());
00080     IF_DEBUG(if(!splitter.isNull())
00081        debugger.counter("splitters from decision engine")++);
00082   }
00083   TRACE("splitters verbose", "findSplitter => ", splitter, " }");
00084   return splitter;
00085 }
00086 
00087 
00088 void DecisionEngineDFS::goalSatisfied()
00089 {
00090 }

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