So, i’ve been recently working through the quantifier instantiation mechanism in wyone. This is a tricky, yet important topic. There’s been a lot of interesting research in this area as well (see further reading below for some examples), although I found the papers often hard work at times.

Anyway, the basic idea is pretty straightforward. Let’s imagine we’re testing the following formula for satisfiability:

in(x,xs) && x < 0 && forall Y [ in(Y,xs) ==> Y >= 0 ]

In this formula, the `forall`

expression enforces a constraint that every element in the “collection” `xs`

must be positive. On the other hand, we have a variable `x`

which is known to be in `xs`

, and is negative. Therefore, we can easily see that there is a contradiction here. *But, how does the SMT solver show this? *The answer is through quantifier instantiation. To do this, it constructs a binding from quantified variables to ground literals (or possibly ground formulas). Once a suitable binding is found, it instantiates the quantifier. For our example, a good binding would be `[Y->x]`

and using this to instantiate our quantifier gives:

in(x,xs) && x < 0 && forall Y [ in(Y,xs) ==> Y >= 0 ] => && in(x,xs) ==> x >= 0 => && x >= 0

At this point, the arithmetic theory of the SMT solver will kick in and immediately derive a contradiction from `x<0 && x>=0`

.

The difficulty in this process stems from the problem of finding a good binding. A lot of work in this area has been done, particularly with systems like Prolog which use unification. Modern SMT solvers usually rely on so-called *triggers* to generate the binding. A trigger is essentially just a pattern match which generates bindings. In our example, you could trigger on `in(X,Y)`

literals: when you saw one in a quantified formula, you’d try and generate a binding by looking at all existing ground instances of it. In our example, that would lead to unifying `in(x,xs)`

against `in(Y,xs)`

and that would generate the required binding.

This approach to quantification has numerous drawbacks. First and foremost, it can be very expensive to determine a binding as this requires a potentially exponential search through all possible trigger matches. Secondly, the problem arises when the SMT solver doesn’t use the exact trigger you need to get the contradiction. This is particularly likely to happen when the formula involves triggering on arithmetic expressions. For example:

f(x-1,x) && !g(x-1,x) && forall X,Y [ f(X,X+Y) ==> g(X,X+Y) ]

(Ok, this is a slightly artificial example, but it makes the point)

The challenge here is to obtain the binding `[X->x-1, Y->1]`

which will lead us to the contradiction. Certainly, this is possible … but the problem of unification is suddenly much harder as we must be prepared to make complex expression rewrites during unification. At some point, the SMT solver may give up searching for matches, and you’ll be forced to write formulas in a way that helps it find them.

Anyway, that’s all for now. But, I’d be quite interested to know how far existing solvers like Z3 or Simplify go in this department …

## Further Reading

**E-matching for Fun and Profit,**Michał Moskal, Jakub Łopuszański, Joseph R. Kiniry.*Electronic Notes in Theoretical Computer Science (ENTCS)*, 198(2): 19-35, 2008. [PDF]**Efficient E-matching for SMT Solvers**, Leonardo de Moura and Nikolaj Bjorner. In*Proceedings of the 21st international conference on Automated Deduction*, LNCS 4603:183-198, 2007. [PDF]**Programming with triggers,**Michał Moskal. In*Proceedings of the Workshop on Satisfiability Modulo Theories*, pages 20–29, 2009. [PDF]

Shouldn’t

forall Y [ in(Y,xs) ==> x >= 0 ]

be

forall Y [ in(Y,xs) ==> Y >= 0 ]

Hi Dan,

Yes, well spotted!!! I’ve correct that now — thanks.

Dave

I assume you’re talking about E-matching and not MBQI?

Hi,

Yeah, it’s about E-Matching.

Dave

Hi ! I am a Master student and currently working on trigger problems in SMT solvers. I enjoyed reading your blog. It gives quite an insight of the triggering problems. I was wondering, in the meanwhile, if you had any interesting research done on it in your solver “wyone”.

And also if you came to know about how Z3/CVC4 handles this quantifier instantiation.

Thanks ! 🙂

Hi Prasoon,

Yes, work has continued on the SMT solver. You can find the source code as part of the WhileyCompiler here:

https://github.com/Whiley/WhileyCompiler

Look in the directory modules/wycs (wycs is the new name for the solver). It still needs plenty of work though! Eventually, I will split the solver out of the compiler so that it is a standalone application.

To be honest, I haven’t spent a lot of time looking at how Z3 and CVC4 work. I would really like to do that, but just haven’t found time yet.

Cheers!

Dave

Hi Dave

Thanks for pointing out the repository of your solver. I will have a look. 🙂

Prasoon