SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Tableau.h File Reference
#include <vector>
#include <stack>
#include <map>
#include <deque>
#include <limits>
#include "Variable.h"
#include <carl-common/memory/IDPool.h>
#include "Tableau.tpp"
Include dependency graph for Tableau.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures

class  smtrat::lra::TableauEntry< T1, T2 >
 
class  smtrat::lra::Tableau< Settings, T1, T2 >
 
struct  smtrat::lra::Tableau< Settings, T1, T2 >::LearnedBound
 
class  smtrat::lra::Tableau< Settings, T1, T2 >::Iterator
 

Namespaces

 smtrat
 Class to create the formulas for axioms.
 
 smtrat::lra
 

Detailed Description

Author
Florian Corzilius corzi.nosp@m.lius.nosp@m.@cs.r.nosp@m.wth-.nosp@m.aache.nosp@m.n.de
Since
2012-04-05
Version
2014-10-01

Definition in file Tableau.h.