SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
PFEModule.tpp
Go to the documentation of this file.
1 /**
2  * @file PFEModule.cpp
3  * @author Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
4  * @author Florian Corzilius <corzilius@cs.rwth-aachen.de>
5  *
6  * @version 2015-09-10
7  * Created on 2015-09-10.
8  */
9 
10 #include "PFEModule.h"
11 
12 namespace smtrat
13 {
14  template<class Settings>
15  PFEModule<Settings>::PFEModule( const ModuleInput* _formula, Conditionals& _conditionals, Manager* _manager ):
16  PModule( _formula, _conditionals, _manager, Settings::moduleName ),
17  varbounds()
18  {
19  removeFactorsFunction = std::bind(&PFEModule<Settings>::removeFactors, this, std::placeholders::_1);
20  removeSquaresFunction = std::bind(&PFEModule<Settings>::removeSquares, this, std::placeholders::_1);
21  implyDefinitenessFunction = std::bind(&PFEModule<Settings>::implyDefiniteness, this, std::placeholders::_1);
22  }
23 
24  template<class Settings>
25  PFEModule<Settings>::~PFEModule()
26  {}
27 
28  template<typename Settings>
29  bool PFEModule<Settings>::addCore(ModuleInput::const_iterator _subformula) {
30  if (varbounds.addBound(_subformula->formula(), _subformula->formula())) {
31  boundsChanged = true;
32  }
33  if (varbounds.isConflicting()) {
34  SMTRAT_LOG_DEBUG("smtrat.pfe", "Identified direct conflict on bounds: " << varbounds.getConflict());
35  mInfeasibleSubsets.push_back(varbounds.getConflict());
36  return false;
37  }
38  return true;
39  }
40 
41  template<class Settings>
42  Answer PFEModule<Settings>::checkCore() {
43  auto receivedFormula = firstUncheckedReceivedSubformula();
44  if (boundsChanged) {
45  clearPassedFormula();
46  receivedFormula = rReceivedFormula().begin();
47  boundsChanged = false;
48  }
49  while (receivedFormula != rReceivedFormula().end()) {
50  if (is_minimizing() && receivedFormula->formula().variables().find(objective()) != receivedFormula->formula().variables().end()) {
51  SMTRAT_LOG_DEBUG("smtrat.pfe", "Ignoring " << receivedFormula->formula() << " as it containts the objective variable " << objective());
52  addReceivedSubformulaToPassedFormula(receivedFormula);
53  ++receivedFormula;
54  continue;
55  }
56  if (receivedFormula->formula().is_bound()) {
57  addReceivedSubformulaToPassedFormula(receivedFormula);
58  ++receivedFormula;
59  continue;
60  }
61  FormulaT formula = carl::visit_result(receivedFormula->formula(), removeFactorsFunction);
62  formula = carl::visit_result(formula, removeSquaresFunction);
63  //formula = carl::visit(formula, implyDefinitenessFunction);
64  if (receivedFormula->formula() != formula) {
65  SMTRAT_LOG_DEBUG("smtrat.pfe", "Simplified " << receivedFormula->formula());
66  SMTRAT_LOG_DEBUG("smtrat.pfe", "to " << formula);
67  SMTRAT_LOG_DEBUG("smtrat.pfe", "due to bounds " << varbounds.getEvalIntervalMap());
68  }
69 
70  if (formula.is_false()) {
71  mInfeasibleSubsets.clear();
72  carl::carlVariables vars = carl::variables(receivedFormula->formula());
73  FormulaSetT infeasibleSubset = varbounds.getOriginSetOfBounds(vars.as_set());
74  infeasibleSubset.insert(receivedFormula->formula());
75  mInfeasibleSubsets.push_back(std::move(infeasibleSubset));
76  return UNSAT;
77  }
78  if (!formula.is_true()) {
79  if (formula == receivedFormula->formula()) {
80  addReceivedSubformulaToPassedFormula(receivedFormula);
81  } else {
82  carl::carlVariables vars = carl::variables(receivedFormula->formula());
83  FormulasT origins = varbounds.getOriginsOfBounds(vars.as_set());
84  origins.push_back(receivedFormula->formula());
85  addSubformulaToPassedFormula(formula, std::make_shared<std::vector<FormulaT>>(std::move(origins)));
86  }
87  }
88  ++receivedFormula;
89  }
90  generateVariableAssignments();
91  SMTRAT_LOG_DEBUG("smtrat.pfe", "Simplification: " << FormulaT(rReceivedFormula()));
92  SMTRAT_LOG_DEBUG("smtrat.pfe", "to " << FormulaT(rPassedFormula()));
93  Answer ans = runBackends();
94  if (ans == UNSAT) {
95  getInfeasibleSubsets();
96  }
97  return ans;
98  }
99 
100  template<typename Settings>
101  void PFEModule<Settings>::removeCore(ModuleInput::const_iterator _subformula) {
102  if (varbounds.removeBound(_subformula->formula(), _subformula->formula()) == 2) {
103  boundsChanged = true;
104  }
105  }
106 
107  template<typename Settings>
108  FormulaT PFEModule<Settings>::removeFactors(const FormulaT& formula){
109  if(formula.type() == carl::FormulaType::CONSTRAINT) {
110  const auto& factors = formula.constraint().lhs_factorization();
111  SMTRAT_LOG_TRACE("smtrat.pfe", "Factorization of " << formula << " = " << factors);
112  std::vector<Factorization::const_iterator> Pq;
113  std::vector<Factorization::const_iterator> Pr;
114  carl::Relation qrel = carl::Relation::GREATER;
115  for (auto it = factors.begin(); it != factors.end(); it++) {
116  auto i = carl::evaluate(it->first, completeBounds(it->first));
117  SMTRAT_LOG_TRACE("smtrat.pfe", "Considering factor " << it->first << " with bounds " << i);
118  if (i.is_positive()) {
119  qrel = combine(qrel, carl::Relation::GREATER, it->second);
120  Pq.push_back(it);
121  } else if (i.is_semi_positive()) {
122  qrel = combine(qrel, carl::Relation::GEQ, it->second);
123  Pq.push_back(it);
124  } else if (i.is_negative()) {
125  qrel = combine(qrel, carl::Relation::LESS, it->second);
126  Pq.push_back(it);
127  } else if (i.is_semi_negative()) {
128  qrel = combine(qrel, carl::Relation::LEQ, it->second);
129  Pq.push_back(it);
130  } else if (i.is_zero()) {
131  qrel = combine(qrel, carl::Relation::EQ, it->second);
132  Pq.push_back(it);
133  } else {
134  Pr.push_back(it);
135  }
136  }
137  if (!Pq.empty()) {
138  carl::Relation rel = formula.constraint().relation();
139  assert(qrel != carl::Relation::NEQ);
140  switch (qrel) {
141  case carl::Relation::GREATER: return FormulaT(getPoly(Pr), rel);
142  case carl::Relation::GEQ:
143  switch (rel) {
144  case carl::Relation::EQ: return FormulaT(carl::FormulaType::OR, {FormulaT(getPoly(Pq), carl::Relation::EQ), FormulaT(getPoly(Pr), rel)});
145  case carl::Relation::NEQ: return FormulaT(carl::FormulaType::AND, {FormulaT(getPoly(Pq), carl::Relation::GREATER), FormulaT(getPoly(Pr), rel)});
146  case carl::Relation::GEQ: return FormulaT(carl::FormulaType::OR, {FormulaT(getPoly(Pq), carl::Relation::EQ), FormulaT(getPoly(Pr), rel)});
147  case carl::Relation::GREATER: return FormulaT(carl::FormulaType::AND, {FormulaT(getPoly(Pq), carl::Relation::GREATER), FormulaT(getPoly(Pr), rel)});
148  case carl::Relation::LEQ: return FormulaT(carl::FormulaType::OR, {FormulaT(getPoly(Pq), carl::Relation::EQ), FormulaT(getPoly(Pr), rel)});
149  case carl::Relation::LESS: return FormulaT(carl::FormulaType::AND, {FormulaT(getPoly(Pq), carl::Relation::GREATER), FormulaT(getPoly(Pr), rel)});
150  default: return formula;
151  }
152  case carl::Relation::EQ: return FormulaT(Poly(0), rel);
153  case carl::Relation::LEQ:
154  switch (rel) {
155  case carl::Relation::EQ: return FormulaT(carl::FormulaType::OR, {FormulaT(getPoly(Pq), carl::Relation::EQ), FormulaT(getPoly(Pr), rel)});
156  case carl::Relation::NEQ: return FormulaT(carl::FormulaType::AND, {FormulaT(getPoly(Pq), carl::Relation::LESS), FormulaT(getPoly(Pr), rel)});
157  case carl::Relation::GEQ: return FormulaT(carl::FormulaType::OR, {FormulaT(getPoly(Pq), carl::Relation::EQ), FormulaT(getPoly(Pr), carl::Relation::LEQ)});
158  case carl::Relation::GREATER: return FormulaT(carl::FormulaType::AND, {FormulaT(getPoly(Pq), carl::Relation::LESS), FormulaT(getPoly(Pr), carl::Relation::LESS)});
159  case carl::Relation::LEQ: return FormulaT(carl::FormulaType::OR, {FormulaT(getPoly(Pq), carl::Relation::EQ), FormulaT(getPoly(Pr), carl::Relation::GEQ)});
160  case carl::Relation::LESS: return FormulaT(carl::FormulaType::AND, {FormulaT(getPoly(Pq), carl::Relation::LESS), FormulaT(getPoly(Pr), carl::Relation::GREATER)});
161  default: return formula;
162  }
163  case carl::Relation::LESS:
164  switch (rel) {
165  case carl::Relation::EQ: return FormulaT(getPoly(Pr), rel);
166  case carl::Relation::NEQ: return FormulaT(getPoly(Pr), rel);
167  case carl::Relation::GEQ: return FormulaT(getPoly(Pr), carl::Relation::LEQ);
168  case carl::Relation::GREATER: return FormulaT(getPoly(Pr), carl::Relation::LESS);
169  case carl::Relation::LEQ: return FormulaT(getPoly(Pr), carl::Relation::GEQ);
170  case carl::Relation::LESS: return FormulaT(getPoly(Pr), carl::Relation::GREATER);
171  default: return formula;
172  }
173  default: return formula;
174  }
175  }
176  }
177  return formula;
178  }
179 
180  template<typename Settings>
181  FormulaT PFEModule<Settings>::removeSquaresFromStrict(const FormulaT& formula) {
182  const auto& factors = formula.constraint().lhs_factorization();
183  std::vector<Factorization::const_iterator> Pq;
184  std::vector<Factorization::const_iterator> Pr;
185 
186  for (auto it = factors.begin(); it != factors.end(); ++it) {
187  if (it->second % 2 == 0) {
188  // This implies that this factor is (strictly) positive and essentially reduces to factor != 0
189  SMTRAT_LOG_DEBUG("smtrat.pfe", "Eliminating factors " << it->first << " ^ " << it->second);
190  Pq.push_back(it);
191  } else {
192  Pr.push_back(it);
193  }
194  }
195 
196  if (Pq.empty()) return formula;
197 
198  FormulasT res;
199  for (const auto& q: Pq) {
200  res.emplace_back(ConstraintT(q->first, carl::Relation::NEQ));
201  }
202  auto polyrest = std::accumulate(Pr.begin(), Pr.end(), Poly(1), [](const auto& a, const auto& b){ return a * carl::pow(b->first, b->second); });
203  res.emplace_back(ConstraintT(polyrest, formula.constraint().relation()));
204  return FormulaT(carl::FormulaType::AND, std::move(res));
205  }
206 
207  template<typename Settings>
208  FormulaT PFEModule<Settings>::removeSquares(const FormulaT& formula) {
209  if(formula.type() != carl::FormulaType::CONSTRAINT) return formula;
210 
211  carl::Relation rel = formula.constraint().relation();
212 
213  switch (rel) {
214  case carl::Relation::GREATER:
215  case carl::Relation::LESS:
216  SMTRAT_LOG_TRACE("smtrat.pfe", "Eliminating squares from " << formula);
217  return removeSquaresFromStrict(formula);
218  case carl::Relation::EQ:
219  case carl::Relation::NEQ:
220  case carl::Relation::GEQ:
221  case carl::Relation::LEQ:
222  default:
223  SMTRAT_LOG_TRACE("smtrat.pfe", "Nothing to do for " << formula);
224  return formula;
225  }
226  }
227 
228  template<typename Settings>
229  FormulaT PFEModule<Settings>::implyDefinitenessFromStrict(const FormulaT& formula) {
230  FormulasT res;
231  res.emplace_back(formula);
232  for (const auto& f: formula.constraint().lhs_factorization()) {
233  res.emplace_back(ConstraintT(f.first, carl::Relation::NEQ));
234  }
235  return FormulaT(carl::FormulaType::AND, std::move(res));
236  }
237 
238  template<typename Settings>
239  FormulaT PFEModule<Settings>::implyDefiniteness(const FormulaT& formula) {
240  if(formula.type() != carl::FormulaType::CONSTRAINT) return formula;
241 
242  carl::Relation rel = formula.constraint().relation();
243 
244  switch (rel) {
245  case carl::Relation::GREATER:
246  case carl::Relation::LESS:
247  case carl::Relation::NEQ:
248  SMTRAT_LOG_TRACE("smtrat.pfe", "Imply definiteness from " << formula);
249  return implyDefinitenessFromStrict(formula);
250  case carl::Relation::EQ:
251  case carl::Relation::GEQ:
252  case carl::Relation::LEQ:
253  default:
254  SMTRAT_LOG_TRACE("smtrat.pfe", "Nothing to do for " << formula);
255  return formula;
256  }
257  }
258 }
259 
260