Some List Functions (in particular, fplus::transform etc.) do not work with custom container. What needs to be added?

[jparsert]

I am using Z3 where I am using a specific container to store expressions etc. The definition of this container can be found exactly here. Unfortunately I am unable to use constructs like transform(foo, some_ast_vector). I suspect it is because there are no default constructors and the context object needs to be carried around everywhere. Is that true? Is there a way for me to provide functions to that container type to make fplus functions behave nicely?

[Dobiasd]

Hi, and thanks for the feedback. :+1:

I have no experience with Z3, but your fplus use-case sounds interesting. The problem could come from the container type having no default ctor (as you said), or from a problem in deducing the resulting container type in the fplus internals.

Could you provide a minimal example to reproduce the compiler error, that you get?

[jparsert]

Note that you need z3 installed.

#include <iostream>
#include "z3++.h"
#include "fplus/fplus.hpp"

int main() {
    z3::context context;
    std::vector<z3::expr> vec;
    vec.push_back(context.bool_const("var1"));
    vec.push_back(context.int_const("var2"));
    z3::ast_vector_tpl<z3::expr> expr_vec = fplus::transform([](auto& x){return x;}, vec);
    return 0;
}

[Dobiasd]

Thanks. Using g++, I get the following error:

fplus_issue_271.cpp: In function ‘int main()’:
fplus_issue_271.cpp:10:89: error: no matching function for call to ‘transform(main()::<lambda(auto:1393&)>, std::vector<z3::expr>&)’
   10 |     z3::ast_vector_tpl<z3::expr> expr_vec = fplus::transform([](auto& x){return x;}, vec);
      |                                                                                         ^
In file included from /usr/local/include/fplus/fplus.hpp:11,
                 from fplus_issue_271.cpp:3:
/usr/local/include/fplus/container_common.hpp:633:14: note: candidate: ‘template<class F, class ContainerIn, class ContainerOut> ContainerOut fplus::transform(F, ContainerIn&&)’
  633 | ContainerOut transform(F f, ContainerIn&& xs)
      |              ^~~~~~~~~
/usr/local/include/fplus/container_common.hpp:633:14: note:   template argument deduction/substitution failed:
/usr/local/include/fplus/container_common.hpp:631:5: error: no type named ‘type’ in ‘struct fplus::internal::invoke_result<main()::<lambda(auto:1393&)>, z3::expr>’
  631 |     typename ContainerOut = typename internal::same_cont_new_t_from_unary_f<
      |     ^~~~~~~~

Let's switch to clang++ for terseness:

fplus_issue_271.cpp:10:45: error: no matching function for call to 'transform'
    z3::ast_vector_tpl<z3::expr> expr_vec = fplus::transform([](auto& x){return x;}, vec);
                                            ^~~~~~~~~~~~~~~~
/usr/local/include/fplus/container_common.hpp:633:14: note: candidate template ignored: substitution failure [with F = (lambda at fplus_issue_271.cpp:10:62), ContainerIn = std::vector<z3::expr, std::allocator<z3::expr> > &]: no type named 'type' in 'fplus::internal::invoke_result<(lambda at fplus_issue_271.cpp:10:62), z3::expr>'
ContainerOut transform(F f, ContainerIn&& xs)
             ^
1 error generated.

So here, the problem comes from the compiler being unable to deduce the auto type for the lambda parameter. We can help by making it explicit:

    z3::ast_vector_tpl<z3::expr> expr_vec = fplus::transform([](const z3::expr& x){return x;}, vec);

Compilation still fails

fplus_issue_271.cpp:10:34: error: no viable conversion from 'std::vector<z3::expr, std::allocator<z3::expr> >' to 'z3::ast_vector_tpl<z3::expr>'
    z3::ast_vector_tpl<z3::expr> expr_vec = fplus::transform([](const z3::expr& x){return x;}, vec);
                                 ^          ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/usr/include/z3++.h:580:9: note: candidate constructor not viable: no known conversion from 'std::vector<z3::expr, std::allocator<z3::expr> >' to 'z3::context &' for 1st argument
        ast_vector_tpl(context & c):object(c) { init(Z3_mk_ast_vector(c)); }
        ^
/usr/include/z3++.h:582:9: note: candidate constructor not viable: no known conversion from 'std::vector<z3::expr, std::allocator<z3::expr> >' to 'const z3::ast_vector_tpl<z3::expr> &' for 1st argument
        ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
        ^

but this time differently. So the assignment = can not convert between the two vector types, i.e., from std::vector<T> to z3::ast_vector_tpl<T>.

The following helps:

    auto expr_vec = fplus::transform([](const z3::expr& x){return x;}, vec);

(We could replace auto with std::vector<z3::expr> if preferred.)

fplus::transform by default, i.e., if not specified otherwise in the template arguments, always returns the same container type as was used for input.

To have a different output container, we could either specify all template arguments, or (for convenience) use fplus::tranform_convert:

   auto expr_vec = fplus::transform_convert<z3::ast_vector_tpl<z3::expr>>([](const z3::expr& x){return x;}, vec);

Now we get to the error of z3::ast_vector_tpl<T> not having a default constructor:

In file included from fplus_issue_271.cpp:3:
In file included from /usr/local/include/fplus/fplus.hpp:11:
/usr/local/include/fplus/container_common.hpp:660:18: error: no matching constructor for initialization of 'z3::ast_vector_tpl<z3::expr>'
    ContainerOut ys;
                 ^
fplus_issue_271.cpp:10:28: note: in instantiation of function template specialization 'fplus::transform_convert<z3::ast_vector_tpl<z3::expr>, (lambda at fplus_issue_271.cpp:10:76), std::vector<z3::expr, std::allocator<z3::expr> > >' requested here
    auto expr_vec = fplus::transform_convert<z3::ast_vector_tpl<z3::expr>>([](const z3::expr& x){return x;}, vec);
                           ^
/usr/include/z3++.h:580:9: note: candidate constructor not viable: requires single argument 'c', but no arguments were provided
        ast_vector_tpl(context & c):object(c) { init(Z3_mk_ast_vector(c)); }
        ^
/usr/include/z3++.h:582:9: note: candidate constructor not viable: requires single argument 's', but no arguments were provided
        ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
        ^
/usr/include/z3++.h:581:9: note: candidate constructor not viable: requires 2 arguments, but 0 were provided
        ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
        ^
/usr/include/z3++.h:583:9: note: candidate constructor not viable: requires 2 arguments, but 0 were provided
        ast_vector_tpl(context& c, ast_vector_tpl const& src): object(c) { init(Z3_ast_vector_translate(src.ctx(), src, c)); }
        ^

So, yeah, FunctionalPlus assumes the target container to have a default constructor in many places.

We get the same error when just trying:

    z3::ast_vector_tpl<int> empty_z3_vector;

Thus, I think you have the following options:

• Provide a wrapper class template around z3::ast_vector_tpl<T>, providing a default constructor (and other needed container functions).
• Extend the Z3 library, i.e., adding a default constructor there.
• Work with other containers, e.g., std::vector<T> for the fplus things and convert from/to z3::ast_vector_tpl<T> where needed.

[jparsert]

Yes, that's what I feared thanks. I have a discussion on the z3 project about default constructors.

[Dobiasd]

In case the discussion is public, it would be cool if you could post a link here. (I'm now interested in the design choices made when implementing custom containers. :slightly_smiling_face:)

[jparsert]

there we were discussion default constructors for the context class. But it carries over to these ast_vectors as these all depend on the context for the "default" constructors.

https://github.com/Z3Prover/z3/discussions/6557