{{{
Hi Ciaran,
Good call on the change to R_sum_over_one.
I thought some more about this and I think we cannot for now support the
ASSUME_DOMAIN_ALWAYS_LARGE flag and quantifier elimination at the same time.
This is because the flag leads to the derivation of polynomials representing
cardinalities, and quantifier elimination places those expressions in
conditions against other numbers, requiring us to solve polynomials. There is
probably a not too complicated way of doing this but that's besides our scope
for now. So I say let's mark the tests with both unknown size types and
quantifiers as unsupported for now and hopefully one day we get to them.
Thanks,
Rodrigo
On 7/30/2012 11:05 PM, Ciaran O'Reilly wrote:
> Hi Rodrigo,
>
> I've gone ahead and implemented an initial version of this (SVN rev=1318),
though as described below it is not able to handle quantifiers.
>
> As an overview of where I am with this, my understanding is that the changes
you outlined were with respect to R_card1_conjunction, where you wanted to
change:
>
> if F is x != t1 and ... x != tk and Phi, where x does not occur in Phi
> if quantification is "for all"
> return 0
> if quantification is "there exists" and |type(X)| > k
> return R_simplify(if Phi then |type(X)| else 0)
>
> to:
>
> if F is x != t1 and ... x != tk and Phi, where x does not occur in Phi
> if quantification is "for all"
> and (ASSUME_DOMAIN_ALWAYS_LARGE or |type(X)| > 0)
> return 0
> if quantification is "there exists"
> and (ASSUME_DOMAIN_ALWAYS_LARGE or |type(X)| > k)
> return R_simplify(if Phi then |type(X)| else 0
>
> and that:
>
> > *where *ASSUME_DOMAIN_ALWAYS_LARGE is said flag. Do you think that would ddd
> > be enough?
>
> Not completely. The logic in R_sum_over_one_variable also needed to be
updated as was restricted to conditionals and numeric constants, i.e.:
>
> S is a numeric constant expression.
> if S is 0
> return 0
> else
> return R_simplify(R_card1_with_heuristic(|Cx|_x, "none") * S)
>
> was changed to:
>
> ASSUME_DOMAIN_ALWAYS_LARGE or S is a numeric constant expression.
> if S is 0
> return 0
> else
> return R_simplify(R_card1_with_heuristic(|Cx|_x, "none") * S)
>
> If you look at the DirectCardinalityTests for testCardinality() you'll see
that the code tests both scenarios now for when the flag is and is not set -
i.e. a tuple of expected results are now checked.
>
> However, I had to comment out several tests in testCardinality() for the time
being as the logic in R_card1 is not capable currently of handling quantified
expressions when the ASSUME_DOMAIN_ALWAYS_LARGE assumption is true, for example
(I've left this specific test commented out at the end of testCardinality() so
you can look at in detail if you like):
>
> R_card({ ( on X ) tuple(X) | there exists Y : X != Y or Y != Z })
>
> when calling R_top_quantifier_elimination as part of the R_card1 logic for
quantifier elimination will calculate this :
>
> if X = Z then 1 = | type(Y) | else 0 = | type(Y) |
>
> which is not currently handled when you call back into R_card1, i.e:
>
> R_card1( | R_top_quantifier_elimination(Q y : G) |_x, quantification )
>
> The code treats this is an unknown expression and throws an exception. Let me
know what you think.
>
> Thanks
>
> Ciaran
>
> On 7/30/2012 12:35 PM, Rodrigo de Salvo Braz wrote:
>> Hi Ciaran,
>>
>> I am thinking that this is just a matter of replacing
>>
>> if quantification is "there exists" and |type(X)| > k
>> return R_simplify( if Phi then |type(X)| else 0)
>>
>> by
>>
>> *if quantification is "there exists" and
>>
>> ( ASSUME_DOMAIN_ALWAYS_LARGE or |type(X)| > k )
>>
>> return R_simplify( if Phi then |type(X)| else 0)
>>
>> *where *ASSUME_DOMAIN_ALWAYS_LARGE is said flag. Do you think that would
>> be enough? Let me know if you would like to discuss more.
>>
>> Incidentally, I also correct and introduced the same flag to the
>> condition that comes right before from
>>
>> if quantification is "for all"
>> return 0
>>
>> to
>>
>> **if quantification is "for all" and
>> ( **ASSUME_DOMAIN_ALWAYS_LARGE or **|type(X)| > 0)
>> return 0*
>>
>> Thanks,
>>
>> Rodrigo
>> *
>> *On 7/29/2012 10:34 PM, Ciaran O'Reilly wrote:
>>> Hi Rodrigo,
>>>
>>> Based on the email I just sent you with respect to 'Issues encountered
>>> when trying to replace R_formula_simplification with R_simplify' I
>>> think I'll need to go ahead and address what you outline below next,
>>> which I think I'll need to go over with you via a tele-conf if that's
>>> ok as you mentioned you'd a clear idea how this should be implemented.
>>>
>>> Thanks
>>>
>>> Ciaran
>>>
>>> On 6/15/2012 3:15 PM, Rodrigo de Salvo Braz wrote:
>>>> Hi Ciaran,
>>>>
>>>> I spent some time thinking of the issue with known type sizes. I was
>>>> thinking of the nice examples in LBPTest in which type sizes are unknown
>>>> and part of the answer. I think those examples are actually being solved
>>>> under an assumption that type sizes are always large enough not to cause
>>>> an existential quantification to be false (or, in other words, to make a
>>>> formula unsatisfiable), and that the only source of them being false
>>>> (unsatisfiable) is the actual quantified formula being false. For
>>>> example, we assume that "X != a and X !=b" is always satisfiable, but
>>>> that is only true if |type(X)| is greater than 2.
>>>>
>>>> I think a good way to deal with this without throwing away those
>>>> examples is to introduce a process flag turning this assumption on and
>>>> off. Then we can leave it on for those examples, or for any cases in the
>>>> future in which we want to say: I don't know the type sizes, but I know
>>>> they are always larger than the number of constants being processed.
>>>>
>>>> This flag will then be used in that code we were just discussing. When
>>>> quantification is "there exists", we return |type(X)| without having to
>>>> look at the extensional set cardinality.
>>>>
>>>> And if we don't have the flag on, then we must have the type sizes.
>>>>
>>>> Incidentally, in the future we will want to deal with unknown type
>>>> sizes. This means dealing with constraints looking like
>>>> 2*|type(X)|*|type(Y)|*|type(W)| + |type(Y)|*|type(Z)| -
>>>> |type(W)|*|type(Z)| = 30
>>>>
>>>> The general case is multi-variable polynomials, for integer variables.
>>>> Then we need to decide when these things are satisfiable (I don't think
>>>> we need to solve model counting on them). As of now, no clue on how to
>>>> do it
>>>>
>>>> Actually, I think we would not *have* to solve them. We could simply
>>>> leave them there and branch on their being true or false, but that would
>>>> create large trees that would have been simplified otherwise.
>>>>
>>>> Thanks,
>>>>
>>>> Rodrigo
}}}
Original issue reported on code.google.com by ctjoreilly@gmail.com on 11 Apr 2013 at 12:19
Original issue reported on code.google.com by
ctjoreilly@gmail.comon 11 Apr 2013 at 12:19