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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/unit-tests/GatsatTester.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 //
    00010
    00011 #ifndef MERS_SOLVERS_SAT_GATSAT_UNITTESTS_GATSATTESTER_HEADER_FILE
    00012 #define MERS_SOLVERS_SAT_GATSAT_UNITTESTS_GATSATTESTER_HEADER_FILE
    00013
    00014 #include <Mers/Models/Base/unit-tests/BMHelper.h>
    00015
    00016 #include <tut.h>
    00017 #include <Mers/Solvers/SAT/GATSAT/GatsatFactory.h>
    00018 #include <Mers/Solvers/SAT/GATSAT/GATSAT.h>
    00019 #include <Mers/Solvers/SAT/AssignmentTesterInterface.h>
    00020 #include <Mers/Models/Base/BaseModelDomainArray.h>
    00021 #include <Mers/Utils/Containers/IntegerArray.h>
    00022 #include <Mers/Utils/Logging/logger.h>
    00023 #include <sstream>
    00024
    00025 namespace Mers {
    00026         namespace Solvers {
    00027                 namespace SAT {
    00028                         namespace GATSAT {
    00029                                 namespace unit_tests {
    00030
    00038                                         class GatsatTester : public tut::BMHelper
    00039                                         {
    00040                                         public:
    00044                                                 GatsatTester();
    00045
    00049                                                 virtual ~GatsatTester();
    00050
    00051                                         protected:
    00058                                                 template<int n>
    00059                                                 void initGATSAT(unsigned int numDomains,
    00060                                                         const struct BMDomainEntry * domains,
    00061                                                         unsigned int numVariables,
    00062                                                         const struct BMVariableEntry * variables,
    00063                                                         unsigned int numSearchVariables,
    00064                                                         const unsigned int * searchVariables,
    00065                                                         unsigned int numClauses,
    00066                                                         const int clauseData[][n],
    00067                                                         const Mers::Solvers::SAT::GATSAT::GatsatFactory &factory)
    00068                                                         throw() {
    00069
    00070                                                         // Load our domain data.
    00071                                                         loadDomainData(numDomains, domains, m_Domains);
    00072
    00073                                                         // Load our variable data.
    00074                                                         loadVariableData(numVariables, variables, m_Domains,
    00075                                                                 m_Variables);
    00076
    00077                                                         // Load our theory
    00078                                                         loadClauses(numClauses, clauseData, m_Variables, m_Theory);
    00079
    00080                                                         // Get our search variables
    00081                                                         getSearchVarData(numSearchVariables, searchVariables,
    00082                                                                 m_Variables, m_SearchVariables);
    00083
    00084                                                         // Set our engine
    00085                                                         m_GAT =
    00086                                                                 factory.createGatsat(m_SearchVariables, m_Variables, m_Theory);
    00087                                                 }
    00088
    00107                                                 void getSearchVarData(unsigned int numVariables,
    00108                                                         const unsigned int * sVarData,
    00109                                                         Mers::Models::Base::BaseModelVariableArray &allVars,
    00110                                                         Mers::Models::Base::BaseModelVariableArray &searchVars) {
    00111                                                         getVariableSubset(numVariables, sVarData, allVars, searchVars);
    00112                                                 }
    00113
    00146                                                 template<int n, int v> void testGATSAT(unsigned int numberOfIClauses,
    00147                                                         const int initialClauseData[][n],
    00148                                                         unsigned int numberOfResults,
    00149                                                         const unsigned int expectedResultsData[][v],
    00150                                                         bool sat,
    00151                                                         bool verifyTermination = true)
    00152                                                 {
    00153                                                         long maximumVisitedStateCount = 10000000;
    00154                                                         long maxSize = 10000000;
    00155
    00156                                                         log4cplus::Logger log = log4cplus::Logger::getInstance(
    00157                                                                 "Mers.Solvers.SAT.GATSAT.unit-tests.GatsatTester");
    00158
    00159                                                         LOG4CPLUS_DEBUG_STR(log, "*** Testing GATSAT ***");
    00160                                                         LOG4CPLUS_DEBUG(log, "*** With " << numberOfIClauses <<
    00161                                                                 " initial clauses and " << numberOfResults <<
    00162                                                                 " expected results.");
    00163
    00164                                                         tut::ensure("GATSAT Generator != NULL", m_GAT != NULL);
    00165
    00166                                                         std::vector<Mers::Models::Base::BaseModelAssignmentArray *>
    00167                                                                 expectedResults;
    00168                                                         Mers::Models::Base::BaseModelSentence initialClauses(
    00169                                                                 Mers::Models::Base::BaseModelSentence::CNF, true);
    00170
    00171                                                         loadAssignments(expectedResults, numberOfResults,
    00172                                                                 expectedResultsData, m_SearchVariables);
    00173                                                         loadClauses(numberOfIClauses, initialClauseData, m_Variables,
    00174                                                                 initialClauses);
    00175
    00176                                                         // Log our initial constraints
    00177                                                         if(initialClauses.size() > 0)
    00178                                                                 LOG4CPLUS_TRACE_STR(log,
    00179                                                                         "Running with Temporary Constraints:");
    00180                                                         for(unsigned int i = 0; i < initialClauses.size(); i++) {
    00181                                                                 std::stringstream ss;
    00182                                                                 initialClauses[i]->printArray(ss, ", ");
    00183                                                                 LOG4CPLUS_TRACE_STR(log, ss.str().c_str());
    00184                                                         }
    00185                                                         // Log our expected results.
    00186                                                         if(expectedResults.size())
    00187                                                                 LOG4CPLUS_TRACE_STR(log, "Runtime Data:");
    00188                                                         for(unsigned int i = 0; i < expectedResults.size(); i++) {
    00189                                                                 std::stringstream ss;
    00190
    00191                                                                 ss << "Exp Res: ";
    00192                                                                 expectedResults[i]->printArray(ss, ", ");
    00193
    00194                                                                 LOG4CPLUS_TRACE_STR(log, ss.str().c_str());
    00195                                                         }
    00196
    00197                                                         tut::ensure_equals("Expected number of results",
    00198                                                                 expectedResults.size(), numberOfResults);
    00199                                                         tut::ensure_equals("Expected number of initial conflicts",
    00200                                                                 initialClauses.size(), numberOfIClauses);
    00201
    00202                                                         AssignmentTesterInterface * tester = m_GAT->getTester();
    00203                                                         tut::ensure("GATSAT Tester != NULL", tester != NULL);
    00204
    00205                                                         for(unsigned int c = 0; c < initialClauses.size(); c++)
    00206                                                         {
    00207                                                                 tester->addTemporaryConstraint(initialClauses[c]);
    00208                                                         }
    00209
    00210                                                         for(unsigned int s = 0; s < expectedResults.size(); s++)
    00211                                                         {
    00212                                                                 // Get the next solution.
    00213                                                                 Mers::Models::Base::BaseModelAssignmentArray const *
    00214                                                                         actualSolution;
    00215
    00216                                                                 if(sat)
    00217                                                                         actualSolution = m_GAT->findSatisfyingSolution(
    00218                                                                                 maximumVisitedStateCount, maxSize);
    00219                                                                 else
    00220                                                                         actualSolution = m_GAT->findUnsatisfyingSolution(
    00221                                                                                 maximumVisitedStateCount, maxSize);
    00222
    00223                                                                 // Get the next expected solution.
    00224                                                                 Mers::Models::Base::BaseModelAssignmentArray const *
    00225                                                                         expectedSolution = expectedResults[s];
    00226
    00227                                                                 tut::ensure("Expecting another solution",
    00228                                                                         actualSolution != NULL);
    00229                                                                 tut::ensure_equals("Actual and expected solution have "
    00230                                                                         "the same length", expectedSolution->getLength(),
    00231                                                                         actualSolution->getLength());
    00232                                                                 tut::ensure_equals("Generated Solution",
    00233                                                                         *actualSolution, *expectedSolution);
    00234
    00235                                                                 {
    00236                                                                         // Log the solution we found.
    00237                                                                         std::stringstream ss;
    00238                                                                         ss << "Solution: ";
    00239                                                                         actualSolution->printArray(ss, ", ");
    00240                                                                         LOG4CPLUS_TRACE_STR(log, ss.str().c_str());
    00241                                                                 }
    00242                                                         }
    00243
    00244                                                         // Verify that the engine terminated.
    00245                                                         if(verifyTermination) {
    00246                                                                 Mers::Models::Base::BaseModelAssignmentArray const *
    00247                                                                         actualSolution;
    00248
    00249                                                                 LOG4CPLUS_TRACE_STR(log, "Checking for termination.");
    00250
    00251                                                                 if(sat)
    00252                                                                         actualSolution = m_GAT->findSatisfyingSolution(
    00253                                                                                 maximumVisitedStateCount, maxSize);
    00254                                                                 else
    00255                                                                         actualSolution = m_GAT->findUnsatisfyingSolution(
    00256                                                                                 maximumVisitedStateCount, maxSize);
    00257
    00258                                                                 LOG4CPLUS_TRACE(log, "Solution was " << actualSolution);
    00259
    00260                                                                 tut::ensure("No additional solutions", actualSolution == NULL);
    00261
    00262                                                                 LOG4CPLUS_TRACE_STR(log, "All Done");
    00263                                                         }
    00264
    00265                                                         for(unsigned int s = 0; s < expectedResults.size(); s++)
    00266                                                                 delete expectedResults[s];
    00267                                                         for(unsigned int s = 0; s < initialClauses.size(); s++)
    00268                                                                 delete initialClauses[s];
    00269
    00270                                                         LOG4CPLUS_DEBUG_STR(log, "*** GATSAT Test Complete");
    00271                                                 }
    00272
    00273                                         protected:
    00275                                                 Mers::Solvers::SAT::GATSAT::GATSAT * m_GAT;
    00276
    00277                                                 // The list of all variables.
    00278                                                 Mers::Models::Base::BaseModelVariableArray m_Variables;
    00279
    00280                                                 // The list of all search variables.
    00281                                                 Mers::Models::Base::BaseModelVariableArray m_SearchVariables;
    00282
    00283                                                 // The list of all domains.
    00284                                                 Mers::Models::Base::BaseModelDomainArray m_Domains;
    00285
    00286                                                 // The theory.
    00287                                                 Mers::Models::Base::BaseModelSentence m_Theory;
    00288                                         };
    00289                                 }
    00290                         }
    00291                 }
    00292         }
    00293 }
    00294
    00295 #endif