STropSettings.h File Reference

#include "Subtropical.h"

Include dependency graph for STropSettings.h:

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

Go to the source code of this file.

Data Structures
struct	smtrat::STropSettings1
	Take conjunctions incrementally, construct linear formulas for LRA solver. More...
struct	smtrat::STropSettings2
struct	smtrat::STropSettings3
	Transform to NNF then replace each constraint with its linear formula (equations become FALSE). Then let LRA solver solve. More...
struct	smtrat::STropSettings3b
	Transform to NNF then replace each constraint with its linear formula (equations become FALSE). Then let LRA solver solve. More...
struct	smtrat::STropSettings2OutputOnly
struct	smtrat::STropSettings3OutputOnly
struct	smtrat::STropSettings3bOutputOnly

Namespaces
	smtrat
	Class to create the formulas for axioms.

Enumerations
enum class	smtrat::Mode { smtrat::INCREMENTAL_CONSTRAINTS , smtrat::TRANSFORM_EQUATION , smtrat::TRANSFORM_FORMULA , smtrat::TRANSFORM_FORMULA_ALT }

Detailed Description

Author

Ömer Sali oemer.nosp@m..sal.nosp@m.i@rwt.nosp@m.h-aa.nosp@m.chen..nosp@m.de

Version

2022-04-19 Created on 2017-09-13.

Definition in file STropSettings.h.