decision_engine_mbtf.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file decision_engine_mbtf.cpp
 * \brief Decision Engine
 * 
 * <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_mbtf.h"
#include "theory_core.h"
#include "search.h"


using namespace std;
using namespace CVCL;

#define CACHE_SIZE 20
#define BASE_TRUST_LEVEL 2
#define TURNOVER_RATE 10

bool DecisionEngineMBTF::isBetter(const Expr& e1, const Expr& e2)
{
  ExprMap<int>::iterator it1 = d_index.find(e1.getSimpFrom());
  ExprMap<int>::iterator it2 = d_index.find(e2.getSimpFrom());

  if (it1 != d_index.end() &&
      (d_cache[it1->second].d_trust >= d_height) &&
      (it2 == d_index.end() ||
       d_cache[it1->second].d_rank < d_cache[it2->second].d_rank))
    return true;
  else
    return false;
}


DecisionEngineMBTF::DecisionEngineMBTF(TheoryCore* core, SearchImplBase* se)
  : DecisionEngine(core, se),
    d_startLevel(core->getCM()->scopeLevel()),
    d_bottomLevel(0),
    d_topLevel(0),
    d_topLevelLock(false),
    d_height(0),
    d_cache(CACHE_SIZE)
{
}


Expr DecisionEngineMBTF::findSplitter(const Expr& e) {
  d_visited.clear();
  Expr splitter; // Null by default
  if (!e.isNull())
  {
    d_height = e.getHeight() - 1;
    // heights seem to be 1 greater than SVC
    // probably because of top-level NOT

    if (!d_topLevelLock)
    {
      d_topLevel = d_core->getCM()->scopeLevel();
      d_topLevelLock = true;
    }

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


void DecisionEngineMBTF::goalSatisfied()
{
  if (d_core->getCM()->scopeLevel() - d_bottomLevel != 0)
  {
    d_bottomLevel = d_core->getCM()->scopeLevel();
    return;
  }

  if (d_splitters.size() == 0)
    return;

  if (!d_topLevelLock)
    d_topLevel = d_bottomLevel - 1;
  d_topLevelLock = false;

  int numSplitters = d_bottomLevel - d_startLevel - 1;
  int numNewSplitters = d_bottomLevel - d_topLevel;

  vector<CacheEntry> newCache(numSplitters);
  ExprMap<int> newIndex;

  int end = d_splitters.size();
  int start = end - numSplitters;
  if (start < 0)
    start = 0;

  const Expr& s = d_splitters[max(0, end - numNewSplitters)];
  Expr topSplitter = s.getSimpFrom();
  if(!topSplitter.isAbsAtomicFormula()) topSplitter = s;

  ExprMap<int>::iterator it = d_index.find(topSplitter);
  int maxTrust = (it != d_index.end()) ? d_cache[it->second].d_trust : numSplitters;

  for (int i = end - 1, j = 0; i >= start; i--, j++)
  {
    const Expr& s = d_splitters[i];
    Expr splitter = s.getSimpFrom();
    if(!splitter.isAbsAtomicFormula()) splitter = s;
    newCache[j].d_expr = splitter;
    newCache[j].d_rank = (numSplitters - j) % numSplitters;
    newIndex[splitter] = j;

    ExprMap<int>::iterator it = d_index.find(splitter);
    if (j == 0) // the effective splitter
      newCache[j].d_trust = maxTrust;
    else if (it != d_index.end())
      newCache[j].d_trust = max(d_cache[it->second].d_trust - 1, 0);
  }

  d_cache = newCache;
  d_index = newIndex;
  d_bestByExpr.clear();
}

---