CVC3  2.4.1
search_simple.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file search_simple.h
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Sat Mar 29 21:53:46 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 #ifndef _cvc3__include__search_simple_h_
22 #define _cvc3__include__search_simple_h_
23 
24 #include "search_impl_base.h"
25 #include "statistics.h"
26 
27 namespace CVC3 {
28 
29 class DecisionEngine;
30 
31 /*!
32  * \defgroup SE_Simple Simple Search Engine
33  * \ingroup SE
34  *
35  * This module includes all the components of a very simplistic search
36  * engine. It is used mainly for debugging purposes.
37  */
38 
39  //! Implementation of the simple search engine
40  /*! \ingroup SE_Simple */
42  /*! \addtogroup SE_Simple
43  * @{
44  */
45 
46  //! Name
47  std::string d_name;
48 
49  //! Decision Engine
51 
52  //! Formula being checked
54  //! Non-literals generated by DP's
56  //! Theorem which records simplification of the last query
58 
59  //! Recursive DPLL algorithm used by checkValid
61  //! Private helper function for checkValid and restart
62  QueryResult checkValidMain(const Expr& e2);
63 
64 public:
65  //! Constructor
66  SearchSimple(TheoryCore* core);
67  //! Destructor
68  ~SearchSimple();
69 
70  // Implementation of virtual SearchEngine methods
71  const std::string& getName() { return d_name; }
74  void addLiteralFact(const Theorem& thm) {}
75  void addNonLiteralFact(const Theorem& thm);
76 
77  /*! @} */ // end addtogroup SE_Simple
78 };
79 
80 }
81 
82 #endif