carl  25.02
Computer ARithmetic Library
SMTLIBStream.h
Go to the documentation of this file.
1 #pragma once
2 
14 #include <carl-formula/sort/Sort.h>
18 
19 #include <iostream>
20 #include <sstream>
21 #include <type_traits>
22 
23 namespace carl::io {
24 
25 /**
26  * Allows to print carl data structures in SMTLIB syntax.
27  */
28 class SMTLIBStream {
29 private:
30  std::stringstream mStream;
31 
32  void write(const mpz_class& n) { *this << carl::toString(n, false); }
33  void write(const mpq_class& n) { *this << carl::toString(n, false); }
34 #ifdef USE_CLN_NUMBERS
35  void write(const cln::cl_I& n) { *this << carl::toString(n, false); }
36  void write(const cln::cl_RA& n) { *this << carl::toString(n, false); }
37 #endif
38 
39  template<typename Pol>
40  void write(const Constraint<Pol>& c) {
41  if (c.relation() == Relation::NEQ) {
42  *this << "(not (= " << c.lhs() << " 0))";
43  } else {
44  *this << "(" << c.relation() << " " << c.lhs() << " 0)";
45  }
46  }
47 
48  template<typename Pol>
49  void write(const VariableComparison<Pol>& c) {
50  auto constraint = carl::as_constraint(c);
51  if (constraint) {
52  *this << *constraint;
53  } else {
54  auto iroot = [&]() {
55  if (std::holds_alternative<MultivariateRoot<Pol>>(c.value())) {
56  return std::get<MultivariateRoot<Pol>>(c.value());
57  } else {
58  return convert_to_mvroot<Pol>(std::get<typename MultivariateRoot<Pol>::RAN>(c.value()), c.var());
59  }
60  }();
61  if (c.relation() == Relation::NEQ) {
62  *this << "(not (" << (c.negated() ? "not" : "") << "= " << c.var() << " (root " << iroot.poly() << " " << iroot.k() << " " << iroot.var() << ")))";
63  } else {
64  *this << "(" << (c.negated() ? "not" : "") << c.relation() << " " << c.var() << " (root " << iroot.poly() << " " << iroot.k() << " " << iroot.var() << "))";
65  }
66  }
67  }
68 
69  template<typename Pol>
70  void write(const Formula<Pol>& f) {
71  switch (f.type()) {
72  case FormulaType::AND:
73  case FormulaType::OR:
74  case FormulaType::IFF:
75  case FormulaType::XOR:
77  case FormulaType::ITE:
78  // *this << "(" << f.type() << " " << stream_joined(" ", f.subformulas()) << ")";
79  *this << "(" << f.type();
80  for (const auto& f : f.subformulas()) {
81  *this << " " << f;
82  }
83  *this << ")";
84  break;
85  case FormulaType::NOT:
86  *this << "(" << f.type() << " " << f.subformula() << ")";
87  break;
88  case FormulaType::BOOL:
89  *this << f.boolean();
90  break;
92  *this << f.constraint();
93  break;
95  *this << f.variable_comparison();
96  break;
98  *this << f.variable_assignment();
99  break;
101  *this << f.bv_constraint();
102  break;
103  case FormulaType::TRUE:
104  case FormulaType::FALSE:
105  *this << f.type();
106  break;
107  case FormulaType::UEQ:
108  *this << f.u_equality();
109  break;
110  case FormulaType::EXISTS:
111  case FormulaType::FORALL:
112  CARL_LOG_ERROR("carl.smtlibstream", "Printing exists or forall is not implemented yet.");
113  break;
114  default:
115  CARL_LOG_ERROR("carl.smtlibstream", "Not supported formula type: " << f.type());
116  }
117  }
118 
119  template<typename Rational, typename Poly>
120  void write(const Model<Rational,Poly>& model) {
121  *this << "(model " << std::endl;
122  for (const auto& m: model) {
123  auto value = m.second;
124  value = model.evaluated(m.first);
125  *this << "\t(define-fun " << m.first << " () ";
126  if (m.first.is_variable()) {
127  *this << m.first.asVariable().type() << std::endl;
128  } else if (m.first.isBVVariable()) {
129  *this << m.first.asBVVariable().sort() << std::endl;
130  } else if (m.first.isUVariable()) {
131  *this << m.first.asUVariable().domain() << std::endl;
132  } else if (m.first.isFunction()) {
133  *this << value;
134  } else {
135  CARL_LOG_ERROR("carl.smtlibstream", "Encountered an unknown type of ModelVariable: " << m.first);
136  assert(false);
137  }
138  *this << "\t\t";
139  value.visit([this](const auto& v){ this->write(v); });
140  *this << std::endl << "\t)" << std::endl;
141  }
142  *this << ")" << std::endl;
143  }
144 
145  template<typename Rational>
147  if (ran.is_numeric()) {
148  *this << ran.value();
149  return;
150  }
151 
152  auto p = ran.polynomial();
153  auto denominator = p.coprime_factor();
154  if ((denominator < 0) == (p.lcoeff() > 0)) denominator *= -1;
155  p *= denominator;
156 
157  *this << "(root-of-with-interval ";
158  const auto& coeffs = p.coefficients();
159  auto it = coeffs.begin();
160  *this << "(coeffs " << *it;
161  it++;
162  for (; it != coeffs.end(); it++) {
163  assert(carl::is_integer(*it));
164  *this << " " << *it;
165  }
166  *this << ") ";
167  *this << ran.interval().lower() << " " << ran.interval().upper();
168  *this << ")";
169  }
170 
171  template<typename Rational, typename Poly>
173  if (mv.isBool()) {
174  *this << mv.asBool();
175  } else if (mv.isRational()) {
176  *this << mv.asRational();
177  } else if (mv.isRAN()) {
178  write(mv.asRAN());
179  }
180  }
181 
182  void write(const Monomial::Arg& m) {
183  if (m) *this << *m;
184  else *this << "1";
185  }
186  void write(const Monomial::Content::value_type& m) {
187  if (m.second == 0) *this << "1";
188  else if (m.second == 1) *this << m.first;
189  else {
190  *this << "(*";
191  for (std::size_t i = 0; i < m.second; ++i) *this << " " << m.first;
192  *this << ")";
193  }
194  }
195  void write(const Monomial& m) {
196  if (m.exponents().empty()) *this << "1";
197  else if (m.exponents().size() == 1) *this << m.exponents().front();
198  else {
199  // *this << "(* " << stream_joined(" ", m.exponents()) << ")";
200  *this << "(* ";
201  for (const auto& e : m.exponents()) {
202  *this << " " << e;
203  }
204  *this << ")";
205  }
206  }
207 
208  template<typename Coeff>
210  if (is_zero(mp)) *this << "0";
211  else if (mp.nr_terms() == 1) *this << mp.lterm();
212  else {
213  *this << "(+";
214  for (auto it = mp.rbegin(); it != mp.rend(); ++it) {
215  *this << " " << *it;
216  }
217  *this << ")";
218  }
219  }
220 
221  void write(Relation r) {
222  switch (r) {
223  case Relation::EQ: *this << "="; break;
224  case Relation::NEQ: *this << "<>"; break;
225  case Relation::LESS: *this << "<"; break;
226  case Relation::LEQ: *this << "<="; break;
227  case Relation::GREATER: *this << ">"; break;
228  case Relation::GEQ: *this << ">="; break;
229  }
230  }
231 
232  template<typename Coeff>
233  void write(const Term<Coeff>& t) {
234  if (!t.monomial()) *this << t.coeff();
235  else {
236  if (carl::is_one(t.coeff())) {
237  *this << t.monomial();
238  } else {
239  *this << "(* " << t.coeff() << " " << t.monomial() << ")";
240  }
241  }
242  }
243 
244  void write(const UEquality& ueq) {
245  if (ueq.negated()) {
246  *this << "(not (= " << ueq.lhs() << " " << ueq.rhs() << "))";
247  } else {
248  *this << "(= " << ueq.lhs() << " " << ueq.rhs() << ")";
249  }
250  }
251 
252  void write(const UFInstance& ufi) {
253  // *this << "(" << ufi.uninterpretedFunction().name() << " " << stream_joined(" ", ufi.args()) << ")";
254  *this << "(" << ufi.uninterpretedFunction().name();
255  for (const auto& a : ufi.args()) {
256  *this << " " << a;
257  }
258  *this << ")";
259  }
260 
261  template<typename Coeff>
263  if (up.is_constant()) *this << up.constant_part();
264  else {
265  *this << "(+";
266  for (std::size_t i = 0; i < up.coefficients().size(); ++i) {
267  std::size_t exp = up.coefficients().size() - i - 1;
268  const auto& coeff = up.coefficients()[exp];
269  if (exp == 0) *this << " " << coeff;
270  else *this << " (* " << coeff << " " << Monomial(up.main_var(), exp) << ")";
271  }
272  *this << ")";
273  }
274  }
275 
276  void write(const UTerm& t) {
278  [this](UVariable v) { *this << v; },
279  [this](UFInstance ufi) { *this << ufi; },
280  }, t.asVariant());
281  }
282 
283  void write(const Variable& v) {
284  *this << v.name();
285  }
286  void write(const VariableType& vt) {
287  switch (vt) {
288  case VariableType::VT_BOOL: *this << "Bool"; break;
289  case VariableType::VT_REAL: *this << "Real"; break;
290  case VariableType::VT_INT: *this << "Int"; break;
291  case VariableType::VT_UNINTERPRETED: *this << "?_Uninterpreted"; break;
292  case VariableType::VT_BITVECTOR: *this << "?_Bitvector"; break;
293  default: *this << "?"; break;
294  }
295  }
296 
297  void write(const bool b) {
298  if (b) *this << "true";
299  else *this << "false";
300  }
301 
302  template<typename T>
303  void write(T&& t) {
304  mStream << t;
305  }
306 
307 public:
308  /// Writes a comment
309  void comment(const std::string& c) {
310  *this << "; " << c << std::endl;
311  }
312  /// Declare a logic via `set-logic`.
313  void declare(Logic l) {
314  *this << "(set-logic " << l << ")" << std::endl;
315  }
316  /// Declare a sort via `declare-sort`.
317  void declare(Sort s) {
318  *this << "(declare-sort " << s << " " << s.arity() << ")" << std::endl;
319  }
320  /// Declare a fresh function via `declare-fun`.
322  // *this << "(declare-fun " << uf.name() << " (" << stream_joined(" ", uf.domain()) << ") ";
323  *this << "(declare-fun " << uf.name() << " (";
324  for (const auto& d : uf.domain()) {
325  *this << " " << d;
326  }
327  *this << ") ";
328  *this << uf.codomain() << ")" << std::endl;
329  }
330  /// Declare a fresh variable via `declare-fun`.
331  void declare(Variable v) {
332  *this << "(declare-fun " << v << " () " << v.type() << ")" << std::endl;
333  }
334  /// Declare a bitvector variable via `declare-fun`.
335  void declare(BVVariable v) {
336  *this << "(declare-fun " << v.variable() << " () " << v.variable().type() << ")" << std::endl;
337  }
338  /// Declare an uninterpreted variable via `declare-fun`.
339  void declare(UVariable v) {
340  *this << "(declare-fun " << v << " () " << v.domain() << ")" << std::endl;
341  }
342  /// Declare a set of functions.
343  void declare(const std::set<UninterpretedFunction>& ufs) {
344  for (const auto& uf: ufs) {
345  declare(uf);
346  }
347  }
348  /// Declare a set of variables.
349  void declare(const carlVariables& vars) {
350  for (const auto& v: vars) {
351  declare(v);
352  }
353  }
354  /// Declare a set of bitvector variables.
355  void declare(const std::set<BVVariable>& bvvs) {
356  for (const auto& bv: bvvs) {
357  declare(bv);
358  }
359  }
360  /// Declare a set of uninterpreted variables.
361  void declare(const std::set<UVariable>& uvs) {
362  for (const auto& uv: uvs) {
363  declare(uv);
364  }
365  }
366  /// Generic initializer including the logic, a set of variables and a set of functions.
367  void initialize(Logic l, const carlVariables& vars, const std::set<UninterpretedFunction>& ufs = {}, const std::set<BVVariable>& bvvs = {}, const std::set<UVariable>& uvs = {}) {
368  declare(l);
369  std::set<Sort> sorts;
370  for (const auto& v: bvvs) {
371  sorts.insert(v.sort());
372  }
373  for (const auto& v: uvs) {
374  sorts.insert(v.domain());
375  }
376  for (const auto& s: sorts) {
377  declare(s);
378  }
379  declare(ufs);
380  declare(vars.filter(carl::variable_type_filter::excluding({VariableType::VT_BITVECTOR, VariableType::VT_UNINTERPRETED})));
381  declare(bvvs);
382  declare(uvs);
383  }
384 
385  /// Generic initializer including the logic and variables and functions from a set of formulas.
386  template<typename Pol>
387  void initialize(Logic l, std::initializer_list<Formula<Pol>> formulas) {
388  carlVariables vars;
389  std::set<UninterpretedFunction> ufs;
390  std::set<BVVariable> bvvs;
391  std::set<UVariable> uvs;
392  for (const auto& f: formulas) {
393  carl::variables(f,vars);
397  }
398  initialize(l, vars, ufs, bvvs, uvs);
399  }
400 
401  /// Set information via `set-info`.
402  void setInfo(const std::string& name, const std::string& value) {
403  *this << "(set-info :" << name << " " << value << ")" << std::endl;
404  }
405 
406  /// Set option via `set-option`.
407  void setOption(const std::string& name, const std::string& value) {
408  *this << "(set-option :" << name << " " << value << ")" << std::endl;
409  }
410 
411  /// Assert a formula via `assert`.
412  template<typename Pol>
413  void assertFormula(const Formula<Pol>& formula) {
414  *this << "(assert " << formula << ")" << std::endl;
415  }
416 
417  /// Minimize an objective via custom `minimize`.
418  template<typename Pol>
419  void minimize(const Pol& objective) {
420  *this << "(minimize " << objective << ")" << std::endl;
421  }
422 
423  /// Check satisfiability via `check-sat`.
424  void checkSat() {
425  *this << "(check-sat)" << std::endl;
426  }
427 
428  /// Print assertions via `get-assertions`.
429  void getAssertions() {
430  *this << "(get-assertions)" << std::endl;
431  }
432 
433  /// Print model via `get-model`.
434  void getModel() {
435  *this << "(get-model)" << std::endl;
436  }
437 
438  /// Echo via `echo`.
439  void echo(const std::string& str) {
440  *this << "(echo \"" << str << "\")" << std::endl;
441  }
442 
443  /// Reset via `reset`.
444  void reset() {
445  *this << "(reset)" << std::endl;
446  }
447 
448  /// Exit via `exit`.
449  void exit() {
450  *this << "(exit)" << std::endl;
451  }
452 
453  /// Write some data to this stream.
454  template<typename T>
456  write(static_cast<const std::decay_t<T>&>(t));
457  return *this;
458  }
459 
460  /// Write io operators (like `std::endl`) directly to the underlying stream.
461  SMTLIBStream& operator<<(std::ostream& (*os)(std::ostream&)) {
462  write(os);
463  return *this;
464  }
465 
466  /// Return the written data as a string.
467  auto str() const {
468  return mStream.str();
469  }
470 
471  /// Return the underlying stream buffer.
472  auto content() const {
473  return mStream.rdbuf();
474  }
475 };
476 
477 /// Write the written data to some `std::ostream`.
478 inline std::ostream& operator<<(std::ostream& os, const SMTLIBStream& ss) {
479  return os << ss.content();
480 }
481 
482 namespace detail {
483 
484 /// Shorthand to allow writing SMTLIB scripts in one line.
485 template<typename Pol>
488  std::initializer_list<Formula<Pol>> mFormulas;
489  bool mGetModel;
491  SMTLIBScriptContainer(Logic l, std::initializer_list<Formula<Pol>> f, bool getModel = false): mLogic(l), mFormulas(f), mGetModel(getModel) {}
492  SMTLIBScriptContainer(Logic l, std::initializer_list<Formula<Pol>> f, const Pol& objective, bool getModel = false): mLogic(l), mFormulas(f), mGetModel(getModel), mObjective(objective) {}
493 };
494 /// Actually write an SMTLIBScriptContainer to an std::ostream.
495 template<typename Pol>
496 std::ostream& operator<<(std::ostream& os, const SMTLIBScriptContainer<Pol>& sc) {
497  SMTLIBStream sls;
498  sls.initialize(sc.mLogic, sc.mFormulas);
499  for (const auto& f: sc.mFormulas) sls.assertFormula(f);
500  if (!is_zero(sc.mObjective)) sls.minimize(sc.mObjective);
501  sls.checkSat();
502  if (sc.mGetModel) sls.getModel();
503  return os << sls;
504 }
505 
506 }
507 
508 /// Shorthand to allow writing SMTLIB scripts in one line.
509 template<typename Pol, typename... Args>
510 detail::SMTLIBScriptContainer<Pol> outputSMTLIB(Logic l, std::initializer_list<Formula<Pol>> formulas, Args&&... args) {
511  return detail::SMTLIBScriptContainer<Pol>(l, formulas, std::forward<Args>(args)...);
512 }
513 
514 namespace detail {
515  template<typename... Args>
517  std::tuple<Args...> mData;
518  explicit SMTLIBOutputContainer(Args&&... args): mData(std::forward<Args>(args)...) {}
519  };
520  template<typename... Args>
521  std::ostream& operator<<(std::ostream& os, const SMTLIBOutputContainer<Args...>& soc) {
522  SMTLIBStream sls;
523  carl::tuple_accumulate(soc.mData, sls, [](auto& sls, const auto& t) -> auto& { return sls << t; });
524  return os << sls;
525  }
526 }
527 
528 /// Generic shorthand to write arbitrary data to an SMTLIBStream and return the result.
529 template<typename... Args>
530 detail::SMTLIBOutputContainer<Args...> asSMTLIB(Args&&... args) {
531  return detail::SMTLIBOutputContainer<Args...>(std::forward<Args>(args)...);
532 }
533 
534 }
#define CARL_LOG_ERROR(channel, msg)
Definition: carl-logging.h:40
MultivariatePolynomial< Rational > Pol
Definition: HornerTest.cpp:17
@ CONSTRAINT
@ BITVECTOR
@ VARCOMPARE
@ VARASSIGN
std::string toString(Relation r)
Definition: Relation.h:73
carlVariables uninterpreted_variables(const T &t)
Definition: Variables.h:261
T tuple_accumulate(Tuple &&t, T &&init, F &&f)
Implements a functional fold (similar to std::accumulate) for std::tuple.
Definition: tuple_util.h:139
std::optional< BasicConstraint< Poly > > as_constraint(const VariableComparison< Poly > &f)
Convert this variable comparison "v < root(..)" into a simpler polynomial (in)equality against zero "...
Interval< Number > exp(const Interval< Number > &i)
Definition: Exponential.h:10
void uninterpreted_functions(const Formula< Pol > &f, std::set< UninterpretedFunction > &ufs)
Definition: Variables.h:43
carlVariables bitvector_variables(const T &t)
Definition: Variables.h:254
bool is_zero(const Interval< Number > &i)
Check if this interval is a point-interval containing 0.
Definition: Interval.h:1453
VariableType
Several types of variables are supported.
Definition: Variable.h:28
void visit(const Formula< Pol > &formula, Visitor func)
Recursively calls func on every subformula.
Definition: Visit.h:12
Logic
Definition: Logic.h:7
bool is_integer(const Interval< Number > &n)
Definition: Interval.h:1445
@ GREATER
Definition: SignCondition.h:15
Relation
Definition: Relation.h:20
void variables(const BasicConstraint< Pol > &c, carlVariables &vars)
bool is_one(const Interval< Number > &i)
Check if this interval is a point-interval containing 1.
Definition: Interval.h:1462
detail::SMTLIBOutputContainer< Args... > asSMTLIB(Args &&... args)
Generic shorthand to write arbitrary data to an SMTLIBStream and return the result.
Definition: SMTLIBStream.h:530
std::ostream & operator<<(std::ostream &os, const MapleStream &ms)
Definition: MapleStream.h:197
detail::SMTLIBScriptContainer< Pol > outputSMTLIB(Logic l, std::initializer_list< Formula< Pol >> formulas, Args &&... args)
Shorthand to allow writing SMTLIB scripts in one line.
Definition: SMTLIBStream.h:510
std::ostream & operator<<(std::ostream &os, const SMTLIBScriptContainer< Pol > &sc)
Actually write an SMTLIBScriptContainer to an std::ostream.
Definition: SMTLIBStream.h:496
auto & get(const std::string &name)
A Variable represents an algebraic variable that can be used throughout carl.
Definition: Variable.h:85
std::string name() const
Retrieves the name of the variable.
Definition: Variable.cpp:8
constexpr VariableType type() const noexcept
Retrieves the type of the variable.
Definition: Variable.h:131
static variable_type_filter excluding(std::initializer_list< VariableType > i)
Definition: Variables.h:24
carlVariables filter(variable_type_filter &&f) const
Definition: Variables.h:178
typename Poly::RootType RAN
Represent a sum type/variant of an (in)equality between a variable on the left-hand side and multivar...
const std::variant< MR, RAN > & value() const
This class represents a univariate polynomial with coefficients of an arbitrary type.
bool is_constant() const
Checks whether the polynomial is constant with respect to the main variable.
const std::vector< Coefficient > & coefficients() const &
Retrieves the coefficients defining this polynomial.
Variable main_var() const
Retrieves the main variable of this polynomial.
NumberType constant_part() const
Returns the constant part of this polynomial.
The general-purpose multivariate polynomial class.
const Term< Coeff > & lterm() const
The leading term.
std::size_t nr_terms() const
Calculate the number of terms.
The general-purpose monomials.
Definition: Monomial.h:59
std::shared_ptr< const Monomial > Arg
Definition: Monomial.h:62
const Content & exponents() const
Definition: Monomial.h:189
Coefficient & coeff()
Get the coefficient.
Definition: Term.h:80
Monomial::Arg & monomial()
Get the monomial.
Definition: Term.h:91
const auto & value() const
Definition: Ran.h:227
const auto & interval() const
Definition: Ran.h:222
const auto & polynomial() const
Definition: Ran.h:218
bool is_numeric() const
Definition: Ran.h:214
Represent a polynomial (in)equality against zero.
Definition: Constraint.h:62
Relation relation() const
Definition: Constraint.h:116
const Pol & lhs() const
Definition: Constraint.h:109
Represent a BitVector-Variable.
Definition: BVVariable.h:13
Variable variable() const
Definition: BVVariable.h:34
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 Formula & subformula() const
Definition: Formula.h:335
const VariableComparison< Pol > & variable_comparison() const
Definition: Formula.h:438
carl::Variable::Arg boolean() const
Definition: Formula.h:458
const Constraint< Pol > & constraint() const
Definition: Formula.h:432
const Formulas< Pol > & subformulas() const
Definition: Formula.h:422
const BVConstraint & bv_constraint() const
Definition: Formula.h:448
const UEquality & u_equality() const
Definition: Formula.h:468
FormulaType type() const
Definition: Formula.h:262
Represent a collection of assignments/mappings from variables to values.
Definition: Model.h:19
const ModelValue< Rational, Poly > & evaluated(const typename Map::key_type &key) const
Return the ModelValue for the given key, evaluated if it's a ModelSubstitution and evaluatable,...
Definition: Model.h:146
Represent a sum type/variant over the different kinds of values that can be assigned to the different...
Definition: ModelValue.h:56
const Poly::RootType & asRAN() const
Definition: ModelValue.h:233
bool isBool() const
Definition: ModelValue.h:143
const Rational & asRational() const
Definition: ModelValue.h:217
bool isRational() const
Definition: ModelValue.h:150
bool asBool() const
Definition: ModelValue.h:209
bool isRAN() const
Definition: ModelValue.h:164
Implements a sort (for defining types of variables and functions).
Definition: Sort.h:20
std::size_t arity() const
Definition: Sort.cpp:14
Implements an uninterpreted equality, that is an equality of either two uninterpreted function instan...
Definition: UEquality.h:23
const UTerm & rhs() const
Definition: UEquality.h:79
bool negated() const
Definition: UEquality.h:65
const UTerm & lhs() const
Definition: UEquality.h:72
Implements an uninterpreted function instance.
Definition: UFInstance.h:25
const UninterpretedFunction & uninterpretedFunction() const
Definition: UFInstance.cpp:21
const std::vector< UTerm > & args() const
Definition: UFInstance.cpp:25
Implements an uninterpreted function.
const std::string & name() const
const std::vector< Sort > & domain() const
Implements an uninterpreted term, that is either an uninterpreted variable or an uninterpreted functi...
Definition: UTerm.h:22
const auto & asVariant() const
Definition: UTerm.h:41
Implements an uninterpreted variable.
Definition: UVariable.h:19
Sort domain() const
Definition: UVariable.h:61
Allows to print carl data structures in SMTLIB syntax.
Definition: SMTLIBStream.h:28
void declare(const std::set< UVariable > &uvs)
Declare a set of uninterpreted variables.
Definition: SMTLIBStream.h:361
void write(const Constraint< Pol > &c)
Definition: SMTLIBStream.h:40
void exit()
Exit via exit.
Definition: SMTLIBStream.h:449
std::stringstream mStream
Definition: SMTLIBStream.h:30
void comment(const std::string &c)
Writes a comment.
Definition: SMTLIBStream.h:309
void declare(UVariable v)
Declare an uninterpreted variable via declare-fun.
Definition: SMTLIBStream.h:339
void declare(const carlVariables &vars)
Declare a set of variables.
Definition: SMTLIBStream.h:349
void reset()
Reset via reset.
Definition: SMTLIBStream.h:444
void write(const UnivariatePolynomial< Coeff > &up)
Definition: SMTLIBStream.h:262
void assertFormula(const Formula< Pol > &formula)
Assert a formula via assert.
Definition: SMTLIBStream.h:413
void write(const ModelValue< Rational, Poly > &mv)
Definition: SMTLIBStream.h:172
void initialize(Logic l, std::initializer_list< Formula< Pol >> formulas)
Generic initializer including the logic and variables and functions from a set of formulas.
Definition: SMTLIBStream.h:387
auto content() const
Return the underlying stream buffer.
Definition: SMTLIBStream.h:472
void declare(Variable v)
Declare a fresh variable via declare-fun.
Definition: SMTLIBStream.h:331
void write(const UEquality &ueq)
Definition: SMTLIBStream.h:244
void write(const VariableComparison< Pol > &c)
Definition: SMTLIBStream.h:49
void declare(const std::set< UninterpretedFunction > &ufs)
Declare a set of functions.
Definition: SMTLIBStream.h:343
void write(const Monomial::Content::value_type &m)
Definition: SMTLIBStream.h:186
void write(const UTerm &t)
Definition: SMTLIBStream.h:276
void declare(BVVariable v)
Declare a bitvector variable via declare-fun.
Definition: SMTLIBStream.h:335
void write(const Model< Rational, Poly > &model)
Definition: SMTLIBStream.h:120
SMTLIBStream & operator<<(T &&t)
Write some data to this stream.
Definition: SMTLIBStream.h:455
void checkSat()
Check satisfiability via check-sat.
Definition: SMTLIBStream.h:424
SMTLIBStream & operator<<(std::ostream &(*os)(std::ostream &))
Write io operators (like std::endl) directly to the underlying stream.
Definition: SMTLIBStream.h:461
void echo(const std::string &str)
Echo via echo.
Definition: SMTLIBStream.h:439
void write(const Variable &v)
Definition: SMTLIBStream.h:283
void declare(Sort s)
Declare a sort via declare-sort.
Definition: SMTLIBStream.h:317
void write(const MultivariatePolynomial< Coeff > &mp)
Definition: SMTLIBStream.h:209
void write(const Formula< Pol > &f)
Definition: SMTLIBStream.h:70
void write(const UFInstance &ufi)
Definition: SMTLIBStream.h:252
void getModel()
Print model via get-model.
Definition: SMTLIBStream.h:434
void write(Relation r)
Definition: SMTLIBStream.h:221
void getAssertions()
Print assertions via get-assertions.
Definition: SMTLIBStream.h:429
void write(const mpz_class &n)
Definition: SMTLIBStream.h:32
void setInfo(const std::string &name, const std::string &value)
Set information via set-info.
Definition: SMTLIBStream.h:402
void minimize(const Pol &objective)
Minimize an objective via custom minimize.
Definition: SMTLIBStream.h:419
void write(const mpq_class &n)
Definition: SMTLIBStream.h:33
void write(const IntRepRealAlgebraicNumber< Rational > &ran)
Definition: SMTLIBStream.h:146
void declare(UninterpretedFunction uf)
Declare a fresh function via declare-fun.
Definition: SMTLIBStream.h:321
void write(const Monomial::Arg &m)
Definition: SMTLIBStream.h:182
auto str() const
Return the written data as a string.
Definition: SMTLIBStream.h:467
void write(const Monomial &m)
Definition: SMTLIBStream.h:195
void write(const Term< Coeff > &t)
Definition: SMTLIBStream.h:233
void initialize(Logic l, const carlVariables &vars, const std::set< UninterpretedFunction > &ufs={}, const std::set< BVVariable > &bvvs={}, const std::set< UVariable > &uvs={})
Generic initializer including the logic, a set of variables and a set of functions.
Definition: SMTLIBStream.h:367
void setOption(const std::string &name, const std::string &value)
Set option via set-option.
Definition: SMTLIBStream.h:407
void declare(Logic l)
Declare a logic via set-logic.
Definition: SMTLIBStream.h:313
void declare(const std::set< BVVariable > &bvvs)
Declare a set of bitvector variables.
Definition: SMTLIBStream.h:355
void write(const VariableType &vt)
Definition: SMTLIBStream.h:286
void write(const bool b)
Definition: SMTLIBStream.h:297
Shorthand to allow writing SMTLIB scripts in one line.
Definition: SMTLIBStream.h:486
SMTLIBScriptContainer(Logic l, std::initializer_list< Formula< Pol >> f, const Pol &objective, bool getModel=false)
Definition: SMTLIBStream.h:492
std::initializer_list< Formula< Pol > > mFormulas
Definition: SMTLIBStream.h:488
SMTLIBScriptContainer(Logic l, std::initializer_list< Formula< Pol >> f, bool getModel=false)
Definition: SMTLIBStream.h:491