Formula.h File Reference
#include <cstring>#include <functional>#include <string>#include <set>#include <boost/dynamic_bitset.hpp>#include "Condition.h"#include "../arithmetic/Constraint.h"#include "../uninterpreted/UEquality.h"#include "../uninterpreted/UFManager.h"#include "../bitvector/BVConstraintPool.h"#include "../bitvector/BVConstraint.h"#include <carl-arith/extended/VariableAssignment.h>#include <carl-arith/extended/VariableComparison.h>#include "Logic.h"#include "FormulaContent.h"#include "functions/Variables.h"#include "Formula.tpp"
Include dependency graph for Formula.h:
This graph shows which files directly or indirectly include this file:
Go to the source code of this file.
Data Structures | |
| class | carl::Formula< Pol > |
| Represent an SMT formula, which can be an atom for some background theory or a boolean combination of (sub)formulas. More... | |
| struct | std::hash< carl::FormulaContent< Pol > > |
| Implements std::hash for formula contents. More... | |
| struct | std::hash< carl::Formula< Pol > > |
| Implements std::hash for formulas. More... | |
Namespaces | |
| carl | |
| carl is the main namespace for the library. | |
Macros | |
| #define | ACTIVITY_LOCK_GUARD |
| #define | VARIABLES_LOCK_GUARD |
Functions | |
| template<typename P > | |
| std::ostream & | carl::operator<< (std::ostream &os, const Formula< P > &f) |
| The output operator of a formula. More... | |
