handle better cancellation for parallel, switch between cube mode and…

… base level mode in smt.threads, expose parameters to control theory_bv and phase caching

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/smt/params/smt_params.cpp

@@ -30,6 +30,8 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_clause_proof = p.clause_proof();
     m_phase_selection = static_cast<phase_selection>(p.phase_selection());
     if (m_phase_selection > PS_THEORY) throw default_exception("illegal phase selection numeral");
+    m_phase_caching_on = p.phase_caching_on();
+    m_phase_caching_off = p.phase_caching_off();
     m_restart_strategy = static_cast<restart_strategy>(p.restart_strategy());
     if (m_restart_strategy > RS_ARITHMETIC) throw default_exception("illegal restart strategy numeral");
     m_restart_factor = p.restart_factor();
@@ -41,8 +43,10 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
     m_max_conflicts = p.max_conflicts();
     m_restart_max   = p.restart_max();
+    m_cube_depth    = p.cube_depth();
     m_threads       = p.threads();
     m_threads_max_conflicts  = p.threads_max_conflicts();
+    m_threads_cube_frequency = p.threads_cube_frequency();
     m_core_validate = p.core_validate();
     m_logic = _p.get_sym("logic", m_logic);
     m_string_solver = p.string_solver();
@@ -105,8 +109,10 @@ void smt_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_phase_caching_off);
     DISPLAY_PARAM(m_minimize_lemmas);
     DISPLAY_PARAM(m_max_conflicts);
+    DISPLAY_PARAM(m_cube_depth);
     DISPLAY_PARAM(m_threads);
     DISPLAY_PARAM(m_threads_max_conflicts);
+    DISPLAY_PARAM(m_threads_cube_frequency);
     DISPLAY_PARAM(m_simplify_clauses);
     DISPLAY_PARAM(m_tick);
     DISPLAY_PARAM(m_display_features);

src/smt/params/smt_params.h

@@ -102,8 +102,10 @@ struct smt_params : public preprocessor_params,
     bool             m_minimize_lemmas;
     unsigned         m_max_conflicts;
     unsigned         m_restart_max;
+    unsigned         m_cube_depth;
     unsigned         m_threads;
     unsigned         m_threads_max_conflicts;
+    unsigned         m_threads_cube_frequency;
     bool             m_simplify_clauses;
     unsigned         m_tick;
     bool             m_display_features;
@@ -251,12 +253,14 @@ struct smt_params : public preprocessor_params,
         m_clause_decay(1),
         m_random_initial_activity(IA_RANDOM_WHEN_SEARCHING),
         m_phase_selection(PS_CACHING_CONSERVATIVE),
-        m_phase_caching_on(400),
+        m_phase_caching_on(700),
         m_phase_caching_off(100),
         m_minimize_lemmas(true),
         m_max_conflicts(UINT_MAX),
+        m_cube_depth(1),
         m_threads(1),
         m_threads_max_conflicts(UINT_MAX),
+        m_threads_cube_frequency(2),
         m_simplify_clauses(true),
         m_tick(1000),
         m_display_features(false),

src/smt/params/smt_params_helper.pyg

@@ -11,6 +11,8 @@ def_module_params(module_name='smt',
                           ('restricted_quasi_macros', BOOL, False, 'try to find universally quantified formulas that are restricted quasi-macros'),
                           ('ematching', BOOL, True, 'E-Matching based quantifier instantiation'),
                           ('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences, 7 - theory'),
+	                  ('phase_caching_on', UINT, 400, 'number of conflicts while phase caching is on'),
+	                  ('phase_caching_off', UINT, 100, 'number of conflicts while phase caching is off'),
                           ('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'),
                           ('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the current restart threshold'),
                           ('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity'),
@@ -20,8 +22,10 @@ def_module_params(module_name='smt',
                           ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
                           ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'),
                           ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
+	                  ('cube_depth', UINT, 1, 'cube depth.'),
                           ('threads', UINT, 1, 'maximal number of parallel threads.'),
                           ('threads.max_conflicts', UINT, 400, 'maximal number of conflicts between rounds of cubing for parallel SMT'),
+                          ('threads.cube_frequency', UINT, 2, 'frequency for using cubing'), 
                           ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
                           ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
                           ('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'),
@@ -40,6 +44,8 @@ def_module_params(module_name='smt',
                           ('induction', BOOL, False, 'enable generation of induction lemmas'),
                           ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
                           ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
+	                  ('bv.eq_axioms', BOOL, True, 'add dynamic equality axioms'),
+                          ('bv.watch_diseq', BOOL, False, 'use watch lists instead of eager axioms for bit-vectors'),
                           ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
                           ('arith.cheap_eqs', BOOL, True, 'false - do not run, true - run cheap equality heuristic'),
                           ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),

src/smt/params/theory_bv_params.cpp

@@ -26,6 +26,7 @@ void theory_bv_params::updt_params(params_ref const & _p) {
     m_hi_div0 = rp.hi_div0();
     m_bv_reflect = p.bv_reflect();
     m_bv_enable_int2bv2int = p.bv_enable_int2bv(); 
+    m_bv_eq_axioms = p.bv_eq_axioms();
 }
 
 #define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
@@ -36,6 +37,7 @@ void theory_bv_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_bv_reflect);
     DISPLAY_PARAM(m_bv_lazy_le);
     DISPLAY_PARAM(m_bv_cc);
+    DISPLAY_PARAM(m_bv_eq_axioms);
     DISPLAY_PARAM(m_bv_blast_max_size);
     DISPLAY_PARAM(m_bv_enable_int2bv2int);
 }

src/smt/params/theory_bv_params.h

@@ -31,16 +31,20 @@ struct theory_bv_params {
     bool         m_bv_reflect;
     bool         m_bv_lazy_le;
     bool         m_bv_cc;
+    bool         m_bv_eq_axioms;
     unsigned     m_bv_blast_max_size;
     bool         m_bv_enable_int2bv2int;
+    bool         m_bv_watch_diseq;
     theory_bv_params(params_ref const & p = params_ref()):
         m_bv_mode(BS_BLASTER),
         m_hi_div0(false),
         m_bv_reflect(true),
         m_bv_lazy_le(false),
         m_bv_cc(false),
+        m_bv_eq_axioms(true),
         m_bv_blast_max_size(INT_MAX),
-        m_bv_enable_int2bv2int(true) {
+        m_bv_enable_int2bv2int(true),
+        m_bv_watch_diseq(false) {
         updt_params(p);
     }
 

src/smt/smt_context.cpp

@@ -3963,6 +3963,7 @@ namespace smt {
         }
     }
 
+
     bool context::resolve_conflict() {
         m_stats.m_num_conflicts++;
         m_num_conflicts ++;

src/smt/smt_context.h

@@ -893,7 +893,11 @@ namespace smt {
 
         void mk_clause(literal l1, literal l2, literal l3, justification * j);
 
-        void mk_th_axiom(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params = 0, parameter * params = nullptr);
+        void context::mk_th_clause(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params, parameter * params, clause_kind k);
+
+        void mk_th_axiom(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params = 0, parameter * params = nullptr) {
+            mk_th_clause(tid, num_lits, lits, num_params, params, CLS_TH_AXIOM);
+        }
 
         void mk_th_axiom(theory_id tid, literal l1, literal l2, unsigned num_params = 0, parameter * params = nullptr);
 
@@ -903,6 +907,24 @@ namespace smt {
             mk_th_axiom(tid, ls.size(), ls.c_ptr(), num_params, params);
         }
 
+        void mk_th_lemma(theory_id tid, literal l1, literal l2, unsigned num_params = 0, parameter * params = nullptr) {
+            literal ls[2] = { l1, l2 };
+            mk_th_lemma(tid, 2, ls, num_params, params);
+        }
+
+        void mk_th_lemma(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params = 0, parameter * params = nullptr) {
+            literal ls[3] = { l1, l2, l3 };
+            mk_th_lemma(tid, 3, ls, num_params, params);
+        }
+
+        void mk_th_lemma(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params = 0, parameter * params = nullptr) {
+            mk_th_clause(tid, num_lits, lits, num_params, params, CLS_TH_LEMMA);
+        }
+
+        void mk_th_lemma(theory_id tid, literal_vector const& ls, unsigned num_params = 0, parameter * params = nullptr) {
+            mk_th_lemma(tid, ls.size(), ls.c_ptr(), num_params, params);
+        }
+
         /*
          * Provide a hint to the core solver that the specified literals form a "theory case split".
          * The core solver will enforce the condition that exactly one of these literals can be
@@ -1209,6 +1231,7 @@ namespace smt {
 
         virtual bool resolve_conflict();
 
+
         // -----------------------------------
         //
         // Propagation

src/smt/smt_internalizer.cpp

@@ -1488,7 +1488,7 @@ namespace smt {
         mk_clause(3, ls, j);
     }
 
-    void context::mk_th_axiom(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params, parameter * params) {
+    void context::mk_th_clause(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params, parameter * params, clause_kind k) {
         justification * js = nullptr;
         TRACE("mk_th_axiom", display_literals_verbose(tout, num_lits, lits) << "\n";);
 
@@ -1501,7 +1501,7 @@ namespace smt {
             SASSERT(tmp.size() == num_lits);
             display_lemma_as_smt_problem(tmp.size(), tmp.c_ptr(), false_literal, m_fparams.m_logic);
         }
-        mk_clause(num_lits, lits, js, CLS_TH_AXIOM);
+        mk_clause(num_lits, lits, js, k);
     }
 
     void context::mk_th_axiom(theory_id tid, literal l1, literal l2, unsigned num_params, parameter * params) {

src/smt/smt_kernel.cpp

@@ -204,6 +204,11 @@ namespace smt {
             lookahead lh(m_kernel);
             return lh.choose();
         }
+
+        expr_ref_vector cubes(unsigned depth) {
+            lookahead lh(m_kernel);
+            return lh.choose_rec(depth);
+        }
 
         void collect_statistics(::statistics & st) const {
             m_kernel.collect_statistics(st);
@@ -379,6 +384,10 @@ namespace smt {
         return m_imp->next_cube();
     }        
 
+    expr_ref_vector kernel::cubes(unsigned depth) {
+        return m_imp->cubes(depth);
+    }        
+
     std::ostream& kernel::display(std::ostream & out) const {
         m_imp->display(out);
         return out;

src/smt/smt_kernel.h

@@ -218,6 +218,11 @@ namespace smt {
         */
         expr_ref next_cube();
 
+        /**
+           \brief return up to 2^depth cubes to case split on.
+        */
+        expr_ref_vector cubes(unsigned depth);
+
         /**
            \brief retrieve upper/lower bound for arithmetic term, if it is implied.
            retrieve implied values if terms are fixed to a value.

src/smt/smt_lookahead.cpp

@@ -64,7 +64,7 @@ namespace smt {
         }
     };
 
-    expr_ref lookahead::choose() {
+    expr_ref lookahead::choose(unsigned budget) {
         ctx.pop_to_base_lvl();
         unsigned sz = ctx.m_bool_var2expr.size();
         bool_var best_v = null_bool_var;
@@ -79,9 +79,12 @@ namespace smt {
         compare comp(ctx);
         std::sort(vars.begin(), vars.end(), comp);
 
-        unsigned nf = 0, nc = 0, ns = 0, bound = 2000, n = 0;
+        unsigned nf = 0, nc = 0, ns = 0, n = 0;
         for (bool_var v : vars) {
-            if (!ctx.bool_var2expr(v)) continue;
+            if (!ctx.bool_var2expr(v)) 
+                continue;
+            if (!m.inc())
+                break;
             literal lit(v, false);
             ctx.propagate();
             if (ctx.inconsistent())
@@ -116,16 +119,22 @@ namespace smt {
             }
             double score = score1 + score2 + 1024*score1*score2;
 
-            if (score > best_score || (score == best_score && ctx.get_random_value() % (++n) == 0)) {
-                if (score > best_score) n = 0;
+            if (score <= 1.1*best_score && best_score <= 1.1*score) {
+                if (ctx.get_random_value() % (++n) == 0) {
+                    best_score = score;
+                    best_v = v;
+                }
+                ns = 0;
+            }
+            else if (score > best_score && (ctx.get_random_value() % 2) == 0) {
+                n = 0;
                 best_score = score;
                 best_v = v;
-                bound += ns;
                 ns = 0;
-            }
+            } 
             ++nc;
             ++ns;
-            if (ns > bound) {
+            if (ns > budget) {
                 break;
             }
         }
@@ -141,4 +150,38 @@ namespace smt {
         }
         return result;
     }
+
+    expr_ref_vector lookahead::choose_rec(unsigned depth) {
+        expr_ref_vector trail(m), result(m);
+        choose_rec(trail, result, depth, 2000);
+        return result;
+    }
+
+    void lookahead::choose_rec(expr_ref_vector & trail, expr_ref_vector& result, unsigned depth, unsigned budget) {
+
+        expr_ref r = choose(budget);
+        if (m.is_true(r)) 
+            result.push_back(mk_and(trail));
+        else if (m.is_false(r))
+            ;
+        else {
+            auto recurse = [&]() {
+                trail.push_back(r);
+                if (depth <= 1 || !m.inc()) {
+                    result.push_back(mk_and(trail));
+                }
+                else {
+                    ctx.push();
+                    ctx.assert_expr(r);
+                    ctx.propagate();
+                    choose_rec(trail, result, depth-1, 2 * (budget / 3));
+                    ctx.pop(1);
+                }
+                trail.pop_back();
+            };
+            recurse();
+            r = m.mk_not(r);
+            recurse();
+        }
+    }
 }

src/smt/smt_lookahead.h

@@ -32,9 +32,14 @@ namespace smt {
 
         double get_score();
 
+        void choose_rec(expr_ref_vector& trail, expr_ref_vector& result, unsigned depth, unsigned budget);
+
     public:
         lookahead(context& ctx);
 
-        expr_ref choose();
+        expr_ref choose(unsigned budget = 2000);
+
+        expr_ref_vector choose_rec(unsigned depth);
+
     };
 }

src/smt/smt_parallel.cpp

@@ -136,6 +136,7 @@ namespace smt {
                 }
                 unit_lim[i] = sz;
             }
+            IF_VERBOSE(1, verbose_stream() << "(smt.thread :units " << sz << ")\n");
         };
 
         std::mutex mux;
@@ -148,12 +149,12 @@ namespace smt {
                 expr_ref c(pm);
 
                 pctx.get_fparams().m_max_conflicts = std::min(thread_max_conflicts, max_conflicts);
-                if (num_rounds > 0) {
+                if (num_rounds > 0 && (pctx.get_fparams().m_threads_cube_frequency % num_rounds) == 0) {
                     cube(pctx, lasms, c);
                 }
                 IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i; 
                            if (num_rounds > 0) verbose_stream() << " :round " << num_rounds;
-                           if (c) verbose_stream() << " :cube: " << mk_bounded_pp(c, pm, 3);
+                           if (c) verbose_stream() << " :cube " << mk_bounded_pp(c, pm, 3);
                            verbose_stream() << ")\n";);
                 lbool r = pctx.check(lasms.size(), lasms.c_ptr());
 
@@ -164,6 +165,7 @@ namespace smt {
                     return;
                 }                
                 else if (r == l_false && pctx.unsat_core().contains(c)) {
+                    IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i << " :learn " << mk_bounded_pp(c, pm, 3) << ")");
                     pctx.assert_expr(mk_not(mk_and(pctx.unsat_core())));
                     return;
                 }