Added user propagator example

[CEisenhofer]

No description provided.

[NikolajBjorner]

@CEisenhofer note that it doesn't build.

[NikolajBjorner]

../examples/c++/userPropagator.cpp:47:27: warning: field 'cnt' will be initialized after field 'values' [-Wreorder-ctor]
model(unsigned cnt) : cnt(cnt), values(nullptr) {
^
../examples/c++/userPropagator.cpp:126:22: warning: unused variable 'id' [-Wunused-variable]
unsigned id = fixedValues[i];
^
../examples/c++/userPropagator.cpp:337:5: warning: delete called on non-final 'user_propagator' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor]
delete propagator;

[NikolajBjorner]

/usr/bin/ld: userPropagator.o: in function main': userPropagator.cpp:(.text.startup+0x0): multiple definition of main'; example.o:example.cpp:(.text.startup+0x0): first defined here
collect2: error: ld returned 1 exit status

[CEisenhofer]

Strange, for me (GCC 11 - WSL Ubuntu) it compiles without problems. How do you build the example?
I just called "make cpp_example" in the examples folder that was generated by CMake and it successfully built two executables from the two source-files in the "c++" directory.

[NikolajBjorner]

You should look at the output of the hosted builds. Click on "Details"

[NikolajBjorner]

There are also many warnings, such as

../examples/c++/userPropagator.cpp:258:31: warning: comparison of integer expressions of different signedness: ‘int’ and ‘std::vector<z3::expr>::size_type’ {aka ‘long unsigned int’} [-Wsign-compare]
  258 |         for (int j = i + 1; j < queens.size(); j++) {
      |                             ~~^~~~~~~~~~~~~~~
../examples/c++/userPropagator.cpp: In function ‘int test23(unsigned int, bool)’:
../examples/c++/userPropagator.cpp:326:23: warning: comparison of integer expressions of different signedness: ‘int’ and ‘std::vector<z3::expr>::size_type’ {aka ‘long unsigned int’} [-Wsign-compare]
  326 |     for (int i = 0; i < queens.size(); i++) {
      |                     ~~^~~~~~~~~~~~~~~
../examples/c++/userPropagator.cpp:337:12: warning: deleting object of polymorphic class type ‘user_propagator’ which has non-virtual destructor might cause undefined behavior [-Wdelete-non-virtual-dtor]
  337 |     delete propagator;
      |            ^~~~~~~~~~
../examples/c++/userPropagator.cpp: In function ‘int main()’:
../examples/c++/userPropagator.cpp:408:27: warning: comparison of integer expressions of different signedness: ‘int’ and ‘const long unsigned int’ [-Wsign-compare]
  408 |         for (int i = 0; i < SIZE(permutation); i++) {
      |                         

These are easy to fix

[NikolajBjorner]

why use malloc from c++?

[NikolajBjorner]

I think you want & instead of *. It saves a character on dereference (. instead of ->) and captures invariant of being non-null

[NikolajBjorner]

maybe just have a constructor for model that performs clone.

[NikolajBjorner]

setting to nullptr is redundant. C++ has scoped ptr that does the free automatically.

[NikolajBjorner]

for (auto j = fixedValues.size(); j > lastCnt; j--)

[NikolajBjorner]

I don't get why you need a model abstraction.
Why not class model : public std::vector {};

[CEisenhofer]

Thanks for your comments! I've refactored the code accordingly. However, I've no clue why the build tries to link the cpp_example.o and the userPropagator.o. (From Azure's log: g++ -o cpp_example example.o userPropagator.o libz3.so -lpthread)
In the CMakeList.txt I've specified to build 2 executables and not to link those two files. (On my PC there is no problem.)
What does Azure execute to test the commit?