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 {
00019 public:
00020
00021 friend class conaux;
00022
00028 friend std::ostream &operator<<(std::ostream &os, const con_type &con);
00029
00035 con_type(bool val = true);
00036
00042 con_type(const std::string &var);
00043
00050 con_type operator&(const con_type &rhs) const;
00051
00058 con_type operator|(const con_type &rhs) const;
00059
00066 con_type operator^(const con_type &rhs) const;
00067
00073 con_type operator!() const;
00074
00079 bool is_false() const;
00080
00085 bool is_true() const;
00086
00091 void project(const std::set<std::string> &to_keep);
00092
00098 std::set<std::string> get_cvars();
00099
00100 private:
00101
00105 bdd constraint;
00106
00110 std::set<std::string> cvars;
00111 };
00112
00117 class conaux
00118 {
00119 public:
00120
00124 class sat_exception: public std::exception {};
00125
00130 static void init(const std::string &constraint_settings);
00131
00136 static void finalise();
00137
00143 static bdd get_variable(const std::string &name);
00144
00150 static std::string get_varname(const int num);
00151
00157 static con_type resolve_sat(const class c_term *t);
00158
00165 static con_type build_tree(const class c_term *term, std::set<std::string> &cvars);
00166
00172 static void allsathandler(char *varset, int size);
00173
00180 static void reindex(con_type &con);
00181
00188 static con_type relate(const std::string &var1, const std::string &var2);
00189
00194 static void report_answer(const con_type &con);
00195
00203 static bool subsumes(const con_type &large, const con_type &small);
00204
00205 private:
00206
00210 static int max_var_amount;
00211
00215 static std::map<std::string, bdd> varmap;
00216
00220 static std::vector<std::string> varnames;
00221 };
00222
00223 #endif // CONSTRAINT_H