Add user propagator feature

[ThomasHaas]

This PR adds the user propagator feature to JavaSMT (~ user-defined theory solvers).
Currently, the only SMT backend that supports this feature is Z3, but CVC5 also seems to be working on adding support for user propagators.
For now, only the most important (and most general) user propagator features are exposed.

The PR contains 3 example implementations: SimpleUserPropagator and two propagators for Nqueens.
Both NQueens propagators are enumerating all models of an Nqueens instance, but one of them also implements the placement constraints inside the user propagator (the other works on the original encoding).
The user propagator gives tremendeous speed-up when enumerating the models: we measure up-to two orders of magnitude speed-up (a couple of minutes rather than hours for large instances).

The speed-up can be easily observed on Nqueens with N=11: iterating all models with the classical approach takes around 22 seconds (on my machine), whereas the user propagator solutions need only about 2 seconds. The difference gets larger with larger N.

Problems: The user propagator feature needs the recent version of Z3 and does not work with the current version used by JavaSMT. Thanks @kfriedberger for updating the Z3 version.

Edit: I just noticed that I accidentally copied the license headers into some of the source files.
How are the licensing rules? Shall I remove the headers or replace them using my name?

[kfriedberger]

Hi Thomas,
thanks for your PR. The user-propagator is very interesting.

Z3

We will update Z3 to the latest version soon. (DONE ✔️ ) Afterwards, I will take a look at this PR.

License

JavaSMT is open-source under Apache-2.0 and there are currently no plans to change the license. For students and other contributers, the simplest approach is to just copy the existing default licencing information and use a header-text like

// This file is part of JavaSMT,
// an API wrapper for a collection of SMT solvers:
// https://github.com/sosy-lab/java-smt
//
// SPDX-FileCopyrightText: {{YEAR}} Dirk Beyer <https://www.sosy-lab.org>
//
// SPDX-License-Identifier: Apache-2.0

I am not sure whether external persons that contribute larger parts of code have to sign some kind of copyright/licensing-transfer, e.g., to allow future changes in the name of Sosy-Lab. We had such a process internally once, long time ago. For such details, we need to ask @PhilippWendler or @dbeyer.

[ThomasHaas]

Thanks for the quick update to Z3's version.
The CI is happy now.

[ThomasHaas]

For the Nqueens example, we copied the already existing Nqueens code and modified it to accomodate for user propagators.
I can try to merge both examples into one to reduce redundancy if that is desired.

[ThomasHaas]

I just fixed some issues in Z3's user propagators for Java (PR).
Without those changes, it is currently not possible to implement the decide-callback which allows the user to react to and modify decisions of the solver.
I guess it is unlikely that you update the Z3 version of JavaSMT by building from sources, right? :)

[kfriedberger]

We can provide Z3 from sources for Linux (64bit) via Ivy and Maven, but we do currently not want to compile Z3 for other platforms. Z3 itself has releases regularly, so other platforms might need to wait for some specific features only a little bit longer.

Thanks for your patience. I still had not yet the time for reviewing the complete PR.

[ThomasHaas]

No problem, it's not too urgent. I will add the remaining feature(s) with the new Z3 release.

[ThomasHaas]

Z3 released a new version with my fixes to the user propagator. In case you update to the new Z3 version, I will add the remaining feature in this PR. But I'm also fine with postponing that feature into a future PR.

[kfriedberger]

Z3 was updated to version 4.12.5.

[ThomasHaas]

I added the last missing feature: listening to and modifying decisions made by the solver.

There is currently a surprising limitation in Z3's user propagators: only a single conflict can be reported in a callback (the other one's will silently get ignored). This limits the feasibility of "lemmas on demand"-approaches that could find multiple conflicts.
Should we document such strange behaviour?

[ThomasHaas]

Any estimate on when this will get reviewed? :)

[kfriedberger]

Can this method be called mutliple times?
If yes, is any existing propagator replaced by the new one?
If no, do we want to throw an exception?
PLease document this behaviour.

[kfriedberger]

Can we add a user-propagator at each point in time, e.g., after pushing several formulas? Or should we create a user-propagator before creating any symbols? For Z3, it seems to be sufficient to just instantiate the user-propagator right before calling the SMT/SAT-check.

[ThomasHaas]

I have not tried out what the limitations are, but it is definitely fine to add the user propagator anytime before the first SAT-check. You can create the whole solver formula and then add the propagator (you need to register the expressions after adding the propagator though)
Whether one can add them after the first SAT-check is something I didn't test.

EDIT: Regarding multiple calls to injectBackend (and initialize): I guess in theory this could get called multiple times if the user reuses the same propagator for multiple solvers (at any given time it should only be associated to a single solver though). Generally I would advise against this practice: the user should simply not do this.

[ThomasHaas]

After thinking more about this, I think it is always bad to register the same user propagator multiple times.
I made this point clear in the documentation and the implementation provided by AbstractUserPropagator will throw an error if the method is called multiple times.

[kfriedberger]

Does this expression need to be a symbol (variable) or can it be a complex boolean formula?
Can we also register non-boolean symbols?

Examples:

• Can we register to "a&&b"? Would the propagator then be called for each operation involving "a&&b" in that exact combination/operation?
• Can we register "counter==42"? Would the propagator then be called for each operation involving "counter"?

[ThomasHaas]

You can register any boolean expression, even counter==42. However, the propagator will notify on the value of the boolean expression and not on any variables inside. Basically, the propagator works on the boolean skeleton of the formula.
So you cannot track the precise value of counter and only indirectly know about its value by tracking atoms/predicates over counter.

Also, the propagator is more on the semantic level rather the syntactic one. If your whole asserted formula is a || b but you registered a && b, the propagator will still notify you once its partially found model fixes the value of a && b.
In this case, the solver will likely do this:

Decide a = false
Unit propagate b = true
Report (a&&b) == false to UserPropagator

You can run the SimpleUserPropagator example I added which showcases various interactions and prints the solver steps involved.

EDIT: While all of the above is true for Z3, I don't really want to give any hard guarantees in case other solvers in the future behave differently. That being said, tracking of simple variables would be sufficient to track arbitrary expressions by enriching the formula with equivalences of the form var <=> expr (Z3 just does this trick internally).

EDIT 2: Z3 has a richer set of user propagator features that also allow the user to register non-boolean expressions.
However, on other types of expressions(*) it only reports equalities/disequalities rather than their concrete values (I didn't add the equality callback though).

(*) An exception are BV expressions which can be bit-blasted to booleans. Because of this, Z3 is able to report values/decisions on booleans and BVs.

[ThomasHaas]

What is your policy regarding API-breaking changes?
I would consider the user propagator to be quite experimental and changes to the API are to be expected in the future.

[kfriedberger]

We try to keep the number of API changes to a minimum, but we do change if neccessary.
For any breaking changes in the API, we need to increment the version number.

[ThomasHaas]

I see, that makes sense.

[kfriedberger]

I am currently going through the code and trying a few things.

There are still some smaller questions, but the overall idea is clear.

The following questions are out of scope for this PR, but we might want to keep track on this topic:

• We have an internal ALL-SAT-routine in the ProverEnvironment. This could be replaced by a user-propagator, at least for Z3, to have a potentially faster ALL-SAT iteration. Correct?
• There is a certain encoding in CPAchecker for converting C-code with pointers to SMT formulas. A user propagator could serve as callback mechanism and solve pointer comparisons, etc, directly and faster than using a pure SMT-based encoding. (@sosy-lab/cpachecker Does someone want to try this?)

[ThomasHaas]

* We have an internal ALL-SAT-routine in the ProverEnvironment. This could be replaced by a user-propagator, at least for Z3, to have a potentially faster ALL-SAT iteration?

I believe this is true, since the Nqueens example is precisely such an ALL-SAT iteration. Whether it is universally more faster than adding blocking clauses from the outside is something I cannot promise though.
In my particular use-case (the reason I wanted this feature in the first place), just moving my theory reasoning into the final check of a user propagator did end up being slower by factor 2-3 (this is not an ALL-SAT problem though).
Also, this will only iterate through boolean models (not sure if your ALL-SAT iteration also gives models over complex theories).

Btw. thanks for the cleanup.

[kfriedberger]

The change looks good so far and it is in a mergable state.

[kfriedberger]

Additonal info: our ALL-SAT receives some important predicates from the user, aka a set of boolean symbols, over which the models should be computed. We ignore symbols from other theories in the iteration.

[ThomasHaas]

Additonal info: our ALL-SAT receives some important predicates from the user, aka a set of boolean symbols, over which the models should be computed. We ignore symbols from other theories in the iteration.

That works just fine. Just register those predicates with the user propagator, collect all the assignments via the onKnownValue-callback and in the onFinalCheck-callback raise a conflict on the assignment over those predicates.

A possible disadvantage for user propagators is that they may iterate the same model multiple times so that the propagator needs to explicitly track the models found so far (which could be exponentially many). This is because clauses learned by conflicts are eligible for clause deletion.
I discussed a related issue with Nikolaj (Z3Prover/z3#7109) and he added a way to generate persistent clauses, but this option is not available right now since JavaSMT has no way to pass parameters to Z3.
For ALL-SAT specifically, deletable clauses might still be preferred though.