SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
ESModule.tpp
Go to the documentation of this file.
1 /**
2  * @file ESModule.tpp
3  * @author Florian Corzilius <corzilius@cs.rwth-aachen.de>
4  *
5  * @version 2015-09-09
6  * Created on 2015-09-09.
7  */
8 
9 #include "ESModule.h"
10 #include <smtrat-solver/Manager.h>
11 
12 #include <carl-arith/constraint/Substitution.h>
13 #include <carl-formula/formula/functions/Substitution.h>
14 #include <carl-arith/poly/umvpoly/functions/Bitsize.h>
15 
16 
17 namespace smtrat
18 {
19  template<class Settings>
20  ESModule<Settings>::ESModule( const ModuleInput* _formula, Conditionals& _conditionals, Manager* _manager ):
21  PModule( _formula, _conditionals, _manager, Settings::moduleName )
22  {}
23 
24  template<class Settings>
25  ESModule<Settings>::~ESModule()
26  {}
27 
28  template<class Settings>
29  void ESModule<Settings>::updateModel() const
30  {
31  clearModel();
32  if( solverState() == SAT || (solverState() != UNSAT && appliedPreprocessing()) )
33  {
34  getBackendsModel();
35  for( const auto& iter : mBoolSubs )
36  {
37  if( iter.first.type() == carl::FormulaType::BOOL )
38  {
39  assert( mModel.find( iter.first.boolean() ) == mModel.end() );
40  mModel.emplace( iter.first.boolean(), iter.second );
41  }
42  }
43  for( const auto& iter : mArithSubs )
44  {
45  assert( mModel.find( iter.first ) == mModel.end() );
46  mModel.emplace( iter.first, carl::createSubstitution<Rational,Poly,ModelPolynomialSubstitution>( iter.second ) );
47  }
48  // All variables which occur in the root of the constructed state tree but were incidentally eliminated
49  // (during the elimination of another variable) can have an arbitrary assignment. If the variable has the
50  // real domain, we leave at as a parameter, and, if it has the integer domain we assign 0 to it.
51  carl::carlVariables _receivedVars;
52  rReceivedFormula().gatherVariables(_receivedVars);
53  auto receivedVars = _receivedVars.as_set();
54  if( solverState() != SAT && appliedPreprocessing() )
55  {
56  carl::carlVariables passedVars;
57  rPassedFormula().gatherVariables(passedVars);
58  auto rvIter = receivedVars.begin();
59  auto pvIter = passedVars.begin();
60  while( rvIter != receivedVars.end() && pvIter != passedVars.end() )
61  {
62  if( *rvIter < *pvIter )
63  ++rvIter;
64  else if( *pvIter < *rvIter )
65  ++pvIter;
66  else
67  {
68  rvIter = receivedVars.erase( rvIter );
69  ++pvIter;
70  }
71  }
72  }
73  for( auto var : receivedVars )
74  {
75  if( var.type() == carl::VariableType::VT_BOOL )
76  mModel.insert(std::make_pair(var, false));
77  else
78  mModel.insert(std::make_pair(var, carl::createSubstitution<Rational,Poly,ModelPolynomialSubstitution>(Poly())));
79  }
80  }
81  }
82 
83  template<class Settings>
84  Answer ESModule<Settings>::checkCore()
85  {
86  mBoolSubs.clear();
87  mArithSubs.clear();
88  FormulaT formula = elimSubstitutions( (FormulaT) rReceivedFormula(), true, true );
89  Answer ans = SAT;
90  if( formula.is_false() )
91  ans = UNSAT;
92  else
93  {
94  addSubformulaToPassedFormula( formula );
95  ans = runBackends();
96  }
97  if( ans == UNSAT )
98  generateTrivialInfeasibleSubset(); // TODO: compute a better infeasible subset
99  return ans;
100  }
101 
102  template<typename Settings>
103  FormulaT ESModule<Settings>::elimSubstitutions( const FormulaT& _formula, bool _elimSubstitutions, bool _outermost )
104  {
105 
106  auto iter = mBoolSubs.find( _formula );
107  if( iter != mBoolSubs.end() )
108  {
109  SMTRAT_LOG_DEBUG("smtrat.es", _formula << " ----> " << (iter->second ? FormulaT( carl::FormulaType::TRUE ) : FormulaT( carl::FormulaType::FALSE )));
110  return iter->second ? FormulaT( carl::FormulaType::TRUE ) : FormulaT( carl::FormulaType::FALSE );
111  }
112  FormulaT result = _formula;
113  switch( _formula.type() )
114  {
115  case carl::FormulaType::AND:
116  {
117  std::vector<std::map<carl::Variable,Poly>::const_iterator> addedArithSubs;
118  std::unordered_map<FormulaT,std::unordered_map<FormulaT, bool>::const_iterator> foundBooleanSubstitutions;
119  bool foundNewSubstitution = true;
120  // we use sets, as we want the sub-formulas to be sorted according to their IDs
121  // a formula has always a greater id than its formulas (and, hence, their sub-formulas etc)
122  // then, for instance, for (and b (or a b)) we would first see that b->true and afterwards
123  // replace b for true in (or a b) as it has a higher ID
124  FormulaSetT foundSubstitutions;
125  FormulaSetT currentSubformulas;
126  for( const FormulaT& subf : result.subformulas() )
127  currentSubformulas.insert( currentSubformulas.end(), subf ); // as sub-formulas are already sorted use hint
128  while( foundNewSubstitution )
129  {
130  FormulaSetT sfs;
131  foundNewSubstitution = false;
132  // Process all equations first.
133  for( const auto& sf : currentSubformulas )
134  {
135  if( sf.type() == carl::FormulaType::CONSTRAINT && sf.constraint().relation() == carl::Relation::EQ )
136  {
137  FormulaT tmp = elimSubstitutions( sf );
138  if( tmp.type() == carl::FormulaType::FALSE )
139  {
140  result = tmp;
141  goto Return;
142  }
143  else if( tmp.type() != carl::FormulaType::TRUE )
144  {
145  auto subs = carl::get_substitution(tmp.constraint(), false, objective());
146  if( subs && (Settings::substitution_bitsize_limit == 0 || carl::bitsize(subs->second) <= Settings::substitution_bitsize_limit))
147  {
148  if (subs->first != objective()) {
149  SMTRAT_LOG_INFO("smtrat.es", "found substitution [" << subs->first << " -> " << subs->second << "]");
150  assert( mArithSubs.find( subs->first ) == mArithSubs.end() );
151  addedArithSubs.push_back( mArithSubs.emplace( subs->first, subs->second ).first );
152  foundSubstitutions.insert( tmp );
153  foundNewSubstitution = true;
154  }
155  }
156  else
157  {
158  sfs.insert( sfs.end(), tmp );
159  }
160  }
161  }
162  }
163  // Now the other sub-formulas.
164  for( const auto& sf : currentSubformulas )
165  {
166  if( sf.type() != carl::FormulaType::CONSTRAINT || sf.constraint().relation() != carl::Relation::EQ || !sf.constraint().lhs().is_linear() )
167  {
168  auto iterC = foundBooleanSubstitutions.find( sf );
169  if( iterC != foundBooleanSubstitutions.end() )
170  {
171  mBoolSubs.erase( iterC->second );
172  foundBooleanSubstitutions.erase( iterC );
173  }
174  FormulaT sfSimplified = elimSubstitutions( sf );
175  if( sfSimplified.is_false() )
176  {
177  result = sfSimplified;
178  goto Return;
179  }
180  else if( !sfSimplified.is_true() )
181  {
182  if( sf != sfSimplified )
183  {
184  foundNewSubstitution = true;
185  if( sfSimplified.type() == carl::FormulaType::AND )
186  sfs.insert( sfSimplified.subformulas().begin(), sfSimplified.subformulas().end() );
187  else
188  sfs.insert( sfs.end(), sfSimplified );
189  }
190  else
191  {
192  if( !(_outermost && sfSimplified.is_literal() && sfSimplified.is_only_propositional()) )
193  sfs.insert( sfs.end(), sfSimplified );
194  if( sfSimplified.type() == carl::FormulaType::NOT )
195  {
196  SMTRAT_LOG_TRACE("smtrat.es", "found boolean substitution [" << sfSimplified.subformula() << " -> false]");
197  assert( mBoolSubs.find( sfSimplified.subformula() ) == mBoolSubs.end() );
198  assert( foundBooleanSubstitutions.find( sfSimplified ) == foundBooleanSubstitutions.end() );
199  foundBooleanSubstitutions.emplace( sfSimplified, mBoolSubs.insert( std::make_pair( sfSimplified.subformula(), false ) ).first );
200  }
201  else
202  {
203  SMTRAT_LOG_TRACE("smtrat.es", "found boolean substitution [" << sfSimplified << " -> true]");
204  assert( mBoolSubs.find( sfSimplified ) == mBoolSubs.end() );
205  assert( foundBooleanSubstitutions.find( sfSimplified ) == foundBooleanSubstitutions.end() );
206  foundBooleanSubstitutions.emplace( sfSimplified, mBoolSubs.insert( std::make_pair( sfSimplified, true ) ).first );
207  }
208  }
209  }
210  }
211  }
212  currentSubformulas = std::move(sfs);
213  }
214  if( currentSubformulas.empty() )
215  {
216  if( !_elimSubstitutions && !foundSubstitutions.empty() )
217  result = FormulaT( carl::FormulaType::AND, std::move(foundSubstitutions) );
218  else
219  result = FormulaT( carl::FormulaType::TRUE );
220  assert(!_elimSubstitutions || result == FormulaT( carl::FormulaType::TRUE ));
221  }
222  else
223  {
224  if( !_elimSubstitutions )
225  currentSubformulas.insert( foundSubstitutions.begin(), foundSubstitutions.end() );
226  result = FormulaT( carl::FormulaType::AND, std::move(currentSubformulas) );
227  }
228  Return:
229  if( !_outermost )
230  {
231  while( !addedArithSubs.empty() )
232  {
233  assert( std::count( addedArithSubs.begin(), addedArithSubs.end(), addedArithSubs.back() ) == 1 );
234  mArithSubs.erase( addedArithSubs.back() );
235  addedArithSubs.pop_back();
236  }
237  while( !foundBooleanSubstitutions.empty() )
238  {
239  mBoolSubs.erase( foundBooleanSubstitutions.begin()->second );
240  foundBooleanSubstitutions.erase( foundBooleanSubstitutions.begin() );
241  }
242  }
243  break;
244  }
245  case carl::FormulaType::ITE:
246  {
247  FormulaT cond = elimSubstitutions( _formula.condition() );
248  if( cond.type() == carl::FormulaType::CONSTRAINT )
249  {
250  auto subs = carl::get_substitution(cond.constraint(), false);
251  if( subs && (Settings::substitution_bitsize_limit == 0 || carl::bitsize(subs->second) <= Settings::substitution_bitsize_limit))
252  {
253  SMTRAT_LOG_DEBUG("smtrat.es", __LINE__ << " found substitution [" << subs->first << " -> " << subs->second << "]" );
254  auto addedBoolSub = cond.type() == carl::FormulaType::NOT ? mBoolSubs.emplace( cond.subformula(), false ) : mBoolSubs.emplace( cond, true );
255  SMTRAT_LOG_DEBUG("smtrat.es", __LINE__ << " found boolean substitution [" << addedBoolSub.first->first << " -> " << (addedBoolSub.first->second ? "true" : "false") << "]");
256  assert( addedBoolSub.second );
257  auto iterB = mArithSubs.emplace( subs->first, subs->second ).first;
258  FormulaT firstCaseTmp = elimSubstitutions( _formula.first_case() );
259  mArithSubs.erase( iterB );
260  mBoolSubs.erase( addedBoolSub.first );
261  addedBoolSub = cond.type() == carl::FormulaType::NOT ? mBoolSubs.emplace( cond.subformula(), true ) : mBoolSubs.emplace( cond, false );
262  SMTRAT_LOG_DEBUG("smtrat.es", __LINE__ << " found boolean substitution [" << addedBoolSub.first->first << " -> " << (addedBoolSub.first->second ? "true" : "false") << "]" );
263  assert( addedBoolSub.second );
264  FormulaT secondCaseTmp = elimSubstitutions( _formula.second_case() );
265  mBoolSubs.erase( addedBoolSub.first );
266  result = FormulaT( carl::FormulaType::ITE, {cond, firstCaseTmp, secondCaseTmp} );
267  break;
268  }
269  else
270  {
271  subs = carl::get_substitution(cond.constraint(), true);
272  if( subs && (Settings::substitution_bitsize_limit == 0 || carl::bitsize(subs->second) <= Settings::substitution_bitsize_limit))
273  {
274  SMTRAT_LOG_DEBUG("smtrat.es", __LINE__ << " found substitution [" << subs->first << " -> " << subs->second << "]" );
275  auto addedBoolSub = cond.type() == carl::FormulaType::NOT ? mBoolSubs.emplace( cond.subformula(), false ) : mBoolSubs.emplace( cond, true );
276  SMTRAT_LOG_DEBUG("smtrat.es", __LINE__ << " found boolean substitution [" << addedBoolSub.first->first << " -> " << (addedBoolSub.first->second ? "true" : "false") << "]" );
277  assert( addedBoolSub.second );
278  FormulaT firstCaseTmp = elimSubstitutions( _formula.first_case() );
279  mBoolSubs.erase( addedBoolSub.first );
280  addedBoolSub = cond.type() == carl::FormulaType::NOT ? mBoolSubs.emplace( cond.subformula(), true ) : mBoolSubs.emplace( cond, false );
281  SMTRAT_LOG_DEBUG("smtrat.es", __LINE__ << " found boolean substitution [" << addedBoolSub.first->first << " -> " << (addedBoolSub.first->second ? "true" : "false") << "]" );
282  assert( addedBoolSub.second );
283  auto iterB = mArithSubs.emplace( subs->first, subs->second ).first;
284  FormulaT secondCaseTmp = elimSubstitutions( _formula.second_case() );
285  mArithSubs.erase( iterB );
286  mBoolSubs.erase( addedBoolSub.first );
287  result = FormulaT( carl::FormulaType::ITE, {cond, firstCaseTmp, secondCaseTmp} );
288  break;
289  }
290  }
291  }
292  if( cond.is_true() )
293  {
294  result = elimSubstitutions( _formula.first_case() );
295  }
296  else if( cond.is_false() )
297  {
298  result = elimSubstitutions( _formula.second_case() );
299  }
300  else
301  {
302  auto addedBoolSub = cond.type() == carl::FormulaType::NOT ? mBoolSubs.emplace( cond.subformula(), false ) : mBoolSubs.emplace( cond, true );
303  SMTRAT_LOG_DEBUG("smtrat.es", __LINE__ << " found boolean substitution [" << addedBoolSub.first->first << " -> " << (addedBoolSub.first->second ? "true" : "false") << "]");
304  assert( addedBoolSub.second );
305  FormulaT firstCaseTmp = elimSubstitutions( _formula.first_case() );
306  mBoolSubs.erase( addedBoolSub.first );
307  addedBoolSub = cond.type() == carl::FormulaType::NOT ? mBoolSubs.emplace( cond.subformula(), true ) : mBoolSubs.emplace( cond, false );
308  SMTRAT_LOG_DEBUG("smtrat.es", __LINE__ << " found boolean substitution [" << addedBoolSub.first->first << " -> " << (addedBoolSub.first->second ? "true" : "false") << "]");
309  assert( addedBoolSub.second );
310  FormulaT secondCaseTmp = elimSubstitutions( _formula.second_case() );
311  mBoolSubs.erase( addedBoolSub.first );
312  result = FormulaT( carl::FormulaType::ITE, {cond, firstCaseTmp, secondCaseTmp} );
313  }
314  break;
315  }
316  case carl::FormulaType::OR:
317  case carl::FormulaType::IFF:
318  case carl::FormulaType::XOR: {
319  FormulasT newSubformulas;
320  bool changed = false;
321  for (const auto& cur: _formula.subformulas()) {
322  FormulaT newCur = elimSubstitutions(cur);
323  if (newCur != cur) changed = true;
324  newSubformulas.push_back(newCur);
325  }
326  if (changed)
327  result = FormulaT(_formula.type(), std::move(newSubformulas));
328  break;
329  }
330  case carl::FormulaType::NOT: {
331  FormulaT cur = elimSubstitutions(_formula.subformula());
332  if (cur != _formula.subformula())
333  result = FormulaT(carl::FormulaType::NOT, cur);
334  break;
335  }
336  case carl::FormulaType::IMPLIES: {
337  FormulaT prem = elimSubstitutions(_formula.premise());
338  FormulaT conc = elimSubstitutions(_formula.conclusion());
339  if ((prem != _formula.premise()) || (conc != _formula.conclusion()))
340  result = FormulaT(carl::FormulaType::IMPLIES, {prem, conc});
341  break;
342  }
343  case carl::FormulaType::CONSTRAINT: {
344  FormulaT tmp = result;
345  while( result != (tmp = carl::substitute(tmp, mArithSubs)) )
346  result = tmp;
347  break;
348  }
349  case carl::FormulaType::BOOL:
350  case carl::FormulaType::BITVECTOR:
351  case carl::FormulaType::UEQ:
352  case carl::FormulaType::TRUE:
353  case carl::FormulaType::FALSE:
354  if (_formula != result) {
355  SMTRAT_LOG_DEBUG("smtrat.es", _formula << " ----> " << result);
356  }
357  return result;
358  case carl::FormulaType::EXISTS:
359  case carl::FormulaType::FORALL: {
360  FormulaT sub = elimSubstitutions(_formula.quantified_formula());
361  if (sub != _formula.quantified_formula())
362  result = FormulaT(_formula.type(), _formula.quantified_variables(), sub);
363  }
364  default: {}
365  }
366  if (!_outermost) {
367  iter = mBoolSubs.find( result );
368  if( iter != mBoolSubs.end() )
369  {
370  SMTRAT_LOG_DEBUG("smtrat.es", _formula << " ----> " << (iter->second ? FormulaT( carl::FormulaType::TRUE ) : FormulaT( carl::FormulaType::FALSE )));
371  return iter->second ? FormulaT( carl::FormulaType::TRUE ) : FormulaT( carl::FormulaType::FALSE );
372  }
373  }
374  if (_formula != result) {
375  SMTRAT_LOG_DEBUG("smtrat.es", _formula << " ----> " << result);
376  }
377  return result;
378  }
379 }
380 
381