prepare for inprocessing

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

src/params/smt_parallel_params.pyg

@@ -8,7 +8,7 @@ def_module_params('smt_parallel',
                         ('frugal_cube_only', BOOL, False, 'only apply frugal cube strategy'),
                         ('relevant_units_only', BOOL, True, 'only share relvant units'),
                         ('max_conflict_mul', DOUBLE, 1.5, 'increment multiplier for max-conflicts'),
-                        ('share_units_initial_only', BOOL, False, 'share only initial Boolean atoms as units'),
+                        ('share_units_initial_only', BOOL, True, 'share only initial Boolean atoms as units'),
                         ('cube_initial_only', BOOL, False, 'cube only on initial Boolean atoms'),
                         ('max_cube_depth', UINT, 20, 'maximum depth (size) of a cube to share'),
                         ('max_greedy_cubes', UINT, 1000, 'maximum number of cube to greedily share before switching to frugal'),
@@ -19,5 +19,6 @@ def_module_params('smt_parallel',
                         ('beam_search', BOOL, False, 'use beam search with PQ to rank cubes given to threads'),
                         ('explicit_hardness', BOOL, False, 'use explicit hardness metric for cube'),
                         ('cubetree', BOOL, False, 'use cube tree data structure for storing cubes'),
-                        ('searchtree', BOOL, False, 'use search tree implementation (parallel2)')
+                        ('searchtree', BOOL, False, 'use search tree implementation (parallel2)'),
+                        ('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification')
               ))

src/smt/smt_context.h

@@ -19,6 +19,7 @@ Revision History:
 #pragma once
 
 #include "ast/quantifier_stat.h"
+#include "ast/simplifiers/dependent_expr_state.h"
 #include "smt/smt_clause.h"
 #include "smt/smt_setup.h"
 #include "smt/smt_enode.h"
@@ -135,6 +136,8 @@ namespace smt {
         bool                        m_internalizing_assertions = false;
         lbool                       m_internal_completed = l_undef;
 
+        scoped_ptr<dependent_expr_simplifier>  m_simplifier;
+
 
         // -----------------------------------
         //

src/smt/smt_parallel2.cpp

@@ -214,6 +214,7 @@ namespace smt {
         m_config.m_explicit_hardness = pp.explicit_hardness();
         m_config.m_cubetree = pp.cubetree();
         m_config.m_max_cube_depth = pp.max_cube_depth();
+        m_config.m_inprocessing = pp.inprocessing();
 
         // don't share initial units
         ctx->pop_to_base_lvl();
@@ -248,6 +249,23 @@ namespace smt {
         m_num_shared_units = sz;
     }
 
+    void parallel2::worker::simplify() {
+        // first attempt: one-shot simplification of the context.
+        if (!m_config.m_inprocessing)
+            return;
+        m_config.m_inprocessing = true;
+        if (!ctx->m_simplifier) {
+            // create a simplifier if none exists
+        }
+
+        // extract assertions from ctx.
+        // feed them to the simplifier
+        // extract simplified assertions from the simplifier
+        // create a new context with the simplified assertions
+        // update ctx with the new context.
+
+    }
+
     void parallel2::worker::collect_statistics(::statistics& st) const {
         ctx->collect_statistics(st);
     }

src/smt/smt_parallel2.h

@@ -136,6 +136,7 @@ namespace smt {
                 bool m_beam_search = false;
                 bool m_explicit_hardness = false;
                 bool m_cubetree = false;
+                bool m_inprocessing = false;
             };
 
             using node = search_tree::node<cube_config>;
@@ -169,6 +170,8 @@ namespace smt {
             void backtrack(expr_ref_vector const& core, node* n);
             void split(node* n, expr* atom);
 
+            void simplify();
+
         public:
             worker(unsigned id, parallel2& p, expr_ref_vector const& _asms);
             void run();