00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
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
00034 SearchEngine::SearchEngine(TheoryCore* core)
00035 : d_core(core),
00036 d_commonRules(core->getTM()->getRules())
00037 {
00038 d_rules = createRules();
00039 }
00040
00041
00042
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
00057 push();
00058 d_core->collectBasicVars();
00059 try {
00060 d_core->refineCounterExample();
00061 } catch(Exception& e) {
00062
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
00081
00082
00083
00084 try {
00085 d_core->buildModel(m);
00086 } catch(Exception& e) {
00087
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
00103
00104
00105
00106 TRACE("model" , "Building a concrete model", "", "}");
00107 }