patrick/anthem
1
0
Fork 0
Code Issues 15 Releases 21 Activity

Add option to turn on integer variable detection

Browse Source
This commit is contained in:
Patrick Lühne 2018-04-20 16:31:53 +02:00
parent 19e1e16e45
commit b60c65a810
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
3 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
app/main.cpp
View File

@ -18,6 +18,7 @@ int main(int argc, char **argv)
("i,input", "Input files", cxxopts::value<std::vector<std::string>>()) ("i,input", "Input files", cxxopts::value<std::vector<std::string>>())
("s,simplify", "Simplify the output") ("s,simplify", "Simplify the output")
("c,complete", "Perform completion") ("c,complete", "Perform completion")
("d,detect-integers", "Detect integer variables")
("color", "Colorize output (always, never, auto)", cxxopts::value<std::string>()->default_value("auto")) ("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")) ("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")); ("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.performSimplification = (parseResult.count("simplify") > 0);
context.performCompletion = (parseResult.count("complete") > 0); context.performCompletion = (parseResult.count("complete") > 0);
context.performIntegerDetection = (parseResult.count("detect-integers") > 0);
colorPolicyString = parseResult["color"].as<std::string>(); colorPolicyString = parseResult["color"].as<std::string>();
parenthesisStyleString = parseResult["parentheses"].as<std::string>(); parenthesisStyleString = parseResult["parentheses"].as<std::string>();
logPriorityString = parseResult["log-priority"].as<std::string>(); logPriorityString = parseResult["log-priority"].as<std::string>();

1
include/anthem/Context.h
View File

@ -77,6 +77,7 @@ struct Context
bool performSimplification{false}; bool performSimplification{false};
bool performCompletion{false}; bool performCompletion{false};
bool performIntegerDetection{false};
std::vector<std::unique_ptr<ast::PredicateDeclaration>> predicateDeclarations; std::vector<std::unique_ptr<ast::PredicateDeclaration>> predicateDeclarations;
ast::PredicateDeclaration::Visibility defaultPredicateVisibility{ast::PredicateDeclaration::Visibility::Visible}; ast::PredicateDeclaration::Visibility defaultPredicateVisibility{ast::PredicateDeclaration::Visibility::Visible};

5
src/anthem/Translation.cpp
View File

@ -8,6 +8,7 @@
#include <anthem/Completion.h> #include <anthem/Completion.h>
#include <anthem/Context.h> #include <anthem/Context.h>
#include <anthem/IntegerVariableDetection.h>
#include <anthem/Simplification.h> #include <anthem/Simplification.h>
#include <anthem/StatementVisitor.h> #include <anthem/StatementVisitor.h>
#include <anthem/output/AST.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"; << "” does not match any declared predicate";
} }
// Detect integer variables
if (context.performIntegerDetection)
detectIntegerVariables(completedFormulas);
// Simplify output if specified // Simplify output if specified
if (context.performSimplification) if (context.performSimplification)
for (auto &completedFormula : completedFormulas) for (auto &completedFormula : completedFormulas)