Add initial value setting for variables in Z3 API, solver, and optimize modules

Author: NikolajBjorner

src/api/api_opt.cpp

@@ -459,6 +459,21 @@ extern "C" {
         Z3_CATCH;
     }
 
-
+    void Z3_API Z3_optimize_set_initial_value(Z3_context c, Z3_optimize o, Z3_ast var, Z3_ast value) {
+        Z3_TRY;
+        LOG_Z3_optimize_set_initial_value(c, o, var, value);
+        RESET_ERROR_CODE();
+        if (to_expr(var)->get_sort() != to_expr(value)->get_sort()) {
+            SET_ERROR_CODE(Z3_INVALID_USAGE, "variable and value should have same sort");
+            return;
+        }
+        ast_manager& m = mk_c(c)->m();
+        if (!m.is_value(to_expr(value))) {
+            SET_ERROR_CODE(Z3_INVALID_USAGE, "a proper value was not supplied");
+            return;
+        }
+        to_optimize_ptr(o)->initialize_value(to_expr(var), to_expr(value));
+        Z3_CATCH;        
+    }
 
 };

src/api/api_solver.cpp

@@ -1143,5 +1143,23 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+    void Z3_API Z3_solver_set_initial_value(Z3_context c, Z3_solver s, Z3_ast var, Z3_ast value) {
+        Z3_TRY;
+        LOG_Z3_solver_set_initial_value(c, s, var, value);
+        RESET_ERROR_CODE();
+        if (to_expr(var)->get_sort() != to_expr(value)->get_sort()) {
+            SET_ERROR_CODE(Z3_INVALID_USAGE, "variable and value should have same sort");
+            return;
+        }
+        ast_manager& m = mk_c(c)->m();
+        if (!m.is_value(to_expr(value))) {
+            SET_ERROR_CODE(Z3_INVALID_USAGE, "a proper value was not supplied");
+            return;
+        }
+        to_solver_ref(s)->user_propagate_initialize_value(to_expr(var), to_expr(value));
+        Z3_CATCH;        
+    }
+
+
 
 };

src/api/c++/z3++.h

@@ -2865,6 +2865,17 @@ namespace z3 {
             check_error(); 
             return result; 
         }
+        void set_initial_value(expr const& var, expr const& value) {
+            Z3_solver_set_initial_value(ctx(), m_solver, var, value);
+            check_error();
+        }
+        void set_initial_value(expr const& var, int i) {
+            set_initial_value(var, ctx().num_val(i, var.get_sort()));
+        }
+        void set_initial_value(expr const& var, bool b) {
+            set_initial_value(var, ctx().bool_val(b));            
+        }
+
         expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
         friend std::ostream & operator<<(std::ostream & out, solver const & s);
 
@@ -3330,6 +3341,17 @@ namespace z3 {
         handle add(expr const& e, unsigned weight) {
             return add_soft(e, weight);
         }
+        void set_initial_value(expr const& var, expr const& value) {
+            Z3_optimize_set_initial_value(ctx(), m_opt, var, value);
+            check_error();
+        }
+        void set_initial_value(expr const& var, int i) {
+            set_initial_value(var, ctx().num_val(i, var.get_sort()));
+        }
+        void set_initial_value(expr const& var, bool b) {
+            set_initial_value(var, ctx().bool_val(b));            
+        }
+
         handle maximize(expr const& e) {
             return handle(Z3_optimize_maximize(ctx(), m_opt, e));
         }

src/api/python/z3/z3.py

@@ -7353,6 +7353,13 @@ def trail_levels(self):
         Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
         return trail, levels
 
+    def set_initial_value(self, var, value):
+        """initialize the solver's state by setting the initial value of var to value
+        """
+        s = var.sort()
+        value = s.cast(value)
+        Z3_solver_set_initial_value(self.ctx.ref(), self.solver, var.ast, value.ast)
+
     def trail(self):
         """Return trail of the solver state after a check() call.
         """
@@ -8032,6 +8039,13 @@ def asoft(a):
             return [asoft(a) for a in arg]
         return asoft(arg)
 
+    def set_initial_value(self, var, value):
+        """initialize the solver's state by setting the initial value of var to value
+        """
+        s = var.sort()
+        value = s.cast(value)
+        Z3_optimize_set_initial_value(self.ctx.ref(), self.optimize, var.ast, value.ast)
+
     def maximize(self, arg):
         """Add objective function to maximize."""
         return OptimizeObjective(

src/api/z3_api.h

@@ -7241,6 +7241,18 @@ extern "C" {
 
     bool Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback cb, unsigned num_fixed, Z3_ast const* fixed, unsigned num_eqs, Z3_ast const* eq_lhs, Z3_ast const* eq_rhs, Z3_ast conseq);
 
+
+    /**
+       \brief provide an initialization hint to the solver. The initialization hint is used to calibrate an initial value of the expression that
+       represents a variable. If the variable is Boolean, the initial phase is set according to \c value. If the variable is an integer or real,
+       the initial Simplex tableau is recalibrated to attempt to follow the value assignment.
+
+       def_API('Z3_solver_set_initial_value', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST), _in(AST)))
+     */
+
+    void Z3_API Z3_solver_set_initial_value(Z3_context c, Z3_solver s, Z3_ast var, Z3_ast value);
+
+
     /**
        \brief Check whether the assertions in a given solver are consistent or not.
 

src/api/z3_optimization.h

@@ -139,6 +139,18 @@ extern "C" {
     */
     void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d);
 
+    /**
+       \brief provide an initialization hint to the solver.
+       The initialization hint is used to calibrate an initial value of the expression that
+       represents a variable. If the variable is Boolean, the initial phase is set
+       according to \c value. If the variable is an integer or real,
+       the initial Simplex tableau is recalibrated to attempt to follow the value assignment.
+
+       def_API('Z3_optimize_set_initial_value', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST), _in(AST)))
+     */
+
+    void Z3_API Z3_optimize_set_initial_value(Z3_context c, Z3_optimize o, Z3_ast var, Z3_ast value);
+    
     /**
        \brief Check consistency and produce optimal values.
        \param c - context

src/math/lp/lar_solver.cpp

@@ -2081,6 +2081,24 @@ namespace lp {
     lpvar lar_solver::to_column(unsigned ext_j) const {
         return m_var_register.external_to_local(ext_j);
     }
+    
+    bool lar_solver::move_lpvar_to_value(lpvar j, mpq const& value) {
+        if (is_base(j))
+            return false;
+
+        impq ivalue(value);
+        auto& lcs = m_mpq_lar_core_solver;
+        auto& slv = m_mpq_lar_core_solver.m_r_solver;
+
+        if (slv.column_has_upper_bound(j) && lcs.m_r_upper_bounds()[j] < ivalue)
+            return false;
+        if (slv.column_has_lower_bound(j) && lcs.m_r_lower_bounds()[j] > ivalue)
+            return false;
+        
+        set_value_for_nbasic_column(j, ivalue);
+        return true;
+    }
+
 
     bool lar_solver::tighten_term_bounds_by_delta(lpvar j, const impq& delta) {
         SASSERT(column_has_term(j));

src/math/lp/lar_solver.h

@@ -623,6 +623,7 @@ class lar_solver : public column_namer {
     lp_status find_feasible_solution();
     void move_non_basic_columns_to_bounds();
     bool move_non_basic_column_to_bounds(unsigned j);
+    bool move_lpvar_to_value(lpvar j, mpq const& value);
     inline bool r_basis_has_inf_int() const {
         for (unsigned j : r_basis()) {
             if (column_is_int(j) && !column_value_is_int(j))

src/opt/opt_context.cpp

@@ -58,8 +58,9 @@ namespace opt {
     }
 
     void context::scoped_state::pop() {
-        m_hard.resize(m_hard_lim.back());
-        m_asms.resize(m_asms_lim.back());
+        m_hard.shrink(m_hard_lim.back());
+        m_asms.shrink(m_asms_lim.back());
+        m_values.shrink(m_values_lim.back());
         unsigned k = m_objectives_term_trail_lim.back();
         while (m_objectives_term_trail.size() > k) {
             unsigned idx = m_objectives_term_trail.back();
@@ -79,6 +80,7 @@ namespace opt {
         m_objectives_lim.pop_back();            
         m_hard_lim.pop_back();   
         m_asms_lim.pop_back();
+        m_values_lim.pop_back();
     }
 
     void context::scoped_state::add(expr* hard) {
@@ -306,13 +308,11 @@ namespace opt {
         if (contains_quantifiers()) {
             warning_msg("optimization with quantified constraints is not supported");
         }
-#if 0
-        if (is_qsat_opt()) {
-            return run_qsat_opt();
-        }
-#endif
         solver& s = get_solver();
         s.assert_expr(m_hard_constraints);
+        for (auto const& [var, value] : m_scoped_state.m_values) {
+            s.user_propagate_initialize_value(var, value);
+        }
 
         opt_params optp(m_params);
         symbol pri = optp.priority();
@@ -697,6 +697,11 @@ namespace opt {
         }
     }
 
+    void context::initialize_value(expr* var, expr* value) {
+        m_scoped_state.m_values.push_back({expr_ref(var, m), expr_ref(value, m)});
+    }
+
+
     /**
      * Set the solver to the SAT core.
      * It requres:

src/opt/opt_context.h

@@ -140,12 +140,14 @@ namespace opt {
             unsigned_vector  m_objectives_lim;
             unsigned_vector  m_objectives_term_trail;
             unsigned_vector  m_objectives_term_trail_lim;
+            unsigned_vector  m_values_lim;
             map_id           m_indices;
 
         public:
             expr_ref_vector   m_hard;
             expr_ref_vector   m_asms;
             vector<objective> m_objectives;
+            vector<std::pair<expr_ref, expr_ref>> m_values;
 
             scoped_state(ast_manager& m):
                 m(m),
@@ -275,6 +277,8 @@ namespace opt {
 
         void add_offset(unsigned id, rational const& o) override;
 
+        void initialize_value(expr* var, expr* value);
+
         void register_on_model(on_model_t& ctx, std::function<void(on_model_t&, model_ref&)>& on_model) { 
             m_on_model_ctx = ctx; 
             m_on_model_eh  = on_model; 

src/opt/opt_solver.h

@@ -116,6 +116,7 @@ namespace opt {
         phase* get_phase() override { return m_context.get_phase(); }
         void set_phase(phase* p) override { m_context.set_phase(p); }
         void move_to_front(expr* e) override { m_context.move_to_front(e); }
+        void user_propagate_initialize_value(expr* var, expr* value) override { m_context.user_propagate_initialize_value(var, value); }
 
         void set_logic(symbol const& logic);
 

src/sat/sat_solver/inc_sat_solver.cpp

@@ -702,6 +702,10 @@ class inc_sat_solver : public solver {
         ensure_euf()->user_propagate_register_decide(r);
     }
 
+    void user_propagate_initialize_value(expr* var, expr* value) override {
+        ensure_euf()->user_propagate_initialize_value(var, value);
+    }
+
 
 private:
 

src/sat/sat_solver/sat_smt_solver.cpp

@@ -577,6 +577,11 @@ class sat_smt_solver : public solver {
         ensure_euf()->user_propagate_register_decide(r);
     }
 
+    void user_propagate_initialize_value(expr* var, expr* value) override {
+        ensure_euf()->user_propagate_initialize_value(var, value);
+    }
+
+
 private:
 
     void add_assumption(expr* a) {

src/sat/smt/euf_solver.cpp

@@ -1256,6 +1256,31 @@ namespace euf {
         add_solver(m_user_propagator);
     }
 
+    void solver::user_propagate_initialize_value(expr* var, expr* value) {
+        if (m.is_bool(var)) {
+            auto lit = expr2literal(var);
+            if (lit == sat::null_literal) {
+                IF_VERBOSE(5, verbose_stream() << "no literal associated with " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
+                return;
+            }
+            if (m.is_true(value))
+                s().set_phase(lit);
+            else if (m.is_false(value))
+                s().set_phase(~lit);
+            else
+                IF_VERBOSE(5, verbose_stream() << "malformed value " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");                
+            return;
+        }
+        auto* th = m_id2solver.get(var->get_sort()->get_family_id(), nullptr);
+        if (!th) {
+            IF_VERBOSE(5, verbose_stream() << "no default initialization associated with " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
+            return;
+        }
+        // th->initialize_value(var, value);
+        IF_VERBOSE(5, verbose_stream() << "no default initialization associated with " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
+    }
+
+
     bool solver::watches_fixed(enode* n) const {
         return m_user_propagator && m_user_propagator->has_fixed() && n->get_th_var(m_user_propagator->get_id()) != null_theory_var;
     }

src/sat/smt/euf_solver.h

@@ -564,6 +564,8 @@ namespace euf {
             m_user_propagator->add_expr(e);
         }
 
+        void user_propagate_initialize_value(expr* var, expr* value);
+
         // solver factory
         ::solver* mk_solver() { return m_mk_solver(); }
         void set_mk_solver(std::function<::solver*(void)>& mk) { m_mk_solver = mk; }

src/smt/smt_context.cpp

@@ -2914,6 +2914,44 @@ namespace smt {
         register_plugin(m_user_propagator);
     }
 
+    void context::user_propagate_initialize_value(expr* var, expr* value) {
+        m_values.push_back({expr_ref(var, m), expr_ref(value, m)});
+        push_trail(push_back_vector(m_values));
+    }
+
+    void context::initialize_value(expr* var, expr* value) {
+        IF_VERBOSE(10, verbose_stream() << "context initialize " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
+        sort* s = var->get_sort();
+        ensure_internalized(var);
+            
+        if (m.is_bool(s)) {
+            auto v = get_bool_var_of_id_option(var->get_id());
+            if (v == null_bool_var) {
+                IF_VERBOSE(5, verbose_stream() << "Boolean variable has no literal " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
+                return;
+            }
+            m_bdata[v].m_phase_available = true;         
+            if (m.is_true(value))
+                m_bdata[v].m_phase = true;
+            else if (m.is_false(value))
+                m_bdata[v].m_phase = false;
+            else
+                IF_VERBOSE(5, verbose_stream() << "Boolean value is not constant " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
+            return;                
+        }
+
+        if (!e_internalized(var))
+            return;
+        enode* n = get_enode(var);
+        theory* th = m_theories.get_plugin(s->get_family_id());
+        if (!th) {
+            IF_VERBOSE(5, verbose_stream() << "No theory is attached to variable " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
+            return;
+        }
+        th->initialize_value(var, value);
+
+    }
+
     bool context::watches_fixed(enode* n) const {
         return m_user_propagator && m_user_propagator->has_fixed() && n->get_th_var(m_user_propagator->get_family_id()) != null_theory_var;
     }
@@ -3756,6 +3794,9 @@ namespace smt {
         TRACE("search", display(tout); display_enodes_lbls(tout););
         TRACE("search_detail", m_asserted_formulas.display(tout););
         init_search();
+        for (auto const& [var, value] : m_values)
+            initialize_value(var, value);
+            
         flet<bool> l(m_searching, true);
         TRACE("after_init_search", display(tout););
         IF_VERBOSE(2, verbose_stream() << "(smt.searching)\n";);