Algorithm.h File Reference

#include "types.h"
#include "FormulaEvaluation.h"
#include "FormulaEvaluationGraph.h"
#include "Sampling.h"
#include "smtrat-cadcells/common.h"
#include "FormulaEvaluationComplexity.h"
#include <algorithm>
#include <iterator>
#include <smtrat-cadcells/representation/heuristics.h>
#include <sstream>
#include "CoveringNGStatistics.h"

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

Functions
carl::Variable	smtrat::covering_ng::first_unassigned_var (const cadcells::Assignment &ass, const cadcells::VariableOrdering &var_order)
bool	smtrat::covering_ng::is_full_sample (const cadcells::Assignment &ass, const cadcells::VariableOrdering &var_order)
template<typename op >
std::optional< Interval< typename op::PropertiesSet > >	smtrat::covering_ng::get_enclosing_interval (cadcells::datastructures::Projections &proj, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &implicant, const cadcells::Assignment &ass)
template<typename op , typename FE >
std::vector< Interval< typename op::PropertiesSet > >	smtrat::covering_ng::get_enclosing_intervals (cadcells::datastructures::Projections &proj, FE &f, const cadcells::Assignment &ass)
template<typename op , cadcells::representation::CoveringHeuristic covering_heuristic>
std::optional< std::pair< Interval< typename op::PropertiesSet >, cadcells::datastructures::CoveringRepresentation< typename op::PropertiesSet > > >	smtrat::covering_ng::characterize_covering (const IntervalSet< typename op::PropertiesSet > &intervals)
template<typename op , cadcells::representation::CellHeuristic cell_heuristic>
std::optional< std::pair< Interval< typename op::PropertiesSet >, cadcells::datastructures::CellRepresentation< typename op::PropertiesSet > > >	smtrat::covering_ng::characterize_interval (Interval< typename op::PropertiesSet > &interval)
template<typename op , typename FE , cadcells::representation::CoveringHeuristic covering_heuristic, smtrat::covering_ng::SamplingAlgorithm sampling_algorithm, smtrat::cadcells::representation::CellHeuristic cell_heuristic>
CoveringResult< typename op::PropertiesSet >	smtrat::covering_ng::exists (cadcells::datastructures::Projections &proj, FE &f, cadcells::Assignment ass, const VariableQuantification &quantification, bool characterize_sat, bool characterize_unsat)
template<typename op , typename FE , cadcells::representation::CoveringHeuristic covering_heuristic, smtrat::covering_ng::SamplingAlgorithm sampling_algorithm, smtrat::cadcells::representation::CellHeuristic cell_heuristic>
CoveringResult< typename op::PropertiesSet >	smtrat::covering_ng::forall (cadcells::datastructures::Projections &proj, FE &f, cadcells::Assignment ass, const VariableQuantification &quantification, bool characterize_sat, bool characterize_unsat)
template<typename op , typename FE , cadcells::representation::CoveringHeuristic covering_heuristic, smtrat::covering_ng::SamplingAlgorithm sampling_algorithm, smtrat::cadcells::representation::CellHeuristic cell_heuristic>
CoveringResult< typename op::PropertiesSet >	smtrat::covering_ng::recurse (cadcells::datastructures::Projections &proj, FE &f, cadcells::Assignment &ass, const VariableQuantification &quantification, bool characterize_sat=false, bool characterize_unsat=false)
template<typename op , typename FE , cadcells::representation::CoveringHeuristic covering_heuristic, smtrat::covering_ng::SamplingAlgorithm sampling_algorithm, smtrat::cadcells::representation::CellHeuristic cell_heuristic>
std::pair< CoveringResult< typename op::PropertiesSet >, std::vector< ParameterTree > >	smtrat::covering_ng::parameter (cadcells::datastructures::Projections &proj, FE &f, cadcells::Assignment ass, const VariableQuantification &quantification)
template<typename op , typename FE , cadcells::representation::CoveringHeuristic covering_heuristic, smtrat::covering_ng::SamplingAlgorithm sampling_algorithm, smtrat::cadcells::representation::CellHeuristic cell_heuristic>
std::pair< CoveringResult< typename op::PropertiesSet >, ParameterTree >	smtrat::covering_ng::recurse_qe (cadcells::datastructures::Projections &proj, FE &f, cadcells::Assignment ass, const VariableQuantification &quantification)