Reified HasKind test not working

[GoogleCodeExporter]

Former HasFunctor expression attributes has been named to HasKind.
The reason for that is that it must test quantified formulas.
They were incorrectly being tested by functor, but since they are not function 
applications, they do not have a functor.
So now HasKind returns a kind of expression, or its functor if it is a function 
application.

However, this attribute does seem to be considered when reified for quantified 
formulas (which have kind KindAttribute.VALUE_FOR_ALL and 
KindAttribute.VALUE_THERE_EXISTS).
This occurs in classes
QuantifierEliminationWrapper, ExistentialOut, and UniversalOut.
I have temporarily placed the test in their rewriterAfterBookeeping methods for 
now, where it works, but it would be good to undertand why reification is not 
working.

Original issue reported on code.google.com by rodrigob...@gmail.com on 30 Sep 2014 at 6:55

[GoogleCodeExporter]

Original comment by ctjoreilly@gmail.com on 30 Sep 2014 at 6:01

• Changed state: Started

[GoogleCodeExporter]

Fix applied in r911. The problem was that the logic in HasKind, which was 
renamed from HasFunctor, was only intended to work with functors and when it 
received a KindAttribute.<constant predicate> was wrappering this inside a 
Symbol i.e.:

Expressions.makeSymbol(kindValue)

instead now this only occurs if this is not true:

kindValue instanceof Expression || KindAttribute.isKindPredicate(kindValue)

In addition, all other code that was using KindAttribute predicates in the 
following way:

this.setReifiedTests(new DefaultRewriterTest(KindAttribute.INSTANCE, 
KindAttribute.VALUE_SCOPED_VARIABLES));

have been updated to use the new unified HasKind mechanism, i.e.:

this.setReifiedTests(new HasKind(KindAttribute.VALUE_SCOPED_VARIABLES));

in order to keep things consistent.

Original comment by ctjoreilly@gmail.com on 30 Sep 2014 at 8:53

• Changed state: Fixed