- void infer_predicates(FuncInst * next_inst, ModelAction * next_act, HashTable<void *, ModelAction *, uintptr_t, 0> * loc_act_map, 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);
+ /* Map a FuncInst to the its predicate when updating predicate trees */
+ HashTable<FuncInst *, Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> inst_pred_map;
+
+ /* Number FuncInsts to detect loops when updating predicate trees */
+ HashTable<FuncInst *, uint32_t, uintptr_t, 0, model_malloc, model_calloc, model_free> inst_id_map;
+
+ /* Delect read actions at the same locations when updating predicate trees */
+ HashTable<void *, ModelAction *, uintptr_t, 0, model_malloc, model_calloc, model_free> loc_act_map;
+
+ 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);