dlinear/Logic_8h_source.html

#pragma once


#include <ostream>

#include <string>


namespace dlinear {


enum class Logic {

  QF_NRA,

  QF_NRA_ODE,

  QF_LRA,

  QF_RDL,

  QF_LIA,

  LRA,

};


Logic parseLogic(const std::string &s);

std::ostream &operator<<(std::ostream &os, const Logic &logic);


}  // namespace dlinear


#ifdef DLINEAR_INCLUDE_FMT


#include "dlinear/util/logging.h"


OSTREAM_FORMATTER(dlinear::Logic)


#endif

dlinear
Global namespace for the dlinear library.

dlinear::Logic
Logic
The SMT-LIB logic the SMT2 file is using.
Definition Logic.h:17

dlinear::Logic::QF_RDL
@ QF_RDL
Quantifier free real difference logic.

dlinear::Logic::QF_NRA
@ QF_NRA
Quantifier free non-linear real arithmetic.

dlinear::Logic::QF_LRA
@ QF_LRA
Quantifier free linear real arithmetic. It is the only one dlinear supports.

dlinear::Logic::QF_LIA
@ QF_LIA
Quantifier free linear integer arithmetic.

dlinear::Logic::LRA
@ LRA
Linear real arithmetic.

dlinear::Logic::QF_NRA_ODE
@ QF_NRA_ODE
Quantifier free non-linear real arithmetic with ODEs.

dlinear::parseLogic
Logic parseLogic(const std::string &s)
Parse the logic from a string.
Definition Logic.cpp:12