Main Page | Namespace List | Class Hierarchy | Alphabetical List | Class List | File List | Class Members | File Members

constraint.h

Go to the documentation of this file.
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

Generated on Wed Feb 16 20:53:35 2005 for Fixpoint Engine by  doxygen 1.3.9.1