types.h File Reference

#include <carl-arith/poly/umvpoly/MultivariatePolynomial.h>
#include <carl-arith/core/Variable.h>
#include <carl-arith/poly/VarInfo.h>
#include <carl-formula/formula/Formula.h>
#include <carl-formula/formula/Logic.h>
#include <carl-common/util/streamingOperators.h>
#include <carl-common/util/enum_util.h>
#include <atomic>

Include dependency graph for types.h:

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

Go to the source code of this file.

Namespaces
	smtrat
	Class to create the formulas for axioms.

Typedefs
using	smtrat::Conditionals = std::vector< std::atomic_bool * >
	A vector of atomic bool pointers. More...
using	smtrat::Rational = mpq_class
using	smtrat::Integer = carl::IntegralType< Rational >::type
using	smtrat::TermT = carl::Term< Rational >
using	smtrat::Poly = carl::MultivariatePolynomial< Rational >
using	smtrat::Factorization = std::map< Poly, carl::uint >
using	smtrat::ConstraintT = carl::Constraint< Poly >
using	smtrat::ConstraintsT = carl::Constraints< Poly >
using	smtrat::VariableAssignmentT = carl::VariableAssignment< Poly >
using	smtrat::VariableComparisonT = carl::VariableComparison< Poly >
using	smtrat::FormulaT = carl::Formula< Poly >
using	smtrat::FormulasT = carl::Formulas< Poly >
using	smtrat::FormulaSetT = carl::FormulaSet< Poly >
using	smtrat::FormulasMultiT = std::multiset< FormulaT >
using	smtrat::RationalAssignment = carl::Assignment< Rational >
using	smtrat::RAN = carl::IntRepRealAlgebraicNumber< Rational >
using	smtrat::thread_priority = std::pair< std::size_t, std::size_t >

Enumerations
enum	smtrat::LemmaLevel { smtrat::NONE = 0 , smtrat::NORMAL = 1 , smtrat::ADVANCED = 2 }
enum	smtrat::Answer {   smtrat::SAT = 0 , smtrat::UNSAT = 1 , smtrat::UNKNOWN = 2 , smtrat::ABORTED = 3 ,   smtrat::OPTIMAL = 4 }
	An enum with the possible answers a Module can give. More...

Functions
bool	smtrat::is_sat (Answer a)
std::ostream &	smtrat::operator<< (std::ostream &os, Answer a)