including all touched tautology literals each round

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

src/sat/sat_simplifier.cpp

@@ -1069,8 +1069,8 @@ namespace sat {
         // Find literals that are in the intersection of all resolvents with l.
         //
         bool resolution_intersection(literal l, bool adding) {
+            unsigned tsz = m_tautology.size();
             reset_intersection();
-            m_tautology.reset();
             if (!process_var(l.var())) return false;
             bool first = true;
             VERIFY(s.value(l) == l_undef);
@@ -1086,6 +1086,7 @@ namespace sat {
                     }
                     if (!first || s.is_marked(lit)) {
                         reset_intersection();
+                        m_tautology.shrink(tsz);
                         return false; // intersection is empty or does not add anything new.
                     }
                     first = false;
@@ -1122,22 +1123,30 @@ namespace sat {
                         for (literal lit : m_new_intersection) 
                             add_intersection(lit);
                     }
-                    if (m_intersection.empty()) 
+                    if (m_intersection.empty()) {
+                        m_tautology.shrink(tsz);
                         return false;
+                    }
                 }
             }
+            if (m_intersection.empty()) {
+                m_tautology.shrink(tsz);
+            }
             // if (first) IF_VERBOSE(0, verbose_stream() << "taut: " << m_tautology << "\n";);
             return first;
         }
 
         bool check_abce_tautology(literal l) {
-            m_tautology.reset();
+            unsigned tsz = m_tautology.size();
             if (!process_var(l.var())) return false;
             for (watched & w : s.get_wlist(l)) {
                 if (w.is_binary_non_learned_clause()) {
                     literal lit = w.get_literal();
                     VERIFY(lit != ~l);
-                    if (!s.is_marked(~lit)) return false;
+                    if (!s.is_marked(~lit)) {
+                        m_tautology.shrink(tsz);
+                        return false;
+                    }
                     m_tautology.push_back(~lit);
                 }
             }
@@ -1153,7 +1162,10 @@ namespace sat {
                         break;
                     }
                 }
-                if (!tautology) return false;
+                if (!tautology) {
+                    m_tautology.shrink(tsz);
+                    return false;
+                }
             }
             return true;
         }
@@ -1352,6 +1364,7 @@ namespace sat {
             unsigned sz = 0, sz0 = m_covered_clause.size();     
             for (literal l : m_covered_clause) s.mark_visited(l);
             shuffle<literal>(m_covered_clause.size(), m_covered_clause.c_ptr(), s.s.m_rand);
+            m_tautology.reset();
             m_mc.stackv().reset();
             m_ala_qhead = 0;
 
@@ -1394,7 +1407,6 @@ namespace sat {
                          * tautology depends on resolution intersection. 
                          * literals used for resolution intersection may have to be flipped.
                          */
-                        m_tautology.reset();
                         for (literal l : m_covered_clause) {
                             m_tautology.push_back(l);
                             s.mark_visited(l);
@@ -1610,6 +1622,7 @@ namespace sat {
           Then the following binary clause is blocked: l \/ ~l'
          */
         void bca(literal l) {
+            m_tautology.reset();
             if (resolution_intersection(l, true)) {
                 // this literal is pure. 
                 return;

src/tactic/portfolio/CMakeLists.txt

@@ -18,6 +18,8 @@ z3_add_component(portfolio
     smtlogic_tactics
     subpaving_tactic
     ufbv_tactic
+  PYG_FILES
+    parallel_params.pyg
   TACTIC_HEADERS
     default_tactic.h
     fd_solver.h

src/tactic/portfolio/parallel_tactic.cpp

@@ -159,8 +159,6 @@ class parallel_tactic : public tactic {
         ref<solver>     m_solver;                 // solver state
         unsigned        m_depth;                  // number of nested calls to cubing
         double          m_width;                  // estimate of fraction of problem handled by state
-        unsigned        m_cube_cutoff;            // saved configuration value
-        double          m_cube_fraction;          // saved configuration value
         unsigned        m_restart_max;            // saved configuration value
 
         expr_ref_vector cube_literals(expr* cube) {
@@ -185,8 +183,6 @@ class parallel_tactic : public tactic {
             m_depth(0),
             m_width(1.0)
         {
-            m_cube_cutoff   = p.get_uint("sat.lookahead.cube.cutoff", 8);
-            m_cube_fraction = p.get_double("sat.lookahead.cube.fraction", 0.4);
             m_restart_max   = p.get_uint("sat.restart.max", 10);
         }
 
@@ -280,17 +276,7 @@ class parallel_tactic : public tactic {
         }        
 
         void set_cube_params() {
-            unsigned cutoff = m_cube_cutoff;
-            double fraction = m_cube_fraction; 
-            if (true || (m_depth == 1 && cutoff > 0)) {
-                m_params.set_sym("lookahead.cube.cutoff", symbol("depth"));
-                m_params.set_uint("lookahead.cube.depth", std::max(m_depth, 10u));
-            }
-            else {
-                m_params.set_sym("lookahead.cube.cutoff", symbol("adaptive_psat"));
-                m_params.set_double("lookahead.cube.fraction", fraction);
-            }
-            get_solver().updt_params(m_params);
+            // get_solver().updt_params(m_params);
         }
         
         void set_conquer_params() {            

src/tactic/smtlogics/qfbv_tactic.cpp

@@ -29,6 +29,7 @@ Notes:
 #include "tactic/aig/aig_tactic.h"
 #include "sat/tactic/sat_tactic.h"
 #include "tactic/portfolio/parallel_tactic.h"
+#include "tactic/portfolio/parallel_params.hpp"
 #include "ackermannization/ackermannize_bv_tactic.h"
 
 #define MEMLIMIT 300
@@ -128,11 +129,11 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
 
 
 tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
-
+    parallel_params pp(p);
+    bool use_parallel = pp.enable();
     tactic * new_sat = cond(mk_produce_proofs_probe(),
                             and_then(mk_simplify_tactic(m), mk_smt_tactic()),
-                            //mk_parallel_tactic(m, p));
-                            mk_sat_tactic(m));
+                            use_parallel ? mk_parallel_tactic(m, p): mk_sat_tactic(m));
 
     return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic());