ConflictGenerator.h File Reference

#include <smtrat-mcsat/smtrat-mcsat.h>

Include dependency graph for ConflictGenerator.h:

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

Go to the source code of this file.

Data Structures
struct	smtrat::mcsat::fm::Bound
struct	smtrat::mcsat::fm::ConflictGenerator< Comparator >
struct	smtrat::mcsat::fm::DefaultComparator
	Does not order anything. More...
struct	smtrat::mcsat::fm::MaxSizeComparator
	This heuristic chooses the explanation excluding the largest interval. More...
struct	smtrat::mcsat::fm::MinSizeComparator
	This heuristic chooses the explanation excluding the smallest interval. More...
struct	smtrat::mcsat::fm::MinVarCountComparator
	This heuristic tries to minimize the number of variables occuring in the explanation. More...

Namespaces
	smtrat
	Class to create the formulas for axioms.
	smtrat::mcsat
	smtrat::mcsat::fm
	A Fourier-Motzkin based backend.

Macros
#define	mcsat_yield(callback, result)   if (callback(std::move(result))) { return; }

Functions
bool	smtrat::mcsat::fm::isSubset (const carl::Variables &subset, const carl::Variables &superset)
std::ostream &	smtrat::mcsat::fm::operator<< (std::ostream &os, const Bound &b)

Macro Definition Documentation

mcsat_yield

#define mcsat_yield	(		callback,
			result
	)		if (callback(std::move(result))) { return; }

Definition at line 68 of file ConflictGenerator.h.