Infinitely many false defineds

[Stef De Pooter]

Model expansion on the following example will result in addition of infinitely many false-defineds (and so, run forever). {{{ #!idp vocabulary V { P(nat) } theory T : V { { P(1). } } }}}

We might be able to avoid this is certain cases... The false-defineds (negative literals) only need to be added when they are needed. So we might be able to generate a dependency graph for the defined predicates and find out we do not need the negative literals.

[Stef De Pooter]

Made it possible to stop idp while adding falsedefineds.

There should be a way to avoid addition of infinitely many falsedefineds. See issue #95.

→ 8f624631821e

[Bart Bogaerts]

Made it possible to stop idp while adding falsedefineds.

There should be a way to avoid addition of infinitely many falsedefineds. See issue #95.

→ 8f624631821e

[Broes De Cat]

Invalid for model expansion (need full model). Solved for satisfiability check and bounded model expansion by theorem proving or lazy grounding.