- /* Store action_lists when calls to update_tree are deferred */
- SnapList<action_list_t *> * action_list_buffer;
+ /* Detect read actions at the same locations when updating predicate trees */
+ ModelVector< ModelVector<loc_inst_map_t *> *> thrd_loc_inst_maps;
+
+ void init_local_maps(thread_id_t tid);
+ void reset_local_maps(thread_id_t tid);
+
+ void update_inst_tree(func_inst_list_t * inst_list);
+ void update_predicate_tree(ModelAction * act);
+ bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, Predicate ** unset_predicate);
+
+ void infer_predicates(FuncInst * next_inst, ModelAction * next_act, SnapVector<struct half_pred_expr *> * half_pred_expressions);
+ void generate_predicates(Predicate * curr_pred, FuncInst * next_inst, SnapVector<struct half_pred_expr *> * half_pred_expressions);
+ bool amend_predicate_expr(Predicate * curr_pred, FuncInst * next_inst, ModelAction * next_act);