ConstraintCategorization.h File Reference

#include <smtrat-common/smtrat-common.h>
#include <smtrat-common/model.h>
#include <carl-common/util/enum_util.h>
#include <iostream>

Include dependency graph for ConstraintCategorization.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.
	smtrat::mcsat
	smtrat::mcsat::constraint_type

Enumerations
enum class	smtrat::mcsat::ConstraintType { smtrat::mcsat::Constant , smtrat::mcsat::Assigned , smtrat::mcsat::Univariate , smtrat::mcsat::Unassigned }
	This type categorizes constraints with respect to a given (partial) model and the next variable to be assigned. More...

Functions
std::ostream &	smtrat::mcsat::operator<< (std::ostream &os, ConstraintType ct)
template<typename T >
ConstraintType	smtrat::mcsat::constraint_type::categorize (const T &t, const Model &model, carl::Variable next)
template<typename T >
bool	smtrat::mcsat::constraint_type::is_constant (const T &t)
	Checks whether the constraint is constant, i.e. More...
template<typename T >
bool	smtrat::mcsat::constraint_type::isAssigned (const T &t, const Model &model)
	Checks whether all variables contained in the constraint are assigned in the model. More...
template<typename T >
bool	smtrat::mcsat::constraint_type::is_univariate (const T &t, const Model &model, carl::Variable next)
	Checks whether the constraint contains only a single unassigned variable, and this is the next one. More...
template<typename T >
bool	smtrat::mcsat::constraint_type::isUnassigned (const T &t, const Model &model, carl::Variable next)
	Checks whether the constraint contains an unassigned variable that is not the next one. More...