Provide way to debug delta relations and expose iteration counter

src/CMakeLists.txt

@@ -33,6 +33,7 @@ set(SOUFFLE_SOURCES
     ast/FunctorDeclaration.cpp
     ast/FunctionalConstraint.cpp
     ast/IntrinsicFunctor.cpp
+    ast/IterationCounter.cpp
     ast/Negation.cpp
     ast/NilConstant.cpp
     ast/Node.cpp
@@ -79,6 +80,7 @@ set(SOUFFLE_SOURCES
     ast/transform/ComponentChecker.cpp
     ast/transform/ComponentInstantiation.cpp
     ast/transform/DebugReporter.cpp
+    ast/transform/DebugDeltaRelation.cpp
     ast/transform/ExecutionPlanChecker.cpp
     ast/transform/ExpandEqrels.cpp
     ast/transform/FoldAnonymousRecords.cpp

src/MainDriver.cpp

@@ -27,6 +27,7 @@
 #include "ast/transform/ComponentChecker.h"
 #include "ast/transform/ComponentInstantiation.h"
 #include "ast/transform/Conditional.h"
+#include "ast/transform/DebugDeltaRelation.h"
 #include "ast/transform/ExecutionPlanChecker.h"
 #include "ast/transform/ExpandEqrels.h"
 #include "ast/transform/Fixpoint.h"
@@ -478,6 +479,7 @@ Own<ast::transform::PipelineTransformer> astTransformationPipeline(Global& glb)
     // Main pipeline
     auto pipeline = mk<ast::transform::PipelineTransformer>(mk<ast::transform::ComponentChecker>(),
             mk<ast::transform::ComponentInstantiationTransformer>(),
+            mk<ast::transform::DebugDeltaRelationTransformer>(),
             mk<ast::transform::IODefaultsTransformer>(),
             mk<ast::transform::SimplifyAggregateTargetExpressionTransformer>(),
             mk<ast::transform::UniqueAggregationVariablesTransformer>(),

src/ast/IterationCounter.cpp

@@ -0,0 +1,22 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2023, The Souffle Developers. All rights reserved
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+#include "ast/IterationCounter.h"
+#include <ostream>
+
+namespace souffle::ast {
+
+void IterationCounter::print(std::ostream& os) const {
+    os << "recursive_iteration_cnt()";
+}
+
+IterationCounter* IterationCounter::cloning() const {
+    return new IterationCounter(getSrcLoc());
+}
+
+}  // namespace souffle::ast

src/ast/IterationCounter.h

@@ -0,0 +1,39 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2023, The Souffle Developers. All rights reserved
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+/************************************************************************
+ *
+ * @file IterationCounter.h
+ *
+ * Defines a counter functor class
+ *
+ ***********************************************************************/
+
+#pragma once
+
+#include "ast/Argument.h"
+#include <iosfwd>
+
+namespace souffle::ast {
+
+/**
+ * @class IterationCounter
+ * @brief iteration counter for recursive strata
+ */
+class IterationCounter : public Argument {
+public:
+    using Argument::Argument;
+
+protected:
+    void print(std::ostream& os) const override;
+
+private:
+    IterationCounter* cloning() const override;
+};
+
+}  // namespace souffle::ast

src/ast/Relation.cpp

@@ -61,14 +61,17 @@ void Relation::print(std::ostream& os) const {
     if (!functionalDependencies.empty()) {
         os << " choice-domain " << join(functionalDependencies, ", ");
     }
+    if (isDeltaDebug) {
+        os << " delta_debug(" << isDeltaDebug.value() << ")";
+    }
 }
 
 bool Relation::equal(const Node& node) const {
     const auto& other = asAssert<Relation>(node);
     return name == other.name && equal_targets(attributes, other.attributes) &&
            qualifiers == other.qualifiers &&
            equal_targets(functionalDependencies, other.functionalDependencies) &&
-           representation == other.representation;
+           representation == other.representation && isDeltaDebug == other.isDeltaDebug;
 }
 
 Relation* Relation::cloning() const {
@@ -77,6 +80,7 @@ Relation* Relation::cloning() const {
     res->qualifiers = qualifiers;
     res->functionalDependencies = clone(functionalDependencies);
     res->representation = representation;
+    res->isDeltaDebug = isDeltaDebug;
     return res;
 }
 

src/ast/Relation.h

@@ -97,6 +97,14 @@ class Relation : public Node {
 
     void apply(const NodeMapper& map) override;
 
+    void setIsDeltaDebug(QualifiedName rel) {
+        isDeltaDebug = rel;
+    }
+
+    std::optional<QualifiedName> getIsDeltaDebug() const {
+        return isDeltaDebug;
+    }
+
 protected:
     void print(std::ostream& os) const override;
 
@@ -122,6 +130,8 @@ class Relation : public Node {
 
     /** Datastructure to use for this relation */
     RelationRepresentation representation{RelationRepresentation::DEFAULT};
+
+    std::optional<QualifiedName> isDeltaDebug;
 };
 
 /**

src/ast/analysis/PrecedenceGraph.cpp

@@ -48,6 +48,13 @@ void PrecedenceGraphAnalysis::run(const TranslationUnit& translationUnit) {
                 souffle::visit(literals[i], addEdgeToR);
             }
         }
+
+        // delta_debug relation are computed from the original relation
+        if (const auto deltaDebug = r->getIsDeltaDebug()) {
+            const auto* dbg = program.getRelation(deltaDebug.value());
+            backingGraph.insert(r, dbg);
+            backingGraph.insert(dbg, r);
+        }
     }
 }
 

src/ast/analysis/typesystem/Type.cpp

@@ -582,6 +582,8 @@ void TypeAnnotationPrinter::branchOnArgument(const Argument* cur, const Type& ty
         print_(type_identity<UserDefinedFunctor>(), *as<UserDefinedFunctor>(cur));
     } else if (isA<Counter>(*cur)) {
         print_(type_identity<Counter>(), *as<Counter>(cur));
+    } else if (isA<IterationCounter>(*cur)) {
+        print_(type_identity<IterationCounter>(), *as<IterationCounter>(cur));
     } else if (isA<Aggregator>(*cur)) {
         print_(type_identity<Aggregator>(), *as<Aggregator>(cur));
     } else {
@@ -719,6 +721,11 @@ void TypeAnnotationPrinter::print_(type_identity<Counter>, [[maybe_unused]] cons
     os << "$∈{number}";
 }
 
+void TypeAnnotationPrinter::print_(
+        type_identity<IterationCounter>, [[maybe_unused]] const IterationCounter& counter) {
+    os << "$∈{unsigned}";
+}
+
 void TypeAnnotationPrinter::print_(type_identity<TypeCast>, const ast::TypeCast& typeCast) {
     os << "as(";
     auto& ty = typeEnv.getType(typeCast.getType());

src/ast/analysis/typesystem/Type.h

@@ -43,6 +43,7 @@ class Clause;
 class Functor;
 class FunctorDeclaration;
 class IntrinsicFunctor;
+class IterationCounter;
 class NumericConstant;
 class Type;
 class UserDefinedFunctor;
@@ -189,6 +190,7 @@ class TypeAnnotationPrinter {
     void print_(type_identity<IntrinsicFunctor>, const IntrinsicFunctor& fun);
     void print_(type_identity<UserDefinedFunctor>, const UserDefinedFunctor& fun);
     void print_(type_identity<Counter>, const Counter& counter);
+    void print_(type_identity<IterationCounter>, const IterationCounter& counter);
     void print_(type_identity<TypeCast>, const ast::TypeCast& typeCast);
     void print_(type_identity<RecordInit>, const RecordInit& record, const RecordType&);
     void print_(type_identity<BranchInit>, const BranchInit& adt);

src/ast/analysis/typesystem/TypeConstrainsAnalysis.cpp

@@ -174,6 +174,10 @@ void TypeConstraintsAnalysis::visit_(type_identity<Counter>, const Counter& coun
     addConstraint(isSubtypeOf(getVar(counter), typeEnv.getConstantType(TypeAttribute::Signed)));
 }
 
+void TypeConstraintsAnalysis::visit_(type_identity<IterationCounter>, const IterationCounter& counter) {
+    addConstraint(isSubtypeOf(getVar(counter), typeEnv.getConstantType(TypeAttribute::Unsigned)));
+}
+
 void TypeConstraintsAnalysis::visit_(type_identity<TypeCast>, const ast::TypeCast& typeCast) {
     auto& typeName = typeCast.getType();
     if (!typeEnv.isType(typeName)) {

src/ast/analysis/typesystem/TypeConstrainsAnalysis.h

@@ -60,6 +60,7 @@ class TypeConstraintsAnalysis : public ConstraintAnalysis<TypeVar> {
     void visit_(type_identity<IntrinsicFunctor>, const IntrinsicFunctor& fun) override;
     void visit_(type_identity<UserDefinedFunctor>, const UserDefinedFunctor& fun) override;
     void visit_(type_identity<Counter>, const Counter& counter) override;
+    void visit_(type_identity<IterationCounter>, const IterationCounter& counter) override;
     void visit_(type_identity<TypeCast>, const ast::TypeCast& typeCast) override;
     void visit_(type_identity<RecordInit>, const RecordInit& record) override;
     void visit_(type_identity<BranchInit>, const BranchInit& adt) override;

src/ast/transform/ComponentInstantiation.cpp

@@ -415,6 +415,15 @@ ComponentContent getInstantiatedContent(Program& program, const ComponentInit& c
             }
         });
 
+        visit(node, [&](Relation& rel) {
+            if (rel.getIsDeltaDebug()) {
+                auto pos = relationNameMapping.find(rel.getIsDeltaDebug().value());
+                if (pos != relationNameMapping.end()) {
+                    rel.setIsDeltaDebug(pos->second);
+                }
+            }
+        });
+
         // rename directives
         visit(node, [&](Directive& directive) {
             auto pos = relationNameMapping.find(directive.getQualifiedName());

src/ast/transform/DebugDeltaRelation.cpp

@@ -0,0 +1,58 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2023, The Souffle Developers. All rights reserved
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+/************************************************************************
+ *
+ * @file DebugDeltaRelation.cpp
+ *
+ ***********************************************************************/
+
+#include "ast/transform/DebugDeltaRelation.h"
+#include "ast/Argument.h"
+#include "ast/Atom.h"
+#include "ast/Clause.h"
+#include "ast/Program.h"
+#include "ast/QualifiedName.h"
+#include "ast/RecordInit.h"
+#include "ast/Relation.h"
+#include "ast/TranslationUnit.h"
+#include "ast/Variable.h"
+#include "ast/analysis/IOType.h"
+#include "ast/utility/Utils.h"
+#include "ast/utility/Visitor.h"
+#include "souffle/utility/ContainerUtil.h"
+#include <algorithm>
+#include <cassert>
+#include <map>
+#include <set>
+#include <utility>
+#include <vector>
+
+namespace souffle::ast::transform {
+
+bool DebugDeltaRelationTransformer::updateSignature(TranslationUnit& translationUnit) {
+    bool changed = false;
+    Program& program = translationUnit.getProgram();
+
+    for (Relation* rel : program.getRelations()) {
+        if (!rel->getIsDeltaDebug().has_value()) {
+            continue;
+        }
+        const QualifiedName originalRelName = rel->getIsDeltaDebug().value();
+        Relation* orig = program.getRelation(originalRelName);
+        assert(orig != nullptr);
+
+
+        rel->setAttributes(clone(orig->getAttributes()));
+        changed = true;
+        rel->addAttribute(mk<Attribute>("<iteration>", "unsigned"));
+    }
+    return changed;
+}
+
+}  // namespace souffle::ast::transform

src/ast/transform/DebugDeltaRelation.h

@@ -0,0 +1,44 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2023, The Souffle Developers. All rights reserved
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+/************************************************************************
+ *
+ * @file DebugDeltaRelation.h
+ *
+ ***********************************************************************/
+
+#pragma once
+
+#include "ast/TranslationUnit.h"
+#include "ast/transform/Transformer.h"
+#include <string>
+
+namespace souffle::ast::transform {
+
+/**
+ * Pass that assign the correct signature to relations declared as delta_debug
+ */
+class DebugDeltaRelationTransformer : public Transformer {
+public:
+    std::string getName() const override {
+        return "DebugDeltaRelationTransformer";
+    }
+
+private:
+    DebugDeltaRelationTransformer* cloning() const override {
+        return new DebugDeltaRelationTransformer();
+    }
+
+    bool updateSignature(TranslationUnit& translationUnit);
+
+    bool transform(TranslationUnit& translationUnit) override {
+        return updateSignature(translationUnit);
+    }
+};
+
+}  // namespace souffle::ast::transform

src/ast/transform/SemanticChecker.cpp

@@ -37,6 +37,7 @@
 #include "ast/Functor.h"
 #include "ast/IntrinsicAggregator.h"
 #include "ast/IntrinsicFunctor.h"
+#include "ast/IterationCounter.h"
 #include "ast/Literal.h"
 #include "ast/Negation.h"
 #include "ast/NilConstant.h"
@@ -414,6 +415,8 @@ bool isConstantArgument(const Argument* arg) {
         // if all argument of functor are constant, then
         // assume functor returned value is constant.
         return all_of(udf->getArguments(), isConstantArgument);
+    } else if (isA<IterationCounter>(arg)) {
+        return false;
     } else if (isA<Counter>(arg)) {
         return false;
     } else if (auto* typeCast = as<ast::TypeCast>(arg)) {
@@ -668,11 +671,21 @@ void SemanticCheckerImpl::checkRelation(const Relation& relation) {
 
     // check whether this relation is empty
     if (program.getClauses(relation).empty() && !ioTypes.isInput(&relation) &&
+            !relation.getIsDeltaDebug().has_value() &&
             !relation.hasQualifier(RelationQualifier::SUPPRESSED)) {
         report.addWarning(WarnType::NoRulesNorFacts,
                 "No rules/facts defined for relation " + toString(relation.getQualifiedName()),
                 relation.getSrcLoc());
     }
+
+    // if the relation is a delta_debug, make sure if has no clause
+    if (relation.getIsDeltaDebug().has_value()) {
+        if (!program.getClauses(relation).empty() || ioTypes.isInput(&relation)) {
+            report.addError("Unexpected rules/facts for delta_debug relation " +
+                                    toString(relation.getQualifiedName()),
+                    relation.getSrcLoc());
+        }
+    }
 }
 
 void SemanticCheckerImpl::checkIO() {

src/ast/utility/Visitor.h

@@ -38,6 +38,7 @@
 #include "ast/FunctorDeclaration.h"
 #include "ast/IntrinsicAggregator.h"
 #include "ast/IntrinsicFunctor.h"
+#include "ast/IterationCounter.h"
 #include "ast/Literal.h"
 #include "ast/Negation.h"
 #include "ast/NilConstant.h"
@@ -88,6 +89,7 @@ struct Visitor : souffle::detail::VisitorBase<R, NodeType, Params...> {
         SOUFFLE_VISITOR_FORWARD(Variable)
         SOUFFLE_VISITOR_FORWARD(UnnamedVariable)
         SOUFFLE_VISITOR_FORWARD(IntrinsicFunctor)
+        SOUFFLE_VISITOR_FORWARD(IterationCounter)
         SOUFFLE_VISITOR_FORWARD(UserDefinedFunctor)
         SOUFFLE_VISITOR_FORWARD(Counter)
         SOUFFLE_VISITOR_FORWARD(NumericConstant)
@@ -137,6 +139,7 @@ struct Visitor : souffle::detail::VisitorBase<R, NodeType, Params...> {
     SOUFFLE_VISITOR_LINK(Variable, Argument)
     SOUFFLE_VISITOR_LINK(UnnamedVariable, Argument)
     SOUFFLE_VISITOR_LINK(Counter, Argument)
+    SOUFFLE_VISITOR_LINK(IterationCounter, Argument)
     SOUFFLE_VISITOR_LINK(TypeCast, Argument)
     SOUFFLE_VISITOR_LINK(BranchInit, Argument)