carl  24.04
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::FORALL:
34  {
35  _content.mProperties |= PROP_CONTAINS_QUANTIFIER_FORALL;
36  auto subFormula = std::get<QuantifierContent<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::TRUE:
42  {
43  _content.mProperties |= STRONG_CONDITIONS;
44  addConstraintProperties( std::get<Constraint<Pol>>(_content.mContent), _content.mProperties );
45  break;
46  }
47  case FormulaType::FALSE:
48  {
49  _content.mProperties |= STRONG_CONDITIONS;
50  addConstraintProperties( std::get<Constraint<Pol>>(_content.mContent), _content.mProperties );
51  break;
52  }
53  case FormulaType::BOOL:
54  {
55  _content.mProperties |= STRONG_CONDITIONS | PROP_CONTAINS_BOOLEAN;
56  break;
57  }
58  case FormulaType::NOT:
59  {
60  Condition subFormulaConds = std::get<Formula<Pol>>(_content.mContent).mpContent->mProperties;
61  if( PROP_IS_AN_ATOM <= subFormulaConds )
62  _content.mProperties |= PROP_IS_A_CLAUSE | PROP_IS_A_LITERAL | PROP_IS_IN_CNF | PROP_IS_LITERAL_CONJUNCTION;
63  _content.mProperties |= (subFormulaConds & WEAK_CONDITIONS);
64  if (!(PROP_CONTAINS_QUANTIFIER_EXISTS <= subFormulaConds) && !(PROP_CONTAINS_QUANTIFIER_FORALL <= subFormulaConds))
65  _content.mProperties |= PROP_IS_IN_PNF;
66  break;
67  }
68  case FormulaType::OR:
69  {
70  _content.mProperties |= PROP_IS_A_CLAUSE | PROP_IS_IN_CNF | PROP_IS_IN_NNF | PROP_IS_IN_PNF;
71  for (auto subFormula = std::get<Formulas<Pol>>(_content.mContent).begin(); subFormula != std::get<Formulas<Pol>>(_content.mContent).end(); ++subFormula)
72  {
73  Condition subFormulaConds = subFormula->properties();
74  if( !(PROP_IS_A_LITERAL<=subFormulaConds) )
75  {
76  _content.mProperties &= ~PROP_IS_A_CLAUSE;
77  _content.mProperties &= ~PROP_IS_IN_CNF;
78  }
79  if( !(PROP_IS_IN_NNF<=subFormulaConds) )
80  _content.mProperties &= ~PROP_IS_IN_NNF;
81  _content.mProperties |= (subFormulaConds & WEAK_CONDITIONS);
82  if (PROP_CONTAINS_QUANTIFIER_EXISTS <= subFormulaConds || PROP_CONTAINS_QUANTIFIER_FORALL <= subFormulaConds)
83  _content.mProperties &= ~PROP_IS_IN_PNF;
84  }
85  break;
86  }
87  case FormulaType::AND:
88  {
89  _content.mProperties |= PROP_IS_LITERAL_CONJUNCTION | PROP_IS_PURE_CONJUNCTION | PROP_IS_IN_CNF | PROP_IS_IN_NNF | PROP_IS_IN_PNF;
90  for (auto subFormula = std::get<Formulas<Pol>>(_content.mContent).begin(); subFormula != std::get<Formulas<Pol>>(_content.mContent).end(); ++subFormula)
91  {
92  Condition subFormulaConds = subFormula->properties();
93  if( !(PROP_IS_A_CLAUSE<=subFormulaConds) )
94  {
95  _content.mProperties &= ~PROP_IS_PURE_CONJUNCTION;
96  _content.mProperties &= ~PROP_IS_LITERAL_CONJUNCTION;
97  _content.mProperties &= ~PROP_IS_IN_CNF;
98  }
99  else if( !(PROP_IS_A_LITERAL<=subFormulaConds) )
100  {
101  _content.mProperties &= ~PROP_IS_PURE_CONJUNCTION;
102  _content.mProperties &= ~PROP_IS_LITERAL_CONJUNCTION;
103  }
104  else if( !(PROP_IS_AN_ATOM <=subFormulaConds) )
105  _content.mProperties &= ~PROP_IS_PURE_CONJUNCTION;
106  if( !(PROP_IS_IN_NNF<=subFormulaConds) )
107  _content.mProperties &= ~PROP_IS_IN_NNF;
108  _content.mProperties |= (subFormulaConds & WEAK_CONDITIONS);
109  if (PROP_CONTAINS_QUANTIFIER_EXISTS <= subFormulaConds || PROP_CONTAINS_QUANTIFIER_FORALL <= subFormulaConds)
110  _content.mProperties &= ~PROP_IS_IN_PNF;
111  }
112  break;
113  }
114  case FormulaType::ITE:
115  case FormulaType::IMPLIES:
116  case FormulaType::IFF:
117  case FormulaType::XOR:
118  {
119  _content.mProperties |= PROP_IS_IN_NNF | PROP_IS_IN_PNF;
120  for (auto subFormula = std::get<Formulas<Pol>>(_content.mContent).begin(); subFormula != std::get<Formulas<Pol>>(_content.mContent).end(); ++subFormula)
121  {
122  Condition subFormulaConds = subFormula->properties();
123  if( !(PROP_IS_IN_NNF<=subFormulaConds) )
124  _content.mProperties &= ~PROP_IS_IN_NNF;
125  _content.mProperties |= (subFormulaConds & WEAK_CONDITIONS);
126  if (PROP_CONTAINS_QUANTIFIER_EXISTS <= subFormulaConds || PROP_CONTAINS_QUANTIFIER_FORALL <= subFormulaConds)
127  _content.mProperties &= ~PROP_IS_IN_PNF;
128  }
129  break;
130  }
131  case FormulaType::CONSTRAINT:
132  {
133  _content.mProperties |= STRONG_CONDITIONS;
134  addConstraintProperties(std::get<Constraint<Pol>>(_content.mContent), _content.mProperties);
135  break;
136  }
137  case FormulaType::VARCOMPARE:
138  {
139  _content.mProperties |= STRONG_CONDITIONS | PROP_CONTAINS_REAL_VALUED_VARS | PROP_CONTAINS_INTEGER_VALUED_VARS;
140  break;
141  }
142  case FormulaType::VARASSIGN:
143  {
144  _content.mProperties |= STRONG_CONDITIONS | PROP_CONTAINS_REAL_VALUED_VARS | PROP_CONTAINS_INTEGER_VALUED_VARS;
145  break;
146  }
147  case FormulaType::BITVECTOR:
148  {
149  _content.mProperties |= STRONG_CONDITIONS | PROP_CONTAINS_BITVECTOR;
150  break;
151  }
152  case FormulaType::UEQ:
153  {
154  _content.mProperties |= STRONG_CONDITIONS | PROP_CONTAINS_UNINTERPRETED_EQUATIONS;
155  break;
156  }
157  default:
158  {
159  CARL_LOG_ERROR("carl.formula", "Undefined formula type " << _content.mType);
160  assert( false );
161  }
162  }
163  }
164 
165  template<typename Pol>
166  void Formula<Pol>::addConstraintProperties( const Constraint<Pol>& _constraint, Condition& _properties )
167  {
168  if( carl::is_zero(_constraint.lhs()) )
169  {
170  _properties |= PROP_CONTAINS_LINEAR_POLYNOMIAL;
171  }
172  else
173  {
174  switch( _constraint.lhs().total_degree() )
175  {
176  case 0:
177  _properties |= PROP_CONTAINS_LINEAR_POLYNOMIAL;
178  break;
179  case 1:
180  _properties |= PROP_CONTAINS_LINEAR_POLYNOMIAL;
181  break;
182  case 2:
183  _properties |= PROP_CONTAINS_NONLINEAR_POLYNOMIAL;
184  break;
185  case 3:
186  _properties |= PROP_CONTAINS_NONLINEAR_POLYNOMIAL;
187  _properties |= PROP_VARIABLE_DEGREE_GREATER_THAN_TWO;
188  break;
189  case 4:
190  _properties |= PROP_CONTAINS_NONLINEAR_POLYNOMIAL;
191  _properties |= PROP_VARIABLE_DEGREE_GREATER_THAN_THREE;
192  break;
193  default:
194  _properties |= PROP_CONTAINS_NONLINEAR_POLYNOMIAL;
195  _properties |= PROP_VARIABLE_DEGREE_GREATER_THAN_FOUR;
196  break;
197  }
198  }
199  switch( _constraint.relation() )
200  {
201  case Relation::EQ:
202  _properties |= PROP_CONTAINS_EQUATION;
203  _properties |= PROP_CONTAINS_WEAK_INEQUALITY;
204  break;
205  case Relation::NEQ:
206  _properties |= PROP_CONTAINS_STRICT_INEQUALITY;
207  break;
208  case Relation::LEQ:
209  _properties |= PROP_CONTAINS_INEQUALITY;
210  _properties |= PROP_CONTAINS_WEAK_INEQUALITY;
211  break;
212  case Relation::GEQ:
213  _properties |= PROP_CONTAINS_INEQUALITY;
214  _properties |= PROP_CONTAINS_WEAK_INEQUALITY;
215  break;
216  case Relation::LESS:
217  _properties |= PROP_CONTAINS_STRICT_INEQUALITY;
218  break;
219  case Relation::GREATER:
220  _properties |= PROP_CONTAINS_STRICT_INEQUALITY;
221  break;
222  default:
223  {
224  }
225  }
226  if( _constraint.hasIntegerValuedVariable() )
227  _properties |= PROP_CONTAINS_INTEGER_VALUED_VARS;
228  if( _constraint.hasRealValuedVariable() )
229  _properties |= PROP_CONTAINS_REAL_VALUED_VARS;
230  if( _constraint.isPseudoBoolean() )
231  _properties |= PROP_CONTAINS_PSEUDOBOOLEAN;
232  }
233 
234 
235 } // namespace carl