cnode/Connective.h
00001 /*
00002  * Connective.h
00003  *
00004  *  Created on: Sep 1, 2008
00005  *      Author: tdillig
00006  */
00007 
00008 #ifndef CONNECTIVE_H_
00009 #define CONNECTIVE_H_
00010 #include "CNode.h"
00011 #include <vector>
00012 #include <string>
00013 #include <set>
00014 #include <boost/serialization/set.hpp>
00015 using namespace std;
00016 
00017 class VarMap;
00018 
00019 class Connective: public CNode {
00020         friend class ILPLeaf;
00021         friend class CNode;
00022         friend class boost::serialization::access;
00023         template<class Archive>
00024         void save(Archive & ar, const unsigned int version) const
00025         {
00026                 ar & boost::serialization::base_object<CNode>(*this);
00027                 ar & operands;
00028                 ar & size;
00029         }
00030         template<class Archive>
00031         void load(Archive & ar, const unsigned int version)
00032         {
00033                 ar & boost::serialization::base_object<CNode>(*this);
00034                 ar & operands;
00035                 ar & size;
00036                 compute_hash_code();
00037         }
00038         BOOST_SERIALIZATION_SPLIT_MEMBER()
00039 private:
00040 
00041         set<CNode*> operands;
00042         int size; //for caching result of get_size()
00043 
00044 
00045 
00046 private:
00047         Connective(){}
00048         Connective(cnode_type connective_type, const set<CNode*>& ops);
00049         Connective(CNode* op); // for the not case
00050         virtual ~Connective();
00051         static CNode* _make_and(const set<CNode*>& ops, bool simplify = true);
00052 
00053 public:
00054         inline static CNode* make_and(const set<CNode*>& ops, bool simplify = true)
00055         {
00056                 return _make_and(ops, simplify);
00057         }
00058 
00059         static CNode* make_or(const set<CNode*>& ops, bool simplify = true);
00060         static CNode* make_implies(CNode* p, CNode* a); // p=> a
00061         static CNode* make_not(CNode* op);
00062         static CNode* make(cnode_type connective_type, const set<CNode*>& ops);
00063         static CNode* make(cnode_type connective_type, CNode* op1, CNode* op2);
00064         virtual bool operator==(const CNode& other);
00065         virtual string to_string();
00066         const set<CNode*>& get_operands();
00067         virtual CNode* substitute(map<Term*, Term*>& subs);
00068 
00069 
00070 private:
00071         string connective_to_string();
00072         void compute_hash_code();
00073 
00074 
00075 
00076 };
00077 
00078 
00079 #endif /* CONNECTIVE_H_ */