Assign each predicate's initial weight ad 100. Remove some unused function and data...

diff --git a/funcnode.cc b/funcnode.cc
index c01173ae747334bff1a913e897da88d5e7243a4b..5a0969d2168d0162b53d5e778c5b090962338d0e 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -22,8 +22,6 @@ FuncNode::FuncNode(ModelHistory * history) :
        thrd_loc_inst_map(),
        thrd_predicate_tree_position(),
        thrd_predicate_trace(),
        thrd_loc_inst_map(),
        thrd_predicate_tree_position(),
        thrd_predicate_trace(),

-       predicate_leaves(),
-       leaves_tmp_storage(),

        failed_predicates(),
        edge_table(32),
        out_edges()
        failed_predicates(),
        edge_table(32),
        out_edges()


@@ -353,8 +351,6 @@ void FuncNode::update_predicate_tree(ModelAction * next_act)
                add_predicate_to_trace(tid, curr_pred);
                break;
        }
                add_predicate_to_trace(tid, curr_pred);
                break;
        }

-
-//     leaves_tmp_storage.push_back(curr_pred);

 }
 
 /* Given curr_pred and next_inst, find the branch following curr_pred that
 }
 
 /* Given curr_pred and next_inst, find the branch following curr_pred that


@@ -496,10 +492,6 @@ void FuncNode::generate_predicates(Predicate * curr_pred, FuncInst * next_inst,
                curr_pred->add_child(new_pred);
                new_pred->set_parent(curr_pred);
 
                curr_pred->add_child(new_pred);
                new_pred->set_parent(curr_pred);
 

-               /* Maintain predicate leaves */
-               predicate_leaves.add(new_pred);
-               predicate_leaves.remove(curr_pred);
-

                /* entry predicates and predicates containing pure write actions
                 * have no predicate expressions */
                if ( curr_pred->is_entry_predicate() )
                /* entry predicates and predicates containing pure write actions
                 * have no predicate expressions */
                if ( curr_pred->is_entry_predicate() )


@@ -541,14 +533,8 @@ void FuncNode::generate_predicates(Predicate * curr_pred, FuncInst * next_inst,
                Predicate * pred= predicates[i];
                curr_pred->add_child(pred);
                pred->set_parent(curr_pred);
                Predicate * pred= predicates[i];
                curr_pred->add_child(pred);
                pred->set_parent(curr_pred);

-
-               /* Add new predicate leaves */
-               predicate_leaves.add(pred);

        }
 
        }
 

-       /* Remove predicate node that has children */
-       predicate_leaves.remove(curr_pred);
-

        /* Free memories allocated by infer_predicate */
        for (uint i = 0;i < half_pred_expressions->size();i++) {
                struct half_pred_expr * tmp = (*half_pred_expressions)[i];
        /* Free memories allocated by infer_predicate */
        for (uint i = 0;i < half_pred_expressions->size();i++) {
                struct half_pred_expr * tmp = (*half_pred_expressions)[i];


@@ -846,41 +832,6 @@ void FuncNode::add_failed_predicate(Predicate * pred)
        failed_predicates.add(pred);
 }
 
        failed_predicates.add(pred);
 }
 

-/* Implement quick sort to sort leaves before assigning base scores */
-template<typename _Tp>
-static int partition(ModelVector<_Tp *> * arr, int low, int high)
-{
-       unsigned int pivot = (*arr)[high] -> get_depth();
-       int i = low - 1;
-
-       for (int j = low;j <= high - 1;j ++) {
-               if ( (*arr)[j] -> get_depth() < pivot ) {
-                       i ++;
-                       _Tp * tmp = (*arr)[i];
-                       (*arr)[i] = (*arr)[j];
-                       (*arr)[j] = tmp;
-               }
-       }
-
-       _Tp * tmp = (*arr)[i + 1];
-       (*arr)[i + 1] = (*arr)[high];
-       (*arr)[high] = tmp;
-
-       return i + 1;
-}
-
-/* Implement quick sort to sort leaves before assigning base scores */
-template<typename _Tp>
-static void quickSort(ModelVector<_Tp *> * arr, int low, int high)
-{
-       if (low < high) {
-               int pi = partition(arr, low, high);
-
-               quickSort(arr, low, pi - 1);
-               quickSort(arr, pi + 1, high);
-       }
-}
-

 void FuncNode::update_predicate_tree_weight(thread_id_t tid)
 {
        failed_predicates.reset();
 void FuncNode::update_predicate_tree_weight(thread_id_t tid)
 {
        failed_predicates.reset();


@@ -890,13 +841,13 @@ void FuncNode::update_predicate_tree_weight(thread_id_t tid)
        // Update predicate weights based on prediate trace
        for (mllnode<Predicate *> * rit = trace->end(); rit != NULL; rit = rit->getPrev()) {
                Predicate * node = rit->getVal();
        // Update predicate weights based on prediate trace
        for (mllnode<Predicate *> * rit = trace->end(); rit != NULL; rit = rit->getPrev()) {
                Predicate * node = rit->getVal();

+               ModelVector<Predicate *> * children = node->get_children();

 
 

-               if (predicate_leaves.contains(node)) {
+               if (children->size() == 0) {

                        double weight = 100.0 / sqrt(node->get_expl_count() + node->get_fail_count() + 1);
                        node->set_weight(weight);
                } else {
                        double weight_sum = 0.0;
                        double weight = 100.0 / sqrt(node->get_expl_count() + node->get_fail_count() + 1);
                        node->set_weight(weight);
                } else {
                        double weight_sum = 0.0;

-                       ModelVector<Predicate *> * children = node->get_children();

                        for (uint i = 0;i < children->size();i++) {
                                Predicate * child = (*children)[i];
                                double weight = child->get_weight();
                        for (uint i = 0;i < children->size();i++) {
                                Predicate * child = (*children)[i];
                                double weight = child->get_weight();

diff --git a/funcnode.h b/funcnode.h
index d8b0bc1a0a6342421dce0c17f1859175495dc158..354534d55cf60f723f7a72ee9bc6cea07ef21f98 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -9,12 +9,12 @@
 #define MAX_DIST 10
 
 typedef ModelList<FuncInst *> func_inst_list_mt;
 #define MAX_DIST 10
 
 typedef ModelList<FuncInst *> func_inst_list_mt;

+typedef ModelList<Predicate *> predicate_trace_t;
+

 typedef HashTable<void *, FuncInst *, uintptr_t, 0, model_malloc, model_calloc, model_free> loc_inst_map_t;
 typedef HashTable<FuncInst *, uint32_t, uintptr_t, 0, model_malloc, model_calloc, model_free> inst_id_map_t;
 typedef HashTable<FuncInst *, Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> inst_pred_map_t;
 
 typedef HashTable<void *, FuncInst *, uintptr_t, 0, model_malloc, model_calloc, model_free> loc_inst_map_t;
 typedef HashTable<FuncInst *, uint32_t, uintptr_t, 0, model_malloc, model_calloc, model_free> inst_id_map_t;
 typedef HashTable<FuncInst *, Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> inst_pred_map_t;
 

-typedef ModelList<Predicate *> predicate_trace_t;
-

 typedef enum edge_type {
        IN_EDGE, OUT_EDGE, BI_EDGE
 } edge_type_t;
 typedef enum edge_type {
        IN_EDGE, OUT_EDGE, BI_EDGE
 } edge_type_t;


@@ -136,8 +136,6 @@ private:
        void init_predicate_tree_data_structure(thread_id_t tid);
        void reset_predicate_tree_data_structure(thread_id_t tid);
 
        void init_predicate_tree_data_structure(thread_id_t tid);
        void reset_predicate_tree_data_structure(thread_id_t tid);
 

-       PredSet predicate_leaves;
-       ModelVector<Predicate *> leaves_tmp_storage;

        PredSet failed_predicates;
 
        /* Store the relation between this FuncNode and other FuncNodes */
        PredSet failed_predicates;
 
        /* Store the relation between this FuncNode and other FuncNodes */

diff --git a/predicate.cc b/predicate.cc
index 22fb0c7e8f8172d8cbf4963970c4edd7b5d85d3c..44f5e8d1844f55ec8e860a5118a6c780b5914d07 100644 (file)
--- a/predicate.cc
+++ b/predicate.cc
@@ -8,7 +8,7 @@ Predicate::Predicate(FuncInst * func_inst, bool is_entry, bool is_exit) :
        exit_predicate(is_exit),
        does_write(false),
        depth(0),
        exit_predicate(is_exit),
        does_write(false),
        depth(0),

-       weight(0),
+       weight(100),

        exploration_count(0),
        store_visible_count(0),
        total_checking_count(0),
        exploration_count(0),
        store_visible_count(0),
        total_checking_count(0),