CVC3 2.2
|
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 bool SearchEngine::tryModelGeneration(Theorem& thm) { 00049 00050 if(!lastThm().isNull()) throw EvalException("Method tryModelGenereation() (or command COUNTERMODEL)\n must be called only after failed QUERY"); 00051 00052 // Save the scope level, to recover on errors 00053 push(); 00054 d_core->collectBasicVars(); 00055 bool success = d_core->refineCounterExample(thm); 00056 if (!success) { 00057 pop(); 00058 return false; 00059 } 00060 00061 QueryResult qres = checkValid(d_core->falseExpr(), thm); 00062 if(qres == VALID) { 00063 pop(); 00064 return false; 00065 } 00066 00067 success = d_core->buildModel(thm); 00068 if (!success) { 00069 pop(); 00070 return false; 00071 } 00072 00073 qres = checkValid(d_core->falseExpr(), thm); 00074 if(qres == VALID) { 00075 pop(); 00076 return false; 00077 } 00078 00079 return true; 00080 } 00081 00082 void SearchEngine::getConcreteModel(ExprMap<Expr>& m) 00083 { 00084 TRACE("model" , "Building a concrete model", "", "{"); 00085 if(!lastThm().isNull()) 00086 throw EvalException 00087 ("Method getConcreteModel() (or command COUNTERMODEL)\n" 00088 " must be called only after failed QUERY"); 00089 // Save the scope level, to recover on errors 00090 push(); 00091 d_core->collectBasicVars(); 00092 try { 00093 d_core->refineCounterExample(); 00094 } catch(Exception& e) { 00095 // Clean up and re-throw the exception 00096 pop(); 00097 throw e; 00098 } 00099 Theorem thm; 00100 QueryResult qres = checkValid(d_core->falseExpr(), thm); 00101 if(qres == VALID) { 00102 vector<Expr> assump; 00103 getAssumptions(assump); 00104 d_core->inconsistentThm().getLeafAssumptions(assump); 00105 Expr a = Expr(RAW_LIST, assump, d_core->getEM()); 00106 pop(); 00107 throw Exception 00108 ("Model Creation failed after refining counterexample\n" 00109 "due to the following assumptions:\n " 00110 +a.toString() 00111 +"\n\nYou might be using an incomplete fragment of the theory"); 00112 } 00113 // else if (qres != INVALID) { 00114 // throw EvalException 00115 // ("Unable to build concrete model"); 00116 // } 00117 try { 00118 d_core->buildModel(m); 00119 } catch(Exception& e) { 00120 // Clean up and re-throw the exception 00121 pop(); 00122 throw e; 00123 } 00124 qres = checkValid(d_core->falseExpr(), thm); 00125 if(qres == VALID) { 00126 vector<Expr> assump; 00127 getAssumptions(assump); 00128 Expr a = Expr(RAW_LIST, assump, d_core->getEM()); 00129 pop(); 00130 throw Exception 00131 ("Model Creation failed due to the following assumptions:\n" 00132 +a.toString() 00133 +"\n\nYou might be using an incomplete fragment of the theory"); 00134 } 00135 // else if (qres != INVALID) { 00136 // throw EvalException 00137 // ("Unable to build concrete model"); 00138 // } 00139 TRACE("model" , "Building a concrete model", "", "}"); 00140 }