Module.h File Reference

#include <vector>
#include <set>
#include <string>
#include <atomic>
#include <mutex>
#include <smtrat-common/smtrat-common.h>
#include <smtrat-common/statistics/Statistics.h>
#include "ModuleInput.h"

Include dependency graph for Module.h:

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

Go to the source code of this file.

Data Structures
struct	smtrat::Branching
	Stores all necessary information of an branch, which can be used to detect probable infinite loop of branchings. More...
class	smtrat::Module
	A base class for all kind of theory solving methods. More...
struct	smtrat::Module::ModuleStatistics
struct	smtrat::Module::Lemma
struct	smtrat::Module::TheoryPropagation

Namespaces
	smtrat
	Class to create the formulas for axioms.

Macros
#define	OLD_SPLITTING_VARS_LOCK_GUARD
#define	OLD_SPLITTING_VARS_LOCK
#define	OLD_SPLITTING_VARS_UNLOCK

Functions
std::ostream &	smtrat::operator<< (std::ostream &os, Module::LemmaType lt)

Detailed Description

Author

Florian Corzilius

Ulrich Loup

Sebastian Junges

Since

2012-01-18

Version

2013-02-06

Definition in file Module.h.

Macro Definition Documentation

OLD_SPLITTING_VARS_LOCK

#define OLD_SPLITTING_VARS_LOCK

Definition at line 252 of file Module.h.

OLD_SPLITTING_VARS_LOCK_GUARD

#define OLD_SPLITTING_VARS_LOCK_GUARD

Definition at line 251 of file Module.h.

OLD_SPLITTING_VARS_UNLOCK

#define OLD_SPLITTING_VARS_UNLOCK

Definition at line 253 of file Module.h.