Add support for initializing variable values in solver and optimize c…

…ontexts in Z3

RELEASE_NOTES.md

@@ -18,7 +18,18 @@ Version 4.13.1
    The projection is described in paper by Haokun Li and Bican Xia,   [Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection](https://arxiv.org/abs/2003.00409). The code ported from https://github.com/hybridSMT/hybridSMT.git
 
 - Add API for providing hints for the solver/optimize contexts for which initial values to attempt to use for variables.
- The new API function are Z3_solver_set_initial_value and Z3_optimize_set_initial_value, respectively. Supply these functions with a Boolean or numeric variable, and a value. The solver will then attempt to use these values in the initial phase of search. The feature is aimed at resolving nearly similar problems, or problems with a predicted model and the intent is that restarting the solver based on a near solution can avoid prune the space of constraints that are initially infeasible. 
+ The new API function are Z3_solver_set_initial_value and Z3_optimize_set_initial_value, respectively. Supply these functions with a Boolean or numeric variable, and a value. The solver will then attempt to use these values in the initial phase of search. The feature is aimed at resolving nearly similar problems, or problems with a predicted model and the intent is that restarting the solver based on a near solution can avoid prune the space of constraints that are initially infeasible.
+ The SMTLIB front-end contains the new command (set-initial-value var value). For example,
+ (declare-const x Int)
+ (set-initial-value x 10)
+ (push)
+ (assert (> x 0))
+ (check-sat)
+ (get-model)
+ produces a model where x = 10. We use (push) to ensure that z3 doesn't run a
+ specialized pre-processor that eliminates x, which renders the initialization
+ without effect.
+
 
 Version 4.13.0
 ==============

src/ast/ast.cpp

@@ -1008,14 +1008,19 @@ sort* basic_decl_plugin::join(unsigned n, expr* const* es) {
 }
 
 sort* basic_decl_plugin::join(sort* s1, sort* s2) {
-    if (s1 == s2) return s1;
+    if (s1 == s2)
+        return s1;
     if (s1->get_family_id() == arith_family_id &&
         s2->get_family_id() == arith_family_id) {
         if (s1->get_decl_kind() == REAL_SORT) {
             return s1;
         }
         return s2;
     }
+    if (s1 == m_bool_sort && s2->get_family_id() == arith_family_id)
+        return s2;
+    if (s2 == m_bool_sort && s1->get_family_id() == arith_family_id)
+        return s1;
     std::ostringstream buffer;
     buffer << "Sorts " << mk_pp(s1, *m_manager) << " and " << mk_pp(s2, *m_manager) << " are incompatible";
     throw ast_exception(buffer.str());

src/ast/converters/generic_model_converter.cpp

@@ -130,6 +130,47 @@ generic_model_converter * generic_model_converter::copy(ast_translation & transl
     return res;
 }
 
+void generic_model_converter::convert_initialize_value(expr_ref& var, expr_ref& value) {
+    for (auto const& e : m_entries) {
+        switch (e.m_instruction) {
+        case HIDE: 
+            break;
+        case ADD: 
+            if (is_uninterp_const(var) && e.m_f == to_app(var)->get_decl())
+                convert_initialize_value(e.m_def, var, value);                
+            break;
+        }
+    }
+}
+
+void generic_model_converter::convert_initialize_value(expr* def, expr_ref& var, expr_ref& value) {
+
+    // var = if(c, th, el) = value
+    // th = value => c = true
+    // el = value => c = false
+    expr* c = nullptr, *th = nullptr, *el = nullptr;
+    if (m.is_ite(def, c, th, el)) {
+        if (value == th) {
+            var = c;
+            value = m.mk_true();
+            return;
+        }
+        if (value == el) {
+            var = c;
+            value = m.mk_false();
+            return;
+        }
+    }
+
+    // var = def = value
+    // => def = value
+    if (is_uninterp(def)) 
+        var = def;        
+
+
+}
+
+
 
 void generic_model_converter::set_env(ast_pp_util* visitor) { 
     if (!visitor) {

src/ast/converters/generic_model_converter.h

@@ -37,6 +37,7 @@ class generic_model_converter : public model_converter {
     vector<entry> m_entries;
 
     expr_ref simplify_def(entry const& e);
+    void convert_initialize_value(expr* def, expr_ref& var, expr_ref& value);
 
 public:
     generic_model_converter(ast_manager & m, char const* orig) : m(m), m_orig(orig) {}
@@ -61,6 +62,8 @@ class generic_model_converter : public model_converter {
 
     model_converter * translate(ast_translation & translator) override { return copy(translator); }
 
+    void convert_initialize_value(expr_ref& var, expr_ref& value) override;
+
     generic_model_converter* copy(ast_translation & translator);
 
     void set_env(ast_pp_util* visitor) override;

src/ast/converters/model_converter.cpp

@@ -107,6 +107,12 @@ class concat_model_converter : public concat_converter<model_converter> {
         m_c2->get_units(fmls);
         m_c1->get_units(fmls);
     }
+
+    void convert_initialize_value(expr_ref& var, expr_ref& value) override {
+        m_c2->convert_initialize_value(var, value);
+        m_c1->convert_initialize_value(var, value);
+    }
+
 
     char const * get_name() const override { return "concat-model-converter"; }
 

src/ast/converters/model_converter.h

@@ -86,6 +86,8 @@ class model_converter : public converter {
 
     virtual void set_env(ast_pp_util* visitor);
 
+    virtual void convert_initialize_value(expr_ref& var, expr_ref& value) { }
+
     /**
        \brief we are adding a formula to the context of the model converter.
        The operator has as side effect of adding definitions as assertions to the

src/cmd_context/basic_cmds.cpp

@@ -330,10 +330,7 @@ class set_initial_value_cmd : public cmd {
     void set_next_arg(cmd_context& ctx, expr* e) override { if (m_var) m_value = e; else m_var = e; }
     void execute(cmd_context& ctx) override {
         SASSERT(m_var && m_value);
-        if (ctx.get_opt())
-            ctx.get_opt()->initialize_value(m_var, m_value);
-        else if (ctx.get_solver())
-            ctx.get_solver()->user_propagate_initialize_value(m_var, m_value);
+        ctx.set_initial_value(m_var, m_value);
     }    
 };
 

src/cmd_context/cmd_context.cpp

@@ -629,6 +629,7 @@ cmd_context::~cmd_context() {
     finalize_cmds();
     finalize_tactic_manager();
     m_proof_cmds = nullptr;
+    m_var2values.reset();
     reset(true);
     m_mcs.reset();
     m_solver = nullptr;
@@ -654,6 +655,8 @@ void cmd_context::set_opt(opt_wrapper* opt) {
     m_opt = opt;
     for (unsigned i = 0; i < m_scopes.size(); ++i) 
         m_opt->push();
+    for (auto const& [var, value] : m_var2values)
+        m_opt->initialize_value(var, value);
     m_opt->set_logic(m_logic);
 }
 
@@ -1874,6 +1877,17 @@ void cmd_context::display_dimacs() {
     }
 }
 
+void cmd_context::set_initial_value(expr* var, expr* value) {
+    if (get_opt()) {
+        get_opt()->initialize_value(var, value);
+        return;
+    }
+    if (get_solver()) 
+        get_solver()->user_propagate_initialize_value(var, value);
+    m_var2values.push_back({expr_ref(var, m()), expr_ref(value, m())});    
+}
+
+
 void cmd_context::display_model(model_ref& mdl) {
     if (mdl) {
         if (mc0()) (*mc0())(mdl);

src/cmd_context/cmd_context.h

@@ -262,6 +262,7 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_
     scoped_ptr_vector<builtin_decl> m_extra_builtin_decls; // make sure that dynamically allocated builtin_decls are deleted
     dictionary<object_ref*>      m_object_refs; // anything that can be named.
     dictionary<sexpr*>           m_user_tactic_decls;
+    vector<std::pair<expr_ref, expr_ref>> m_var2values;
 
     dictionary<func_decls>       m_func_decls;
     obj_map<func_decl, symbol>   m_func_decl2alias;
@@ -421,6 +422,7 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_
     solver* get_solver() { return m_solver.get(); }
     void set_solver(solver* s) { m_solver = s; }
     void set_proof_cmds(proof_cmds* pc) { m_proof_cmds = pc; }
+    void set_initial_value(expr* var, expr* value);
 
     void set_solver_factory(solver_factory * s);
     void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }

src/opt/opt_context.cpp

@@ -311,7 +311,9 @@ namespace opt {
         }
         solver& s = get_solver();
         s.assert_expr(m_hard_constraints);
-        for (auto const& [var, value] : m_scoped_state.m_values) {
+        for (auto & [var, value] : m_scoped_state.m_values) {
+            if (m_model_converter)
+                m_model_converter->convert_initialize_value(var, value);
             s.user_propagate_initialize_value(var, value);
         }
 

src/sat/sat_solver/inc_sat_solver.cpp

@@ -703,7 +703,14 @@ class inc_sat_solver : public solver {
     }
 
     void user_propagate_initialize_value(expr* var, expr* value) override {
-        ensure_euf()->user_propagate_initialize_value(var, value);
+        expr_ref _var(var, m), _value(value, m);
+        if (m_mcs.back())
+            m_mcs.back()->convert_initialize_value(_var, _value);
+        sat::bool_var b = m_map.to_bool_var(_var);
+        if (b != sat::null_bool_var)
+            m_solver.set_phase(sat::literal(b, m.is_false(_value)));
+        else if (get_euf())  
+           ensure_euf()->user_propagate_initialize_value(_var, _value);
     }