Drop clause if it contains an impossible BinaryConstraint (#2376)

* Drop clause if impossible BinaryConstraint

Some BinaryConstraint atoms can be determined to be impossible during
synthesis. Introduce a transform to eliminate clauses containing such
impossible atoms.

These kinds of atoms are not likely to be written directly, but can
easily arise with inlined code.

* Rewrite as SimplifyBinaryConstraintsTransform

debian/souffle.bash-completion

@@ -35,7 +35,7 @@ _souffle()
             return
             ;;
         --disable-transformers)
-            COMPREPLY=( $(compgen -W "AstComponentChecker AstExecutionPlanChecker AstPragmaChecker AstSemanticChecker AstUserDefinedFunctorsTransformer ComponentInstantiationTransformer FoldAnonymousRecords GroundedTermsChecker InlineRelationsTransformer MagicSetTransformer MaterializeAggregationQueriesTransformer MaterializeSingletonAggregationTransformer MetaTransformer MinimiseProgramTransformer NameUnnamedVariablesTransformer NormaliseConstraintsTransformer PartitionBodyLiteralsTransformer PolymorphicObjectsTransformer ProvenanceTransformer ReduceExistentialsTransformer RemoveBooleanConstraintsTransformer RemoveEmptyRelationsTransformer RemoveRedundantRelationsTransformer RemoveRedundantSumsTransformer RemoveRelationCopiesTransformer RemoveTypecastsTransformer ReorderLiteralsTransformer ReplaceSingletonVariablesTransformer ResolveAliasesTransformer ResolveAnonymousRecordAliases UniqueAggregationVariablesTransformer" -- "$cur" ) )
+            COMPREPLY=( $(compgen -W "AstComponentChecker AstExecutionPlanChecker AstPragmaChecker AstSemanticChecker AstUserDefinedFunctorsTransformer ComponentInstantiationTransformer FoldAnonymousRecords GroundedTermsChecker InlineRelationsTransformer MagicSetTransformer MaterializeAggregationQueriesTransformer MaterializeSingletonAggregationTransformer MetaTransformer MinimiseProgramTransformer NameUnnamedVariablesTransformer NormaliseConstraintsTransformer PartitionBodyLiteralsTransformer PolymorphicObjectsTransformer ProvenanceTransformer ReduceExistentialsTransformer RemoveBooleanConstraintsTransformer RemoveEmptyRelationsTransformer RemoveRedundantRelationsTransformer RemoveRedundantSumsTransformer RemoveRelationCopiesTransformer RemoveTypecastsTransformer ReorderLiteralsTransformer ReplaceSingletonVariablesTransformer ResolveAliasesTransformer ResolveAnonymousRecordAliases SimplifyConstantBinaryConstraintsTransformer UniqueAggregationVariablesTransformer" -- "$cur" ) )
             return
             ;;
     esac

src/CMakeLists.txt

@@ -104,6 +104,7 @@ set(SOUFFLE_SOURCES
     ast/transform/ResolveAliases.cpp
     ast/transform/ResolveAnonymousRecordAliases.cpp
     ast/transform/SemanticChecker.cpp
+    ast/transform/SimplifyConstantBinaryConstraints.cpp
     ast/transform/SubsumptionQualifier.cpp
     ast/transform/SimplifyAggregateTargetExpression.cpp
     ast/transform/Transformer.cpp

src/MainDriver.cpp

@@ -56,6 +56,7 @@
 #include "ast/transform/ResolveAnonymousRecordAliases.h"
 #include "ast/transform/SemanticChecker.h"
 #include "ast/transform/SimplifyAggregateTargetExpression.h"
+#include "ast/transform/SimplifyConstantBinaryConstraints.h"
 #include "ast/transform/SubsumptionQualifier.h"
 #include "ast/transform/UniqueAggregationVariables.h"
 #include "ast2ram/TranslationStrategy.h"
@@ -472,6 +473,8 @@ Own<ast::transform::PipelineTransformer> astTransformationPipeline(Global& glb)
             mk<ast::transform::InlineUnmarkExcludedTransform>(),
             mk<ast::transform::InlineRelationsTransformer>(), mk<ast::transform::GroundedTermsChecker>(),
             mk<ast::transform::ResolveAliasesTransformer>(),
+            mk<ast::transform::SimplifyConstantBinaryConstraintsTransformer>(),
+            mk<ast::transform::RemoveBooleanConstraintsTransformer>(),
             mk<ast::transform::RemoveRedundantRelationsTransformer>(),
             mk<ast::transform::RemoveRelationCopiesTransformer>(),
             mk<ast::transform::RemoveEmptyRelationsTransformer>(),
@@ -1145,4 +1148,3 @@ int main(Global& glb, const char* souffle_executable) {
 }
 
 }  // end of namespace souffle
-

src/ast/transform/SimplifyConstantBinaryConstraints.cpp

@@ -0,0 +1,88 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2018, 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 SimplifyConstantBinaryConstraints.cpp
+ *
+ ***********************************************************************/
+
+#include "ast/transform/SimplifyConstantBinaryConstraints.h"
+#include "ast/BinaryConstraint.h"
+#include "ast/BooleanConstraint.h"
+#include "ast/Clause.h"
+#include "ast/Constant.h"
+#include "ast/Literal.h"
+#include "ast/Program.h"
+#include "ast/Relation.h"
+#include "ast/TranslationUnit.h"
+#include "souffle/BinaryConstraintOps.h"
+
+namespace souffle::ast::transform {
+
+bool SimplifyConstantBinaryConstraintsTransformer::transform(TranslationUnit& translationUnit) {
+    Program& program = translationUnit.getProgram();
+    bool changed = false;
+
+    for (Relation* rel : program.getRelations()) {
+        for (auto&& clause : program.getClauses(*rel)) {
+            bool canSimplify = false;
+
+            for (Literal* lit : clause->getBodyLiterals()) {
+                if (auto* bc = as<BinaryConstraint>(lit)) {
+                    if (isA<Constant>(*bc->getLHS()) && isA<Constant>(*bc->getRHS()) &&
+                            (bc->getBaseOperator() == BinaryConstraintOp::EQ ||
+                                    bc->getBaseOperator() == BinaryConstraintOp::NE)) {
+                        canSimplify = true;
+                        break;
+                    }
+                }
+            }
+
+            if (!canSimplify) {
+                continue;
+            }
+
+            auto replacementClause = Own<Clause>(clause->cloneHead());
+            for (Literal* lit : clause->getBodyLiterals()) {
+                bool replaced = false;
+
+                if (auto* bc = as<BinaryConstraint>(lit)) {
+                    auto* lhs = bc->getLHS();
+                    auto* rhs = bc->getRHS();
+                    Constant *lhsConst, *rhsConst;
+                    if ((lhsConst = as<Constant>(lhs)) && (rhsConst = as<Constant>(rhs))) {
+                        bool constsEq = *lhsConst == *rhsConst;
+                        if (bc->getBaseOperator() == BinaryConstraintOp::EQ ||
+                                bc->getBaseOperator() == BinaryConstraintOp::NE) {
+                            bool literalBool = constsEq;
+                            if (bc->getBaseOperator() == BinaryConstraintOp::NE) {
+                                literalBool = !constsEq;
+                            }
+                            BooleanConstraint replacementLiteral(literalBool);
+                            replacementClause->addToBody(clone(replacementLiteral));
+                            replaced = true;
+                        }
+                    }
+                }
+
+                if (!replaced) {
+                    replacementClause->addToBody(clone(lit));
+                }
+            }
+
+            program.removeClause(*clause);
+            program.addClause(std::move(replacementClause));
+            changed = true;
+        }
+    }
+
+    return changed;
+}
+
+}  // namespace souffle::ast::transform

src/ast/transform/SimplifyConstantBinaryConstraints.h

@@ -0,0 +1,40 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2018, 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 SimplifyConstantBinaryConstraints.h
+ *
+ ***********************************************************************/
+
+#pragma once
+
+#include "ast/TranslationUnit.h"
+#include "ast/transform/Transformer.h"
+#include <string>
+
+namespace souffle::ast::transform {
+
+/**
+ * Rewrites constant binary constraints into boolean constraints
+ */
+class SimplifyConstantBinaryConstraintsTransformer : public Transformer {
+public:
+    std::string getName() const override {
+        return "SimplifyConstantBinaryConstraintsTransformer";
+    }
+
+private:
+    SimplifyConstantBinaryConstraintsTransformer* cloning() const override {
+        return new SimplifyConstantBinaryConstraintsTransformer();
+    }
+
+    bool transform(TranslationUnit& translationUnit) override;
+};
+
+}  // namespace souffle::ast::transform