carl  25.02
Computer ARithmetic Library
FormulaContent.h
Go to the documentation of this file.
1 #pragma once
2 
4 
5 #include <iostream>
6 #include <variant>
7 
8 namespace carl {
9  // Forward declaration.
10  template<typename Pol>
11  class Formula;
12  // Forward declaration.
13  template<typename Pol>
14  class FormulaPool;
15 
16 
17  template<typename Poly>
18  using Formulas = std::vector<Formula<Poly>>;
19  template<typename Poly>
20  using FormulaSet = std::set<Formula<Poly>>;
21  template<typename Poly>
22  using FormulasMulti = std::multiset<Formula<Poly>>;
23 
24 
25  ///
26  /**
27  * Represent the type of a formula to allow faster/specialized processing.
28  *
29  * For each (supported) SMTLIB theory, we have
30  * - Constants
31  * - Variables
32  * - Functions
33  * - Additional functions (not specified, but used in the wild)
34  */
35  enum FormulaType {
36  // Generic
38 
39  // Core Theory
43  IFF,
44 
45  // Arithmetic Theory
49 
50  // Bitvector Theory
52 
53  // Uninterpreted Theory
54  UEQ
55  };
56 
57 
58 
59  /**
60  * @param _type The formula type to get the string representation for.
61  * @return The string representation of the given type.
62  */
63  inline std::string formulaTypeToString(FormulaType _type) {
64  switch (_type) {
65  case FormulaType::ITE: return "ite";
66  case FormulaType::EXISTS: return "exists";
67  case FormulaType::FORALL: return "forall";
68  case FormulaType::AUX_EXISTS: return "aux_exists";
69  case FormulaType::TRUE: return "true";
70  case FormulaType::FALSE: return "false";
71  case FormulaType::BOOL: return "bool";
72  case FormulaType::NOT: return "not";
73  case FormulaType::IMPLIES: return "=>";
74  case FormulaType::AND: return "and";
75  case FormulaType::OR: return "or";
76  case FormulaType::XOR: return "xor";
77  case FormulaType::IFF: return "=";
78  case FormulaType::CONSTRAINT: return "constraint";
79  case FormulaType::VARCOMPARE: return "varcompare";
80  case FormulaType::VARASSIGN: return "varassign";
81  case FormulaType::BITVECTOR: return "bv";
82  case FormulaType::UEQ: return "ueq";
83  default:
84  CARL_LOG_ERROR("carl.formula", "Unknown formula type " << unsigned(_type));
85  return "???";
86  }
87  }
88  inline std::ostream& operator<<(std::ostream& os, FormulaType t) {
89  return os << formulaTypeToString(t);
90  }
91 
92  /**
93  * Stores the variables and the formula bound by a quantifier.
94  */
95  template<typename Pol>
97  {
98  /// The quantified variables.
99  std::vector<carl::Variable> mVariables;
100  /// The formula bound by this quantifier.
102 
103  /**
104  * Constructs the content of a quantified formula.
105  * @param _vars The quantified variables.
106  * @param _formula The formula bound by this quantifier.
107  */
108  QuantifierContent( std::vector<carl::Variable>&& _vars, Formula<Pol>&& _formula ):
109  mVariables( std::move(_vars) ),
110  mFormula( std::move(_formula) )
111  {}
112 
113  /**
114  * Checks this content of a quantified formula and the given content of a quantified formula is equal.
115  * @param _qc The content of a quantified formula to check for equality.
116  * @return true, if this content of a quantified formula and the given content of a quantified formula is equal.
117  */
118  bool operator==(const QuantifierContent& _qc) const
119  {
120  return (mFormula == _qc.mFormula) && (mVariables == _qc.mVariables);
121  }
122  };
123 
124  template<typename Pol>
126  {
127  /// The quantified variables.
128  std::vector<carl::Variable> mVariables;
129  /// The guard.
131  /// The formula bound by this quantifier.
133 
134  AuxQuantifierContent( std::vector<carl::Variable>&& _vars, Formula<Pol>&& _aux_formula, Formula<Pol>&& _formula ):
135  mVariables( std::move(_vars) ),
136  mAuxFormula( std::move(_aux_formula) ),
137  mFormula( std::move(_formula) )
138  {}
139 
140  bool operator==(const AuxQuantifierContent& _qc) const
141  {
142  return (mAuxFormula == _qc.mAuxFormula) && (mFormula == _qc.mFormula) && (mVariables == _qc.mVariables);
143  }
144  };
145 
146  template<typename Pol>
147  class FormulaContent : public boost::intrusive::unordered_set_base_hook<>
148  {
149  friend class Formula<Pol>;
150  friend class FormulaPool<Pol>;
151  template<typename P>
152  friend std::ostream& operator<<(std::ostream& os, const FormulaContent<P>& f);
153 
154  private:
155 
156  // Member.
157  /// The hash value.
158  size_t mHash = 0;
159  /// The unique id.
160  size_t mId = 0;
161  /// The activity for this formula, which means, how much is this formula involved in the solving procedure.
162  mutable double mActivity = 0.0;
163  /// The number of formulas existing with this content.
164  mutable size_t mUsages = 0;
165  /// The type of this formula.
167  /// The content of this formula.
168  std::variant<carl::Variable, // The variable, in case this formula wraps a variable.
169  Constraint<Pol>, // The constraint, in case this formula wraps a constraint.
170  VariableComparison<Pol>, // A constraint comparing a single variable with a value.
171  VariableAssignment<Pol>, // A constraint assigning a single variable to a value.
172  BVConstraint, // The bitvector constraint.
173  UEquality, // The uninterpreted equality, in case this formula wraps an uninterpreted equality.
174  Formula<Pol>, // The only sub-formula, in case this formula is an negation.
175  Formulas<Pol>, // The subformulas, in case this formula is a n-nary operation as AND, OR, IFF or XOR.
177  AuxQuantifierContent<Pol>> mContent; // The quantifed variables and the bound formula, in case this formula is a quantified formula.
178  /// The negation
179  const FormulaContent<Pol> *mNegation = nullptr;
180  /// The propositions of this formula.
182  #ifdef THREAD_SAFE
183  /// Mutex for access to activity.
184  mutable std::mutex mActivityMutex;
185  /// Mutex for collecting the variables within this formula.
186  mutable std::mutex mVariablesMutex;
187  #endif
188  /// Container collecting the variables which occur in this formula.
189  mutable Variables* mpVariables = nullptr;
190 
191  FormulaContent() = delete;
192  FormulaContent(const FormulaContent&) = delete;
194 
195  /**
196  * Constructs the formula (true), if the given bool is true and the formula (false) otherwise.
197  * @param _true Specifies whether to create the formula (true) or (false).
198  * @param _id A unique id of the formula to create.
199  */
200  FormulaContent(FormulaType _type, std::size_t _id = 0);
201 
202  /**
203  * Constructs a formula being a variable.
204  * @param _variable
205  */
207 
208  /**
209  * Constructs a formula being a constraint.
210  * @param _constraint The pointer to the constraint.
211  */
213 
214  FormulaContent(VariableComparison<Pol>&& _variableComparison);
215 
216  FormulaContent(VariableAssignment<Pol>&& _variableAssignment);
217 
218  /**
219  * Constructs a formula being a bitvector constraint.
220  * @param _constraint The pointer to the constraint.
221  */
222  FormulaContent(BVConstraint&& _constraint);
223 
224  /**
225  * Constructs a formula being an uninterpreted equality.
226  * @param _ueq The pointer to the constraint.
227  */
229 
230  /**
231  * Constructs a formula of the given type with a single subformula. This is usually a negation.
232  */
233  FormulaContent(FormulaType _type, Formula<Pol>&& _subformula);
234 
235  FormulaContent(FormulaType _type, const std::initializer_list<Formula<Pol>>& _subformula);
236  FormulaContent(FormulaType _type, Formulas<Pol>&& _subformula);
237 
238 
239  /**
240  * Constructs a quantifier expression: (exists (vars) term) or (forall (vars) term)
241  * @param _type The type of the quantifier to construct.
242  * @param _vars The variables that are bound.
243  * @param _term The term in which the variables are bound.
244  */
245  FormulaContent(FormulaType _type, std::vector<carl::Variable>&& _vars, const Formula<Pol>& _term);
246 
247  FormulaContent(FormulaType _type, std::vector<carl::Variable>&& _vars, const Formula<Pol>& _aux_term, const Formula<Pol>& _term);
248 
249 
250 
251  public:
252 
253  /**
254  * Destructor.
255  */
257  if( mpVariables != nullptr )
258  delete mpVariables;
259  }
260 
261  std::size_t hash() const {
262  return mHash;
263  }
264  std::size_t id() const {
265  return mId;
266  }
267 
268  bool is_nary() const
269  {
270  switch (mType) {
271  case FormulaType::TRUE: return false;
272  case FormulaType::FALSE: return false;
273  case FormulaType::BOOL: return false;
274  case FormulaType::NOT: return false;
275  case FormulaType::IMPLIES: return true;
276  case FormulaType::AND: return true;
277  case FormulaType::OR: return true;
278  case FormulaType::XOR: return true;
279  case FormulaType::IFF: return true;
280  case FormulaType::ITE: return true;
281  case FormulaType::EXISTS: return false;
282  case FormulaType::AUX_EXISTS: return false;
283  case FormulaType::FORALL: return false;
284  case FormulaType::CONSTRAINT: return false;
285  case FormulaType::VARCOMPARE: return false;
286  case FormulaType::VARASSIGN: return false;
287  case FormulaType::BITVECTOR: return false;
288  case FormulaType::UEQ: return false;
289  }
290  return false;
291  }
292 
293  bool operator==(const FormulaContent& _content) const;
294  };
295  /**
296  * The output operator of a formula.
297  * @param os The stream to print on.
298  * @param f
299  */
300  template<typename Pol>
301  std::ostream& operator<<(std::ostream& os, const FormulaContent<Pol>& f) {
302  switch (f.mType) {
303  case FormulaType::FALSE:
304  return os << formulaTypeToString(f.mType);
305  case FormulaType::TRUE:
306  return os << formulaTypeToString(f.mType);
307  case FormulaType::BOOL:
308  return os << std::get<carl::Variable>(f.mContent);
310  return os << std::get<Constraint<Pol>>(f.mContent);
312  return os << std::get<VariableAssignment<Pol>>(f.mContent);
314  return os << std::get<VariableComparison<Pol>>(f.mContent);
316  return os << std::get<BVConstraint>(f.mContent);
317  case FormulaType::UEQ:
318  return os << std::get<UEquality>(f.mContent);
319  case FormulaType::NOT:
320  return os << "!(" << std::get<Formula<Pol>>(f.mContent) << ")";
321  case FormulaType::EXISTS:
322  os << "(exists";
323  for (auto v: std::get<QuantifierContent<Pol>>(f.mContent).mVariables) os << " " << v;
324  return os << ")(" << std::get<QuantifierContent<Pol>>(f.mContent).mFormula << ")";
326  os << "(aux_exists";
327  for (auto v: std::get<AuxQuantifierContent<Pol>>(f.mContent).mVariables) os << " " << v;
328  return os << ")(" << std::get<AuxQuantifierContent<Pol>>(f.mContent).mAuxFormula << ")(" << std::get<AuxQuantifierContent<Pol>>(f.mContent).mFormula << ")";
329  case FormulaType::FORALL:
330  os << "(forall";
331  for (auto v: std::get<QuantifierContent<Pol>>(f.mContent).mVariables) os << " " << v;
332  return os << ")(" << std::get<QuantifierContent<Pol>>(f.mContent).mFormula << ")";
333  default:
334  assert(f.is_nary());
335  return os << "(" << carl::stream_joined(" " + formulaTypeToString(f.mType) + " ", std::get<Formulas<Pol>>(f.mContent)) << ")";
336  }
337  }
338 
339  template<typename Pol>
340  std::ostream& operator<<(std::ostream& os, const FormulaContent<Pol>* fc) {
341  assert(fc != nullptr);
342  return os << *fc;
343  }
344 
345 }
346 
347 #include "FormulaContent.tpp"
A small wrapper that configures logging for carl.
#define CARL_LOG_ERROR(channel, msg)
Definition: carl-logging.h:40
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
std::set< Formula< Poly > > FormulaSet
std::ostream & operator<<(std::ostream &os, const BasicConstraint< Poly > &c)
Prints the given constraint on the given stream.
std::vector< Formula< Poly > > Formulas
std::string formulaTypeToString(FormulaType _type)
auto stream_joined(const std::string &glue, const T &v)
Allows to easily output some container with all elements separated by some string.
std::multiset< Formula< Poly > > FormulasMulti
std::set< Variable > Variables
Definition: Common.h:18
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...
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
Stores the variables and the formula bound by a quantifier.
Formula< Pol > mFormula
The formula bound by this quantifier.
QuantifierContent(std::vector< carl::Variable > &&_vars, Formula< Pol > &&_formula)
Constructs the content of a quantified formula.
bool operator==(const QuantifierContent &_qc) const
Checks this content of a quantified formula and the given content of a quantified formula is equal.
std::vector< carl::Variable > mVariables
The quantified variables.
Formula< Pol > mFormula
The formula bound by this quantifier.
Formula< Pol > mAuxFormula
The guard.
AuxQuantifierContent(std::vector< carl::Variable > &&_vars, Formula< Pol > &&_aux_formula, Formula< Pol > &&_formula)
std::vector< carl::Variable > mVariables
The quantified variables.
bool operator==(const AuxQuantifierContent &_qc) const
FormulaContent(const FormulaContent &)=delete
~FormulaContent()
Destructor.
Variables * mpVariables
Container collecting the variables which occur in this formula.
bool operator==(const FormulaContent &_content) const
std::size_t hash() const
friend std::ostream & operator<<(std::ostream &os, const FormulaContent< P > &f)
double mActivity
The activity for this formula, which means, how much is this formula involved in the solving procedur...
FormulaContent(FormulaType _type, Formulas< Pol > &&_subformula)
FormulaContent(FormulaType _type, std::size_t _id=0)
Constructs the formula (true), if the given bool is true and the formula (false) otherwise.
FormulaContent(FormulaType _type, const std::initializer_list< Formula< Pol >> &_subformula)
std::size_t id() const
FormulaType mType
The type of this formula.
FormulaContent(FormulaContent &&o)
FormulaContent(VariableAssignment< Pol > &&_variableAssignment)
FormulaContent(FormulaType _type, std::vector< carl::Variable > &&_vars, const Formula< Pol > &_term)
Constructs a quantifier expression: (exists (vars) term) or (forall (vars) term)
size_t mUsages
The number of formulas existing with this content.
FormulaContent(FormulaType _type, Formula< Pol > &&_subformula)
Constructs a formula of the given type with a single subformula.
FormulaContent(UEquality &&_ueq)
Constructs a formula being an uninterpreted equality.
const FormulaContent< Pol > * mNegation
The negation.
Condition mProperties
The propositions of this formula.
FormulaContent(Constraint< Pol > &&_constraint)
Constructs a formula being a constraint.
FormulaContent(Variable _variable)
Constructs a formula being a variable.
FormulaContent(BVConstraint &&_constraint)
Constructs a formula being a bitvector constraint.
FormulaContent(FormulaType _type, std::vector< carl::Variable > &&_vars, const Formula< Pol > &_aux_term, const Formula< Pol > &_term)
size_t mId
The unique id.
std::variant< carl::Variable, Constraint< Pol >, VariableComparison< Pol >, VariableAssignment< Pol >, BVConstraint, UEquality, Formula< Pol >, Formulas< Pol >, QuantifierContent< Pol >, AuxQuantifierContent< Pol > > mContent
The content of this formula.
FormulaContent(VariableComparison< Pol > &&_variableComparison)
size_t mHash
The hash value.
Implements an uninterpreted equality, that is an equality of either two uninterpreted function instan...
Definition: UEquality.h:23