SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
BVModule.tpp
Go to the documentation of this file.
1 /*
2  * SMT-RAT - Satisfiability-Modulo-Theories Real Algebra Toolbox
3  * Copyright (C) 2012 Florian Corzilius, Ulrich Loup, Erika Abraham, Sebastian Junges
4  *
5  * This file is part of SMT-RAT.
6  *
7  * SMT-RAT is free software: you can redistribute it and/or modify
8  * it under the terms of the GNU General Public License as published by
9  * the Free Software Foundation, either version 3 of the License, or
10  * (at your option) any later version.
11  *
12  * SMT-RAT is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with SMT-RAT. If not, see <http://www.gnu.org/licenses/>.
19  *
20  */
21 /**
22  * @file BVModule.tpp
23  * @author Andreas Krueger <andreas.krueger@rwth-aachen.de>
24  * @author Florian Corzilius <corzilius@cs.rwth-aachen.de>
25  *
26  * @version 2015-02-05
27  * Created on 2015-02-05.
28  */
29 
30 #include "BVModule.h"
31 #include <limits>
32 
33 #include <carl-formula/model/Assignment.h>
34 #include <carl-formula/formula/functions/Complexity.h>
35 
36 //#define DEBUG_BVMODULE
37 
38 namespace smtrat
39 {
40  /**
41  * Constructors.
42  */
43 
44  template<class Settings>
45  BVModule<Settings>::BVModule( const ModuleInput* _formula, Conditionals& _conditionals, Manager* _manager ):
46  Module( _formula, _conditionals, _manager ),
47  mModelComputed( true ),
48  mEncoder(),
49  mBlastedFormulas(),
50  mPositionInFormulasToBlast(),
51  mFormulasToBlast()
52  {}
53 
54  /**
55  * Destructor.
56  */
57 
58  template<class Settings>
59  BVModule<Settings>::~BVModule()
60  {}
61 
62 
63  template<class Settings>
64  bool BVModule<Settings>::informCore( const FormulaT& /* _constraint */ )
65  {
66  return true;
67  }
68 
69  template<class Settings>
70  void BVModule<Settings>::init()
71  {}
72 
73  template<class Settings>
74  bool BVModule<Settings>::addCore( ModuleInput::const_iterator _subformula )
75  {
76  if( _subformula->formula().is_true() )
77  return true;
78  mModelComputed = false;
79  if( _subformula->formula().is_false() )
80  {
81  receivedFormulasAsInfeasibleSubset( _subformula );
82  return false;
83  }
84  if( Settings::incremental_flattening )
85  {
86  auto sortKey = std::make_pair( evaluateBVFormula(_subformula->formula()), _subformula->formula().id() );
87  #ifdef DEBUG_BVMODULE
88  std::cout << std::endl << std::endl << "add formula" << std::endl;
89  std::cout << _subformula->formula() << std::endl;
90  std::cout << "Evaluation: " << sortKey << std::endl;
91  #endif
92  auto ret = mFormulasToBlast.insert( std::make_pair(sortKey, _subformula->formula() ) );
93  assert( ret.second );
94  assert( mPositionInFormulasToBlast.find( _subformula->formula() ) == mPositionInFormulasToBlast.end() );
95  mPositionInFormulasToBlast[_subformula->formula()] = ret.first;
96  }
97  return true;
98  }
99 
100  template<class Settings>
101  void BVModule<Settings>::removeCore( ModuleInput::const_iterator _subformula )
102  {
103  if( Settings::incremental_flattening )
104  {
105  auto iterA = mBlastedFormulas.find( _subformula->formula() );
106  if( iterA != mBlastedFormulas.end() )
107  {
108  #ifdef DEBUG_BVMODULE
109  std::cout << std::endl << std::endl << "remove formula" << std::endl;
110  std::cout << _subformula->formula() << std::endl;
111  #endif
112  mBlastedFormulas.erase( iterA );
113  }
114  else
115  {
116  #ifdef DEBUG_BVMODULE
117  std::cout << std::endl << std::endl << "remove formula" << std::endl;
118  std::cout << _subformula->formula() << std::endl;
119  #endif
120  auto iterB = mPositionInFormulasToBlast.find( _subformula->formula() );
121  assert( iterB != mPositionInFormulasToBlast.end() );
122  mFormulasToBlast.erase( iterB->second );
123  mPositionInFormulasToBlast.erase( iterB );
124  }
125  }
126  }
127 
128  template<class Settings>
129  void BVModule<Settings>::updateModel() const
130  {
131  if( solverState() != SAT )
132  return;
133  if( !Settings::incremental_flattening || !mModelComputed )
134  {
135  transferBackendModel();
136  }
137  if( Settings::incremental_flattening && !mModelComputed )
138  mModelComputed = true;
139  }
140 
141 
142  template<class Settings>
143  void BVModule<Settings>::transferBackendModel() const
144  {
145  clearModel();
146  const Model& bModel = backendsModel();
147  // Build bitvector values from the values of the single bits
148  auto& blastings = mEncoder.bitvectorBlastings();
149 
150  for(auto const & bitvectorToBits : blastings)
151  {
152  carl::BVValue composedValue(bitvectorToBits.first.width());
153 
154  for(std::size_t i=0;i<bitvectorToBits.second.size();++i)
155  {
156  auto iter = bModel.find( bitvectorToBits.second[i] );
157  assert( iter != bModel.end() );
158  composedValue[i] = iter->second.asBool();
159  }
160  mModel.emplace(bitvectorToBits.first, composedValue);
161  }
162  if( rReceivedFormula().containsBooleanVariables() )
163  {
164  carl::carlVariables bvars;
165  rReceivedFormula().gatherVariables(bvars);
166  auto modelIter = mModel.begin();
167  for( carl::Variable var : bvars )
168  {
169  if (var.type() != carl::VariableType::VT_BOOL) continue;
170  auto bmodelIter = bModel.find( var );
171  assert( bmodelIter != bModel.end() );
172  modelIter = mModel.emplace_hint( modelIter, var, bmodelIter->second.asBool() );
173  }
174  }
175  getDefaultModel( mModel, (FormulaT) rReceivedFormula() );
176  }
177 
178  template<class Settings>
179  Answer BVModule<Settings>::checkCore()
180  {
181  if( Settings::incremental_flattening )
182  {
183  #ifdef DEBUG_BVMODULE
184  std::cout << "Check in BVModule" << std::endl;
185  #endif
186  getDefaultModel( mModel, (FormulaT) rReceivedFormula() );
187  #ifdef DEBUG_BVMODULE
188  std::cout << "initial model:" << std::endl;
189  std::cout << mModel << std::endl << std::endl;
190  #endif
191  if( !mFormulasToBlast.empty() )
192  {
193  FormulaT origin = mFormulasToBlast.begin()->second;
194  #ifdef DEBUG_BVMODULE
195  std::cout << std::endl << std::endl << "Take into account: " << std::endl;
196  std::cout << origin << std::endl;
197  #endif
198  const FormulaSetT& formulasToPass = mEncoder.encode( origin );
199  mFormulasToBlast.erase( mFormulasToBlast.begin() );
200  for( const FormulaT& formulaToPass : formulasToPass )
201  addSubformulaToPassedFormula( formulaToPass, origin );
202  }
203  while( true )
204  {
205  #ifdef DEBUG_BVMODULE
206  std::cout << std::endl << "Run backends" << std::endl;
207  #endif
208  Answer backendAnswer = runBackends();
209  #ifdef DEBUG_BVMODULE
210  std::cout << " --> " << backendAnswer << std::endl << std::endl;
211  #endif
212  switch( backendAnswer )
213  {
214  case UNSAT:
215  {
216  getInfeasibleSubsets();
217  return UNSAT;
218  }
219  case SAT:
220  {
221  transferBackendModel();
222  const Model& currentModel = model();
223  #ifdef DEBUG_BVMODULE
224  std::cout << "current model: " << std::endl;
225  std::cout << currentModel << std::endl;
226  #endif
227  auto iter = mFormulasToBlast.begin();
228  for( ; iter != mFormulasToBlast.end(); ++iter )
229  {
230  unsigned tmp = satisfies( currentModel, iter->second );
231  #ifdef DEBUG_BVMODULE
232  std::cout << "currentModel satisfies" << std::endl << iter->second << std::endl << " -> " << tmp << std::endl;
233  #endif
234  assert( tmp != 2 );
235  if( tmp == 0 )
236  {
237  #ifdef DEBUG_BVMODULE
238  std::cout << std::endl << std::endl << "Not yet satisfied: " << std::endl;
239  std::cout << iter->second << std::endl;
240  #endif
241  break;
242  }
243  }
244  if( iter == mFormulasToBlast.end() )
245  {
246  #ifdef DEBUG_BVMODULE
247  std::cout << "All formulas satisfied!" << std::endl;
248  #endif
249  mModelComputed = true;
250  return SAT;
251  }
252  else
253  {
254  #ifdef DEBUG_BVMODULE
255  std::cout << std::endl << std::endl << "Take into account: " << std::endl;
256  std::cout << iter->second << std::endl;
257  #endif
258  const FormulaSetT& formulasToPass = mEncoder.encode( iter->second );
259  for( const FormulaT& formulaToPass : formulasToPass )
260  addSubformulaToPassedFormula( formulaToPass, iter->second );
261  mPositionInFormulasToBlast.erase( iter->second );
262  mFormulasToBlast.erase( iter );
263  }
264  break;
265  }
266  default:
267  assert( backendAnswer == UNKNOWN );
268  return UNKNOWN;
269  }
270  }
271  assert( false );
272  return SAT;
273  }
274  else
275  {
276  auto receivedSubformula = firstUncheckedReceivedSubformula();
277  while(receivedSubformula != rReceivedFormula().end())
278  {
279  const FormulaWithOrigins& fwo = *receivedSubformula;
280  const FormulaT& formula = fwo.formula();
281 
282  const FormulaSetT& formulasToPass = mEncoder.encode(formula);
283 
284  for(const FormulaT& formulaToPass : formulasToPass)
285  addSubformulaToPassedFormula(formulaToPass, formula);
286  ++receivedSubformula;
287  }
288 
289  Answer backendAnswer = runBackends();
290  if(backendAnswer == UNSAT)
291  {
292  getInfeasibleSubsets();
293  }
294 
295  return backendAnswer;
296  }
297  }
298 
299  template<class Settings>
300  size_t BVModule<Settings>::evaluateBVFormula( const FormulaT& _formula )
301  {
302  if( _formula.type() == carl::FormulaType::CONSTRAINT && _formula.constraint().relation() == carl::Relation::EQ )
303  return carl::complexity(_formula);
304  return Settings::equation_preference_weight * carl::complexity(_formula);
305  }
306 }
307 
308