Fix UP's decide callback

[CEisenhofer]

Reason we need this:
Although we can trace the current model in the UP by observing "fixed", we might not get all assignments due to RP.
Problem: If we pass something to "decide" that is already assigned, we crash. This is problematic, as the UP has no way to detect this up front.

[NikolajBjorner]

why is the variant where you change the signature of next_split_cb to return an lbool to indicate possible assignment discrepancies not an option?
In other words change API for

void Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase)

to

Z3_lbool Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase)

Or said in another way, isn't the issue that has_split_candidate should return false if the UP comes up with something assigned?

[CEisenhofer]

The real problem is "decide", rather than "next_split". Returning a value from "next_split" that indicates if the variable is already assigned solves the problem for "next_split" but not for "decide". (Also: This would make "next_split" a function to query the Boolean-Assignment)
If we change the reference-arguments from "decide", there is no way the API can report back that the variable is already assigned (and throws an exception).

I see two options:

1. A function that let us query the current assignment of a Boolean expression (there was once the discussion about querying integer-bounds on-demand, so this would fit in this category)
2. Change "decide" such that the decision of the core can be overridden by calling "next_split" within "decide" rather than changing the (reference) arguments of "decide".

[NikolajBjorner]

FAILED: src/api/java/CMakeFiles/z3java.dir/Native.cpp.o
/usr/bin/clang++ -D_EXTERNAL_RELEASE -D_MP_INTERNAL -I/home/vsts/work/1/s/src/api -I/home/vsts/work/1/s/build/src/api -I/usr/lib/jvm/temurin-11-jdk-amd64/include -I/usr/lib/jvm/temurin-11-jdk-amd64/include/linux -Werror=odr -Werror=delete-non-virtual-dtor -Werror=overloaded-virtual -Werror=non-virtual-dtor -Werror=null-dereference -fcolor-diagnostics -O3 -DNDEBUG -std=gnu++17 -fPIC -mfpmath=sse -msse -msse2 -Wall -MD -MT src/api/java/CMakeFiles/z3java.dir/Native.cpp.o -MF src/api/java/CMakeFiles/z3java.dir/Native.cpp.o.d -o src/api/java/CMakeFiles/z3java.dir/Native.cpp.o -c /home/vsts/work/1/s/build/src/api/java/Native.cpp
/home/vsts/work/1/s/build/src/api/java/Native.cpp:204:3: error: no matching function for call to 'Z3_solver_propagate_decide'
Z3_solver_propagate_decide((Z3_context)ctx, (Z3_solver)solver, decide_eh);
^~~~~~~~~~~~~~~~~~~~~~~~~~
/home/vsts/work/1/s/src/api/z3_api.h:7105:17: note: candidate function not viable: no known conversion from 'void (void *, Z3_solver_callback, Z3_ast, unsigned int, Z3_lbool)' (aka 'void (void *, _Z3_solver_callback *, _Z3_ast *, unsigned int, Z3_lbool)') to 'Z3_decide_eh ' (aka 'void ()(void *, _Z3_solver_callback *, _Z3_ast *, unsigned int, bool)') for 3rd argument
void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh);
^
1 error generated.

[NikolajBjorner]

Do you have to touch scripts/update_api.py?

[NikolajBjorner]

you might become a certified Java Enterprise SE developer!

[CEisenhofer]

Interestingly, my PC could compile it and generate a working .jar file 😅