Lattice support (#2438)

introduce support of lattice types

src/CMakeLists.txt

@@ -34,6 +34,7 @@ set(SOUFFLE_SOURCES
     ast/FunctionalConstraint.cpp
     ast/IntrinsicFunctor.cpp
     ast/IterationCounter.cpp
+    ast/Lattice.cpp
     ast/Negation.cpp
     ast/NilConstant.cpp
     ast/Node.cpp
@@ -87,6 +88,7 @@ set(SOUFFLE_SOURCES
     ast/transform/GroundedTermsChecker.cpp
     ast/transform/GroundWitnesses.cpp
     ast/transform/InlineRelations.cpp
+    ast/transform/InsertLatticeOperations.cpp
     ast/transform/MagicSet.cpp
     ast/transform/MaterializeAggregationQueries.cpp
     ast/transform/MaterializeSingletonAggregation.cpp

src/MainDriver.cpp

@@ -37,6 +37,7 @@
 #include "ast/transform/IOAttributes.h"
 #include "ast/transform/IODefaults.h"
 #include "ast/transform/InlineRelations.h"
+#include "ast/transform/InsertLatticeOperations.h"
 #include "ast/transform/MagicSet.h"
 #include "ast/transform/MaterializeAggregationQueries.h"
 #include "ast/transform/MaterializeSingletonAggregation.h"
@@ -479,6 +480,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::LatticeTransformer>(),
             mk<ast::transform::DebugDeltaRelationTransformer>(),
             mk<ast::transform::IODefaultsTransformer>(),
             mk<ast::transform::SimplifyAggregateTargetExpressionTransformer>(),

src/RelationTag.h

@@ -58,7 +58,6 @@ enum class RelationRepresentation {
     BTREE,         // use btree data-structure
     BTREE_DELETE,  // use btree_delete data-structure
     EQREL,         // use union data-structure
-    PROVENANCE,    // use custom btree data-structure with provenance extras
     INFO,          // info relation for provenance
 };
 
@@ -168,7 +167,6 @@ inline std::ostream& operator<<(std::ostream& os, RelationRepresentation represe
         case RelationRepresentation::BTREE_DELETE: return os << "btree_delete";
         case RelationRepresentation::BRIE: return os << "brie";
         case RelationRepresentation::EQREL: return os << "eqrel";
-        case RelationRepresentation::PROVENANCE: return os << "provenance";
         case RelationRepresentation::INFO: return os << "info";
         case RelationRepresentation::DEFAULT: return os;
     }

src/ast/Attribute.cpp

@@ -14,23 +14,29 @@
 namespace souffle::ast {
 
 Attribute::Attribute(std::string n, QualifiedName t, SrcLocation loc)
-        : Node(std::move(loc)), name(std::move(n)), typeName(std::move(t)) {}
+        : Node(std::move(loc)), name(std::move(n)), typeName(std::move(t)), isLattice(false) {}
+
+Attribute::Attribute(std::string n, QualifiedName t, bool isLattice, SrcLocation loc)
+        : Node(std::move(loc)), name(std::move(n)), typeName(std::move(t)), isLattice(isLattice) {}
 
 void Attribute::setTypeName(QualifiedName name) {
     typeName = std::move(name);
 }
 
 void Attribute::print(std::ostream& os) const {
     os << name << ":" << typeName;
+    if (isLattice) {
+        os << "<>";
+    }
 }
 
 bool Attribute::equal(const Node& node) const {
     const auto& other = asAssert<Attribute>(node);
-    return name == other.name && typeName == other.typeName;
+    return name == other.name && typeName == other.typeName && isLattice == other.isLattice;
 }
 
 Attribute* Attribute::cloning() const {
-    return new Attribute(name, typeName, getSrcLoc());
+    return new Attribute(name, typeName, isLattice, getSrcLoc());
 }
 
 }  // namespace souffle::ast

src/ast/Attribute.h

@@ -35,6 +35,7 @@ namespace souffle::ast {
 class Attribute : public Node {
 public:
     Attribute(std::string n, QualifiedName t, SrcLocation loc = {});
+    Attribute(std::string n, QualifiedName t, bool isLattice, SrcLocation loc = {});
 
     /** Return attribute name */
     const std::string& getName() const {
@@ -49,6 +50,10 @@ class Attribute : public Node {
     /** Set type name */
     void setTypeName(QualifiedName name);
 
+    bool getIsLattice() const {
+        return isLattice;
+    }
+
 protected:
     void print(std::ostream& os) const override;
 
@@ -63,6 +68,9 @@ class Attribute : public Node {
 
     /** Type name */
     QualifiedName typeName;
+
+    /** Is lattice element */
+    bool isLattice;
 };
 
 }  // namespace souffle::ast

src/ast/Component.cpp

@@ -39,6 +39,15 @@ std::vector<Type*> Component::getTypes() const {
     return toPtrVector(types);
 }
 
+void Component::addLattice(Own<Lattice> t) {
+    assert(t != nullptr);
+    lattices.push_back(std::move(t));
+}
+
+std::vector<Lattice*> Component::getLattices() const {
+    return toPtrVector(lattices);
+}
+
 void Component::copyBaseComponents(const Component& other) {
     baseComponents = clone(other.baseComponents);
 }

src/ast/Component.h

@@ -20,6 +20,7 @@
 #include "ast/ComponentInit.h"
 #include "ast/ComponentType.h"
 #include "ast/Directive.h"
+#include "ast/Lattice.h"
 #include "ast/Node.h"
 #include "ast/Relation.h"
 #include "ast/Type.h"
@@ -64,6 +65,11 @@ class Component : public Node {
     /** Get types */
     std::vector<Type*> getTypes() const;
 
+    /** Add lattice */
+    void addLattice(Own<Lattice> lat);
+
+    std::vector<Lattice*> getLattices() const;
+
     /** Copy base components */
     void copyBaseComponents(const Component& other);
 
@@ -129,6 +135,9 @@ class Component : public Node {
     /** Types declarations */
     VecOwn<Type> types;
 
+    /** Types declarations */
+    VecOwn<Lattice> lattices;
+
     /** Relations */
     VecOwn<Relation> relations;
 

src/ast/Lattice.cpp

@@ -0,0 +1,107 @@
+/*
+ * 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/Lattice.h"
+#include "souffle/utility/MiscUtil.h"
+#include "souffle/utility/StreamUtil.h"
+
+#include <utility>
+
+namespace souffle::ast {
+
+std::optional<LatticeOperator> latticeOperatorFromString(const std::string& str) {
+    if (str == "Bottom") return Bottom;
+    if (str == "Top") return Top;
+    if (str == "Lub") return Lub;
+    if (str == "Glb") return Glb;
+    if (str == "Leq") return Leq;
+    return std::nullopt;
+}
+
+std::string latticeOperatorToString(const LatticeOperator op) {
+    switch (op) {
+        case Bottom: return "Bottom";
+        case Top: return "Top";
+        case Lub: return "Lub";
+        case Glb: return "Glb";
+        case Leq: return "Leq";
+        default: assert(false && "unknown lattice operator");
+    }
+    return "";
+}
+
+Lattice::Lattice(QualifiedName name, std::map<LatticeOperator, Own<ast::Argument>> ops, SrcLocation loc)
+        : Node(std::move(loc)), name(std::move(name)), operators(std::move(ops)) {}
+
+void Lattice::setQualifiedName(QualifiedName name) {
+    this->name = std::move(name);
+}
+
+const std::map<LatticeOperator, const ast::Argument*> Lattice::getOperators() const {
+    std::map<LatticeOperator, const ast::Argument*> ops;
+    for (const auto& [op, arg] : operators) {
+        ops.emplace(std::make_pair(op, arg.get()));
+    }
+    return ops;
+}
+
+bool Lattice::hasGlb() const {
+    return operators.count(Glb) > 0;
+}
+
+bool Lattice::hasLub() const {
+    return operators.count(Lub) > 0;
+}
+
+bool Lattice::hasBottom() const {
+    return operators.count(Bottom) > 0;
+}
+
+bool Lattice::hasTop() const {
+    return operators.count(Top) > 0;
+}
+
+const ast::Argument* Lattice::getLub() const {
+    return operators.at(Lub).get();
+}
+
+const ast::Argument* Lattice::getGlb() const {
+    return operators.at(Glb).get();
+}
+
+const ast::Argument* Lattice::getBottom() const {
+    return operators.at(Bottom).get();
+}
+
+const ast::Argument* Lattice::getTop() const {
+    return operators.at(Top).get();
+}
+
+void Lattice::print(std::ostream& os) const {
+    os << ".lattice " << getQualifiedName() << " {\n   ";
+    bool first = true;
+    for (const auto& [op, arg] : operators) {
+        if (!first) {
+            os << ",\n   ";
+        }
+        os << latticeOperatorToString(op) << " -> " << *arg;
+        first = false;
+    }
+    os << "\n}";
+}
+
+bool Lattice::equal(const Node& node) const {
+    const auto& other = asAssert<Lattice>(node);
+    return getQualifiedName() == other.getQualifiedName() && equal_targets(operators, other.operators);
+}
+
+Lattice* Lattice::cloning() const {
+    return new Lattice(getQualifiedName(), clone(operators), getSrcLoc());
+}
+
+}  // namespace souffle::ast

src/ast/Lattice.h

@@ -0,0 +1,77 @@
+/*
+ * 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 Lattice.h
+ *
+ * Defines the Lattice class
+ *
+ ***********************************************************************/
+
+#pragma once
+
+#include "ast/Argument.h"
+#include "ast/Node.h"
+#include "ast/QualifiedName.h"
+#include "parser/SrcLocation.h"
+
+#include <map>
+#include <optional>
+
+namespace souffle::ast {
+
+enum LatticeOperator { Bottom = 0, Top, Lub, Glb, Leq };
+
+std::optional<LatticeOperator> latticeOperatorFromString(const std::string& str);
+
+/**
+ *  @class Lattice
+ *  @brief An class to define Lattice attributes for a type
+ */
+class Lattice : public Node {
+public:
+    Lattice(QualifiedName name, std::map<LatticeOperator, Own<ast::Argument>> operators,
+            SrcLocation loc = {});
+
+    /** Return type name */
+    const QualifiedName& getQualifiedName() const {
+        return name;
+    }
+
+    /** Set type name */
+    void setQualifiedName(QualifiedName name);
+
+    const std::map<LatticeOperator, const ast::Argument*> getOperators() const;
+
+    bool hasGlb() const;
+    bool hasLub() const;
+    bool hasBottom() const;
+    bool hasTop() const;
+
+    const ast::Argument* getLub() const;
+    const ast::Argument* getGlb() const;
+    const ast::Argument* getBottom() const;
+    const ast::Argument* getTop() const;
+
+protected:
+    void print(std::ostream& os) const override;
+
+private:
+    bool equal(const Node& node) const override;
+
+    Lattice* cloning() const override;
+
+private:
+    /** type name */
+    QualifiedName name;
+
+    const std::map<LatticeOperator, Own<ast::Argument>> operators;
+};
+
+}  // namespace souffle::ast