CVC3  2.4.1
decision_engine_dfs.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file decision_engine_dfs.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_dfs.h"
24 #include "theory_core.h"
25 #include "search.h"
26 
27 
28 using namespace std;
29 using namespace CVC3;
30 
31 
32 bool DecisionEngineDFS::isBetter(const Expr& e1, const Expr& e2)
33 {
34  return false;
35 }
36 
37 
38 /*****************************************************************************/
39 /*!
40  * Function: DecisionEngineDFS::DecisionEngineDFS
41  *
42  * Author: Clark Barrett
43  *
44  * Created: Sun Jul 13 22:52:51 2003
45  *
46  * Constructor
47  */
48 /*****************************************************************************/
49 DecisionEngineDFS::DecisionEngineDFS(TheoryCore* core, SearchImplBase* se)
50  : DecisionEngine(core, se)
51 {
52 }
53 
54 
55 /*****************************************************************************/
56 /*!
57  * Function: DecisionEngineDFS::findSplitter
58  *
59  * Author: Clark Barrett
60  *
61  * Created: Sun Jul 13 22:53:18 2003
62  *
63  * Main function to choose the next splitter.
64  * \return NULL if all known splitters are assigned.
65  */
66 /*****************************************************************************/
68  TRACE("splitters verbose", "findSplitter(", e, ") {");
69  Expr splitter; // Null by default
70  d_visited.clear();
71 
72  if (!e.isNull()) {
73  splitter = findSplitterRec(e);
74  // It's OK not to find a splitter, since e may contain only "bad"
75  // splitters, according to d_se->isGoodSplitter(e)
76 
77 // DebugAssert(!splitter.isNull(),
78 // "findSplitter: can't find splitter in non-literal: "
79 // + e.toString());
80  IF_DEBUG(if(!splitter.isNull())
81  debugger.counter("splitters from decision engine")++;)
82  }
83  TRACE("splitters verbose", "findSplitter => ", splitter, " }");
84  return splitter;
85 }
86 
87 
89 {
90 }
bool isNull() const
Definition: expr.h:1223
void clear()
Definition: expr_map.h:175
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.
ExprMap< Expr > d_visited
Visited cache for findSplitterRec traversal.
virtual void goalSatisfied()
Search should call this when it derives 'false'.
virtual Expr findSplitter(const Expr &e)
Find the next splitter.
#define IF_DEBUG(code)
Definition: debug.h:406
API to to a generic proof search engine (a.k.a. SAT solver)
Definition: kinds.h:99