Probably a bug in new Java API (unstable branch)


I'm trying to use new Java API from unstable branch in my research project.
I've built jar library from source on Windows 64 bit by folowing instructions in Leonardo de Moura's blog here.

The folowing example demonstrate different results of using Java API methods:

1) In the first example I try to fill the Solver with BoolExpr manually using solver.Assert() method
2) In the second example I read the SMT file and parse it's contents with context.ParseSMTLIB2File() method

The expected result of running these examples is UNSATISFIABLE, but first example result is SATISFIABLE and second is UNSATISFIABLE.

All the expressions in both cases are the same, but statistics of the solvers is different.

It seems that in the first example Z3 does not instantiate quantifier properly.

file attachments

Closed Feb 22, 2013 at 5:49 PM by leodemoura
The problem was found.


leodemoura wrote Feb 22, 2013 at 5:49 PM

There is no bug.
The problem is the following line of code:
       expressions.add(context.MkForall(sorts, symbols, body, 0, null, null, null, null));
This MkForall is building a quantifier by binding in body the free variables: var 0 and var 1. It binds two variables because sorts and symbols have size 2. Moreover, it associates the names in symbols with these variables. Since body does not have free variables, the quantifier is equivalent to body.

In Z3, the free variables are created using the function mkBound (MkBound in previous versions). This function takes two arguments: int index, Sort ty. The index is the de Bruijn index for the variable.

In the past, several users complained that de Bruijn indices were not "user friendly" and were hard to use.
Then, we included a new mkForall API that takes a vector of "constants" that should be transformed into variables. In this API, Z3 automatically converts these constants into free variables and invokes the old API.

If we replace the line of code above with:
        expressions.add(context.MkForall(new Expr[]{obconst, pconst}, body, 0, null, null, null, null));
We get the expected quantifier. This version reflects your true intention, since you created the constants obconst and pconst and used them to create body.

We may ask, why Z3 displayed the following output when we executed your program?

(forall ((ob SimpleObject) (p Int))
(let ((a!1 (= (var (target (ptr p))) ob)))
(let ((a!2 (and a!1 (= (shift (ptr p)) 0))))
  (=> a!2 (= (dereffrom p) (value ob))))))
(= (var Va10) objVa10)
(= (value (var Va10)) 123)
(and (= (target objVp10) Va10) (= (shift objVp10) 0) (= (ptr Vp10) objVp10))
(= (dereffrom Vp10) 124))

The pretty printer missed a name clash between the constants ob and p and the variables named ob and p. The pretty printer should have renamed the variables ob and p when displaying the formula to avoid the clash and all this confusion.

wintersteiger wrote Feb 22, 2013 at 6:08 PM

Thanks to Leo for identifying the problem and proposing a fix. I would just like to add that the testcases that were submitted for this issue are based on an old version of the Java API. Most function calls have since been renamed to comply with the usual Java naming conventions and the version that will be released with the next Z3 release will use this new naming scheme.

krikunts wrote Feb 22, 2013 at 6:42 PM

Thank you very much for resolving this so fast!
This string representation was a bit confusing.
You saved lots of time to me.