ModuleInput.h File Reference

#include <algorithm>
#include <list>
#include <vector>
#include <set>
#include <iterator>
#include <smtrat-common/smtrat-common.h>
#include <smtrat-common/model.h>

Include dependency graph for ModuleInput.h:

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

Go to the source code of this file.

Data Structures
class	smtrat::FormulaWithOrigins
	Stores a formula along with its origins. More...
class	smtrat::ModuleInput
	The input formula a module has to consider for it's satisfiability check. More...
struct	smtrat::ModuleInput::IteratorCompare

Namespaces
	smtrat
	Class to create the formulas for axioms.

Functions
std::ostream &	smtrat::operator<< (std::ostream &os, const ModuleInput &mi)
template<typename AnnotationType >
void	smtrat::annotateFormula (const FormulaT &, const std::vector< AnnotationType > &)

Detailed Description

Author

Florian Corzilius

Version

2014-05-16

Definition in file ModuleInput.h.