How to set context and solver parameters using the managed API?

Aug 11, 2014 at 12:23 AM
I'm trying to configure the MBQI subsystem of Z3 using the managed API. I tried passing a settings dictionary to the constructor of Context. I also tried setting Solver.Parameters to some value. I tried parameter names like "MBQI_MAX_ITERATIONS", "mbqi.max_iterations" and "mbqi-max-iterations". All of the lower and with a leading colon as well.

Is it even possible to set values such as MBQI and MBQI_MAX_ITERATIONS using the managed API?

I can tell that the parameters do not take because MBQI stays active if I try to disable it. Also, I see in the solver statistics that the MBQI max iteration count is 1000 (contrary to what I specified).

This is regarding the unstable branch.
Coordinator
Aug 11, 2014 at 7:20 PM
Thanks for the report! How are you invoking MBQI? Theoretically, tactics could overwrite parameters. Depending on where/how you set the option it may also need the "smt." module prefix, i.e., as a global parameter it would be called "smt.mbqi.max_iterations".
Aug 11, 2014 at 10:42 PM
Edited Aug 11, 2014 at 10:44 PM
I set the following params:
mbqi.max_iterations
mbqi-max-iterations
MBQI_MAX_ITERATIONS
smt.mbqi.max_iterations
smt.mbqi-max-iterations
smt.MBQI_MAX_ITERATIONS
mbqi.max_iterations
mbqi-max-iterations
mbqi_max_iterations
smt.mbqi.max_iterations
smt.mbqi-max-iterations
smt.mbqi_max_iterations
:mbqi.max_iterations
:mbqi-max-iterations
:MBQI_MAX_ITERATIONS
:smt.mbqi.max_iterations
:smt.mbqi-max-iterations
:smt.MBQI_MAX_ITERATIONS
:mbqi.max_iterations
:mbqi-max-iterations
:mbqi_max_iterations
:smt.mbqi.max_iterations
:smt.mbqi-max-iterations
:smt.mbqi_max_iterations
All set to 10000U. Here's the essence of what I did:
        static Context CreateContext()
        {
            var mbqiMaxIterations = "10000";
            var settings = new Dictionary<string, string>()
            {
                { "MODEL", "true" },
                { "MBQI", "false" }, //experimenting... didn't take
                { "MBQI_MAX_ITERATIONS", mbqiMaxIterations },
                { "MBQI.MAX_ITERATIONS", mbqiMaxIterations },
                { "mbqi.max_iterations", mbqiMaxIterations },
                { "smt.mbqi.max_iterations", mbqiMaxIterations },
                { "MBQI_TRACE", "true" },
            };

                return new Context(settings);
        }


                using (var context = CreateContext())
                {
                    var solver = context.MkSimpleSolver();

                    {
                        var @params = context.MkParams();

                        foreach (var colon in new[] { false, true })
                            foreach (var lower in new[] { false, true })
                            foreach (var smt in new[] { false, true })
                                foreach (var str in new[] { "mbqi.max_iterations", "mbqi-max-iterations", "MBQI_MAX_ITERATIONS" })
                                {
                                    var name = (colon ? ":" : "") + (smt ? "smt." : "") + (lower ? str.ToLowerInvariant() : str);
                                    Debug.WriteLine(name);
                                    @params.Add(name, 10000U);
                                }

                        solver.Parameters = @params;
                    }

                    solver.Assert(SOME_EXPRESSION);

                    var status = solver.Check();
                }
I omitted SOME_EXPRESSION. Shouldn't one of those many param names work?

What's the right way to configure Z3 using the managed API? I'm interested in configuring MBQI and the SAT engine (both with MkSimpleSolver as well as with tactics and pre-configured logics).

If I might say so: Documentation is the only important weakness to Z3 that I noticed so far... Besides that Z3 is a dream to work with. Features, performance and API are excellent.

Here's how I know that MBQI stopped after 1000 iterations:
Image
Coordinator
Aug 12, 2014 at 6:08 PM
Thanks again for reporting this. I haven't had time to properly debug this, but I can already tell that it's either a reference counting issue inside of Z3, or a concurrent garbage collector issue on the managed level (essentially the Params object is deallocated before it gets to tell the solver all options). We know that there is a bug that in some way is triggered by the concurrent GC, but I haven't had time to dig any deeper yet. It's likely that this is the same problem though, and I can make it happen (or go away) by strategically setting breakpoints...
Aug 12, 2014 at 6:37 PM
I added
                    var keepAliveObjects = new List<object>();
                    //...
                    keepAliveObjects.Add(solver);
                    keepAliveObjects.Add(@params);
                    //...
                    solver.Assert(assertExpr);
                    var status = solver.Check();
                    //...
                    GC.KeepAlive(keepAliveObjects);
to make sure that these objects are kept alive. This did not change anything. This configuration issue appears to be deterministic.
Coordinator
Aug 12, 2014 at 6:40 PM
Yes, it appears fairly deterministic, but as soon as I set a breakpoint at solver.Parameters = @params; it suddenly starts to work. This one might take a while to debug.
Coordinator
Aug 12, 2014 at 6:44 PM
This is no confirmed non-deterministic; I got the same binary with the same breakpoints but different pauses between typing F5 to behave both ways.
Aug 12, 2014 at 7:02 PM
I do not believe it is a GC issue. I added
            GC.Collect();
            GCSettings.LatencyMode = GCLatencyMode.LowLatency;
            Console.WriteLine(GC.CollectionCount(0));
            Console.WriteLine(GC.CollectionCount(1));
            Console.WriteLine(GC.CollectionCount(2));
to the beginning of the test. I added the last three lines to the end of the test. I get "1 1 1, 1 1 1". No GC happening. LowLatency mode is very aggressive in avoiding GCs.
Coordinator
Aug 12, 2014 at 7:12 PM
Thanks for the additional experiment! Yes, it's quite possible the GC is not the problem. At the moment I have two non-determinism bug reports that seem to happen in the managed world only and I'm hoping that it's different faces of the same bug, but that may turn out to be wrong of course.
Coordinator
Aug 14, 2014 at 11:28 AM
Thanks again for pointing us in the right direction. It turns out that there were actually two different bugs at play here. The non-determinism is still there, but all the parameter settings should now make it all the way through (as of this fix). This is just a quick fix and in future we will have to do some refactoring of the parameter setting infrastructure so that bugs like this don't occur anymore.
Aug 14, 2014 at 11:38 AM
Glad I could help. Could you give a brief overview of how the params must be named that I try to set using the managed API? I'm interested in:
  1. The settings dictionary for new Context(...)
  2. The params for tactics
  3. Solver.Parameters
I understand the same "logical" parameter has different names in these variants?
Coordinator
Oct 6, 2014 at 12:53 PM
Just a note on this one: We'll prepare more documentation for the parameter setting infrastructure when we get closer to the next release.

Briefly, the parameters for the context are exactly those that are listed in the documentation for Z3_mk_config(void); The others are those that are given Tactic.ParameterDescriptions and Solver.ParameterDescriptions. As of right now, there may still be bugs in the infrastructure that effectively could have the effect that a correctly named parameter is not set. We're still working on that.