Lazy grounding and groundwithbounds

[Bart Bogaerts]

To make lazy grounding work with groundwithbounds, we want the information of the propagaion to be used when creating generators. I did this in commit [[https://bitbucket.org/broesdecat/idp/changeset/467241565bdc39e5b89ea20b7361a6ec2f44dc01|467241565bdc39e5b89ea20b7361a6ec2f44dc01]]

Since the propagationinfo is now passed to the generators but NOT given to the structure, we can get a situation where some sentences are not grounded, but the information that allows to do that is not in the structure.

We should think about how this can be fixed since running over the entire structure to do LUP might be too expensive.
I believe the solution will be in lazily running over the structure: every time we ground an atom, we first check if
it satisfies the ct or the cf bdd in the symbolic structure.

[Bart Bogaerts]

I've checked a bit more details. Actually, there are two problems:

• What do we want to do? If lazy grounding is on, avoid running over the entire structure to do the "lifted unit propagation"
• BUT: we still want to use the information from the propagation. Hence, we should build our "generators and checkers" (BDD's), using the derived BDDs for atoms.
• PROBLEM 1: If we do this, we will decide to not ground some formulas based on information that is not in the structure. We should be able to guarantee that this information gets in the structure at some point. My proposal: do this at any point, but ONLY for the output vocabulary (in case of lazy grounding of course)
• PROBLEM 2: We should also guarantee that the grounder can NEVER decide an atom that might be decided by the propagation. Therefor, the atomgrounder should get the right grounders: the UNIMPROVED bdds should be used (we never want to lose info here) (only for atoms of course)

This being said, I will try to fix it ;-)

[Bart Bogaerts]

Additional remark: if we do it this way, it should be GUARANTEED that we will not try to find "alltwovaluedextensions" unless the output-voc is the entire vocabulary!

[Bart Bogaerts]

Added outputvocabulary to the createBounds

see issue 226 This was needed because in some cases we want to use groundwithbounds WITHOUT having to run over the entire structure with LUP THUS, we will only run over the outputvoc, the vocabulary that we are really interested in. Depending on the outputvoc, the options LUP and GWB, we can than decide wether or not we want to replace our atoms by their BDDs in the Symbolicstructure-evaluation

→ Wiki macro error: Changeset 32f57670ead9 not found.