carl  24.04
Computer ARithmetic Library
FormulaContent.h File Reference
#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:

Go to the source code of this file.

Data Structures

struct  carl::QuantifierContent< Pol >
 Stores the variables and the formula bound by a quantifier. More...
 
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::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)