Add support for initializing variable values in solver and optimize contexts in Z3

src/ast/ast.cpp

@@ -1008,7 +1008,8 @@ 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) {
@@ -1016,6 +1017,10 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) {
         }
         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 @@ private:
     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 @@ public:
 
     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 @@ public:
         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 @@ public:
     
     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