prepare for variable scoping and autarkies

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

src/api/api_solver.cpp

@@ -557,7 +557,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_solver_cube(c, s, cutoff);
         ast_manager& m = mk_c(c)->m();
-        expr_ref_vector result(m);
+        expr_ref_vector result(m), vars(m);
         unsigned timeout     = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
         unsigned rlimit      = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
         bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", false);
@@ -568,7 +568,7 @@ extern "C" {
             scoped_timer timer(timeout, &eh);
             scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
             try {
-                result.append(to_solver_ref(s)->cube(cutoff));
+                result.append(to_solver_ref(s)->cube(vars, cutoff));
             }
             catch (z3_exception & ex) {
                 mk_c(c)->handle_exception(ex);
@@ -580,6 +580,7 @@ extern "C" {
         for (expr* e : result) {
             v->m_ast_vector.push_back(e);
         }
+        // TBD: save return variables from vars into variable ast-vector.
         RETURN_Z3(of_ast_vector(v));
         Z3_CATCH_RETURN(0);        
     }

src/muz/spacer/spacer_itp_solver.h

@@ -119,7 +119,7 @@ public:
     {NOT_IMPLEMENTED_YET();}
     virtual void assert_lemma(expr* e) { NOT_IMPLEMENTED_YET(); }
     virtual expr_ref lookahead(const expr_ref_vector &,const expr_ref_vector &) { return expr_ref(m.mk_true(), m); }
-    virtual expr_ref_vector cube(unsigned) { return expr_ref_vector(m); }
+    virtual expr_ref_vector cube(expr_ref_vector&, unsigned) { return expr_ref_vector(m); }
 
 
     virtual void push();

src/muz/spacer/spacer_virtual_solver.h

@@ -94,7 +94,7 @@ public:
     virtual void reset();
 
     virtual void set_progress_callback(progress_callback *callback) {UNREACHABLE();}
-    virtual expr_ref_vector cube(unsigned) { return expr_ref_vector(m); }
+    virtual expr_ref_vector cube(expr_ref_vector&, unsigned) { return expr_ref_vector(m); }
 
     virtual solver *translate(ast_manager &m, params_ref const &p);
 

src/opt/maxres.cpp

@@ -285,10 +285,12 @@ public:
             m_last_index = 0;
             bool first = index > 0;
             SASSERT(index < asms.size() || asms.empty());
+			IF_VERBOSE(1, verbose_stream() << "start hill climb " << index << " asms: " << asms.size() << "\n";);
             while (index < asms.size() && is_sat == l_true) {
                 while (!first && asms.size() > 20*(index - m_last_index) && index < asms.size()) {
                     index = next_index(asms, index);
                 }
+				IF_VERBOSE(1, verbose_stream() << "hill climb " << index << "\n";);
                 first = false;
                 // IF_VERBOSE(3, verbose_stream() << "weight: " << get_weight(asms[0].get()) << " " << get_weight(asms[index-1].get()) << " num soft: " << index << "\n";);
                 m_last_index = index;

src/opt/opt_solver.h

@@ -108,7 +108,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_vector cube(unsigned) { return expr_ref_vector(m); }
+        virtual expr_ref_vector cube(expr_ref_vector&, unsigned) { return expr_ref_vector(m); }
         void set_logic(symbol const& logic);
 
         smt::theory_var add_objective(app* term);

src/sat/sat_asymm_branch.h

@@ -42,7 +42,6 @@ namespace sat {
         unsigned   m_asymm_branch_rounds;
         unsigned   m_asymm_branch_delay;
         bool       m_asymm_branch_sampled;
-        bool       m_asymm_branch_propagate;
         bool       m_asymm_branch_all;
         int64      m_asymm_branch_limit;
 

src/sat/sat_elim_eqs.cpp

@@ -182,7 +182,8 @@ namespace sat {
             literal  l(v, false);
             literal r  = roots[v];
             SASSERT(v != r.var());
-            if (m_solver.is_external(v) || !m_solver.set_root(l, r)) {
+            if (m_solver.is_external(v)) {
+                m_solver.set_root(l, r);
                 // cannot really eliminate v, since we have to notify extension of future assignments
                 m_solver.mk_bin_clause(~l, r, false);
                 m_solver.mk_bin_clause(l, ~r, false);

src/sat/sat_elim_vars.cpp

@@ -123,13 +123,13 @@ namespace sat{
         TRACE("elim_vars",
               tout << "eliminate " << v << "\n";
               for (watched const& w : simp.get_wlist(~pos_l)) {
-                  if (w.is_binary_unblocked_clause()) {
+                  if (w.is_binary_non_learned_clause()) {
                       tout << pos_l << " " << w.get_literal() << "\n";
                   }
               }
               m.display(tout, b1);
               for (watched const& w : simp.get_wlist(~neg_l)) {
-                  if (w.is_binary_unblocked_clause()) {
+                  if (w.is_binary_non_learned_clause()) {
                       tout << neg_l << " " << w.get_literal() << "\n";
                   }
               }

src/sat/sat_solver/inc_sat_solver.cpp

@@ -305,7 +305,7 @@ public:
         return 0;
     }
 
-    virtual expr_ref_vector cube(unsigned backtrack_level) {
+    virtual expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) {
         if (!m_internalized) {
             dep2asm_t dep2asm;
             m_model = 0;

src/smt/smt_solver.cpp

@@ -222,7 +222,7 @@ namespace smt {
             return expr_ref(m.mk_true(), m);
         }
 
-        virtual expr_ref_vector cube(unsigned) {
+        virtual expr_ref_vector cube(expr_ref_vector&, unsigned) {
             return expr_ref_vector(get_manager());
         }
 

src/solver/combined_solver.cpp

@@ -275,8 +275,8 @@ public:
         return m_solver1->get_num_assumptions() + m_solver2->get_num_assumptions();
     }
 
-    virtual expr_ref_vector cube(unsigned backtrack_level) {
+    virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) {
-        return m_solver1->cube(backtrack_level);
+        return m_solver1->cube(vars, backtrack_level);
     }
 
     virtual expr * get_assumption(unsigned idx) const {

src/solver/solver.h

@@ -190,7 +190,7 @@ public:
        \brief extract a lookahead candidates for branching.
     */
 
-    virtual expr_ref_vector cube(unsigned backtrack_level) = 0;
+    virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) = 0;
 
     /**
        \brief Display the content of this solver.

src/solver/solver_pool.cpp

@@ -223,7 +223,7 @@ public:
     virtual void get_labels(svector<symbol> & r) { return m_base->get_labels(r); }
     virtual void set_progress_callback(progress_callback * callback) { m_base->set_progress_callback(callback); }
 
-    virtual expr_ref_vector cube(unsigned ) { return expr_ref_vector(m); }
+    virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned ) { return expr_ref_vector(m); }
 
     virtual ast_manager& get_manager() const { return m_base->get_manager(); } 
 

src/solver/tactic2solver.cpp

@@ -77,7 +77,7 @@ public:
 
     virtual ast_manager& get_manager() const; 
 
-    virtual expr_ref_vector cube(unsigned ) {
+    virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned ) {
         return expr_ref_vector(get_manager());
     }
 

src/tactic/portfolio/bounded_int2bv_solver.cpp

@@ -162,7 +162,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_vector cube(unsigned backtrack_level) { flush_assertions(); return m_solver->cube(backtrack_level); }
+    virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) { flush_assertions(); return m_solver->cube(vars, backtrack_level); }
     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) {
         flush_assertions();

src/tactic/portfolio/enum2bv_solver.cpp

@@ -103,7 +103,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_vector cube(unsigned backtrack_level) { return m_solver->cube(backtrack_level); }
+    virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) { return m_solver->cube(vars, backtrack_level); }
     
     virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
         datatype_util dt(m);

src/tactic/portfolio/parallel_tactic.cpp

@@ -414,7 +414,8 @@ private:
         cubes.reset();
         s.set_cube_params();
         while (true) {
-            expr_ref_vector c = s.get_solver().cube(UINT_MAX); // TBD tune this
+            expr_ref_vector vars(m);
+            expr_ref_vector c = s.get_solver().cube(vars, UINT_MAX); // TBD tune this
             if (c.empty()) {
                 report_undef(s);
                 return;

src/tactic/portfolio/pb2bv_solver.cpp

@@ -100,7 +100,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_vector cube(unsigned backtrack_level) { flush_assertions(); return m_solver->cube(backtrack_level); }
+    virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) { flush_assertions(); return m_solver->cube(vars, backtrack_level); }
     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) {
         flush_assertions();