smtrat::mcsat::onecell Namespace Reference

Data Structures
struct	BaseSettings
struct	DefaultSettings
struct	Explanation

Functions
template<typename Settings >
std::optional< cadcells::DNF >	onecell (const std::vector< cadcells::Atom > &constraints, const cadcells::Polynomial::ContextType &context, const cadcells::Assignment &sample)
	An MCSAT-style single cell explanation function. More...

Function Documentation

onecell()

template<typename Settings >

std::optional<cadcells::DNF> smtrat::mcsat::onecell::onecell	(	const std::vector< cadcells::Atom > &	constraints,
		const cadcells::Polynomial::ContextType &	context,
		const cadcells::Assignment &	sample
	)

An MCSAT-style single cell explanation function.

A set of constraints is called infeasible w.r.t. an assignment if the defining polynomials are univariate under the sample and there does not exists a value for the unassigned variable that satisfies all constraints.

This method eliminates the unassigned variable using get_level_covering or get_delineation and then constructs a single cell in the assigned variables level by level.

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 set of constraints whose conjunction describes an unsatisfying cell that can be concluded from the input constraints.

Definition at line 31 of file onecell.h.

Here is the call graph for this function: