cnode/BooleanVar.h Source File

00001 /*
00002  * BooleanVar.h
00003  *
00004  *  Created on: Jul 25, 2009
00005  *      Author: tdillig
00006  */
00007 
00008 #ifndef BOOLEANVAR_H_
00009 #define BOOLEANVAR_H_
00010 
00011 #include "Leaf.h"
00012 
00013 class EqLeaf;
00014 
00015 class BooleanVar: public Leaf {
00016         friend class CNode;
00017         friend class boost::serialization::access;
00018 private:
00019         unsigned int id;
00020         static unsigned int next_id;
00021         static map<unsigned int, string> names;
00022         static map<string, unsigned int> names_rev;
00023 
00024         template<class Archive>
00025         void save(Archive & ar, const unsigned int version) const
00026         {
00027                 ar & boost::serialization::base_object<CNode>(*this);
00028                 string name = "";
00029                 if(names.count(id) > 0)
00030                         name = names[id];
00031                 ar & name;
00032 
00033         }
00034         template<class Archive>
00035         void load(Archive & ar, const unsigned int version)
00036         {
00037                 ar & boost::serialization::base_object<CNode>(*this);
00038                 string name;
00039                 ar & name;
00040                 if(name != "")
00041                 {
00042                         if(names_rev.count(name) > 0)
00043                         {
00044                                 id = names_rev[name];
00045                                 //recompute hash code since id changed
00046                                 this->hash_c = 30673 + 7*id;
00047                         }
00048 
00049                         else
00050                         {
00051                                 names[id] = name;
00052                                 names_rev[name] = id;
00053 
00054                         }
00055 
00056                 }
00057 
00058         }
00059         BOOST_SERIALIZATION_SPLIT_MEMBER()
00060 protected:
00061         BooleanVar();
00062         BooleanVar(const string & name);
00063         virtual ~BooleanVar();
00064         static void clear();
00065 public:
00066         static BooleanVar* make();
00067         static BooleanVar* make(const string & name);
00068         unsigned int get_id() const;
00069         virtual bool operator==(const CNode& other);
00070         virtual string to_string();
00071         string get_name();
00072         virtual CNode* substitute(map<Term*, Term*>& subs);
00073 
00074         /*
00075          * Translates boolean var x to x=1, and !x to x!=1.
00076          */
00077         EqLeaf* to_eqleaf() const;
00078 
00079 };
00080 
00081 #endif /* BOOLEANVAR_H_ */