+void FuncNode::update_predicate_tree(action_list_t * act_list, HashTable<ModelAction *, FuncInst *, uintptr_t, 4> * act_inst_map)
+{
+ if (act_list == NULL || act_list->size() == 0)
+ return;
+/*
+ if (predicate_tree_initialized) {
+ return;
+ }
+ predicate_tree_initialized = true;
+*/
+ /* map a FuncInst to the parent of its predicate */
+ HashTable<FuncInst *, Predicate *, uintptr_t, 0> inst_pred_map(128);
+ HashTable<void *, ModelAction *, uintptr_t, 0> loc_act_map(128);
+
+ sllnode<ModelAction *> *it = act_list->begin();
+ Predicate * curr_pred = predicate_tree_entry;
+
+ while (it != NULL) {
+ ModelAction * next_act = it->getVal();
+ FuncInst * next_inst = act_inst_map->get(next_act);
+ Predicate * old_pred = curr_pred;
+
+ bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &loc_act_map);
+
+ // check back edges
+ if (!branch_found) {
+ Predicate * back_pred = curr_pred->get_backedge();
+ if (back_pred != NULL) {
+ curr_pred = back_pred;
+ continue;
+ }
+
+ if (inst_pred_map.contains(next_inst)) {
+ back_pred = inst_pred_map.get(next_inst);
+ curr_pred->set_backedge(back_pred);
+ curr_pred = back_pred;
+ continue;
+ }
+ }
+
+ if (!inst_pred_map.contains(next_inst))
+ inst_pred_map.put(next_inst, old_pred);
+
+ if (!branch_found) {
+ if ( loc_act_map.contains(next_act->get_location()) ) {
+ Predicate * new_pred1 = new Predicate(next_inst);
+ new_pred1->add_predicate(EQUALITY, next_act->get_location(), true);
+
+ Predicate * new_pred2 = new Predicate(next_inst);
+ new_pred2->add_predicate(EQUALITY, next_act->get_location(), false);
+
+ curr_pred->add_child(new_pred1);
+ curr_pred->add_child(new_pred2);
+ //new_pred1->add_parent(curr_pred);
+ //new_pred2->add_parent(curr_pred);
+
+ ModelAction * last_act = loc_act_map.get(next_act->get_location());
+ uint64_t last_read = last_act->get_reads_from_value();
+ uint64_t next_read = next_act->get_reads_from_value();
+
+ if ( last_read == next_read )
+ curr_pred = new_pred1;
+ else
+ curr_pred = new_pred2;
+ } else {
+ Predicate * new_pred = new Predicate(next_inst);
+ curr_pred->add_child(new_pred);
+ //new_pred->add_parent(curr_pred);
+
+ curr_pred = new_pred;
+ }
+ }
+
+ loc_act_map.put(next_act->get_location(), next_act);
+ it = it->getNext();
+ }
+
+// model_print("function %s\n", func_name);
+// print_predicate_tree();
+}
+
+/* Given curr_pred and next_inst, find the branch following curr_pred that contains next_inst and the correct predicate
+ * @return true if branch found, false otherwise.
+ */
+bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act,
+ HashTable<void *, ModelAction *, uintptr_t, 0> * loc_act_map)