smtrat::covering_ng::variables::impl Namespace Reference

Functions
template<mcsat::VariableOrdering vo>
std::vector< carl::Variable >	variable_ordering (const carl::QuantifierPrefix &quantifiers, const FormulaT &formula)
	Calculates a variable ordering based on the given quantifier blocks and the given formula. More...
std::vector< carl::Variable >	sort_earliest_splitting (const carl::QuantifierPrefix &prefix, const FormulaT &base_formula)
	Calculates a variable ordering based on the given quantifier blocks and the given formula. More...

Function Documentation

sort_earliest_splitting()

std::vector<carl::Variable> smtrat::covering_ng::variables::impl::sort_earliest_splitting ( const carl::QuantifierPrefix &  prefix, const FormulaT &  base_formula  )

inline

Calculates a variable ordering based on the given quantifier blocks and the given formula.

Heuristic such that the formula can be split as early as possible

Parameters

quantifiers	The quantifier blocks (Variables in a block can be exchanged, blocks can not be exchanged)
base_formula	Formula to calculate the variable ordering for.

Returns

Variable ordering.

The variable ordering is calculated as follows:

1. Identify the first opportunity to split the formula. This is the first time that the formula is not an atom and not a negation of an atom. If there is no such opportunity, return some other variable ordering.
2. For each pairwise combination of subformulas, calculate the set of shared variables
3. Iterate over the quantifier blocks and for each block, sort the variables by the number of occurrences in the sets of shared variables and the size of the smallest set of shared variables in which the variable occurs. If the heuristic is inconclusive, sort the remaining variables of this block by some other variable ordering
4. Return the resulting vector.

Definition at line 111 of file VariableOrdering.h.

Here is the call graph for this function:

Here is the caller graph for this function:

variable_ordering()

template<mcsat::VariableOrdering vo>

std::vector<carl::Variable> smtrat::covering_ng::variables::impl::variable_ordering ( const carl::QuantifierPrefix &  quantifiers, const FormulaT &  formula  )

inline

Calculates a variable ordering based on the given quantifier blocks and the given formula.

Template Parameters

vo	The variable ordering heuristic to use.

Parameters

quantifiers	The quantifier blocks (Variables in a block can be exchanged, blocks can not be exchanged)
formula	Formula to calculate the variable ordering for.

Returns

Variable ordering.

The variable ordering is calculated as follows:

1. Calculate the variable ordering for the formula as if there were no quantifiers. This is done by calling mcsat::calculate_variable_order<vo>(constraints). In code this is called the unblocked variable ordering
2. Sort the variables in the unblocked variable ordering by the quantifier block they are in. The order of the quantifier blocks is the same as in the vector quantifiers. Use a stable sort such that the order of the variables in a quantifier block is not changed.
3. Return the resulting vector.

Definition at line 67 of file VariableOrdering.h.

Here is the caller graph for this function: