Merge pull request #107 from potassco/fix/parsing

fix parsing of numbers
potassco · Nov 29, 2023 · 50d8437 · 50d8437
2 parents b3535b7 + c8031c1
commit 50d8437
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 7 deletions.
diff --git a/libclingcon/src/parsing.cc b/libclingcon/src/parsing.cc
@@ -374,10 +374,10 @@ struct VectorHash {
 
 void push_co(val_t co, CoVarVec &res) { res.emplace_back(co, INVALID_VAR); }
 
-void push_co_var(val_t co, var_t var, CoVarVec &res) { res.emplace_back(co, var); }
-
 void push_co(val_t co, NonlinearTermVec &res) { res.emplace_back(co, VarVec{}); }
 
+void push_co_var(val_t co, var_t var, CoVarVec &res) { res.emplace_back(co, var); }
+
 void push_co_var(val_t co, var_t var, NonlinearTermVec &res) { res.emplace_back(co, VarVec{var}); }
 
 void push_co_vars(val_t co, var_t l_var, var_t r_var, CoVarVec &res) {
@@ -396,6 +396,15 @@ void push_co_vars(val_t co, VarVec const &l_vars, VarVec const &r_vars, Nonlinea
     res.emplace_back(co, std::move(vars));
 }
 
+void push_value(Clingo::Symbol const &sym, CoVarVec &res) {
+    check_syntax(sym.type() == Clingo::SymbolType::Number);
+    push_co(sym.number(), res);
+}
+
+void push_value(Clingo::Symbol const &sym, NonlinearTermVec &res) {
+    check_syntax(sym.type() == Clingo::SymbolType::Number);
+    push_co(sym.number(), res);
+}
 using Clingcon::simplify;
 
 auto simplify(NonlinearTermVec &vec, bool drop_zero) -> val_t {
@@ -493,7 +502,7 @@ void parse_constraint_elem(AbstractConstraintBuilder &builder, Clingo::TheoryTer
 
             auto b = evaluate(args.back());
             if (b.type() == Clingo::SymbolType::Number) {
-                push_co(-b.number(), res);
+                push_co(safe_inv(b.number()), res);
             } else {
                 push_co_var(-1, builder.add_variable(b), res);
             }
@@ -532,6 +541,8 @@ void parse_constraint_elem(AbstractConstraintBuilder &builder, Clingo::TheoryTer
                 push_co_vars(safe_mul(l_co, r_co), l_vars, r_vars, res);
             }
         }
+    } else if (match(term, "**", 2) || match(term, "/", 2) || match(term, "\\", 2)) {
+        push_value(evaluate(term), res);
     } else if (term.type() == Clingo::TheoryTermType::Symbol || term.type() == Clingo::TheoryTermType::Function ||
                term.type() == Clingo::TheoryTermType::Tuple) {
         push_co_var(1, builder.add_variable(evaluate(term)), res);
@@ -887,8 +898,8 @@ auto parse(AbstractConstraintBuilder &builder, Clingo::TheoryAtoms theory_atoms)
         bool is_sum_h = match(atom.term(), "__sum_h", 0);
         bool is_diff_b = match(atom.term(), "__diff_b", 0);
         bool is_diff_h = match(atom.term(), "__diff_h", 0);
-        bool is_nsum_h = match(atom.term(), "__nsum_b", 0);
-        bool is_nsum_b = match(atom.term(), "__nsum_h", 0);
+        bool is_nsum_h = match(atom.term(), "__nsum_h", 0);
+        bool is_nsum_b = match(atom.term(), "__nsum_b", 0);
         if (is_sum_b || is_sum_h) {
             if (!parse_constraint<CoVarVec>(builder, atom, is_sum_b)) {
                 return false;

diff --git a/libclingcon/tests/parsing.cc b/libclingcon/tests/parsing.cc
@@ -248,6 +248,7 @@ TEST_CASE("parsing", "[parsing]") {
     }
     SECTION("parse") {
         SECTION("sum head") {
+            REQUIRE(parse("&sum { 7; 2**3 } >= 0.") == "2 -> 0 <= 15.");
             REQUIRE(parse("&sum { x; y; z } = 0.") == "2 -> 1*x + 1*y + 1*z <= 0."
                                                       "2 -> -1*x + -1*y + -1*z <= 0.");
             REQUIRE(parse("&sum { x; y; z } != 0.") == "{ 3, 4, -2 }."
@@ -311,8 +312,8 @@ TEST_CASE("parsing", "[parsing]") {
             REQUIRE(parse("&maximize { x - z }.") == "#minimize { -1*x + 1*z }.");
         }
         SECTION("nonlinear") {
-            REQUIRE(parse("&nsum { 2*x*y + 3*z + 4 } <= 5.") == "2 -> 2*x*y + 3*z <= 1."
-                                                                "-2 -> -2*x*y + -3*z <= -2.");
+            REQUIRE(parse("&nsum { 2*x*y + 3*z + 4 } <= 5.") == "2 -> 2*x*y + 3*z <= 1.");
+            REQUIRE(parse("&nsum { (2**3)*x*y + (3**4)*z + (5**6) } <= 5.") == "2 -> 8*x*y + 81*z <= -15620.");
         }
     }
 }