carl  25.02
Computer ARithmetic Library
Formula.tpp
Go to the documentation of this file.
1 /**
2  * @file Formula.tpp
3  * @author Florian Corzilius<corzilius@cs.rwth-aachen.de>
4  * @author Ulrich Loup
5  * @author Sebastian Junges
6  * @since 2012-02-09
7  * @version 2014-10-30
8  */
9 
10 
11 #include "Formula.h"
12 #include "FormulaPool.h"
13 #include <carl-arith/poly/umvpoly/functions/Complexity.h>
14 #include "functions/Visit.h"
15 
16 namespace carl
17 {
18 
19  template<typename Pol>
20  void Formula<Pol>::init( FormulaContent<Pol>& _content )
21  {
22  _content.mProperties = Condition();
23  switch( _content.mType )
24  {
25  case FormulaType::EXISTS:
26  {
27  _content.mProperties |= PROP_CONTAINS_QUANTIFIER_EXISTS;
28  auto subFormula = std::get<QuantifierContent<Pol>>(_content.mContent).mFormula;
29  _content.mProperties |= (subFormula.properties() & WEAK_CONDITIONS);
30  _content.mProperties |= (subFormula.properties() & PROP_IS_IN_PNF);
31  break;
32  }
33  case FormulaType::AUX_EXISTS:
34  {
35  _content.mProperties |= PROP_CONTAINS_QUANTIFIER_EXISTS;
36  auto subFormula = std::get<AuxQuantifierContent<Pol>>(_content.mContent).mFormula;
37  _content.mProperties |= (subFormula.properties() & WEAK_CONDITIONS);
38  _content.mProperties |= (subFormula.properties() & ~PROP_IS_IN_PNF);
39  break;
40  }
41  case FormulaType::FORALL:
42  {
43  _content.mProperties |= PROP_CONTAINS_QUANTIFIER_FORALL;
44  auto subFormula = std::get<QuantifierContent<Pol>>(_content.mContent).mFormula;
45  _content.mProperties |= (subFormula.properties() & WEAK_CONDITIONS);
46  _content.mProperties |= (subFormula.properties() & PROP_IS_IN_PNF);
47  break;
48  }
49  case FormulaType::TRUE:
50  {
51  _content.mProperties |= STRONG_CONDITIONS;
52  addConstraintProperties( std::get<Constraint<Pol>>(_content.mContent), _content.mProperties );
53  break;
54  }
55  case FormulaType::FALSE:
56  {
57  _content.mProperties |= STRONG_CONDITIONS;
58  addConstraintProperties( std::get<Constraint<Pol>>(_content.mContent), _content.mProperties );
59  break;
60  }
61  case FormulaType::BOOL:
62  {
63  _content.mProperties |= STRONG_CONDITIONS | PROP_CONTAINS_BOOLEAN;
64  break;
65  }
66  case FormulaType::NOT:
67  {
68  Condition subFormulaConds = std::get<Formula<Pol>>(_content.mContent).mpContent->mProperties;
69  if( PROP_IS_AN_ATOM <= subFormulaConds )
70  _content.mProperties |= PROP_IS_A_CLAUSE | PROP_IS_A_LITERAL | PROP_IS_IN_CNF | PROP_IS_LITERAL_CONJUNCTION;
71  _content.mProperties |= (subFormulaConds & WEAK_CONDITIONS);
72  if (!(PROP_CONTAINS_QUANTIFIER_EXISTS <= subFormulaConds) && !(PROP_CONTAINS_QUANTIFIER_FORALL <= subFormulaConds))
73  _content.mProperties |= PROP_IS_IN_PNF;
74  break;
75  }
76  case FormulaType::OR:
77  {
78  _content.mProperties |= PROP_IS_A_CLAUSE | PROP_IS_IN_CNF | PROP_IS_IN_NNF | PROP_IS_IN_PNF;
79  for (auto subFormula = std::get<Formulas<Pol>>(_content.mContent).begin(); subFormula != std::get<Formulas<Pol>>(_content.mContent).end(); ++subFormula)
80  {
81  Condition subFormulaConds = subFormula->properties();
82  if( !(PROP_IS_A_LITERAL<=subFormulaConds) )
83  {
84  _content.mProperties &= ~PROP_IS_A_CLAUSE;
85  _content.mProperties &= ~PROP_IS_IN_CNF;
86  }
87  if( !(PROP_IS_IN_NNF<=subFormulaConds) )
88  _content.mProperties &= ~PROP_IS_IN_NNF;
89  _content.mProperties |= (subFormulaConds & WEAK_CONDITIONS);
90  if (PROP_CONTAINS_QUANTIFIER_EXISTS <= subFormulaConds || PROP_CONTAINS_QUANTIFIER_FORALL <= subFormulaConds)
91  _content.mProperties &= ~PROP_IS_IN_PNF;
92  }
93  break;
94  }
95  case FormulaType::AND:
96  {
97  _content.mProperties |= PROP_IS_LITERAL_CONJUNCTION | PROP_IS_PURE_CONJUNCTION | PROP_IS_IN_CNF | PROP_IS_IN_NNF | PROP_IS_IN_PNF;
98  for (auto subFormula = std::get<Formulas<Pol>>(_content.mContent).begin(); subFormula != std::get<Formulas<Pol>>(_content.mContent).end(); ++subFormula)
99  {
100  Condition subFormulaConds = subFormula->properties();
101  if( !(PROP_IS_A_CLAUSE<=subFormulaConds) )
102  {
103  _content.mProperties &= ~PROP_IS_PURE_CONJUNCTION;
104  _content.mProperties &= ~PROP_IS_LITERAL_CONJUNCTION;
105  _content.mProperties &= ~PROP_IS_IN_CNF;
106  }
107  else if( !(PROP_IS_A_LITERAL<=subFormulaConds) )
108  {
109  _content.mProperties &= ~PROP_IS_PURE_CONJUNCTION;
110  _content.mProperties &= ~PROP_IS_LITERAL_CONJUNCTION;
111  }
112  else if( !(PROP_IS_AN_ATOM <=subFormulaConds) )
113  _content.mProperties &= ~PROP_IS_PURE_CONJUNCTION;
114  if( !(PROP_IS_IN_NNF<=subFormulaConds) )
115  _content.mProperties &= ~PROP_IS_IN_NNF;
116  _content.mProperties |= (subFormulaConds & WEAK_CONDITIONS);
117  if (PROP_CONTAINS_QUANTIFIER_EXISTS <= subFormulaConds || PROP_CONTAINS_QUANTIFIER_FORALL <= subFormulaConds)
118  _content.mProperties &= ~PROP_IS_IN_PNF;
119  }
120  break;
121  }
122  case FormulaType::ITE:
123  case FormulaType::IMPLIES:
124  case FormulaType::IFF:
125  case FormulaType::XOR:
126  {
127  _content.mProperties |= PROP_IS_IN_NNF | PROP_IS_IN_PNF;
128  for (auto subFormula = std::get<Formulas<Pol>>(_content.mContent).begin(); subFormula != std::get<Formulas<Pol>>(_content.mContent).end(); ++subFormula)
129  {
130  Condition subFormulaConds = subFormula->properties();
131  if( !(PROP_IS_IN_NNF<=subFormulaConds) )
132  _content.mProperties &= ~PROP_IS_IN_NNF;
133  _content.mProperties |= (subFormulaConds & WEAK_CONDITIONS);
134  if (PROP_CONTAINS_QUANTIFIER_EXISTS <= subFormulaConds || PROP_CONTAINS_QUANTIFIER_FORALL <= subFormulaConds)
135  _content.mProperties &= ~PROP_IS_IN_PNF;
136  }
137  break;
138  }
139  case FormulaType::CONSTRAINT:
140  {
141  _content.mProperties |= STRONG_CONDITIONS;
142  addConstraintProperties(std::get<Constraint<Pol>>(_content.mContent), _content.mProperties);
143  break;
144  }
145  case FormulaType::VARCOMPARE:
146  {
147  _content.mProperties |= STRONG_CONDITIONS; //| PROP_CONTAINS_REAL_VALUED_VARS | PROP_CONTAINS_INTEGER_VALUED_VARS;
148  _content.mProperties |= PROP_CONTAINS_NONLINEAR_POLYNOMIAL;
149  _content.mProperties |= PROP_CONTAINS_ROOT_EXPRESSION;
150  break;
151  }
152  case FormulaType::VARASSIGN:
153  {
154  _content.mProperties |= STRONG_CONDITIONS; //| PROP_CONTAINS_REAL_VALUED_VARS | PROP_CONTAINS_INTEGER_VALUED_VARS;
155  _content.mProperties |= PROP_CONTAINS_ROOT_EXPRESSION;
156  break;
157  }
158  case FormulaType::BITVECTOR:
159  {
160  _content.mProperties |= STRONG_CONDITIONS | PROP_CONTAINS_BITVECTOR;
161  break;
162  }
163  case FormulaType::UEQ:
164  {
165  _content.mProperties |= STRONG_CONDITIONS | PROP_CONTAINS_UNINTERPRETED_EQUATIONS;
166  break;
167  }
168  default:
169  {
170  CARL_LOG_ERROR("carl.formula", "Undefined formula type " << _content.mType);
171  assert( false );
172  }
173  }
174  }
175 
176  template<typename Pol>
177  void Formula<Pol>::addConstraintProperties( const Constraint<Pol>& _constraint, Condition& _properties )
178  {
179  if( carl::is_zero(_constraint.lhs()) )
180  {
181  _properties |= PROP_CONTAINS_LINEAR_POLYNOMIAL;
182  }
183  else
184  {
185  switch( _constraint.lhs().total_degree() )
186  {
187  case 0:
188  _properties |= PROP_CONTAINS_LINEAR_POLYNOMIAL;
189  break;
190  case 1:
191  _properties |= PROP_CONTAINS_LINEAR_POLYNOMIAL;
192  break;
193  case 2:
194  _properties |= PROP_CONTAINS_NONLINEAR_POLYNOMIAL;
195  break;
196  case 3:
197  _properties |= PROP_CONTAINS_NONLINEAR_POLYNOMIAL;
198  _properties |= PROP_VARIABLE_DEGREE_GREATER_THAN_TWO;
199  break;
200  case 4:
201  _properties |= PROP_CONTAINS_NONLINEAR_POLYNOMIAL;
202  _properties |= PROP_VARIABLE_DEGREE_GREATER_THAN_THREE;
203  break;
204  default:
205  _properties |= PROP_CONTAINS_NONLINEAR_POLYNOMIAL;
206  _properties |= PROP_VARIABLE_DEGREE_GREATER_THAN_FOUR;
207  break;
208  }
209  }
210  switch( _constraint.relation() )
211  {
212  case Relation::EQ:
213  _properties |= PROP_CONTAINS_EQUATION;
214  _properties |= PROP_CONTAINS_WEAK_INEQUALITY;
215  break;
216  case Relation::NEQ:
217  _properties |= PROP_CONTAINS_STRICT_INEQUALITY;
218  break;
219  case Relation::LEQ:
220  _properties |= PROP_CONTAINS_INEQUALITY;
221  _properties |= PROP_CONTAINS_WEAK_INEQUALITY;
222  break;
223  case Relation::GEQ:
224  _properties |= PROP_CONTAINS_INEQUALITY;
225  _properties |= PROP_CONTAINS_WEAK_INEQUALITY;
226  break;
227  case Relation::LESS:
228  _properties |= PROP_CONTAINS_STRICT_INEQUALITY;
229  break;
230  case Relation::GREATER:
231  _properties |= PROP_CONTAINS_STRICT_INEQUALITY;
232  break;
233  default:
234  {
235  }
236  }
237  if( _constraint.hasIntegerValuedVariable() )
238  _properties |= PROP_CONTAINS_INTEGER_VALUED_VARS;
239  if( _constraint.hasRealValuedVariable() )
240  _properties |= PROP_CONTAINS_REAL_VALUED_VARS;
241  if( _constraint.isPseudoBoolean() )
242  _properties |= PROP_CONTAINS_PSEUDOBOOLEAN;
243  }
244 
245 
246 } // namespace carl