add parameter incremental to ensure preprocessing does not interefere…

… with adding constraints during search

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

src/opt/opt_context.cpp

@@ -137,9 +137,6 @@ namespace opt {
         m_model_fixed(),
         m_objective_refs(m),
         m_core(m),
-        m_enable_sat(false),
-        m_is_clausal(false),
-        m_pp_neat(false),
         m_unknown("unknown")
     {
         params_ref p;
@@ -196,6 +193,8 @@ namespace opt {
 
     void context::add_hard_constraint(expr* f) {
         if (m_calling_on_model) {
+            if (!m_incremental)
+                throw default_exception("Set opt.incremental = true to allow adding constraints during search");
             get_solver().assert_expr(f);
             for (auto const& [k, v] : m_maxsmts)
                 v->reset_upper();
@@ -838,19 +837,14 @@ namespace opt {
         }
 
         goal_ref g(alloc(goal, m, true, !asms.empty()));
-        for (expr* fml : fmls) {
+        for (expr* fml : fmls) 
             g->assert_expr(fml);
-        }
-        for (expr * a : asms) {
+        for (expr * a : asms) 
             g->assert_expr(a, a);
-        }
         tactic_ref tac0 = 
             and_then(mk_simplify_tactic(m, m_params), 
                      mk_propagate_values_tactic(m),
-                     mk_solve_eqs_tactic(m),
-                     // NB: cannot ackermannize because max/min objectives would disappear
-                     // mk_ackermannize_bv_tactic(m, m_params), 
-                     // NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints
+                     m_incremental ? mk_skip_tactic() : mk_solve_eqs_tactic(m),
                      mk_simplify_tactic(m));   
         opt_params optp(m_params);
         tactic_ref tac1, tac2, tac3, tac4;
@@ -861,7 +855,7 @@ namespace opt {
             m.linearize(core, deps);           
             has_dep |= !deps.empty();
         }
-        if (optp.elim_01() && m_logic.is_null() && !has_dep) {
+        if (optp.elim_01() && m_logic.is_null() && !has_dep && !m_incremental) {
             tac1 = mk_dt2bv_tactic(m);
             tac2 = mk_lia2card_tactic(m);
             tac3 = mk_eq2bv_tactic(m);
@@ -1568,6 +1562,7 @@ namespace opt {
         m_maxsat_engine = _p.maxsat_engine();
         m_pp_neat = _p.pp_neat();
         m_pp_wcnf = _p.pp_wcnf();
+        m_incremental = _p.incremental();
     }
 
     std::string context::to_string()  {

src/opt/opt_context.h

@@ -194,11 +194,12 @@ namespace opt {
         func_decl_ref_vector         m_objective_refs;
         expr_ref_vector              m_core;
         tactic_ref                   m_simplify;
-        bool                         m_enable_sat { true } ;
-        bool                         m_enable_sls { false };
-        bool                         m_is_clausal { false };
-        bool                         m_pp_neat { true };
-        bool                         m_pp_wcnf { false };
+        bool                         m_enable_sat = true;
+        bool                         m_enable_sls = false;
+        bool                         m_is_clausal = false;
+        bool                         m_pp_neat = false;
+        bool                         m_pp_wcnf = false;
+        bool                         m_incremental = false;
         symbol                       m_maxsat_engine;
         symbol                       m_logic;
         svector<symbol>              m_labels;

src/opt/opt_params.pyg

@@ -15,6 +15,7 @@ def_module_params('opt',
                           ('enable_core_rotate', BOOL, False, 'enable core rotation to both sample cores and correction sets'),
                           ('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'),
                           ('elim_01', BOOL, True, 'eliminate 01 variables'),
+			  ('incremental', BOOL, False, 'set incremental mode. It disables pre-processing and enables adding constraints in model event handler'),
                           ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'),
                           ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'),
                           ('pp.wcnf', BOOL, False, 'print maxsat benchmark into wcnf format'),