adding symba designated strategy (back?) to optsmt

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

src/opt/opt_context.cpp

@@ -435,6 +435,7 @@ namespace opt {
     }
 
     void context::init_solver() {
+        setup_arith_solver();
         #pragma omp critical (opt_context)
         {
             m_opt_solver = alloc(opt_solver, m, m_params, m_fm);
@@ -443,6 +444,16 @@ namespace opt {
         }
     }
 
+    void context::setup_arith_solver() {
+        opt_params p(m_params);        
+        if (p.optsmt_engine() == symbol("symba") ||
+            p.optsmt_engine() == symbol("farkas")) {
+            std::stringstream strm;
+            strm << AS_OPTINF;
+            gparams::set("smt.arith.solver", strm.str().c_str());
+        }
+    }
+
     void context::update_solver() {
         if (!m_enable_sat || !probe_bv()) {
             return;

src/opt/opt_context.h

@@ -224,6 +224,7 @@ namespace opt {
 
         void    init_solver();
         void    update_solver();
+        void    setup_arith_solver();
         void    add_maxsmt(symbol const& id);
         void    set_simplify(tactic *simplify);
         void    set_pareto(pareto_base* p);        

src/opt/opt_params.pyg

@@ -2,7 +2,7 @@ def_module_params('opt',
                   description='optimization parameters',
                   export=True,
                   params=(('timeout', UINT, UINT_MAX, 'set timeout'),
-                          ('engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"),
+                          ('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"),
 	                  ('maxsat_engine', SYMBOL, 'wmax', "select engine for maxsat: 'fu_malik', 'core_maxsat', 'wmax', 'pbmax', 'maxres', 'bcd2', 'wpm2', 'sls', 'maxhs'"),
                           ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"),
                           ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),

src/opt/optsmt.cpp

@@ -107,6 +107,62 @@ namespace opt {
         return l_true;        
     }
 
+    lbool optsmt::symba_opt() {
+        smt::theory_opt& opt = m_s->get_optimizer();
+
+        if (typeid(smt::theory_inf_arith) != typeid(opt)) {
+            return l_undef;
+        }
+
+
+        expr_ref_vector ors(m), disj(m);
+        expr_ref or(m), bound(m.mk_true(), m);
+        for (unsigned i = 0; i < m_upper.size(); ++i) {
+            ors.push_back(m_s->mk_ge(i, m_upper[i]));
+        }
+        {
+            solver::scoped_push _push(*m_s);
+            or = m.mk_or(ors.size(), ors.c_ptr());
+            m_s->assert_expr(or);
+            lbool is_sat = l_true;
+            while (!m_cancel) {
+                is_sat = m_s->check_sat(0,0);
+                if (is_sat == l_true) {
+                    disj.reset();
+                    m_s->maximize_objectives(disj);
+                    m_s->get_model(m_model);                   
+                    set_max(m_lower, m_s->get_objective_values()); 
+                    for (unsigned i = 0; i < ors.size(); ++i) {
+                        expr_ref tmp(m);
+                        m_model->eval(ors[i].get(), tmp);
+                        if (m.is_true(tmp)) {
+                            m_lower[i] = m_upper[i];
+                            ors[i] = m.mk_false();
+                        }
+                        if (m.is_false(ors[i].get())) {
+                            disj[i] = m.mk_false();
+                        }
+                    }
+                    or = m.mk_or(ors.size(), ors.c_ptr());
+                    bound = m.mk_or(disj.size(), disj.c_ptr());
+                    m_s->assert_expr(or);
+                }
+                else if (is_sat == l_undef) {
+                    return l_undef;
+                }
+                else {
+                    break;
+                }
+            }
+        }
+        m_s->assert_expr(bound);
+        
+        if (m_cancel) {
+            return l_undef;
+        }
+        return basic_opt();
+    }
+
     void optsmt::update_lower(unsigned idx, inf_eps const& v, bool override) {
         if (m_lower[idx] < v || override) {
             m_lower[idx] = v;            
@@ -124,13 +180,13 @@ namespace opt {
         m_s->maximize_objectives(disj);
         m_s->get_model(m_model);
         set_max(m_lower, m_s->get_objective_values());
-        IF_VERBOSE(1, 
+        TRACE("opt",
-                   for (unsigned i = 0; i < m_lower.size(); ++i) {
+              for (unsigned i = 0; i < m_lower.size(); ++i) {
-                       verbose_stream() << m_lower[i] << " ";
+                  tout << m_lower[i] << " ";
-                   }
+              }
-                   verbose_stream() << "\n";
+              tout << "\n";
-                   model_pp(verbose_stream(), *m_model);
+              model_pp(tout, *m_model);
-                   );
+              );
         expr_ref constraint(m);        
         constraint = m.mk_or(disj.size(), disj.c_ptr());
         m_s->assert_expr(constraint);
@@ -171,13 +227,13 @@ namespace opt {
                 lbool is_sat = m_s->check_sat(1, bounds.c_ptr() + i);
                 switch(is_sat) {
                 case l_true:
-                    IF_VERBOSE(2, verbose_stream() << "Setting lower bound for v" << m_vars[i] << " to " << m_upper[i] << "\n";);
+                    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();
                     break;
                 case l_false:
-                    IF_VERBOSE(2, verbose_stream() << "conflict: " << th.conflict_minimize() << "\n";);
+                    IF_VERBOSE(2, verbose_stream() << "(optsmt conflict: " << th.conflict_minimize() << ") \n";);
                     if (!th.conflict_minimize().is_finite()) {
                         // bounds is not in the core. The context is unsat.
                         m_upper[i] = m_lower[i];
@@ -288,13 +344,15 @@ namespace opt {
         }
         // assertions added during search are temporary.
         solver::scoped_push _push(*m_s);
-        if (m_engine == symbol("farkas")) {
+        if (m_optsmt_engine == symbol("farkas")) {
             is_sat = farkas_opt();
         }
+        else if (m_optsmt_engine == symbol("symba")) {
+            is_sat = symba_opt();
+        }
         else {
             is_sat = basic_opt();
         }
-
         return is_sat;
     }
 
@@ -337,7 +395,7 @@ namespace opt {
 
     void optsmt::updt_params(params_ref& p) {
         opt_params _p(p);
-        m_engine = _p.engine();        
+        m_optsmt_engine = _p.optsmt_engine();        
     }
 
     void optsmt::reset() {

src/opt/optsmt.h

@@ -35,7 +35,7 @@ namespace opt {
         vector<inf_eps>  m_upper;
         app_ref_vector   m_objs;
         svector<smt::theory_var> m_vars;
-        symbol           m_engine;
+        symbol           m_optsmt_engine;
         model_ref        m_model;
     public:
         optsmt(ast_manager& m): m(m), m_s(0), m_cancel(false), m_objs(m) {}
@@ -67,6 +67,8 @@ namespace opt {
         
         lbool basic_opt();
 
+        lbool symba_opt();
+
         lbool basic_lex(unsigned idx, bool is_maximize);
 
         lbool farkas_opt();

src/smt/smt_setup.cpp

@@ -703,7 +703,12 @@ namespace smt {
     }
 
     void setup::setup_mi_arith() {
-        m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
+        if (m_params.m_arith_mode == AS_OPTINF) {
+            m_context.register_plugin(alloc(smt::theory_inf_arith, m_manager, m_params));            
+        }
+        else {
+            m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
+        }
     }
 
     void setup::setup_arith() {