solver/NormalForm.h
```00001 /*
00002  * NormalForm.h
00003  *
00004  *  Created on: Sep 2, 2008
00005  *      Author: tdillig
00006  */
00007
00008 #ifndef NORMALFORM_H_
00009 #define NORMALFORM_H_
00010
00011 #include <set>
00012 #include <map>
00013 #include <string>
00014 using namespace std;
00015 #include "EqLeaf.h"
00016 #include "ILPLeaf.h"
00017 #include "CNode.h"
00018 #include "Leaf.h"
00019 #include "QuantifiedLeaf.h"
00020 #include "Clause.h"
00021 class Leaf;
00022 class VarMap;
00023 class Connective;
00024 class NodeMap;
00025
00026 #include <iostream>
00027 using namespace std;
00028
00029
00030
00031 /*
00032  * Normal form can be used to convert constraints to
00033  * DNF or CNF. The constructor assumes negations have been
00034  * pushed in.
00035  *
00036  * To efficiently simplify the formulas while converting to
00037  * normal form, leaves need to be shared. This is because to
00038  * check contradictions and tautologies, we keep leaves in two different
00039  * sets neg_leaf and pos_leaf according to their phase and
00040  * check for set intersection. If the set intersection is non-empty
00041  * we can detect contradictions (in DNF) and tautologies (in CNF).
00042  * Having a shared leaf representation is crucial for
00043  * detecting contradictions and tautologies efficiently
00044  * without resorting to deep equality checks.
00045  *
00046  * In addition, we check whether any of the outer clauses subsume
00047  * one another to avoid entire redundant clauses.
00048  */
00049 class NormalForm {
00050 private:
00051         set<Clause* >* clauses;
00052         bool is_dnf; // cnf if false
00053 public:
00054
00055         /*
00056          * The constructor assumes negations have been pushed in.
00057          */
00058         NormalForm(CNode* n, bool is_dnf);
00059         set<Clause* >* get_clauses();
00060         string to_string(VarMap& vm);
00061
00062         /*
00063          * Returns a fresh constraint from the normal form
00064          * representation -- Must be deleted by whoever
00065          * captures its return value.
00066          */
00067         CNode* get_constraint();
00068         static CNode* get_constraint_from_clause(Clause *c, bool use_and);
00069         virtual ~NormalForm();
00070 private:
00071         set<Clause* >* make_normal_form(CNode* n);
00072         bool is_outer_connective(cnode_type kind);
00073         Clause* combine_clauses(Clause* clause1, Clause* clause2);
00074         set<Clause* >* product_clauses(set<Clause* >* nf1,
00075                         set<Clause* >* nf2);
00076         void delete_nf(set<Clause*>* nf);
00077         set<Clause* >* add_clauses(set<Clause* >* nf1,
00078                         set<Clause*>* nf2);
00079         void remove_redundant_clauses(set<Clause*>* clauses);
00080
00081 };
00082
00083 #endif /* NORMALFORM_H_ */
```