SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
formula_analyzer.cpp
Go to the documentation of this file.
1 #include "formula_analyzer.h"
2 
3 #include "config.h"
4 #include <smtrat-common/smtrat-common.h>
5 
6 #ifdef CLI_ENABLE_ANALYZER
7 
8 #include "parser_smtlib_utils.h"
9 #include "execute_smtlib.h"
10 
11 namespace smtrat {
12 
13 int analyze_file(const std::string& filename) {
14  auto e = parseformula::FormulaCollector();
15  executeFile(filename, e);
16 
17  auto& stats = analyze_formula(e.getFormula());
18 
19  if (e.has_info("status")) {
20  stats.add("answer", e.get_info("status"));
21  }
22 
23  return 0;
24 }
25 
26 }
27 
28 #else
29 
30 namespace smtrat {
31 
32 int analyze_file(const std::string&) {
33  return 0;
34 }
35 
36 }
37 
38 #endif
execute_smtlib.h
formula_analyzer.h
smtrat
Class to create the formulas for axioms.
Definition: handle_options.h:10
smtrat::analyze_formula
analyzer::AnalyzerStatistics & analyze_formula(const FormulaT &f)
Definition: smtrat-analyzer.cpp:10
smtrat::analyze_file
int analyze_file(const std::string &)
Definition: formula_analyzer.cpp:32
smtrat::executeFile
int executeFile(const std::string &pathToInputFile, Executor &e)
Parse the file and save it in formula.
Definition: execute_smtlib.h:38
parser_smtlib_utils.h