User propagator - C++ API

[imarmanis]

Hi, I'm looking for a working example for the user propagator in C++.
I have tried the following, but the call to fixed leads to a segmentation fault (without any other output).
The version I'm using is 4.8.12.

#include "z3++.h"

using namespace z3;

std::function<void(unsigned, expr const &)> my_fixed = [](unsigned, expr const&) {std::cout << "Fixed\n";};

class MyPropagator : public user_propagator_base
{
    public:
        void push() { std::cout << "Push\n"; }
        void pop(unsigned n) { std::cout << "Pop\n"; }
        user_propagator_base *fresh(Z3_context ctx) { std::cout << "Fresh\n"; return nullptr; }
        MyPropagator(solver *s) : user_propagator_base(s) { fixed(my_fixed); }
};

int main()
{
    context c;
    solver s(c, (struct z3::solver::simple) {});
    MyPropagator p(&s);
    return 0;
}

It seems that, compared to the python api, a call to Z3_solver_propagate_init is missing from the constructor
of user_propagator_base.
Adding that, I no longer get the segmentation fault but other problems appear when I
actually use the propagator, so I'm unsure if that was actually the problem.

[NikolajBjorner]

I have only been using the Python bindings and likely omitted crucial functionality from the C++ bindings.
The Python bindings, on the other hand, have been well exercised in one use case for production plant optimization.
Otherwise, this is a newer feature with likely teething issues.

[imarmanis]

I see, thank you.

Just in case there is something obviously wrong with it,
I added the following to the constructor of user_propagator_base

user_propagator_base(solver* s): s(s), c(nullptr) {
     assert(s);
     Z3_solver_propagate_init(ctx(), *s, this, push_eh, pop_eh, fresh_eh);
 }

but it led to some strange behavior,
namely something unsatisfiable, when run without this change,
turns to satisfiable.

[imarmanis]

A minimal example about the mentioned behavior (using latest commit ):

#include "z3++.h"

using namespace z3;

std::function<void(unsigned, expr const &)> my_fixed = [](unsigned, expr const&) {};

class MyPropagator : public user_propagator_base
{
    public:
        void push() {}
        void pop(unsigned n) {}
        user_propagator_base *fresh(Z3_context ctx) { return nullptr; }
        MyPropagator(solver *s) : user_propagator_base(s) {}
};

int main()
{
    context c;
    solver s(c, (struct solver::simple) {});

    MyPropagator p(&s);
    expr b = c.bool_const("b");
    expr e = c.bool_const("e");
    expr v = c.bv_const("v", 2);

    s.add(e);
    s.add(implies(e, b && (v == c.bv_val(0, 2))));
    s.add(!(v >= c.bv_val(0, 2)));

    std::cout << s.check() << "\n";
    return 0;
}

Depending on whether the declaration of p is included, the result changes.
The same happens if it is moved with respect to the s.add calls.
Is there some implicit assumption that, e.g., user propagators should be constructed
only after all formulas are added to the solver?