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