#include <carl-logging/carl-logging.h>
#include <iostream>
#include <variant>
#include "FormulaContent.tpp"

Include dependency graph for FormulaContent.h:

This graph shows which files directly or indirectly include this file:

Data Structures
struct	carl::QuantifierContent< Pol >
	Stores the variables and the formula bound by a quantifier. More...

struct	carl::AuxQuantifierContent< Pol >

class	carl::FormulaContent< Pol >

Namespaces
	carl
	carl is the main namespace for the library.

Typedefs
template<typename Poly >
using	carl::Formulas = std::vector< Formula< Poly > >

template<typename Poly >
using	carl::FormulaSet = std::set< Formula< Poly > >

template<typename Poly >
using	carl::FormulasMulti = std::multiset< Formula< Poly > >

Enumerations
enum	carl::FormulaType { carl::ITE , carl::EXISTS , carl::FORALL , carl::AUX_EXISTS , carl::TRUE , carl::FALSE , carl::BOOL , carl::NOT , carl::NOT , carl::IMPLIES , carl::AND , carl::AND , carl::OR , carl::OR , carl::XOR , carl::XOR , carl::IFF , carl::CONSTRAINT , carl::VARCOMPARE , carl::VARASSIGN , carl::BITVECTOR , carl::UEQ }
	Represent the type of a formula to allow faster/specialized processing. More...

Functions
std::string	carl::formulaTypeToString (FormulaType _type)

std::ostream &	carl::operator<< (std::ostream &os, FormulaType t)

template<typename Pol >
std::ostream &	carl::operator<< (std::ostream &os, const FormulaContent< Pol > &f)
	The output operator of a formula. More...

template<typename Pol >
std::ostream &	carl::operator<< (std::ostream &os, const FormulaContent< Pol > *fc)

Data Structures

Namespaces