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
16
namespace
mcrl2
17
{
18
namespace
smt
19
{
20
21
enum
answer
22
{
23
UNSAT
= 0,
24
UNKNOWN
= 1,
25
SAT
= 2
26
};
27
28
inline
29
std::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
mcrl2::smt::operator<<
std::ostream & operator<<(std::ostream &out, const answer &a)
Definition
answer.h:29
mcrl2::smt::answer
answer
Definition
answer.h:22
mcrl2::smt::SAT
@ SAT
Definition
answer.h:25
mcrl2::smt::UNSAT
@ UNSAT
Definition
answer.h:23
mcrl2::smt::UNKNOWN
@ UNKNOWN
Definition
answer.h:24
mcrl2
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition
indexed_set.h:72
smt
include
mcrl2
smt
answer.h
Generated by
1.9.7