fixes to lookahead

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

src/opt/opt_solver.h

@@ -107,6 +107,7 @@ namespace opt {
         virtual ast_manager& get_manager() const { return m; } 
         virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
         virtual lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);
+        virtual expr_ref lookahead(expr_ref_vector const& candidates) { return expr_ref(m.mk_true(), m); }
         void set_logic(symbol const& logic);
 
         smt::theory_var add_objective(app* term);

src/sat/sat_lookahead.cpp

@@ -151,7 +151,7 @@ namespace sat {
                 }
                 if (m_num_tc1 < m_config.m_tc1_limit) {
                     ++m_num_tc1;
-                    IF_VERBOSE(3, verbose_stream() << "tc1: " << u << " " << w << "\n";);
+                    IF_VERBOSE(30, verbose_stream() << "tc1: " << u << " " << w << "\n";);
                     add_binary(u, w);
                 }
             }
@@ -285,9 +285,11 @@ namespace sat {
         for (bool_var const* it = m_freevars.begin(), * end = m_freevars.end(); it != end; ++it) {
             SASSERT(is_undef(*it));
             bool_var x = *it;
-            if (!m_select_lookahead_vars.empty() && m_select_lookahead_vars.contains(x)) {
+            if (!m_select_lookahead_vars.empty()) {
-                m_candidates.push_back(candidate(x, m_rating[x]));
+                if (m_select_lookahead_vars.contains(x)) {
-                sum += m_rating[x];                
+                    m_candidates.push_back(candidate(x, m_rating[x]));
+                    sum += m_rating[x];
+                }                
             }
             else if (newbies || active_prefix(x)) {
                 m_candidates.push_back(candidate(x, m_rating[x]));
@@ -1214,7 +1216,7 @@ namespace sat {
                     continue;
                 }
                 if (scope_lvl() == 1) {
-                    IF_VERBOSE(3, verbose_stream() << scope_lvl() << " " << lit << " binary: " << m_binary_trail.size() << " trail: " << m_trail_lim.back() << "\n";);
+                    IF_VERBOSE(30, verbose_stream() << scope_lvl() << " " << lit << " binary: " << m_binary_trail.size() << " trail: " << m_trail_lim.back() << "\n";);
                 }
                 TRACE("sat", tout << "lookahead: " << lit << " @ " << m_lookahead[i].m_offset << "\n";);
                 reset_wnb(lit);
@@ -1602,6 +1604,7 @@ namespace sat {
 
 
     literal lookahead::select_lookahead(bool_var_vector const& vars) {
+        IF_VERBOSE(1, verbose_stream() << "(sat-select " << vars.size() << ")\n";);
         scoped_ext _sext(*this);
         m_search_mode = lookahead_mode::searching;
         scoped_level _sl(*this, c_fixed_truth);

src/sat/sat_solver/inc_sat_solver.cpp

@@ -281,8 +281,10 @@ public:
     }
 
     virtual expr_ref lookahead(expr_ref_vector const& candidates) { 
+        IF_VERBOSE(1, verbose_stream() << "(sat-lookahead " << candidates.size() << ")\n";);
         sat::bool_var_vector vars;
         expr_ref_vector lit2expr(m);
+        lit2expr.resize(m_solver.num_vars() * 2);
         m_map.mk_inv(lit2expr);
         for (auto c : candidates) {
             sat::bool_var v = m_map.to_bool_var(c);
@@ -290,17 +292,21 @@ public:
                 vars.push_back(v);
             }
         }
+        IF_VERBOSE(1, verbose_stream() << "vars: " << vars.size() << "\n";);
         if (vars.empty()) {
             return expr_ref(m.mk_true(), m);
         }
         sat::literal l = m_solver.select_lookahead(vars);
         if (m_solver.inconsistent()) {
+            IF_VERBOSE(1, verbose_stream() << "(sat-lookahead inconsistent)\n";);
             return expr_ref(m.mk_false(), m);
         }
         if (l == sat::null_literal) {
             return expr_ref(m.mk_true(), m);
         }
-        return expr_ref(lit2expr[l.index()].get(), m);
+        expr_ref result(lit2expr[l.index()].get(), m);
+        IF_VERBOSE(1, verbose_stream() << "solution: " << l << " " << result << "\n";);
+        return result;
     }
     virtual void get_lemmas(expr_ref_vector & lemmas) { 
         IF_VERBOSE(1, verbose_stream() << "(sat-get-lemmas " << lemmas.size() << ")\n";);

src/smt/smt_solver.cpp

@@ -219,6 +219,11 @@ namespace smt {
             return m_context.get_formulas()[idx];
         }
 
+        virtual expr_ref lookahead(expr_ref_vector const& candidates) { 
+            ast_manager& m = get_manager();
+            return expr_ref(m.mk_true(), m);
+        }
+
         struct collect_fds_proc {
             ast_manager & m;
             func_decl_set & m_fds;

src/solver/combined_solver.cpp

@@ -274,6 +274,10 @@ public:
         return m_solver1->get_num_assumptions() + m_solver2->get_num_assumptions();
     }
 
+    virtual expr_ref lookahead(expr_ref_vector const& candidates) { 
+        return m_solver1->lookahead(candidates); 
+    }
+
     virtual expr * get_assumption(unsigned idx) const {
         unsigned c1 = m_solver1->get_num_assumptions();
         if (idx < c1) return m_solver1->get_assumption(idx);

src/solver/solver.cpp

@@ -162,9 +162,13 @@ bool solver::is_literal(ast_manager& m, expr* e) {
     return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e));
 }
 
+#if 0
 expr_ref solver::lookahead(expr_ref_vector const& candidates) {
+    std::cout << "lookahead: " << candidates.size() << "\n";
+    INVOKE_DEBUGGER();
     ast_manager& m = candidates.get_manager();
     return expr_ref(m.mk_true(), m);
 }
+#endif
 
 

src/solver/solver.h

@@ -176,7 +176,7 @@ public:
        \brief extract a lookahead candidates for branching.
     */
 
-    virtual expr_ref lookahead(expr_ref_vector const& candidates);
+    virtual expr_ref lookahead(expr_ref_vector const& candidates) = 0;
 
     /**
        \brief extract learned lemmas.

src/solver/tactic2solver.cpp

@@ -75,6 +75,12 @@ public:
     virtual expr * get_assertion(unsigned idx) const;
 
     virtual ast_manager& get_manager() const; 
+
+    virtual expr_ref lookahead(expr_ref_vector const& candidates) {
+        ast_manager& m = get_manager();
+        std::cout << "tactic2solver\n";
+        return expr_ref(m.mk_true(), m);
+    }
 };
 
 ast_manager& tactic2solver::get_manager() const { return m_assertions.get_manager(); }

src/tactic/portfolio/bounded_int2bv_solver.cpp

@@ -149,7 +149,7 @@ public:
     virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
     virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
     virtual ast_manager& get_manager() const { return m;  }
-    virtual expr_ref lookahead(expr_ref_vector& candidates) { flush_assertions(); return m_solver->lookahead(candidates); }
+    virtual expr_ref lookahead(expr_ref_vector const& candidates) { flush_assertions(); return m_solver->lookahead(candidates); }
     virtual void get_lemmas(expr_ref_vector & lemmas) { flush_assertions(); m_solver->get_lemmas(lemmas); }
     virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
     virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {

src/tactic/portfolio/enum2bv_solver.cpp

@@ -97,7 +97,7 @@ public:
     virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
     virtual ast_manager& get_manager() const { return m;  }
     virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
-    virtual expr_ref lookahead(expr_ref_vector& candidates) { return m_solver->lookahead(candidates); }
+    virtual expr_ref lookahead(expr_ref_vector const& candidates) { return m_solver->lookahead(candidates); }
     virtual void get_lemmas(expr_ref_vector & lemmas) { m_solver->get_lemmas(lemmas); }
     
     virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {

src/tactic/portfolio/pb2bv_solver.cpp

@@ -93,7 +93,7 @@ public:
     virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
     virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
     virtual ast_manager& get_manager() const { return m;  }
-    virtual expr_ref lookahead(expr_ref_vector& candidates) { flush_assertions(); return m_solver->lookahead(candidates); }
+    virtual expr_ref lookahead(expr_ref_vector const& candidates) { flush_assertions(); return m_solver->lookahead(candidates); }
     virtual void get_lemmas(expr_ref_vector & lemmas) { flush_assertions(); m_solver->get_lemmas(lemmas); }
     virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }    
     virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {