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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ISAT/ISATTester.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 #if !defined(ISATTester_)
    00016 #define ISATTester_
    00017
    00018 #if defined _MSC_VER
    00019 #pragma warning(disable:4786)
    00020 #endif // #if defined _MSC_VER
    00021
    00022 #include <cstdlib>
    00023
    00024 #include <Mers/Solvers/SAT/AssignmentTesterInterface.h>
    00025
    00026 #include "ISAT.h"
    00027 #include "ISATClauses.h"
    00028 #include <Mers/Models/Base/BaseModelVariableArray.h>
    00029 #include <Mers/Models/Base/BaseModelClauseArray.h>
    00030
    00031 namespace Mers {
    00032         namespace Models {
    00033                 namespace Base {
    00034                         class BaseModelSentence;
    00035                 }
    00036         }
    00037 }
    00038
    00039 namespace Mers {
    00040         namespace Solvers {
    00041                 namespace SAT {
    00042                         namespace ISAT {
    00043
    00044                                 class ISATClause;
    00045
    00052                                 class ISATTester : public Mers::Solvers::SAT::AssignmentTesterInterface
    00053                                 {
    00055                                         // Friends
    00057
    00058                                         friend std::ostream &operator<<(std::ostream&, ISATTester const &);
    00059
    00060                                 public:
    00062                                         // Public Constructors, Copy Constructors, & Destructors
    00064
    00079                                         ISATTester(Mers::Models::Base::BaseModelVariableArray const & variableSet,
    00080                                                                                  Mers::Models::Base::BaseModelVariableArray const & searchVariableSet,
    00081                                                                                  Mers::Models::Base::BaseModelSentence const & constraintSet);
    00082
    00086                                         virtual ~ISATTester();
    00087
    00089                                         // Public Function Members
    00091
    00118                                         virtual SolutionType tryAssignment(
    00119                                                                                                                                                                                  Mers::Models::Base::BaseModelAssignmentArray const * candidate, int group, bool satisfy,
    00120                                                                                                                                                                                  Mers::Models::Base::BaseModelAssignmentArray &conflict);
    00121
    00128                                         virtual void printStatistics(bool verbose = false) const;
    00129
    00135                                         virtual void setDebug(unsigned int state);
    00136
    00137
    00145                                         void setDPLLFlag(bool dpll_flag);
    00146
    00155                                         void filterSearchVariables(bool filterFlag) {
    00156                                                 mUseFilter = filterFlag;
    00157                                         }
    00158
    00159                                         void            suppressWarnings(bool off = true);
    00160
    00161                                         void            addConstraint(Mers::Models::Base::BaseModelClause const * c);
    00162                                         void                    addTemporaryConstraint(Mers::Models::Base::BaseModelClause const * c);
    00163                                         void            setTemporaryConstraint(Mers::Models::Base::BaseModelClause const * c);
    00164                                         void            clearTemporaryConstraint();
    00165                                         void            constrainByReachability();
    00166                                         void            constrainByNextValue();
    00167                                         void            addDomainConstraints();
    00168
    00173                                         virtual double getNumberOfSteps() const;
    00174
    00182                                         bool            SAT_consistent(bool useDPLL, bool certain = true);
    00183
    00191                                         bool            UNSAT_inconsistent(bool useDPLL, bool certain = true);
    00192
    00193                                         bool            consistent(bool satisfy, bool useDPLL);
    00194                                         bool            consistentMaybe(bool satisfy, bool useDPLL);
    00195
    00197                                         // Private Object & Data Members
    00199
    00200                                         bool            hasTemporary;
    00201
    00202                                 private:
    00204                                         // Private Function Members
    00206
    00207                                         void                    init(Mers::Models::Base::BaseModelSentence const & baseConstraintSet,
    00208                                                                                                  Mers::Models::Base::BaseModelSentence const & satConstraintSet,
    00209                                                                                                  Mers::Models::Base::BaseModelSentence const & unsatConstraintSet);
    00210                                         //#     isatClause      constraintToisatClause(Constraint const * cons, bool disjunctive = true);
    00211
    00212                                         ISATClause *    insert_disjunctive_constraint(Mers::Models::Base::BaseModelAssignmentArray const *constraint_p);
    00213                                         void                    insert_conjunctive_constraint_as_candidate(Mers::Models::Base::BaseModelAssignmentArray const *constraint_p);
    00214                                         void                    clear_candidate();
    00215
    00217                                         // Private Object & Data Members
    00219
    00220                                         Mers::Solvers::SAT::ISAT::ISAT                  SAT_engine;
    00221                                         ISATClauses                                     fact_clauses;
    00222                                         ISATClauses                                     candidate_clauses;
    00223                                         bool                      noWarn;
    00224                                         bool useDPLL;
    00225
    00227                                         //search variables.
    00228                                         bool mUseFilter;
    00229
    00231                                         Mers::Models::Base::BaseModelVariableArray propositionVariables;
    00232
    00235                                         Mers::Models::Base::BaseModelClauseArray allAssignments;
    00236
    00237                                         // The subset of the variables that can be returned in conflicts.
    00238                                         Mers::Models::Base::BaseModelVariableArray mSearchVariables;
    00239                                 };
    00240                         }
    00241                 }
    00242         }
    00243 }
    00244
    00245 #endif // #if !defined(ISATTester_)
    00246