fix "variable only occurs once" checker

src/ast/transform/SemanticChecker.cpp

@@ -517,44 +517,113 @@ void SemanticCheckerImpl::checkClause(const Clause& clause) {
 }
 
 void SemanticCheckerImpl::checkComplexRule(const std::set<const Clause*>& multiRule) {
-    std::map<std::string, int> var_count;
-    std::map<std::string, const ast::Variable*> var_pos;
-
-    auto count_var = [&](const ast::Variable& var) {
-        const auto& varName = var.getName();
-        if (0 == var_count[varName]++) {
-            var_pos[varName] = &var;
-        } else {
-            const auto& PrevLoc = var_pos[varName]->getSrcLoc();
-            const auto& Loc = var.getSrcLoc();
-            if (PrevLoc < Loc) {
-                var_pos[varName] = &var;
+    // variable v occurs only once if:
+    // - it occurs at most once in each clause body of the (possibly) multi-clause rule.
+    // - and it never occurs in any clause head of the (possibly) multi-clause rule.
+    //
+    // note that ungrounded variables are already detected by another check so
+    // we don't report them here (ungrounded variables warning, argument in
+    // fact is not constant warning).
+
+    /// variables that occurs in some clause head, these variables are not
+    /// candidate to "occurs only once" warning.
+    std::set<std::string> varOccursInSomeHead;
+
+    /// variables that occurs more than once in some clause body, these
+    /// variables are not candidate to "occurs only once" warning.
+    std::set<std::string> varOccursMoreThanOnceInSomeBody;
+
+    /// variables that never occur in clause head, and at most once in
+    /// each clause body, these variables "occurs only once".
+    std::set<std::string> varOccursAtMostOnce;
+
+    struct VarsCounter : public Visitor<void> {
+        // map from variable name to the occurrence count
+        std::map<std::string, int> occurrences;
+
+        void visit_(type_identity<ast::Variable>, const ast::Variable& var) override {
+            const auto& name = var.getName();
+            if (name[0] == '_') {
+                // do not count variables starting with underscore
+                return;
+            }
+            auto it = occurrences.find(name);
+            if (it == occurrences.end()) {
+                occurrences[name] = 1;
+            } else {
+                it->second += 1;
             }
         }
     };
 
-    // Count the variable occurrence for the body of a
-    // complex rule only once.
-    // TODO (b-scholz): for negation / disjunction this is not quite
-    // right; we would need more semantic information here.
-    for (auto literal : (*multiRule.begin())->getBodyLiterals()) {
-        visit(*literal, count_var);
+    {  // find variables that occurs in some clause head
+        VarsCounter vc;
+        for (const Clause* cl : multiRule) {
+            // count occurrences in clause head
+            visit(cl->getHead(), vc);
+        }
+        for (const auto& entry : vc.occurrences) {
+            varOccursInSomeHead.emplace(entry.first);
+        }
     }
 
-    // Count variable occurrence for each head separately
-    for (auto clause : multiRule) {
-        visit(*(clause->getHead()), count_var);
+    for (const Clause* cl : multiRule) {
+        // TODO (b-scholz): for negation / disjunction this is not quite
+        // right; we would need more semantic information here.
+        VarsCounter vc;
+        for (auto lit : cl->getBodyLiterals()) {
+            visit(*lit, vc);
+        }
+
+        for (const auto& entry : vc.occurrences) {
+            const std::string name = entry.first;
+            if (varOccursInSomeHead.count(name) > 0) {
+                // variable occurs in some head => not a candidate for
+                // "variable occurs only once"
+                continue;
+            }
+
+            const int occurences = entry.second;
+            if (occurences == 1 && varOccursMoreThanOnceInSomeBody.count(name) == 0) {
+                varOccursAtMostOnce.emplace(name);
+            } else {
+                // variable occurs more than once in some body => not a
+                // candidate for "variable occurs only once"
+                varOccursMoreThanOnceInSomeBody.emplace(name);
+                varOccursAtMostOnce.erase(name);
+            }
+        }
     }
 
-    // Check that a variables occurs more than once
-    for (const auto& cur : var_count) {
-        int numAppearances = cur.second;
-        const auto& varName = cur.first;
-        const auto& varLocation = var_pos[varName]->getSrcLoc();
-        if (varName[0] != '_' && numAppearances == 1) {
-            report.addWarning(
-                    WarnType::VarAppearsOnce, "Variable " + varName + " only occurs once", varLocation);
+    /// Find the least source location of a variable.
+    struct VarFinder : public Visitor<void> {
+        const std::string& name;
+        bool seen = false;
+        SrcLocation leastLoc = {};
+
+        explicit VarFinder(const std::string& varName) : name(varName) {}
+
+        void visit_(type_identity<ast::Variable>, const ast::Variable& var) override {
+            if (var.getName() == name) {
+                if (!seen) {
+                    leastLoc = var.getSrcLoc();
+                    seen = true;
+                } else if (var.getSrcLoc() < leastLoc) {
+                    leastLoc = var.getSrcLoc();
+                }
+            }
+        }
+    };
+
+    for (const auto& name : varOccursAtMostOnce) {
+        VarFinder vf(name);
+        // find the least source location of the variable to give a warning location
+        for (const Clause* cl : multiRule) {
+            for (auto lit : cl->getBodyLiterals()) {
+                visit(*lit, vf);
+            }
         }
+        report.addWarning(WarnType::VarAppearsOnce, "Variable " + name + " only occurs once", vf.leastLoc);
     }
 }
 

tests/semantic/fact_plus/fact_plus.err

@@ -1,7 +1,4 @@
 Error: Argument in fact is not constant in file fact_plus.dl at line 10
 F(1+a,"AA").
 --^----------
-Warning: Variable a only occurs once in file fact_plus.dl at line 10
-F(1+a,"AA").
-----^--------
 1 errors generated, evaluation aborted

tests/semantic/fact_variable/fact_variable.err

@@ -1,7 +1,4 @@
 Error: Argument in fact is not constant in file fact_variable.dl at line 7
 F(BB,"AA").
 --^---------
-Warning: Variable BB only occurs once in file fact_variable.dl at line 7
-F(BB,"AA").
---^---------
 1 errors generated, evaluation aborted

tests/semantic/rule_typecompat/rule_typecompat.err

@@ -54,9 +54,6 @@ The argument's declared type is R in file rule_typecompat.dl at line 12
 Error: Ungrounded variable y in file rule_typecompat.dl at line 30
 G(x,y) :- A(x).
 ----^-----------
-Warning: Variable y only occurs once in file rule_typecompat.dl at line 30
-G(x,y) :- A(x).
-----^-----------
 Error: Unable to deduce type for variable x in file rule_typecompat.dl at line 33
 A(x) :- B(x), C(x).
 --^-----------------
@@ -82,9 +79,6 @@ The argument's declared type is T in file rule_typecompat.dl at line 11
 Error: Ungrounded variable y in file rule_typecompat.dl at line 41
 F(x,y) :- F(x,z), G(z,x).
 ----^---------------------
-Warning: Variable y only occurs once in file rule_typecompat.dl at line 41
-F(x,y) :- F(x,z), G(z,x).
-----^---------------------
 Error: Unable to deduce type for variable v in file rule_typecompat.dl at line 47
 F(x,y) :- F(x,v), F(w,y), A(v), D(v).
 --------------^-----------------------
@@ -169,4 +163,4 @@ F(x,y) :- F(x,y), t < x.
 Warning: Variable t only occurs once in file rule_typecompat.dl at line 63
 F(x,y) :- F(x,y), t < x.
 ------------------^------
-18 errors generated, evaluation aborted
+18 errors generated, evaluation aborted

tests/semantic/var_single/var_single.err

@@ -1,9 +1,6 @@
 Error: Ungrounded variable X in file var_single.dl at line 8
 A(X) :- A(Y).
 --^-----------
-Warning: Variable X only occurs once in file var_single.dl at line 8
-A(X) :- A(Y).
---^-----------
 Warning: Variable Y only occurs once in file var_single.dl at line 8
 A(X) :- A(Y).
 ----------^---