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