FormulaEvaluationGraph.cpp File Reference

#include "FormulaEvaluationGraph.h"
#include <carl-arith/constraint/Conversion.h>
#include <carl-arith/ran/Conversion.h>
#include <carl-common/util/streamingOperators.h>
#include "CoveringNGStatistics.h"

Include dependency graph for FormulaEvaluationGraph.cpp:

Go to the source code of this file.

Data Structures
struct	smtrat::covering_ng::formula::formula_ds::overloaded< Ts >
struct	smtrat::covering_ng::formula::formula_ds::FormulaClassification
struct	smtrat::covering_ng::formula::pp::PolyInfo

Namespaces
	smtrat
	Class to create the formulas for axioms.
	smtrat::covering_ng
	smtrat::covering_ng::formula
	smtrat::covering_ng::formula::formula_ds
	smtrat::covering_ng::formula::pp

Enumerations
enum	smtrat::covering_ng::formula::formula_ds::CompareResult { smtrat::covering_ng::formula::formula_ds::SUBSET , smtrat::covering_ng::formula::formula_ds::SUPSET , smtrat::covering_ng::formula::formula_ds::EQ , smtrat::covering_ng::formula::formula_ds::NONE }

Functions
template<class... Ts>
	smtrat::covering_ng::formula::formula_ds::overloaded (Ts...) -> overloaded< Ts... >
void	smtrat::covering_ng::formula::formula_ds::print (std::ostream &stream, const FormulaDB &db, const FormulaID id, const std::size_t level)
void	smtrat::covering_ng::formula::formula_ds::log (const FormulaDB &db, const FormulaID id)
FormulaID	smtrat::covering_ng::formula::formula_ds::to_formula_db (cadcells::datastructures::Projections &c, const FormulaT &f, FormulaDB &db, VariableToFormula &vartof, std::map< std::size_t, FormulaID > &cache)
CompareResult	smtrat::covering_ng::formula::formula_ds::compare (const Formula::Reason &a, const Formula::Reason &b)
bool	smtrat::covering_ng::formula::formula_ds::merge_reason (Formula::Reasons &set, const Formula::Reason &add)
bool	smtrat::covering_ng::formula::formula_ds::merge_reasons (Formula::Reasons &set, const Formula::Reasons &adds)
Formula::Reason	smtrat::covering_ng::formula::formula_ds::merge (const Formula::Reason &a, const Formula::Reason &b)
Formula::Reasons	smtrat::covering_ng::formula::formula_ds::combine_reasons (const Formula::Reasons &a, const Formula::Reasons &b)
FormulaClassification	smtrat::covering_ng::formula::formula_ds::classify_formulas (const FormulaDB &db, const std::vector< FormulaID > &formulas)
carl::Variable	smtrat::covering_ng::formula::new_var (const cadcells::Assignment &old_ass, const cadcells::Assignment &new_ass)
carl::BasicConstraint< Poly >	smtrat::covering_ng::formula::pp::normalize (const carl::BasicConstraint< Poly > &c)
FormulaT	smtrat::covering_ng::formula::pp::preprocess (const FormulaT &f)
void	smtrat::covering_ng::formula::postprocess (cadcells::datastructures::Projections &proj, boost::container::flat_set< cadcells::datastructures::PolyConstraint > &i)