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

# /Users/fpy/titan-1-5-MBARI/Mers/Models/Base/Utils/MutualExclusionAndExhaustion.h

    00001 //=============================================================================
    00002 //MutualExclusionAndExhaustion.h: interface for the
    00003 //MutualExclusionAndExhaustion class.
    00004 //
    00005 // Copyright (c) 2003           Model-based Embedded and Robotic Systems Group
    00006 // All Rights Reserved          Massachusetts Institute of Technology
    00007 //
    00008 // This software is provided as is. Model-based Embedded and Robotic Systems
    00009 // (MERS) group does not assume any responsibility.
    00010 //
    00011 // Author:                      Paul Elliott
    00012 // Organization:        Model-based Embedded and Robotic Systems Group
    00013 //                                      Massachusetts Institute of Technology
    00014 //
    00015 // Basic class for adding and removing mutual exclusion and exhaustion
    00016 // clauses from a theory.  This class operates on a BaseModelClause.
    00017 //
    00018 // Mutual exclusion clauses, for a variable v with domain (d1, d2,
    00019 // .. dn) are of the form (!(v = d1) or !(v = d2)) and (!(v = d1) or
    00020 // !(v = d3)) and .. (!(v = d1) or !(v = dn)) and .. (!(v = d2) or !(v
    00021 // = d3)) and ... (!(v = dn-1) or !(v = dn)).  So n^2 / 2 terms for a
    00022 // domain of size n.  This constraint states that there cannot be more
    00023 // than one assignment to v.
    00024 //
    00025 // An Exhaustion clause is of the form ((v = d1) or (v = d2) or (v =
    00026 // d3) or .. (v = dn)).  This constraint says that there must be at
    00027 // least one assignment to v.
    00028 //
    00029 // Combined, these state that there must be exactly one assignment to
    00030 // each variable v.
    00031 //
    00032 // Traditional SAT engines require these clauses because they only
    00033 // work with literals, such as (v = d3), and this can either be true
    00034 // or false.
    00035 //
    00036 // However, some of the SAT engines know that the variable v has the
    00037 // domain d, and so knows that (v = d3) really means "v is assigned
    00038 // d3", so the mutual exclusion and exhaustion clauses are redundant,
    00039 // if not harmfull.
    00040 //
    00041 //=============================================================================
    00042
    00043 #ifndef MUTUALEXCLUSIONANDEXHAUSTION_HEADER_FILE
    00044 #define MUTUALEXCLUSIONANDEXHAUSTION_HEADER_FILE
    00045
    00046 class BaseModelVariableArray;
    00047 class BaseModelSentence;
    00048
    00055 class MutualExclusionAndExhaustion
    00056 {
    00057 public:
    00058         //-----------------------------------------
    00059         // Constructors
    00060         //-----------------------------------------
    00061
    00065         MutualExclusionAndExhaustion();
    00066
    00067         //-----------------------------------------
    00068         // Copy constructors
    00069         //-----------------------------------------
    00070
    00075         MutualExclusionAndExhaustion(MutualExclusionAndExhaustion const &other);
    00076
    00077         //-----------------------------------------
    00078         // Destructors
    00079         //-----------------------------------------
    00080
    00084         MutualExclusionAndExhaustion();
    00085
    00086         //-----------------------------------------
    00087         // Functions
    00088         //-----------------------------------------
    00089
    00100         static int removeMEE(BaseModelSentence &theory);
    00101
    00113         static int addMEE(BaseModelSentence &theory);
    00114
    00129         static int addMEE(BaseModelVariableArray const &variables,
    00130                 BaseModelSentence &theory);
    00131
    00132 };
    00133
    00134 #endif