CVC3  2.4.1
search_simple.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file search_simple.cpp
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Sat Mar 29 21:59:36 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 #include "search_simple.h"
22 #include "theory_core.h"
23 #include "typecheck_exception.h"
24 #include "search_rules.h"
25 
26 #include "decision_engine_dfs.h"
27 //#include "decision_engine_caching.h"
28 //#include "decision_engine_mbtf.h"
29 #include "expr_transform.h"
30 #include "command_line_flags.h"
31 
32 
33 using namespace std;
34 using namespace CVC3;
35 
36 
37 QueryResult SearchSimple::checkValidRec(Theorem& thm)
38 {
39  if (d_core->outOfResources()) return ABORT;
40  TRACE_MSG("search", "checkValidRec() {");
41  if (d_core->inconsistent()) {
42  TRACE("search", "checkValidRec => ", d_core->inconsistentThm(),
43  " (context inconsistent) }");
44  d_decisionEngine->goalSatisfied();
45  thm = d_core->inconsistentThm();
46  return UNSATISFIABLE;
47  }
48 
49  Theorem e = d_goal.get();
50  bool workingOnGoal = true;
51  if (d_goal.get().getExpr().isTrue()) {
52  e = d_nonLiterals.get();
53  workingOnGoal = false;
54  }
55 
56  Theorem simp = simplify(e);
57  Expr rhs = simp.getExpr();
58  if (rhs.hasFind()) {
59  simp = d_commonRules->iffMP(simp, d_core->find(rhs));
60  rhs = simp.getExpr();
61  }
62 
63  if (workingOnGoal) d_goal.set(simp);
64  else d_nonLiterals.set(simp);
65 
66  if (rhs.isFalse()) {
67  TRACE("search", "checkValidRec => ", simp, " (rhs=false) }");
68  d_decisionEngine->goalSatisfied();
69  thm = simp;
70  return UNSATISFIABLE;
71  }
72  else if (rhs.isTrue()) {
73  if (workingOnGoal || !d_core->checkSATCore()) {
74  return checkValidRec(thm);
75  }
76  TRACE("search", "checkValidRec => ", "Null (true)", "}");
77  thm = Theorem();
78  return SATISFIABLE;
79  }
80  Expr splitter = d_decisionEngine->findSplitter(rhs);
81  DebugAssert(!splitter.isNull(), "Expected splitter");
82  d_decisionEngine->pushDecision(splitter);
83  QueryResult qres = checkValidRec(thm);
84  if (qres == UNSATISFIABLE) {
85  d_decisionEngine->popDecision();
86  d_decisionEngine->pushDecision(splitter, false);
87  Theorem thm2;
88  qres = checkValidRec(thm2);
89  if (qres == UNSATISFIABLE) {
90  d_decisionEngine->popDecision();
91  thm = d_rules->caseSplit(splitter, thm, thm2);
92  return qres;
93  }
94  thm = thm2;
95  return qres;
96  }
97  return qres;
98 }
99 
100 
101 SearchSimple::SearchSimple(TheoryCore* core)
102  : SearchImplBase(core),
103  d_name("simple"),
104  d_goal(core->getCM()->getCurrentContext()),
105  d_nonLiterals(core->getCM()->getCurrentContext()),
106  d_simplifiedThm(core->getCM()->getCurrentContext())
107 {
108 // if (core->getFlags()["de"].getString() == "caching")
109 // d_decisionEngine = new DecisionEngineCaching(core, this);
110 // else if (core->getFlags()["de"].getString() == "mbtf")
111 // d_decisionEngine = new DecisionEngineMBTF(core, this);
112 // else
113  d_decisionEngine = new DecisionEngineDFS(core, this);
114 
117 }
118 
119 
121 {
122  delete d_decisionEngine;
123 }
124 
125 
127 {
128  Theorem thm;
129 
130  QueryResult qres = checkValidRec(thm);
131 
132  if (qres == SATISFIABLE && d_core->incomplete()) qres = UNKNOWN;
133 
134  if (qres == SATISFIABLE) {
136  "checkValid: Expected true goal");
137  vector<Expr> a;
140  for (vector<Expr>::iterator i=a.begin(), iend=a.end(); i != iend; ++i) {
141  d_lastCounterExample[*i] = true;
142  }
143  }
144  else if (qres != UNSATISFIABLE) return qres;
145 
146  processResult(thm, e2);
147 
148  if (qres == UNSATISFIABLE) {
149  TRACE_MSG("search terse", "checkValid => true}");
150  TRACE("search", "checkValid => true; theorem = ", d_lastValid, "}");
151 
153  d_lastValid =
154  d_commonRules->iffMP(d_lastValid, d_commonRules->symmetryRule(e_iff_e2));
155  d_core->getCM()->pop();
156  }
157  else {
158  TRACE_MSG("search terse", "checkValid => false}");
159  TRACE_MSG("search", "checkValid => false; }");
160  }
161  return qres;
162 }
163 
164 
166 {
167  DebugAssert(d_goal.get().getExpr().isTrue(),"checkValid: Expected true goal");
168  DebugAssert(d_nonLiterals.get().getExpr().isTrue(),"checkValid: Expected true nonLiterals");
169 
170  TRACE("search", "checkValid(", e, ") {");
171  TRACE_MSG("search terse", "checkValid() {");
172 
173  if (!e.getType().isBool()) {
174  throw TypecheckException
175  ("checking validity of a non-boolean expression:\n\n "
176  + e.toString()
177  + "\n\nwhich has the following type:\n\n "
178  + e.getType().toString());
179  }
180 
181  // A successful query should leave the context unchanged
182  d_core->getCM()->push();
184 
186  TRACE("search", "checkValid: simplifiedThm = ", d_simplifiedThm, "");
187 
188  const Expr& not_e2 = d_simplifiedThm.get().getRHS();
189  Expr e2 = not_e2.negate();
190 
191  // Assert not_e2 if it's not already asserted
192  TRACE_MSG("search terse", "checkValid: Asserting !e: ");
193  TRACE("search", "checkValid: Asserting !e: ", not_e2, "");
194  Theorem not_e2_thm;
195  if(d_assumptions.count(not_e2) == 0) {
196  not_e2_thm = newUserAssumption(not_e2);
197  } else {
198  not_e2_thm = d_assumptions[not_e2];
199  }
200  d_core->addFact(not_e2_thm);
201  d_goal.set(not_e2_thm);
202 
203  return checkValidMain(e2);
204 }
205 
206 
208 {
209  TRACE("search", "restart(", e, ") {");
210  TRACE_MSG("search terse", "restart() {");
211 
212  if (!e.getType().isBool()) {
213  throw TypecheckException
214  ("argument to restart is a non-boolean expression:\n\n "
215  + e.toString()
216  + "\n\nwhich has the following type:\n\n "
217  + e.getType().toString());
218  }
219 
220  if (d_bottomScope == 0) {
221  throw Exception("Call to restart with no current query");
222  }
224 
225  Expr e2 = d_simplifiedThm.get().getRHS().negate();
226 
227  TRACE_MSG("search terse", "restart: Asserting e: ");
228  TRACE("search", "restart: Asserting e: ", e, "");
229  if(d_assumptions.count(e) == 0) {
231  }
232 
233  return checkValidMain(e2);
234 }
235 
236 
238 {
240 }