dlinear/SatResult_8h_source.html

#pragma once


#include <ostream>


namespace dlinear {


enum class SatResult {

  SAT_NO_RESULT,

  SAT_UNSOLVED,

  SAT_UNSATISFIABLE,

  SAT_SATISFIABLE,

  SAT_DELTA_SATISFIABLE,

};


std::ostream &operator<<(std::ostream &os, const SatResult &sat_result);


}  // namespace dlinear


#ifdef DLINEAR_INCLUDE_FMT


#include "dlinear/util/logging.h"


OSTREAM_FORMATTER(dlinear::SatResult)


#endif

dlinear
Global namespace for the dlinear library.

dlinear::SatResult
SatResult
Result of running the theory solver over the literals decided by the SAT solver.
Definition SatResult.h:17

dlinear::SatResult::SAT_NO_RESULT
@ SAT_NO_RESULT
No result has been obtained yet.

dlinear::SatResult::SAT_SATISFIABLE
@ SAT_SATISFIABLE
The problem is satisfiable.

dlinear::SatResult::SAT_UNSATISFIABLE
@ SAT_UNSATISFIABLE
The problem is unsatisfiable.

dlinear::SatResult::SAT_UNSOLVED
@ SAT_UNSOLVED
The problem has not been solved. An error may have occurred.

dlinear::SatResult::SAT_DELTA_SATISFIABLE
@ SAT_DELTA_SATISFIABLE
The problem is satisfiable, but with a delta >= 0.