Modes 

namespace modes 

Functions

enum ENUM (BlockModelsMode)

Mode for blocking models.

Specifies how models are blocked in Solver::blockModel and Solver::blockModelValues .

std :: ostream & operator << ( std :: ostream & out , BlockModelsMode mode ) 

Serialize a BlockModelsMode to given stream.

Parameters :

• out – The output stream

• mode – The mode.

Returns :

The output stream

enum ENUM (LearnedLitType)

Types of learned literals.

Specifies categories of literals learned for the method Solver::getLearnedLiterals .

Note that a literal may conceptually belong to multiple categories. We classify literals based on the first criteria in this list that they meet.

std :: ostream & operator << ( std :: ostream & out , LearnedLitType type ) 

Serialize a LearnedLitType to given stream.

Parameters :

• out – The output stream

• type – The learned literal type.

Returns :

The output stream

enum ENUM (ProofComponent)

Components to include in a proof.

std :: ostream & operator << ( std :: ostream & out , ProofComponent pc ) 

Serialize a ProofComponent to given stream.

Parameters :

• out – The output stream

• pc – The proof component.

Returns :

The output stream

enum ENUM (FindSynthTarget)

Find synthesis targets, used as an argument to Solver::findSynth . These specify various kinds of terms that can be found by this method.

std :: ostream & operator << ( std :: ostream & out , FindSynthTarget target ) 

Serialize a FindSynthTarget to given stream.

Parameters :

• out – The output stream

• targetThe – synthesis find target.

Returns :

The output stream