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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/OpSAT/Opsat.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 //# CHECKED MJP 08-07-2002
    00014
    00015 #ifndef __OPSAT__
    00016 #define __OPSAT__
    00017
    00018 #include <cstdlib>
    00019 #include <iostream>
    00020
    00021 #include <Mers/Solvers/SAT/GATSAT/GATSAT.h>
    00022 #include <Mers/Utils/Containers/DynamicArrayTemplate.h>
    00023 #include <Mers/Models/CCA/CCATransition.h>
    00024
    00025 #include <vector>
    00026
    00027 namespace Mers {
    00028         namespace Models {
    00029                 namespace Base {
    00030                         class BaseModelVariableArray;
    00031                         class BaseModelSentence;
    00032                         class BaseModelClause;
    00033                 }
    00034                 namespace CCA {
    00035                         class CCAVariables;
    00036                         class CCAModel;
    00037                 }
    00038         }
    00039         namespace Utils {
    00040                 namespace Containers {
    00041                         class IntegerArray;
    00042                 }
    00043         }
    00044         namespace Generators {
    00045                 namespace BFIG {
    00046                         class BFIGObjectiveFunction;
    00047                 }
    00048         }
    00049         namespace Solvers {
    00050                 namespace SAT {
    00051                         namespace GATSAT {
    00052                                 namespace OpSAT {
    00053
    00062                                         class Opsat : public GATSAT
    00063                                         {
    00064                                         public:
    00065                                                 typedef Mers::Utils::Containers::DynamicArrayTemplate<Mers::Models::Base::BaseModelSentence const> GuardArray;
    00066
    00068                                                 //      CONSTRUCTOR
    00070
    00092                                                 Opsat(Mers::Models::Base::BaseModelVariableArray const & designVariables,
    00093                                                                         Mers::Generators::BFIG::BFIGObjectiveFunction const * ocspObjectiveFunction,
    00094                                                                         Mers::Models::Base::BaseModelVariableArray const & allVariables,
    00095                                                                         Mers::Models::Base::BaseModelSentence const & constraintSet,
    00096                                                                         bool use_dpll = true, double cutoffCost = 1e10);
    00097
    00098
    00120                                                 Opsat(Mers::Models::CCA::CCAVariables const & designVariables,
    00121                                                                         Mers::Models::CCA::CCAModel const & model, bool use_dpll,
    00122                                                                         double cutoffCost);
    00123
    00142                                                 Opsat(Mers::Models::CCA::CCAVariables const & designVariables,
    00143                                                                         Mers::Models::CCA::CCAModel const & model,
    00144                                                                         bool use_dpll = true);
    00145
    00168                                                 Opsat(Mers::Models::CCA::CCAVariables const & designVariables,
    00169                                                         Mers::Models::CCA::CCAModel const & model,
    00170                                                         Mers::Models::Base::BaseModelSentence const & constraintSet,
    00171                                                         bool use_dpll, double cutoffCost);
    00172
    00173
    00193                                                 Opsat(Mers::Models::CCA::CCAVariables const & designVariables,
    00194                                                         Mers::Models::CCA::CCAModel const & model,
    00195                                                         Mers::Models::Base::BaseModelSentence const & constraintSet,
    00196                                                         bool use_dpll = true);
    00197
    00205                                                 Opsat(Mers::Models::Base::BaseModelVariableArray const & designVariables,
    00206                                                                         Mers::Utils::Containers::IntegerArray const &valueMap,
    00207                                                                         std::vector<double> const & designVarProbs,
    00208                                                                         Mers::Models::Base::BaseModelVariableArray const & allVariables,
    00209                                                                         Mers::Models::Base::BaseModelSentence const & constraintSet,
    00210                                                                         bool use_dpll, double cutoffCost);
    00211
    00216                                                 Opsat(Mers::Models::Base::BaseModelVariableArray const & designVariables,
    00217                                                                         Mers::Utils::Containers::IntegerArray const &valueMap,
    00218                                                                         std::vector<double> const & designVarProbs,
    00219                                                                         Mers::Models::Base::BaseModelVariableArray const & allVariables,
    00220                                                                         Mers::Models::Base::BaseModelSentence const & constraintSet,
    00221                                                                         bool use_dpll = true);
    00222
    00230                                                 Opsat(Mers::Models::Base::BaseModelVariableArray const & variableSet,
    00231                                                         Mers::Utils::Containers::IntegerArray const &valueMap,
    00232                                                         std::vector<double> const & designVarProbs,
    00233                                                         Mers::Models::Base::BaseModelSentence const & constraintSet,
    00234                                                         double cutoffCost);
    00235
    00240                                                 Opsat(Mers::Models::Base::BaseModelVariableArray const & variableSet,
    00241                                                         Mers::Utils::Containers::IntegerArray const &valueMap,
    00242                                                         std::vector<double> const & designVarProbs,
    00243                                                         Mers::Models::Base::BaseModelSentence const & constraintSet);
    00244
    00262                                                 Opsat(Mers::Generators::AssignmentGeneratorInterface * myGenerator,
    00263                                                                         Mers::Models::Base::BaseModelVariableArray const & searchVariables,
    00264                                                                         Mers::Models::Base::BaseModelVariableArray const & allVariables,
    00265                                                                         Mers::Models::Base::BaseModelSentence const & constraintSet,
    00266                                                                         bool use_dpll = true);
    00267
    00268                                                 ~Opsat();
    00269
    00271                                                 //      PUBLIC FUNCTION METHODS
    00273
    00288                                                 void setTemporaryConstraint(Mers::Models::Base::BaseModelClause const * c);
    00289
    00304                                                 void constrainByReachability();
    00305
    00312                                                 void              constrainByNextState();
    00313
    00319                                                 void              clearTemporaryConstraint();
    00320
    00327                                                 void              addConstraint(Mers::Models::Base::BaseModelClause const * c);
    00328
    00329                                                 void              skipExpanding(bool doSkip);
    00330
    00331 #ifndef EMBEDDED
    00332
    00341                                                 friend std::ostream & operator <<(std::ostream &out, Opsat const &other);
    00342 #endif
    00343
    00344                                         protected:
    00348                                                 void testTheory();
    00349
    00350
    00351                                         private:
    00353                                                 //      Functions
    00355
    00372                                                 void createBFIG(Mers::Models::Base::BaseModelVariableArray const & designVariables,
    00373                                                         Mers::Generators::BFIG::BFIGObjectiveFunction const * ocspObjectiveFunction,
    00374                                                         Mers::Models::Base::BaseModelVariableArray const &allVariables,
    00375                                                         double cutoffCost);
    00376
    00377
    00393                                                 void createBFIG(Mers::Models::CCA::CCAVariables const & designVariables,
    00394                                                         Mers::Models::CCA::CCAModel const & model, double cutoffCost);
    00395
    00408                                                 void createBFIG(Mers::Models::CCA::CCAVariables const & designVariables,
    00409                                                         Mers::Models::CCA::CCAModel const & model);
    00410
    00436                                                 void createBFIG(Mers::Models::Base::BaseModelVariableArray const & designVariables,
    00437                                                         Mers::Models::Base::BaseModelVariableArray const &allVariables,
    00438                                                         Mers::Utils::Containers::IntegerArray const &valueMap,
    00439                                                         std::vector<double> const & probabilities,
    00440                                                         double cutoffCost);
    00441
    00464                                                 void createBFIG(Mers::Models::Base::BaseModelVariableArray const & designVariables,
    00465                                                         Mers::Models::Base::BaseModelVariableArray const &allVariables,
    00466                                                         Mers::Utils::Containers::IntegerArray const &valueMap,
    00467                                                         std::vector<double> const & probabilities);
    00468
    00470                                                 //      PRIVATE DATA MEMBERS
    00472
    00473                                                 bool                   noExpand;
    00474                                         };
    00475                                 }
    00476                         }
    00477                 }
    00478         }
    00479 }
    00480
    00481 #endif //ndef __OPSAT__
    00482