CVC3  2.4.1
search.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file search.cpp
4  *
5  * Author: Clark Barrett, Vijay Ganesh (CNF Converter)
6  *
7  * Created: Fri Jan 17 14:19:54 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 
22 #include "search.h"
23 #include "search_rules.h"
24 #include "theory_core.h"
25 #include "eval_exception.h"
26 #include "theorem_manager.h"
27 #include "command_line_flags.h"
28 
29 
30 using namespace CVC3;
31 using namespace std;
32 
33 
34 //! Constructor
36  : d_core(core),
37  d_commonRules(core->getTM()->getRules())
38 {
39 
40  const CLFlags& flg = (core->getTM()->getFlags());
41  if (flg["lfsc-mode"].getInt()!= 0){
42  d_rules = createRules(this);
43 
44  }
45  else
46  d_rules = createRules();
47 
48 }
49 
50 
51 //! Destructor
53 {
54  delete d_rules;
55 }
56 
58 
59  if(!lastThm().isNull()) throw EvalException("Method tryModelGenereation() (or command COUNTERMODEL)\n must be called only after failed QUERY");
60 
61  // Save the scope level, to recover on errors
62  push();
64  bool success = d_core->refineCounterExample(thm);
65  if (!success) {
66  pop();
67  return false;
68  }
69 
70  QueryResult qres = checkValid(d_core->falseExpr(), thm);
71  if(qres == VALID) {
72  pop();
73  return false;
74  }
75 
76  success = d_core->buildModel(thm);
77  if (!success) {
78  pop();
79  return false;
80  }
81 
82  qres = checkValid(d_core->falseExpr(), thm);
83  if(qres == VALID) {
84  pop();
85  return false;
86  }
87 
88  return true;
89 }
90 
92 {
93  TRACE("model" , "Building a concrete model", "", "{");
94  if(!lastThm().isNull())
95  throw EvalException
96  ("Method getConcreteModel() (or command COUNTERMODEL)\n"
97  " must be called only after failed QUERY");
98  // Save the scope level, to recover on errors
99  push();
101  try {
103  } catch(Exception& e) {
104  // Clean up and re-throw the exception
105  pop();
106  throw e;
107  }
108  Theorem thm;
109  QueryResult qres = checkValid(d_core->falseExpr(), thm);
110  if(qres == VALID) {
111  vector<Expr> assump;
112  getAssumptions(assump);
114  Expr a = Expr(RAW_LIST, assump, d_core->getEM());
115  pop();
116  throw Exception
117  ("Model Creation failed after refining counterexample\n"
118  "due to the following assumptions:\n "
119  +a.toString()
120  +"\n\nYou might be using an incomplete fragment of the theory");
121  }
122 // else if (qres != INVALID) {
123 // throw EvalException
124 // ("Unable to build concrete model");
125 // }
126  try {
127  d_core->buildModel(m);
128  } catch(Exception& e) {
129  // Clean up and re-throw the exception
130  pop();
131  throw e;
132  }
133  qres = checkValid(d_core->falseExpr(), thm);
134  if(qres == VALID) {
135  vector<Expr> assump;
136  getAssumptions(assump);
137  Expr a = Expr(RAW_LIST, assump, d_core->getEM());
138  pop();
139  throw Exception
140  ("Model Creation failed due to the following assumptions:\n"
141  +a.toString()
142  +"\n\nYou might be using an incomplete fragment of the theory");
143  }
144 // else if (qres != INVALID) {
145 // throw EvalException
146 // ("Unable to build concrete model");
147 // }
148  TRACE("model" , "Building a concrete model", "", "}");
149 }