From b66360d0b5fca4652dee85abb43980af5b2e77f8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 7 Apr 2020 11:15:34 -0700
Subject: [PATCH] fix #3809

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/simplex/model_based_opt.cpp |   1 +
 src/muz/rel/dl_base.cpp              | 138 +++++++++++----------------
 src/muz/rel/dl_base.h                |  38 ++++----
 src/muz/rel/dl_table.cpp             |   2 +-
 src/muz/spacer/spacer_context.cpp    |  12 +--
 5 files changed, 84 insertions(+), 107 deletions(-)

diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index 74f808f1d..73c9e0d1e 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -1088,6 +1088,7 @@ namespace opt {
         if (D.is_zero()) {
             throw default_exception("modulo 0 is not defined");
         }
+        if (D.is_neg()) D = abs(D);
         TRACE("opt1", display(tout << "lcm: " << D << " x: v" << x << " tableau\n"););
         rational val_x = m_var2value[x];
         rational u = mod(val_x, D);
diff --git a/src/muz/rel/dl_base.cpp b/src/muz/rel/dl_base.cpp
index d2c552355..784a812e3 100644
--- a/src/muz/rel/dl_base.cpp
+++ b/src/muz/rel/dl_base.cpp
@@ -39,21 +39,19 @@ namespace datalog {
     }
 
     void dealloc_ptr_vector_content(ptr_vector<relation_base> & v) {
-        ptr_vector<relation_base>::iterator it = v.begin();
-        ptr_vector<relation_base>::iterator end = v.end();
-        for(; it!=end; ++it) {
-            (*it)->deallocate();
+        for (auto& r : v) {
+            r->deallocate();
         }
     }
 
     void get_renaming_args(const unsigned_vector & map, const relation_signature & orig_sig, 
-            expr_ref_vector & renaming_arg) {
+                           expr_ref_vector & renaming_arg) {
         ast_manager & m = renaming_arg.get_manager();
         unsigned sz = map.size();
         unsigned ofs = sz-1;
         renaming_arg.resize(sz, static_cast<expr *>(nullptr));
-        for(unsigned i=0; i<sz; i++) {
-            if(map[i]!=UINT_MAX) {
+        for (unsigned i = 0; i < sz; i++) {
+            if (map[i] != UINT_MAX) {
                 renaming_arg.set(ofs-i, m.mk_var(map[i], orig_sig[i]));
             }
         }
@@ -74,13 +72,13 @@ namespace datalog {
 #endif
 
     void relation_signature::output(ast_manager & m, std::ostream & out) const {
-        unsigned sz=size();
-        out<<"(";
-        for(unsigned i=0; i<sz; i++) {
-            if(i) { out<<","; }
+        unsigned sz = size();
+        out << "(";
+        for (unsigned i = 0; i < sz; i++) {
+            if (i != 0) out << ","; 
             out << mk_pp((*this)[i], m);
         }
-        out<<")";
+        out << ")";
     }
 
 
@@ -90,8 +88,8 @@ namespace datalog {
         ast_manager & m = get_plugin().get_ast_manager();
         app_ref bottom_ref(m.mk_false(), m);
         scoped_ptr<relation_mutator_fn> reset_fn = get_manager().mk_filter_interpreted_fn(*this, bottom_ref);
-        if(!reset_fn) {
-            NOT_IMPLEMENTED_YET();
+        if (!reset_fn) {
+            throw default_exception("filter function does not exist");
         }
         (*reset_fn)(*this);
     }
@@ -106,16 +104,16 @@ namespace datalog {
         unsigned s2sz=s2.size();
         unsigned s1first_func=s1sz-s1.functional_columns();
         unsigned s2first_func=s2sz-s2.functional_columns();
-        for(unsigned i=0; i<s1first_func; i++) {
+        for (unsigned i=0; i<s1first_func; i++) {
             result.push_back(s1[i]);
         }
-        for(unsigned i=0; i<s2first_func; i++) {
+        for (unsigned i=0; i<s2first_func; i++) {
             result.push_back(s2[i]);
         }
-        for(unsigned i=s1first_func; i<s1sz; i++) {
+        for (unsigned i=s1first_func; i<s1sz; i++) {
             result.push_back(s1[i]);
         }
-        for(unsigned i=s2first_func; i<s2sz; i++) {
+        for (unsigned i=s2first_func; i<s2sz; i++) {
             result.push_back(s2[i]);
         }
         result.set_functional_columns(s1.functional_columns()+s2.functional_columns());
@@ -127,13 +125,13 @@ namespace datalog {
 
         unsigned func_cnt = src.functional_columns();
 
-        if(removed_cols==nullptr) {
+        if (removed_cols==nullptr) {
             result.set_functional_columns(func_cnt);
             return;
         }
 
         unsigned first_src_fun = src.first_functional();
-        if(removed_cols[0]<first_src_fun) {
+        if (removed_cols[0]<first_src_fun) {
             //if we remove at least one non-functional column, all the columns in the result are non-functional
             result.set_functional_columns(0);
         }
@@ -150,8 +148,8 @@ namespace datalog {
 
         unsigned remaining_fun = src.functional_columns();
         unsigned first_src_fun = src.first_functional();
-        for(int i=col_cnt-1; i>=0; i--) {
-            if(removed_cols[i]<first_src_fun) {
+        for (int i=col_cnt-1; i>=0; i--) {
+            if (removed_cols[i]<first_src_fun) {
                 break;
             }
             remaining_fun--;
@@ -168,7 +166,7 @@ namespace datalog {
         //after the join the column order is
         //(non-functional of s1)(non-functional of s2)(functional of s1)(functional of s2)
 
-        if(s1.functional_columns()==0 && s2.functional_columns()==0) {
+        if (s1.functional_columns()==0 && s2.functional_columns()==0) {
             from_project(aux, removed_col_cnt, removed_cols, result);
             SASSERT(result.functional_columns()==0);
             return;
@@ -187,27 +185,27 @@ namespace datalog {
 
         union_find_default_ctx uf_ctx;
         union_find<> uf(uf_ctx); //the numbers in uf correspond to column indexes after the join
-        for(unsigned i=0; i<join_sig_sz; i++) {
+        for (unsigned i=0; i<join_sig_sz; i++) {
             VERIFY(uf.mk_var() == i);
         }
 
-        for(unsigned i=0; i<joined_col_cnt; i++) {
+        for (unsigned i=0; i<joined_col_cnt; i++) {
             unsigned idx1 = (s1_first_func>cols1[i]) ? cols1[i] : (first_func_ofs+cols1[i]-s1_first_func);
             unsigned idx2 = (s2_first_func>cols2[i]) ? (second_ofs+cols2[i]) : (second_func_ofs+cols2[i]-s2_first_func);
             uf.merge(idx1, idx2);
         }
-        for(unsigned i=0; i<first_func_ofs; i++) { //we only count the non-functional columns
+        for (unsigned i=0; i<first_func_ofs; i++) { //we only count the non-functional columns
             remaining_in_equivalence_class[uf.find(i)]++;
         }
 
-        for(unsigned i=0; i<removed_col_cnt; i++) {
+        for (unsigned i=0; i<removed_col_cnt; i++) {
             unsigned rc = removed_cols[i];
-            if(rc>=first_func_ofs) {
+            if (rc>=first_func_ofs) {
                 //removing functional columns won't make us merge rows
                 continue;
             }
             unsigned eq_class_idx = uf.find(rc);
-            if(remaining_in_equivalence_class[eq_class_idx]>1) {
+            if (remaining_in_equivalence_class[eq_class_idx]>1) {
                 remaining_in_equivalence_class[eq_class_idx]--;
             }
             else {
@@ -216,7 +214,7 @@ namespace datalog {
             }
         }
 
-        if(merging_rows_can_happen) {
+        if (merging_rows_can_happen) {
             //this one marks all columns as non-functional
             from_project(aux, removed_col_cnt, removed_cols, result);
             SASSERT(result.functional_columns()==0);
@@ -227,9 +225,6 @@ namespace datalog {
         }
     }
 
-
-
-
     // -----------------------------------
     //
     // table_base
@@ -239,17 +234,17 @@ namespace datalog {
     //here we give generic implementation of table operations using iterators
 
     bool table_base::empty() const {
-        return begin()==end();
+        return begin() == end();
     }
     
     void table_base::remove_facts(unsigned fact_cnt, const table_fact * facts) {
-        for(unsigned i=0; i<fact_cnt; i++) {
+        for (unsigned i = 0; i < fact_cnt; i++) {
             remove_fact(facts[i]);
         }
     }
 
     void table_base::remove_facts(unsigned fact_cnt, const table_element * facts) {
-        for(unsigned i=0; i<fact_cnt; i++) {
+        for (unsigned i = 0; i < fact_cnt; i++) {
             remove_fact(facts + i*get_signature().size());
         }
     }
@@ -257,25 +252,19 @@ namespace datalog {
 
     void table_base::reset() {
         vector<table_fact> to_remove;
-        table_base::iterator it = begin();
-        table_base::iterator iend = end();
         table_fact row;
-        for(; it!=iend; ++it) {
-            it->get_fact(row);
+        for (auto& k : *this) {
+            k.get_fact(row);
             to_remove.push_back(row);
         }
         remove_facts(to_remove.size(), to_remove.c_ptr());
     }
 
     bool table_base::contains_fact(const table_fact & f) const {
-        iterator it = begin();
-        iterator iend = end();
-
         table_fact row;
-
-        for(; it!=iend; ++it) {
-            it->get_fact(row);
-            if(vectors_equal(row, f)) {
+        for (auto const& k : *this) {
+            k.get_fact(row);
+            if (vectors_equal(row, f)) {
                 return true;
             }
         }
@@ -283,27 +272,25 @@ namespace datalog {
     }
 
     bool table_base::fetch_fact(table_fact & f) const {
-        if(get_signature().functional_columns()==0) {
+        if (get_signature().functional_columns() == 0) {
             return contains_fact(f);
         }
         else {
             unsigned sig_sz = get_signature().size();
             unsigned non_func_cnt = sig_sz-get_signature().functional_columns();
-            table_base::iterator it = begin();
-            table_base::iterator iend = end();
             table_fact row;
-            for(; it!=iend; ++it) {
-                it->get_fact(row);
+            for (auto& k : *this) {
+                k.get_fact(row);
                 bool differs = false;
-                for(unsigned i=0; i<non_func_cnt; i++) {
-                    if(row[i]!=f[i]) {
+                for (unsigned i=0; i<non_func_cnt; i++) {
+                    if (row[i]!=f[i]) {
                         differs = true;
                     }
                 }
-                if(differs) {
+                if (differs) {
                     continue;
                 }
-                for(unsigned i=non_func_cnt; i<sig_sz; i++) {
+                for (unsigned i=non_func_cnt; i<sig_sz; i++) {
                     f[i]=row[i];
                 }
                 return true;
@@ -313,15 +300,15 @@ namespace datalog {
     }
 
     bool table_base::suggest_fact(table_fact & f) {
-        if(get_signature().functional_columns()==0) {
-            if(contains_fact(f)) {
+        if (get_signature().functional_columns()==0) {
+            if (contains_fact(f)) {
                 return false;
             }
             add_new_fact(f);
             return true;
         }
         else {
-            if(fetch_fact(f)) {
+            if (fetch_fact(f)) {
                 return false;
             }
             add_new_fact(f);
@@ -330,7 +317,7 @@ namespace datalog {
     }
 
     void table_base::ensure_fact(const table_fact & f) {
-        if(get_signature().functional_columns()==0) {
+        if (get_signature().functional_columns() == 0) {
             add_fact(f);
         }
         else {
@@ -341,14 +328,9 @@ namespace datalog {
 
     table_base * table_base::clone() const {
         table_base * res = get_plugin().mk_empty(get_signature());
-
-        iterator it = begin();
-        iterator iend = end();
-
         table_fact row;
-
-        for(; it!=iend; ++it) {
-            it->get_fact(row);
+        for (auto& k : *this) {
+            k.get_fact(row);
             res->add_new_fact(row);
         }
         return res;
@@ -394,9 +376,9 @@ namespace datalog {
             warning_msg("%s", buffer.str().c_str());
         }
 
-        for(table_element i = 0; i < upper_bound; i++) {
+        for (table_element i = 0; i < upper_bound; i++) {
             fact[0] = i;
-            if(empty_table || !contains_fact(fact)) {
+            if (empty_table || !contains_fact(fact)) {
                 res->add_fact(fact);
             }
         }
@@ -407,12 +389,9 @@ namespace datalog {
         out << "table with signature ";
         print_container(get_signature(), out);
         out << ":\n";
-
-        iterator it = begin();
-        iterator iend = end();
-        for(; it!=iend; ++it) {
-            const row_interface & r = *it;
-            r.display(out);
+        
+        for (auto& k : *this) {
+            k.display(out);
         }
 
         out << "\n";
@@ -448,8 +427,8 @@ namespace datalog {
 
     void table_base::row_interface::get_fact(table_fact & result) const {
         result.reset();
-        unsigned n=size();
-        for(unsigned i=0; i<n; i++) {
+        unsigned n = size();
+        for (unsigned i = 0; i < n; i++) {
             result.push_back((*this)[i]);
         }
     }
@@ -470,10 +449,7 @@ namespace datalog {
         dl_decl_util util(m);
         bool_rewriter brw(m);
         table_fact fact;
-        iterator it = begin();
-        iterator iend = end();
-        for(; it != iend; ++it) {
-            const row_interface & r = *it;   
+        for (row_interface const& r : *this) {
             r.get_fact(fact);
             conjs.reset();
             for (unsigned i = 0; i < fact.size(); ++i) {
diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h
index d1cc8d06f..22bff5aff 100644
--- a/src/muz/rel/dl_base.h
+++ b/src/muz/rel/dl_base.h
@@ -96,12 +96,12 @@ namespace datalog {
         public:
             bool operator==(const signature & o) const {
                 unsigned n=signature_base_base::size();
-                if(n!=o.size()) {
+                if (n!=o.size()) {
                     return false;
                 }
                 return memcmp(this->c_ptr(), o.c_ptr(), n*sizeof(sort))==0;
-                /*for(unsigned i=0; i<n; i++) {
-                    if((*this)[i]!=o[i]) {
+                /*for (unsigned i=0; i<n; i++) {
+                    if ((*this)[i]!=o[i]) {
                         return false;
                     }
                 }
@@ -117,15 +117,15 @@ namespace datalog {
                 result.reset();
 
                 unsigned s1sz=s1.size();
-                for(unsigned i=0; i<s1sz; i++) {
+                for (unsigned i=0; i<s1sz; i++) {
                     result.push_back(s1[i]);
                 }
                 unsigned s2sz=s2.size();
-                for(unsigned i=0; i<s2sz; i++) {
+                for (unsigned i=0; i<s2sz; i++) {
                     result.push_back(s2[i]);
                 }
 #if Z3DEBUG
-                for(unsigned i=0; i<col_cnt; i++) {
+                for (unsigned i=0; i<col_cnt; i++) {
                     SASSERT(cols1[i]<s1sz);
                     SASSERT(cols2[i]<s2sz);
                 }
@@ -171,7 +171,7 @@ namespace datalog {
                     const unsigned * permutation, signature & result) {
                 result.reset();
                 unsigned n = src.size();
-                for(unsigned i=0; i<n; i++) {
+                for (unsigned i=0; i<n; i++) {
                     result.push_back(src[permutation[i]]);
                 }
             }
@@ -591,8 +591,8 @@ namespace datalog {
                 unsigned neg_sig_size = neg_t.get_signature().size();
                 m_overlap = false;
                 m_bound.resize(neg_sig_size, false);
-                for(unsigned i=0; i<joined_col_cnt; i++) {
-                    if(m_bound[negated_cols[i]]) {
+                for (unsigned i=0; i<joined_col_cnt; i++) {
+                    if (m_bound[negated_cols[i]]) {
                         m_overlap = true;
                     }
                     m_bound[negated_cols[i]]=true;
@@ -611,14 +611,14 @@ namespace datalog {
             void make_neg_bindings(T & tgt_neg, const U & src) const {
                 SASSERT(m_all_neg_bound);
                 SASSERT(!m_overlap);
-                for(unsigned i=0; i<m_joined_col_cnt; i++) {
+                for (unsigned i=0; i<m_joined_col_cnt; i++) {
                     tgt_neg[m_cols2[i]]=src[m_cols1[i]];
                 }
             }
             template<typename T, typename U>
             bool bindings_match(const T & tgt_neg, const U & src) const {
-                for(unsigned i=0; i<m_joined_col_cnt; i++) {
-                    if(tgt_neg[m_cols2[i]]!=src[m_cols1[i]]) {
+                for (unsigned i=0; i<m_joined_col_cnt; i++) {
+                    if (tgt_neg[m_cols2[i]]!=src[m_cols1[i]]) {
                         return false;
                     }
                 }
@@ -661,10 +661,10 @@ namespace datalog {
             base_object * operator()(const base_object & o) override {
                 const base_object * res = &o;
                 scoped_rel<base_object> res_scoped;
-                if(m_renamers_initialized) {
+                if (m_renamers_initialized) {
                     typename renamer_vector::iterator rit = m_renamers.begin();
                     typename renamer_vector::iterator rend = m_renamers.end();
-                    for(; rit!=rend; ++rit) {
+                    for (; rit!=rend; ++rit) {
                         res_scoped = (**rit)(*res);
                         res = res_scoped.get();
                     }
@@ -683,7 +683,7 @@ namespace datalog {
                     }
                     m_renamers_initialized = true;
                 }
-                if(res_scoped) {
+                if (res_scoped) {
                     SASSERT(res==res_scoped.get());
                     //we don't want to delete the last one since we'll be returning it
                     return res_scoped.release();
@@ -989,7 +989,7 @@ namespace datalog {
 #if Z3DEBUG
             unsigned first_src_fun = src.size()-src.functional_columns();
             bool in_func = permutation_cycle[0]>=first_src_fun;
-            for(unsigned i=1;i<cycle_len;i++) {
+            for (unsigned i=1;i<cycle_len;i++) {
                 SASSERT(in_func == (permutation_cycle[i]>=first_src_fun));
             }
 #endif
@@ -1007,7 +1007,7 @@ namespace datalog {
 #if Z3DEBUG
             unsigned sz = src.size();
             unsigned first_src_fun = sz-src.functional_columns();
-            for(unsigned i=first_src_fun;i<sz;i++) {
+            for (unsigned i=first_src_fun;i<sz;i++) {
                 SASSERT(permutation[i]>=first_src_fun);
             }
 #endif
@@ -1107,7 +1107,7 @@ namespace datalog {
             void dec_ref() {
                 SASSERT(m_ref_cnt>0);
                 m_ref_cnt--;
-                if(m_ref_cnt==0) {
+                if (m_ref_cnt==0) {
                     dealloc(this);
                 }
             }
@@ -1137,7 +1137,7 @@ namespace datalog {
             void dec_ref() {
                 SASSERT(m_ref_cnt>0);
                 m_ref_cnt--;
-                if(m_ref_cnt==0) {
+                if (m_ref_cnt==0) {
                     dealloc(this);
                 }
             }
diff --git a/src/muz/rel/dl_table.cpp b/src/muz/rel/dl_table.cpp
index 45d3d9f47..1275577e3 100644
--- a/src/muz/rel/dl_table.cpp
+++ b/src/muz/rel/dl_table.cpp
@@ -251,7 +251,7 @@ namespace datalog {
             }
             shift += num_bits;
             if (shift >= 32) {
-                  throw default_exception("bit-vector table is specialized to small domains that are powers of two");
+                throw default_exception("bit-vector table is specialized to small domains that are powers of two");
             }
         }
         m_bv.reserve(1 << shift);
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index a20a5d1e3..db9af2265 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -2924,12 +2924,12 @@ expr_ref context::get_ground_sat_answer() const {
                    << "Sat answer unavailable when result is false\n";);
         return expr_ref(m);
     }
-
+    
     // convert a ground refutation into a linear counterexample
     // only works for linear CHC systems
     expr_ref_vector cex(m);
     proof_ref pf = get_ground_refutation();
-
+    
     proof_ref_vector premises(m);
     expr_ref conclusion(m);
     svector<std::pair<unsigned, unsigned>> positions;
@@ -2946,18 +2946,18 @@ expr_ref context::get_ground_sat_answer() const {
         } else {
             pf.reset();
             break;
-    }
-
+        }
+        
         premises.reset();
         conclusion.reset();
         positions.reset();
         substs.reset();
-        }
+    }
     SASSERT(!pf || !m.is_hyper_resolve(pf));
     if (pf) {
         cex.push_back(m.get_fact(pf));
     }
-
+    
     TRACE ("spacer", tout << "ground cex\n" << cex << "\n";);
 
     return mk_and(cex);