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

constraint.hpp

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 {
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

Generated on Mon Mar 21 00:07:37 2005 for Fixpoint Engine by  doxygen 1.3.9.1