smtrat::covering_ng Namespace Reference

Namespaces
	formula
	variables

Data Structures
struct	sampling
struct	sampling< SamplingAlgorithm::LOWER_UPPER_BETWEEN_SAMPLING >
	First checks lower bound and then upper bound, then checks between the cells if they are covered. More...
struct	sampling< SamplingAlgorithm::LOWER_UPPER_BETWEEN_SAMPLING_AVOID_RAN >
	First checks lower bound and then upper bound, then checks between the cells if they are covered (defers choosing interval endpoints as much as possible). More...
struct	IntervalCompare
	Sorts interval by their lower bounds. More...
struct	CoveringResult
struct	ParameterTree
class	VariableQuantification

Typedefs
template<typename PropertiesSet >
using	Interval = cadcells::datastructures::SampledDerivationRef< PropertiesSet >
template<typename PropertiesSet >
using	IntervalSet = std::set< Interval< PropertiesSet >, IntervalCompare< PropertiesSet > >

Enumerations
enum class	SamplingAlgorithm { LOWER_UPPER_BETWEEN_SAMPLING , LOWER_UPPER_BETWEEN_SAMPLING_AVOID_RAN }
enum class	Status {   SAT , UNSAT , FAILED_PROJECTION , FAILED ,   PARAMETER }

Functions
carl::Variable	first_unassigned_var (const cadcells::Assignment &ass, const cadcells::VariableOrdering &var_order)
bool	is_full_sample (const cadcells::Assignment &ass, const cadcells::VariableOrdering &var_order)
template<typename op >
std::optional< Interval< typename op::PropertiesSet > >	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 > >	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 > > >	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 > > >	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 >	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 >	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 >	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 > >	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 >	recurse_qe (cadcells::datastructures::Projections &proj, FE &f, cadcells::Assignment ass, const VariableQuantification &quantification)
void	simplify (ParameterTree &tree)
template<typename PropertiesSet >
std::ostream &	operator<< (std::ostream &os, const CoveringResult< PropertiesSet > &result)
static std::ostream &	operator<< (std::ostream &os, const ParameterTree &tree)
std::ostream &	operator<< (std::ostream &os, const VariableQuantification &vq)

Typedef Documentation

Interval

template<typename PropertiesSet >

using smtrat::covering_ng::Interval = typedef cadcells::datastructures::SampledDerivationRef<PropertiesSet>

Definition at line 19 of file types.h.

IntervalSet

template<typename PropertiesSet >

using smtrat::covering_ng::IntervalSet = typedef std::set<Interval<PropertiesSet>, IntervalCompare<PropertiesSet> >

Definition at line 32 of file types.h.

Enumeration Type Documentation

SamplingAlgorithm

enum smtrat::covering_ng::SamplingAlgorithm

strong

Enumerator
LOWER_UPPER_BETWEEN_SAMPLING
LOWER_UPPER_BETWEEN_SAMPLING_AVOID_RAN

Definition at line 6 of file Sampling.h.

Status

enum smtrat::covering_ng::Status

strong

Enumerator
SAT
UNSAT
FAILED_PROJECTION
FAILED
PARAMETER

Definition at line 34 of file types.h.

Function Documentation

characterize_covering()

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 )

inline

Definition at line 76 of file Algorithm.h.

Here is the call graph for this function:

characterize_interval()

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 )

inline

Definition at line 96 of file Algorithm.h.

Here is the call graph for this function:

exists()

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  )

inline

Definition at line 139 of file Algorithm.h.

Here is the call graph for this function:

Here is the caller graph for this function:

first_unassigned_var()

carl::Variable smtrat::covering_ng::first_unassigned_var ( const cadcells::Assignment &  ass, const cadcells::VariableOrdering &  var_order  )

inline

Definition at line 18 of file Algorithm.h.

Here is the call graph for this function:

Here is the caller graph for this function:

forall()

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  )

inline

Definition at line 222 of file Algorithm.h.

Here is the call graph for this function:

get_enclosing_interval()

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  )

inline

Definition at line 34 of file Algorithm.h.

get_enclosing_intervals()

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  )

inline

Definition at line 59 of file Algorithm.h.

Here is the call graph for this function:

is_full_sample()

bool smtrat::covering_ng::is_full_sample ( const cadcells::Assignment &  ass, const cadcells::VariableOrdering &  var_order  )

inline

Definition at line 26 of file Algorithm.h.

Here is the call graph for this function:

Here is the caller graph for this function:

operator<<() [1/3]

template<typename PropertiesSet >

std::ostream& smtrat::covering_ng::operator<<	(	std::ostream &	os,
		const CoveringResult< PropertiesSet > &	result
	)

Definition at line 78 of file types.h.

operator<<() [2/3]

static std::ostream& smtrat::covering_ng::operator<< ( std::ostream &  os, const ParameterTree &  tree  )

static

Definition at line 138 of file types.h.

operator<<() [3/3]

std::ostream& smtrat::covering_ng::operator<< ( std::ostream &  os, const VariableQuantification &  vq  )

inline

Definition at line 183 of file types.h.

Here is the call graph for this function:

parameter()

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  )

inline

Definition at line 298 of file Algorithm.h.

Here is the call graph for this function:

Here is the caller graph for this function:

recurse()

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  )

inline

Definition at line 124 of file Algorithm.h.

Here is the call graph for this function:

recurse_qe()

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  )

inline

Definition at line 397 of file Algorithm.h.

Here is the call graph for this function:

simplify()

void smtrat::covering_ng::simplify

(

ParameterTree &

tree

)

Definition at line 5 of file Simplification.cpp.

Here is the call graph for this function:

Here is the caller graph for this function: