forked from vprover/vampire
-
Notifications
You must be signed in to change notification settings - Fork 0
/
SATLiteral.cpp
57 lines (44 loc) · 1.11 KB
/
SATLiteral.cpp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
/*
* File SATLiteral.cpp.
*
* This file is part of the source code of the software program
* Vampire. It is protected by applicable
* copyright laws.
*
* This source code is distributed under the licence found here
* https://vprover.github.io/license.html
* and in the source directory
*
* In summary, you are allowed to use Vampire for non-commercial
* purposes but not allowed to distribute, modify, copy, create derivatives,
* or use in competitions.
* For other uses of Vampire please contact developers for a different
* licence, which we will make an effort to provide.
*/
/**
* @file SATLiteral.cpp
* Implements class SATLiteral.
*/
#include <ostream>
#include "Shell/Options.hpp"
#include "Lib/Int.hpp"
#include "Kernel/Term.hpp"
#include "SATLiteral.hpp"
namespace SAT
{
using namespace std;
using namespace Lib;
using namespace Shell;
vstring SATLiteral::toString() const
{
if(isPositive()) {
return Int::toString(var());
} else {
return "~"+Int::toString(var());
}
}
std::ostream& operator<< (std::ostream& out, const SAT::SATLiteral& lit )
{
return out<<lit.toString();
}
};