From 0d75dc34b1752d629cd6192800cd80a09dab63b8 Mon Sep 17 00:00:00 2001 From: Adam Date: Mon, 16 Jan 2023 05:02:23 -0500 Subject: [PATCH] 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 | 2 +- src/CMakeLists.txt | 1 + src/MainDriver.cpp | 4 +- .../SimplifyConstantBinaryConstraints.cpp | 88 +++++++++++++++++++ .../SimplifyConstantBinaryConstraints.h | 40 +++++++++ 5 files changed, 133 insertions(+), 2 deletions(-) create mode 100644 src/ast/transform/SimplifyConstantBinaryConstraints.cpp create mode 100644 src/ast/transform/SimplifyConstantBinaryConstraints.h diff --git a/debian/souffle.bash-completion b/debian/souffle.bash-completion index a8491942b5b..5b6b2f029fe 100644 --- a/debian/souffle.bash-completion +++ b/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 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 680d9490cdd..15761d4a67a 100644 --- a/src/CMakeLists.txt +++ b/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 diff --git a/src/MainDriver.cpp b/src/MainDriver.cpp index 2741759a4b1..ae383c01688 100644 --- a/src/MainDriver.cpp +++ b/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 astTransformationPipeline(Global& glb) mk(), mk(), mk(), mk(), + mk(), + mk(), mk(), mk(), mk(), @@ -1145,4 +1148,3 @@ int main(Global& glb, const char* souffle_executable) { } } // end of namespace souffle - diff --git a/src/ast/transform/SimplifyConstantBinaryConstraints.cpp b/src/ast/transform/SimplifyConstantBinaryConstraints.cpp new file mode 100644 index 00000000000..bba91a5f5a4 --- /dev/null +++ b/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 + * - /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(lit)) { + if (isA(*bc->getLHS()) && isA(*bc->getRHS()) && + (bc->getBaseOperator() == BinaryConstraintOp::EQ || + bc->getBaseOperator() == BinaryConstraintOp::NE)) { + canSimplify = true; + break; + } + } + } + + if (!canSimplify) { + continue; + } + + auto replacementClause = Own(clause->cloneHead()); + for (Literal* lit : clause->getBodyLiterals()) { + bool replaced = false; + + if (auto* bc = as(lit)) { + auto* lhs = bc->getLHS(); + auto* rhs = bc->getRHS(); + Constant *lhsConst, *rhsConst; + if ((lhsConst = as(lhs)) && (rhsConst = as(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 diff --git a/src/ast/transform/SimplifyConstantBinaryConstraints.h b/src/ast/transform/SimplifyConstantBinaryConstraints.h new file mode 100644 index 00000000000..4b9785925ad --- /dev/null +++ b/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 + * - /licenses/SOUFFLE-UPL.txt + */ + +/************************************************************************ + * + * @file SimplifyConstantBinaryConstraints.h + * + ***********************************************************************/ + +#pragma once + +#include "ast/TranslationUnit.h" +#include "ast/transform/Transformer.h" +#include + +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