fixes to #52, #53

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

src/opt/opt_context.cpp

@@ -388,7 +388,6 @@ namespace opt {
             }
             break;
         case O_MAXSMT: {
-            m_opt_solver->ensure_pb();
             pb_util      pb(m);
             unsigned sz = obj.m_terms.size();
             ptr_vector<expr> terms;
@@ -475,6 +474,9 @@ namespace opt {
             m_opt_solver->set_logic(m_logic);
             m_solver = m_opt_solver.get();
         }
+        if (opt_params(m_params).priority() == symbol("pareto")) {
+            m_opt_solver->ensure_pb();
+        }        
     }
 
     void context::setup_arith_solver() {
@@ -497,6 +499,9 @@ namespace opt {
             m_maxsat_engine != symbol("sls")) {
             return;
         }
+        if (opt_params(m_params).priority() == symbol("pareto")) {
+            return;
+        }
         m_params.set_bool("minimize_core_partial", true); // false);
         m_params.set_bool("minimize_core", true);
         m_sat_solver = mk_inc_sat_solver(m, m_params);

src/opt/opt_solver.cpp

@@ -204,38 +204,52 @@ namespace opt {
         m_valid_objectives[i] = true;
         TRACE("opt", tout << (has_shared?"has shared":"non-shared") << "\n";);
         if (m_context.get_context().update_model(has_shared)) {
-            if (has_shared) {
+            if (has_shared && val != current_objective_value(i)) {
-                val2 = current_objective_value(i);                
+                decrement_value(i, val);
-                if (val2 != val) {
+            }
-                    decrement_value(i, val);
+            else {
-                }
+                set_model(i);
             }
         }
         else {
             SASSERT(has_shared);
-            // model is not final. We set the current objective to
+            decrement_value(i, val);            
-            // close to the optimal (ignoring types).
-            decrement_value(i, val);
         }
         m_objective_values[i] = val;
+        TRACE("opt", { tout << val << "\n"; 
+                tout << blocker << "\n";
+                model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); });
+    }
 
+    void opt_solver::set_model(unsigned i) {
         model_ref mdl;
         get_model(mdl);
         m_models.set(i, mdl.get());
-
-        TRACE("opt", { tout << m_objective_values[i] << "\n"; 
-                  tout << blocker << "\n";
-                   model_smt2_pp(tout << "update model:\n", m, *mdl, 0); });
     }
 
-    void opt_solver::decrement_value(unsigned i, inf_eps& val) {
+    lbool opt_solver::decrement_value(unsigned i, inf_eps& val) {
-        if (arith_util(m).is_real(m_objective_sorts[i].get())) {
+        push_core();
-            val -= inf_eps(inf_rational(rational(0),true));
+        expr_ref ge = mk_ge(i, val);
+        TRACE("opt", tout << ge << "\n";);
+        assert_expr(ge);
+        lbool is_sat = m_context.check(0, 0);
+        if (is_sat == l_true) {
+            set_model(i);
         }
-        else {
+        pop_core(1);
-            val -= inf_eps(inf_rational(rational(1)));
+        TRACE("opt", tout << is_sat << "\n";);
+        if (is_sat != l_true) {
+            // cop-out approximation
+            if (arith_util(m).is_real(m_objective_sorts[i].get())) {
+                val -= inf_eps(inf_rational(rational(0), true));
+            }
+            else {
+                val -= inf_eps(inf_rational(rational(1)));
+            }
+            m_valid_objectives[i] = false;
         }
-        m_valid_objectives[i] = false;
+        return is_sat;
+
     }
 
     
@@ -308,8 +322,7 @@ namespace opt {
         smt::theory_var v = m_objective_vars[i];
         return get_optimizer().value(v);
     }
-
+    
-
     expr_ref opt_solver::mk_ge(unsigned var, inf_eps const& val) {
         smt::theory_opt& opt = get_optimizer();
         smt::theory_var v = m_objective_vars[var];

src/opt/opt_solver.h

@@ -134,7 +134,8 @@ namespace opt {
                                char const * logic = "", char const * status = "unknown", char const * attributes = "");
 
     private:
-        void decrement_value(unsigned i, inf_eps& val);
+        lbool decrement_value(unsigned i, inf_eps& val);
+        void set_model(unsigned i);
     };
 }
 

src/opt/optsmt.cpp

@@ -69,10 +69,19 @@ namespace opt {
     lbool optsmt::basic_opt() {
         lbool is_sat = l_true;
 
+        expr_ref bound(m.mk_true(), m), tmp(m);
+        expr* vars[1];
+
+        solver::scoped_push _push(*m_s);
         while (is_sat == l_true && !m_cancel) {
-            is_sat = m_s->check_sat(0, 0); 
+
+            tmp = m.mk_fresh_const("b", m.mk_bool_sort());            
+            vars[0] = tmp;
+            bound = m.mk_implies(tmp, bound);
+            m_s->assert_expr(bound);
+            is_sat = m_s->check_sat(1, vars); 
             if (is_sat == l_true) {
-                update_lower();
+                bound = update_lower();
             }
         }      
         
@@ -125,17 +134,23 @@ namespace opt {
 
 
         expr_ref_vector ors(m), disj(m);
-        expr_ref fml(m), bound(m.mk_true(), m);
+        expr_ref fml(m), bound(m.mk_true(), m), tmp(m);
-        for (unsigned i = 0; i < m_upper.size(); ++i) {
+        expr* vars[1];
-            ors.push_back(m_s->mk_ge(i, m_upper[i]));
-        }
         {
-            solver::scoped_push _push(*m_s);
+            for (unsigned i = 0; i < m_upper.size(); ++i) {
+                ors.push_back(m_s->mk_ge(i, m_upper[i]));
+            }
+            
             fml = m.mk_or(ors.size(), ors.c_ptr());
-            m_s->assert_expr(fml);
+            tmp = m.mk_fresh_const("b", m.mk_bool_sort());
+            fml = m.mk_implies(tmp, fml);
+            vars[0] = tmp;
             lbool is_sat = l_true;
+
+            solver::scoped_push _push(*m_s);
             while (!m_cancel) {
-                is_sat = m_s->check_sat(0,0);
+                m_s->assert_expr(fml);
+                is_sat = m_s->check_sat(1,vars);
                 if (is_sat == l_true) {
                     disj.reset();
                     m_s->maximize_objectives(disj);
@@ -151,7 +166,9 @@ namespace opt {
                     }
                     set_max(m_lower, m_s->get_objective_values(), disj);
                     fml = m.mk_or(ors.size(), ors.c_ptr());
-                    m_s->assert_expr(fml);
+                    tmp = m.mk_fresh_const("b", m.mk_bool_sort());
+                    fml = m.mk_implies(tmp, fml);
+                    vars[0] = tmp;
                 }
                 else if (is_sat == l_undef) {
                     return l_undef;
@@ -181,7 +198,7 @@ namespace opt {
         m_upper[idx] = v;                    
     }
 
-    void optsmt::update_lower() {
+    expr_ref optsmt::update_lower() {
         expr_ref_vector disj(m);
         m_s->get_model(m_model);
         m_s->maximize_objectives(disj);
@@ -201,9 +218,7 @@ namespace opt {
         IF_VERBOSE(3, verbose_stream() << disj << "\n";);
         IF_VERBOSE(3, model_pp(verbose_stream(), *m_model););
 
-        expr_ref constraint(m);        
+        return expr_ref(m.mk_or(disj.size(), disj.c_ptr()), m);
-        constraint = m.mk_or(disj.size(), disj.c_ptr());
-        m_s->assert_expr(constraint);
     }
 
     lbool optsmt::update_upper() {
@@ -243,7 +258,7 @@ namespace opt {
                     IF_VERBOSE(2, verbose_stream() << "(optsmt lower bound for v" << m_vars[i] << " := " << m_upper[i] << ")\n";);
                     m_lower[i] = mid[i];
                     th.enable_record_conflict(0);
-                    update_lower();
+                    m_s->assert_expr(update_lower());
                     break;
                 case l_false:
                     IF_VERBOSE(2, verbose_stream() << "(optsmt conflict: " << th.conflict_minimize() << ") \n";);

src/opt/optsmt.h

@@ -80,7 +80,7 @@ namespace opt {
 
         void set_max(vector<inf_eps>& dst, vector<inf_eps> const& src, expr_ref_vector& fmls);
 
-        void update_lower();
+        expr_ref update_lower();
 
         lbool update_upper();
 

src/smt/params/smt_params_helper.pyg

@@ -51,10 +51,10 @@ def_module_params(module_name='smt',
                           ('pb.enable_simplex', BOOL, False, 'enable simplex to check rational feasibility'),
                           ('array.weak', BOOL, False, 'weak array theory'),
                           ('array.extensional', BOOL, True, 'extensional array theory'),
-						  ('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'),
+                          ('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'),
-						  ('dack.eq', BOOL, False, 'enable dynamic ackermannization for transtivity of equalities'),
+                          ('dack.eq', BOOL, False, 'enable dynamic ackermannization for transtivity of equalities'),
-						  ('dack.factor', DOUBLE, 0.1, 'number of instance per conflict'),
+                          ('dack.factor', DOUBLE, 0.1, 'number of instance per conflict'),
-						  ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'),
+                          ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'),
-						  ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
+                          ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
-						  ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded')
+                          ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded')
                           ))

src/tactic/bv/bit_blaster_tactic.cpp

@@ -19,7 +19,7 @@ Notes:
 #include"tactical.h"
 #include"bit_blaster_model_converter.h"
 #include"bit_blaster_rewriter.h"
-#include"ast_smt2_pp.h"
+#include"ast_pp.h"
 #include"model_pp.h"
 #include"rewriter_types.h"
 
@@ -82,6 +82,7 @@ class bit_blaster_tactic : public tactic {
                 }
                 if (curr != new_curr) {
                     change = true;
+                    TRACE("bit_blaster", tout << mk_pp(curr, m()) << " -> " << mk_pp(new_curr, m()) << "\n";);
                     g->update(idx, new_curr, new_pr, g->dep(idx));
                 }
             }