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 }