Keep duplicate clauses for btree_sum

souffle-lang · May 11, 2022 · 917a36f · 917a36f
1 parent 2fe0709
commit 917a36f
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 7 deletions.
diff --git a/src/ast/transform/MinimiseProgram.cpp b/src/ast/transform/MinimiseProgram.cpp
@@ -267,6 +267,12 @@ bool MinimiseProgramTransformer::reduceLocallyEquivalentClauses(TranslationUnit&
         for (auto&& cl : program.getClauses(*rel)) {
             auto* clause = &*cl;
             bool added = false;
+            const auto* head = clause->getHead();
+            const auto* relation = program.getRelation(*head);
+            // keep duplicate clauses for btree_sum
+            if (relation->getRepresentation() == RelationRepresentation::BTREE_SUM) {
+                continue;
+            }
 
             for (std::vector<Clause*>& eqClass : equivalenceClasses) {
                 const auto& normedRep = normalisations.getNormalisation(eqClass[0]);
@@ -353,6 +359,10 @@ bool MinimiseProgramTransformer::removeRedundantClauses(TranslationUnit& transla
             return false;
         }
         const auto* head = clause->getHead();
+        const auto* relation = program.getRelation(*head);
+        if (relation->getRepresentation() == RelationRepresentation::BTREE_SUM) {
+            return false;
+        }
         for (const auto* lit : clause->getBodyLiterals()) {
             if (*head == *lit) {
                 return true;

diff --git a/src/synthesiser/Relation.cpp b/src/synthesiser/Relation.cpp
@@ -317,17 +317,16 @@ void DirectRelation::generateTypeStruct(std::ostream& out) {
                 std::size_t attrib = ind[i];
                 const auto& typecast = typecasts[attrib];
                 std::string lt;
-                if (i + 1 == bound && isAggregate) {
-                    if (aggregateOp == "max") {
+                if (i + 1 == bound && isAggregate && aggregateOp == "max") {
                         lt = ">";
-                    } else if (aggregateOp == "sum") {
-                        lt = "!=";
-                    }
                 } else {
                     lt = "<";
                 }
-
-                out << "(" << typecast << "(a[" << attrib << "])" << lt << typecast << "(b[" << attrib << "]))";
+                if (i + 1 == bound && aggregateOp == "sum") {
+                    out << "true";
+                } else {
+                    out << "(" << typecast << "(a[" << attrib << "])" << lt << typecast << "(b[" << attrib << "]))";
+                }
                 if (i + 1 < bound) {
                     out << "|| ((" << typecast << "(a[" << attrib << "]) == " << typecast << "(b[" << attrib
                         << "])) && (";