properly handle diff terms

README.md

@@ -77,8 +77,9 @@ is equivalent to
 ```
 
 Another shortcut (for compatibility with [clingo-dl]) are `&diff` constraints.
-Terms in braces must be variables and the right-hand-side must be a number.
-The same relations as for &sum constraints are accepted. 
+The same relations as for &sum constraints are accepted.
+Terms in braces must should be variables and the right-hand-side should be a number.
+The program
 ```
 { x }.
 &diff { a-b } <= 5.

libclingo-lpx/src/parsing.cc

@@ -242,7 +242,8 @@ struct EvaluateNum {
     return std::visit(EvaluateNum{}, evaluate(true, term));
 }
 
-void parse_diff_elem(Clingo::TheoryTerm const &term, std::vector<Term> &res) {
+auto parse_diff_elem(Clingo::TheoryTerm const &term) -> std::vector<Term> {
+    std::vector<Term> res;
     if (match(term, "-", 2)) {
         auto args = term.arguments();
         std::visit(
@@ -268,6 +269,7 @@ void parse_diff_elem(Clingo::TheoryTerm const &term, std::vector<Term> &res) {
     } else {
         throw_syntax_error("Invalid Syntax: invalid difference constraint");
     }
+    return res;
 }
 
 void parse_sum_elem(Clingo::TheoryTerm const &term, std::vector<Term> &res) {
@@ -396,9 +398,12 @@ void parse_theory(Clingo::TheoryAtoms const &theory, LitMapper const &mapper, Va
             check_syntax(atom.has_guard() && atom.elements().size() == 1 &&
                              atom.elements().front().tuple().size() == 1 && atom.elements().front().condition().empty(),
                          "&diff invalid difference constraint");
-            auto lhs = std::vector<Term>{};
-            auto &&elem = *atom.elements().begin();
-            parse_diff_elem(elem.tuple().front(), lhs);
+            auto lhs = parse_diff_elem(atom.elements().begin()->tuple().front());
+            size_t n = lhs.size();
+            parse_sum_elem(atom.guard().second, lhs);
+            for (auto it = lhs.begin() + n, ie = lhs.end(); it != ie; ++it) {
+                it->co.neg();
+            }
             auto rhs = simplify(cos, lhs);
             auto lit = mapper(atom.literal());
             iqs.emplace_back(Inequality{std::move(lhs), std::move(rhs), evaluate_cmp(atom.guard().first), lit});

libclingo-lpx/src/parsing.hh

@@ -24,7 +24,7 @@ constexpr char const *THEORY = R"(
     &minimize/0 : sum_term, directive;
     &maximize/0 : sum_term, directive;
     &sum/0      : sum_term, {<=,=,>=}, sum_term, head;
-    &diff/0     : sum_term, {<=,=,>=}, diff_term, head;
+    &diff/0     : sum_term, {<=,=,>=}, sum_term, head;
     &dom/0      : dom_term, {=}, dom_term, head
 }.
 )";
@@ -49,7 +49,7 @@ constexpr char const *THEORY_Q = R"(
     &minimize/0 : sum_term, directive;
     &maximize/0 : sum_term, directive;
     &sum/0      : sum_term, {<=,=,>=,<,>}, sum_term, head;
-    &diff/0     : sum_term, {<=,=,>=,<,>}, diff_term, head;
+    &diff/0     : sum_term, {<=,=,>=,<,>}, sum_term, head;
     &dom/0      : dom_term, {=}, dom_term, head
 }.
 )";