Improved quantifier implementation

[theyoucheng]

Added support for certain form of quantifiers

• the quantifier variable must be in a bounded (max/min) range
• quantifier variable in the quantifier body is instantiated with every integer within the bounded range
• this implementation does not handle quantifiers inside an assertion

[martin-cs]

There are some issues here:

1. Do you recall we discussed test cases and had a sufficient set on the board? You took a photo? I see that you've covered some of these but I'm not sure it's all of them.
2. If I understand correctly; you've moved the instantiation into simplify. I don't think this the right place for it as it means it will be removed before it gets to the solver, meaning that the different back-ends can't handle this in a smart way (i.e. creating an extra variable rather than expanding an existential into a disjunct). Please move this back to src/solvers/flattening. If you want, create a file in src/util/ for just the instantiation code, go for it. Simplify for quantifiers should just handle not(\exists(.)) -> \forall(not(.)) etc.

[theyoucheng]

Thanks Martin!

On 10/4/16 8:10 AM, Martin wrote:

There are some issues here:

Do you recall we discussed test cases and had a sufficient set on
the board? You took a photo? I see that you've covered some of
these but I'm not sure it's all of them.

I took the photo and I can add more regression tests.

If I understand correctly; you've moved the instantiation into
simplify. I don't think this the right place for it as it means it
will be removed before it gets to the solver, meaning that the
different back-ends can't handle this in a smart way (i.e.
creating an extra variable rather than expanding an existential
into a disjunct). Please move this back to src/solvers/flattening.
If you want, create a file in src/util/ for just the instantiation
code, go for it. Simplify for quantifiers should just handle
not(\exists(.)) -> \forall(not(.)) etc.

At first, I did implement it in "src/solvers/flattening/". However,
there are two difficulties.

• If the quantifier variable is the array index, I do not know how to
  enforce the array bound check
• In the solver end, I do not know how a good way to "simplify" a
  non-standard formula (e.g., when dealing with nested quantifiers) into a
  standard form. This makes the implementation redundant and cumbersome.

Therefore, I moved the code into simplify.

What if on one hand I simplify the quantifier by instantiating it but on
the other hand I keep the "quantifier information" in a way such that
optimization can be made in the solver end?

Let us find a time to talk more on this. Thanks!

Best,
Youcheng

—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
#245 (comment), or
mute the thread
https://github.com/notifications/unsubscribe-auth/ATYfm4aINNudpvJNpzlahyPJeRcZoNaGks5qwfvygaJpZM4KNLyL.

Youcheng Sun
Research Assistant
Department of Computer Science
University of Oxford
Wolfson Building, Parks Road
Oxford OX1 3QD
https://sites.google.com/site/theyoucheng/

[martin-cs]

On Tue, 2016-10-04 at 02:57 -0700, Youcheng Sun wrote:

Thanks Martin!

On 10/4/16 8:10 AM, Martin wrote:

There are some issues here:

Do you recall we discussed test cases and had a sufficient set on
the board? You took a photo? I see that you've covered some of
these but I'm not sure it's all of them.

I took the photo and I can add more regression tests.

Please do all of them. Some could give subtle errors and I would far
rather we found them in testing.

If I understand correctly; you've moved the instantiation into
simplify. I don't think this the right place for it as it means it
will be removed before it gets to the solver, meaning that the
different back-ends can't handle this in a smart way (i.e.
creating an extra variable rather than expanding an existential
into a disjunct). Please move this back to src/solvers/flattening.
If you want, create a file in src/util/ for just the instantiation
code, go for it. Simplify for quantifiers should just handle
not(\exists(.)) -> \forall(not(.)) etc.

At first, I did implement it in "src/solvers/flattening/". However,
there are two difficulties.

• If the quantifier variable is the array index, I do not know how to
  enforce the array bound check

This is an orthogonal concern. If they user wants bounds checks then
they should use --bound-check and that should add appropriate
assertions. This will need to be implemented but it is an independent
concern to how to do quantifier instantiation.

• In the solver end, I do not know how a good way to "simplify" a
  non-standard formula (e.g., when dealing with nested quantifiers) into a
  standard form. This makes the implementation redundant and cumbersome.

Is calling simplify_expr() not enough?

Therefore, I moved the code into simplify.

What if on one hand I simplify the quantifier by instantiating it but on
the other hand I keep the "quantifier information" in a way such that
optimization can be made in the solver end?

This will not solve the problem. The problem is that there are many
different ways of handling quantifiers. Complete instantiation before
solving is the most basic. It is sufficient for the use case at hand,
sort of, but long-term it is not the right thing to do. If we are using
the SMT (or other) backends, then the quantifiers must be presented to
them.

By implementing quantifier instantiation in the simplifier it will be
removed long before it gets to the back-end, in effect, forcing us to
only ever use complete, eager instantiation; even when the back-end is
capable of much more. It would be as much of a hack as the current way
of doing things that we were trying to fix in the first place. Given
that other people are working on string solvers to do smarter handling
of quantifiers this is not just a theoretical concern.

Let us find a time to talk more on this. Thanks!

I get back to the UK tomorrow night so I will be organising meetings for
the next few days.

Cheers,

• Martin

[kroening]

@theyoucheng can you please rebase?

[theyoucheng]

This is an obsolete pull request. The improvement for quantifier has been merged in a later patch #287

Best,
Youcheng