preparing for more efficient asymmetric branching

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

src/api/python/z3/z3.py

@@ -6335,7 +6335,7 @@ class Solver(Z3PPObject):
 
     def from_string(self, s):
         """Parse assertions from a string"""
-        Z3_solver_from_string(self.ctx.ref(), self.solver, filename)
+        Z3_solver_from_string(self.ctx.ref(), self.solver, s)
         
     def assertions(self):
         """Return an AST vector containing all added constraints.

src/sat/sat_asymm_branch.cpp

@@ -56,25 +56,8 @@ namespace sat {
                        << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
         }
     };
-    
-    void asymm_branch::operator()(bool force) {
-        ++m_calls;
-        if (m_calls <= 1)
-            return;
-        if (!m_asymm_branch && !m_asymm_branch_all)
-            return;
-        s.propagate(false); // must propagate, since it uses s.push()
-        if (s.m_inconsistent)
-            return;
-        if (!force && m_counter > 0) {
-            m_counter /= 100;
-            return;
-        }
-        CASSERT("asymm_branch", s.check_invariant());
-        TRACE("asymm_branch_detail", s.display(tout););
-        report rpt(*this);
-        svector<char> saved_phase(s.m_phase);
-        m_counter  = 0; 
+
+    void asymm_branch::process(clause_vector& clauses) {
         int64 limit = -m_asymm_branch_limit;
         std::stable_sort(s.m_clauses.begin(), s.m_clauses.end(), clause_size_lt());
         m_counter -= s.m_clauses.size();
@@ -114,6 +97,27 @@ namespace sat {
             m_counter = -m_counter;
             throw ex;
         }
+    }
+    
+    void asymm_branch::operator()(bool force) {
+        ++m_calls;
+        if (m_calls <= 1)
+            return;
+        if (!m_asymm_branch && !m_asymm_branch_all)
+            return;
+        s.propagate(false); // must propagate, since it uses s.push()
+        if (s.m_inconsistent)
+            return;
+        if (!force && m_counter > 0) {
+            m_counter /= 100;
+            return;
+        }
+        CASSERT("asymm_branch", s.check_invariant());
+        TRACE("asymm_branch_detail", s.display(tout););
+        report rpt(*this);
+        svector<char> saved_phase(s.m_phase);
+        m_counter  = 0; 
+        process(s.m_clauses);
         m_counter = -m_counter;
         s.m_phase = saved_phase;
         m_asymm_branch_limit *= 2;

src/sat/sat_asymm_branch.h

@@ -44,6 +44,8 @@ namespace sat {
         unsigned m_elim_literals;
 
         bool process(clause & c);
+
+        void process(clause_vector & c);
         
         bool process_all(clause & c);
         

src/sat/sat_config.cpp

@@ -176,6 +176,8 @@ namespace sat {
         m_reward_multiplier = 0.9;
         m_reward_offset = 1000000.0;
 
+        m_variable_decay = p.variable_decay();
+
         // PB parameters
         s = p.pb_solver();
         if (s == symbol("circuit")) {

src/sat/sat_config.h

@@ -95,6 +95,8 @@ namespace sat {
         double             m_simplify_mult2;
         unsigned           m_simplify_max;
 
+        unsigned           m_variable_decay;
+
         gc_strategy        m_gc_strategy;
         unsigned           m_gc_initial;
         unsigned           m_gc_increment;

src/sat/sat_lookahead.cpp

@@ -2303,7 +2303,16 @@ namespace sat {
      */
 
     void lookahead::add_hyper_binary() {
+
+        std::cout << "binary trail size: " << m_binary_trail.size() << "\n";
+        std::cout << "Are windfalls still on the trail at base level?\n";
         unsigned num_lits = m_s.num_vars() * 2;
+        unsigned_vector bin_size(num_lits);
+        for (unsigned idx : m_binary_trail) {
+            bin_size[idx]++;
+        }
+        
+
         union_find_default_ctx ufctx;
         union_find<union_find_default_ctx> uf(ufctx);
         for (unsigned i = 0; i < num_lits; ++i) uf.mk_var();

src/sat/sat_params.pyg

@@ -9,6 +9,7 @@ def_module_params('sat',
                           ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'),
                           ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
                           ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
+                          ('variable_decay', UINT, 120, 'multiplier (divided by 100) for the VSIDS activity increement'), 
                           ('inprocess.max', UINT, UINT_MAX, 'maximal number of inprocessing passes'),
                           ('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'),
                           ('branching.anti_exploration', BOOL, False, 'apply anti-exploration heuristic for branch selection'),

src/sat/sat_solver.cpp

@@ -1415,6 +1415,7 @@ namespace sat {
         m_next_simplify           = 0;
         m_min_d_tk                = 1.0;
         m_search_lvl              = 0;
+        m_conflicts_since_gc      = 0;
         m_asymm_branch.init_search();
         m_stopwatch.reset();
         m_stopwatch.start();
@@ -1660,6 +1661,7 @@ namespace sat {
     void solver::gc() {
         if (m_conflicts_since_gc <= m_gc_threshold)
             return;
+        IF_VERBOSE(1, verbose_stream() << "gc\n";);
         CASSERT("sat_gc_bug", check_invariant());
         switch (m_config.m_gc_strategy) {
         case GC_GLUE:

src/sat/sat_solver.h

@@ -575,8 +575,8 @@ namespace sat {
         }
 
         void decay_activity() {
-            m_activity_inc *= 11;
-            m_activity_inc /= 10;
+            m_activity_inc *= m_config.m_variable_decay;
+            m_activity_inc /= 100;
         }
 
     private:

src/tactic/aig/aig.cpp

@@ -635,10 +635,8 @@ struct aig_manager::imp {
         }
 
         bool check_cache() const {
-            obj_map<expr, aig_lit>::iterator it  = m_cache.begin();
-            obj_map<expr, aig_lit>::iterator end = m_cache.end();
-            for (; it != end; ++it) {
-                SASSERT(ref_count(it->m_value) > 0);
+            for (auto const& kv : m_cache) {
+                SASSERT(ref_count(kv.m_value) > 0);
             }
             return true;
         }

src/tactic/portfolio/pb2bv_solver.cpp

@@ -50,7 +50,7 @@ public:
     virtual solver* translate(ast_manager& dst_m, params_ref const& p) {
         flush_assertions();
         solver* result = alloc(pb2bv_solver, dst_m, p, m_solver->translate(dst_m, p));
-        model_converter_ref mc = concat(mc0(), m_solver->get_model_converter().get());
+        model_converter_ref mc = mc0();
         if (mc) {
             ast_translation tr(m, dst_m);
             result->set_model_converter(mc->translate(tr));