carl  25.02
Computer ARithmetic Library
Formula.h
Go to the documentation of this file.
1 /**
2  * @file Formula.h
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 #pragma once
11 
12 #include <cstring>
13 #include <functional>
14 #include <string>
15 #include <set>
16 #include <boost/dynamic_bitset.hpp>
17 #include "Condition.h"
18 #include "../arithmetic/Constraint.h"
19 #include "../uninterpreted/UEquality.h"
20 #include "../uninterpreted/UFManager.h"
21 #include "../bitvector/BVConstraintPool.h"
22 #include "../bitvector/BVConstraint.h"
25 #include "Logic.h"
26 
27 #include "FormulaContent.h"
28 
29 #include "functions/Variables.h"
30 
31 namespace carl
32 {
33  // Forward definition.
34  template<typename Pol>
35  class Formula;
36 
37  // Forward declaration
38  template<typename Pol>
39  class FormulaPool;
40 
41  /**
42  * Represent an SMT formula, which can be an atom for some background
43  * theory or a boolean combination of (sub)formulas.
44  */
45  template<typename Pol>
46  class Formula
47  {
48  friend class FormulaPool<Pol>;
49  friend class FormulaContent<Pol>;
50  template<typename P>
51  friend std::ostream& operator<<(std::ostream& os, const Formula<P>& f);
52 
53  public:
54  /// A constant iterator to a sub-formula of a formula.
56  /// A constant reverse iterator to a sub-formula of a formula.
58  /// A typedef for the template argument.
60 
61  private:
62  /**
63  * Adds the propositions of the given constraint to the propositions of this formula.
64  * @param _constraint The constraint to add propositions for.
65  * @param _properties
66  */
67  static void addConstraintProperties( const Constraint<Pol>& _constraint, Condition& _properties );
68 
69  // Members.
70 
71  /// The content of this formula.
73 
74 
75  explicit Formula( const FormulaContent<Pol>* _content ):
76  mpContent( _content )
77  {
78  if( _content != nullptr )
79  FormulaPool<Pol>::getInstance().reg( _content );
80  }
81 
82  #ifdef THREAD_SAFE
83  #define ACTIVITY_LOCK_GUARD std::lock_guard<std::mutex> lock1( mpContent->mActivityMutex );
84  #define VARIABLES_LOCK_GUARD std::lock_guard<std::mutex> lock3( mpContent->mVariablesMutex );
85  #else
86  #define ACTIVITY_LOCK_GUARD
87  #define VARIABLES_LOCK_GUARD
88  #endif
89 
90  public:
91 
92  /**
93  * Gets the propositions of this formula. It updates and stores the propositions
94  * if they are not up to date, hence this method is quite efficient.
95  */
96  static void init( FormulaContent<Pol>& _content );
97 
98  explicit Formula( FormulaType _type = FALSE ):
99  Formula( FormulaPool<Pol>::getInstance().create( _type ) )
100  {}
101 
102  explicit Formula( Variable::Arg _booleanVar ):
103  Formula( FormulaPool<Pol>::getInstance().create( _booleanVar ) )
104  {}
105 
106  explicit Formula( const Pol& _pol, Relation _rel ):
107  Formula( FormulaPool<Pol>::getInstance().create( Constraint<Pol>( _pol, _rel ) ) )
108  {}
109 
110  explicit Formula( const Constraint<Pol>& _constraint ):
111  Formula( FormulaPool<Pol>::getInstance().create( _constraint ) )
112  {}
113 
114  explicit Formula( const VariableComparison<Pol>& _variableComparison ):
115  Formula( FormulaPool<Pol>::getInstance().create( _variableComparison ) )
116  {}
117 
118  explicit Formula( const VariableAssignment<Pol>& _variableAssignment ):
119  Formula( FormulaPool<Pol>::getInstance().create( _variableAssignment ) )
120  {}
121 
122  explicit Formula( const BVConstraint& _constraint ):
123  Formula( FormulaPool<Pol>::getInstance().create( _constraint ) )
124  {}
125 
126  explicit Formula( FormulaType _type, Formula&& _subformula ):
127  Formula(FormulaPool<Pol>::getInstance().create(_type, std::move(_subformula)))
128  {}
129 
130  explicit Formula( FormulaType _type, const Formula& _subformula ):
131  Formula(FormulaPool<Pol>::getInstance().create(_type, std::move(Formula(_subformula))))
132  {}
133 
134  explicit Formula( FormulaType _type, const Formula& _subformulaA, const Formula& _subformulaB ):
135  Formula( FormulaPool<Pol>::getInstance().create( _type, {_subformulaA, _subformulaB} ))
136  {
137  assert( _type == FormulaType::AND || _type == FormulaType::IFF || _type == FormulaType::IMPLIES || _type == FormulaType::OR || _type == FormulaType::XOR );
138  }
139 
140  explicit Formula( FormulaType _type, const Formula& _subformulaA, const Formula& _subformulaB, const Formula& _subformulaC):
141  Formula( FormulaPool<Pol>::getInstance().create(_type, {_subformulaA, _subformulaB, _subformulaC}))
142  {}
143 
144  explicit Formula( FormulaType _type, const FormulasMulti<Pol>& _subformulas ):
145  Formula( FormulaPool<Pol>::getInstance().create( _subformulas ) )
146  {
147  assert( _type == FormulaType::XOR );
148  }
149 
150  explicit Formula( FormulaType _type, const Formulas<Pol>& _subasts ):
151  Formula( FormulaPool<Pol>::getInstance().create( _type, _subasts ) )
152  {}
153 
154  explicit Formula( FormulaType _type, Formulas<Pol>&& _subasts ):
155  Formula( FormulaPool<Pol>::getInstance().create( _type, std::move(_subasts) ) )
156  {}
157 
158  explicit Formula( FormulaType _type, const std::initializer_list<Formula<Pol>>& _subasts ):
159  Formula( FormulaPool<Pol>::getInstance().create( _type, std::move(Formulas<Pol>(_subasts.begin(), _subasts.end()) ) ))
160  {}
161 
162  explicit Formula( FormulaType _type, const FormulaSet<Pol>& _subasts ):
163  Formula( FormulaPool<Pol>::getInstance().create( _type, std::move(Formulas<Pol>(_subasts.begin(), _subasts.end()) ) ))
164  {}
165 
166  explicit Formula( FormulaType _type, FormulaSet<Pol>&& _subasts ):
167  Formula( FormulaPool<Pol>::getInstance().create( _type, std::move(Formulas<Pol>(_subasts.begin(), _subasts.end()) ) ))
168  {}
169 
170  explicit Formula( FormulaType _type, std::vector<Variable>&& _vars, const Formula& _term ):
171  Formula( FormulaPool<Pol>::getInstance().create( _type, std::move( _vars ), _term ) )
172  {}
173 
174  explicit Formula( FormulaType _type, const std::vector<Variable>& _vars, const Formula& _term ):
175  Formula( _type, std::move( std::vector<Variable>( _vars ) ), _term )
176  {}
177 
178  explicit Formula( FormulaType _type, std::vector<Variable>&& _vars, const Formula& _aux_term, const Formula& _term ):
179  Formula( FormulaPool<Pol>::getInstance().create( _type, std::move( _vars ), _aux_term, _term ) )
180  {}
181 
182  explicit Formula( FormulaType _type, const std::vector<Variable>& _vars, const Formula& _aux_term, const Formula& _term ):
183  Formula( _type, std::move( std::vector<Variable>( _vars ) ), _aux_term, _term )
184  {}
185 
186  explicit Formula( const UTerm& _lhs, const UTerm& _rhs, bool _negated ):
187  Formula( FormulaPool<Pol>::getInstance().create( _lhs, _rhs, _negated ) )
188  {}
189 
190  explicit Formula( UEquality&& _eq ):
191  Formula( FormulaPool<Pol>::getInstance().create( std::move( _eq ) ) )
192  {}
193 
194  explicit Formula( const UEquality& _eq ):
195  Formula( FormulaPool<Pol>::getInstance().create( std::move( UEquality( _eq ) ) ) )
196  {}
197 
198  Formula( const Formula& _formula ):
199  mpContent( _formula.mpContent )
200  {
201  if( _formula.mpContent != nullptr )
202  FormulaPool<Pol>::getInstance().reg( _formula.mpContent );
203  }
204 
205  Formula(Formula&& _formula) noexcept:
206  mpContent(_formula.mpContent)
207  {
208  _formula.mpContent = nullptr;
209  }
210 
212  {
213  if( mpContent != nullptr )
214  {
216  }
217  }
218 
219  Formula& operator=( const Formula& _formula )
220  {
221  if( _formula.mpContent != nullptr )
222  FormulaPool<Pol>::getInstance().reg( _formula.mpContent );
223  if( mpContent != nullptr )
225  mpContent = _formula.mpContent;
226  return *this;
227  }
228 
229  Formula& operator=( Formula&& _formula )
230  {
231  if( mpContent != nullptr )
233  mpContent = _formula.mpContent;
234  _formula.mpContent = nullptr;
235  return *this;
236  }
237 
238  // Methods.
239 
240  /**
241  * @return The activity for this formula, which means, how much is this formula involved in the solving procedure.
242  */
243  double activity() const
244  {
246  return mpContent->mActivity;
247  }
248 
249  /**
250  * Sets the activity to the given value.
251  * @param _activity The value to set the activity to.
252  */
253  void set_activity( double _activity ) const
254  {
256  mpContent->mActivity = _activity;
257  }
258 
259  /**
260  * @return The type of this formula.
261  */
263  {
264  return mpContent->mType;
265  }
266 
267  /**
268  * @return A hash value for this formula.
269  */
270  std::size_t hash() const
271  {
272  return mpContent->mHash;
273  }
274 
275  /**
276  * @return The unique id for this formula.
277  */
278  std::size_t id() const
279  {
280  return mpContent->mId;
281  }
282 
283  /**
284  * @return true, if this formula represents TRUE.
285  */
286  bool is_true() const
287  {
288  return mpContent->mType == FormulaType::TRUE;
289  }
290 
291  /**
292  * @return true, if this formula represents FALSE.
293  */
294  bool is_false() const
295  {
296  return mpContent->mType == FormulaType::FALSE;
297  }
298 
299  /**
300  * @return The bit-vector representing the propositions of this formula. For further information see the Condition class.
301  */
302  const Condition& properties() const
303  {
304  return mpContent->mProperties;
305  }
306 
307  const Variables& variables() const
308  {
310  if( mpContent->mpVariables == nullptr ) {
311  mpContent->mpVariables = new Variables(carl::variables(*this).as_set());
312  }
313  return *(mpContent->mpVariables);
314  }
315 
316  Formula negated() const
317  {
318  return Formula( mpContent->mNegation );
319  }
321  {
322  return Formula(FormulaPool<Pol>::getInstance().getBaseFormula(mpContent));
323  }
324 
325  const Formula& remove_negations() const
326  {
327  if( type() == FormulaType::NOT )
328  return subformula().remove_negations();
329  return *this;
330  }
331 
332  /**
333  * @return A constant reference to the only sub-formula, in case this formula is an negation.
334  */
335  const Formula& subformula() const
336  {
337  assert( mpContent->mType == NOT );
338  return std::get<Formula<Pol>>(mpContent->mContent);
339  }
340 
341  /**
342  * @return A constant reference to the premise, in case this formula is an implication.
343  */
344  const Formula& premise() const
345  {
346  assert( mpContent->mType == IMPLIES );
347  return std::get<Formulas<Pol>>(mpContent->mContent)[0];
348  }
349 
350  /**
351  * @return A constant reference to the conclusion, in case this formula is an implication.
352  */
353  const Formula& conclusion() const
354  {
355  assert( mpContent->mType == IMPLIES );
356  return std::get<Formulas<Pol>>(mpContent->mContent)[1];
357  }
358 
359  /**
360  * @return A constant reference to the condition, in case this formula is an ite-expression of formulas.
361  */
362  const Formula& condition() const
363  {
364  assert( mpContent->mType == ITE );
365  return std::get<Formulas<Pol>>(mpContent->mContent)[0];
366  }
367 
368  /**
369  * @return A constant reference to the then-case, in case this formula is an ite-expression of formulas.
370  */
371  const Formula& first_case() const
372  {
373  assert( mpContent->mType == ITE );
374  return std::get<Formulas<Pol>>(mpContent->mContent)[1];
375  }
376 
377  /**
378  * @return A constant reference to the else-case, in case this formula is an ite-expression of formulas.
379  */
380  const Formula& second_case() const
381  {
382  assert( mpContent->mType == ITE );
383  return std::get<Formulas<Pol>>(mpContent->mContent)[2];
384  }
385 
386  /**
387  * @return A constant reference to the quantifed variables, in case this formula is a quantified formula.
388  */
389  const std::vector<carl::Variable>& quantified_variables() const
390  {
391  if ( mpContent->mType == FormulaType::EXISTS || mpContent->mType == FormulaType::FORALL )
392  return std::get<QuantifierContent<Pol>>(mpContent->mContent).mVariables;
393  else {
394  assert (mpContent->mType == FormulaType::AUX_EXISTS );
395  return std::get<AuxQuantifierContent<Pol>>(mpContent->mContent).mVariables;
396  }
397  }
398 
399  /**
400  * @return A constant reference to the bound formula, in case this formula is a quantified formula.
401  */
403  {
404  if( mpContent->mType == FormulaType::EXISTS || mpContent->mType == FormulaType::FORALL)
405  return std::get<QuantifierContent<Pol>>(mpContent->mContent).mFormula;
406  else {
407  assert (mpContent->mType == FormulaType::AUX_EXISTS );
408  return std::get<AuxQuantifierContent<Pol>>(mpContent->mContent).mFormula;
409  }
410  }
411 
413  {
414  assert (mpContent->mType == FormulaType::AUX_EXISTS );
415  return std::get<AuxQuantifierContent<Pol>>(mpContent->mContent).mAuxFormula;
416  }
417 
418  /**
419  * @return A constant reference to the list of sub-formulas of this formula. Note, that
420  * this formula has to be a Boolean combination, if you invoke this method.
421  */
422  const Formulas<Pol>& subformulas() const
423  {
424  assert( is_nary() );
425  return std::get<Formulas<Pol>>(mpContent->mContent);
426  }
427 
428  /**
429  * @return A constant reference to the constraint represented by this formula. Note, that
430  * this formula has to be of type CONSTRAINT, if you invoke this method.
431  */
433  {
434  assert( mpContent->mType == FormulaType::CONSTRAINT || mpContent->mType == FormulaType::TRUE || mpContent->mType == FormulaType::FALSE );
435  return std::get<Constraint<Pol>>(mpContent->mContent);
436  }
437 
439  assert(mpContent->mType == FormulaType::VARCOMPARE);
440  return std::get<VariableComparison<Pol>>(mpContent->mContent);
441  }
442 
444  assert(mpContent->mType == FormulaType::VARASSIGN);
445  return std::get<VariableAssignment<Pol>>(mpContent->mContent);
446  }
447 
449  {
450  assert( mpContent->mType == FormulaType::BITVECTOR );
451  return std::get<BVConstraint>(mpContent->mContent);
452  }
453 
454  /**
455  * @return The name of the Boolean variable represented by this formula. Note, that
456  * this formula has to be of type BOOL, if you invoke this method.
457  */
459  {
460  assert( mpContent->mType == FormulaType::BOOL );
461  return std::get<carl::Variable>(mpContent->mContent);
462  }
463 
464  /**
465  * @return A constant reference to the uninterpreted equality represented by this formula. Note, that
466  * this formula has to be of type UEQ, if you invoke this method.
467  */
468  const UEquality& u_equality() const
469  {
470  assert( mpContent->mType == FormulaType::UEQ );
471  return std::get<UEquality>(mpContent->mContent);
472  }
473 
474  /**
475  * @return The number of sub-formulas of this formula.
476  */
477  size_t size() const
478  {
482  return 1;
483  else
484  return std::get<Formulas<Pol>>(mpContent->mContent).size();
485  }
486 
487  /**
488  * @return true, if this formula has sub-formulas;
489  * false, otherwise.
490  */
491  bool empty() const
492  {
494  || mpContent->mType == FormulaType::TRUE || mpContent->mType == FormulaType::FALSE
495  || mpContent->mType == FormulaType::BITVECTOR )
496  return false;
497  else
498  return std::get<Formulas<Pol>>(mpContent->mContent).empty();
499  }
500 
501  /**
502  * @return A constant iterator to the beginning of the list of sub-formulas of this formula.
503  */
505  {
506  assert( is_nary() );
507  return std::get<Formulas<Pol>>(mpContent->mContent).begin();
508  }
509 
510  /**
511  * @return A constant iterator to the end of the list of sub-formulas of this formula.
512  */
514  {
515  assert( is_nary() );
516  return std::get<Formulas<Pol>>(mpContent->mContent).end();
517  }
518 
519  /**
520  * @return A constant reverse iterator to the beginning of the list of sub-formulas of this formula.
521  */
523  {
524  assert( is_nary() );
525  return std::get<Formulas<Pol>>(mpContent->mContent).rbegin();
526  }
527 
528  /**
529  * @return A constant reverse iterator to the end of the list of sub-formulas of this formula.
530  */
532  {
533  assert( is_nary() );
534  return std::get<Formulas<Pol>>(mpContent->mContent).rend();
535  }
536 
537  /**
538  * @return A reference to the last sub-formula of this formula.
539  */
540  const Formula& back() const
541  {
542  assert( is_boolean_combination() );
543  if (mpContent->mType == FormulaType::NOT)
544  return std::get<Formula<Pol>>(mpContent->mContent);
545  else
546  return *(--(std::get<Formulas<Pol>>(mpContent->mContent).end()));
547  }
548 
549  /**
550  * Checks if the given property holds for this formula. (Very cheap operation which only relies on bit checks)
551  * @param _property The property to check this formula for.
552  * @return true, if the given property holds for this formula;
553  * false, otherwise.
554  */
555  bool property_holds( const Condition& _property ) const
556  {
557  return (mpContent->mProperties | ~_property) == ~PROP_TRUE;
558  }
559 
560  /**
561  * @return true, if this formula is a Boolean atom.
562  */
563  bool is_atom() const
564  {
565  return (mpContent->mType == FormulaType::CONSTRAINT || mpContent->mType == FormulaType::BOOL
568  || mpContent->mType == FormulaType::FALSE || mpContent->mType == FormulaType::TRUE);
569  }
570 
571  bool is_literal() const
572  {
574  }
575 
576  /**
577  * @return true, if the outermost operator of this formula is Boolean;
578  * false, otherwise.
579  */
581  {
582  return !is_atom();
583  }
584 
585  bool is_bound() const
586  {
588  if (mpContent->mType == FormulaType::NOT) {
589  if (std::get<Formula<Pol>>(mpContent->mContent).mpContent->mType != FormulaType::CONSTRAINT) return false;
590  return carl::is_bound(std::get<Constraint<Pol>>(std::get<Formula<Pol>>(mpContent->mContent).mpContent->mContent), true);
591  }
592  return false;
593  }
594 
595  /**
596  * @return true, if the type of this formulas allows n-ary combinations of sub-formulas, for an arbitrary n.
597  */
598  bool is_nary() const
599  {
600  return mpContent->is_nary();
601  }
602 
603  /**
604  * @return true, if this formula is a conjunction of constraints;
605  * false, otherwise.
606  */
608  {
610  return !(PROP_CONTAINS_BOOLEAN <= properties());
611  else
612  return false;
613  }
614 
615  /**
616  * @return true, if this formula is a conjunction of real constraints;
617  * false, otherwise.
618  */
620  {
623  else
624  return false;
625  }
626 
627  /**
628  * @return true, if this formula is a conjunction of integer constraints;
629  * false, otherwise.
630  */
632  {
635  else
636  return false;
637  }
638 
639  /**
640  * @return true, if this formula is propositional;
641  * false, otherwise.
642  */
644  {
650  }
651 
652  Logic logic() const {
658  return Logic::QF_BV;
659  } else if (!(carl::PROP_CONTAINS_BITVECTOR <= properties())
664  return Logic::QF_UF;
665  } else if (!(carl::PROP_CONTAINS_BITVECTOR <= properties())
670  return Logic::QF_PB;
671  } else if (!(carl::PROP_CONTAINS_BITVECTOR <= properties())
677  return Logic::QF_NIA;
678  } else {
679  return Logic::QF_LIA;
680  }
681  } else if (!(carl::PROP_CONTAINS_BITVECTOR <= properties())
687  return Logic::QF_NRA;
688  } else {
689  return Logic::QF_LRA;
690  }
691  } else if (!(carl::PROP_CONTAINS_BITVECTOR <= properties())
697  return Logic::QF_NIRA;
698  } else {
699  return Logic::QF_LIRA;
700  }
701  } else {
702  return Logic::UNDEFINED;
703  }
704  }
705 
706  /**
707  * @param _formula The pointer to the formula for which to check whether it points to a sub-formula
708  * of this formula.
709  * @return true, the given pointer to a formula points to a sub-formula of this formula;
710  * false, otherwise.
711  */
712  bool contains( const Formula& _formula ) const
713  {
714  if( *this == _formula )
715  return true;
716  if( is_atom() )
717  return false;
718  if( mpContent->mType == FormulaType::NOT )
719  return std::get<Formula<Pol>>(mpContent->mContent) == _formula;
720  else
721  return std::find(std::get<Formulas<Pol>>(mpContent->mContent).begin(), std::get<Formulas<Pol>>(mpContent->mContent).end(), _formula) != std::get<Formulas<Pol>>(mpContent->mContent).end();
722  }
723 
724  /**
725  * @param _formula The formula to compare with.
726  * @return true, if this formula and the given formula are equal;
727  * false, otherwise.
728  */
729  bool operator==( const Formula& _formula ) const
730  {
731  return mpContent == _formula.mpContent;
732  }
733 
734  /**
735  * @param _formula The formula to compare with.
736  * @return true, if this formula and the given formula are not equal.
737  */
738  bool operator!=( const Formula& _formula ) const
739  {
740  return mpContent != _formula.mpContent;
741  }
742 
743  /**
744  * @param _formula The formula to compare with.
745  * @return true, if the id of this formula is less than the id of the given one.
746  */
747  bool operator<( const Formula& _formula ) const
748  {
749  assert( mpContent->mId != 0 );
750  assert( _formula.id() != 0 );
751  return mpContent->mId < _formula.id();
752  }
753 
754  /**
755  * @param _formula The formula to compare with.
756  * @return true, if the id of this formula is greater than the id of the given one.
757  */
758  bool operator>( const Formula& _formula ) const
759  {
760  assert( mpContent->mId != 0 );
761  assert( _formula.id() != 0 );
762  return mpContent->mId > _formula.id();
763  }
764 
765  /**
766  * @param _formula The formula to compare with.
767  * @return true, if the id of this formula is less or equal than the id of the given one.
768  */
769  bool operator<=( const Formula& _formula ) const
770  {
771  assert( mpContent->mId != 0 );
772  assert( _formula.id() != 0 );
773  return mpContent->mId <= _formula.id();
774  }
775 
776  /**
777  * @param _formula The formula to compare with.
778  * @return true, if the id of this formula is greater or equal than the id of the given one.
779  */
780  bool operator>=( const Formula& _formula ) const
781  {
782  assert( mpContent->mId != 0 );
783  assert( _formula.id() != 0 );
784  return mpContent->mId >= _formula.id();
785  }
786 
787  Formula operator!() const {
788  return negated();
789  }
790  };
791 
792  /**
793  * The output operator of a formula.
794  * @param os The stream to print on.
795  * @param f The formula to print.
796  */
797  template<typename P>
798  inline std::ostream& operator<<(std::ostream& os, const Formula<P>& f) {
799  return os << *f.mpContent;
800  }
801 } // namespace carl
802 
803 namespace std
804 {
805  /**
806  * Implements std::hash for formula contents.
807  */
808  template<typename Pol>
809  struct hash<carl::FormulaContent<Pol>>
810  {
811  public:
812  /**
813  * @param _formulaContent The formula content to get the hash for.
814  * @return The hash of the given formula content.
815  */
816  std::size_t operator()( const carl::FormulaContent<Pol>& _formulaContent ) const
817  {
818  return _formulaContent.hash();
819  }
820  };
821 
822  /**
823  * Implements std::hash for formulas.
824  */
825  template<typename Pol>
826  struct hash<carl::Formula<Pol>>
827  {
828  public:
829  /**
830  * @param _formula The formula to get the hash for.
831  * @return The hash of the given formula.
832  */
833  std::size_t operator()( const carl::Formula<Pol>& _formula ) const
834  {
835  return _formula.hash();
836  }
837  };
838 } // namespace std
839 
840 #include "Formula.tpp"
#define ACTIVITY_LOCK_GUARD
Definition: Formula.h:86
#define VARIABLES_LOCK_GUARD
Definition: Formula.h:87
MultivariatePolynomial< Rational > Pol
Definition: HornerTest.cpp:17
carl is the main namespace for the library.
FormulaType
Represent the type of a formula to allow faster/specialized processing.
@ CONSTRAINT
@ BITVECTOR
@ VARCOMPARE
@ AUX_EXISTS
@ VARASSIGN
static constexpr Condition PROP_CONTAINS_NONLINEAR_POLYNOMIAL
Definition: Condition.h:69
std::set< Formula< Poly > > FormulaSet
std::ostream & operator<<(std::ostream &os, const BasicConstraint< Poly > &c)
Prints the given constraint on the given stream.
static constexpr Condition PROP_CONTAINS_BOOLEAN
Definition: Condition.h:71
static constexpr Condition PROP_TRUE
Definition: Condition.h:49
bool is_bound(const BasicConstraint< Pol > &constr)
Definition: Bound.h:11
static constexpr Condition PROP_IS_A_LITERAL
Definition: Condition.h:56
std::vector< Formula< Poly > > Formulas
static constexpr Condition PROP_IS_PURE_CONJUNCTION
Definition: Condition.h:54
Logic
Definition: Logic.h:7
static constexpr Condition PROP_CONTAINS_UNINTERPRETED_EQUATIONS
Definition: Condition.h:74
static constexpr Condition PROP_CONTAINS_INTEGER_VALUED_VARS
Definition: Condition.h:72
static constexpr Condition PROP_CONTAINS_REAL_VALUED_VARS
Definition: Condition.h:73
std::multiset< Formula< Poly > > FormulasMulti
Relation
Definition: Relation.h:20
static constexpr Condition PROP_CONTAINS_BITVECTOR
Definition: Condition.h:75
void variables(const BasicConstraint< Pol > &c, carlVariables &vars)
std::set< Variable > Variables
Definition: Common.h:18
static constexpr Condition PROP_CONTAINS_PSEUDOBOOLEAN
Definition: Condition.h:76
auto & get(const std::string &name)
A Variable represents an algebraic variable that can be used throughout carl.
Definition: Variable.h:85
Represent a sum type/variant of an (in)equality between a variable on the left-hand side and multivar...
static FormulaPool< Pol > & getInstance()
Returns the single instance of this class by reference.
Definition: Singleton.h:45
Represent a polynomial (in)equality against zero.
Definition: Constraint.h:62
Represent an SMT formula, which can be an atom for some background theory or a boolean combination of...
Definition: Formula.h:47
const VariableAssignment< Pol > & variable_assignment() const
Definition: Formula.h:443
const FormulaContent< Pol > * mpContent
The content of this formula.
Definition: Formula.h:72
const Formula & subformula() const
Definition: Formula.h:335
bool operator==(const Formula &_formula) const
Definition: Formula.h:729
Formula(const Formula &_formula)
Definition: Formula.h:198
const_iterator begin() const
Definition: Formula.h:504
Formula(FormulaType _type, const Formula &_subformula)
Definition: Formula.h:130
Formula(FormulaType _type, const std::vector< Variable > &_vars, const Formula &_term)
Definition: Formula.h:174
Formula(const Pol &_pol, Relation _rel)
Definition: Formula.h:106
bool is_constraint_conjunction() const
Definition: Formula.h:607
const VariableComparison< Pol > & variable_comparison() const
Definition: Formula.h:438
const Formula & premise() const
Definition: Formula.h:344
Formula(FormulaType _type=FALSE)
Definition: Formula.h:98
Pol PolynomialType
A typedef for the template argument.
Definition: Formula.h:59
const Formula & conclusion() const
Definition: Formula.h:353
const Formula & quantified_formula() const
Definition: Formula.h:402
Logic logic() const
Definition: Formula.h:652
carl::Variable::Arg boolean() const
Definition: Formula.h:458
bool is_nary() const
Definition: Formula.h:598
bool is_only_propositional() const
Definition: Formula.h:643
Formula(FormulaType _type, std::vector< Variable > &&_vars, const Formula &_aux_term, const Formula &_term)
Definition: Formula.h:178
bool is_integer_constraint_conjunction() const
Definition: Formula.h:631
Formula(FormulaType _type, const Formula &_subformulaA, const Formula &_subformulaB, const Formula &_subformulaC)
Definition: Formula.h:140
bool is_bound() const
Definition: Formula.h:585
bool is_real_constraint_conjunction() const
Definition: Formula.h:619
typename Formulas< Pol >::const_iterator const_iterator
A constant iterator to a sub-formula of a formula.
Definition: Formula.h:55
bool contains(const Formula &_formula) const
Definition: Formula.h:712
const Formula & remove_negations() const
Definition: Formula.h:325
double activity() const
Definition: Formula.h:243
bool is_atom() const
Definition: Formula.h:563
Formula(const FormulaContent< Pol > *_content)
Definition: Formula.h:75
const Constraint< Pol > & constraint() const
Definition: Formula.h:432
Formula(Variable::Arg _booleanVar)
Definition: Formula.h:102
const std::vector< carl::Variable > & quantified_variables() const
Definition: Formula.h:389
Formula & operator=(const Formula &_formula)
Definition: Formula.h:219
bool property_holds(const Condition &_property) const
Checks if the given property holds for this formula.
Definition: Formula.h:555
const Formulas< Pol > & subformulas() const
Definition: Formula.h:422
Formula(const BVConstraint &_constraint)
Definition: Formula.h:122
bool empty() const
Definition: Formula.h:491
static void init(FormulaContent< Pol > &_content)
Gets the propositions of this formula.
Formula(const Constraint< Pol > &_constraint)
Definition: Formula.h:110
const Formula & first_case() const
Definition: Formula.h:371
const_reverse_iterator rbegin() const
Definition: Formula.h:522
Formula(Formula &&_formula) noexcept
Definition: Formula.h:205
bool operator>=(const Formula &_formula) const
Definition: Formula.h:780
const_reverse_iterator rend() const
Definition: Formula.h:531
Formula(const UTerm &_lhs, const UTerm &_rhs, bool _negated)
Definition: Formula.h:186
Formula operator!() const
Definition: Formula.h:787
typename Formulas< Pol >::const_reverse_iterator const_reverse_iterator
A constant reverse iterator to a sub-formula of a formula.
Definition: Formula.h:57
bool operator<=(const Formula &_formula) const
Definition: Formula.h:769
size_t size() const
Definition: Formula.h:477
bool operator<(const Formula &_formula) const
Definition: Formula.h:747
const Formula & second_case() const
Definition: Formula.h:380
Formula(FormulaType _type, Formulas< Pol > &&_subasts)
Definition: Formula.h:154
const BVConstraint & bv_constraint() const
Definition: Formula.h:448
std::size_t id() const
Definition: Formula.h:278
Formula(FormulaType _type, const FormulaSet< Pol > &_subasts)
Definition: Formula.h:162
Formula(FormulaType _type, const Formula &_subformulaA, const Formula &_subformulaB)
Definition: Formula.h:134
Formula(FormulaType _type, std::vector< Variable > &&_vars, const Formula &_term)
Definition: Formula.h:170
const UEquality & u_equality() const
Definition: Formula.h:468
friend std::ostream & operator<<(std::ostream &os, const Formula< P > &f)
The output operator of a formula.
Definition: Formula.h:798
const Formula & quantified_aux_formula() const
Definition: Formula.h:412
bool operator!=(const Formula &_formula) const
Definition: Formula.h:738
Formula(FormulaType _type, const std::vector< Variable > &_vars, const Formula &_aux_term, const Formula &_term)
Definition: Formula.h:182
bool is_literal() const
Definition: Formula.h:571
FormulaType type() const
Definition: Formula.h:262
Formula(FormulaType _type, const Formulas< Pol > &_subasts)
Definition: Formula.h:150
bool is_false() const
Definition: Formula.h:294
Formula(FormulaType _type, FormulaSet< Pol > &&_subasts)
Definition: Formula.h:166
Formula base_formula() const
Definition: Formula.h:320
Formula negated() const
Definition: Formula.h:316
void set_activity(double _activity) const
Sets the activity to the given value.
Definition: Formula.h:253
bool is_true() const
Definition: Formula.h:286
Formula & operator=(Formula &&_formula)
Definition: Formula.h:229
Formula(FormulaType _type, const std::initializer_list< Formula< Pol >> &_subasts)
Definition: Formula.h:158
std::size_t hash() const
Definition: Formula.h:270
const_iterator end() const
Definition: Formula.h:513
const Condition & properties() const
Definition: Formula.h:302
Formula(UEquality &&_eq)
Definition: Formula.h:190
static void addConstraintProperties(const Constraint< Pol > &_constraint, Condition &_properties)
Adds the propositions of the given constraint to the propositions of this formula.
bool is_boolean_combination() const
Definition: Formula.h:580
Formula(const UEquality &_eq)
Definition: Formula.h:194
Formula(FormulaType _type, Formula &&_subformula)
Definition: Formula.h:126
bool operator>(const Formula &_formula) const
Definition: Formula.h:758
const Variables & variables() const
Definition: Formula.h:307
const Formula & condition() const
Definition: Formula.h:362
Formula(const VariableAssignment< Pol > &_variableAssignment)
Definition: Formula.h:118
const Formula & back() const
Definition: Formula.h:540
Formula(const VariableComparison< Pol > &_variableComparison)
Definition: Formula.h:114
Formula(FormulaType _type, const FormulasMulti< Pol > &_subformulas)
Definition: Formula.h:144
std::size_t operator()(const carl::FormulaContent< Pol > &_formulaContent) const
Definition: Formula.h:816
std::size_t operator()(const carl::Formula< Pol > &_formula) const
Definition: Formula.h:833
std::size_t hash() const
Implements an uninterpreted equality, that is an equality of either two uninterpreted function instan...
Definition: UEquality.h:23
Implements an uninterpreted term, that is either an uninterpreted variable or an uninterpreted functi...
Definition: UTerm.h:22