smtrat::mcsat::nlsat::Explanation Struct Reference

#include <Explanation.h>

Public Member Functions
std::optional< mcsat::Explanation >	operator() (const mcsat::Bookkeeping &data, carl::Variable var, const FormulasT &reason, bool) const
	We construct a formula 'E -> I', i.e. More...

Detailed Description

Definition at line 12 of file Explanation.h.

Member Function Documentation

operator()()

std::optional< mcsat::Explanation > smtrat::mcsat::nlsat::Explanation::operator()	(	const mcsat::Bookkeeping &	data,
		carl::Variable	var,
		const FormulasT &	reason,
		bool
	)		const

We construct a formula 'E -> I', i.e.

'e1 & e2 ... en -> i', called "Explanation", in its clausal form '-e1 v -e2 ... en v i', where e1, e2.. are reason Atoms and CAD cell bound atoms, and i is the implication. It "explains" why the assignment point in data is inconsistent with the reason atoms/constraints and the implication in that it constructs a whole region of assignments points, which the assignment point in data is a part of.

Parameters

variableOrdering	Determine the order of variables, e.g. x1, x2, .. x10
data	Represent the assigned variables and their assigned values in different representations. These are a prefix of the variableOrdering, e.g. x1, x2, .. x5
var	The smallest/first variable in the variableOrdering that is not assigned by data, e.g. x6
reason	A collection of atoms that are inconsistent together or imply the implication. These atoms mention only variables x1, x2.. x6 (some atom definitely mentions x6) and possibly x7..x10 if they are irrelevant and "vanish" under the assignment in data, e.g. x1*x7+x6=0 (for x1 := 0) or x6*(x7^2+1)>0 (equiv to x6>0, since x7^2+1 > 0)

Definition at line 11 of file Explanation.cpp.

Here is the call graph for this function:

---

The documentation for this struct was generated from the following files:

• smtrat-mcsat/explanations/nlsat/Explanation.h
• smtrat-mcsat/explanations/nlsat/Explanation.cpp