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