3 * @author Florian Corzilius<corzilius@cs.rwth-aachen.de>
5 * @author Sebastian Junges
12 #include "FormulaPool.h"
13 #include <carl-arith/poly/umvpoly/functions/Complexity.h>
14 #include "functions/Visit.h"
19 template<typename Pol>
20 void Formula<Pol>::init( FormulaContent<Pol>& _content )
22 _content.mProperties = Condition();
23 switch( _content.mType )
25 case FormulaType::EXISTS:
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);
33 case FormulaType::AUX_EXISTS:
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);
41 case FormulaType::FORALL:
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);
49 case FormulaType::TRUE:
51 _content.mProperties |= STRONG_CONDITIONS;
52 addConstraintProperties( std::get<Constraint<Pol>>(_content.mContent), _content.mProperties );
55 case FormulaType::FALSE:
57 _content.mProperties |= STRONG_CONDITIONS;
58 addConstraintProperties( std::get<Constraint<Pol>>(_content.mContent), _content.mProperties );
61 case FormulaType::BOOL:
63 _content.mProperties |= STRONG_CONDITIONS | PROP_CONTAINS_BOOLEAN;
66 case FormulaType::NOT:
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;
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)
81 Condition subFormulaConds = subFormula->properties();
82 if( !(PROP_IS_A_LITERAL<=subFormulaConds) )
84 _content.mProperties &= ~PROP_IS_A_CLAUSE;
85 _content.mProperties &= ~PROP_IS_IN_CNF;
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;
95 case FormulaType::AND:
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)
100 Condition subFormulaConds = subFormula->properties();
101 if( !(PROP_IS_A_CLAUSE<=subFormulaConds) )
103 _content.mProperties &= ~PROP_IS_PURE_CONJUNCTION;
104 _content.mProperties &= ~PROP_IS_LITERAL_CONJUNCTION;
105 _content.mProperties &= ~PROP_IS_IN_CNF;
107 else if( !(PROP_IS_A_LITERAL<=subFormulaConds) )
109 _content.mProperties &= ~PROP_IS_PURE_CONJUNCTION;
110 _content.mProperties &= ~PROP_IS_LITERAL_CONJUNCTION;
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;
122 case FormulaType::ITE:
123 case FormulaType::IMPLIES:
124 case FormulaType::IFF:
125 case FormulaType::XOR:
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)
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;
139 case FormulaType::CONSTRAINT:
141 _content.mProperties |= STRONG_CONDITIONS;
142 addConstraintProperties(std::get<Constraint<Pol>>(_content.mContent), _content.mProperties);
145 case FormulaType::VARCOMPARE:
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;
152 case FormulaType::VARASSIGN:
154 _content.mProperties |= STRONG_CONDITIONS; //| PROP_CONTAINS_REAL_VALUED_VARS | PROP_CONTAINS_INTEGER_VALUED_VARS;
155 _content.mProperties |= PROP_CONTAINS_ROOT_EXPRESSION;
158 case FormulaType::BITVECTOR:
160 _content.mProperties |= STRONG_CONDITIONS | PROP_CONTAINS_BITVECTOR;
163 case FormulaType::UEQ:
165 _content.mProperties |= STRONG_CONDITIONS | PROP_CONTAINS_UNINTERPRETED_EQUATIONS;
170 CARL_LOG_ERROR("carl.formula", "Undefined formula type " << _content.mType);
176 template<typename Pol>
177 void Formula<Pol>::addConstraintProperties( const Constraint<Pol>& _constraint, Condition& _properties )
179 if( carl::is_zero(_constraint.lhs()) )
181 _properties |= PROP_CONTAINS_LINEAR_POLYNOMIAL;
185 switch( _constraint.lhs().total_degree() )
188 _properties |= PROP_CONTAINS_LINEAR_POLYNOMIAL;
191 _properties |= PROP_CONTAINS_LINEAR_POLYNOMIAL;
194 _properties |= PROP_CONTAINS_NONLINEAR_POLYNOMIAL;
197 _properties |= PROP_CONTAINS_NONLINEAR_POLYNOMIAL;
198 _properties |= PROP_VARIABLE_DEGREE_GREATER_THAN_TWO;
201 _properties |= PROP_CONTAINS_NONLINEAR_POLYNOMIAL;
202 _properties |= PROP_VARIABLE_DEGREE_GREATER_THAN_THREE;
205 _properties |= PROP_CONTAINS_NONLINEAR_POLYNOMIAL;
206 _properties |= PROP_VARIABLE_DEGREE_GREATER_THAN_FOUR;
210 switch( _constraint.relation() )
213 _properties |= PROP_CONTAINS_EQUATION;
214 _properties |= PROP_CONTAINS_WEAK_INEQUALITY;
217 _properties |= PROP_CONTAINS_STRICT_INEQUALITY;
220 _properties |= PROP_CONTAINS_INEQUALITY;
221 _properties |= PROP_CONTAINS_WEAK_INEQUALITY;
224 _properties |= PROP_CONTAINS_INEQUALITY;
225 _properties |= PROP_CONTAINS_WEAK_INEQUALITY;
228 _properties |= PROP_CONTAINS_STRICT_INEQUALITY;
230 case Relation::GREATER:
231 _properties |= PROP_CONTAINS_STRICT_INEQUALITY;
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;