Allows to print carl data structures in SMTLIB syntax. More...

#include <SMTLIBStream.h>

Collaboration diagram for carl::io::SMTLIBStream:

[legend]

Public Member Functions
void	comment (const std::string &c)
	Writes a comment. More...

void	declare (Logic l)
	Declare a logic via `set-logic`. More...

void	declare (Sort s)
	Declare a sort via `declare-sort`. More...

void	declare (UninterpretedFunction uf)
	Declare a fresh function via `declare-fun`. More...

void	declare (Variable v)
	Declare a fresh variable via `declare-fun`. More...

void	declare (BVVariable v)
	Declare a bitvector variable via `declare-fun`. More...

void	declare (UVariable v)
	Declare an uninterpreted variable via `declare-fun`. More...

void	declare (const std::set< UninterpretedFunction > &ufs)
	Declare a set of functions. More...

void	declare (const carlVariables &vars)
	Declare a set of variables. More...

void	declare (const std::set< BVVariable > &bvvs)
	Declare a set of bitvector variables. More...

void	declare (const std::set< UVariable > &uvs)
	Declare a set of uninterpreted variables. More...

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. More...

template<typename Pol >
void	initialize (Logic l, std::initializer_list< Formula< Pol >> formulas)
	Generic initializer including the logic and variables and functions from a set of formulas. More...

void	setInfo (const std::string &name, const std::string &value)
	Set information via `set-info`. More...

void	setOption (const std::string &name, const std::string &value)
	Set option via `set-option`. More...

template<typename Pol >
void	assertFormula (const Formula< Pol > &formula)
	Assert a formula via `assert`. More...

template<typename Pol >
void	minimize (const Pol &objective)
	Minimize an objective via custom `minimize`. More...

void	checkSat ()
	Check satisfiability via `check-sat`. More...

void	getAssertions ()
	Print assertions via `get-assertions`. More...

void	getModel ()
	Print model via `get-model`. More...

void	echo (const std::string &str)
	Echo via `echo`. More...

void	reset ()
	Reset via `reset`. More...

void	exit ()
	Exit via `exit`. More...

template<typename T >
SMTLIBStream &	operator<< (T &&t)
	Write some data to this stream. More...

SMTLIBStream &	operator<< (std::ostream &(*os)(std::ostream &))
	Write io operators (like `std::endl`) directly to the underlying stream. More...

auto	str () const
	Return the written data as a string. More...

auto	content () const
	Return the underlying stream buffer. More...

Private Member Functions
void	write (const mpz_class &n)

void	write (const mpq_class &n)

template<typename Pol >
void	write (const Constraint< Pol > &c)

template<typename Pol >
void	write (const VariableComparison< Pol > &c)

template<typename Pol >
void	write (const Formula< Pol > &f)

template<typename Rational , typename Poly >
void	write (const Model< Rational, Poly > &model)

template<typename Rational >
void	write (const IntRepRealAlgebraicNumber< Rational > &ran)

template<typename Rational , typename Poly >
void	write (const ModelValue< Rational, Poly > &mv)

void	write (const Monomial::Arg &m)

void	write (const Monomial::Content::value_type &m)

void	write (const Monomial &m)

template<typename Coeff >
void	write (const MultivariatePolynomial< Coeff > &mp)

void	write (Relation r)

template<typename Coeff >
void	write (const Term< Coeff > &t)

void	write (const UEquality &ueq)

void	write (const UFInstance &ufi)

template<typename Coeff >
void	write (const UnivariatePolynomial< Coeff > &up)

void	write (const UTerm &t)

void	write (const Variable &v)

void	write (const VariableType &vt)

void	write (const bool b)

template<typename T >
void	write (T &&t)

Private Attributes
std::stringstream	mStream

Detailed Description

Allows to print carl data structures in SMTLIB syntax.

Definition at line 28 of file SMTLIBStream.h.

Member Function Documentation

◆ assertFormula()

template<typename Pol >

void carl::io::SMTLIBStream::assertFormula ( const Formula< Pol > & formula )

inline

Assert a formula via assert.

Definition at line 409 of file SMTLIBStream.h.

Here is the caller graph for this function:

◆ checkSat()

void carl::io::SMTLIBStream::checkSat ( )

inline

Check satisfiability via check-sat.

Definition at line 420 of file SMTLIBStream.h.

Here is the caller graph for this function:

◆ comment()

void carl::io::SMTLIBStream::comment ( const std::string & c )

inline

Writes a comment.

Definition at line 305 of file SMTLIBStream.h.

◆ content()

auto carl::io::SMTLIBStream::content ( ) const

inline

Return the underlying stream buffer.

Definition at line 468 of file SMTLIBStream.h.

Here is the caller graph for this function:

◆ declare() [1/10]

void carl::io::SMTLIBStream::declare ( BVVariable v )

inline

Declare a bitvector variable via declare-fun.

Definition at line 331 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ declare() [2/10]

void carl::io::SMTLIBStream::declare ( const carlVariables & vars )

inline

Declare a set of variables.

Definition at line 345 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ declare() [3/10]

void carl::io::SMTLIBStream::declare ( const std::set< BVVariable > & bvvs )

inline

Declare a set of bitvector variables.

Definition at line 351 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ declare() [4/10]

void carl::io::SMTLIBStream::declare ( const std::set< UninterpretedFunction > & ufs )

inline

Declare a set of functions.

Definition at line 339 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ declare() [5/10]

void carl::io::SMTLIBStream::declare ( const std::set< UVariable > & uvs )

inline

Declare a set of uninterpreted variables.

Definition at line 357 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ declare() [6/10]

void carl::io::SMTLIBStream::declare ( Logic l )

inline

Declare a logic via set-logic.

Definition at line 309 of file SMTLIBStream.h.

Here is the caller graph for this function:

◆ declare() [7/10]

void carl::io::SMTLIBStream::declare ( Sort s )

inline

Declare a sort via declare-sort.

Definition at line 313 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ declare() [8/10]

void carl::io::SMTLIBStream::declare ( UninterpretedFunction uf )

inline

Declare a fresh function via declare-fun.

Definition at line 317 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ declare() [9/10]

void carl::io::SMTLIBStream::declare ( UVariable v )

inline

Declare an uninterpreted variable via declare-fun.

Definition at line 335 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ declare() [10/10]

void carl::io::SMTLIBStream::declare ( Variable v )

inline

Declare a fresh variable via declare-fun.

Definition at line 327 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ echo()

void carl::io::SMTLIBStream::echo ( const std::string & str )

inline

Echo via echo.

Definition at line 435 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ exit()

void carl::io::SMTLIBStream::exit ( )

inline

Exit via exit.

Definition at line 445 of file SMTLIBStream.h.

◆ getAssertions()

void carl::io::SMTLIBStream::getAssertions ( )

inline

Print assertions via get-assertions.

Definition at line 425 of file SMTLIBStream.h.

◆ getModel()

void carl::io::SMTLIBStream::getModel ( )

inline

Print model via get-model.

Definition at line 430 of file SMTLIBStream.h.

Here is the caller graph for this function:

◆ initialize() [1/2]

void carl::io::SMTLIBStream::initialize	(	Logic	l,
		const carlVariables &	vars,
		const std::set< UninterpretedFunction > &	ufs = `{}`,
		const std::set< BVVariable > &	bvvs = `{}`,
		const std::set< UVariable > &	uvs = `{}`
	)

inline

Generic initializer including the logic, a set of variables and a set of functions.

Definition at line 363 of file SMTLIBStream.h.

Here is the caller graph for this function:

◆ initialize() [2/2]

template<typename Pol >

void carl::io::SMTLIBStream::initialize	(	Logic	l,
		std::initializer_list< Formula< Pol >>	formulas
	)

inline

Generic initializer including the logic and variables and functions from a set of formulas.

Definition at line 383 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ minimize()

template<typename Pol >

void carl::io::SMTLIBStream::minimize ( const Pol & objective )

inline

Minimize an objective via custom minimize.

Definition at line 415 of file SMTLIBStream.h.

Here is the caller graph for this function:

◆ operator<<() [1/2]

SMTLIBStream& carl::io::SMTLIBStream::operator<< ( std::ostream &(*)(std::ostream &) os )

inline

Write io operators (like std::endl) directly to the underlying stream.

Definition at line 457 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ operator<<() [2/2]

template<typename T >

SMTLIBStream& carl::io::SMTLIBStream::operator<< ( T && t )

inline

Write some data to this stream.

Definition at line 451 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ reset()

void carl::io::SMTLIBStream::reset ( )

inline

Reset via reset.

Definition at line 440 of file SMTLIBStream.h.

◆ setInfo()

void carl::io::SMTLIBStream::setInfo	(	const std::string &	name,
		const std::string &	value
	)

inline

Set information via set-info.

Definition at line 398 of file SMTLIBStream.h.

◆ setOption()

void carl::io::SMTLIBStream::setOption	(	const std::string &	name,
		const std::string &	value
	)

inline

Set option via set-option.

Definition at line 403 of file SMTLIBStream.h.

◆ str()

auto carl::io::SMTLIBStream::str ( ) const

inline

Return the written data as a string.

Definition at line 463 of file SMTLIBStream.h.

Here is the caller graph for this function:

◆ write() [1/22]

void carl::io::SMTLIBStream::write ( const bool b )

inlineprivate

Definition at line 293 of file SMTLIBStream.h.

◆ write() [2/22]

template<typename Pol >

void carl::io::SMTLIBStream::write ( const Constraint< Pol > & c )

inlineprivate

Definition at line 40 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ write() [3/22]

template<typename Pol >

void carl::io::SMTLIBStream::write ( const Formula< Pol > & f )

inlineprivate

Definition at line 66 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ write() [4/22]

template<typename Rational >

void carl::io::SMTLIBStream::write ( const IntRepRealAlgebraicNumber< Rational > & ran )

inlineprivate

Definition at line 142 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ write() [5/22]

template<typename Rational , typename Poly >

void carl::io::SMTLIBStream::write ( const Model< Rational, Poly > & model )

inlineprivate

Definition at line 116 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ write() [6/22]

template<typename Rational , typename Poly >

void carl::io::SMTLIBStream::write ( const ModelValue< Rational, Poly > & mv )

inlineprivate

Definition at line 168 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ write() [7/22]

void carl::io::SMTLIBStream::write ( const Monomial & m )

inlineprivate

Definition at line 191 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ write() [8/22]

void carl::io::SMTLIBStream::write ( const Monomial::Arg & m )

inlineprivate

Definition at line 178 of file SMTLIBStream.h.

◆ write() [9/22]

void carl::io::SMTLIBStream::write ( const Monomial::Content::value_type & m )

inlineprivate

Definition at line 182 of file SMTLIBStream.h.

◆ write() [10/22]

void carl::io::SMTLIBStream::write ( const mpq_class & n )

inlineprivate

Definition at line 33 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ write() [11/22]

void carl::io::SMTLIBStream::write ( const mpz_class & n )

inlineprivate

Definition at line 32 of file SMTLIBStream.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ write() [12/22]

template<typename Coeff >

void carl::io::SMTLIBStream::write ( const MultivariatePolynomial< Coeff > & mp )

inlineprivate

Definition at line 205 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ write() [13/22]

template<typename Coeff >

void carl::io::SMTLIBStream::write ( const Term< Coeff > & t )

inlineprivate

Definition at line 229 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ write() [14/22]

void carl::io::SMTLIBStream::write ( const UEquality & ueq )

inlineprivate

Definition at line 240 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ write() [15/22]

void carl::io::SMTLIBStream::write ( const UFInstance & ufi )

inlineprivate

Definition at line 248 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ write() [16/22]

template<typename Coeff >

void carl::io::SMTLIBStream::write ( const UnivariatePolynomial< Coeff > & up )

inlineprivate

Definition at line 258 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ write() [17/22]

void carl::io::SMTLIBStream::write ( const UTerm & t )

inlineprivate

Definition at line 272 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ write() [18/22]

void carl::io::SMTLIBStream::write ( const Variable & v )

inlineprivate

Definition at line 279 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ write() [19/22]

template<typename Pol >

void carl::io::SMTLIBStream::write ( const VariableComparison< Pol > & c )

inlineprivate

Definition at line 49 of file SMTLIBStream.h.

Here is the call graph for this function:

◆ write() [20/22]

void carl::io::SMTLIBStream::write ( const VariableType & vt )

inlineprivate

Definition at line 282 of file SMTLIBStream.h.

◆ write() [21/22]

void carl::io::SMTLIBStream::write ( Relation r )

inlineprivate

Definition at line 217 of file SMTLIBStream.h.

◆ write() [22/22]

template<typename T >

void carl::io::SMTLIBStream::write ( T && t )

inlineprivate

Definition at line 299 of file SMTLIBStream.h.

Field Documentation

◆ mStream

std::stringstream carl::io::SMTLIBStream::mStream

private

Definition at line 30 of file SMTLIBStream.h.

The documentation for this class was generated from the following file:

carl-io/SMTLIBStream.h

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Member Function Documentation

◆ assertFormula()

◆ checkSat()

◆ comment()

◆ content()

◆ declare() [1/10]

◆ declare() [2/10]

◆ declare() [3/10]

◆ declare() [4/10]

◆ declare() [5/10]

◆ declare() [6/10]

◆ declare() [7/10]

◆ declare() [8/10]

◆ declare() [9/10]

◆ declare() [10/10]

◆ echo()

◆ exit()

◆ getAssertions()

◆ getModel()

◆ initialize() [1/2]

◆ initialize() [2/2]

◆ minimize()

◆ operator<<() [1/2]

◆ operator<<() [2/2]

◆ reset()

◆ setInfo()

◆ setOption()

◆ str()

◆ write() [1/22]

◆ write() [2/22]

◆ write() [3/22]

◆ write() [4/22]

◆ write() [5/22]

◆ write() [6/22]

◆ write() [7/22]

◆ write() [8/22]

◆ write() [9/22]

◆ write() [10/22]

◆ write() [11/22]

◆ write() [12/22]

◆ write() [13/22]

◆ write() [14/22]

◆ write() [15/22]

◆ write() [16/22]

◆ write() [17/22]

◆ write() [18/22]

◆ write() [19/22]

◆ write() [20/22]

◆ write() [21/22]

◆ write() [22/22]

Field Documentation

◆ mStream