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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ValidSAT/VSATNode.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_VSATNODE_H__F647BE97_86ED_4E75_AF47_404977DC1EBA__INCLUDED_)
    00015 #define AFX_VSATNODE_H__F647BE97_86ED_4E75_AF47_404977DC1EBA__INCLUDED_
    00016
    00017 #if _MSC_VER > 1000
    00018 #pragma once
    00019 #endif // _MSC_VER > 1000
    00020
    00021 #ifdef _MSC_VER
    00022 #pragma warning( disable : 4786 )
    00023 #endif
    00024
    00025 #include <Mers/Utils/Containers/IntegerArray.h>
    00026 #include <Mers/Utils/Containers/DynamicArrayTemplate.h>
    00027 #include "VSATVariable.h"
    00028 #include <Mers/Models/Base/BaseModelSentence.h>
    00029
    00030 namespace Mers {
    00031         namespace Solvers {
    00032                 namespace SAT {
    00033                         namespace ValidSAT {
    00034
    00041                                 class VSATNode
    00042                                 {
    00043                                 public:
    00046                                         enum SolutionType {Unsatisfiable, Satisfiable, Valid, Unknown};
    00047
    00065                                         VSATNode(Mers::Utils::Containers::DynamicArrayTemplate<VSATVariable> const &myVariables,
    00066                                                                          Mers::Models::Base::BaseModelSentence const &myConstraint,
    00067                                                                          bool myTestForValid);
    00068
    00078                                         VSATNode(VSATNode const &other);
    00079
    00083                                         virtual ~VSATNode();
    00084
    00091                                         void addConstraint(Mers::Models::Base::BaseModelClause const * newConstraint);
    00092
    00124                                         void propagate(Mers::Models::Base::BaseModelAssignment const &asg, bool positive, bool ignoreConstraint = true,
    00125                                                                                                  bool unitPropagate = true);
    00126
    00134                                         SolutionType getStatus()
    00135                                         {
    00136                                                 return solutionStatus;
    00137                                         }
    00138
    00149                                         SolutionType evaluate();
    00150
    00158                                         double getExpandCount();
    00159
    00166                                         Mers::Models::Base::BaseModelAssignmentArray & getUnsatAssignment();
    00167
    00174                                         Mers::Models::Base::BaseModelAssignmentArray & getValidAssignment();
    00175
    00181                                         virtual void setDebug(unsigned int state)
    00182                                         {
    00183                                                 debug = state;
    00184                                         }
    00185
    00186                                 protected:
    00192                                         void adjustValidAssignment();
    00193
    00194                                 protected:
    00197                                         Mers::Utils::Containers::DynamicArrayTemplate<Mers::Models::Base::BaseModelAssignmentArray> domains;
    00198
    00200                                         Mers::Utils::Containers::DynamicArrayTemplate<VSATVariable> allVariables;
    00201
    00204                                         Mers::Utils::Containers::IntegerArray unassignedVariableIndex;
    00205
    00209                                         Mers::Utils::Containers::DynamicArrayTemplate<VSATVariable> unassignedVariables;
    00210
    00213                                         Mers::Models::Base::BaseModelSentence constraints;
    00214
    00216                                         SolutionType solutionStatus;
    00217
    00221                                         bool notValid;
    00222
    00225                                         double numberOfExpandedNodes;
    00226
    00229                                         bool testForValid;
    00230
    00232                                         Mers::Models::Base::BaseModelAssignmentArray validAssignment;
    00234                                         Mers::Models::Base::BaseModelAssignmentArray unsatAssignment;
    00235
    00237                                         unsigned int debug;
    00238                                 };
    00239                         }
    00240                 }
    00241         }
    00242 }
    00243
    00244 #endif // !defined(AFX_VSATNODE_H__F647BE97_86ED_4E75_AF47_404977DC1EBA__INCLUDED_)