Petar Vukmirovic
2020-03-13 19:39:3 (GMT)
Hi Simon!
I have been working on my PAAR paper and I have always been amazed by your ElimPredVar rule
Petar Vukmirovic
2020-03-13 19:40:38 (GMT)
I took the liberty to document it in our paper, but fully acknowledged that you are the author of the rule
image.png
Petar Vukmirovic
2020-03-13 19:41:26 (GMT)
However, I think that there is a bug in the implementation
Petar Vukmirovic
2020-03-13 19:44:24 (GMT)
for sure after substitution
this will get clausified in many many clauses
Petar Vukmirovic
2020-03-13 19:44:30 (GMT)
however, Zipperposition creates only one
Petar Vukmirovic
2020-03-13 19:44:48 (GMT)
if you would look at the end of the funciton that implements this rule,
Petar Vukmirovic
2020-03-13 19:45:44 (GMT)
it does not perform any clausification.
Petar Vukmirovic
2020-03-13 19:46:33 (GMT)
can you
- check if I did not make any claims (and if you agree that this rule is documented in our paper)
- check if the implementation is indeed not buggy.
Simon Cruanes
2020-03-13 20:33:13 (GMT)
Petar Vukmirovic said:
however, Zipperposition creates only one
I think I was just lazy and relied on some simplification rule to CNF this away later. I didn't see other bugs in the implementation.
I totally agree with the rule being in the paper, yes :slight_smile: . It seems correct, although (as many things) it's fuzzy in my head now. It does eliminate the negative literals.
Petar Vukmirovic
2020-03-13 22:54:31 (GMT)
Thanks a lot
Petar Vukmirovic
2020-03-13 22:54:56 (GMT)
My biggest problem is that I do not think that the literals are created as they should be
Petar Vukmirovic
2020-03-13 22:55:8 (GMT)
New clauses that are created as results of this rule
Petar Vukmirovic
2020-03-13 22:55:17 (GMT)
Should be pairs of literals
Simon Cruanes
2020-03-13 23:13:56 (GMT)
So it could be more of a problem in CNF's postprocessing?
Petar Vukmirovic
2020-03-14 10:8:31 (GMT)
well this rule does not do any CNF reasoning
Petar Vukmirovic
2020-03-14 10:9:12 (GMT)
I changed it so that it removes negative literals, and applies the subst to positive literals, relying on CNF afterwards to correctly clausify the "clause"
Simon Cruanes
2020-03-14 19:25:33 (GMT)
The CNF reasoning is done in other rules, iirc. But I might be wrong.