From b60c65a8107d8a73576e5cfbaa24eac00807b636 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Fri, 20 Apr 2018 16:31:53 +0200
Subject: [PATCH] Add option to turn on integer variable detection

---
 app/main.cpp               | 2 ++
 include/anthem/Context.h   | 1 +
 src/anthem/Translation.cpp | 5 +++++
 3 files changed, 8 insertions(+)

diff --git a/app/main.cpp b/app/main.cpp
index 1697ef9..71c7cc5 100644
--- a/app/main.cpp
+++ b/app/main.cpp
@@ -18,6 +18,7 @@ int main(int argc, char **argv)
 		("i,input", "Input files", cxxopts::value<std::vector<std::string>>())
 		("s,simplify", "Simplify the output")
 		("c,complete", "Perform completion")
+		("d,detect-integers", "Detect integer variables")
 		("color", "Colorize output (always, never, auto)", cxxopts::value<std::string>()->default_value("auto"))
 		("parentheses", "Parenthesis style (normal, full)", cxxopts::value<std::string>()->default_value("normal"))
 		("p,log-priority", "Log messages starting from this priority (debug, info, warning, error)", cxxopts::value<std::string>()->default_value("info"));
@@ -50,6 +51,7 @@ int main(int argc, char **argv)
 
 		context.performSimplification = (parseResult.count("simplify") > 0);
 		context.performCompletion = (parseResult.count("complete") > 0);
+		context.performIntegerDetection = (parseResult.count("detect-integers") > 0);
 		colorPolicyString = parseResult["color"].as<std::string>();
 		parenthesisStyleString = parseResult["parentheses"].as<std::string>();
 		logPriorityString = parseResult["log-priority"].as<std::string>();
diff --git a/include/anthem/Context.h b/include/anthem/Context.h
index a341a43..e533776 100644
--- a/include/anthem/Context.h
+++ b/include/anthem/Context.h
@@ -77,6 +77,7 @@ struct Context
 
 	bool performSimplification{false};
 	bool performCompletion{false};
+	bool performIntegerDetection{false};
 
 	std::vector<std::unique_ptr<ast::PredicateDeclaration>> predicateDeclarations;
 	ast::PredicateDeclaration::Visibility defaultPredicateVisibility{ast::PredicateDeclaration::Visibility::Visible};
diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp
index 58bfa06..b1f69b2 100644
--- a/src/anthem/Translation.cpp
+++ b/src/anthem/Translation.cpp
@@ -8,6 +8,7 @@
 
 #include <anthem/Completion.h>
 #include <anthem/Context.h>
+#include <anthem/IntegerVariableDetection.h>
 #include <anthem/Simplification.h>
 #include <anthem/StatementVisitor.h>
 #include <anthem/output/AST.h>
@@ -109,6 +110,10 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 				<< "” does not match any declared predicate";
 	}
 
+	// Detect integer variables
+	if (context.performIntegerDetection)
+		detectIntegerVariables(completedFormulas);
+
 	// Simplify output if specified
 	if (context.performSimplification)
 		for (auto &completedFormula : completedFormulas)