File List

Here is a list of all files with brief descriptions:

[detail level 12345]

► benchmax
► backends
► slurm
SlurmSettings.cpp
SlurmSettings.h
SlurmUtilities.cpp
SlurmUtilities.h
► ssh
Node.h
SSHConnection.h
SSHScheduler.cpp
SSHScheduler.h
SSHSettings.cpp
SSHSettings.h
Backend.h
Backends.h
CondorBackend.h
Jobs.h
LocalBackend.h
SlurmBackend.h
SSHBackend.h
► benchmarks
benchmarks.cpp
benchmarks.h
BenchmarkSet.cpp
BenchmarkSet.h
► results
BenchmarkResult.h
CSVWriter.h
Database.h
Database_mysqlconnector.h
Database_mysqlpp.h
Results.h
XMLWriter.h
► settings
PresetSettings.cpp
PresetSettings.h
Settings.h
SettingsParser.cpp
SettingsParser.h
► tools
MathSAT.h
Minisat.h
Minisatp.h
SMTRAT.h
SMTRAT_Analyzer.h
SMTRAT_OPB.h
Tool.h
Tools.cpp
Tools.h
Z3.h
► utils
execute.h
filesystem.h
parsing.h
benchmax.cpp
config.h
logging.h
► cli
► parser
► theories
AbstractTheory.h
Arithmetic.cpp
Arithmetic.h
Attribute.h
Bitvector.cpp
Bitvector.h
BooleanEncoding.cpp
BooleanEncoding.h
Common.h
Conversions.h
Core.cpp
Core.h
FunctionInstantiator.h
ParserState.h
Theories.h
TheoryTypes.h
Uninterpreted.cpp
Uninterpreted.h
Attribute.h
Common.h
Identifier.h
InstructionHandler.h
Lexicon.h
Parser.h
ParserSettings.h
ParserWrapper.cpp
ParserWrapper.h
Script.h
SExpression.h
Sort.h
Term.h
VariantMap.h
► tools
cnf_conversion.cpp
cnf_conversion.h
compile_information.cpp
compile_information.h
config.h
execute_smtlib.h
ExecutionState.h
Executor.h
formula_analyzer.cpp
formula_analyzer.h
parser_dimacs.h
parser_opb.h
parser_smtlib.cpp
parser_smtlib.h
parser_smtlib_utils.h
preprocessor.cpp
preprocessor.h
CLIStatistics.h
config.h
ExitCodes.h
handle_options.h
ResourceLimitation.h
smtratSolver.cpp
► doc
► markdown
developers
modules
tools
► smtrat-analyzer
► analyzers
cad_projections.cpp
cad_projections.h
cnf.cpp
cnf.h
formula_types.cpp
formula_types.h
utils.h
variables.cpp
variables.h
settings.h
smtrat-analyzer.cpp
smtrat-analyzer.h
statistics.h
► smtrat-cad
► debug
DotHelper.h
TikzHistoryPrinter.h
► lifting
LiftingTree.h
Sample.h
SampleComparator.h
SampleIteratorQueue.h
► projection
BaseProjection.h
PolynomialLiftingQueue.h
Projection.h
Projection_EC.h
Projection_F.h
Projection_Model.h
Projection_NO.h
Projection_NU.h
Projection_S.h
Projection_utils.h
ProjectionComparator.h
ProjectionInformation.h
► projectionoperator
Brown.h
Collins.h
Hong.h
Lazard.h
McCallum.h
McCallum_partial.h
ProjectionOperator.h
utils.h
► utils
CADConstraints.h
CADCore.h
CADPreprocessor.cpp
CADPreprocessor.h
ConflictGraph.cpp
ConflictGraph.h
DynamicPriorityQueue.h
MISGeneration.h
Origin.h
Preprocessor.cpp
Preprocessor.h
► variableordering
triangular_ordering.cpp
triangular_ordering.h
CAD.h
common.h
Settings.h
smtrat-cad.cpp
smtrat-cad.h
► smtrat-cadcells
► algorithms
interval.h
level_covering.h
unsat_intervals.h
► datastructures
delineation.h
derivation.h
polynomials.h
projections.h
properties.h
representation.h
roots.h
► operators
operator.h
operator_mccallum.h
operator_mccallum_filtered.h
operator_mccallum_pdel.h
properties.h
properties_util.h
rules.h
rules_covering.h
rules_filter.h
rules_filter_util.h
rules_null.h
rules_pdel.h
► representation
► approximation
ApproximationSettings.h
CellApproximator.h
criteria.h
ran_approximation.h
heuristics.h
heuristics_approximation.h
heuristics_cell.h
heuristics_covering.h
util.h
CADCellsStatistics.cpp
CADCellsStatistics.h
common.h
helper_formula.h
OCApproximationStatistics.h
smtrat-cadcells.cpp
smtrat-cadcells.h
► smtrat-common
► checkpoints
Checkpoints.h
► settings
Settings.h
SettingsComponents.h
SettingsParser.cpp
SettingsParser.h
► statistics
Statistics.h
StatisticsSettings.h
► validation
Validation.h
ValidationCollector.h
ValidationPoint.h
ValidationPrinter.h
ValidationSettings.h
config.h
logging.h	Use your own judgement for the following log levels: TRACE Finer-grained informational events than the DEBUG
model.h
smtrat-common.cpp
smtrat-common.h
types.h
► smtrat-coveringng
Algorithm.h
CoveringNGStatistics.cpp
CoveringNGStatistics.h
FormulaEvaluation.h
FormulaEvaluationComplexity.h
FormulaEvaluationGraph.cpp
FormulaEvaluationGraph.h
Sampling.h
Simplification.cpp
Simplification.h
types.h
VariableOrdering.h
► smtrat-expressions
► simplifier
BaseSimplifier.h
DuplicateSimplifier.h
MergeSimplifier.h
NegationSimplifier.h
Simplifier.h
SingletonSimplifier.h
Expression.cpp
Expression.h
ExpressionContent.cpp
ExpressionContent.h
ExpressionConverter.h
ExpressionHash.h
ExpressionPool.cpp
ExpressionPool.h
ExpressionTest.h
ExpressionTypes.h
ExpressionVisitor.h
► smtrat-fmplex
eliminate.cpp
eliminate.h
fmplex.cpp
fmplex.h
Matrix.h
Node.h
► smtrat-max-smt
MaxSMT.h
MaxSMT_FuMalikIncremental.h
MaxSMT_LinearSearch.h
MaxSMT_MSU3.h
smtrat-max-smt.cpp
smtrat-max-smt.h
► smtrat-mcsat
► assignments
► arithmetic
AAFStatistics.h
AssignmentFinder.cpp
AssignmentFinder.h
AssignmentFinder_arithmetic.h
AssignmentFinder_ctx.h
Covering.h
RootIndexer.h
► smtaf
AssignmentFinder.h
AssignmentFinder_SMT.cpp
AssignmentFinder_SMT.h
SMTAFStatistics.h
SequentialAssignment.h
► explanations
► fm
ConflictGenerator.h
Explanation.cpp
Explanation.h
FMStatistics.h
► icp
Dependencies.h
Explanation.cpp
Explanation.h
ICPStatistics.h
IntervalPropagation.h
► nlsat
Explanation.cpp
Explanation.h
ExplanationGenerator.h
NLSATStatistics.h
► onecell
Explanation.h
OCStatistics.h
onecell.h
► onecellcad
► levelwise
Explanation.cpp
Explanation.h
OneCellCAD.h	Construct a single open CAD Cell IN A LEVEL-WISE MANNER around a given point that is sign-invariant on a given set of polynomials
► recursive
Explanation.cpp
Explanation.h
OneCellCAD.h	Construct a single open CAD Cell around a given point that is sign-invariant on a given set of polynomials
OpenCAD.h	Construct a single open CAD Cell around a given point that is sign-invariant on a given set of polynomials
Assertables.h	A collection of helper functions to check assertable conditions for CAD properties, preconditions and invariants
OCStatistics.h
RealAlgebraicPoint.h
utils.cpp
utils.h
► vs
Explanation.cpp
Explanation.h
ExplanationGenerator.h
VSHelper.h
VSStatistics.h
FastParallelExplanation.h
FullParallelExplanation.h
ParallelExplanation.h
SequentialExplanation.h
► utils
Bookkeeping.h
ClauseChain.cpp
ClauseChain.h
ConstraintCategorization.h
RootExpr.h
► variableordering
feature_based.h
greedy_max_univariate.h
helper.h
VariableOrdering.h
smtrat-mcsat.cpp
smtrat-mcsat.h
► smtrat-modules
► BEModule
BEModule.h	A module, which searches for bounds of arithmetic variables and polynomials
BEModule.tpp
BESettings.h
BESettings1Instantiation.cpp
► BVModule
BVDirectEncoder.h
BVModule.h
BVModule.tpp
BVSettings.h
BVSettings1Instantiation.cpp
► CNFerModule
CNFerModule.h
CNFerModule.tpp
CNFerModuleStatistics.h
► CoCoAGBModule
CoCoAGBModule.h
CoCoAGBModule.tpp
CoCoAGBSettings.h
CoCoAGBSettings1Instantiation.cpp
CoCoAGBSettings2Instantiation.cpp
► CoveringNGModule
CoveringNGModule.h
CoveringNGModule.tpp
CoveringNGSettings.h
CoveringNGSettingsDefaultInstantiation.cpp
► CSplitModule
Bimap.h
CSplitModule.h
CSplitModule.tpp
CSplitSettings.h
CSplitSettings1Instantiation.cpp
► CubeLIAModule
CubeLIAModule.h
CubeLIAModule.tpp
CubeLIASettings.h
CubeLIASettings1Instantiation.cpp
► CurryModule
CurryModule.h
CurryModule.tpp
CurrySettings.h
CurrySettings1Instantiation.cpp
► EMModule
EMModule.h
EMModule.tpp
EMSettings.h
EMSettings1Instantiation.cpp
► ESModule
ESModule.h	A module, which iteratively finds boolean and arithmetic substitutions and applies them to all formulas which are connected to this substitution by a conjunction
ESModule.tpp
ESSettings.h
ESSettingsDefaultInstantiation.cpp
ESSettingsLimitSubstitutionInstantiation.cpp
► FPPModule
FPPModule.h
FPPModule.tpp
FPPSettings.h
FPPSettings1Instantiation.cpp
FPPSettings1OldInstantiation.cpp
FPPSettings2Instantiation.cpp
FPPSettings3Instantiation.cpp
FPPSettingsOptimizationInstantiation.cpp
FPPSettingsPBGroebnerInstantiation.cpp
FPPSettingsPBInstantiation.cpp
FPPStatistics.h
► GBModule
GBCalculationStatistics.cpp
GBCalculationStatistics.h
GBModule.h
GBModule.tpp
GBModuleState.h
GBModuleStatistics.cpp
GBModuleStatistics.h
GBSettings.h
GBSettings1Instantiation.cpp
GBSettings3Instantiation.cpp
GBSettings41Instantiation.cpp
GBSettings43Instantiation.cpp
GBSettings4Instantiation.cpp
GBSettings51AInstantiation.cpp
GBSettings51Instantiation.cpp
GBSettings5Instantiation.cpp
GBSettings61AInstantiation.cpp
GBSettings61Instantiation.cpp
GBSettings63Instantiation.cpp
GBSettings6Instantiation.cpp
InequalitiesTable.h
InequalitiesTable.tpp
RewriteRules.h
UsingDeclarations.h
VariableRewriteRule.h
► GBPPModule
GBPPModule.h	Supports optimization
GBPPModule.tpp
GBPPSettings.h
GBPPSettings1Instantiation.cpp
► ICEModule
ForwardHyperGraph.h
ForwardHyperGraph.tpp
ICEModule.h
ICEModule.tpp
ICESettings.h
ICESettings1Instantiation.cpp
► ICPModule
ContractionCandidate.cpp
ContractionCandidate.h
ContractionCandidateManager.cpp
ContractionCandidateManager.h
HistoryNode.h
ICPModule.h
ICPModule.tpp
ICPSettings.h	Class to create a settings object for the ICPModule
ICPSettings1Instantiation.cpp
ICPSettings2Instantiation.cpp
ICPSettings3Instantiation.cpp
ICPSettings4Instantiation.cpp
IcpVariable.h
utils.cpp
utils.h
► IncWidthModule
IncWidthModule.h
IncWidthModule.tpp
IncWidthSettings.h
IncWidthSettings1Instantiation.cpp
IncWidthSettings2Instantiation.cpp
IncWidthSettings3Instantiation.cpp
► IntBlastModule
IntBlastModule.h
IntBlastModule.tpp
IntBlastSettings.h
IntBlastSettings1Instantiation.cpp
IntBlastSettings2Instantiation.cpp
PolyTree.cpp
PolyTree.h
PolyTreePool.cpp
PolyTreePool.h
► IntEqModule
IntEqModule.h
IntEqModule.tpp
IntEqSettings.h
IntEqSettings1Instantiation.cpp
► LRAModule
► tableau
Bound.h
Bound.tpp
Numeric.cpp
Numeric.h
Tableau.h
Tableau.tpp
TableauSettings.h	Class to create a settings object for the Tableau
Value.h
Value.tpp
Variable.h
Variable.tpp
LRAModule.h
LRAModule.tpp
LRAModuleStatistics.h
LRASettings.h	Class to create a settings object for the LRAModule
LRASettings1Instantiation.cpp
LRASettings2Instantiation.cpp
LRASettingsICPInstantiation.cpp
► LVEModule
LVEModule.h	Supports optimization
LVEModule.tpp
LVESettings.h
LVESettings1Instantiation.cpp
LVEStatistics.h
utils.h
► MCBModule
MCBModule.h
MCBModule.tpp
MCBSettings.h
MCBSettings1Instantiation.cpp
► NewCADModule
NewCADModule.h
NewCADModule.tpp
NewCADSettings.h
NewCADSettings_LOLSInstantiation.cpp
NewCADSettings_LOLTAInstantiation.cpp
NewCADSettings_LOLTInstantiation.cpp
NewCADSettings_LOLTSAInstantiation.cpp
NewCADSettings_LOLTSInstantiation.cpp
NewCADSettings_LOSInstantiation.cpp
NewCADSettings_LOTInstantiation.cpp
NewCADSettings_LOTLSAInstantiation.cpp
NewCADSettings_LOTSAInstantiation.cpp
NewCADSettings_LOTSInstantiation.cpp
NewCADSettings_LOTypeInstantiation.cpp
NewCADSettings_PODInstantiation.cpp
NewCADSettings_POLDInstantiation.cpp
NewCADSettings_POlDInstantiation.cpp
NewCADSettings_POPDInstantiation.cpp
NewCADSettings_POSDInstantiation.cpp
NewCADSettingsBrownInstantiation.cpp
NewCADSettingsCollinsInstantiation.cpp
NewCADSettingsEnumerateAllInstantiation.cpp
NewCADSettingsEQ_BDInstantiation.cpp
NewCADSettingsEQ_BInstantiation.cpp
NewCADSettingsEQ_BRDInstantiation.cpp
NewCADSettingsEQ_BRIDInstantiation.cpp
NewCADSettingsEQ_BRIInstantiation.cpp
NewCADSettingsEQ_BRInstantiation.cpp
NewCADSettingsEQ_BSDInstantiation.cpp
NewCADSettingsEQ_BSIDInstantiation.cpp
NewCADSettingsEQ_BSIInstantiation.cpp
NewCADSettingsEQ_BSInstantiation.cpp
NewCADSettingsEQ_RDInstantiation.cpp
NewCADSettingsEQ_RIDInstantiation.cpp
NewCADSettingsEQ_RIInstantiation.cpp
NewCADSettingsEQ_RInstantiation.cpp
NewCADSettingsEQ_SDInstantiation.cpp
NewCADSettingsEQ_SIDInstantiation.cpp
NewCADSettingsEQ_SIInstantiation.cpp
NewCADSettingsEQ_SInstantiation.cpp
NewCADSettingsF1Instantiation.cpp
NewCADSettingsFO1Instantiation.cpp
NewCADSettingsFOSInstantiation.cpp
NewCADSettingsFOVInstantiation.cpp
NewCADSettingsFUInstantiation.cpp
NewCADSettingsFVInstantiation.cpp
NewCADSettingsHongInstantiation.cpp
NewCADSettingsInterleaveInstantiation.cpp
NewCADSettingsLazardInstantiation.cpp
NewCADSettingsMcCallumInstantiation.cpp
NewCADSettingsMcCallumPartialInstantiation.cpp
NewCADSettingsMISBaseInstantiation.cpp
NewCADSettingsMISExactInstantiation.cpp
NewCADSettingsMISGreedyInstantiation.cpp
NewCADSettingsMISGreedyPreInstantiation.cpp
NewCADSettingsMISGreedyWeightedInstantiation.cpp
NewCADSettingsMISHybridInstantiation.cpp
NewCADSettingsMISTrivialInstantiation.cpp
NewCADSettingsNaiveInstantiation.cpp
NewCADSettingsNOInstantiation.cpp
NewCADSettingsNUInstantiation.cpp
NewCADSettingsPPInstantiation.cpp
NewCADSettingsPPRRInstantiation.cpp
NewCADSettingsPPVEInstantiation.cpp
NewCADSettingsPPVERRInstantiation.cpp
NewCADSettingsSOInstantiation.cpp
NewCADSettingsSUInstantiation.cpp
NewCADStatistics.h
► NewCoveringModule
Backend.h
Helper.h
LevelWiseInformation.h
NewCoveringModule.h
NewCoveringModule.tpp
NewCoveringSettings.h
NewCoveringSettings1Instantiation.cpp
NewCoveringSettings2Instantiation.cpp
NewCoveringSettings3Instantiation.cpp
NewCoveringSettings4Instantiation.cpp
NewCoveringStatistics.h
Sampling.h
► NewGBPPModule
NewGBPPModule.h
NewGBPPModule.tpp
NewGBPPSettings.h
NewGBPPSettings1Instantiation.cpp
► NRAILModule
► dto
RationalCapsule.cpp
RationalCapsule.h
VariableCapsule.cpp
VariableCapsule.h
► factory
AxiomFactory.cpp
AxiomFactory.h
LOG.h
MonomialMappingByVariablePool.h
NRAILModule.h
NRAILModule.tpp
NRAILSettings.h
NRAILSettings10Instantiation.cpp
NRAILSettings11Instantiation.cpp
NRAILSettings12Instantiation.cpp
NRAILSettings13Instantiation.cpp
NRAILSettings14Instantiation.cpp
NRAILSettings15Instantiation.cpp
NRAILSettings16Instantiation.cpp
NRAILSettings17Instantiation.cpp
NRAILSettings18Instantiation.cpp
NRAILSettings19Instantiation.cpp
NRAILSettings1Instantiation.cpp
NRAILSettings20Instantiation.cpp
NRAILSettings21Instantiation.cpp
NRAILSettings22Instantiation.cpp
NRAILSettings23Instantiation.cpp
NRAILSettings24Instantiation.cpp
NRAILSettings25Instantiation.cpp
NRAILSettings2Instantiation.cpp
NRAILSettings3Instantiation.cpp
NRAILSettings4Instantiation.cpp
NRAILSettings5Instantiation.cpp
NRAILSettings6Instantiation.cpp
NRAILSettings7Instantiation.cpp
NRAILSettings8Instantiation.cpp
NRAILSettings9Instantiation.cpp
Util.h
► PBGaussModule
PBGaussModule.h	Supports optimization
PBGaussModule.tpp
PBGaussSettings.h
PBGaussSettings1Instantiation.cpp
► PBPPModule
► Encoders
CardinalityEncoder.cpp
CardinalityEncoder.h
ExactlyOneCommanderEncoder.cpp
ExactlyOneCommanderEncoder.h
LongFormulaEncoder.cpp
LongFormulaEncoder.h
MixedSignEncoder.cpp
MixedSignEncoder.h
PseudoBoolEncoder.cpp
PseudoBoolEncoder.h
PseudoBoolNormalizer.cpp
PseudoBoolNormalizer.h
RNSEncoder.cpp
RNSEncoder.h
ShortFormulaEncoder.cpp
ShortFormulaEncoder.h
TotalizerEncoder.cpp
TotalizerEncoder.h
PBPPModule.h	Supports optimization
PBPPModule.tpp
PBPPSettings.h
PBPPSettings1Instantiation.cpp
PBPPSettingsBaseInstantiation.cpp
PBPPSettingsBasicInstantiation.cpp
PBPPSettingsCardinalityOnly05Instantiation.cpp
PBPPSettingsCardinalityOnly05NormalizeInstantiation.cpp
PBPPSettingsCardinalityOnly20Instantiation.cpp
PBPPSettingsCardinalityOnly20NormalizeInstantiation.cpp
PBPPSettingsFull05Instantiation.cpp
PBPPSettingsFull20Instantiation.cpp
PBPPSettingsLIAOnlyInstantiation.cpp
PBPPSettingsLIAOnlyWithNormalizeInstantiation.cpp
PBPPSettingsMaxSMTInstantiation.cpp
PBPPSettingsWithCardConstrInstantiation.cpp
PBPPSettingsWithMixedConstrInstantiation.cpp
PBPPSettingsWithNormalizeInstantiation.cpp
PBPPSettingsWithRNSInstantiation.cpp
PBPPStatistics.h
► PFEModule
PFEModule.h	Removes factors of polynomials from the formula
PFEModule.tpp
PFESettings.h
PFESettings1Instantiation.cpp
► PNFerModule
PNFerModule.cpp
PNFerModule.h
► SATModule
► mcsat
BaseBackend.h
MCSATMixin.h
MCSATMixin.tpp
MCSATSettings.h
MCSATStatistics.h
VarSchedulerMcsat.h
Alg.h
Alloc.h
ClauseChecker.h
Heap.h
IntTypes.h
Map.h
Options.cpp
Options.h
Queue.h
SATModule.h
SATModule.tpp
SATModuleStatistics.h
SATSettings.h	Class to create a settings object for the SATModule
SATSettings1Instantiation.cpp
SATSettings3Instantiation.cpp
SATSettingsMCSATDefaultInstantiation.cpp
SATSettingsMCSATFMICPOCInstantiation.cpp
SATSettingsMCSATFMICPVSNLInstantiation.cpp
SATSettingsMCSATFMICPVSOCInstantiation.cpp
SATSettingsMCSATFMICPVSOCLWH12Instantiation.cpp
SATSettingsMCSATFMICPVSOCNewInstantiation.cpp
SATSettingsMCSATFMICPVSOCNewOCInstantiation.cpp
SATSettingsMCSATFMOCNewInstantiation.cpp
SATSettingsMCSATInstantiation.cpp
SATSettingsMCSATNLInstantiation.cpp
SATSettingsMCSATOCInstantiation.cpp
SATSettingsMCSATOCNewInstantiation.cpp
SATSettingsMCSATVSOCNewInstantiation.cpp
SATSettingsStopAfterUnknownInstantiation.cpp
SolverTypes.h
Sort.h
VarScheduler.h
VarSchedulerForwardDeclarations.h
Vec.h
XAlloc.h
► SplitSOSModule
SplitSOSModule.h	Splits the sum-of-squares (sos) decomposition of all constraints with a sos as left-hand side
SplitSOSModule.tpp
SplitSOSSettings.h
SplitSOSSettings1Instantiation.cpp
► STropModule
STropModule.h
STropModule.tpp
STropModuleStatistics.h
STropSettings.h
STropSettings1Instantiation.cpp
STropSettings2Instantiation.cpp
STropSettings2OutputOnlyInstantiation.cpp
STropSettings3bInstantiation.cpp
STropSettings3bOutputOnlyInstantiation.cpp
STropSettings3Instantiation.cpp
STropSettings3OutputOnlyInstantiation.cpp
Subtropical.h
► SymmetryModule
SymmetryModule.h
SymmetryModule.tpp
SymmetrySettings.h
SymmetrySettings1Instantiation.cpp
► VSModule
Condition.cpp
Condition.h
State.cpp
State.h
Substitute.cpp
Substitute.h
Substitution.cpp
Substitution.h
VSModule.h
VSModule.tpp
VSSettings.h
VSSettings1Instantiation.cpp
VSSettings234Instantiation.cpp
VSStatistics.h
null.cpp
► smtrat-optimization
Optimization.h
smtrat-optimization.cpp
smtrat-optimization.h
► smtrat-qe
► cad
CAD.h
CADElimination.cpp
CADElimination.h
Projection.h
qe.cpp
qe.h
► coverings
► util
to_formula.cpp
to_formula.h
qe.cpp
qe.h
Settings.h
Statistics.h
► fm
eigen_helpers.h
FMQEStatistics.h
FourierMotzkinQE.cpp
FourierMotzkinQE.h
qe.cpp
qe.h
► fmplex
FMplexQE.cpp
FMplexQE.h
FMplexQEStatistics.h
Node.h
qe.cpp
qe.h
► util
EqualitySubstitution.h
Matrix.h
quantifier_splitting.h
VariableIndex.h
QEQuery.h
smtrat-qe.cpp
smtrat-qe.h
► smtrat-solver
Manager.cpp
Manager.h
Module.cpp
Module.h
ModuleInput.cpp
ModuleInput.h
PModule.cpp
PModule.h	All preprocessing modules shall derive from this module, that is modules, which simplify their received formula to an equisatisfiable formula being passed to their backends
smtrat-solver.h
StrategyGraph.h
ThreadPool.cpp
ThreadPool.h
► smtrat-strategies
► strategies
► CoveringNG
Default.h
GBDefault.h
PPBooleanExploration.h
PPBooleanExplorationOnlyBool.h
PPBooleanExplorationWithBool.h
PPBooleanOff.h
PPBooleanPartialPropagationSotd.h
PPBooleanPartialPropagationTdeg.h
PPBooleanPropagation.h
PPDefault.h
PPFilterBoundsOnly.h
PPFilterBoundsOnlyComplete.h
PPFilterNoop.h
PPGBDefault.h
PPImplicantsLevelSize.h
PPImplicantsLevelSotd.h
PPImplicantsPickeringTotal.h
PPImplicantsSizeOnly.h
PPImplicantsSotd.h
PPImplicantsSotdReverse.h
PPImplicantsTdeg.h
PPImplicantsVars.h
PPImplicantsVarsVarorderSplitting.h
PPInprocessingOn.h
PPSTropDefault.h
PPVarorderPickering.h
PPVarorderUnivariate.h
► Filter
BCAll.h
BCBc.h
BCBoundsOnly.h
BCDeg10.h
BCDeg2.h
BCDeg5.h
BCIndep.h
BCIntersect.h
BCIrred.h
BCIrredIndep.h
BCNoop.h
BCRational.h
LDBBoundsOnly.h
LDBNoop.h
► MCSAT
FMICPOC.h
FMICPVSNL.h
FMICPVSOC.h
FMICPVSOCLWH11.h
FMICPVSOCLWH12.h
FMICPVSOCLWH13.h
FMICPVSOCNew.h
FMICPVSOCNewOC.h
FMICPVSOCNNASC.h
FMICPVSOCNNDSC.h
FMICPVSOCPARALLEL.h
FMNL.h
FMOCNew.h
FMVSNL.h
FMVSOC.h
ICPNL.h
NL.h
OC.h
OCLWH11.h
OCLWH12.h
OCLWH13.h
OCLWH21.h
OCLWH22.h
OCLWH23.h
OCLWH31.h
OCLWH32.h
OCLWH33.h
OCNew.cpp
OCNew.h
OCNewBC.h
OCNewLDB.h
OCNewLDBCovering.h
OCNewLDBCoveringCache.h
OCNewLDBCoveringCacheGlobal.h
OCNN.h
OCNNASC.h
OCNNDSC.h
OCPARALLEL.h
PPDefault.h
PPNL.h
PPOC.h
PPOCNew.h
VSNL.h
VSOCNew.h
► MIS
Exact.h
Greedy.h
GreedyExact.h
GreedyPre.h
GreedyWeighted.h
Hybrid.h
Trivial.h
► NewCAD
Brown.h
Collins.h
FOS.h
FU.h
FU_SC.h
FU_SI.h
FU_SInf.h
FU_SL.h
FU_SR.h
FU_SZ.h
Hong.h
LOLS.h
LOLT.h
LOLTA.h
LOLTS.h
LOLTSA.h
LOS.h
LOT.h
LOTLSA.h
LOTS.h
LOTSA.h
McCallum.h
McCallumPartial.h
Naive.h
NO.h
NU.h
Only.h
POD.h
POLD.h
POPD.h
POSD.h
PP.h
PPRR.h
PPVE.h
PPVERR.h
SAT.h
SO.h
SU.h
► NewCADEQ
B.h
BD.h
BR.h
BRD.h
BRI.h
BRID.h
BS.h
BSD.h
BSI.h
BSID.h
R.h
RD.h
RI.h
RID.h
S.h
SD.h
SI.h
SID.h
► NewCovering
Backtracking.h
FilterBoundsOnly.h
Incomplete.h
Incremental.h
IncrementalBacktracking.h
PPComplete.h
PPFilterBoundsOnly.h
PPFilterBoundsOnlyComplete.h
PPIncomplete.h
Vanilla.h
► NRARefinement
Solver.h
Solver1.h
Solver10.h
Solver11.h
Solver12.h
Solver13.h
Solver14.h
Solver15.h
Solver16.h
Solver17.h
Solver18.h
Solver19.h
Solver2.h
Solver20.h
Solver21.h
Solver22.h
Solver23.h
Solver24.h
Solver25.h
Solver3.h
Solver4.h
Solver5.h
Solver6.h
Solver7.h
Solver8.h
Solver9.h
► PseudoBool
PBPPStrategyGroe_Norm_PB_LIA.h
PBPPStrategyGroe_PB_LIA.h
PBPPStrategyLIA.h
PBPPStrategyLIA_ICP.h
PBPPStrategyLIA_VS.h
PBPPStrategyNorm_LIA.h
PBPPStrategyNorm_LIA_ICP.h
PBPPStrategyNorm_LIA_VS.h
PBPPStrategyNorm_PB_LIA.h
PBPPStrategyPB_LIA.h
► STrop
BackendsOnly.h
CADBackendsOnly.h
Formula.h
FormulaAlt.h
FormulaAltOutputOnly.h
FormulaAltWCADBackends.h
FormulaAltWCADBackendsFull.h
FormulaOutputOnly.h
FormulaWBackends.h
FormulaWBackendsFull.h
FormulaWCADBackends.h
FormulaWCADBackendsFull.h
FormulaWMCSAT.h
Incremental.h
IncrementalWBackends.h
IncrementalWCADBackends.h
MCSATOnly.h
TransformationEQ.h
TransformationEQOutputOnly.h
TransformationEQWBackends.h
TransformationEQWCADBackends.h
AllModulesStrategy.h
BVPreprocessing.h
BVSolver.h
CSplitFull.h
CSplitOnly.h
Default.h
DefaultTwo.h
LIASolver.h
LRASolver.h
MAXSATBackendStrategy.h
MAXSMTPBPPStrategy.h
NIABB.h
NIABlast.h
NIASolver.h
NRA_CAD.h
NRA_ICPVSCAD.h
NRA_LRAVSCAD.h
NRA_VSCAD.h
NRASolver.h
NRASolverCov.h
OnlyCAD.h
OnlyGB.h
OnlySAT.h
OnlySATPP.h
OnlyVS.h
OptimizationPreprocessing.h
OptimizationStrategy.h
PBPPStrategy.h
PBPPStrategy2.h
PBPPStrategyBasic.h
PBPPStrategyGauss.h
PBPPStrategyGroebner.h
PBPPStrategyLIAOnly.h
PBPPStrategyRNS.h
PBPPStrategyWithCardConstr.h
PBPPStrategyWithMixedConstr.h
PBPreprocessing.h
PreprocessingOne.h
PreprocessingTwo.h
RatIntBlast.h
SMTCOMP.h
config.h
smtrat-strategies.cpp
smtrat-strategies.h
► smtrat-unsat-cores
smtrat-unsat-cores.cpp
smtrat-unsat-cores.h
UnsatCore.h
UnsatCore_ModelExclusion.h
► smtrat-variablebounds
smtrat-variablebounds.cpp
smtrat-variablebounds.h
VariableBounds.h
VariableBounds.tpp