- Main Page
- Namespaces
- Classes
- Files
- Related Pages

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/GATSAT.h

    00001
    00002 //
    00003 // Copyright (c) 2004           Model-based Embedded and Robotic Systems Group
    00004 // All Rights Reserved          Massachusetts Institute of Technology
    00005 //
    00006 // This software is provided as is. Model-based Embedded and Robotic Systems
    00007 // (MERS) group does not assume any responsibility.
    00008 //
    00009 // Organization:        Model-based Embedded and Robotic Systems Group
    00010 //                                      Massachusetts Institute of Technology
    00011 //
    00013
    00014 #ifndef GATSATHeaderFile
    00015 #define GATSATHeaderFile
    00016
    00017 #include <cstdlib>
    00018
    00019 #include <Mers/Solvers/SAT/SATInterface.h>
    00020 #include <Mers/Models/Base/BaseModelClauseArray.h>
    00021 #include <Mers/Utils/Logging/logger.h>
    00022
    00023 namespace Mers {
    00024         namespace Generators {
    00025                 class AssignmentGeneratorInterface;
    00026         }
    00027 }
    00028
    00029
    00030 namespace Mers {
    00031         namespace Solvers {
    00032                 namespace SAT {
    00033
    00034                         class AssignmentTesterInterface;
    00035
    00036                         namespace GATSAT {
    00037
    00044                                 class GATSAT : public Mers::Solvers::SAT::SATInterface
    00045                                 {
    00046                                 public:
    00048                                         // Constructors
    00050
    00062                                         GATSAT();
    00063
    00075                                         GATSAT(Mers::Generators::AssignmentGeneratorInterface * myGenerator,
    00076                                                                  Mers::Solvers::SAT::AssignmentTesterInterface * myTester);
    00077
    00079                                         // Destructors
    00081
    00085                                         virtual ~GATSAT();
    00086
    00088                                         // Functions
    00090
    00105                                         virtual Mers::Models::Base::BaseModelClause * findSatisfyingSolution(
    00106                                                 int maximumVisitedStateCount, int maxSize);
    00107
    00123                                         virtual Mers::Models::Base::BaseModelClause * findUnsatisfyingSolution(
    00124                                                 int maximumVisitedStateCount, int maxSize);
    00125
    00133                                         virtual void setDebug(unsigned int state);
    00134
    00138                                         virtual void printStatistics() const;
    00139
    00143                                         virtual Mers::Generators::AssignmentGeneratorInterface * getGenerator();
    00144
    00148                                         virtual Mers::Solvers::SAT::AssignmentTesterInterface * getTester();
    00149
    00150                                 protected:
    00152                                         // Data
    00154
    00156                                         Mers::Generators::AssignmentGeneratorInterface * generator;
    00158                                         Mers::Solvers::SAT::AssignmentTesterInterface * tester;
    00159
    00160                                 private:
    00162                                         static log4cplus::Logger m_Logger;
    00163                                 };
    00164                         }
    00165                 }
    00166         }
    00167 }
    00168
    00169 #endif //ndef GATSATHeaderFile
    00170