solver/EqualityFinder.h
```00001 /*
00002  * EqualityFinder.h
00003  *
00004  *  Created on: Mar 15, 2009
00005  *      Author: isil
00006  */
00007
00008
00009 #ifndef EQUALITYFINDER_H_
00010 #define EQUALITYFINDER_H_
00011
00012 #include <map>
00013 #include <set>
00014 #include <string>
00015
00016 using namespace std;
00017 class Term;
00018 class CNode;
00019
00020 /*
00021  * Inference of equalities implied by this constraint.
00022  * Currently, we infer only non-disjunctive equalities, but
00023  * we could very easily extend this to return disjunctive equalities as
00024  * well. The inference is sound & complete -- all equalities it finds
00025  * are actually implied and it is guaranteed to find all equalities
00026  * implied by the CNode* node.
00027  */
00028 class EqualityFinder {
00029 private:
00030         set<Term*> equalities;
00031         map<Term*, CNode*> disjunctive_equalities;
00032         CNode* node;
00033         Term* var;
00034         bool disjunctive;
00035         bool no_equality;
00036
00037 public:
00038         EqualityFinder(CNode* node, Term* var, bool find_disjunctive_eqs);
00039         const set<Term*> & get_equalities();
00040         const map<Term*, CNode*>& get_disjunctive_equalities();
00041         ~EqualityFinder();
00042 private:
00043         void find_equalities(CNode* cur, CNode* active_constraint,
00044                         set<Term*>& cur_equalities);
00045         void find_disjunctive_equalities(CNode* cur, CNode* active_constraint,
00046                         map<Term*, CNode*>& cur_equalities);
00047         void find_equalities_conjunct(CNode* c, set<Term*>& cur_eqs);
00048         inline void process_equality_for_disjunct(CNode* disjunct,
00049                         set<Term*>& cur_equalities);
00050         bool implies(CNode* c1, CNode* c2);