SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
SymmetryModule.tpp
Go to the documentation of this file.
1 /**
2  * @file SymmetryModule.cpp
3  */
4 
5 #include "SymmetryModule.h"
6 
7 #include <carl-formula/symmetry/symmetry.h>
8 
9 namespace smtrat
10 {
11  template<class Settings>
12  SymmetryModule<Settings>::SymmetryModule(const ModuleInput* _formula, Conditionals& _conditionals, Manager* _manager):
13  PModule( _formula, _conditionals, _manager, Settings::moduleName )
14  {}
15 
16  template<class Settings>
17  SymmetryModule<Settings>::~SymmetryModule()
18  {}
19 
20  template<class Settings>
21  Answer SymmetryModule<Settings>::checkCore()
22  {
23  if (is_minimizing()) {
24  SMTRAT_LOG_ERROR("smtrat.symmetry", "Optimization not supported");
25  assert(false);
26  }
27 
28  for (auto it = rReceivedFormula().begin(); it != rReceivedFormula().end(); ++it) {
29  addReceivedSubformulaToPassedFormula(it);
30  }
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);
35  }
36 
37  Answer ans = runBackends();
38  if (ans == UNSAT) {
39  generateTrivialInfeasibleSubset();
40  }
41  return ans;
42  }
43 }
44 
45