solver/VariableEliminator.h
00001 /*
00002  * VariableEliminator.h
00003  *
00004  *  Created on: Feb 8, 2009
00005  *      Author: tdillig
00006  */
00007 
00008 #ifndef VARIABLEELIMINATOR_H_
00009 #define VARIABLEELIMINATOR_H_
00010 
00011 #include <vector>
00012 #include <set>
00013 #include <map>
00014 #include "Solver.h"
00015 using namespace std;
00016 class CNode;
00017 class Term;
00018 class FunctionTerm;
00019 class Clause;
00020 class VariableTerm;
00021 class EqLeaf;
00022 class ModLeaf;
00023 
00024 /*
00025  * Eliminates existentially quantified variables.
00026  */
00027 class VariableEliminator:public Solver {
00028 private:
00029 
00030         int fresh_var_counter;
00031         bool over_approximate;
00032         bool track_new_inequalities;
00033 
00034         /*
00035          * Is it (potentially) necessary to simplify the constraint
00036          * after we eliminated a variable?
00037          */
00038         bool simplify;
00039 
00040         bool large_lcm;
00041 
00042         CNode* orig_c;
00043 
00044         /*
00045          * A mapping from the var id to be eliminated to the set of pairs
00046          * that this var is "sandwiched" between when applying Cooper's method.
00047          * This is used by the EqualityFinder to find inferred
00048          * equalities in the ILP domain.
00049          */
00050         map<VariableTerm*, set<pair<Term*, Term*> > > new_inequality_terms;
00051 
00052 public:
00053         VariableEliminator(CNode *n, vector<VariableTerm*> & to_eliminate,
00054                         simplification_level level,
00055                         bool over_approximate, bool track_new_inequalities = false);
00056         VariableEliminator(CNode *n, VariableTerm* to_eliminate,
00057                         simplification_level level,
00058                         bool over_approximate, bool track_new_inequalities = false);
00059 
00060 
00061         const map<VariableTerm*, set<pair<Term*, Term*> > > & get_new_inequalities();
00062 
00063         virtual ~VariableEliminator();
00064 private:
00065         CNode* eliminate_var(CNode* node, VariableTerm* var);
00066         CNode* eliminate_var_rec(CNode* node, VariableTerm* var, CNode* active_constraint);
00067         CNode* eliminate_var_conjunct(CNode* node, VariableTerm* var);
00068         void get_direct_parents(Term* t, set<FunctionTerm*>& parents,
00069                         map<Term*, set<Term*> >& eq_members);
00070 
00071         /*
00072          * Used for existential variable elimination. If x is a term to be
00073          * eliminated and has no members in its equivalence class, replace all
00074          * function terms it appears in with a fresh variable term.
00075          */
00076         void introduce_fresh_vars_for_function_terms(Clause& cl,
00077                 VariableTerm* elim_t,
00078                 set<FunctionTerm*>& direct_parents,
00079                 map<VariableTerm*, FunctionTerm*>& fresh_vars_to_functions,
00080                 map<FunctionTerm*, VariableTerm*>& functions_to_fresh_vars,
00081                 map<int, set<FunctionTerm*> >& function_id_to_functions);
00082 
00083         VariableTerm* introduce_fresh_var_for_function_term(Clause& cl,
00084                 VariableTerm* elim_term, FunctionTerm* ft,
00085                 map<VariableTerm*, FunctionTerm*>& fresh_vars_to_functions,
00086                 map<FunctionTerm*, VariableTerm*>& functions_to_fresh_vars,
00087                 map<int, set<FunctionTerm*> >& function_id_to_functions);
00088 
00089         void replace_function_with_freshvar_in_clause(Clause& cl, FunctionTerm* ft,
00090                         VariableTerm* fresh_var);
00091 
00092         CNode* replace_function_with_freshvar_in_leaf(EqLeaf* eq, FunctionTerm* ft,
00093                         VariableTerm* fresh_var);
00094         void get_function_terms_in_clause(Clause& cl, map<int, set<FunctionTerm*> >&
00095                         functions_in_clause);
00096 
00097         CNode* eliminate_var_from_ilp_domain(Clause& cl, VariableTerm* evar, set<CNode*>&
00098                         mod_constraints);
00099         ILPLeaf* find_ilp_equality_with_evar(Clause& cl, VariableTerm* evar_id);
00100         Term* get_ilp_substitution(ILPLeaf* eq_ilp, Term* evar );
00101         void apply_ilp_substitution(Clause& cl, Term* evar, Term* sub, long int coef);
00102         CNode* apply_ilp_substitution(ILPLeaf* ilp, Term* evar, Term* sub,
00103                         long int coef);
00104         void separate_equations_by_sign(Clause& cl, Term* evar,
00105                         set<ILPLeaf*>& positive, set<ILPLeaf*>& negative);
00106         void get_neq_equations_with_evar(Clause& cl, Term* evar, set<Leaf*> & neqs);
00107         CNode* expand_neq_constraints(Clause& cl, set<Leaf*>& neqs);
00108         bool expand_neq_constraints_with_bound(Clause& cl, set<Leaf*>& neqs,
00109                         set<ILPLeaf*>& result, Term* evar, bool lt);
00110 
00111         bool contains_related_var(set<Leaf*> neq, VariableTerm* evar_id);
00112         CNode* apply_cooper(Clause& cl, Term* evar, set<ILPLeaf*>& positive,
00113                         set<ILPLeaf*>& negative);
00114         CNode* eliminate_denestings(CNode* node, map<Term*, Term*>& denestings,
00115                         VariableTerm* evar_id, int initial_count, bool include_evar);
00116         CNode* eliminate_mod_temps(CNode* node, set<VariableTerm*>& to_eliminate);
00117 
00118         void update_denestings(map<Term*, Term*>& denestings, map<Term*, Term*>&
00119                         substitutions);
00120         CNode* remove_eq_var_with_no_parents(Clause& cl, VariableTerm* evar);
00121 
00122         /*
00123          * Checks if the evar is only contained in a single
00124          * mod leaf. If this is the case, returns this mod constraint,
00125          * otherwise null.
00126          */
00127         ModLeaf* find_single_mod_constraint(Clause& cl, VariableTerm* evar);
00128 
00129         inline void add_new_inequality(Term* t, ILPLeaf* t1, ILPLeaf* t2);
00130 
00131 
00132 
00133 
00134 
00135 };
00136 
00137 #endif /* VARIABLEELIMINATOR_H_ */