utils.h File Reference

#include <carl-arith/poly/umvpoly/functions/Derivative.h>
#include <carl-arith/poly/umvpoly/functions/Factorization.h>
#include <carl-arith/poly/umvpoly/functions/Resultant.h>
#include <carl-arith/poly/umvpoly/functions/Definiteness.h>
#include <carl-arith/poly/umvpoly/functions/Representation.h>
#include <smtrat-common/smtrat-common.h>
#include <smtrat-common/model.h>
#include <smtrat-cad/projectionoperator/utils.h>
#include <smtrat-mcsat/utils/Bookkeeping.h>
#include <algorithm>
#include <optional>
#include <set>
#include <unordered_map>
#include <variant>
#include <vector>
#include <carl-arith/ran/ran.h>
#include "RealAlgebraicPoint.h"
#include "OCStatistics.h"
#include "Assertables.h"

Include dependency graph for utils.h:

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

Go to the source code of this file.

Data Structures
struct	smtrat::mcsat::onecellcad::TagPoly
	Tagged Polynomials. More...
struct	smtrat::mcsat::onecellcad::Section
	Represent a cell's (closed-interval-boundary) component along th k-th axis. More...
struct	smtrat::mcsat::onecellcad::Sector
	Represent a cell's open-interval boundary object along one single axis by two irreducible, multivariate polynomials of level k. More...
class	smtrat::mcsat::onecellcad::OneCellCAD

Namespaces
	smtrat
	Class to create the formulas for axioms.
	smtrat::mcsat
	smtrat::mcsat::onecellcad

Typedefs
using	smtrat::mcsat::onecellcad::RAN = smtrat::RAN
using	smtrat::mcsat::onecellcad::RANMap = std::map< carl::Variable, RAN >
using	smtrat::mcsat::onecellcad::CADCell = std::vector< std::variant< Sector, Section > >
	Represent a single cell [brown15]. More...

Enumerations
enum class	smtrat::mcsat::onecellcad::InvarianceType { smtrat::mcsat::onecellcad::ORD_INV , smtrat::mcsat::onecellcad::SIGN_INV }
	Invariance Types. More...

Functions
std::ostream &	smtrat::mcsat::onecellcad::operator<< (std::ostream &os, const InvarianceType &inv)
bool	smtrat::mcsat::onecellcad::operator< (const InvarianceType &l, const InvarianceType &r)
std::ostream &	smtrat::mcsat::onecellcad::operator<< (std::ostream &os, const TagPoly &p)
bool	smtrat::mcsat::onecellcad::operator== (const TagPoly &lhs, const TagPoly &rhs)
std::ostream &	smtrat::mcsat::onecellcad::operator<< (std::ostream &os, const std::vector< TagPoly > &polys)
std::ostream &	smtrat::mcsat::onecellcad::operator<< (std::ostream &os, const std::vector< std::vector< TagPoly >> &lvls)
std::size_t	smtrat::mcsat::onecellcad::getDegree (TagPoly p, carl::Variable v)
std::optional< std::size_t >	smtrat::mcsat::onecellcad::levelOf (const std::vector< carl::Variable > &variableOrder, const Poly &poly)
	Find the index of the highest variable (wrt. More...
std::vector< TagPoly >	smtrat::mcsat::onecellcad::nonConstIrreducibleFactors (std::vector< carl::Variable > variableOrder, Poly poly, InvarianceType tag)
void	smtrat::mcsat::onecellcad::appendOnCorrectLevel (const Poly &poly, InvarianceType tag, std::vector< std::vector< TagPoly >> &polys, std::vector< carl::Variable > variableOrder)
std::ostream &	smtrat::mcsat::onecellcad::operator<< (std::ostream &os, const Section &s)
std::ostream &	smtrat::mcsat::onecellcad::operator<< (std::ostream &os, const Sector &s)
std::ostream &	smtrat::mcsat::onecellcad::operator<< (std::ostream &os, const CADCell &cell)
std::vector< Poly >	smtrat::mcsat::onecellcad::asMultiPolys (const std::vector< TagPoly > polys)
bool	smtrat::mcsat::onecellcad::contains (const std::vector< TagPoly > &polys, const Poly &poly)
template<typename T >
bool	smtrat::mcsat::onecellcad::contains (const std::vector< T > &list, const T &elem)
MultivariateRootT	smtrat::mcsat::onecellcad::asRootExpr (carl::Variable rootVariable, Poly poly, std::size_t rootIdx)
RealAlgebraicPoint< smtrat::Rational >	smtrat::mcsat::onecellcad::asRANPoint (const mcsat::Bookkeeping &data)
template<typename T >
std::vector< T >	smtrat::mcsat::onecellcad::prefix (const std::vector< T > vars, std::size_t prefixSize)
std::vector< std::pair< Poly, Poly > >	smtrat::mcsat::onecellcad::duplicateElimination (std::vector< std::pair< Poly, Poly >> vec)
void	smtrat::mcsat::onecellcad::duplicateElimination (std::vector< Poly > &vec)
Poly	smtrat::mcsat::onecellcad::discriminant (const carl::Variable &mainVariable, const Poly &p)
	Projection related utilities for onecellcad. More...
Poly	smtrat::mcsat::onecellcad::resultant (const carl::Variable &mainVariable, const Poly &p1, const Poly &p2)
Poly	smtrat::mcsat::onecellcad::leadcoefficient (const carl::Variable &mainVariable, const Poly &p)
void	smtrat::mcsat::onecellcad::addResultants (std::vector< std::pair< Poly, Poly >> &resultants, std::vector< std::vector< TagPoly >> &polys, carl::Variable mainVar, const std::vector< carl::Variable > &variableOrder)
std::size_t	smtrat::mcsat::onecellcad::cellDimension (const CADCell &cell, const std::size_t uptoLevel)
CADCell	smtrat::mcsat::onecellcad::fullSpaceCell (std::size_t cellComponentCount)
bool	smtrat::mcsat::onecellcad::optimized_singleLevelFullProjection (carl::Variable mainVar, size_t currentLevel, std::vector< std::vector< TagPoly >> &projectionLevels, OneCellCAD &cad)
void	smtrat::mcsat::onecellcad::singleLevelFullProjection (std::vector< carl::Variable > &variableOrder, carl::Variable mainVar, size_t currentLevel, std::vector< std::vector< TagPoly >> &projectionLevels)