#5486 - improve type elaboration by epsilon to make common cases pars…

…e without type annotation

src/ast/datatype_decl_plugin.cpp

@@ -367,6 +367,25 @@ namespace datatype {
             return m.mk_func_decl(name, arity, domain, range, info);
         }
 
+        ptr_vector<constructor> plugin::get_constructors(symbol const& s) const {
+            ptr_vector<constructor> result;
+            for (auto [k, d] : m_defs) 
+                for (auto* c : *d)
+                    if (c->name() == s)
+                        result.push_back(c);
+            return result;
+        }
+
+        ptr_vector<accessor> plugin::get_accessors(symbol const& s) const {
+            ptr_vector<accessor> result;
+            for (auto [k, d] : m_defs) 
+                for (auto* c : *d)
+                    for (auto* a : *c)
+                        if (a->name() == s)
+                            result.push_back(a);
+            return result;
+        }
+
         func_decl * decl::plugin::mk_recognizer(unsigned num_parameters, parameter const * parameters, 
                                                 unsigned arity, sort * const * domain, sort *) {
             ast_manager& m = *m_manager;
@@ -556,9 +575,8 @@ namespace datatype {
 
         void plugin::remove(symbol const& s) {
             def* d = nullptr;
-            if (m_defs.find(s, d)) {
+            if (m_defs.find(s, d)) 
                 dealloc(d);
-            }
             m_defs.remove(s);
         }
 

src/ast/datatype_decl_plugin.h

@@ -248,6 +248,8 @@ namespace datatype {
 
             def const& get_def(sort* s) const { return *(m_defs[datatype_name(s)]); }
             def& get_def(symbol const& s) { return *(m_defs[s]); }
+            ptr_vector<constructor> get_constructors(symbol const& s) const;
+            ptr_vector<accessor> get_accessors(symbol const& s) const;
             bool is_declared(sort* s) const { return m_defs.contains(datatype_name(s)); }
             unsigned get_axiom_base_id(symbol const& s) { return m_axiom_bases[s]; }
             util & u() const;

src/cmd_context/cmd_context.cpp

@@ -1194,6 +1194,55 @@ bool cmd_context::try_mk_macro_app(symbol const & s, unsigned num_args, expr * c
     return false;
 }
 
+bool cmd_context::try_mk_pdecl_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, expr_ref & r) const {
+    sort_ref_vector binding(m());
+    auto match = [&](sort* s, sort* ps) {
+        if (ps == s)
+            return true;
+        if (m().is_uninterp(ps) && ps->get_name().is_numerical()) {
+            int index = ps->get_name().get_num();
+            binding.reserve(index + 1);
+            binding[index] = s;
+            return true;
+        }
+        // Other matching is TBD
+        return false;
+    };
+    datatype::util dt(m());
+    func_decl_ref fn(m());
+    for (auto* c : dt.plugin().get_constructors(s)) {
+        if (c->accessors().size() != num_args)
+            continue;
+        binding.reset();
+        unsigned i = 0;
+        for (auto* a : *c) 
+            if (!match(args[i++]->get_sort(), a->range()))
+                goto match_failure;
+        if (binding.size() != c->get_def().params().size())
+            goto match_failure;
+        for (auto* b : binding)
+            if (!b)
+                goto match_failure;
+
+        fn = c->instantiate(binding);
+        r = m().mk_app(fn, num_args, args);
+        return true;
+    match_failure:
+        ;
+    }    
+    if (num_args != 1)
+        return false;
+
+    for (auto* a : dt.plugin().get_accessors(s)) {        
+        fn = a->instantiate(args[0]->get_sort());
+        r = m().mk_app(fn, num_args, args);
+        return true;
+    }
+
+    return false;
+}
+
+
 void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * args, 
                          unsigned num_indices, parameter const * indices, sort * range,
                          expr_ref & result) const {
@@ -1206,7 +1255,9 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
         return;    
     if (try_mk_builtin_app(s, num_args, args, num_indices, indices, range, result)) 
         return;
-
+    if (!range && try_mk_pdecl_app(s, num_args, args, num_indices, indices, result))
+        return;
+
     std::ostringstream buffer;
     buffer << "unknown constant " << s;
     if (num_args > 0) {
@@ -1899,7 +1950,7 @@ void cmd_context::complete_model(model_ref& md) const {
             SASSERT(!v->has_var_params());
             IF_VERBOSE(12, verbose_stream() << "(model.completion " << k << ")\n"; );
             ptr_vector<sort> param_sorts(v->get_num_params(), m().mk_bool_sort());
-            sort * srt = v->instantiate(*m_pmanager, param_sorts.size(), param_sorts.data());
+            sort * srt = v->instantiate(pm(), param_sorts.size(), param_sorts.data());
             if (!md->has_uninterpreted_sort(srt)) {
                 expr * singleton = m().get_some_value(srt);
                 md->register_usort(srt, 1, &singleton);

src/cmd_context/cmd_context.h

@@ -425,6 +425,7 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_
     bool try_mk_declared_app(symbol const & s, unsigned num_args, expr * const * args, 
                              unsigned num_indices, parameter const * indices, sort * range,
                              func_decls& fs, expr_ref & result) const;
+    bool try_mk_pdecl_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, expr_ref & r) const;
     void erase_cmd(symbol const & s);
     void erase_func_decl(symbol const & s);
     void erase_func_decl(symbol const & s, func_decl * f);