carl  24.04
Computer ARithmetic Library
Assignment.tpp
Go to the documentation of this file.
1 /**
2  * Class to create a state object.
3  * @author Florian Corzilius
4  * @since 2014-01-14
5  * @version 2014-01-14
6  */
7 
8 #include "Assignment.h"
9 #include <carl-formula/uninterpreted/SortValueManager.h>
10 #include <carl-formula/formula/functions/Substitution.h>
11 
12 
13 namespace carl
14 {
15  template<typename Rational, typename Poly>
16  bool getRationalAssignmentsFromModel( const Model<Rational,Poly>& _model, std::map<Variable,Rational>& _rationalAssigns )
17  {
18  bool result = true;
19  for( auto ass = _model.begin(); ass != _model.end(); ++ass )
20  {
21  if (ass->second.isRational())
22  {
23  _rationalAssigns.insert( _rationalAssigns.end(), std::make_pair(ass->first.asVariable(), ass->second.asRational()));
24  }
25  else if (ass->second.isSqrtEx())
26  {
27  if( ass->second.asSqrtEx().is_constant() && !ass->second.asSqrtEx().has_sqrt() )
28  {
29  assert( ass->first.is_variable() );
30  Rational value = ass->second.asSqrtEx().constant_part().constant_part()/ass->second.asSqrtEx().denominator().constant_part();
31  assert( !(ass->first.asVariable().type() == carl::VariableType::VT_INT) || carl::is_integer( value ) );
32  _rationalAssigns.insert( _rationalAssigns.end(), std::make_pair(ass->first.asVariable(), value));
33  }
34  else
35  {
36  result = false;
37  }
38  }
39  else if (ass->second.isRAN())
40  {
41  if (ass->second.asRAN().is_numeric())
42  {
43  assert( ass->first.is_variable() );
44  _rationalAssigns.insert( _rationalAssigns.end(), std::make_pair(ass->first.asVariable(), ass->second.asRAN().value()) );
45  }
46  }
47  }
48  return result;
49  }
50 
51  template<typename Rational, typename Poly>
52  unsigned satisfies( const Model<Rational,Poly>& _assignment, const Formula<Poly>& _formula )
53  {
54  std::map<Variable,Rational> rationalAssigns;
55  getRationalAssignmentsFromModel( _assignment, rationalAssigns );
56  std::map<carl::BVVariable, carl::BVTerm> bvAssigns;
57  for( auto& varAndValue : _assignment )
58  {
59  if( varAndValue.first.isBVVariable() )
60  {
61  assert(varAndValue.second.isBVValue());
62  carl::BVTerm replacement(carl::BVTermType::CONSTANT, varAndValue.second.asBVValue());
63  bvAssigns[varAndValue.first.asBVVariable()] = replacement;
64  }
65  }
66  return satisfies( _assignment, rationalAssigns, bvAssigns, _formula );
67  }
68 
69  template<typename Rational, typename Poly>
70  bool isPartOf( const std::map<Variable,Rational>& _assignment, const Model<Rational,Poly>& _model )
71  {
72  auto assIter = _assignment.begin();
73  auto modIter = _model.begin();
74  while( assIter != _assignment.end() && modIter != _model.end() )
75  {
76  if( modIter->first < assIter->first )
77  {
78  ++assIter;
79  }
80  else if( assIter->first < modIter->first )
81  {
82  return false;
83  }
84  else
85  {
86  ++assIter;
87  ++modIter;
88  }
89  }
90  return assIter == _assignment.end();
91  }
92 
93  template<typename Rational, typename Poly>
94  SortValue satisfiesUF( const Model<Rational,Poly>& _model, const UFInstance _ufi )
95  {
96  auto iter = _model.find( _ufi.uninterpretedFunction() );
97  if( iter == _model.end() )
98  return defaultSortValue(_ufi.uninterpretedFunction().codomain());
99  assert( iter->second.isUFModel() );
100  const UFModel& ufm = iter->second.asUFModel();
101  std::vector<SortValue> inst;
102  for( const carl::UTerm& arg : _ufi.args() )
103  {
104  if(arg.isUVariable()) {
105  auto iterB = _model.find( arg.asUVariable() );
106  if( iterB == _model.end() )
107  return defaultSortValue(_ufi.uninterpretedFunction().codomain());
108  assert( iterB->second.isSortValue() );
109  inst.push_back( iterB->second.asSortValue() );
110  } else if(arg.isUFInstance()) {
111  inst.push_back(satisfiesUF(_model, arg.asUFInstance()));
112  }
113  }
114  SortValue sv = ufm.get( inst );
115  return sv;
116  }
117 
118  template<typename Rational, typename Poly>
119  unsigned satisfies( const Model<Rational,Poly>& _model, const std::map<Variable,Rational>& _assignment, const std::map<carl::BVVariable, carl::BVTerm>& _bvAssigns, const Formula<Poly>& _formula )
120  {
121  assert( isPartOf( _assignment, _model ) );
122  switch( _formula.type() )
123  {
124  case carl::FormulaType::TRUE:
125  {
126  return 1;
127  }
128  case carl::FormulaType::FALSE:
129  {
130  return 0;
131  }
132  case carl::FormulaType::BOOL:
133  {
134  auto ass = _model.find( _formula.boolean() );
135  return ass == _model.end() ? 2 : (ass->second.asBool() ? 1 : 0);
136  }
137  case carl::FormulaType::CONSTRAINT:
138  {
139  return satisfied_by(_formula.constraint(), _assignment);
140  }
141  case carl::FormulaType::BITVECTOR:
142  {
143  Formula<Poly> substituted = carl::substitute(_formula, _bvAssigns);
144  if(substituted.is_true())
145  return 1;
146  else if(substituted.is_false())
147  return 0;
148  return 2;
149  }
150  case carl::FormulaType::NOT:
151  {
152  switch( satisfies( _model, _assignment, _bvAssigns, _formula.subformula() ) )
153  {
154  case 0:
155  return 1;
156  case 1:
157  return 0;
158  default:
159  return 2;
160  }
161  }
162  case carl::FormulaType::OR:
163  {
164  unsigned result = 0;
165  for( const Formula<Poly>& subFormula : _formula.subformulas() )
166  {
167  switch( satisfies( _model, _assignment, _bvAssigns, subFormula ) )
168  {
169  case 0:
170  break;
171  case 1:
172  return 1;
173  default:
174  if( result != 2 ) result = 2;
175  }
176  }
177  return result;
178  }
179  case carl::FormulaType::AND:
180  {
181  unsigned result = 1;
182  for( const Formula<Poly>& subFormula : _formula.subformulas() )
183  {
184  switch( satisfies( _model, _assignment, _bvAssigns, subFormula ) )
185  {
186  case 0:
187  return 0;
188  case 1:
189  break;
190  default:
191  if( result != 2 ) result = 2;
192  }
193  }
194  return result;
195  }
196  case carl::FormulaType::IMPLIES:
197  {
198  unsigned result = satisfies( _model, _assignment, _bvAssigns, _formula.premise() );
199  if( result == 0 ) return 1;
200  switch( satisfies( _model, _assignment, _bvAssigns, _formula.conclusion() ) )
201  {
202  case 0:
203  return result == 1 ? 0 : 2;
204  case 1:
205  return 1;
206  default:
207  return 2;
208  }
209  }
210  case carl::FormulaType::ITE:
211  {
212  unsigned result = satisfies( _model, _assignment, _bvAssigns, _formula.condition() );
213  switch( result )
214  {
215  case 0:
216  return satisfies( _model, _assignment, _bvAssigns, _formula.second_case() );
217  case 1:
218  return satisfies( _model, _assignment, _bvAssigns, _formula.first_case() );
219  default:
220  return 2;
221  }
222  }
223  case carl::FormulaType::IFF:
224  {
225  auto subFormula = _formula.subformulas().begin();
226  unsigned result = satisfies( _model, _assignment, _bvAssigns, *subFormula );
227  bool containsTrue = (result == 1 ? true : false);
228  bool containsFalse = (result == 0 ? true : false);
229  ++subFormula;
230  while( subFormula != _formula.subformulas().end() )
231  {
232  unsigned resultTmp = satisfies( _model, _assignment, _bvAssigns, *subFormula );
233  switch( resultTmp )
234  {
235  case 0:
236  containsFalse = true;
237  break;
238  case 1:
239  containsTrue = true;
240  break;
241  default:
242  result = 2;
243  }
244  if( containsFalse && containsTrue )
245  return 0;
246  ++subFormula;
247  }
248  return (result == 2 ? 2 : 1);
249  }
250  case carl::FormulaType::XOR:
251  {
252  auto subFormula = _formula.subformulas().begin();
253  unsigned result = satisfies( _model, _assignment, _bvAssigns, *subFormula );
254  if( result == 2 ) return 2;
255  ++subFormula;
256  while( subFormula != _formula.subformulas().end() )
257  {
258  unsigned resultTmp = satisfies( _model, _assignment, _bvAssigns, *subFormula );
259  if( resultTmp == 2 ) return 2;
260  result = resultTmp != result;
261  ++subFormula;
262  }
263  return result;
264  }
265  case carl::FormulaType::EXISTS:
266  {
267  ///@todo do something here
268  return 2;
269  }
270  case carl::FormulaType::FORALL:
271  {
272  ///@todo do something here
273  return 2;
274  }
275  case carl::FormulaType::UEQ:
276  {
277  const carl::UEquality& eq = _formula.u_equality();
278  std::size_t lhsResult = 0;
279  std::size_t rhsResult = 0;
280  // get sortvalue for lhs and rhs
281  if( eq.lhs().isUVariable() )
282  {
283  auto iter = _model.find( eq.lhs().asUVariable() );
284  if( iter == _model.end() )
285  return 2;
286  assert( iter->second.isSortValue() );
287  lhsResult = iter->second.asSortValue().id();
288  }
289  else
290  {
291  SortValue sv = satisfiesUF(_model, eq.lhs().asUFInstance());
292  if( sv == defaultSortValue( sv.sort() ) )
293  return 2;
294  lhsResult = sv.id();
295  }
296  if( eq.rhs().isUVariable() )
297  {
298  auto iter = _model.find( eq.rhs().asUVariable() );
299  if( iter == _model.end() )
300  return 2;
301  assert( iter->second.isSortValue() );
302  rhsResult = iter->second.asSortValue().id();
303  }
304  else
305  {
306  SortValue sv = satisfiesUF(_model, eq.rhs().asUFInstance());
307  if( sv == defaultSortValue( sv.sort() ) )
308  return 2;
309  rhsResult = sv.id();
310  }
311  // check eq.negated() <=> sv(lhs) != sv(rhs)
312  return eq.negated() ? lhsResult != rhsResult : lhsResult == rhsResult;
313  }
314  default:
315  {
316  assert( false );
317  std::cerr << "Undefined operator!" << std::endl;
318  return 2;
319  }
320  }
321  }
322 
323  template<typename Rational, typename Poly>
324  void getDefaultModel( Model<Rational,Poly>& /*_defaultModel*/, const carl::UEquality& /*_constraint*/, bool /*_overwrite*/, size_t /*_seed*/ )
325  {
326  assert(false);
327  }
328 
329  template<typename Rational, typename Poly>
330  void getDefaultModel( Model<Rational,Poly>& _defaultModel, const carl::BVTerm& _bvTerm, bool _overwrite, size_t _seed )
331  {
332  if( _bvTerm.type() == carl::BVTermType::VARIABLE )
333  {
334  auto ass = _defaultModel.find( _bvTerm.variable() );
335  if( ass == _defaultModel.end() )
336  {
337  _defaultModel.emplace(_bvTerm.variable(), carl::BVValue(_bvTerm.variable().width()));
338  }
339  else
340  {
341  // TODO: something with the seed
342  }
343  }
344  else if( carl::typeIsUnary( _bvTerm.type() ) )
345  getDefaultModel( _defaultModel, _bvTerm.operand(), _overwrite, _seed );
346  else if( carl::typeIsBinary( _bvTerm.type() ) )
347  {
348  getDefaultModel( _defaultModel, _bvTerm.first(), _overwrite, _seed );
349  getDefaultModel( _defaultModel, _bvTerm.second(), _overwrite, _seed );
350  }
351  else if( _bvTerm.type() == carl::BVTermType::EXTRACT )
352  getDefaultModel( _defaultModel, _bvTerm.operand(), _overwrite, _seed );
353  }
354 
355  template<typename Rational, typename Poly>
356  void getDefaultModel( Model<Rational,Poly>& _defaultModel, const Constraint<Poly>& _constraint, bool /*_overwrite*/, size_t /*_seed*/ )
357  {
358  for( carl::Variable var : variables(_constraint) )
359  {
360  auto ass = _defaultModel.find( var );
361  if( ass == _defaultModel.end() )
362  {
363  _defaultModel.emplace(var, 0);
364  }
365  else
366  {
367  // TODO: something with the seed
368  }
369  }
370  }
371 
372  template<typename Rational, typename Poly>
373  void getDefaultModel( Model<Rational,Poly>& _defaultModel, const Formula<Poly>& _formula, bool _overwrite, size_t _seed )
374  {
375  switch( _formula.type() )
376  {
377  case carl::FormulaType::TRUE:
378  case carl::FormulaType::FALSE:
379  case carl::FormulaType::BOOL:
380  {
381  auto ass = _defaultModel.find( _formula.boolean() );
382  if( ass == _defaultModel.end() )
383  {
384  _defaultModel.emplace(_formula.boolean(), false);
385  }
386  else
387  {
388  // TODO: something with the seed
389  }
390  return;
391  }
392  case carl::FormulaType::CONSTRAINT:
393  getDefaultModel( _defaultModel, _formula.constraint(), _overwrite, _seed );
394  return;
395  case carl::FormulaType::BITVECTOR:
396  getDefaultModel( _defaultModel, _formula.bv_constraint().lhs(), _overwrite, _seed );
397  getDefaultModel( _defaultModel, _formula.bv_constraint().rhs(), _overwrite, _seed );
398  return;
399  case carl::FormulaType::UEQ:
400  getDefaultModel( _defaultModel, _formula.u_equality(), _overwrite, _seed );
401  return;
402  case carl::FormulaType::NOT:
403  getDefaultModel( _defaultModel, _formula.subformula(), _overwrite, _seed );
404  return;
405  default:
406  assert( _formula.is_nary() );
407  for (const auto& subFormula: _formula.subformulas() )
408  getDefaultModel(_defaultModel, subFormula, _overwrite, _seed);
409  }
410  }
411 
412  template<typename Rational, typename Poly>
413  Formula<Poly> representingFormula(const ModelVariable& mv, const Model<Rational,Poly>& model) {
414  auto it = model.find(mv);
415  assert(it != model.end());
416  return representingFormula(mv, it->second);
417  }
418  template<typename Rational, typename Poly>
419  Formula<Poly> representingFormula(const ModelVariable& mv, const ModelValue<Rational,Poly>& val) {
420  if (val.isBool()) {
421  assert(mv.is_variable());
422  if (val.asBool()) return Formula<Poly>(mv.asVariable());
423  else return Formula<Poly>(FormulaType::NOT, Formula<Poly>(mv.asVariable()));
424  } else if (val.isRational()) {
425  assert(mv.is_variable());
426  return Formula<Poly>(VariableAssignment<Poly>(mv.asVariable(), val.asRational()));
427  } else if (val.isSqrtEx()) {
428  assert(false);
429  } else if (val.isRAN()) {
430  return Formula<Poly>(VariableAssignment<Poly>(mv.asVariable(), val.asRAN()));
431  } else if (val.isBVValue()) {
432  assert(false);
433  } else if (val.isSortValue()) {
434  assert(false);
435  } else if (val.isUFModel()) {
436  assert(false);
437  } else if (val.isSubstitution()) {
438  return val.asSubstitution()->representingFormula(mv);
439  }
440  assert(false);
441  return Formula<Poly>(FormulaType::FALSE);
442  }
443 }