1 #ifndef __INC_PROP_H_ 2 #define __INC_PROP_H_ 3 4 #include <utility> 5 6 #include <chuffed/core/propagator.h> 7 #include <chuffed/vars/int-view.h> 8 #include <chuffed/support/misc.h> 9 #include <chuffed/support/sparse_set.h> 10 #include <climits> 11 12 #include <chuffed/mdd/opts.h> 13 14 #include <chuffed/mdd/MDD.h> 15 16 #ifdef FULLPROP 17 #undef USE_WATCHES 18 #endif 19 20 #ifdef USE_WATCHES 21 //#define VAL_DEAD(val) (val_entries[(val)].count == 0 || edges[val_edges[val_entries[(val)].first_off]].kill_flags) 22 #define VAL_DEAD(val) (edges[val_edges[val_entries[(val)].first_off]].kill_flags) 23 #else 24 #define VAL_DEAD(val) (val_entries[(val)].supp_count == 0) 25 #endif 26 27 typedef int Value; 28 29 typedef struct i_edge { 30 Value val; 31 unsigned int kill_flags; 32 char watch_flags; 33 int begin; 34 int end; 35 } inc_edge; 36 37 typedef struct { 38 int var; 39 40 int in_start; 41 int num_in; 42 int out_start; 43 int num_out; 44 #ifndef USE_WATCHES 45 int count_in; 46 int count_out; 47 #endif 48 49 unsigned char stat_flag; 50 unsigned int kill_flag; 51 } inc_node; 52 53 typedef struct { 54 int var; 55 int val; 56 int first_off; 57 int count; 58 int val_lim; 59 #ifndef USE_WATCHES 60 int supp_count; 61 #endif 62 // unsigned char stat_flag; 63 signed char stat_flag; 64 int* search_cache; 65 } val_entry; 66 67 class MDDTemplate { 68 public: 69 70 MDDTemplate(MDDTable& tab, _MDD root, vec<int>& domain_sizes); 71 getDoms()72 vec<int>& getDoms() { return _doms; } 73 74 // Instrumentation 75 uint64_t explncount; 76 uint64_t nodecount; 77 78 // MDD hack stuff 79 vec<int> _doms; 80 vec<val_entry> _val_entries; 81 vec<inc_node> _mdd_nodes; 82 83 vec<int> _val_edges; 84 vec<int> _node_edges; 85 vec<inc_edge> _edges; 86 }; 87 88 template<int U = 0> 89 class MDDProp : public Propagator { 90 public: 91 MDDProp(MDDTemplate*, vec< IntView<U> >& _vars, const MDDOpts& opts); 92 93 bool fullProp(void); 94 unsigned char fullPropRec(int node, int timestamp); 95 96 void genReason(vec<int>& out, Value value); 97 98 void shrinkReason(vec<int>& reason, Value value, int threshold = 2); 99 100 void incConstructReason(unsigned int lim, vec<int>& out, Value val, int threshold = 2); 101 // void incConstructReason(unsigned int lim, vec<int>& out, Value val, int threshold = INT_MAX); 102 103 void fullConstructReason(int lim, vec<int>& out, Value val); 104 unsigned char mark_frontier(int node_id, int var, Value val, int lim); 105 unsigned char mark_frontier_total(int var, Value val, int lim); 106 // void retrieveReason(vec<int>& out,int var, int val, int lim, int threshold = INT_MAX); 107 void retrieveReason(vec<int>& out,int var, int val, int lim, int threshold = 2); 108 109 void static_inference(vec<int>& out); 110 void static_inference(vec<Lit>& out); 111 numNodes(void)112 inline int numNodes(void) { return nodes.size(); } 113 114 void debugStateTikz(unsigned int lim, bool debug = true); 115 void verify(void); 116 117 // Wake up only parts relevant to this event wakeup(int i,int c)118 void wakeup(int i, int c) { 119 assert( boolvars[i].isFixed() ); 120 if( boolvars[i].getVal() ) 121 { 122 assert( 0 ); 123 } else { 124 if( fixedvars.elem(i) ) 125 return; 126 clear_queue.push(i); 127 val_entries[i].val_lim = fixedvars.size(); 128 fixedvars.insert(i); 129 pushInQueue(); 130 } 131 } 132 133 // Propagate woken up parts 134 bool propagate(); 135 get_val_lit(int v)136 inline Lit get_val_lit(int v) 137 { 138 #ifndef WEAKNOGOOD 139 return intvars[val_entries[v].var].getLit(val_entries[v].val,1); 140 #else 141 int eval = v < 0 ? -1*(v+2) : v; 142 return intvars[val_entries[eval].var].getLit(val_entries[eval].val, v < 0 ? 0 : 1); 143 #endif 144 } 145 explain(Lit p,int inf)146 Clause* explain(Lit p, int inf) 147 { 148 vec<int> expl; 149 genReason(expl, inf); 150 151 if(opts.expl_strat == MDDOpts::E_KEEP) 152 { 153 vec<Lit> ps(expl.size()); 154 for(int k = 1; k < expl.size(); k++) 155 ps[k] = get_val_lit(expl[k]); 156 ps[0] = p; 157 158 Clause* c = Clause_new(ps, true); 159 c->learnt = true; 160 sat.addClause(*c); 161 return c; 162 } else { 163 Clause* r = Reason_new(expl.size()); 164 for(int k = 1; k < expl.size(); k++) 165 (*r)[k] = get_val_lit(expl[k]); 166 return r; 167 } 168 } 169 170 // Clear intermediate states clearPropState()171 void clearPropState() { 172 clear_queue.clear(); 173 in_queue = false; 174 } 175 176 private: 177 void clear_val(Value v); 178 void kill_dom(unsigned int, inc_edge* e, vec<int>& kfa, vec<int>& kfb); 179 180 // Parameters 181 MDDOpts opts; 182 183 // Data 184 vec< IntView<U> > intvars; 185 vec<BoolView> boolvars; 186 187 vec<val_entry> val_entries; 188 vec<inc_node> nodes; 189 190 vec<int> val_edges; 191 vec<int> node_edges; 192 193 vec<inc_edge> edges; 194 195 double act_decay; 196 double act_inc; 197 vec<double> activity; bumpActivity(int val)198 void bumpActivity(int val) { activity[val] += act_inc; } decayActivity(void)199 void decayActivity(void) { act_inc *= act_decay; } 200 201 bool simple; 202 203 TrailedSet fixedvars; 204 // Intermediate state 205 vec<int> clear_queue; 206 }; 207 208 template<int U> 209 MDDProp<U>* MDDProp_new(MDDTemplate*, vec< IntView<U> >& vars); 210 211 void mdd_decomp_dc(vec<IntVar*> xs, MDDTable& t, _MDD root); 212 #endif 213