merge

Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>

src/ast/ast_translation.cpp

@@ -52,7 +52,6 @@ void ast_translation::cache(ast * s, ast * t) {
         m_to_manager.inc_ref(t);
         m_cache.insert(s, t);
         ++m_insert_count;
-
     }
 }
 

src/sat/sat_asymm_branch.cpp

@@ -55,9 +55,11 @@ namespace sat {
         ~report() {
             m_watch.stop();
             IF_VERBOSE(SAT_VB_LVL, 
-                       verbose_stream() << " (sat-asymm-branch :elim-literals "
+                       unsigned num_learned = (m_asymm_branch.m_elim_learned_literals - m_elim_learned_literals);
-                       << (m_asymm_branch.m_elim_literals - m_elim_literals)
+                       unsigned num_total = (m_asymm_branch.m_elim_literals - m_elim_literals);
-                       << " :elim-learned-literals " << (m_asymm_branch.m_elim_learned_literals - m_elim_learned_literals)
+                       verbose_stream() 
+                       << " (sat-asymm-branch :elim-literals " << (num_total - num_learned) 
+                       << " :elim-learned-literals " << num_learned
                        << " :hidden-tautologies " << (m_asymm_branch.m_hidden_tautologies - m_hidden_tautologies)
                        << " :cost " << m_asymm_branch.m_counter
                        << mem_stat()
@@ -76,12 +78,15 @@ namespace sat {
             s.propagate(false); 
             if (s.m_inconsistent)
                 break;
-            std::cout << "elim: " << m_elim_literals - elim << "\n";
+            unsigned num_elim = m_elim_literals - elim;
-            if (m_elim_literals == elim)
+            IF_VERBOSE(1, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";);
+            if (num_elim == 0)
                 break;
-        }
+            if (num_elim > 1000) 
-        std::cout << "elim-literals: " << m_elim_literals - elim0 << "\n";
+                i = 0;
-        std::cout << "elim-learned-literals: " << m_elim_learned_literals - eliml0 << "\n";
+        }        
+        IF_VERBOSE(1, if (m_elim_learned_literals > eliml0) 
+                          verbose_stream() << "(sat-asymm-branch :elim " << m_elim_learned_literals - eliml0 << ")\n";);
         return m_elim_literals > elim0;
     }
 
@@ -128,6 +133,16 @@ namespace sat {
             throw ex;
         }
     }
+
+    void asymm_branch::operator()(big& big) {
+        s.propagate(false); 
+        if (s.m_inconsistent)
+            return;
+        report rpt(*this);
+        svector<char> saved_phase(s.m_phase);
+        process(&big);
+        s.m_phase = saved_phase;
+    }
     
     void asymm_branch::operator()(bool force) {
         ++m_calls;
@@ -244,7 +259,6 @@ namespace sat {
                     lemma[j++] = l;
                 }
             }
-            // std::cout << lemma.size() << " -> " << j << "\n";
             lemma.shrink(j);
         }
     }
@@ -347,8 +361,7 @@ namespace sat {
                 break;
             }
         }
-        new_sz = j;        
+        new_sz = j;                
-        // std::cout << "cleanup: " << c.id() << ": " << literal_vector(new_sz, c.begin()) << " delta: " << (c.size() - new_sz) << " " << skip_idx << " " << new_sz << "\n";
         return re_attach(scoped_d, c, new_sz);
     }
 
@@ -386,7 +399,7 @@ namespace sat {
     bool asymm_branch::process_sampled(big& big, clause & c) {
         scoped_detach scoped_d(s, c);
         sort(big, c);
-#if 0
+#if 1
         if (uhte(big, c)) {
             ++m_hidden_tautologies;
             scoped_d.del_clause();

src/sat/sat_asymm_branch.h

@@ -87,6 +87,8 @@ namespace sat {
 
         void operator()(bool force = false);
 
+        void operator()(big& big);
+
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);
 

src/sat/sat_big.cpp

@@ -24,12 +24,8 @@ namespace sat {
     big::big() {}
 
     void big::init_big(solver& s, bool learned) {
-        m_num_vars = s.num_vars();
+        init_adding_edges(s.num_vars());
         unsigned num_lits = m_num_vars * 2;
-        m_dag.reset();
-        m_roots.reset();
-        m_dag.resize(num_lits, 0);
-        m_roots.resize(num_lits, true);
         literal_vector lits;
         SASSERT(num_lits == m_dag.size() && num_lits == m_roots.size());
         for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) {
@@ -44,11 +40,31 @@ namespace sat {
                     edges.push_back(v);
                 }
             }
+        }
+        done_adding_edges();
+    }
+
+    void big::init_adding_edges(unsigned num_vars) {
+        m_num_vars = num_vars;
+        unsigned num_lits = m_num_vars * 2;
+        m_dag.reset();
+        m_roots.reset();
+        m_dag.resize(num_lits, 0);
+        m_roots.resize(num_lits, true);
+    }
+
+    void big::add_edge(literal u, literal v) {
+        m_dag[u.index()].push_back(v);
+    }
+
+    void big::done_adding_edges() {
+        for (auto& edges : m_dag) {
             shuffle<literal>(edges.size(), edges.c_ptr(), m_rand);
         }
-        init_dfs_num(learned);
+        init_dfs_num();
     }
 
+
     struct big::pframe {
         literal m_parent;
         literal m_child;
@@ -58,7 +74,7 @@ namespace sat {
         literal parent() const { return m_parent; }
     };
 
-    void big::init_dfs_num(bool learned) {
+    void big::init_dfs_num() {
         unsigned num_lits = m_num_vars * 2;
         m_left.reset();
         m_right.reset();

src/sat/sat_big.h

@@ -34,13 +34,24 @@ namespace sat {
         svector<int>           m_left, m_right;
         literal_vector         m_root, m_parent;
 
-        void init_dfs_num(bool learned);
+        void init_dfs_num();
         struct pframe;
 
     public:
 
         big();
+        /**
+           \brief initialize a BIG from a solver.
+         */
         void init_big(solver& s, bool learned);
+
+        /**
+           \brief initialize a BIG externally by adding implications.
+        */
+        void init_adding_edges(unsigned num_vars);
+        void add_edge(literal u, literal v);
+        void done_adding_edges();
+
         void ensure_big(solver& s, bool learned) { if (m_left.empty()) init_big(s, learned); }
         int get_left(literal l) const { return m_left[l.index()]; }
         int get_right(literal l) const { return m_right[l.index()]; }
@@ -49,6 +60,7 @@ namespace sat {
         bool reaches(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; }        
         bool connected(literal u, literal v) const { return reaches(u, v) || reaches(~v, ~u); }
         void display(std::ostream& out) const;
+
     };
 };
 

src/sat/sat_config.cpp

@@ -74,6 +74,7 @@ namespace sat {
         m_local_search_threads = p.local_search_threads();
         m_lookahead_simplify = p.lookahead_simplify();
         m_lookahead_simplify_bca = p.lookahead_simplify_bca();
+        m_lookahead_simplify_asymm_branch = p.lookahead_simplify_asymm_branch();
         if (p.lookahead_reward() == symbol("heule_schur")) 
             m_lookahead_reward = heule_schur_reward;
         else if (p.lookahead_reward() == symbol("heuleu")) 

src/sat/sat_config.h

@@ -92,6 +92,7 @@ namespace sat {
         bool               m_local_search;
         bool               m_lookahead_simplify;
         bool               m_lookahead_simplify_bca;
+        bool               m_lookahead_simplify_asymm_branch;
         cutoff_t           m_lookahead_cube_cutoff;
         double             m_lookahead_cube_fraction;
         unsigned           m_lookahead_cube_depth;

src/sat/sat_lookahead.cpp

@@ -2310,14 +2310,42 @@ namespace sat {
                 elim_eqs elim(m_s);
                 elim(roots, to_elim);
 
+                if (get_config().m_lookahead_simplify_asymm_branch) {
+                    big_asymm_branch();
+                }
                 if (get_config().m_lookahead_simplify_bca) {
                     add_hyper_binary();
                 }
+                
             }
         }   
         m_lookahead.reset();        
     }
 
+    /**
+       \brief extract binary implication graph from learned binary clauses and use it
+       for strengthening clauses.
+     */
+
+    void lookahead::big_asymm_branch() {
+        unsigned num_lits = m_s.num_vars() * 2;
+        unsigned idx = 0;
+        big big;
+        big.init_adding_edges(m_s.num_vars());
+        for (auto const& lits : m_binary) {
+            literal u = get_parent(to_literal(idx++));
+            if (u == null_literal) continue;
+            for (literal v : lits) {
+                v = get_parent(v);
+                if (v != null_literal) 
+                    big.add_edge(u, v);
+            }            
+        }
+        big.done_adding_edges();
+        asymm_branch ab(m_s, m_s.m_params);
+        ab(big);
+    }
+
     /**
        \brief reduction based on binary implication graph
      */

src/sat/sat_lookahead.h

@@ -555,6 +555,8 @@ namespace sat {
 
         void add_hyper_binary();
 
+        void big_asymm_branch();
+
         double psat_heur();
 
     public:

src/sat/sat_params.pyg

@@ -49,6 +49,7 @@ def_module_params('sat',
                           ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
                           ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
                           ('lookahead_simplify.bca', BOOL, False, 'add learned binary clauses as part of lookahead simplification'),
+                          ('lookahead_simplify.asymm_branch', BOOL, False, 'apply asymmetric branch simplification with lookahead simplifier'),
                           ('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'),
                           ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu')))
 

src/sat/sat_simplifier.cpp

@@ -1772,7 +1772,7 @@ namespace sat {
 
         // eliminate variable
         ++s.m_stats.m_elim_var_res;
-        //VERIFY(!is_external(v));
+        VERIFY(!is_external(v));
         model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
         save_clauses(mc_entry, m_pos_cls);
         save_clauses(mc_entry, m_neg_cls);