solver/CNF.h
00001 /*
00002  * CNF.h
00003  *
00004  *  Created on: Jul 25, 2009
00005  *      Author: tdillig
00006  */
00007 
00008 #ifndef CNF_H_
00009 #define CNF_H_
00010 
00011 #include "SatSolver.h"
00012 #include "Vec.h"
00013 #include <set>
00014 #include <map>
00015 #include <string>
00016 
00017 class CNode;
00018 class Leaf;
00019 
00020 using namespace std;
00021 
00022 class CNF {
00023 private:
00024         set<vec<minisat::Lit>* >  cnf;
00025         map<CNode*, minisat::Var> node_to_var_map;
00026         map<minisat::Var, CNode*> var_to_node_map;
00027 
00028 public:
00029         CNF(CNode* node, minisat::Solver& s);
00030         ~CNF();
00031         vec<minisat::Lit>* add_clause(CNode* clause, minisat::Solver& s);
00032         void and_cnf(CNF& other);
00033         string to_string();
00034         set<vec<minisat::Lit>* > & get_cnf();
00035         Leaf* get_leaf_from_literal(minisat::Var l);
00036         void and_node(CNode* node, minisat::Solver& s);
00037         map<minisat::Var, CNode*>& get_var_to_node_map();
00038 private:
00039         minisat::Lit make_cnf_rec(minisat::Solver& s,
00040                         CNode* node,  bool insert_literal);
00041 
00042 
00043 };
00044 
00045 #endif /* CNF_H_ */