From 2b62c6227de206978a407883f87fc6af0e6c965e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Sun, 22 Apr 2018 14:43:15 +0200 Subject: [PATCH] Move Domain class to Utils header --- include/anthem/AST.h | 2 +- include/anthem/Arithmetics.h | 26 ++++++++++---------- include/anthem/Domain.h | 27 --------------------- include/anthem/StatementVisitor.h | 2 +- include/anthem/Utils.h | 16 +++++++------ src/anthem/IntegerVariableDetection.cpp | 32 ++++++++++++------------- src/anthem/Translation.cpp | 2 +- 7 files changed, 41 insertions(+), 66 deletions(-) delete mode 100644 include/anthem/Domain.h diff --git a/include/anthem/AST.h b/include/anthem/AST.h index d8a1132..3507a2b 100644 --- a/include/anthem/AST.h +++ b/include/anthem/AST.h @@ -2,7 +2,7 @@ #define __ANTHEM__AST_H #include -#include +#include namespace anthem { diff --git a/include/anthem/Arithmetics.h b/include/anthem/Arithmetics.h index 3bd6c10..ec501d6 100644 --- a/include/anthem/Arithmetics.h +++ b/include/anthem/Arithmetics.h @@ -14,7 +14,7 @@ namespace anthem struct DefaultVariableDomainAccessor { - ast::Domain operator()(const ast::Variable &variable) + Domain operator()(const ast::Variable &variable) { return variable.declaration->domain; } @@ -59,11 +59,11 @@ struct IsTermArithmeticVisitor { switch (function.declaration->domain) { - case ast::Domain::General: + case Domain::General: return EvaluationResult::False; - case ast::Domain::Integer: + case Domain::Integer: return EvaluationResult::True; - case ast::Domain::Unknown: + case Domain::Unknown: return EvaluationResult::Unknown; } @@ -127,11 +127,11 @@ struct IsTermArithmeticVisitor switch (domain) { - case ast::Domain::General: + case Domain::General: return EvaluationResult::False; - case ast::Domain::Integer: + case Domain::Integer: return EvaluationResult::True; - case ast::Domain::Unknown: + case Domain::Unknown: return EvaluationResult::Unknown; } @@ -184,11 +184,11 @@ struct IsTermIntegerVisitor { switch (function.declaration->domain) { - case ast::Domain::General: + case Domain::General: return EvaluationResult::False; - case ast::Domain::Integer: + case Domain::Integer: return EvaluationResult::True; - case ast::Domain::Unknown: + case Domain::Unknown: return EvaluationResult::Unknown; } @@ -236,11 +236,11 @@ struct IsTermIntegerVisitor { switch (variable.declaration->domain) { - case ast::Domain::General: + case Domain::General: return EvaluationResult::False; - case ast::Domain::Integer: + case Domain::Integer: return EvaluationResult::True; - case ast::Domain::Unknown: + case Domain::Unknown: return EvaluationResult::Unknown; } diff --git a/include/anthem/Domain.h b/include/anthem/Domain.h deleted file mode 100644 index 0625081..0000000 --- a/include/anthem/Domain.h +++ /dev/null @@ -1,27 +0,0 @@ -#ifndef __ANTHEM__DOMAIN_H -#define __ANTHEM__DOMAIN_H - -namespace anthem -{ -namespace ast -{ - -//////////////////////////////////////////////////////////////////////////////////////////////////// -// -// Domain -// -//////////////////////////////////////////////////////////////////////////////////////////////////// - -enum class Domain -{ - General, - Integer, - Unknown, -}; - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -} -} - -#endif diff --git a/include/anthem/StatementVisitor.h b/include/anthem/StatementVisitor.h index 20f2b76..1701113 100644 --- a/include/anthem/StatementVisitor.h +++ b/include/anthem/StatementVisitor.h @@ -237,7 +237,7 @@ struct StatementVisitor const size_t arity = aritySymbol.number(); auto functionDeclaration = context.findOrCreateFunctionDeclaration(function.name, arity); - functionDeclaration->domain = ast::Domain::Integer; + functionDeclaration->domain = Domain::Integer; return true; }; diff --git a/include/anthem/Utils.h b/include/anthem/Utils.h index ae2e528..56633ab 100644 --- a/include/anthem/Utils.h +++ b/include/anthem/Utils.h @@ -1,13 +1,6 @@ #ifndef __ANTHEM__UTILS_H #define __ANTHEM__UTILS_H -#include - -#include - -#include -#include - namespace anthem { @@ -50,6 +43,15 @@ enum class OperationResult //////////////////////////////////////////////////////////////////////////////////////////////////// +enum class Domain +{ + General, + Integer, + Unknown, +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + } #endif diff --git a/src/anthem/IntegerVariableDetection.cpp b/src/anthem/IntegerVariableDetection.cpp index af4aa4b..297754e 100644 --- a/src/anthem/IntegerVariableDetection.cpp +++ b/src/anthem/IntegerVariableDetection.cpp @@ -18,19 +18,19 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// -using VariableDomainMap = std::map; +using VariableDomainMap = std::map; //////////////////////////////////////////////////////////////////////////////////////////////////// -ast::Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap) +Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap) { - if (variable.declaration->domain != ast::Domain::Unknown) + if (variable.declaration->domain != Domain::Unknown) return variable.declaration->domain; const auto match = variableDomainMap.find(variable.declaration); if (match == variableDomainMap.end()) - return ast::Domain::Unknown; + return Domain::Unknown; return match->second; } @@ -40,14 +40,14 @@ ast::Domain domain(const ast::Variable &variable, VariableDomainMap &variableDom void clearVariableDomainMap(VariableDomainMap &variableDomainMap) { for (auto &variableDeclaration : variableDomainMap) - variableDeclaration.second = ast::Domain::Unknown; + variableDeclaration.second = Domain::Unknown; } //////////////////////////////////////////////////////////////////////////////////////////////////// struct VariableDomainMapAccessor { - ast::Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap) + Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap) { return domain(variable, variableDomainMap); } @@ -247,7 +247,7 @@ struct EvaluateFormulaVisitor const auto &argument = predicate.arguments[i]; const auto ¶meter = predicate.declaration->parameters[i]; - if (parameter.domain != ast::Domain::Integer) + if (parameter.domain != Domain::Integer) continue; const auto isArgumentArithmetic = isArithmetic(argument, variableDomainMap); @@ -392,7 +392,7 @@ struct CheckIfDefinitionFalseFunctor OperationResult operator()(ast::VariableDeclaration &variableDeclaration, ast::Formula &, ast::Formula &definition, VariableDomainMap &variableDomainMap) { - if (variableDeclaration.domain != ast::Domain::Unknown) + if (variableDeclaration.domain != Domain::Unknown) return OperationResult::Unchanged; clearVariableDomainMap(variableDomainMap); @@ -403,14 +403,14 @@ struct CheckIfDefinitionFalseFunctor return OperationResult::Unchanged; // As a hypothesis, make the parameter’s domain noninteger - variableDomainMap[&variableDeclaration] = ast::Domain::General; + variableDomainMap[&variableDeclaration] = Domain::General; 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 = ast::Domain::Integer; + variableDeclaration.domain = Domain::Integer; return OperationResult::Changed; } @@ -425,7 +425,7 @@ struct CheckIfQuantifiedFormulaFalseFunctor OperationResult operator()(ast::VariableDeclaration &variableDeclaration, ast::Formula &quantifiedFormula, VariableDomainMap &variableDomainMap) { - if (variableDeclaration.domain != ast::Domain::Unknown) + if (variableDeclaration.domain != Domain::Unknown) return OperationResult::Unchanged; clearVariableDomainMap(variableDomainMap); @@ -436,14 +436,14 @@ struct CheckIfQuantifiedFormulaFalseFunctor return OperationResult::Unchanged; // As a hypothesis, make the parameter’s domain noninteger - variableDomainMap[&variableDeclaration] = ast::Domain::General; + variableDomainMap[&variableDeclaration] = Domain::General; 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 = ast::Domain::Integer; + variableDeclaration.domain = Domain::Integer; return OperationResult::Changed; } @@ -458,7 +458,7 @@ struct CheckIfCompletedFormulaTrueFunctor OperationResult operator()(ast::VariableDeclaration &variableDeclaration, ast::Formula &, ast::Formula &completedFormula, VariableDomainMap &variableDomainMap) { - if (variableDeclaration.domain != ast::Domain::Unknown) + if (variableDeclaration.domain != Domain::Unknown) return OperationResult::Unchanged; clearVariableDomainMap(variableDomainMap); @@ -469,14 +469,14 @@ struct CheckIfCompletedFormulaTrueFunctor return OperationResult::Unchanged; // As a hypothesis, make the parameter’s domain noninteger - variableDomainMap[&variableDeclaration] = ast::Domain::General; + variableDomainMap[&variableDeclaration] = Domain::General; 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 = ast::Domain::Integer; + variableDeclaration.domain = Domain::Integer; return OperationResult::Changed; } diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index c291690..aaafb4f 100644 --- a/src/anthem/Translation.cpp +++ b/src/anthem/Translation.cpp @@ -147,7 +147,7 @@ void translate(const char *fileName, std::istream &stream, Context &context) { auto ¶meter = predicateDeclaration->parameters[i]; - if (parameter.domain != ast::Domain::Integer) + if (parameter.domain != Domain::Integer) continue; context.logger.outputStream()