add output for inprocessing

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

src/sat/sat_config.cpp

@@ -76,6 +76,7 @@ namespace sat {
         m_restart_max     = p.restart_max();
         m_propagate_prefetch = p.propagate_prefetch();
         m_inprocess_max   = p.inprocess_max();
+        m_inprocess_out   = p.inprocess_out();
 
         m_random_freq     = p.random_freq();
         m_random_seed     = p.random_seed();
@@ -108,6 +109,7 @@ namespace sat {
         m_cut_lut           = p.cut_lut();
         m_cut_xor           = p.cut_xor();
         m_cut_dont_cares    = p.cut_dont_cares();
+        m_cut_force         = p.cut_force();
         m_lookahead_simplify = p.lookahead_simplify();
         m_lookahead_double = p.lookahead_double();
         m_lookahead_simplify_bca = p.lookahead_simplify_bca();

src/sat/sat_config.h

@@ -105,6 +105,7 @@ namespace sat {
         double             m_fast_glue_avg;
         double             m_slow_glue_avg;
         unsigned           m_inprocess_max;
+        symbol             m_inprocess_out;
         double             m_random_freq;
         unsigned           m_random_seed;
         unsigned           m_burst_search;
@@ -125,6 +126,7 @@ namespace sat {
         bool               m_cut_lut;
         bool               m_cut_xor;
         bool               m_cut_dont_cares;
+        bool               m_cut_force;
         bool               m_anf_simplify;
         unsigned           m_anf_delay;
         bool               m_anf_exlin;

src/sat/sat_cut_simplifier.cpp

@@ -157,6 +157,7 @@ namespace sat {
 
     void cut_simplifier::operator()() {
 
+        bool force = s.m_config.m_cut_force;
         report _report(*this);
         TRACE("cut_simplifier", s.display(tout););
         unsigned n = 0, i = 0;
@@ -167,7 +168,7 @@ namespace sat {
             aig2clauses();
             ++i;
         }
-        while (i*i < m_stats.m_num_calls && n < m_stats.m_num_eqs + m_stats.m_num_units);
+        while ((force || i*i < m_stats.m_num_calls) && n < m_stats.m_num_eqs + m_stats.m_num_units);
     }
 
     /**

src/sat/sat_params.pyg

@@ -21,6 +21,7 @@ def_module_params('sat',
                           ('restart.emaslowglue', DOUBLE, 1e-5, 'ema alpha factor for slow moving average'),
                           ('variable_decay', UINT, 110, 'multiplier (divided by 100) for the VSIDS activity increment'),
                           ('inprocess.max', UINT, UINT_MAX, 'maximal number of inprocessing passes'),
+                          ('inprocess.out', SYMBOL, '', 'file to dump result of the first inprocessing step and exit'),
                           ('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'),
                           ('branching.anti_exploration', BOOL, False, 'apply anti-exploration heuristic for branch selection'),
                           ('random_freq', DOUBLE, 0.01, 'frequency of random case splits'),
@@ -78,6 +79,7 @@ def_module_params('sat',
                           ('cut.lut',   BOOL, False, 'extract luts from clauses for cut simplification'),
                           ('cut.xor',   BOOL, False, 'extract xors from clauses for cut simplification'),
                           ('cut.dont_cares', BOOL, True, 'integrate dont cares with cuts'),
+                          ('cut.force', BOOL, False, 'force redoing cut-enumeration until a fixed-point'),
                           ('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'),
                           # - depth: the maximal cutoff is fixed to the value of lookahead.cube.depth.
                           #          So if the value is 10, at most 1024 cubes will be generated of length 10.

src/sat/sat_solver.cpp

@@ -1934,6 +1934,14 @@ namespace sat {
         if (m_cut_simplifier && m_simplifications > m_config.m_cut_delay && !inconsistent()) {
             (*m_cut_simplifier)();
         }
+
+        if (m_config.m_inprocess_out.is_non_empty_string()) {
+            std::ofstream fout(m_config.m_inprocess_out.str());
+            if (fout) {
+                display_dimacs(fout);
+            }
+            throw solver_exception("output generated");
+        }
     }
 
     bool solver::set_root(literal l, literal r) {