00001 #ifndef CONSTRAINT_H
00002 #define CONSTRAINT_H
00003
00004 #include <map>
00005 #include <vector>
00006 #include <set>
00007 #include <string>
00008 #include <sstream>
00009
00010 #include <bdd.h>
00011
00017 class con_type
00018 {
00024 friend std::ostream &operator<<(std::ostream &os, const con_type &con);
00025
00031 con_type(bool val = true);
00032
00038 con_type(const std::string &var);
00039
00046 con_type operator&(const con_type &rhs) const;
00047
00054 con_type operator|(const con_type &rhs) const;
00055
00062 con_type operator^(const con_type &rhs) const;
00063
00069 con_type operator!() const;
00070
00075 bool is_false() const;
00076
00081 bool is_true() const;
00082
00087 void project(const std::set<std::string> &to_keep);
00088
00092 bdd constraint;
00093
00097 std::set<std::string> cvars;
00098 };
00099
00104 class conaux
00105 {
00109 class sat_exception: public exception {};
00110
00115 static void init(const std::string &constraint_settings);
00116
00121 static void finalise();
00122
00128 static bdd get_variable(const std::string &name);
00129
00135 static std::string get_varname(const int num);
00136
00142 static con_type resolve_sat(const class c_term *t);
00143
00150 static con_type build_tree(const class c_term *term, std::set<std::string> &cvars);
00151
00157 static void allsathandler(char *varset, int size);
00158
00165 static void reindex(con_type &con);
00166
00173 static con_type relate(const string &var1, const string &var2);
00174
00179 static void report_answer(const con_type &con);
00180
00188 static bool subsumes(const con_type &large, const con_type &small);
00189
00190 private:
00191
00195 static int max_var_amount;
00196
00200 static map<string, bdd> varmap;
00201
00205 static vector<string> varnames;
00206 };
00207
00208 #endif // CONSTRAINT_H