SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
STropModule.tpp
Go to the documentation of this file.
1 /**
2  * @file STropModule.cpp
3  * @author Ömer Sali <oemer.sali@rwth-aachen.de>
4  *
5  * @version 2018-04-04
6  * Created on 2017-09-13.
7  */
8 
9 #include "STropModule.h"
10 #include <carl-formula/formula/functions/NNF.h>
11 
12 namespace smtrat {
13 template<class Settings>
14 STropModule<Settings>::STropModule(const ModuleInput* _formula, Conditionals& _conditionals, Manager* _manager)
15  : Module(_formula, _conditionals, _manager)
16  , mSeparators()
17  , mChangedSeparators()
18  , mRelationalConflicts(0)
19  , mLinearizationConflicts()
20  , mCheckedWithBackends(false)
21 {}
22 
23 template<class Settings>
24 bool STropModule<Settings>::addCore(ModuleInput::const_iterator _subformula) {
25  addReceivedSubformulaToPassedFormula(_subformula);
26  const FormulaT& formula = _subformula->formula();
27  if (formula.type() == carl::FormulaType::FALSE) {
28  SMTRAT_STATISTICS_CALL(mStatistics.answer_by(STropModuleStatistics::AnswerBy::PARSER));
29  mInfeasibleSubsets.push_back({formula});
30  return false;
31  }
32  if(Settings::mode != Mode::INCREMENTAL_CONSTRAINTS) {
33  return mInfeasibleSubsets.empty();
34  }
35  if (formula.type() == carl::FormulaType::CONSTRAINT) {
36  /// Normalize the left hand side of the constraint and turn the relation accordingly
37  auto constr = subtropical::normalize(formula.constraint().constr());
38 
39  /// Store the normalized constraint and mark the separator object as changed
40  SeparatorGroup& separator{mSeparators.emplace(constr.lhs(), constr.lhs()).first->second};
41  separator.mRelations.insert(constr.relation());
42  mChangedSeparators.insert(&separator);
43 
44  /// Check if the asserted constraint affects the amount of equations
45  if(!separator.mEquationInduced){
46  if(separator.mRelations.count(carl::Relation::GEQ) * separator.mRelations.count(carl::Relation::LEQ)
47  + separator.mRelations.count(carl::Relation::EQ) > 0){
48  separator.mEquationInduced = true;
49  ++mRelationalConflicts;
50  }
51  }
52 
53  /// Check if the asserted relation trivially conflicts with other asserted relations
54  switch (constr.relation()) {
55  case carl::Relation::EQ:
56  if (separator.mRelations.count(carl::Relation::NEQ))
57  mInfeasibleSubsets.push_back({
58  FormulaT(constr.lhs(), carl::Relation::EQ),
59  FormulaT(constr.lhs(), carl::Relation::NEQ)
60  });
61  if (separator.mRelations.count(carl::Relation::LESS))
62  mInfeasibleSubsets.push_back({
63  FormulaT(constr.lhs(), carl::Relation::EQ),
64  FormulaT(constr.lhs(), carl::Relation::LESS)
65  });
66  if (separator.mRelations.count(carl::Relation::GREATER))
67  mInfeasibleSubsets.push_back({
68  FormulaT(constr.lhs(), carl::Relation::EQ),
69  FormulaT(constr.lhs(), carl::Relation::GREATER)
70  });
71  break;
72  case carl::Relation::NEQ:
73  if (separator.mRelations.count(carl::Relation::EQ))
74  mInfeasibleSubsets.push_back({
75  FormulaT(constr.lhs(), carl::Relation::NEQ),
76  FormulaT(constr.lhs(), carl::Relation::EQ)
77  });
78  break;
79  case carl::Relation::LESS:
80  if (separator.mRelations.count(carl::Relation::EQ))
81  mInfeasibleSubsets.push_back({
82  FormulaT(constr.lhs(), carl::Relation::LESS),
83  FormulaT(constr.lhs(), carl::Relation::EQ)
84  });
85  if (separator.mRelations.count(carl::Relation::GEQ))
86  mInfeasibleSubsets.push_back({
87  FormulaT(constr.lhs(), carl::Relation::LESS),
88  FormulaT(constr.lhs(), carl::Relation::GEQ)
89  });
90  [[fallthrough]];
91  case carl::Relation::LEQ:
92  if (separator.mRelations.count(carl::Relation::GREATER))
93  mInfeasibleSubsets.push_back({
94  FormulaT(constr.lhs(), constr.relation()),
95  FormulaT(constr.lhs(), carl::Relation::GREATER)
96  });
97  break;
98  case carl::Relation::GREATER:
99  if (separator.mRelations.count(carl::Relation::EQ))
100  mInfeasibleSubsets.push_back({
101  FormulaT(constr.lhs(), carl::Relation::GREATER),
102  FormulaT(constr.lhs(), carl::Relation::EQ)
103  });
104  if (separator.mRelations.count(carl::Relation::LEQ))
105  mInfeasibleSubsets.push_back({
106  FormulaT(constr.lhs(), carl::Relation::GREATER),
107  FormulaT(constr.lhs(), carl::Relation::LEQ)
108  });
109  [[fallthrough]];
110  case carl::Relation::GEQ:
111  if (separator.mRelations.count(carl::Relation::LESS))
112  mInfeasibleSubsets.push_back({
113  FormulaT(constr.lhs(), constr.relation()),
114  FormulaT(constr.lhs(), carl::Relation::LESS)
115  });
116  break;
117  default:
118  assert(false);
119  }
120  }
121  if (mInfeasibleSubsets.empty()) {
122  SMTRAT_STATISTICS_CALL(mStatistics.answer_by(STropModuleStatistics::AnswerBy::TRIVIAL_UNSAT));
123  }
124  return mInfeasibleSubsets.empty();
125 }
126 
127 template<class Settings>
128 void STropModule<Settings>::removeCore(ModuleInput::const_iterator _subformula) {
129  if(Settings::mode != Mode::INCREMENTAL_CONSTRAINTS){
130  return;
131  }
132  const FormulaT& formula = _subformula->formula();
133  if (formula.type() == carl::FormulaType::CONSTRAINT) {
134  /// Normalize the left hand side of the constraint and turn the relation accordingly
135  auto constr = subtropical::normalize(formula.constraint().constr());
136 
137  /// Retrieve the normalized constraint and mark the separator object as changed
138  SeparatorGroup& separator{mSeparators.at(constr.lhs())};
139  separator.mRelations.erase(constr.relation());
140  mChangedSeparators.insert(&separator);
141 
142  /// Check if the removed constraint affects the amount of equations
143  if(separator.mEquationInduced){
144  if(separator.mRelations.count(carl::Relation::GEQ) * separator.mRelations.count(carl::Relation::LEQ)
145  + separator.mRelations.count(carl::Relation::EQ) == 0){
146  separator.mEquationInduced = false;
147  --mRelationalConflicts;
148  }
149  }
150  }
151 }
152 
153 template<class Settings>
154 void STropModule<Settings>::updateModel() const {
155  if(Settings::mode == Mode::TRANSFORM_EQUATION || mSolverState != Answer::SAT) {
156  return;
157  }
158  if (!mModelComputed) {
159  if (mCheckedWithBackends) {
160  clearModel();
161  getBackendsModel();
162  excludeNotReceivedVariablesFromModel();
163  } else {
164  clearModel();
165  mModel = mEncoding.construct_assignment(mLRAModule.model(), FormulaT(rReceivedFormula()));
166  }
167  mModelComputed = true;
168  }
169 }
170 
171 template<class Settings>
172 Answer STropModule<Settings>::checkCore() {
173  SMTRAT_TIME_START(theoryStart);
174  // Report unsatisfiability if the already found conflicts are still unresolved
175  if (!mInfeasibleSubsets.empty()) {
176  SMTRAT_TIME_FINISH(mStatistics.theory_timer(), theoryStart);
177  SMTRAT_STATISTICS_CALL(mStatistics.answer_by(STropModuleStatistics::AnswerBy::TRIVIAL_UNSAT));
178  if (Settings::output_only) {
179  SMTRAT_VALIDATION_ADD("smtrat.subtropical", "transformation", FormulaT(carl::FormulaType::FALSE), true);
180  }
181  return Answer::UNSAT;
182  }
183 
184  if constexpr(Settings::mode == Mode::INCREMENTAL_CONSTRAINTS) {
185  assert(!Settings::output_only);
186  // Predicate that decides if the given conflict is a subset of the asserted constraints
187  const auto hasConflict = [&](const Conflict& conflict) {
188  return std::all_of(
189  conflict.begin(),
190  conflict.end(),
191  [&](const auto& conflictEntry) {
192  return ((conflictEntry.second == subtropical::Direction::NEGATIVE
193  || conflictEntry.second == subtropical::Direction::BOTH)
194  && (conflictEntry.first->mRelations.count(carl::Relation::LESS)
195  || conflictEntry.first->mRelations.count(carl::Relation::LEQ)))
196  || ((conflictEntry.second == subtropical::Direction::POSITIVE
197  || conflictEntry.second == subtropical::Direction::BOTH)
198  && (conflictEntry.first->mRelations.count(carl::Relation::GREATER)
199  || conflictEntry.first->mRelations.count(carl::Relation::GEQ)))
200  || (conflictEntry.second == subtropical::Direction::BOTH
201  && conflictEntry.first->mRelations.count(carl::Relation::NEQ));
202  }
203  );
204  };
205 
206  // Apply the method only if the asserted formula is not trivially undecidable
207  if (!mRelationalConflicts
208  && rReceivedFormula().is_constraint_conjunction()
209  && std::none_of(mLinearizationConflicts.begin(), mLinearizationConflicts.end(), hasConflict)) {
210  // Update the linearization of all changed separators
211  for (SeparatorGroup *separatorPtr : mChangedSeparators) {
212  SeparatorGroup& separator{*separatorPtr};
213 
214  // Determine the direction that shall be active
215  std::optional<subtropical::Direction> direction;
216  if (!separator.mRelations.empty()) {
217  if (separator.mActiveDirection
218  && *separator.mActiveDirection == subtropical::Direction::NEGATIVE
219  && ((separator.mRelations.count(carl::Relation::LESS)
220  || separator.mRelations.count(carl::Relation::LEQ)))) {
221  direction = subtropical::Direction::NEGATIVE;
222  } else if (separator.mActiveDirection
223  && *separator.mActiveDirection == subtropical::Direction::POSITIVE
224  && ((separator.mRelations.count(carl::Relation::GREATER)
225  || separator.mRelations.count(carl::Relation::GEQ)))) {
226  direction = subtropical::Direction::POSITIVE;
227  } else {
228  direction = subtropical::direction(*separator.mRelations.rbegin());
229  }
230  }
231 
232  // Update the linearization if the direction has changed
233  if (separator.mActiveDirection != direction) {
234  if (separator.mActiveDirection) {
235  remove_lra_formula(separator.mActiveFormula);
236  separator.mActiveFormula = FormulaT(carl::FormulaType::FALSE);
237  }
238  separator.mActiveDirection = direction;
239  if (separator.mActiveDirection) {
240  separator.mActiveFormula = mEncoding.encode_separator(separator.mSeparator, *separator.mActiveDirection, Settings::separatorType);
241  add_lra_formula(separator.mActiveFormula);
242  }
243  }
244  }
245  mChangedSeparators.clear();
246 
247  // Restrict the normal vector component of integral variables to positive values
248  std::set<carl::Variable> toErase;
249  std::transform(mActiveIntegerFormulas.begin(), mActiveIntegerFormulas.end(), std::inserter(toErase, toErase.end()), [](auto pair){ return pair.first; });
250  for (auto& variable : carl::variables(FormulaT(rReceivedFormula()))) {
251  toErase.erase(variable);
252  if (variable.type() == carl::VariableType::VT_INT && mActiveIntegerFormulas.find(variable) == mActiveIntegerFormulas.end()) {
253  mActiveIntegerFormulas[variable] = mEncoding.encode_integer(variable);
254  add_lra_formula(mActiveIntegerFormulas[variable]);
255  }
256  }
257  for (const auto& variable : toErase) {
258  remove_lra_formula(mActiveIntegerFormulas[variable]);
259  mActiveIntegerFormulas.erase(variable);
260  }
261 
262  // Check the constructed linearization with the LRA solver
263  SMTRAT_STATISTICS_CALL(mStatistics.transformation_applicable());
264  if (mLRAModule.check(true) == Answer::SAT) {
265  SMTRAT_TIME_FINISH(mStatistics.theory_timer(), theoryStart);
266  SMTRAT_STATISTICS_CALL(mStatistics.answer_by(STropModuleStatistics::AnswerBy::METHOD));
267  mCheckedWithBackends = false;
268  return Answer::SAT;
269  } else {
270  /// Learn the conflicting set of separators to avoid its recheck in the future
271  for (const FormulaSetT& lra_conflict : mLRAModule.infeasibleSubsets()) {
272  carl::carlVariables variables;
273  for (const FormulaT& formula : lra_conflict)
274  carl::variables(formula, variables);
275  Conflict conflict;
276  for (const auto& separatorsEntry : mSeparators) {
277  const SeparatorGroup& separator{separatorsEntry.second};
278  if (separator.mActiveDirection
279  && variables.has(separator.mSeparator.bias))
280  conflict.emplace_back(&separator, *separator.mActiveDirection);
281  }
282  mLinearizationConflicts.emplace_back(std::move(conflict));
283  }
284  }
285  }
286  } else if constexpr(Settings::mode == Mode::TRANSFORM_EQUATION) {
287  SMTRAT_TIME_START(transformationStart);
288  FormulaT negationFreeFormula = carl::to_nnf(FormulaT(rReceivedFormula()));
289  if (negationFreeFormula.type() == carl::FormulaType::FALSE) {
290  SMTRAT_STATISTICS_CALL(mStatistics.answer_by(STropModuleStatistics::AnswerBy::PARSER));
291  std::set<FormulaT> infset;
292  for (const auto& f : rReceivedFormula()) {
293  infset.insert(f.formula());
294  }
295  mInfeasibleSubsets.push_back(infset);
296  if (Settings::output_only) {
297  SMTRAT_VALIDATION_ADD("smtrat.subtropical", "transformation", FormulaT(carl::FormulaType::FALSE), true);
298  }
299  return Answer::UNSAT;
300  } else if (negationFreeFormula.type() == carl::FormulaType::TRUE) {
301  SMTRAT_STATISTICS_CALL(mStatistics.answer_by(STropModuleStatistics::AnswerBy::PARSER));
302  if (Settings::output_only) {
303  SMTRAT_VALIDATION_ADD("smtrat.subtropical", "transformation", FormulaT(carl::FormulaType::TRUE), true);
304  }
305  return Answer::SAT;
306  }
307  FormulaT equation = subtropical::transform_to_equation(negationFreeFormula);
308  SMTRAT_TIME_FINISH(mStatistics.transformation_timer(), transformationStart);
309  if(equation.type() != carl::FormulaType::FALSE) {
310  subtropical::Separator separator(equation.constraint().lhs().normalize());
311  auto direction = subtropical::direction_for_equality(separator);
312  if(!direction) {
313  SMTRAT_TIME_FINISH(mStatistics.theory_timer(), theoryStart);
314  SMTRAT_STATISTICS_CALL(mStatistics.answer_by(STropModuleStatistics::AnswerBy::METHOD));
315  SMTRAT_STATISTICS_CALL(mStatistics.transformation_applicable());
316  mCheckedWithBackends = false;
317  if (Settings::output_only) {
318  SMTRAT_VALIDATION_ADD("smtrat.subtropical", "transformation", FormulaT(carl::FormulaType::TRUE), true);
319  }
320  return Answer::SAT;
321  } else {
322  SMTRAT_STATISTICS_CALL(mStatistics.transformation_applicable());
323  if (!Settings::output_only) {
324  mLRAModule.reset();
325  mLRAModule.add(mEncoding.encode_separator(separator, *direction, Settings::separatorType));
326  if (mLRAModule.check(true) == Answer::SAT) {
327  SMTRAT_TIME_FINISH(mStatistics.theory_timer(), theoryStart);
328  SMTRAT_STATISTICS_CALL(mStatistics.answer_by(STropModuleStatistics::AnswerBy::METHOD));
329  mCheckedWithBackends = false;
330  return Answer::SAT;
331  }
332  } else {
333  SMTRAT_VALIDATION_ADD("smtrat.subtropical", "transformation", mEncoding.encode_separator(separator, *direction, Settings::separatorType), true);
334  return Answer::UNKNOWN;
335  }
336  }
337  }
338  } else {
339  static_assert(Settings::mode == Mode::TRANSFORM_FORMULA || Settings::mode == Mode::TRANSFORM_FORMULA_ALT);
340  SMTRAT_TIME_START(transformationStart);
341  FormulaT negationFreeFormula = carl::to_nnf(FormulaT(rReceivedFormula()));
342  if (negationFreeFormula.type() == carl::FormulaType::FALSE) {
343  SMTRAT_STATISTICS_CALL(mStatistics.answer_by(STropModuleStatistics::AnswerBy::PARSER));
344  std::set<FormulaT> infset;
345  for (const auto& f : rReceivedFormula()) {
346  infset.insert(f.formula());
347  }
348  mInfeasibleSubsets.push_back(infset);
349  if (Settings::output_only) {
350  SMTRAT_VALIDATION_ADD("smtrat.subtropical", "transformation", FormulaT(carl::FormulaType::FALSE), true);
351  }
352  return Answer::UNSAT;
353  } else if (negationFreeFormula.type() == carl::FormulaType::TRUE) {
354  SMTRAT_STATISTICS_CALL(mStatistics.answer_by(STropModuleStatistics::AnswerBy::PARSER));
355  if (Settings::output_only) {
356  SMTRAT_VALIDATION_ADD("smtrat.subtropical", "transformation", FormulaT(carl::FormulaType::TRUE), true);
357  }
358  return Answer::SAT;
359  }
360  FormulaT translatedFormula = (Settings::mode == Mode::TRANSFORM_FORMULA) ? subtropical::encode_as_formula(negationFreeFormula, mEncoding, Settings::separatorType) : subtropical::encode_as_formula_alt(negationFreeFormula, mEncoding, Settings::separatorType);
361  SMTRAT_TIME_FINISH(mStatistics.transformation_timer(), transformationStart);
362  if(translatedFormula.type() != carl::FormulaType::FALSE){
363  SMTRAT_STATISTICS_CALL(mStatistics.transformation_applicable());
364  if (!Settings::output_only) {
365  mLRAModule.reset();
366  mLRAModule.add(translatedFormula);
367  if (mLRAModule.check(true) == Answer::SAT) {
368  SMTRAT_TIME_FINISH(mStatistics.theory_timer(), theoryStart);
369  SMTRAT_STATISTICS_CALL(mStatistics.answer_by(STropModuleStatistics::AnswerBy::METHOD));
370  mCheckedWithBackends = false;
371  return Answer::SAT;
372  }
373  } else {
374  SMTRAT_VALIDATION_ADD("smtrat.subtropical", "transformation", translatedFormula, true);
375  return Answer::UNKNOWN;
376  }
377  }
378  }
379 
380  // Check the asserted formula with the backends
381  if (Settings::output_only) {
382  SMTRAT_VALIDATION_ADD("smtrat.subtropical", "transformation", FormulaT(carl::FormulaType::FALSE), true);
383  return Answer::UNKNOWN;
384  } else {
385  SMTRAT_STATISTICS_CALL(mStatistics.failed());
386  mCheckedWithBackends = true;
387  Answer answer = runBackends();
388  SMTRAT_TIME_FINISH(mStatistics.theory_timer(), theoryStart);
389  SMTRAT_STATISTICS_CALL(mStatistics.answer_by(STropModuleStatistics::AnswerBy::BACKEND));
390  if (answer == Answer::UNSAT)
391  getInfeasibleSubsets();
392  return answer;
393  }
394 }
395 
396 template<class Settings>
397 inline void STropModule<Settings>::add_lra_formula(const FormulaT& formula) {
398  mLRAModule.add(formula);
399 }
400 
401 template<class Settings>
402 inline void STropModule<Settings>::remove_lra_formula(const FormulaT& formula) {
403  if (formula.type() == carl::FormulaType::AND) {
404  auto iter = mLRAModule.formulaBegin();
405  for (const auto& subformula : formula.subformulas()) {
406  iter = mLRAModule.remove(std::find(iter, mLRAModule.formulaEnd(), subformula));
407  }
408  }
409  else {
410  mLRAModule.remove(std::find(mLRAModule.formulaBegin(), mLRAModule.formulaEnd(), formula));
411  }
412 }
413 }