solver/UniversalInstantiator.h
00001 /*
00002  * UniversalInstantiator.h
00003  *
00004  *  Created on: Sep 12, 2008
00005  *      Author: tdillig
00006  */
00007 
00008 #ifndef UNIVERSALINSTANTIATOR_H_
00009 #define UNIVERSALINSTANTIATOR_H_
00010 #include <map>
00011 #include <set>
00012 using namespace std;
00013 
00014 class CNode;
00015 class Connective;
00016 class EqLeaf;
00017 class ILPLeaf;
00018 class VarMap;
00019 class Term;
00020 class SubstitutionExpression;
00021 class QuantifiedLeaf;
00022 
00023 /*
00024  * Struct used to reperesent a quantified variable.
00025  * The orig_id is the unique id associated with the whole
00026  * quantifier leaf to differentiate between variables that
00027  * appear in different quantified clauses.
00028  */
00029 struct qvar{
00030         long int id;
00031         int var_id;
00032         bool operator<(const qvar & other) const
00033         {
00034                 if(id!=other.id)
00035                         return id < other.id;
00036                 return var_id<other.var_id;
00037         }
00038 };
00039 // --------------------------------------
00040 
00041 class UniversalInstantiator {
00042 private:
00043         bool *success;
00044         /*
00045          * Used for numbering renamed existentially quantified variables.
00046          */
00047         int cur_varindex;
00048 
00049         /*
00050          * A mapping from a universally quantified variable
00051          * to the function id and argument number in which it appears.
00052          * For instance, Ai. ( ...f(a,i, b)), we would have
00053          * a mapping from i to (f's id, arg# 1).
00054          * Note: A universally quantified variable
00055          * is not allowed to appear as different arguments
00056          * inside a given function.
00057          */
00058         map<qvar, map<int, int>* > fun_arg_universal;
00059         map<pair<int, int>,set<qvar>* > reverse_fun_arg_universal;
00060 
00061         /*
00062          * A mapping from universally quantified variables
00063          * to a set of SubstitutionExpression's it needs
00064          * to be instantiated with.
00065          */
00066         map<qvar, set<Term*>* > index_set;
00067 
00068         /*
00069          * A mapping from SubstituionExpression's to what variables
00070          * they need to be instantiated with. If a subsitution expression
00071          * is a just a variable or constant, the int will be either
00072          * the constant or variable id associated with the constant or variable.
00073          * For complex expressions, this will be the var id for
00074          * some fresh temporary.
00075          */
00076         map<Term*, int> sub_exp_to_var_id;
00077 
00078         /*
00079          * The resulting node after instantiating universals.
00080          */
00081         CNode* new_conn;
00082 
00083 
00084 
00085 public:
00086         /*
00087          * In the constructor, success can be used to indicate a parse
00088          * error in the index guard.
00089          */
00090         UniversalInstantiator(CNode* node, bool * success = NULL);
00091 
00092         /*
00093          * Returns the resulting constraint after instantiating the quantified
00094          * variables. The return value must be deleted by whoever calls this method.
00095          */
00096         CNode* get_constraint();
00097         virtual ~UniversalInstantiator();
00098 private:
00099         CNode* process_clause(CNode* c);
00100         bool contains_quantifier(CNode* c);
00101         bool preprocess_constraint(CNode* c);
00102         CNode* rec_preprocess_constraint(CNode* c, bool phase,
00103                         map<int,int> & var_subs, QuantifiedLeaf* ql);
00104         CNode* process_eq_leaf(EqLeaf* l, map<int,int> & var_subs,
00105                         QuantifiedLeaf* ql);
00106         CNode* process_ilp_leaf(ILPLeaf*l, map<int,int> & var_subs,
00107                         QuantifiedLeaf* ql);
00108         Term* process_term(Term* t, map<int,int> & var_subs, int fun_id,
00109                         int arg_num, QuantifiedLeaf* ql);
00110         bool build_index_set(CNode* clause, set<int> &qvars);
00111         bool build_index_set_index_guard(CNode* c, set<int> &qvars,
00112                         QuantifiedLeaf *ql);
00113         bool build_index_set_term(Term* t, set<int> &qvars, int fun_id, int arg_num);
00114         void delete_fun_arg_universal();
00115         void error();
00116         void add_to_index_set(qvar qv, Term* t);
00117         bool process_eq_leaf_in_index_guard(EqLeaf* eq, set<int> &qvars,
00118                         QuantifiedLeaf* ql);
00119         bool process_ilp_leaf_in_index_guard(ILPLeaf* ilp, set<int> &qvars,
00120                                 QuantifiedLeaf* ql);
00121         void get_equivalence_class(qvar qv, set<qvar>& eq_class);
00122         CNode* instantiate_universals(CNode *c,
00123                         map<int, Term*> & sub_map);
00124         Term* instantiate_term(Term* t,
00125                         map<int, Term*> &sub_map);
00126 
00127 
00128 };
00129 
00130 #endif /* UNIVERSALINSTANTIATOR_H_ */