various fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/cmd_context/cmd_context.cpp

@@ -1372,6 +1372,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
             while (r == l_true && get_opt()->is_pareto()) {
                 was_pareto = true;
                 get_opt()->display_assignment(regular_stream());
+                regular_stream() << "\n";
                 r = get_opt()->optimize();
             }
         }

src/muz/rel/dl_product_relation.cpp

@@ -184,8 +184,10 @@ namespace datalog {
     }
 
     relation_base * product_relation_plugin::mk_full(func_decl* p, const relation_signature & s, family_id kind) {
-        if (kind == null_family_id) {
+        if (kind == null_family_id || !m_spec_store.contains_signature(s)) {
-            return alloc(product_relation, *this, s);
+            product_relation* result = alloc(product_relation, *this, s);
+            result->m_default_empty = false;
+            return result;
         }
         rel_spec spec;
         m_spec_store.get_relation_spec(s, kind, spec);

src/opt/opt_cmds.cpp

@@ -269,6 +269,7 @@ public:
                 if (r == l_true && opt.is_pareto()) {
                     while (r == l_true) {
                         display_result(ctx);
+                        ctx.regular_stream() << "\n";
                         r = opt.optimize();
                     }
                     if (p.get_bool("print_statistics", false)) {
@@ -314,7 +315,6 @@ public:
             if (mdl) {
                 ctx.regular_stream() << "(model " << std::endl;
                 model_smt2_pp(ctx.regular_stream(), ctx, *(mdl.get()), 2);
-                // m->display(ctx.regular_stream());
                 ctx.regular_stream() << ")" << std::endl;                    
             }
         }

src/opt/opt_context.cpp

@@ -42,6 +42,7 @@ namespace opt {
     void context::scoped_state::push() {
         m_hard_lim.push_back(m_hard.size());
         m_objectives_lim.push_back(m_objectives.size());        
+        m_objectives_term_trail_lim.push_back(m_objectives_term_trail.size());
     }
 
     void context::scoped_state::pop() {
@@ -372,48 +373,10 @@ namespace opt {
 
     void context::yield() {
         m_pareto->get_model(m_model);
-        update_lower(true);
+        update_bound(true, true);
-        for (unsigned i = 0; i < m_objectives.size(); ++i) {
+        update_bound(true, false);
-            objective const& obj = m_objectives[i];
-            switch(obj.m_type) {
-            case O_MINIMIZE:
-            case O_MAXIMIZE:
-                m_optsmt.update_upper(obj.m_index, m_optsmt.get_lower(obj.m_index), true);
-                break;
-            case O_MAXSMT: {
-                rational r = m_maxsmts.find(obj.m_id)->get_lower();
-                m_maxsmts.find(obj.m_id)->update_upper(r, true);
-                break;
-            }
-            }
-        }        
     }
 
-
-#if 0
-        // use PB
-        expr_ref mk_pb_cmp(objective const& obj, model_ref& mdl, bool is_ge) {
-            rational r, sum(0);
-            expr_ref val(m), result(m);
-            unsigned sz = obj.m_terms.size();
-            pb_util pb(m);
-
-            for (unsigned i = 0; i < sz; ++i) {
-                expr* t = obj.m_terms[i];
-                VERIFY(mdl->eval(t, val));
-                if (m.is_true(val)) {
-                    sum += r;
-                }
-            }
-            if (is_ge) {
-                result = pb.mk_ge(obj.m_terms.size(), obj.m_weights.c_ptr(), obj.m_terms.c_ptr(), r);
-            }
-            else {
-                result = pb.mk_le(obj.m_terms.size(), obj.m_weights.c_ptr(), obj.m_terms.c_ptr(), r);
-            }
-        }
-#endif
-
     lbool context::execute_pareto() {
         if (!m_pareto) {
             m_pareto = alloc(gia_pareto, m, *this, m_solver.get(), m_params);
@@ -761,7 +724,7 @@ namespace opt {
         }
     }
 
-    void context::update_lower(bool override) {
+    void context::update_bound(bool override, bool is_lower) {
         expr_ref val(m);
         for (unsigned i = 0; i < m_objectives.size(); ++i) {
             objective const& obj = m_objectives[i];
@@ -770,18 +733,27 @@ namespace opt {
             case O_MINIMIZE:
                 if (m_model->eval(obj.m_term, val) && is_numeral(val, r)) {
                     r += obj.m_offset;
-                    m_optsmt.update_lower(obj.m_index, inf_eps(-r), override);
+                    if (is_lower) {
+                        m_optsmt.update_lower(obj.m_index, inf_eps(-r), override);
+                    }
+                    else {
+                        m_optsmt.update_upper(obj.m_index, inf_eps(-r), override);
+                    }
                 }
                 break;
             case O_MAXIMIZE:
                 if (m_model->eval(obj.m_term, val) && is_numeral(val, r)) {
                     r += obj.m_offset;
-                    m_optsmt.update_lower(obj.m_index, inf_eps(r), override);
+                    if (is_lower) {
+                        m_optsmt.update_lower(obj.m_index, inf_eps(r), override);
+                    }
+                    else {
+                        m_optsmt.update_upper(obj.m_index, inf_eps(r), override);
+                    }
                 }
                 break;
             case O_MAXSMT: {
                 bool ok = true;
-                r = obj.m_offset;
                 for (unsigned j = 0; ok && j < obj.m_terms.size(); ++j) {
                     if (m_model->eval(obj.m_terms[j], val)) {
                         if (!m.is_true(val)) {
@@ -793,7 +765,12 @@ namespace opt {
                     }
                 }
                 if (ok) {
-                    m_maxsmts.find(obj.m_id)->update_upper(r, override);
+                    if (is_lower) {
+                        m_maxsmts.find(obj.m_id)->update_upper(r, override);
+                    }
+                    else {
+                        m_maxsmts.find(obj.m_id)->update_lower(r, override);
+                    }
                 }
                 break;
             }

src/opt/opt_context.h

@@ -192,7 +192,8 @@ namespace opt {
         void from_fmls(expr_ref_vector const& fmls);
         void simplify_fmls(expr_ref_vector& fmls);
 
-        void update_lower(bool override);
+        void update_lower(bool override) { update_bound(override, true); }
+        void update_bound(bool override, bool is_lower);
 
         inf_eps get_lower_as_num(unsigned idx);
         inf_eps get_upper_as_num(unsigned idx);

src/opt/weighted_maxsat.cpp

@@ -39,6 +39,8 @@ Notes:
 #include "scoped_timer.h"
 #include "optsmt.h"
 
+#define USE_SIMPLEX 0
+
 namespace opt {
 
     class scoped_stopwatch {
@@ -644,7 +646,7 @@ namespace opt {
 
         virtual void set_cancel(bool f) { 
             maxsmt_solver_base::set_cancel(f); 
-            // maxs->set_cancel(f);
+            maxs->set_cancel(f);
             m_optsmt.set_cancel(f);
         }
 
@@ -655,7 +657,7 @@ namespace opt {
 
         virtual void collect_statistics(statistics& st) const {
             maxsmt_solver_base::collect_statistics(st);
-            // maxs->s().collect_statistics(st);
+            maxs->s().collect_statistics(st);
             st.update("hsmax-num-iterations", m_stats.m_num_iterations);
             st.update("hsmax-num-core-reductions-n", m_stats.m_num_core_reductions_failure);
             st.update("hsmax-num-core-reductions-y", m_stats.m_num_core_reductions_success);
@@ -738,21 +740,26 @@ namespace opt {
                 m_aux_active.push_back(false);
                 m_core_activity.push_back(0);
                 m_aux2index.insert(m_aux.back(), i);
+#if USE_SIMPLEX
                 m_aux2index.insert(m_iaux.back(), i);
                 fml = m.mk_and(a.mk_le(a.mk_numeral(rational::zero(), true), iaux), 
                                a.mk_le(iaux, a.mk_numeral(rational::one(), true)));
                 rational const& w = m_weights[i];
                 sum.push_back(a.mk_mul(a.mk_numeral(w, w.is_int()), iaux));
                 m_solver.assert_expr(fml);
+#endif
                 if (tt) {
                     m_asms.push_back(m_aux.back());
                     ensure_active(i);
                 }
             }
+#if USE_SIMPLEX
             obj = a.mk_add(sum.size(), sum.c_ptr());
             m_objective = m_optsmt.add(obj);
             m_optsmt.setup(m_solver);
-            // maxs->init_soft(m_weights, m_aux);
+#else
+            maxs->init_soft(m_weights, m_aux);
+#endif
             TRACE("opt", print_seed(tout););
         }
 
@@ -878,9 +885,9 @@ namespace opt {
         //
         // produce the non-optimal hitting set by using the 10% heuristic.
         // of most active cores constraints.
+        // m_asms contains the current core.
         //
         void find_non_optimal_hitting_set(ptr_vector<expr>& hs) {
-            // m_asms contains the current core.
             std::sort(m_asms.begin(), m_asms.end(), lt_activity(*this));
             for (unsigned i = m_asms.size(); i > 9*m_asms.size()/10;) { 
                 --i;
@@ -899,7 +906,7 @@ namespace opt {
         lbool next_seed() {
             scoped_stopwatch _sw(m_stats.m_aux_sat_time);
             TRACE("opt", tout << "\n";);
-#if 1
+#if USE_SIMPLEX
             m_solver.display(std::cout);
             lbool is_sat = m_optsmt.lex(m_objective);
             if (is_sat == l_true) {
@@ -919,7 +926,27 @@ namespace opt {
             }
             
 #else
-            lbool is_sat = maxs->s().check_sat(0,0);
+
+            // min c_i*(not x_i) for x_i are soft clauses.
+            // max c_i*x_i for x_i are soft clauses
+            
+            lbool is_sat = l_true;
+            if (m_lower.is_pos()) {
+                expr_ref fml(m);
+                solver::scoped_push _scope(maxs->s());
+                fml = pb.mk_le(num_soft(), m_weights.c_ptr(), m_naux.c_ptr(), m_lower);
+                maxs->add_hard(fml);
+                //fml = pb.mk_ge(num_soft(), m_weights.c_ptr(), m_naux.c_ptr(), m_lower);
+                //maxs->add_hard(fml);
+                std::cout << fml << "\n";
+                is_sat = maxs->s().check_sat(0,0);
+                if (is_sat == l_true) {
+                    maxs->set_model();
+                    extract_seed();
+                    return l_true;
+                }
+            }
+            is_sat = maxs->s().check_sat(0,0);
             if (is_sat == l_true) {
                 maxs->set_model();
             }
@@ -927,24 +954,27 @@ namespace opt {
                 return is_sat;
             }
             is_sat = (*maxs)();            
-                    
+                                
             if (is_sat == l_true) {
-                model_ref mdl;
+                extract_seed();
-                maxs->get_model(mdl);
-                for (unsigned i = 0; i < num_soft(); ++i) {
-                    if (is_active(i)) {
-                        m_seed[i] = is_true(mdl, m_aux[i].get());
-                    }
-                    else {
-                        m_seed[i] = false;
-                    }
-                }
-                TRACE("opt", print_seed(tout););
             }
 #endif
             return is_sat;
         }
 
+        void extract_seed() {
+            model_ref mdl;
+            maxs->get_model(mdl);
+            m_lower.reset();
+            for (unsigned i = 0; i < num_soft(); ++i) {
+                m_seed[i] = is_active(i) && is_true(mdl, m_aux[i].get());
+                if (!m_seed[i]) {
+                    m_lower += m_weights[i];
+                }
+            }
+            TRACE("opt", print_seed(tout););
+        }
+
         //
         // check assignment returned by maxs with the original
         // hard constraints. 
@@ -1018,15 +1048,16 @@ namespace opt {
                     }
                 }
             }
-            //rational old_upper = m_upper;
+            rational upper(0);
-            m_upper.reset();
             for (unsigned i = 0; i < num_soft(); ++i) {
                 if (!m_seed[i]) {
-                    m_upper += m_weights[i];
+                    upper += m_weights[i];
                 }
-            }            
+            }       
-            //SASSERT(old_upper > m_upper);
+            if (upper < m_upper) {
-            TRACE("opt", tout << "new upper: " << m_upper << "\n";);
+                m_upper = upper;
+                TRACE("opt", tout << "new upper: " << m_upper << "\n";);
+            }
             return true;
         }
 
@@ -1109,7 +1140,7 @@ namespace opt {
             }
             expr_ref_vector fmls(m);
             expr_ref fml(m);
-#if 1
+#if USE_SIMPLEX
             for (unsigned i = 0; i < num_soft(); ++i) {
                 if (!indices.contains(i)) {
                     fmls.push_back(m_iaux[i].get());
@@ -1126,9 +1157,9 @@ namespace opt {
             }
             fml = m.mk_or(fmls.size(), fmls.c_ptr());
             maxs->add_hard(fml);
+            set_upper();
 #endif
             TRACE("opt", tout << fml << "\n";);
-            // set_upper();
         }
 
         // constrain the upper bound.
@@ -1143,7 +1174,7 @@ namespace opt {
         void block_up() {
             expr_ref_vector fmls(m);
             expr_ref fml(m);
-#if 1
+#if USE_SIMPLEX
             for (unsigned i = 0; i < m_asms.size(); ++i) {
                 unsigned index = m_aux2index.find(m_asms[i]);
                 m_core_activity[index]++;
@@ -1655,7 +1686,7 @@ namespace opt {
             else if (m_engine == symbol("hsmax")) {
                 ref<opt_solver> s0 = alloc(opt_solver, m, m_params, symbol());
                 s0->check_sat(0,0);                
-                maxsmt_solver_base* s2 = alloc(pbmax, s0.get(), m); // , s0->get_context();
+                maxsmt_solver_base* s2 = alloc(pbmax, s0.get(), m); // , s0->get_context());
                 s2->set_converter(s0->mc_ref().get());
                 m_maxsmt = alloc(hsmax, s.get(), m, s2);
             }