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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ValidSAT/ValidSAT.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 #if !defined(AFX_ValidSAT_H__919094E2_0024_407B_A715_A813D47AA3BA__INCLUDED_)
    00015 #define AFX_ValidSAT_H__919094E2_0024_407B_A715_A813D47AA3BA__INCLUDED_
    00016
    00017 #if _MSC_VER > 1000
    00018 #pragma once
    00019 #endif // _MSC_VER > 1000
    00020
    00021 #include "VSATNode.h"
    00022
    00023 #include <Mers/Utils/Containers/DynamicArrayTemplate.h>
    00024 #include <Mers/Solvers/SAT/AssignmentTesterInterface.h>
    00025 #include <Mers/Models/Base/BaseModelSentence.h>
    00026 #include "VSATVariable.h"
    00027
    00028 namespace Mers {
    00029         namespace Models {
    00030                 namespace Base {
    00031                         class BaseModelVariableArray;
    00032                 }
    00033         }
    00034 }
    00035
    00036 namespace Mers {
    00037         namespace Solvers {
    00038                 namespace SAT {
    00039                         namespace ValidSAT {
    00040
    00047                                 class ValidSAT : public Mers::Solvers::SAT::AssignmentTesterInterface
    00048                                 {
    00049                                 public:
    00050
    00058                                         virtual void addConstraint(Mers::Models::Base::BaseModelClause const * constraint);
    00059
    00067                                         virtual void addTemporaryConstraint(Mers::Models::Base::BaseModelClause const * constraint);
    00068
    00077                                         virtual void setTemporaryConstraint(Mers::Models::Base::BaseModelClause const * constraint);
    00078
    00082                                         virtual void clearTemporaryConstraint();
    00083
    00084
    00108                                         ValidSAT(Mers::Models::Base::BaseModelVariableArray const &myAllVariables,
    00109                                                                          Mers::Models::Base::BaseModelVariableArray const &myDecisionVariables,
    00110                                                                          Mers::Models::Base::BaseModelSentence const &myConstraint,
    00111                                                                          bool myTestForValid = true);
    00112
    00116                                         virtual ~ValidSAT();
    00117
    00144                                         virtual SolutionType tryAssignment(
    00145                                                                                                                                                                                  Mers::Models::Base::BaseModelAssignmentArray const * candidate, int group, bool satisfy,
    00146                                                                                                                                                                                  Mers::Models::Base::BaseModelAssignmentArray &conflict);
    00147
    00154                                         void printStatistics(bool verbose = false) const;
    00155
    00161                                         virtual void setDebug(unsigned int state);
    00162
    00167                                         virtual double getNumberOfSteps() const {
    00168                                                 return numberOfExpandedNodes;
    00169                                         }
    00170
    00171                                 protected:
    00174                                         Mers::Models::Base::BaseModelSentence constraint;
    00176                                         Mers::Utils::Containers::DynamicArrayTemplate<VSATVariable> variables;
    00177
    00178                                         // the VSAT Node containing the initial model constraints
    00179                                         // w/o any additional constraints.
    00180                                         VSATNode * modelNode;
    00181
    00182                                         // the VSAT Node containing the current model constraints
    00183                                         // with all temporary constraints.
    00184                                         VSATNode * activeNode;
    00185
    00186                                         // number of nodes expanded during all searches for
    00187                                         // Valid/SAT/UNSAT.
    00188                                         double numberOfExpandedNodes;
    00189
    00190                                         // number of Valid, SAT, and UNSAT answers returned.
    00191                                         unsigned int validTests, satisfiableTests, unsatisfiableTests;
    00192
    00193                                         // true if we're testing for Valid, false if we're just
    00194                                         // testing for sat/unsat.
    00195                                         bool testForValid;
    00196                                 };
    00197                         }
    00198                 }
    00199         }
    00200 }
    00201
    00202 #endif // !defined(AFX_ValidSAT_H__919094E2_0024_407B_A715_A813D47AA3BA__INCLUDED_)