tweak parsing of &dom directives

potassco · Jun 21, 2024 · 04bf958 · 04bf958
1 parent 3b05c9a
commit 04bf958
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 7 deletions.
diff --git a/libclingcon/clingcon/parsing.hh b/libclingcon/clingcon/parsing.hh
@@ -38,7 +38,6 @@ namespace Clingcon {
 //! This theory has to be loaded to use CSP constraints.
 constexpr char const *THEORY = R"(
 #theory cp {
-    var_term  { };
     sum_term {
     -  : 3, unary;
     ** : 2, binary, right;
@@ -79,7 +78,7 @@ constexpr char const *THEORY = R"(
     &show/0 : sum_term, directive;
     &distinct/0 : sum_term, head;
     &disjoint/0 : disjoint_term, head;
-    &dom/0 : dom_term, {=}, var_term, head
+    &dom/0 : dom_term, {=}, sum_term, head
 }.
 )";
 
@@ -117,8 +116,8 @@ class AbstractConstraintBuilder {
     //! Extend the minimize constraint.
     virtual void add_minimize(val_t co, var_t var) = 0;
     //! Add a distinct constraint.
-    [[nodiscard]] virtual auto add_distinct(lit_t lit, std::vector<std::pair<CoVarVec, val_t>> const &elems)
-        -> bool = 0;
+    [[nodiscard]] virtual auto add_distinct(lit_t lit,
+                                            std::vector<std::pair<CoVarVec, val_t>> const &elems) -> bool = 0;
     //! Add a disjoint constraint.
     [[nodiscard]] virtual auto add_disjoint(lit_t lit, CoVarVec const &elems) -> bool = 0;
     //! Add a domain for the given variable.

diff --git a/libclingcon/src/parsing.cc b/libclingcon/src/parsing.cc
@@ -30,7 +30,6 @@
 #include <numeric>
 #include <set>
 #include <unordered_map>
-#include <unordered_set>
 
 namespace Clingcon {
 
@@ -698,8 +697,8 @@ template <class TermVec>
 // Contraints are represented as a triple of a literal, its elements, and an
 // upper bound.
 template <class TermVec, bool is_sum = true>
-[[nodiscard]] auto parse_constraint(AbstractConstraintBuilder &builder, Clingo::TheoryAtom const &atom, bool strict)
-    -> bool {
+[[nodiscard]] auto parse_constraint(AbstractConstraintBuilder &builder, Clingo::TheoryAtom const &atom,
+                                    bool strict) -> bool {
     check_syntax(atom.has_guard());
 
     TermVec elements;
@@ -797,6 +796,7 @@ void parse_show(AbstractConstraintBuilder &builder, Clingo::TheoryAtom const &at
 
     check_syntax(atom.has_guard(), "Invalid Syntax: invalid dom statement");
     auto var = evaluate(atom.guard().second);
+    check_syntax(var.type() != Clingo::SymbolType::Number, "Invalid Syntax: invalid dom statement");
 
     return builder.add_dom(builder.solver_literal(atom.literal()), builder.add_variable(var), elements);
 }