From 5f298b69659a9955b50e96100f541989e2ce58b8 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <t-nclaud@microsoft.com>
Date: Fri, 5 Apr 2013 18:02:41 -0700
Subject: [PATCH] spread some static love

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
---
 src/muz_qe/dl_mk_similarity_compressor.cpp | 28 +++++++++++-----------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/src/muz_qe/dl_mk_similarity_compressor.cpp b/src/muz_qe/dl_mk_similarity_compressor.cpp
index 9868c82f6..9855196c9 100644
--- a/src/muz_qe/dl_mk_similarity_compressor.cpp
+++ b/src/muz_qe/dl_mk_similarity_compressor.cpp
@@ -42,7 +42,7 @@ namespace datalog {
     /**
        Allows to traverse head and positive tails in a single for loop starting from -1
      */
-    app * get_by_tail_index(rule * r, int idx) {
+    static app * get_by_tail_index(rule * r, int idx) {
         if(idx==-1) {
             return r->get_head();
         }
@@ -51,11 +51,11 @@ namespace datalog {
     }
 
     template<typename T>
-    int aux_compare(T a, T b) {
+    static int aux_compare(T a, T b) {
         return (a>b) ? 1 : ( (a==b) ? 0 : -1);
     }
 
-    int compare_var_args(app* t1, app* t2) {
+    static int compare_var_args(app* t1, app* t2) {
         SASSERT(t1->get_num_args()==t2->get_num_args());
         int res;
         unsigned n = t1->get_num_args();
@@ -73,7 +73,7 @@ namespace datalog {
         return 0;
     }
 
-    int compare_args(app* t1, app* t2, int & skip_countdown) {
+    static int compare_args(app* t1, app* t2, int & skip_countdown) {
         SASSERT(t1->get_num_args()==t2->get_num_args());
         int res;
         unsigned n = t1->get_num_args();
@@ -98,7 +98,7 @@ namespace datalog {
        Two rules are in the same rough similarity class if they differ only in constant arguments
        of positive uninterpreted predicates.
      */
-    int rough_compare(rule * r1, rule * r2) {
+    static int rough_compare(rule * r1, rule * r2) {
         int res = aux_compare(r1->get_tail_size(), r2->get_tail_size());
         if(res!=0) { return res; }
         res = aux_compare(r1->get_uninterpreted_tail_size(), r2->get_uninterpreted_tail_size());
@@ -129,7 +129,7 @@ namespace datalog {
        \c r1 and \c r2 must be equal according to the \c rough_compare function for this function
        to be called.
      */
-    int total_compare(rule * r1, rule * r2, int skipped_arg_index = INT_MAX) {
+    static int total_compare(rule * r1, rule * r2, int skipped_arg_index = INT_MAX) {
         SASSERT(rough_compare(r1, r2)==0);
         int pos_tail_sz = r1->get_positive_tail_size();
         for(int i=-1; i<pos_tail_sz; i++) {
@@ -165,7 +165,7 @@ namespace datalog {
 
     typedef svector<const_info> info_vector;
 
-    void collect_const_indexes(app * t, int tail_index, info_vector & res) {
+    static void collect_const_indexes(app * t, int tail_index, info_vector & res) {
         unsigned n = t->get_num_args();
         for(unsigned i=0; i<n; i++) {
             if(is_var(t->get_arg(i))) {
@@ -175,7 +175,7 @@ namespace datalog {
         }
     }
 
-    void collect_const_indexes(rule * r, info_vector & res) {
+    static void collect_const_indexes(rule * r, info_vector & res) {
         collect_const_indexes(r->get_head(), -1, res);
         unsigned pos_tail_sz = r->get_positive_tail_size();
         for(unsigned i=0; i<pos_tail_sz; i++) {
@@ -184,7 +184,7 @@ namespace datalog {
     }
 
     template<class T>
-    void collect_orphan_consts(rule * r, const info_vector & const_infos, T & tgt) {
+    static void collect_orphan_consts(rule * r, const info_vector & const_infos, T & tgt) {
         unsigned const_cnt = const_infos.size();
         tgt.reset();
         for(unsigned i=0; i<const_cnt; i++) {
@@ -198,7 +198,7 @@ namespace datalog {
         }
     }
     template<class T>
-    void collect_orphan_sorts(rule * r, const info_vector & const_infos, T & tgt) {
+    static void collect_orphan_sorts(rule * r, const info_vector & const_infos, T & tgt) {
         unsigned const_cnt = const_infos.size();
         tgt.reset();
         for(unsigned i=0; i<const_cnt; i++) {
@@ -215,7 +215,7 @@ namespace datalog {
        \brief From the \c tail_indexes and \c arg_indexes remove elements corresponding to constants
        that are the same in rules \c *first ... \c *(after_last-1).
      */
-    void remove_stable_constants(rule_vector::iterator first, rule_vector::iterator after_last, 
+    static void remove_stable_constants(rule_vector::iterator first, rule_vector::iterator after_last, 
             info_vector & const_infos) {
         SASSERT(after_last-first>1);
         unsigned const_cnt = const_infos.size();
@@ -252,7 +252,7 @@ namespace datalog {
        first constant that is equal to it in all the rules. If there is no such, it will contain
        its own index.
      */
-    void detect_equal_constants(rule_vector::iterator first, rule_vector::iterator after_last, 
+    static void detect_equal_constants(rule_vector::iterator first, rule_vector::iterator after_last, 
             info_vector & const_infos) {
         SASSERT(first!=after_last);
         unsigned const_cnt = const_infos.size();
@@ -302,7 +302,7 @@ namespace datalog {
         }
     }
 
-    unsigned get_constant_count(rule * r) {
+    static unsigned get_constant_count(rule * r) {
         unsigned res = r->get_head()->get_num_args() - count_variable_arguments(r->get_head());
         unsigned pos_tail_sz = r->get_positive_tail_size();
         for(unsigned i=0; i<pos_tail_sz; i++) {
@@ -311,7 +311,7 @@ namespace datalog {
         return res;
     }
 
-    bool initial_comparator(rule * r1, rule * r2) {
+    static bool initial_comparator(rule * r1, rule * r2) {
         int res = rough_compare(r1, r2);
         if(res!=0) { return res>0; }
         return total_compare(r1, r2)>0;