Handle forall quantifiers in LP-based reachability compiler

[gfrances]

As described in #73 by @anubhav-cs, the LP-based reachability compiler still does not handle universal quantifiers. We should implement that ASAP. Issue #73 contains some other hints and code for that.

[miquelramirez]

Does this need to be part of the default grounding pipeline for tarski @gfrances or it is something for the user to decide whether or not to do?

We have implemented already universal quantifier elimination in the framework, so it should be possible to reuse that code to compile away UniversalEffect into many LogicalEffect. Correct me if I am wrong, but then we could just use the LP grounder without problems. Or perhaps, do you think that integrating that into the LP grounding could result in more succinct formulae than doing quantifier elimination as a pre-processing step of the grounding?

[gfrances]

No, at the moment I cannot think of any better way of doing this than simply compiling away the universal quantifiers over the finite universe of the problem (note that the issue is about standard universal quantification in formulas, not about UniversalEffects!). Meaning that upon the user requesting any LP⁻related operation on some problem that features some universal quantifier in preconditions, effect conditions or goal, we should either:

1. Raise some exception and let the user deal with that (e.g. by explicitly preprocessing the problem to compile away these quantifiers.
2. Do this compilation of universal quantifiers ourselves, and then apply whatever operation was requested.

Do you have any preference? Maybe it's worth thinking about this carefully, as we'll run into this type of decisions over and over. Perhaps a good option would be to always raise if the syntactic features of the problem are not supported by the operation in the question, but then have some higher layer that does the necessary transformations (so that I as a user can choose not to care about them)

[anubhav-cs]

@gfrances @miquelramirez - I compiled away (forall ...) universal quantifiers in the preconditions using the UniversalQuantifierElimination. However, for a specific case - (forall ... (imply ...)), which is transformed into a compound formula with connective.Or in NNF form, the test results in error.

/tmp/tmpt9bkmrj5:229:1-18: error: unsafe variables in:
 __f1(P):-[#inc_base];1=1.
/tmp/tmpt9bkmrj5:229:6-7: note: 'P' is unsafe

The error is at the following rules in /tmp/tmpppz07mf_

__f1(P) :- 1 = 1.
__f1(P) :- started(o18).

This can be reproduced by cloning tarski-test and executing test.py. Also, here is the content of file - tmpt9bkmrj5

[miquelramirez]

Hi @anubhav-cs,

yep, if you have an imply you'll have to transform the formula into DNF and split the operators as per Gazen and Knoblock (so you end up with one operator per clause of the DNF formula).

Miquel.

[gfrances]

Hi @anubhav-cs,

this was due to a bug in the generation of the auxiliary LP rules that are created for subformulas such as disjunctions. Say we have a precondition "p and (q or r(x))". The logic program we generate will create an auxiliary predicate with some name like __f3(X), whose semantics will informally be "the subformula q or r(X)" is reachable. This is translated into LP rules

__f3(X) :- q.
__f3(X) :- r(X).

And then the whole precondition is translated into a rule

action_name(X) :- p, __f3(X).

The problem was that the above rule __f3(X) :- q is not safe, as X is not bound by anything. The standard solution is simply to qualify X with its type, e.g. __f3(X) :- q, object(X). This should be fixed in 62199846, at the moment in the devel branch. If you have a minute to try it, please let me know if you see any problems.

[miquelramirez]

Thanks @gfrances , @anubhav-cs is testing this atm.

[anubhav-cs]

Thanks @gfrances, I have tested it on sample problems and it is working fine.