#6319

align use of optsmt and the new core (they should not be used together)

src/opt/opt_context.cpp

@@ -697,11 +697,26 @@ namespace opt {
         }
     }
 
+    /**
+     * Set the solver to the SAT core.
+     * It requres:
+     * - either EUF is enabled or the query is finite domain.
+     * - it is a MaxSAT query because linear optimiation is not exposed over the EUF core.
+     *   - opt_solver relies on features from the legacy core.
+     * - the MaxSAT engine does not depend on old core features (branch and bound solver for MaxSAT)
+     * - proofs are not enabled
+     * Relaxation of these filters are possible by adding functionality to the new core.
+     * - Pareto optimizaiton might already be possible with EUF = true
+     * - optsmt needs to be disetangled from the legacy core
+     */
     void context::update_solver() {
         sat_params p(m_params);
         if (!p.euf() && (!m_enable_sat || !probe_fd())) 
             return;
         
+        if (!is_maxsat_query())
+            return;
+
         if (m_maxsat_engine != symbol("maxres") &&
             m_maxsat_engine != symbol("rc2") &&
             m_maxsat_engine != symbol("rc2tot") &&
@@ -755,24 +770,29 @@ namespace opt {
         }        
     };
 
+    bool context::is_maxsat_query() {
+        for (objective& obj : m_objectives) 
+            if (obj.m_type != O_MAXSMT)
+                return false;
+        return true;
+    }
+
     bool context::probe_fd() {
         expr_fast_mark1 visited;
         is_fd proc(m);
+        if (!is_maxsat_query())
+            return false;
         try {            
             for (objective& obj : m_objectives) {
-                if (obj.m_type != O_MAXSMT) return false;
                 maxsmt& ms = *m_maxsmts.find(obj.m_id);
-                for (unsigned j = 0; j < ms.size(); ++j) {
+                for (unsigned j = 0; j < ms.size(); ++j) 
                     quick_for_each_expr(proc, visited, ms[j]);
-                }
             }
             unsigned sz = get_solver().get_num_assertions();
-            for (unsigned i = 0; i < sz; i++) {
+            for (unsigned i = 0; i < sz; i++) 
                 quick_for_each_expr(proc, visited, get_solver().get_assertion(i));
-            }
+            for (expr* f : m_hard_constraints) 
-            for (expr* f : m_hard_constraints) {
                 quick_for_each_expr(proc, visited, f);
-            }
         }
         catch (const is_fd::found_fd &) {
             return false;

src/opt/opt_context.h

@@ -330,6 +330,7 @@ namespace opt {
 
         struct is_fd;
         bool probe_fd();
+        bool is_maxsat_query();
 
         struct is_propositional_fn;
         bool is_propositional(expr* e);