Arithmetic term rewriter #263
Conversation
- Obtain from ExternalAtom its input/output literals, and lower/upper bounds from IntervalTerm. - Add ArithmeticTermsRewriting. - In AlphaTest create mutable list of rules for Program.
Codecov Report
@@ Coverage Diff @@
## master #263 +/- ##
============================================
+ Coverage 77.42% 77.68% +0.26%
- Complexity 2312 2362 +50
============================================
Files 178 179 +1
Lines 7788 7897 +109
Branches 1354 1387 +33
============================================
+ Hits 6030 6135 +105
Misses 1336 1336
- Partials 422 426 +4
Continue to review full report at Codecov.
|
# Conflicts: # src/main/java/at/ac/tuwien/kr/alpha/common/atoms/ExternalAtom.java # src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java # src/test/java/at/ac/tuwien/kr/alpha/api/AlphaTest.java
There was a problem hiding this comment.
This looks good! There are a couple of minor issues with regards to readability and test coverage which I noted in the respective detailed comments.
Since I know it's time-consuming, the following is purely a suggestion, but I think it would make sense to write a bit of documentation about how arithmetic term handling now works from an ASP programmer's point of view, i.e. "what can I do?", "which types of expressions are (or aren't) supported", "(high-level) what are my expressions rewritten to?". I think this could go into the pull request description. I'm planning to do the same thing for my currently open PR for aggregates - if we start documenting new features this way, we would have a starting point for things that can eventually be consolidated into a manual for Alpha.
| @@ -110,6 +111,25 @@ private static boolean unifyTerms(Term left, Term right, Unifier currentSubstitu | |||
| } | |||
| return true; | |||
| } | |||
| if (leftSubs instanceof ArithmeticTerm && rightSubs instanceof ArithmeticTerm) { | |||
There was a problem hiding this comment.
Since Unification#unifyTerms is already pretty long and also recursive, would it make sense to split it up into a few methods? I was thinking something along the lines of unifyFunctionTerms, unifyArithmeticTerms, unifyWithVariableTerm, basically getting each of the ifs and accompanying recursive calls into their own method.
There was a problem hiding this comment.
As we discussed, I do not think that splitting this up into multiple methods increases readability much.
| final ArithmeticTerm leftArithmeticTerm = (ArithmeticTerm) leftSubs; | ||
| final ArithmeticTerm rightArithmeticTerm = (ArithmeticTerm) rightSubs; | ||
| if (!leftArithmeticTerm.getArithmeticOperator().equals(rightArithmeticTerm.getArithmeticOperator())) { | ||
| return false; |
There was a problem hiding this comment.
Codecov is complaining that this and the other return false;s in this method aren't covered by any tests. In general, I couldn't find any dedicated unit tests for Unification. I thínk it would make sense to create a new UnificationTest that specifically checks correct behavior of Unifications public methods (thereby covering the whole class).
There was a problem hiding this comment.
Test cases added, I hope those statements are now better covered.
| } else if (atomToRewrite instanceof ExternalAtom) { | ||
| // Rewrite output terms, as so-far only the input terms list has been rewritten. | ||
| List<Term> rewrittenOutputTerms = new ArrayList<>(); | ||
| for (Term term : ((ExternalAtom) atomToRewrite).getOutput()) { |
There was a problem hiding this comment.
Codecov is complaining that the ExternalAtom part is not covered by any tests. Generally, I think it would make sense to have a dedicated ArithmeticTermsRewritingTest in addition to the existing (more "regession-test-like") ArithmeticTermsTest. The advantage of such a "real unit test" would be (in addition to codecov being able to measure coverage better) that a set of more fine-grained tests would also be an ideal starting point for debugging if ever any issues related to this code occurred.
There was a problem hiding this comment.
ArithmeticTermsRewritingTest is now also included.
- Polished ArithmeticTermsRewriting a bit. - Add ArithmeticTermsRewritingTest, also testing with ExternalAtoms.
Add ArithmeticTerm rewriting, allowing arithmetic expressions in ordinary literals and heads. Fixes #260 and checks another item from #89.
The rewriting works as follows:
for every rule, take every arithmetic expression
Ethat occurs in an atomAthat is not aComparisonLiteral, replaceEinAwith a fresh variableVand add to the body of the rule a newComparisonLiteralwith contentsV = E.For example:
p(X+1) :- q(Y/2), r(f(X*2),Y), X-2 = Y*3, X = 0..9.is rewritten to
p(_A1) :- q(_A2), r(f(_A3),Y), X-2 = Y*3, X = 0..9, _A1 = X+1, _A2 = Y/2, _A3 = X*2.where
_A1,_A2, and_A3are new variables starting with_to prevent name clashes with variables from the input program.[Note that due to recursion, the literals in the actual rewritten rule are ordered differently, to be precise:
p(_A1) :- _A1 = X+1, _A2 = Y/2, q(_A2), _A3 = X*2, r(f(_A3),Y), X-2 = Y*3, X = 0..9., but that should be rather irrelevant for the solver.]