smtrat::mcsat::nlsat::ExplanationGenerator Class Reference

#include <ExplanationGenerator.h>

Collaboration diagram for smtrat::mcsat::nlsat::ExplanationGenerator:

Data Structures
struct	ProjectionSettings

Public Member Functions
	ExplanationGenerator (const std::vector< FormulaT > &constraints, const std::vector< carl::Variable > &vars, carl::Variable, const Model &model)
void	generateExplanation (const FormulaT &impliedAtom, std::vector< FormulasT > &explainAtomsinLvls) const
	Construct explanation in non-clausal form (without the impliedAtom/implication). More...
mcsat::Explanation	getExplanation (const FormulaT &impliedAtom) const
	Compute explanation in clausal form. More...

Private Member Functions
void	generateBoundsFor (FormulasT &boundsAsAtoms, carl::Variable var, std::size_t level, const Model &model) const
	Construct expressions for the bounds of the CADCell component (a single sector/section) at the given level. More...

Private Attributes
Model	mModel
std::vector< FormulaT >	mConstraints
cad::CADConstraints< ProjectionSettings::backtracking >	mCADConstraints
cad::ModelBasedProjectionT< ProjectionSettings >	mProjection

Detailed Description

Definition at line 92 of file ExplanationGenerator.h.

Constructor & Destructor Documentation

ExplanationGenerator()

smtrat::mcsat::nlsat::ExplanationGenerator::ExplanationGenerator ( const std::vector< FormulaT > &  constraints, const std::vector< carl::Variable > &  vars, carl::Variable  , const Model &  model  )

inline

Definition at line 161 of file ExplanationGenerator.h.

Here is the call graph for this function:

Member Function Documentation

generateBoundsFor()

void smtrat::mcsat::nlsat::ExplanationGenerator::generateBoundsFor ( FormulasT &  boundsAsAtoms, carl::Variable  var, std::size_t  level, const Model &  model  ) const

inlineprivate

Construct expressions for the bounds of the CADCell component (a single sector/section) at the given level.

Parameters

boundsAsAtoms

Output argument for cell component bounds at level as atomic formulas.

Definition at line 111 of file ExplanationGenerator.h.

Here is the call graph for this function:

Here is the caller graph for this function:

generateExplanation()

void smtrat::mcsat::nlsat::ExplanationGenerator::generateExplanation ( const FormulaT &  impliedAtom, std::vector< FormulasT > &  explainAtomsinLvls  ) const

inline

Construct explanation in non-clausal form (without the impliedAtom/implication).

It consists of atomic formulas as expressions for cell component bounds and the constraintAtoms for which a CAD was constructed. Each cell component creates zero, one or two explanation atoms. The impliedAtom is not added to facilitate conversion into a clausal form afterwards.

Definition at line 198 of file ExplanationGenerator.h.

Here is the call graph for this function:

Here is the caller graph for this function:

getExplanation()

mcsat::Explanation smtrat::mcsat::nlsat::ExplanationGenerator::getExplanation ( const FormulaT &  impliedAtom ) const

inline

Compute explanation in clausal form.

Definition at line 228 of file ExplanationGenerator.h.

Here is the call graph for this function:

Here is the caller graph for this function:

Field Documentation

mCADConstraints

cad::CADConstraints<ProjectionSettings::backtracking> smtrat::mcsat::nlsat::ExplanationGenerator::mCADConstraints

private

Definition at line 103 of file ExplanationGenerator.h.

mConstraints

std::vector<FormulaT> smtrat::mcsat::nlsat::ExplanationGenerator::mConstraints

private

Definition at line 102 of file ExplanationGenerator.h.

mModel

Model smtrat::mcsat::nlsat::ExplanationGenerator::mModel

private

Definition at line 100 of file ExplanationGenerator.h.

mProjection

cad::ModelBasedProjectionT<ProjectionSettings> smtrat::mcsat::nlsat::ExplanationGenerator::mProjection

private

Definition at line 104 of file ExplanationGenerator.h.

---

The documentation for this class was generated from the following file:

• smtrat-mcsat/explanations/nlsat/ExplanationGenerator.h