Generating functions <-> predicates
In e.g. dfasat, the generator when Trans is a partial function is much more complex than the generator for when Trans is a predicate. Trans is given in the structure. Can we improve this?
Comments (7)
-
-
Removed partial-function checks from GenerateBddAccToBounds
For 3 reasons: * They were incorrect: only conditions about having an image were added, never about not having one (in the different cases true/false, other things should have happened) resulting in generating too much * They were not needed: out-of-bounds checks happen by the type checks above, other non-image checks happen by taking the inverse of the graphinter at appropriate places * They slowed down the grounding A LOT see issue
#375. Fixes it at least partially, but I didn't compare with the predicate version yet.→ <<cset f32cd1a9e798>>
-
Removed partial-function checks from GenerateBddAccToBounds
For 3 reasons: * They were incorrect: only conditions about having an image were added, never about not having one (in the different cases true/false, other things should have happened) resulting in generating too much * They were not needed: out-of-bounds checks happen by the type checks above, other non-image checks happen by taking the inverse of the graphinter at appropriate places * They slowed down the grounding A LOT see issue
#375. Fixes it at least partially, but I didn't compare with the predicate version yet.→ <<cset eecc61e04e12>>
-
reporter - changed status to resolved
-
reporter Refs
#375: history rename→ <<cset 256717e3e870>>
-
reporter -
Refs
#375: history rename→ <<cset 9e9a1c890bc8>>
- Log in to comment
Removed partial-function checks from GenerateBddAccToBounds
For 3 reasons: * They were incorrect: only conditions about having an image were added, never about not having one (in the different cases true/false, other things should have happened) resulting in generating too much * They were not needed: out-of-bounds checks happen by the type checks above, other non-image checks happen by taking the inverse of the graphinter at appropriate places * They slowed down the grounding A LOT see issue
#375. Fixes it at least partially, but I didn't compare with the predicate version yet.→ <<cset 446365dbd247>>