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).
- Do something about the combinatorial explosion with the DNF conversion
(e.g. issue450).
- Remove negated rules from the output and compute it in the search
component if needed (issue454).
- Remove axiom layers from the output and compute it in the search
component if needed (issue978).
- Document that derived variables must be binary (issue54).
- Simplify axioms (issue161)
- See if the changes to the output format impact issue371.
Related issues and messages:
- issue54: non-binary derived variables currently not supported
- issue161: simplify axioms
- issue165: partly or fully the same thing as issue450 (see below)
- issue371: wishes for the output format
- 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
(outdated after the merge of issue453)
- 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

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

2020-07-22 13:37:20

salome

set

title: translator bugs related to axioms and negative conditions -> translator issues related to axioms and negative conditions messages:
+ msg9666 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 -> What needs to be done:
~~- Finish refactoring of axiom_rules.py (issue453).~~
~~- Try different options for axiom_rules.py (within issue453).~~
- Do something about the combinatorial explosion with the DNF conversion
(e.g. issue450).
- Remove negated rules from the output and compute it in the search
component if needed (issue454).
- Remove axiom layers from the output and compute it in the search
component if needed (issue978).
- Document that derived variables must be binary (issue54).
- Simplify axioms (issue161)
- See if the changes to the output format impact issue371.
Related issues and messages:
- issue54: non-binary derived variables currently not supported
- issue161: simplify axioms
- issue165: partly or fully the same thing as issue450 (see below)
- issue371: wishes for the output format
- 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
(outdated after the merge of issue453)
- 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 18:22:31

salome

set

messages:
+ 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