From 19e1e16e450e5622ef7ae4041c4f3d4ef2b1f3e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Sun, 29 Apr 2018 21:32:14 +0200 Subject: [PATCH] Implement integer variable detection This adds support for detecting integer variables in formulas. The idea is to iteratively assume variables to be noninteger and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence. The implementation consists of two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom check. Three such checks are implemented. The first one tests whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second one checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer. The third check consists in testing if making a variable noninteger turns the entire formula obtained from completion true. In this case, the statement can be dropped and the variable is concluded to be integer as well. --- include/anthem/IntegerVariableDetection.h | 22 ++ src/anthem/IntegerVariableDetection.cpp | 332 ++++++++++++++++++++++ 2 files changed, 354 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..8fa5d07 --- /dev/null +++ b/src/anthem/IntegerVariableDetection.cpp @@ -0,0 +1,332 @@ +#include + +#include +#include +#include +#include +#include +#include +#include +#include +#include + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// IntegerVariableDetection +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +using VariableDomainMap = std::map; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap) +{ + if (variable.declaration->domain != Domain::Unknown) + return variable.declaration->domain; + + const auto match = variableDomainMap.find(variable.declaration); + + if (match == variableDomainMap.end()) + return Domain::Unknown; + + return match->second; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void clearVariableDomainMap(VariableDomainMap &variableDomainMap) +{ + for (auto &variableDeclaration : variableDomainMap) + variableDeclaration.second = Domain::Unknown; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct VariableDomainMapAccessor +{ + Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap) + { + return domain(variable, variableDomainMap); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Type type(const ast::Term &term, VariableDomainMap &variableDomainMap) +{ + return type(term, variableDomainMap); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variableDomainMap) +{ + return evaluate(formula, variableDomainMap); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +struct ForEachVariableDeclarationVisitor +{ + template + static OperationResult visit(ast::And &and_, Arguments &&... arguments) + { + auto operationResult = OperationResult::Unchanged; + + for (auto &argument : and_.arguments) + if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward(arguments)...) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + return operationResult; + } + + template + static OperationResult visit(ast::Biconditional &biconditional, Arguments &&... arguments) + { + auto operationResult = OperationResult::Unchanged; + + if (biconditional.left.accept(ForEachVariableDeclarationVisitor(), std::forward(arguments)...) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + if (biconditional.right.accept(ForEachVariableDeclarationVisitor(), std::forward(arguments)...) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + return operationResult; + } + + template + static OperationResult visit(ast::Boolean &, Arguments &&...) + { + return OperationResult::Unchanged; + } + + template + static OperationResult visit(ast::Comparison &, Arguments &&...) + { + return OperationResult::Unchanged; + } + + template + static OperationResult visit(ast::Exists &exists, Arguments &&... arguments) + { + auto operationResult = OperationResult::Unchanged; + + if (exists.argument.accept(ForEachVariableDeclarationVisitor(), std::forward(arguments)...) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + for (auto &variableDeclaration : exists.variables) + if (Functor()(*variableDeclaration, exists.argument, std::forward(arguments)...) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + return operationResult; + } + + template + static OperationResult visit(ast::ForAll &forAll, Arguments &&... arguments) + { + auto operationResult = OperationResult::Unchanged; + + if (forAll.argument.accept(ForEachVariableDeclarationVisitor(), std::forward(arguments)...) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + for (auto &variableDeclaration : forAll.variables) + if (Functor()(*variableDeclaration, forAll.argument, std::forward(arguments)...) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + return operationResult; + } + + template + static OperationResult visit(ast::Implies &implies, Arguments &&... arguments) + { + auto operationResult = OperationResult::Unchanged; + + if (implies.antecedent.accept(ForEachVariableDeclarationVisitor(), std::forward(arguments)...) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + if (implies.consequent.accept(ForEachVariableDeclarationVisitor(), std::forward(arguments)...) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + return operationResult; + } + + template + static OperationResult visit(ast::In &, Arguments &&...) + { + return OperationResult::Unchanged; + } + + template + static OperationResult visit(ast::Not ¬_, Arguments &&... arguments) + { + return not_.argument.accept(ForEachVariableDeclarationVisitor(), std::forward(arguments)...); + } + + template + static OperationResult visit(ast::Or &or_, Arguments &&... arguments) + { + auto operationResult = OperationResult::Unchanged; + + for (auto &argument : or_.arguments) + if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward(arguments)...) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + return operationResult; + } + + template + static OperationResult visit(ast::Predicate &, Arguments &&...) + { + return OperationResult::Unchanged; + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct CheckIfDefinitionFalseFunctor +{ + OperationResult operator()(ast::VariableDeclaration &variableDeclaration, + ast::Formula &, ast::Formula &definition, VariableDomainMap &variableDomainMap) + { + if (variableDeclaration.domain != Domain::Unknown) + return OperationResult::Unchanged; + + clearVariableDomainMap(variableDomainMap); + + // As a hypothesis, make the parameter’s domain noninteger + variableDomainMap[&variableDeclaration] = Domain::Noninteger; + + const auto result = evaluate(definition, variableDomainMap); + + if (result == EvaluationResult::Error || result == EvaluationResult::False) + { + // If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer + variableDeclaration.domain = Domain::Integer; + return OperationResult::Changed; + } + + return OperationResult::Unchanged; + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct CheckIfQuantifiedFormulaFalseFunctor +{ + OperationResult operator()(ast::VariableDeclaration &variableDeclaration, + ast::Formula &quantifiedFormula, VariableDomainMap &variableDomainMap) + { + if (variableDeclaration.domain != Domain::Unknown) + return OperationResult::Unchanged; + + clearVariableDomainMap(variableDomainMap); + + // As a hypothesis, make the parameter’s domain noninteger + variableDomainMap[&variableDeclaration] = Domain::Noninteger; + + const auto result = evaluate(quantifiedFormula, variableDomainMap); + + if (result == EvaluationResult::Error || result == EvaluationResult::False) + { + // If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer + variableDeclaration.domain = Domain::Integer; + return OperationResult::Changed; + } + + return OperationResult::Unchanged; + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct CheckIfCompletedFormulaTrueFunctor +{ + OperationResult operator()(ast::VariableDeclaration &variableDeclaration, + ast::Formula &, ast::Formula &completedFormula, VariableDomainMap &variableDomainMap) + { + if (variableDeclaration.domain != Domain::Unknown) + return OperationResult::Unchanged; + + clearVariableDomainMap(variableDomainMap); + + // As a hypothesis, make the parameter’s domain noninteger + variableDomainMap[&variableDeclaration] = Domain::Noninteger; + + const auto result = evaluate(completedFormula, variableDomainMap); + + if (result == EvaluationResult::Error || result == EvaluationResult::True) + { + // If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer + variableDeclaration.domain = Domain::Integer; + return OperationResult::Changed; + } + + 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) +{ + VariableDomainMap variableDomainMap; + auto operationResult = OperationResult::Changed; + + while (operationResult == OperationResult::Changed) + { + operationResult = OperationResult::Unchanged; + + for (auto &completedFormula : completedFormulas) + { + if (completedFormula.accept(ForEachVariableDeclarationVisitor(), variableDomainMap) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + if (completedFormula.accept(ForEachVariableDeclarationVisitor(), completedFormula, variableDomainMap) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + if (!completedFormula.is()) + continue; + + auto &forAll = completedFormula.get(); + + if (!forAll.argument.is()) + continue; + + auto &biconditional = forAll.argument.get(); + + if (!biconditional.left.is()) + continue; + + auto &predicate = biconditional.left.get(); + auto &definition = biconditional.right; + + if (completedFormula.accept(ForEachVariableDeclarationVisitor(), definition, variableDomainMap) == OperationResult::Changed) + operationResult = OperationResult::Changed; + + assert(predicate.arguments.size() == predicate.declaration->arity()); + + for (size_t i = 0; i < predicate.arguments.size(); i++) + { + auto &variableArgument = predicate.arguments[i]; + auto ¶meter = predicate.declaration->parameters[i]; + + assert(variableArgument.is()); + + auto &variable = variableArgument.get(); + + parameter.domain = variable.declaration->domain; + } + } + } +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +}