search_simple.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file search_simple.h
00004  * 
00005  * Author: Clark Barrett
00006  * 
00007  * Created: Sat Mar 29 21:53:46 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 
00021 #ifndef _cvc3__include__search_simple_h_
00022 #define _cvc3__include__search_simple_h_
00023 
00024 #include "search_impl_base.h"
00025 #include "statistics.h"
00026 
00027 namespace CVC3 {
00028 
00029 class DecisionEngine;
00030 
00031 /*!
00032  * \defgroup SE_Simple Simple Search Engine
00033  * \ingroup SE
00034  *
00035  * This module includes all the components of a very simplistic search
00036  * engine.  It is used mainly for debugging purposes.
00037  */
00038 
00039   //! Implementation of the simple search engine
00040   /*! \ingroup SE_Simple */
00041 class SearchSimple: public SearchImplBase {
00042   /*! \addtogroup SE_Simple 
00043    * @{
00044    */
00045 
00046   //! Name
00047   std::string d_name;
00048 
00049   //! Decision Engine
00050   DecisionEngine* d_decisionEngine;
00051 
00052   //! Formula being checked
00053   CDO<Theorem> d_goal;
00054   //! Non-literals generated by DP's
00055   CDO<Theorem> d_nonLiterals;
00056   //! Theorem which records simplification of the last query
00057   CDO<Theorem> d_simplifiedThm;
00058 
00059   //! Recursive DPLL algorithm used by checkValid
00060   QueryResult checkValidRec(Theorem& thm);
00061   //! Private helper function for checkValid and restart
00062   QueryResult checkValidMain(const Expr& e2);
00063 
00064 public:
00065   //! Constructor
00066   SearchSimple(TheoryCore* core);
00067   //! Destructor
00068   ~SearchSimple();
00069   
00070   // Implementation of virtual SearchEngine methods
00071   const std::string& getName() { return d_name; }
00072   QueryResult checkValidInternal(const Expr& e);
00073   QueryResult restartInternal(const Expr& e);
00074   void addLiteralFact(const Theorem& thm) {}
00075   void addNonLiteralFact(const Theorem& thm);
00076 
00077   /*! @} */ // end addtogroup SE_Simple
00078 };
00079 
00080 }
00081 
00082 #endif

Generated on Wed Nov 18 16:13:31 2009 for CVC3 by  doxygen 1.5.2