|
| Date |
User |
Action |
Args |
| 2023-07-21 14:34:32 | malte | set | messages:
+ msg11152
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
- issue98: support derived predicates properly in our heuristics
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, issue111).
- 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
- issue98: support derived predicates properly in our heuristics
- issue111: Implement different ways to handle negative preconditions
Issues that have test cases that are important and we should consolidate:
- issue165
- issue450
- issue453
- issue862 |
| 2023-07-21 14:29:08 | malte | set | title: translator issues related to axioms and negative conditions -> issues related to axioms and negative conditions
messages:
+ msg11149
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 -> 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
- issue98: support derived predicates properly in our heuristics
Issues that have test cases that are important and we should consolidate:
- issue165
- issue450
- issue453
- issue862 |
| 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 |
| 2019-06-14 14:29:45 | silvan | set | nosy:
+ silvan |
| 2019-06-14 14:27:59 | malte | create | |