onecell.h File Reference

#include <set>
#include <smtrat-cadcells/common.h>
#include <smtrat-cadcells/helper_formula.h>
#include <smtrat-cadcells/operators/operator_mccallum.h>
#include <smtrat-cadcells/operators/operator_mccallum_pdel.h>
#include <smtrat-cadcells/operators/operator_mccallum_filtered.h>
#include <smtrat-cadcells/representation/heuristics.h>
#include <smtrat-cadcells/algorithms/level_covering.h>
#include <smtrat-cadcells/algorithms/interval.h>
#include <carl-formula/formula/functions/Visit.h>

Include dependency graph for onecell.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::onecell

Functions
template<typename Settings >
std::optional< cadcells::DNF >	smtrat::mcsat::onecell::onecell (const std::vector< cadcells::Atom > &constraints, const cadcells::Polynomial::ContextType &context, const cadcells::Assignment &sample)
	An MCSAT-style single cell explanation function. More...