dlinear  0.0.1
Delta-complete SMT solver for linear programming
Loading...
Searching...
No Matches
SatResult.cpp
1
6#include "SatResult.h"
7
8#include "dlinear/util/exception.h"
9
10namespace dlinear {
11
12std::ostream &operator<<(std::ostream &os, const SatResult &logic) {
13 switch (logic) {
14 case SatResult::SAT_NO_RESULT:
15 return os << "no-result";
16 case SatResult::SAT_UNSOLVED:
17 return os << "unsolved";
18 case SatResult::SAT_UNSATISFIABLE:
19 return os << "unsat";
20 case SatResult::SAT_SATISFIABLE:
21 return os << "sat";
22 case SatResult::SAT_DELTA_SATISFIABLE:
23 return os << "delta-sat";
24 default:
25 DLINEAR_UNREACHABLE();
26 }
27}
28
29} // namespace dlinear
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.