Fastest way to check if a Z3 model fulfills constraints? BitVectors, Z3 3.2, C# API, x64, multi-threaded

1
votes

Given a set of constraints (assertions) in Z3 I am wondering what is the most efficient way of checking if a model that I already have fulfills these assertions. The model was obtained from similar set of constraints. I require a yes/no answer, not a soft constraint as in Specifying initial model values for Z3.

I am operating on bit vectors using x64 version of Z3 3.2, using C# API on Windows 7 x64. I am multi-threading by instantiating multiple Z3 Context objects, one per thread. I am not using Z3 4.0 due to lack of support for multi-threading.

My current approach is just to assert the model as an additional set of constraints using Context.AssertCnstr(Term) and then simply calling Context.Check().

1
z3
Z3 3.2 is not thread safe. That is, it is not safe to use different Z3 Context objects in different threads without synchronization. Z3 4.0 fixes this problem. BTW, why do you say Z3 4.0 lacks support for multi-threading. - Leonardo de Moura
@LeonardodeMoura After many trials and errors I found that the solution "one Context per one thread" is actually the only solution that allows me to use all of my 8 cores in parallel and that doesn't throw any kind of exceptions. I can provide you with a snippet demonstrating this if you wish (and with not working examples too). I say that Z3 4.0 lacks support for multi-threading because Z3 4.0 release notes state "Parallel Z3 is disabled in this release." and I was unable to find "x64_mt\Microsoft.Z3.dll" in Z3 4.0 installation. The "x64_mt" dir is missing. It is available in Z3 3.2 - Konrad Jamrozik

1 Answers

1
votes

Z3 exposes a method called "Z3_model_eval" or "Model.Eval" (from C#) that takes a model and an expression. Evaluation may fail if the expression contains quantifiers and the evaluator cannot determine the truth value of the quantified formula modulo the model. If model evaluation succeeds, you can inspect the returned value to determine whether the model forces the assertions to be true. The documentation for Z3_model_eval details the contract in more detail:

http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86670c291a16640b932e7892176a9d1b

Model evaluation will not detect tautologies, so serializing a model as a formula and having Z3 check the implication between the model and assertions may be more appropriate for some uses.