carl
24.04
Computer ARithmetic Library
|
#include <carl-logging/carl-logging.h>
#include <iostream>
#include <variant>
#include "FormulaContent.tpp"
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) |