From 165f6ac0596b57148a16343231d5d62e8ac104c9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 19 Apr 2018 15:08:50 +0200 Subject: [PATCH] Implement basic integer variable detection MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers. --- include/anthem/IntegerVariableDetection.h | 22 ++ src/anthem/IntegerVariableDetection.cpp | 419 ++++++++++++++++++++++ src/anthem/Translation.cpp | 4 + 3 files changed, 445 insertions(+) create mode 100644 include/anthem/IntegerVariableDetection.h create mode 100644 src/anthem/IntegerVariableDetection.cpp diff --git a/include/anthem/IntegerVariableDetection.h b/include/anthem/IntegerVariableDetection.h new file mode 100644 index 0000000..c6afd77 --- /dev/null +++ b/include/anthem/IntegerVariableDetection.h @@ -0,0 +1,22 @@ +#ifndef __ANTHEM__INTEGER_VARIABLE_DETECTION_H +#define __ANTHEM__INTEGER_VARIABLE_DETECTION_H + +#include +#include + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// IntegerVariableDetection +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void detectIntegerVariables(std::vector &completedFormulas); + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} + +#endif diff --git a/src/anthem/IntegerVariableDetection.cpp b/src/anthem/IntegerVariableDetection.cpp new file mode 100644 index 0000000..6370e32 --- /dev/null +++ b/src/anthem/IntegerVariableDetection.cpp @@ -0,0 +1,419 @@ +#include + +#include +#include +#include +#include +#include +#include + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// IntegerVariableDetection +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +ast::VariableDeclaration::Domain domain(ast::Term &term); + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +enum class OperationResult +{ + Unchanged, + Changed, +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct TermDomainVisitor +{ + static ast::VariableDeclaration::Domain visit(ast::BinaryOperation &binaryOperation) + { + const auto leftDomain = domain(binaryOperation.left); + const auto rightDomain = domain(binaryOperation.right); + + if (leftDomain == ast::VariableDeclaration::Domain::General || rightDomain == ast::VariableDeclaration::Domain::General) + return ast::VariableDeclaration::Domain::General; + + if (leftDomain == ast::VariableDeclaration::Domain::Integer || rightDomain == ast::VariableDeclaration::Domain::Integer) + return ast::VariableDeclaration::Domain::Integer; + + return ast::VariableDeclaration::Domain::Unknown; + } + + static ast::VariableDeclaration::Domain visit(ast::Boolean &) + { + return ast::VariableDeclaration::Domain::General; + } + + static ast::VariableDeclaration::Domain visit(ast::Constant &) + { + // Constants may be set to values of any type + + // TODO: implement explicit integer specifications + return ast::VariableDeclaration::Domain::General; + } + + static ast::VariableDeclaration::Domain visit(ast::Function &) + { + // Functions may return values of any type + + // TODO: implement explicit integer specifications + return ast::VariableDeclaration::Domain::General; + } + + static ast::VariableDeclaration::Domain visit(ast::Integer &) + { + return ast::VariableDeclaration::Domain::Integer; + } + + static ast::VariableDeclaration::Domain visit(ast::Interval &interval) + { + const auto fromDomain = domain(interval.from); + const auto toDomain = domain(interval.to); + + if (fromDomain == ast::VariableDeclaration::Domain::General || toDomain == ast::VariableDeclaration::Domain::General) + return ast::VariableDeclaration::Domain::General; + + if (fromDomain == ast::VariableDeclaration::Domain::Integer || toDomain == ast::VariableDeclaration::Domain::Integer) + return ast::VariableDeclaration::Domain::Integer; + + return ast::VariableDeclaration::Domain::Unknown; + } + + static ast::VariableDeclaration::Domain visit(ast::SpecialInteger &) + { + // TODO: check correctness + return ast::VariableDeclaration::Domain::Integer; + } + + static ast::VariableDeclaration::Domain visit(ast::String &) + { + return ast::VariableDeclaration::Domain::General; + } + + static ast::VariableDeclaration::Domain visit(ast::UnaryOperation &unaryOperation) + { + return domain(unaryOperation.argument); + } + + static ast::VariableDeclaration::Domain visit(ast::Variable &variable) + { + return variable.declaration->domain; + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +ast::VariableDeclaration::Domain domain(ast::Term &term) +{ + return term.accept(TermDomainVisitor()); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +bool isVariable(const ast::Term &term, const ast::VariableDeclaration &variableDeclaration) +{ + if (!term.is()) + return false; + + auto &variable = term.get(); + + return (variable.declaration == &variableDeclaration); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct VariableDomainInFormulaVisitor +{ + static ast::VariableDeclaration::Domain visit(ast::And &and_, ast::VariableDeclaration &variableDeclaration) + { + bool integer = false; + + for (auto &argument : and_.arguments) + { + const auto domain = argument.accept(VariableDomainInFormulaVisitor(), variableDeclaration); + + if (domain == ast::VariableDeclaration::Domain::General) + return ast::VariableDeclaration::Domain::General; + + if (domain == ast::VariableDeclaration::Domain::Integer) + integer = true; + } + + if (integer) + return ast::VariableDeclaration::Domain::Integer; + + return ast::VariableDeclaration::Domain::Unknown; + } + + static ast::VariableDeclaration::Domain visit(ast::Biconditional &biconditional, ast::VariableDeclaration &variableDeclaration) + { + const auto leftDomain = biconditional.left.accept(VariableDomainInFormulaVisitor(), variableDeclaration); + const auto rightDomain = biconditional.left.accept(VariableDomainInFormulaVisitor(), variableDeclaration); + + if (leftDomain == ast::VariableDeclaration::Domain::General || rightDomain == ast::VariableDeclaration::Domain::General) + return ast::VariableDeclaration::Domain::General; + + if (leftDomain == ast::VariableDeclaration::Domain::Integer || rightDomain == ast::VariableDeclaration::Domain::Integer) + return ast::VariableDeclaration::Domain::Integer; + + return ast::VariableDeclaration::Domain::Unknown; + } + + static ast::VariableDeclaration::Domain visit(ast::Boolean &, ast::VariableDeclaration &) + { + // Variable doesn’t occur in Booleans, hence it’s still considered integer until the contrary is found + return ast::VariableDeclaration::Domain::Unknown; + } + + static ast::VariableDeclaration::Domain visit(ast::Comparison &comparison, ast::VariableDeclaration &variableDeclaration) + { + const auto leftIsVariable = isVariable(comparison.left, variableDeclaration); + const auto rightIsVariable = isVariable(comparison.right, variableDeclaration); + + // TODO: implement more cases + if (!leftIsVariable && !rightIsVariable) + return ast::VariableDeclaration::Domain::Unknown; + + auto &otherSide = (leftIsVariable ? comparison.right : comparison.left); + + return domain(otherSide); + } + + static ast::VariableDeclaration::Domain visit(ast::Exists &exists, ast::VariableDeclaration &variableDeclaration) + { + return exists.argument.accept(VariableDomainInFormulaVisitor(), variableDeclaration); + } + + static ast::VariableDeclaration::Domain visit(ast::ForAll &forAll, ast::VariableDeclaration &variableDeclaration) + { + return forAll.argument.accept(VariableDomainInFormulaVisitor(), variableDeclaration); + } + + static ast::VariableDeclaration::Domain visit(ast::Implies &implies, ast::VariableDeclaration &variableDeclaration) + { + const auto antecedentDomain = implies.antecedent.accept(VariableDomainInFormulaVisitor(), variableDeclaration); + const auto consequentDomain = implies.antecedent.accept(VariableDomainInFormulaVisitor(), variableDeclaration); + + if (antecedentDomain == ast::VariableDeclaration::Domain::General || consequentDomain == ast::VariableDeclaration::Domain::General) + return ast::VariableDeclaration::Domain::General; + + if (antecedentDomain == ast::VariableDeclaration::Domain::Integer || consequentDomain == ast::VariableDeclaration::Domain::Integer) + return ast::VariableDeclaration::Domain::Integer; + + return ast::VariableDeclaration::Domain::Unknown; + } + + static ast::VariableDeclaration::Domain visit(ast::In &in, ast::VariableDeclaration &variableDeclaration) + { + const auto elementIsVariable = isVariable(in.element, variableDeclaration); + const auto setIsVariable = isVariable(in.set, variableDeclaration); + + // TODO: implement more cases + if (!elementIsVariable && !setIsVariable) + return ast::VariableDeclaration::Domain::Unknown; + + auto &otherSide = (elementIsVariable ? in.set : in.element); + + return domain(otherSide); + } + + static ast::VariableDeclaration::Domain visit(ast::Not ¬_, ast::VariableDeclaration &variableDeclaration) + { + return not_.argument.accept(VariableDomainInFormulaVisitor(), variableDeclaration); + } + + static ast::VariableDeclaration::Domain visit(ast::Or &or_, ast::VariableDeclaration &variableDeclaration) + { + bool integer = false; + + for (auto &argument : or_.arguments) + { + const auto domain = argument.accept(VariableDomainInFormulaVisitor(), variableDeclaration); + + if (domain == ast::VariableDeclaration::Domain::General) + return ast::VariableDeclaration::Domain::General; + + if (domain == ast::VariableDeclaration::Domain::Integer) + integer = true; + } + + if (integer) + return ast::VariableDeclaration::Domain::Integer; + + return ast::VariableDeclaration::Domain::Unknown; + } + + static ast::VariableDeclaration::Domain visit(ast::Predicate &, ast::VariableDeclaration &) + { + // TODO: implement correctly + return ast::VariableDeclaration::Domain::Unknown; + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// Recursively finds every variable declaration and executes functor to the formula in the scope of the declaration +struct DetectIntegerVariablesVisitor +{ + static OperationResult visit(ast::And &and_) + { + auto operationResult = OperationResult::Unchanged; + + for (auto &argument : and_.arguments) + if (argument.accept(DetectIntegerVariablesVisitor()) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + return operationResult; + } + + static OperationResult visit(ast::Biconditional &biconditional) + { + auto operationResult = OperationResult::Unchanged; + + if (biconditional.left.accept(DetectIntegerVariablesVisitor()) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + if (biconditional.right.accept(DetectIntegerVariablesVisitor()) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + return operationResult; + } + + static OperationResult visit(ast::Boolean &) + { + return OperationResult::Unchanged; + } + + static OperationResult visit(ast::Comparison &) + { + return OperationResult::Unchanged; + } + + static OperationResult visit(ast::Exists &exists) + { + auto operationResult = OperationResult::Unchanged; + + if (exists.argument.accept(DetectIntegerVariablesVisitor()) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + for (auto &variableDeclaration : exists.variables) + if (variableDeclaration->domain == ast::VariableDeclaration::Domain::Unknown + && exists.argument.accept(VariableDomainInFormulaVisitor(), *variableDeclaration) == ast::VariableDeclaration::Domain::Integer) + { + operationResult = OperationResult::Changed; + variableDeclaration->domain = ast::VariableDeclaration::Domain::Integer; + } + + return operationResult; + } + + static OperationResult visit(ast::ForAll &forAll) + { + auto operationResult = OperationResult::Unchanged; + + if (forAll.argument.accept(DetectIntegerVariablesVisitor()) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + for (auto &variableDeclaration : forAll.variables) + if (variableDeclaration->domain == ast::VariableDeclaration::Domain::Unknown + && forAll.argument.accept(VariableDomainInFormulaVisitor(), *variableDeclaration) == ast::VariableDeclaration::Domain::Integer) + { + operationResult = OperationResult::Changed; + variableDeclaration->domain = ast::VariableDeclaration::Domain::Integer; + } + + return operationResult; + } + + static OperationResult visit(ast::Implies &implies) + { + auto operationResult = OperationResult::Unchanged; + + if (implies.antecedent.accept(DetectIntegerVariablesVisitor()) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + if (implies.consequent.accept(DetectIntegerVariablesVisitor()) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + return operationResult; + } + + static OperationResult visit(ast::In &) + { + return OperationResult::Unchanged; + } + + static OperationResult visit(ast::Not ¬_) + { + return not_.argument.accept(DetectIntegerVariablesVisitor()); + } + + static OperationResult visit(ast::Or &or_) + { + auto operationResult = OperationResult::Unchanged; + + for (auto &argument : or_.arguments) + if (argument.accept(DetectIntegerVariablesVisitor()) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + return operationResult; + } + + static OperationResult visit(ast::Predicate &) + { + return OperationResult::Unchanged; + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// Assumes the completed formulas to be in translated but not simplified form. +// That is, completed formulas are either variable-free or universally quantified +void detectIntegerVariables(std::vector &completedFormulas) +{ + auto operationResult{OperationResult::Changed}; + + while (operationResult == OperationResult::Changed) + { + operationResult = OperationResult::Unchanged; + + for (auto &completedFormula : completedFormulas) + { + if (!completedFormula.is()) + continue; + + auto &forAll = completedFormula.get(); + + // TODO: check that integrity constraints are also handled + if (!forAll.argument.is()) + continue; + + auto &biconditional = forAll.argument.get(); + + if (!biconditional.left.is()) + continue; + + auto &definition = biconditional.right; + + if (definition.accept(DetectIntegerVariablesVisitor()) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + for (auto &variableDeclaration : forAll.variables) + if (variableDeclaration->domain == ast::VariableDeclaration::Domain::Unknown + && definition.accept(VariableDomainInFormulaVisitor(), *variableDeclaration) == ast::VariableDeclaration::Domain::Integer) + { + operationResult = OperationResult::Changed; + variableDeclaration->domain = ast::VariableDeclaration::Domain::Integer; + } + } + } +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index 4772d97..7be6031 100644 --- a/src/anthem/Translation.cpp +++ b/src/anthem/Translation.cpp @@ -8,6 +8,7 @@ #include #include +#include #include #include #include @@ -109,6 +110,9 @@ void translate(const char *fileName, std::istream &stream, Context &context) << "” does not match any declared predicate"; } + // Detect integer variables + detectIntegerVariables(completedFormulas); + // Simplify output if specified if (context.performSimplification) for (auto &completedFormula : completedFormulas)