SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Common.h
Go to the documentation of this file.
1 #pragma once
2 
4 
5 #include <boost/variant.hpp>
6 
7 #include <iostream>
8 #include <sstream>
9 
10 namespace smtrat {
11 namespace parser {
12 
13  struct TheoryError {
14  private:
15  std::stringstream ss;
16  std::string currentTheory;
17  public:
18  TheoryError& operator()(const std::string& theory) {
19  currentTheory = theory;
20  return *this;
21  }
22  friend inline std::ostream& operator<<(std::ostream& os, const TheoryError& te) {
23  return os << te.ss.str();
24  }
26  ss << std::endl << "\t" << currentTheory << ": ";
27  return *this;
28  }
29  template<typename T>
30  TheoryError& operator<<(const T& t) {
31  ss << t;
32  return *this;
33  }
34  };
35 
36  struct Identifier {
37  std::string symbol;
38  std::vector<std::size_t>* indices;
39  Identifier(): symbol(""), indices(nullptr) {}
40  Identifier(const std::string& symbol): symbol(symbol), indices(nullptr) {}
41  Identifier(const std::string& symbol, const std::vector<std::size_t>& indices): symbol(symbol), indices(new std::vector<std::size_t>(indices)) {}
42  Identifier(const std::string& symbol, const std::vector<Integer>& indices): symbol(symbol), indices(new std::vector<std::size_t>(indices.size())) {
43  for (std::size_t i = 0; i < indices.size(); i++) {
44  (*this->indices)[i] = carl::to_int<carl::uint>(indices[i]);
45  }
46  }
48  symbol = i.symbol;
49  delete indices;
50  indices = nullptr;
51  if (i.indices != nullptr) indices = new std::vector<std::size_t>(*i.indices);
52  return *this;
53  }
54  Identifier(const Identifier& i) {
55  symbol = i.symbol;
56  indices = nullptr;
57  if (i.indices != nullptr) indices = new std::vector<std::size_t>(*i.indices);
58  }
60  delete indices;
61  }
62  operator std::string() const {
63  if (indices == nullptr || indices->size() == 0) {
64  return symbol;
65  }
66  std::stringstream ss;
67  ss << symbol << "|" << indices->front();
68  for (std::size_t i = 1; i < indices->size(); i++) ss << "," << (*indices)[i];
69  return ss.str();
70  }
71  };
72  inline std::ostream& operator<<(std::ostream& os, const Identifier& identifier) {
73  return os << std::string(identifier);
74  }
75 
76  template<typename T>
77  struct SExpressionSequence;
78  template<typename T>
79  using SExpression = boost::variant<T, boost::recursive_wrapper<SExpressionSequence<T>>>;
80  template<typename T>
81  struct SExpressionSequence: public std::vector<SExpression<T>> {
82  SExpressionSequence(const std::vector<SExpression<T>>& v): std::vector<SExpression<T>>(v) {}
83  SExpressionSequence(std::vector<SExpression<T>>&& v): std::vector<SExpression<T>>(std::move(v)) {}
84  };
85  template<typename T>
86  inline std::ostream& operator<<(std::ostream& os, const SExpressionSequence<T>& ses) {
87  return os << std::vector<SExpression<T>>(ses);
88  }
89 
90 }
91 }
std::ostream & operator<<(std::ostream &os, OptimizationType ot)
boost::variant< T, boost::recursive_wrapper< SExpressionSequence< T > >> SExpression
Definition: Common.h:79
Class to create the formulas for axioms.
Identifier(const std::string &symbol)
Definition: Common.h:40
Identifier & operator=(const Identifier &i)
Definition: Common.h:47
std::string symbol
Definition: Common.h:37
std::vector< std::size_t > * indices
Definition: Common.h:38
Identifier(const Identifier &i)
Definition: Common.h:54
Identifier(const std::string &symbol, const std::vector< std::size_t > &indices)
Definition: Common.h:41
Identifier(const std::string &symbol, const std::vector< Integer > &indices)
Definition: Common.h:42
SExpressionSequence(const std::vector< SExpression< T >> &v)
Definition: Common.h:82
SExpressionSequence(std::vector< SExpression< T >> &&v)
Definition: Common.h:83
TheoryError & operator<<(const T &t)
Definition: Common.h:30
TheoryError & next()
Definition: Common.h:25
std::stringstream ss
Definition: Common.h:15
std::string currentTheory
Definition: Common.h:16
friend std::ostream & operator<<(std::ostream &os, const TheoryError &te)
Definition: Common.h:22
TheoryError & operator()(const std::string &theory)
Definition: Common.h:18