smtrat-mcsat.h File Reference

#include "utils/Bookkeeping.h"
#include "utils/ClauseChain.h"
#include "utils/ConstraintCategorization.h"
#include <smtrat-common/smtrat-common.h>

Include dependency graph for smtrat-mcsat.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Namespaces
	smtrat
	Class to create the formulas for axioms.
	smtrat::mcsat

Typedefs
using	smtrat::mcsat::ModelValues = std::vector< std::pair< carl::Variable, ModelValue > >
using	smtrat::mcsat::AssignmentOrConflict = std::variant< ModelValues, FormulasT >
using	smtrat::mcsat::Explanation = std::variant< FormulaT, ClauseChain >

Functions
FormulaT	smtrat::mcsat::resolveExplanation (const Explanation &expl)