solver/ClauseSolve.h
00001 /*
00002  * ClauseSolve.h
00003  *
00004  *  Created on: Feb 8, 2009
00005  *      Author: tdillig
00006  */
00007 
00008 #ifndef CLAUSESOLVE_H_
00009 #define CLAUSESOLVE_H_
00010 
00011 #include <set>
00012 #include <vector>
00013 #include <map>
00014 #include <list>
00015 using namespace std;
00016 #include "InteractionManager.h"
00017 #include "util.h"
00018 #include "bignum.h"
00019 
00020 
00021 
00022 class CNode;
00023 class VarMap;
00024 class NormalForm;
00025 class Clause;
00026 class Term;
00027 class ILPLeaf;
00028 class EqLeaf;
00029 class Leaf;
00030 class FunctionTerm;
00031 class Matrix;
00032 class Equation;
00033 class Solver;
00034 class ModLeaf;
00035 
00036 #include "bignum.h"
00037 #include "SatValue.h"
00038 
00039 
00040 
00041 
00042 class ClauseSolve {
00043          friend class InteractionManager;
00044          friend class QueryComparator;
00045          friend class VariableEliminator;
00046          friend class EqualityFinder;
00047 
00048 private:
00049         bool repeated_solve;
00050 
00051         bool sat;
00052         Clause* cl;
00053         map<Term*, SatValue>* assignments;
00054 
00055         map<Term*, bignum> ilp_assignments;
00056 
00057 
00058         /*
00059          * All members in an equivalence class, indexed by the representative.
00060          */
00061         map<Term*, set<Term*> >  eq_members;
00062 
00063         /*
00064          * Tracks size of each equivalence class; used for
00065          *  deciding which representative to pick
00066          */
00067         map<Term*, int> eq_size;
00068 
00069         /*
00070          * Tracks the constant in each eqv class, if any.
00071          *  This is used to detect contradictions during union.
00072          */
00073         map<Term*, int> eq_class_const;
00074 
00075         /*
00076          * Used for propagating equalities during union
00077          */
00078         map<Term*, set<Term*> > eq_parents;
00079 
00080         /*
00081          * Mapping from variables to their columns in the matrix
00082          */
00083         map<int, int>  var_to_col_map;
00084 
00085         /*
00086          * Names of the ilp variables
00087          */
00088         vector<string> vars;
00089 
00090         /*
00091          * Set of id's of ILP variables
00092          */
00093         set<int> ilp_vars;
00094 
00095         /*
00096          * Set of variables that appear inside a function symbol.
00097          */
00098         set<int> function_vars;
00099 
00100         /*
00101          * Matrix representing the ilp constraints
00102          */
00103         Matrix* m;
00104 
00105         /*
00106          * A set of disjunctive ILP disequalities ( { {<a, b>, <c, d>}, {e,f} }
00107          * means (a!=b | c!= d) & (e!=f).
00108          */
00109         set< set< pair<Equation*, bignum> > > neq_constraints;
00110 
00111 
00112 
00113         /*
00114          * The top level terms in the original clause (before denesting).
00115          * This ivar is only initialized if assignments is non-null because
00116          * it is only used for generating satisfying assignments.
00117          * For us, a top level term either occurs inside an arithmetic expression or
00118          * does not have parent terms.
00119          */
00120         set<Term*> top_level_terms;
00121 
00122         /*
00123          * This map is only filled if assignments is non-null.
00124          */
00125         map<Term*, Term*> denestings;
00126 
00127         /*
00128          * A set of all constants
00129          */
00130         set<Term*> constants;
00131 
00132 
00133 
00134         /*
00135          * An auxiliary struct to help us undo a conditional union operation.
00136          * - old_rep denotes a term that was a representative, but that became
00137          * a non-representative during this undo operation.
00138          * - eq_members is the set of elements in old_rep's equivalence class
00139          * before this union operation.
00140          * - has_constant/constant denote whether this congruence class had
00141          * a constant before the union operation, and if so what this constant is.
00142          * NOTE: Although the maps eq_size and eq_parents are updated during
00143          * a normal union operation, they are not updated during a conditional
00144          * union because both are only necessary for performing multiple union
00145          * operations whereas we assume conditional unions are performed once and
00146          * then immediately undone.
00147          *
00148          */
00149         struct history_elem {
00150                 Term* old_rep;
00151                 set<Term*>* eq_members;
00152                 bool has_constant;
00153                 int constant;
00154 
00155                 history_elem(Term* old_rep, set<Term*>& eq_members):old_rep(old_rep),
00156                                 eq_members(&eq_members)
00157                 {
00158 
00159                 }
00160 
00161         };
00162 
00163         /*
00164          * This is used for undo'ing a single conditional union.
00165          */
00166         vector< history_elem > undo_buffer;
00167 
00168         /*
00169          * STATS
00170          */
00171         int time_denesting;
00172         int time_initial_ilp;
00173         int time_initial_union_find;
00174         int time_total_ilp;
00175         int time_total_union_find;
00176         int time_preparing_queries;
00177         int start;
00178         int num_interaction_queries;
00179 
00180 
00181 
00182 public:
00183         ClauseSolve(CNode* node, map<Term*, SatValue>* assignments = NULL);
00184         ClauseSolve(Clause* clause,  map<Term*, SatValue>* assignments = NULL);
00185         ~ClauseSolve();
00186         bool is_sat();
00187         void print_stats();
00188 
00189 
00190 
00191 private:
00192         bool solve(CNode* node);
00193         bool clause_sat();
00194         void init_congruence_classes_term(Term *t, Term* parent,
00195                  set<Term*> & cur_parents, set<int> & function_ids);
00196         void init_congruence_classes(set<int> & function_ids,
00197                         set<Term*> & eq_terms);
00198         void clear_ilp_representatives(set<ILPLeaf*> & leaves);
00199         void clear_mod_representatives(set<ModLeaf*> & leaves);
00200         //bool minimize_shared_ilp_vars(set<ILPLeaf*>& ilp_leaves, bool pos,
00201         //              set<int>& function_terms, set<Term*> &eq_terms);
00202         //bool minimize_shared_mod_vars(set<ModLeaf*>& mod_leaves, bool pos);
00203         bool process_equalities();
00204         bool perform_union(Term* t1, Term* t2);
00205         Term* find_representative(Term* t);
00206         bool congruent(FunctionTerm* f1, FunctionTerm* f2);
00207         string terms_to_string(set<Term*>& eq_class );
00208         bool have_contradictory_constants(Term* rep1, Term* rep2);
00209         bool has_contradiction();
00210 
00211         /*
00212          * Perform conditional union supports the ability to undo the union by
00213          * keeping some scratch state around. However, only the representative
00214          * fields and eq_members maps are updated while performing the union
00215          * because it is assumed that the union will be undone.
00216          * changed_eq_classes contains the representatives of the congruence classes
00217          * changed by the union.
00218          */
00219         bool perform_conditional_union(Term* t1, Term* t2,
00220                         set<Term*>& changed_eq_classes, bool& used_function_axiom);
00221         void undo_conditional_union();
00222 
00223         void compute_ilp_var_ids();
00224         void build_var_to_col_map();
00225         void construct_ilp_matrix();
00226         void populate_matrix_row(ILPLeaf* l, bool sign);
00227         bool add_inequality(set<pair<Term*, Term*> > disjunctive_ineq,
00228                         set< pair<Equation*, bignum> > & new_inequality);
00229         void add_inequality(ILPLeaf* ilp);
00230         void generate_sat_assignment(vector<bignum>* ilp_assignments);
00231         void add_equality(Term* t1, Term* t2);
00232         void print_neq_matrix();
00233         void add_ilp_vars_in_mod_leaf(ModLeaf* ml, bool pos, int counter);
00234         void convert_mod(ModLeaf* ml, bool pos, int counter);
00235         inline void add_ilp_to_matrix(ILPLeaf* ilp);
00236         inline void init_top_level_terms();
00237         inline void init_top_level_terms_eq(set<EqLeaf*>& eq_leaves);
00238         inline void init_top_level_terms_ilp(set<ILPLeaf*>& ilp_leaves);
00239         inline void init_top_level_terms_mod(set<ModLeaf*>& mod_leaves);
00240         void init_top_level_terms_term(Term* t);
00241         void print_congruence_classes();
00242         void clear();
00243         void get_ilp_assignment(vector<bignum>& ilp_assign);
00244         void init(set<VariableTerm*>& vars );
00245 
00246         /*
00247          * Checks whether the given ilp assignments cause any contradiction
00248          * in the eq domain. If they don't, we are done.
00249          */
00250         bool check_assignment();
00251 
00252         void print_eq_classes();
00253         string eq_classes_to_string();
00254 
00255         void init_stats();
00256 
00257         //bool minimize_shared_variables(set<int> & function_terms, set<Term*> &eq_terms);
00258 
00259 
00260 };
00261 
00262 #endif /* CLAUSESOLVE_H_ */