search.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file search.cpp
00004  * 
00005  * Author: Clark Barrett, Vijay Ganesh (CNF Converter)
00006  * 
00007  * Created: Fri Jan 17 14:19:54 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 
00021 
00022 #include "search.h"
00023 #include "search_rules.h"
00024 #include "theory_core.h"
00025 #include "eval_exception.h"
00026 #include "theorem_manager.h"
00027 
00028 
00029 using namespace CVC3;
00030 using namespace std;
00031 
00032 
00033 //! Constructor
00034 SearchEngine::SearchEngine(TheoryCore* core)
00035   : d_core(core),
00036     d_commonRules(core->getTM()->getRules())
00037 {
00038   d_rules = createRules();
00039 }
00040 
00041 
00042 //! Destructor
00043 SearchEngine::~SearchEngine()
00044 {
00045   delete d_rules;
00046 }
00047 
00048 
00049 void SearchEngine::getConcreteModel(ExprMap<Expr>& m)
00050 {
00051   TRACE("model" ,  "Building a concrete model", "", "{");
00052   if(!lastThm().isNull())
00053     throw EvalException
00054       ("Method getConcreteModel() (or command COUNTERMODEL)\n"
00055        " must be called only after failed QUERY");
00056   // Save the scope level, to recover on errors
00057   push();
00058   d_core->collectBasicVars();
00059   try {
00060     d_core->refineCounterExample();
00061   } catch(Exception& e) {
00062     // Clean up and re-throw the exception
00063     pop();
00064     throw e;
00065   }
00066   Theorem thm;
00067   QueryResult qres = checkValid(d_core->falseExpr(), thm);
00068   if(qres == VALID) {
00069     vector<Expr> assump;
00070     getAssumptions(assump);
00071     d_core->inconsistentThm().getLeafAssumptions(assump);
00072     Expr a = Expr(RAW_LIST, assump, d_core->getEM());
00073     pop();
00074     throw EvalException
00075       ("Model Creation failed after refining counterexample\n"
00076        "due to the following assumptions:\n "
00077        +a.toString()       
00078        +"\n\nYou might be using an incomplete fragment of the theory");
00079   }
00080 //   else if (qres != INVALID) {
00081 //     throw EvalException
00082 //       ("Unable to build concrete model");
00083 //   }
00084   try {
00085     d_core->buildModel(m);
00086   } catch(Exception& e) {
00087     // Clean up and re-throw the exception
00088     pop();
00089     throw e;
00090   }
00091   qres = checkValid(d_core->falseExpr(), thm);
00092   if(qres == VALID) {
00093     vector<Expr> assump;
00094     getAssumptions(assump);
00095     Expr a = Expr(RAW_LIST, assump, d_core->getEM());
00096     pop();
00097     throw EvalException
00098       ("Model Creation failed due to the following assumptions:\n"
00099        +a.toString()
00100        +"\n\nYou might be using an incomplete fragment of the theory");
00101   }
00102 //   else if (qres != INVALID) {
00103 //     throw EvalException
00104 //       ("Unable to build concrete model");
00105 //   }
00106   TRACE("model" ,  "Building a concrete model", "", "}"); 
00107 }

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