search.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file search.cpp
 * 
 * Author: Clark Barrett, Vijay Ganesh (CNF Converter)
 * 
 * Created: Fri Jan 17 14:19:54 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 "search.h"
#include "search_rules.h"
#include "theory_core.h"
#include "eval_exception.h"
#include "theorem_manager.h"


using namespace CVCL;
using namespace std;


//! Constructor
SearchEngine::SearchEngine(TheoryCore* core)
  : d_core(core),
    d_commonRules(core->getTM()->getRules())
{
  d_rules = createRules();
}


//! Destructor
SearchEngine::~SearchEngine()
{
  delete d_rules;
}


void SearchEngine::getConcreteModel(ExprMap<Expr> & m)
{
  TRACE("model" ,  "Building a concrete model", "", "{");
  if(!lastThm().isNull())
    throw EvalException
      ("Method getConcreteModel() (or command COUNTERMODEL)\n"
       " must be called only after failed QUERY");
  // Save the scope level, to recover on errors
  int scope = d_core->getCM()->scopeLevel();
  d_core->getCM()->push();
  d_core->collectBasicVars();
  bool v;
  try {
    d_core->refineCounterExample();
  } catch(Exception& e) {
    // Clean up and re-throw the exception
    d_core->getCM()->popto(scope);
    throw e;
  }
  v =!checkValid(d_core->falseExpr()).isNull();
  if(v) {
    vector<Expr> assump;
    getAssumptions(assump);
    d_core->inconsistentThm().getLeafAssumptions(assump);
    Expr a = Expr(RAW_LIST, assump, d_core->getEM());
    d_core->getCM()->popto(scope);
    throw EvalException
      ("Model Creation failed after refining counterexample\n"
       "due to the following assumptions:\n "
       +a.toString()       
       +"\n\nYou might be using an incomplete fragment of the theory");
  }
  try {
    d_core->buildModel(m);
  } catch(Exception& e) {
    // Clean up and re-throw the exception
    d_core->getCM()->popto(scope);
    throw e;
  }
  v =!checkValid(d_core->falseExpr()).isNull();
  if(v) {
    vector<Expr> assump;
    getAssumptions(assump);
    Expr a = Expr(RAW_LIST, assump, d_core->getEM());
    d_core->getCM()->popto(scope);
    throw EvalException
      ("Model Creation failed due to the following assumptions:\n"
       +a.toString()
       +"\n\nYou might be using an incomplete fragment of the theory");
  }
  TRACE("model" ,  "Building a concrete model", "", "}"); 
}

---