mCRL2
Loading...
Searching...
No Matches
answer.h
Go to the documentation of this file.
1// Author(s): Thomas Neele
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
10
11#ifndef MCRL2_SMT_ANSWER_H
12#define MCRL2_SMT_ANSWER_H
13
14#include <iostream>
15
16namespace mcrl2
17{
18namespace smt
19{
20
22{
23 UNSAT = 0,
25 SAT = 2
26};
27
28inline
29std::ostream& operator<<(std::ostream& out, const answer& a)
30{
31 switch(a)
32 {
33 case smt::answer::SAT: return out << "sat";
34 case smt::answer::UNSAT: return out << "unsat";
35 case smt::answer::UNKNOWN: return out << "unknown";
36 default: std::abort();
37 }
38}
39
40} // namespace smt
41} // namespace mcrl2
42
43#endif // MCRL2_SMT_ANSWER_H
std::ostream & operator<<(std::ostream &out, const answer &a)
Definition answer.h:29
@ UNKNOWN
Definition answer.h:24
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72