CVC3  2.4.1
decision_engine.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file decision_engine.cpp
4  * \brief Decision Engine
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Sun Jul 13 22:44:55 2003
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 
23 #include "decision_engine.h"
24 #include "theory_core.h"
25 #include "search.h"
26 
27 
28 using namespace std;
29 using namespace CVC3;
30 
31 
32 DecisionEngine::DecisionEngine(TheoryCore* core, SearchImplBase* se)
33  : d_core(core), d_se(se),
34  d_splitters(core->getCM()->getCurrentContext()),
35  d_splitterCount(core->getStatistics().counter("splitters"))
36 {
37  IF_DEBUG(d_splitters.setName("CDList[SearchEngineDefault.d_splitters]");)
38 }
39 
40 /*****************************************************************************/
41 /*!
42  * Function: DecisionEngine::findSplitterRec
43  *
44  * Author: Clark Barrett
45  *
46  * Created: Sun Jul 13 22:47:06 2003
47  *
48  * Search the expression e (depth-first) for an atomic formula. Note that in
49  * order to support the "simplify in-place" option, each sub-expression is
50  * checked to see if it has a find pointer, and if it does, the find is
51  * followed instead of continuing to recurse on the given expression.
52  * \return a NULL expr if no atomic formula is found.
53  */
54 /*****************************************************************************/
56 {
57  Expr best;
58 
59  if(d_visited.count(e) > 0)
60  return d_visited[e];
61 
62  if (e.isTrue() || e.isFalse() || e.isAtomic()
63  || !d_se->isGoodSplitter(e)) {
64  d_visited[e] = best;
65  return best;
66  }
67 
68  if (e.isAbsAtomicFormula()) {
69  d_visited[e] = e;
70  return e;
71  }
72 
74  if (it != d_bestByExpr.end()) {
75  d_visited[e] = it->second;
76  return it->second;
77  }
78 
79  vector<int> order(e.arity());
80  int i = 0;
81 
82  if (e.isITE())
83  {
84  order[i++] = 0;
85  order[i++] = 1;//e.getHighestKid(); // always 1 or 2
86  order[i++] = 2;//3 - e.getHighestKid();
87  }
88 
89  else
90  {
91  if (e.arity() > 0)
92  {
93  order[i++] = 0;//e.getHighestKid();
94  for (int k = 0; k < e.arity(); ++k)
95  if (k != 0)//e.getHighestKid())
96  order[i++] = k;
97  }
98  }
99 
100  for (int k = 0; k < e.arity(); k++)
101  {
102  Expr splitter =
103  findSplitterRec(d_core->findExpr(e[order[k]]));
104  if (!splitter.isNull() && (best.isNull() || isBetter(splitter, best)))
105  best = splitter;
106  }
107 
108  d_bestByExpr[e] = best;
109  d_visited[e] = best;
110  return best;
111 }
112 
113 
114 /*****************************************************************************/
115 /*!
116  * Function: DecisionEngine::pushDecision
117  *
118  * Author: Clark Barrett
119  *
120  * Created: Sun Jul 13 22:55:16 2003
121  *
122  * \param splitter
123  * \param whichCase If true, increment the splitter count and assert the
124  * splitter. If false, do NOT increment the splitter count and assert the
125  * negation of the splitter. Defaults to true.
126  */
127 /*****************************************************************************/
128 void DecisionEngine::pushDecision(Expr splitter, bool whichCase)
129 {
130  string stCase = whichCase ? "TRUE" : "FALSE";
131  if (whichCase) d_splitterCount++;
132  d_core->getCM()->push();
133  TRACE("search trace", "Asserting splitter("+stCase+"): ", splitter, "");
134  TRACE("search", "Asserting splitter("+stCase+"): ", splitter, "");
135  d_splitters.push_back(splitter);
136  if (!whichCase)
137  splitter = splitter.negate();
138  Theorem thm = d_se->newIntAssumption(splitter);
139  d_core->addFact(thm);
140  // Search engine needs to know what original facts it derived or
141  // split on, so that we don't split on them twice. addFact() may
142  // simplify these facts before calling addLiteralFact() and lose
143  // this information. There is no reason to add non-literals though,
144  // as we never split on them directly.
145  if(thm.getExpr().isAbsLiteral())
146  d_se->addLiteralFact(thm);
147 }
148 
149 
151 {
152  d_core->getCM()->pop();
153  TRACE("search trace", "Pop: scope level =", d_core->getCM()->scopeLevel(), "");
154 }
155 
156 
158 {
159  d_core->getCM()->popto(dl);
160  TRACE("search trace", "Popto: scope level =", d_core->getCM()->scopeLevel(), "");
161 }
162 
163 
165 {
166  return d_splitters.back();
167 }
int arity() const
Definition: expr.h:1201
bool isNull() const
Definition: expr.h:1223
bool isAtomic() const
Test if e is atomic.
Definition: expr.cpp:550
Data structure of expressions in CVC3.
Definition: expr.h:133
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
Expr findSplitterRec(const Expr &e)
Abstract API to the proof search engine.
bool isTrue() const
Definition: expr.h:356
bool isITE() const
Definition: expr.h:423
iterator find(const Expr &e)
Definition: expr_map.h:194
bool isFalse() const
Definition: expr.h:355
ExprMap< Expr > d_visited
Visited cache for findSplitterRec traversal.
Expr lastSplitter()
Return the last known splitter.
bool isAbsAtomicFormula() const
An abstract atomic formua is an atomic formula or a quantified formula.
Definition: expr.h:398
virtual bool isBetter(const Expr &e1, const Expr &e2)=0
const T & back() const
Definition: cdlist.h:82
T & push_back(const T &data, int scope=-1)
Definition: cdlist.h:66
SearchImplBase * d_se
Pointer to search engine.
void popto(int toLevel)
Definition: context.h:403
size_t count(const Expr &e) const
Definition: expr_map.h:173
void pushDecision(Expr splitter, bool whichCase=true)
Push context and record the splitter.
virtual Theorem newIntAssumption(const Expr &e)
Add a new internal asserion.
bool isGoodSplitter(const Expr &e)
Check if a splitter is required for completeness.
virtual void addLiteralFact(const Theorem &thm)=0
Notify the search engine about a new literal fact.
Expr negate() const
Definition: expr.h:937
Expr findExpr(const Expr &e)
Return the find of e, or e if it has no find.
Definition: theory.h:503
#define IF_DEBUG(code)
Definition: debug.h:406
void popTo(int dl)
Pop to given scope.
Expr getExpr() const
Definition: theorem.cpp:230
TheoryCore * d_core
Pointer to core theory.
ContextManager * getCM() const
Definition: theory_core.h:348
ExprMap< Expr > d_bestByExpr
CDList< Expr > d_splitters
List of currently active splitters.
void popDecision()
Pop last decision (and context)
API to to a generic proof search engine (a.k.a. SAT solver)
bool isAbsLiteral() const
Test if e is an abstract literal.
Definition: expr.h:406
StatCounter d_splitterCount
Total number of splitters.
Definition: kinds.h:99
iterator end()
Definition: expr_map.h:191
void addFact(const Theorem &e)
Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure;...