2 * @file SymmetryModule.cpp
5 #include "SymmetryModule.h"
7 #include <carl-formula/symmetry/symmetry.h>
11 template<class Settings>
12 SymmetryModule<Settings>::SymmetryModule(const ModuleInput* _formula, Conditionals& _conditionals, Manager* _manager):
13 PModule( _formula, _conditionals, _manager, Settings::moduleName )
16 template<class Settings>
17 SymmetryModule<Settings>::~SymmetryModule()
20 template<class Settings>
21 Answer SymmetryModule<Settings>::checkCore()
23 if (is_minimizing()) {
24 SMTRAT_LOG_ERROR("smtrat.symmetry", "Optimization not supported");
28 for (auto it = rReceivedFormula().begin(); it != rReceivedFormula().end(); ++it) {
29 addReceivedSubformulaToPassedFormula(it);
31 auto symm = carl::formula::breakSymmetries(FormulaT(rPassedFormula()));
32 if (!symm.is_true()) {
33 SMTRAT_LOG_DEBUG("smtrat.symmetry", "Broke symmetries by" << std::endl << symm);
34 addSubformulaToPassedFormula(symm);
37 Answer ans = runBackends();
39 generateTrivialInfeasibleSubset();