decision_engine_dfs.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file decision_engine_dfs.cpp
 * \brief Decision Engine
 * 
 * Author: Clark Barrett
 * 
 * Created: Sun Jul 13 22:44:55 2003
 *
 * <hr>
 * Copyright (C) 2003 by the Board of Trustees of Leland Stanford
 * Junior University and by New York University. 
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.  In particular:
 *
 * - The above copyright notice and this permission notice must appear
 * in all copies of the software and related documentation.
 *
 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
 * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/


#include "decision_engine_dfs.h"
#include "theory_core.h"
#include "search.h"


using namespace std;
using namespace CVCL;


bool DecisionEngineDFS::isBetter(const Expr& e1, const Expr& e2)
{
  return false;
}


/*****************************************************************************/
/*!
 * Function: DecisionEngineDFS::DecisionEngineDFS
 *
 * Author: Clark Barrett
 *
 * Created: Sun Jul 13 22:52:51 2003
 *
 * Constructor
 */
/*****************************************************************************/
DecisionEngineDFS::DecisionEngineDFS(TheoryCore* core, SearchImplBase* se)
  : DecisionEngine(core, se)
{
}


/*****************************************************************************/
/*!
 * Function: DecisionEngineDFS::findSplitter
 *
 * Author: Clark Barrett
 *
 * Created: Sun Jul 13 22:53:18 2003
 *
 * Main function to choose the next splitter.
 * \return NULL if all known splitters are assigned.
 */
/*****************************************************************************/
Expr DecisionEngineDFS::findSplitter(const Expr& e) {
  TRACE("splitters verbose", "findSplitter(", e, ") {");
  Expr splitter; // Null by default
  d_visited.clear();

  if (!e.isNull()) {
    splitter = findSplitterRec(e);
    // It's OK not to find a splitter, since e may contain only "bad"
    // splitters, according to d_se->isGoodSplitter(e)

//     DebugAssert(!splitter.isNull(),
//              "findSplitter: can't find splitter in non-literal: "
//              + e.toString());
    IF_DEBUG(if(!splitter.isNull())
             debugger.counter("splitters from decision engine")++);
  }
  TRACE("splitters verbose", "findSplitter => ", splitter, " }");
  return splitter;
}


void DecisionEngineDFS::goalSatisfied()
{
}

---