Issue924

Title translator bugs related to axioms and negative conditions
Priority meta Status chatting
Superseder Nosy List augusto, cedric, gabi, jendrik, malte, salome, silvan
Assigned To Keywords translator
Optional summary
What needs to be done:
- Finish refactoring of axiom_rules.py (issue453).
- Try different options for axiom_rules.py (within issue453):
  - overapproximate negated axioms: 1) current way (negate = buggy),
    2) trivially overapproximate; 3) trivially overapproximate for cycles,
    negate when there are no cycles
  - keep redundant positive axioms: yes/no (=> in the medium term, we would
    like to always have the positive form as the "real" form)
  - layers: use minimum number of layers (as currently) or maximum number of
    layer (=> in the medium term, we probably only want to decide on one
    of these two)
  - overapproximate necessary literals: 1) full relevance analysis 2) consider 
    all non-derived literals as necessary 3) old implementation
    (The old implementation considered all positive literals as necessary,
    which is wrong but usually works well. Ideally we will decide between
    1 and 3 or keep 1 and 3 as options)
- Do something about the combinatiorial explosion with the DNF conversion
  (e.g. issue450).

Related issues and messages:
- issue165: partly or fully the same thing as issue450 (see below)
- issue450: negating axiom rules is implemented as a CNF-to-DNF conversion,
which can explode exponentially
- issue453: axiom semantics when negated are wrong because the idea of just
negating the formula that encodes the triggering conditions is semantically wrong
- issue454: about getting rid of negated axiom rules in the translator
- msg8204: explains the axiom code and contains notes and what could be improved
- msg8235: lists which domains and search configurations are relevant when
dealing with the axioms

Issues that have test cases that are important and we should consolidate:
- issue165
- issue450
- issue453
- issue862

Created on 2019-06-14.14:27:59 by malte, last changed by salome.

Summary
What needs to be done:
- Finish refactoring of axiom_rules.py (issue453).
- Try different options for axiom_rules.py (within issue453):
  - overapproximate negated axioms: 1) current way (negate = buggy),
    2) trivially overapproximate; 3) trivially overapproximate for cycles,
    negate when there are no cycles
  - keep redundant positive axioms: yes/no (=> in the medium term, we would
    like to always have the positive form as the "real" form)
  - layers: use minimum number of layers (as currently) or maximum number of
    layer (=> in the medium term, we probably only want to decide on one
    of these two)
  - overapproximate necessary literals: 1) full relevance analysis 2) consider 
    all non-derived literals as necessary 3) old implementation
    (The old implementation considered all positive literals as necessary,
    which is wrong but usually works well. Ideally we will decide between
    1 and 3 or keep 1 and 3 as options)
- Do something about the combinatiorial explosion with the DNF conversion
  (e.g. issue450).

Related issues and messages:
- issue165: partly or fully the same thing as issue450 (see below)
- issue450: negating axiom rules is implemented as a CNF-to-DNF conversion,
which can explode exponentially
- issue453: axiom semantics when negated are wrong because the idea of just
negating the formula that encodes the triggering conditions is semantically wrong
- issue454: about getting rid of negated axiom rules in the translator
- msg8204: explains the axiom code and contains notes and what could be improved
- msg8235: lists which domains and search configurations are relevant when
dealing with the axioms

Issues that have test cases that are important and we should consolidate:
- issue165
- issue450
- issue453
- issue862
Messages
msg8909 (view) Author: salome Date: 2019-06-14.18:22:31
Add option "overapproximate necessary literals" to the collection of options in
the summary
msg8905 (view) Author: malte Date: 2019-06-14.14:27:59
There is a tangled web of issues related to bugs related to axioms and negated
conditions. They have a somewhat messy overlap, so in this meta-issue we try to
introduce a bit of order and collect TODOs.
History
Date User Action Args
2019-06-14 18:22:31salomesetmessages: + msg8909
summary: What needs to be done: - Finish refactoring of axiom_rules.py (issue453). - Try different options for axiom_rules.py (within issue453): - overapproximate negated axioms: 1) current way (negate = buggy), 2) trivially overapproximate; 3) trivially overapproximate for cycles, negate when there are no cycles - keep redundant positive axioms: yes/no (=> in the medium term, we would like to always have the positive form as the "real" form) - layers: use minimum number of layers (as currently) or maximum number of layer (=> in the medium term, we probably only want to decide on one of these two) - Do something about the combinatiorial explosion with the DNF conversion (e.g. issue450). Related issues and messages: - issue165: partly or fully the same thing as issue450 (see below) - issue450: negating axiom rules is implemented as a CNF-to-DNF conversion, which can explode exponentially - issue453: axiom semantics when negated are wrong because the idea of just negating the formula that encodes the triggering conditions is semantically wrong - issue454: about getting rid of negated axiom rules in the translator - msg8204: explains the axiom code and contains notes and what could be improved - msg8235: lists which domains and search configurations are relevant when dealing with the axioms Issues that have test cases that are important and we should consolidate: - issue165 - issue450 - issue453 - issue862 -> What needs to be done: - Finish refactoring of axiom_rules.py (issue453). - Try different options for axiom_rules.py (within issue453): - overapproximate negated axioms: 1) current way (negate = buggy), 2) trivially overapproximate; 3) trivially overapproximate for cycles, negate when there are no cycles - keep redundant positive axioms: yes/no (=> in the medium term, we would like to always have the positive form as the "real" form) - layers: use minimum number of layers (as currently) or maximum number of layer (=> in the medium term, we probably only want to decide on one of these two) - overapproximate necessary literals: 1) full relevance analysis 2) consider all non-derived literals as necessary 3) old implementation (The old implementation considered all positive literals as necessary, which is wrong but usually works well. Ideally we will decide between 1 and 3 or keep 1 and 3 as options) - Do something about the combinatiorial explosion with the DNF conversion (e.g. issue450). Related issues and messages: - issue165: partly or fully the same thing as issue450 (see below) - issue450: negating axiom rules is implemented as a CNF-to-DNF conversion, which can explode exponentially - issue453: axiom semantics when negated are wrong because the idea of just negating the formula that encodes the triggering conditions is semantically wrong - issue454: about getting rid of negated axiom rules in the translator - msg8204: explains the axiom code and contains notes and what could be improved - msg8235: lists which domains and search configurations are relevant when dealing with the axioms Issues that have test cases that are important and we should consolidate: - issue165 - issue450 - issue453 - issue862
2019-06-14 14:29:45silvansetnosy: + silvan
2019-06-14 14:27:59maltecreate