Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

src/muz/base/rule_properties.cpp

@@ -26,7 +26,7 @@ Notes:
 
 using namespace datalog;
 rule_properties::rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& p): 
-    m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_generate_proof(false) {}
+    m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_dl(m), m_generate_proof(false) {}
 
 rule_properties::~rule_properties() {}
 
@@ -168,7 +168,7 @@ void rule_properties::operator()(app* n) {
     if (m_is_predicate(n)) {
         insert(m_interp_pred, m_rule);
     }    
-    else if (is_uninterp(n)) {
+    else if (is_uninterp(n) && !m_dl.is_rule_sort(n->get_decl()->get_range())) {
         m_uninterp_funs.insert(n->get_decl(), m_rule);
     }
     else if (m_dt.is_accessor(n)) {

src/muz/base/rule_properties.h

@@ -32,6 +32,7 @@ namespace datalog {
         context&      m_ctx;
         i_expr_pred&  m_is_predicate;
         datatype_util m_dt;
+        dl_decl_util  m_dl;
         bool          m_generate_proof;
         rule*         m_rule;
         obj_map<quantifier, rule*> m_quantifiers;

src/muz/rel/dl_compiler.cpp

@@ -408,13 +408,14 @@ namespace datalog {
 
     void compiler::get_local_indexes_for_projection(app * t, var_counter & globals, unsigned ofs, 
             unsigned_vector & res) {
+        // TODO: this can be optimized to avoid renames in some cases
         unsigned n = t->get_num_args();
         for(unsigned i = 0; i<n; i++) {
             expr * e = t->get_arg(i);
-            if(!is_var(e) || globals.get(to_var(e)->get_idx())!=0) {
+            if (is_var(e) && globals.get(to_var(e)->get_idx()) > 0) {
-                continue;
+              globals.update(to_var(e)->get_idx(), -1);
+              res.push_back(i + ofs);
             }
-            res.push_back(i+ofs);
         }
     }
 
@@ -422,11 +423,30 @@ namespace datalog {
         SASSERT(r->get_positive_tail_size()==2);
         ast_manager & m = m_context.get_manager();
         rule_counter counter;
-        counter.count_rule_vars(m, r);
+        // leave one column copy per var in the head (avoids later duplication)
+        counter.count_vars(m, r->get_head(), -1);
+
+        // take interp & neg preds into account (at least 1 column copy if referenced)
+        unsigned n = r->get_tail_size();
+        if (n > 2) {
+          rule_counter counter_tail;
+          for (unsigned i = 2; i < n; ++i) {
+            counter_tail.count_vars(m, r->get_tail(i));
+          }
+
+          rule_counter::iterator I = counter_tail.begin(), E = counter_tail.end();
+          for (; I != E; ++I) {
+            int& n = counter.get(I->m_key);
+            if (n == 0)
+              n = -1;
+          }
+        }
+
         app * t1 = r->get_tail(0);
         app * t2 = r->get_tail(1);
-        counter.count_vars(m, t1, -1);
+        counter.count_vars(m, t1);
-        counter.count_vars(m, t2, -1);
+        counter.count_vars(m, t2);
+
         get_local_indexes_for_projection(t1, counter, 0, res);
         get_local_indexes_for_projection(t2, counter, t1->get_num_args(), res);
     }

src/muz/rel/dl_instruction.cpp

@@ -266,7 +266,6 @@ namespace datalog {
             : m_clone(clone), m_src(src), m_tgt(tgt) {}
         virtual bool perform(execution_context & ctx) {
             if (ctx.reg(m_src)) log_verbose(ctx);            
-            ctx.make_empty(m_tgt);
             if (m_clone) {
                 ctx.set_reg(m_tgt, ctx.reg(m_src) ? ctx.reg(m_src)->clone() : 0);
             }
@@ -370,9 +369,9 @@ namespace datalog {
             m_cols2(col_cnt, cols2), m_res(result) {}
         virtual bool perform(execution_context & ctx) {
             log_verbose(ctx);            
-            ctx.make_empty(m_res);
             ++ctx.m_stats.m_join;
             if (!ctx.reg(m_rel1) || !ctx.reg(m_rel2)) {
+                ctx.make_empty(m_res);
                 return true;
             }
             relation_join_fn * fn;
@@ -755,8 +754,8 @@ namespace datalog {
             reg_idx tgt) : m_projection(projection), m_src(src), 
             m_cols(col_cnt, cols), m_tgt(tgt) {}
         virtual bool perform(execution_context & ctx) {
-            ctx.make_empty(m_tgt);
             if (!ctx.reg(m_src)) {
+                ctx.make_empty(m_tgt);
                 return true;
             }
 
@@ -823,8 +822,8 @@ namespace datalog {
         }
         virtual bool perform(execution_context & ctx) {
             log_verbose(ctx);            
-            ctx.make_empty(m_res);
             if (!ctx.reg(m_rel1) || !ctx.reg(m_rel2)) {
+                ctx.make_empty(m_res);
                 return true;
             }
             ++ctx.m_stats.m_join_project;
@@ -1000,7 +999,6 @@ namespace datalog {
         virtual bool perform(execution_context & ctx) {
             log_verbose(ctx);            
             ++ctx.m_stats.m_unary_singleton;
-            ctx.make_empty(m_tgt);
             relation_base * rel = ctx.get_rel_context().get_rmanager().mk_empty_relation(m_sig, m_pred);
             rel->add_fact(m_fact);
             ctx.set_reg(m_tgt, rel);
@@ -1034,7 +1032,6 @@ namespace datalog {
         virtual bool perform(execution_context & ctx) {
             log_verbose(ctx);            
             ++ctx.m_stats.m_total;
-            ctx.make_empty(m_tgt);
             ctx.set_reg(m_tgt, ctx.get_rel_context().get_rmanager().mk_full_relation(m_sig, m_pred));
             return true;
         }

src/muz/rel/dl_mk_explanations.cpp

@@ -854,7 +854,10 @@ namespace datalog {
                 scoped_ptr<relation_join_fn> product_fun = rmgr.mk_join_fn(orig_rel, *m_e_fact_relation, 0, 0, 0);
                 SASSERT(product_fun);
                 scoped_rel<relation_base> aux_extended_rel = (*product_fun)(orig_rel, *m_e_fact_relation);
+                TRACE("dl", tout << aux_extended_rel << " " << aux_extended_rel->get_plugin().get_name() << "\n";
+                      tout << e_rel.get_plugin().get_name() << "\n";);
                 scoped_ptr<relation_union_fn> union_fun = rmgr.mk_union_fn(e_rel, *aux_extended_rel);
+                TRACE("dl", tout << union_fun << "\n";);
                 SASSERT(union_fun);
                 (*union_fun)(e_rel, *aux_extended_rel);
             }

src/muz/rel/karr_relation.h

@@ -45,7 +45,7 @@ namespace datalog {
         {}            
         
         virtual bool can_handle_signature(const relation_signature & sig) {
-            return true;
+            return get_manager().get_context().karr();
         }
 
         static symbol get_name() { return symbol("karr_relation"); }

src/muz/rel/rel_context.cpp

@@ -115,7 +115,7 @@ namespace datalog {
 
         rm.register_plugin(alloc(bound_relation_plugin, rm));
         rm.register_plugin(alloc(interval_relation_plugin, rm));
-        rm.register_plugin(alloc(karr_relation_plugin, rm));
+        if (m_context.karr()) rm.register_plugin(alloc(karr_relation_plugin, rm));
         rm.register_plugin(alloc(product_set_plugin, rm));
         rm.register_plugin(alloc(udoc_plugin, rm));
         rm.register_plugin(alloc(check_relation_plugin, rm));

src/muz/rel/udoc_relation.cpp

@@ -1028,7 +1028,9 @@ namespace datalog {
     }
 
     class udoc_plugin::join_project_fn : public convenient_relation_join_project_fn {
+#if 0
         udoc_plugin::join_fn   m_joiner;
+#endif
         union_find_default_ctx union_ctx;
         bit_vector             m_to_delete; 
         subset_ints            m_equalities;
@@ -1043,7 +1045,9 @@ namespace datalog {
                 t1.get_signature(), t2.get_signature(), 
                 col_cnt, cols1, cols2,
                 removed_col_cnt, rm_cols),
+#if 0
               m_joiner(t1.get_plugin(), t1, t2, col_cnt, cols1, cols2),
+#endif
               m_equalities(union_ctx)
         {
             udoc_plugin& p = t1.get_plugin();
@@ -1152,12 +1156,36 @@ namespace datalog {
 
     };
 
+
+    class udoc_plugin::join_project_and_fn : public relation_join_fn {
+    public:
+      join_project_and_fn() {}
+
+      virtual relation_base* operator()(relation_base const& t1, relation_base const& t2) {
+          udoc_relation *result = get(t1.clone());
+          result->get_udoc().intersect(result->get_dm(), get(t2).get_udoc());
+          return result;
+      }
+    };
+
     relation_join_fn * udoc_plugin::mk_join_project_fn(
         relation_base const& t1, relation_base const& t2,
         unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, 
         unsigned removed_col_cnt, const unsigned * removed_cols) {    
         if (!check_kind(t1) || !check_kind(t2))
             return 0;
+        // special case where we have h(X) :- f(X), g(X).
+        if (joined_col_cnt == removed_col_cnt &&
+            t1.get_signature().size() == joined_col_cnt &&
+            t2.get_signature().size() == joined_col_cnt) {
+            for (unsigned i = 0; i < removed_col_cnt; ++i) {
+                if (removed_cols[i] != i)
+                    goto general_fn;
+            }
+            return alloc(join_project_and_fn);
+        }
+
+      general_fn:
         return alloc(join_project_fn, get(t1), get(t2),
                      joined_col_cnt, cols1, cols2,
                      removed_col_cnt, removed_cols);

src/muz/rel/udoc_relation.h

@@ -82,6 +82,7 @@ namespace datalog {
         friend class udoc_relation;
         class join_fn;
         class join_project_fn;
+        class join_project_and_fn;
         class project_fn;
         class union_fn;
         class rename_fn;

src/opt/opt_context.cpp

@@ -995,7 +995,7 @@ namespace opt {
             args.push_back(m_arith.mk_numeral(r, r.is_int()));
         }
         if (!eps.is_zero()) {
-            expr* ep = m.mk_const(symbol("epsilon"), m_arith.mk_int());
+            expr* ep = m.mk_const(symbol("epsilon"), m_arith.mk_real());
             if (eps.is_one()) {
                 args.push_back(ep);
             }

src/smt/theory_arith_aux.h

@@ -1377,11 +1377,11 @@ namespace smt {
                 SASSERT(satisfy_bounds());
                 result = skipped_row?BEST_EFFORT:OPTIMIZED;
                 break; 
-           }
+            }
 
             if (x_i == null_theory_var) {
                 // can increase/decrease x_j as much as we want.
-                if (inc && upper(x_j)) {
+                if (inc && upper(x_j) && !skipped_row) {
                     update_value(x_j, upper_bound(x_j) - get_value(x_j));
                     TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";);
                     SASSERT(valid_row_assignment());
@@ -1389,7 +1389,7 @@ namespace smt {
                     SASSERT(satisfy_integrality());
                     continue;
                 }
-                if (!inc && lower(x_j)) {
+                if (!inc && lower(x_j) && !skipped_row) {
                     update_value(x_j, lower_bound(x_j) - get_value(x_j));
                     TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";);
                     SASSERT(valid_row_assignment());
@@ -1463,6 +1463,7 @@ namespace smt {
     template<typename Ext>
     bool theory_arith<Ext>::move_to_bound(theory_var x_i, bool move_to_lower) {
         inf_numeral delta, delta_abs;
+        numeral lc(1);
 
         if (move_to_lower) {
             delta = lower_bound(x_i) - get_value(x_i);
@@ -1475,7 +1476,7 @@ namespace smt {
 
         TRACE("opt", tout << "Original delta: " << delta << "\n";);
 
-        delta_abs = abs(delta);
+        delta_abs = abs(delta);        
         //
         // Decrease absolute value of delta according to bounds on rows where x_i is used.
         //
@@ -1483,28 +1484,31 @@ namespace smt {
         typename svector<col_entry>::iterator it  = c.begin_entries();
         typename svector<col_entry>::iterator end = c.end_entries();
         for (; it != end && delta_abs.is_pos(); ++it) {
-            if (!it->is_dead()) {
+            if (it->is_dead()) continue;
-                row & r = m_rows[it->m_row_id];
+            row & r = m_rows[it->m_row_id];
-                theory_var s = r.get_base_var();
+            theory_var s = r.get_base_var();
-                if (s != null_theory_var && !is_quasi_base(s)) {
+            if (s != null_theory_var && !is_quasi_base(s)) {
-                    numeral const & coeff = r[it->m_row_idx].m_coeff;
+                numeral const & coeff = r[it->m_row_idx].m_coeff;
-                    SASSERT(!coeff.is_zero());
+                SASSERT(!coeff.is_zero());
-                    bool inc_s = coeff.is_pos() ? move_to_lower : !move_to_lower; // NSB: review this..
+                bool inc_s = coeff.is_pos() ? move_to_lower : !move_to_lower; // NSB: review this..
-                    bound * b = get_bound(s, inc_s);
+                bound * b = get_bound(s, inc_s);
-                    if (b) {
+                if (b) {
-                        inf_numeral delta2 = abs((get_value(s) - b->get_value())/coeff);
+                    inf_numeral delta2 = abs((get_value(s) - b->get_value())/coeff);
-                        if (delta2 < delta_abs) {
+                    if (delta2 < delta_abs) {
-                            delta_abs = delta2;
+                        delta_abs = delta2;
-                        }
                     }
                 }
+                if (is_int(x_i)) {
+                    lc = lcm(lc, denominator(abs(coeff)));
+                }
             }
         }
 
         bool truncated = false;
         if (is_int(x_i)) {
-            truncated = !delta_abs.is_int();
+            inf_numeral tmp = delta_abs/lc;
-            delta_abs = floor(delta_abs);
+            truncated = !tmp.is_int();
+            delta_abs = lc*floor(tmp);            
         }
 
         if (move_to_lower) {