smtrat::cadcells::algorithms Namespace Reference

Various algorithms as well as helper functions for developing new algorithms. More...

Functions
template<typename op , representation::CellHeuristic cell_heuristic>
std::optional< std::pair< carl::Variable, datastructures::SymbolicInterval > >	get_interval (datastructures::SampledDerivationRef< typename op::PropertiesSet > &cell_deriv)
	Single cell construction algorithm. More...
template<typename op , representation::CoveringHeuristic covering_heuristic>
std::optional< datastructures::SampledDerivationRef< typename op::PropertiesSet > >	get_level_covering (datastructures::Projections &proj, const std::vector< Atom > &constraints, const Assignment &sample)
	Computes an unsat covering w.r.t. More...
template<typename op >
std::vector< datastructures::SampledDerivationRef< typename op::PropertiesSet > >	get_unsat_intervals (const Constraint &c, datastructures::Projections &proj, const Assignment &sample)
template<typename op >
std::vector< datastructures::SampledDerivationRef< typename op::PropertiesSet > >	get_unsat_intervals (const VariableComparison &c, datastructures::Projections &proj, const Assignment &sample)
template<typename op >
std::vector< datastructures::SampledDerivationRef< typename op::PropertiesSet > >	get_unsat_intervals (const Atom &c, datastructures::Projections &proj, const Assignment &sample)
	Returns the unsat intervals of the given atom w.r.t. More...

Detailed Description

Various algorithms as well as helper functions for developing new algorithms.

Function Documentation

get_interval()

template<typename op , representation::CellHeuristic cell_heuristic>

std::optional<std::pair<carl::Variable, datastructures::SymbolicInterval> > smtrat::cadcells::algorithms::get_interval

(

datastructures::SampledDerivationRef< typename op::PropertiesSet > &

cell_deriv

)

Single cell construction algorithm.

Template Parameters

op	The operator.
cell_heuristic	The cell heuristic.

Parameters

cell_deriv

A derivation object to construct the cell from.

Returns

A vector of pairs of variables and their symbolic intervals on success or std::nullopt otherwise.

Definition at line 16 of file interval.h.

Here is the call graph for this function:

get_level_covering()

template<typename op , representation::CoveringHeuristic covering_heuristic>

std::optional<datastructures::SampledDerivationRef<typename op::PropertiesSet> > smtrat::cadcells::algorithms::get_level_covering	(	datastructures::Projections &	proj,
		const std::vector< Atom > &	constraints,
		const Assignment &	sample
	)

Computes an unsat covering w.r.t.

a set of constraints.

If a constraint is univariate under a sample, for the unassinged variables, the constraint induces intervals in which the constraint will be conflicting. If multiple such intervals from a set of constraints cover the real line, then the partial sample cannot be extended without making a conflict. This conflict is generalized.

Parameters

constraints	Atoms of the same level such that sample cannot be extended for the highest variable without making one atom false. Note that this property is not checked.
sample	A sample such that all but the highest variable in constraints are assigned.

Returns

A sampled derivation which contains the information to reproduce the conflict.

Definition at line 15 of file level_covering.h.

Here is the call graph for this function:

get_unsat_intervals() [1/3]

template<typename op >

std::vector<datastructures::SampledDerivationRef<typename op::PropertiesSet> > smtrat::cadcells::algorithms::get_unsat_intervals	(	const Atom &	c,
		datastructures::Projections &	proj,
		const Assignment &	sample
	)

Returns the unsat intervals of the given atom w.r.t.

an underlying sample.

Parameters

c	A constraint or a variable comparison.
sample	A sample point such that the highest variable in c w.r.t. the variable odering in proj is the only unassigned variable.

Returns

A list of sampled derivations with the same delineated derivations. The samples for the unassigned variables are sampled from the respective interval.

Definition at line 189 of file unsat_intervals.h.

get_unsat_intervals() [2/3]

template<typename op >

std::vector<datastructures::SampledDerivationRef<typename op::PropertiesSet> > smtrat::cadcells::algorithms::get_unsat_intervals	(	const Constraint &	c,
		datastructures::Projections &	proj,
		const Assignment &	sample
	)

Definition at line 8 of file unsat_intervals.h.

Here is the call graph for this function:

get_unsat_intervals() [3/3]

template<typename op >

std::vector<datastructures::SampledDerivationRef<typename op::PropertiesSet> > smtrat::cadcells::algorithms::get_unsat_intervals	(	const VariableComparison &	c,
		datastructures::Projections &	proj,
		const Assignment &	sample
	)

Definition at line 101 of file unsat_intervals.h.

Here is the call graph for this function: