Microsoft Research has released Z3 2.4. Z3 is a Satisfiability Modulo Theories problem solver. This is the first time I’ve downloaded Z3 and the first time I’ve researched SMT problems, so I’m unfamiliar with them at this point. Being a little curious as to what implications this could have for the .NET framework, I opened up the dotnet example.
The it has a simple cs file and a build.cmd, so I built it. When I ran the resulting executable, I’m not sure if I received the expected output because parser_example5 through an exception. The other example wrote formulas to the screen so that was pretty neat. After I opened the cs file, it turns out the example5 was expected to receive an error: “/* the following string has a parsing error: missing parenthesis */.”
From my brief analysis of this library, it appears that you build an equation with it, then you ask Z3 to prove it. My gripe is the syntax of it. You can build yourself a z3 context easily enough,
using (Config config = new Config())
{
config.SetParamValue("MODEL", "true");
using (Context context = new Context(config))
{
}
}
but working with it afterwards is a pain to manage. Also, why can’t I take advantage of object initializers to set up the config class? I can understand why you may not want to the context to dispose of the config file in case there are other context’s using the config, but there is some fishy about that the setup.
Let’s prove something simple. If x==y, then it stands to reason that f(x) == f(y).
The first thing I’m going to do is write an extension method for the z3 Context class so I can prove a term. I will use the Prove method found in the examples, modified for my usage.
public static string Prove(this Context context, Term term)
{
context.Push();
Term not = context.MkNot(term);
context.AssertCnstr(not);
switch (context.Check())
{
case LBool.False:
return "valid";
case LBool.Undef:
return "unknown";
case LBool.True:
return "invalid";
}
return null;
}
Next I’m going to write out the steps necessary to assert that x is equal to y, then ask if fx is equal to fy. This code is contained within the using blocks above.
FuncDecl f = context.MkFuncDecl("f", context.MkIntSort(), context.MkIntSort());
Term x = context.MkConst("x", context.MkIntSort());
Term y = context.MkConst("y", context.MkIntSort());
Term fx = context.MkApp(f, x);
Term fy = context.MkApp(f, y);
context.AssertCnstr(context.MkEq(x, y));
Term proof = context.MkEq(fx, fy);
Console.WriteLine("f(x) == f(y): {0}", context.Prove(proof));
That’s a lot of code, but it is valid! “f(x) == f(y): valid” was returned. But how can we be sure that it won’t always return that? Let’s assert the constraint that x is greater than y.
context.AssertCnstr(context.MkGt(x, y));
Now we received the text “f(x) == f(y): invalid.”
You probably don’t want to write all of that code out. Z3 comes with a few parsers, but I haven’t figured out the syntax for them yet. The methods to call on the context is ParseSmtlibFile, ParseSmtLibString, ParseZ3File, ParseZ3String, ParseSimplifyFile, ParseSimplifyString.
The code reads to me like C++. Looking at the .NET assembly in reflector, it is just a wrapper over unsafe assemblies. It is a shame, as I would play with it a lot more if it felt like I was using .NET. No worries though: the way things are nowadays it’s a matter of time before I find LinqToZ3 on Codeplex.
Subscribe