expose internal API for set_phase

src/muz/spacer/spacer_iuc_solver.h

@@ -120,6 +120,7 @@ public:
     void set_produce_models(bool f) override  { m_solver.set_produce_models(f); }
     void assert_expr_core(expr *t) override  { m_solver.assert_expr(t); }
     void assert_expr_core2(expr *t, expr *a) override   { NOT_IMPLEMENTED_YET(); }
+    void set_phase(expr* e) override { m_solver.set_phase(e); }
     expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
     void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override { m_solver.get_levels(vars, depth); }
     expr_ref_vector get_trail() override { return m_solver.get_trail(); }

src/opt/opt_solver.h

@@ -110,6 +110,7 @@ namespace opt {
         void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override; 
         expr_ref_vector get_trail() override { return m_context.get_trail(); }
         expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
+        void set_phase(expr* e) override { NOT_IMPLEMENTED_YET(); }
 
         void set_logic(symbol const& logic);
 

src/sat/sat_solver.h

@@ -352,7 +352,8 @@ namespace sat {
         bool was_eliminated(bool_var v) const { return m_eliminated[v]; }
         void set_eliminated(bool_var v, bool f) override;
         bool was_eliminated(literal l) const { return was_eliminated(l.var()); }
-        void set_phase(literal l) override { m_phase[l.var()] = !l.sign(); }
+        void set_phase(literal l) override { m_best_phase[l.var()] = m_phase[l.var()] = !l.sign(); }
+        void set_phase(bool_var b, bool sign) { set_phase(literal(b, sign)); }
         unsigned scope_lvl() const { return m_scope_lvl; }
         unsigned search_lvl() const { return m_search_lvl; }
         bool  at_search_lvl() const { return m_scope_lvl == m_search_lvl; }

src/sat/sat_solver/inc_sat_solver.cpp

@@ -294,6 +294,13 @@ public:
         }
     }
 
+    void set_phase(expr* e) override { 
+        bool is_not = m.is_not(e, e);
+        sat::bool_var b = m_map.to_bool_var(e);
+        if (b != sat::null_bool_var)
+            m_solver.set_phase(b, is_not);
+    }
+
     unsigned get_scope_level() const override {
         return m_num_scopes;
     }

src/smt/smt_solver.cpp

@@ -158,6 +158,9 @@ namespace {
         void assert_expr_core(expr * t) override {
             m_context.assert_expr(t);
         }
+        void set_phase(expr* e) override { 
+            NOT_IMPLEMENTED_YET();
+        }
 
         void assert_expr_core2(expr * t, expr * a) override {
             if (m_name2assertion.contains(a)) {

src/solver/combined_solver.cpp

@@ -135,6 +135,8 @@ public:
         return r;
     }
 
+    void set_phase(expr* e) override { m_solver1->set_phase(e); m_solver2->set_phase(e); }
+
     void updt_params(params_ref const & p) override {
         solver::updt_params(p);
         m_solver1->updt_params(p);

src/solver/solver.h

@@ -111,7 +111,7 @@ public:
         for (expr* e : ts) assert_expr(e);
     }
 
-//    void set_phase(expr* e) = 0;
+    virtual void set_phase(expr* e) = 0;
 
     void assert_expr(ptr_vector<expr> const& ts) { 
         for (expr* e : ts) assert_expr(e);

src/solver/solver_pool.cpp

@@ -68,6 +68,7 @@ public:
     }
 
     solver* base_solver() { return m_base.get(); }
+    void set_phase(expr* e) override { m_base->set_phase(e); }
 
     solver* translate(ast_manager& m, params_ref const& p) override { UNREACHABLE(); return nullptr; }
     void updt_params(params_ref const& p) override {

src/solver/tactic2solver.cpp

@@ -79,6 +79,7 @@ public:
 
     unsigned get_num_assertions() const override;
     expr * get_assertion(unsigned idx) const override;
+    void set_phase(expr* e) override { }
 
 
     expr_ref_vector cube(expr_ref_vector& vars, unsigned ) override {

src/tactic/fd_solver/bounded_int2bv_solver.cpp

@@ -151,6 +151,7 @@ public:
     void set_progress_callback(progress_callback * callback) override { m_solver->set_progress_callback(callback);  }
     void collect_statistics(statistics & st) const override { m_solver->collect_statistics(st); }
     void get_unsat_core(expr_ref_vector & r) override { m_solver->get_unsat_core(r); }
+    void set_phase(expr* e) override { m_solver->set_phase(e); }
     void get_model_core(model_ref & mdl) override {
         m_solver->get_model(mdl);
         if (mdl) {

src/tactic/fd_solver/enum2bv_solver.cpp

@@ -89,6 +89,7 @@ public:
     void set_progress_callback(progress_callback * callback) override { m_solver->set_progress_callback(callback);  }
     void collect_statistics(statistics & st) const override { m_solver->collect_statistics(st); }
     void get_unsat_core(expr_ref_vector & r) override { m_solver->get_unsat_core(r); }
+    void set_phase(expr* e) override { m_solver->set_phase(e); }
     void get_model_core(model_ref & mdl) override { 
         m_solver->get_model(mdl);
         if (mdl) {

src/tactic/fd_solver/pb2bv_solver.cpp

@@ -96,6 +96,7 @@ public:
             if (mc) (*mc)(mdl);
         }
     } 
+    void set_phase(expr* e) override { m_solver->set_phase(e); }
 
     void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override {
         m_solver->get_levels(vars, depth);

src/tactic/fd_solver/smtfd_solver.cpp

@@ -2031,6 +2031,8 @@ namespace smtfd {
             return r;
         }
 
+        void set_phase(expr* e) override {}
+
         void updt_params(params_ref const & p) override { 
             ::solver::updt_params(p); 
             if (m_fd_sat_solver) {