mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

Minor fix in sat::literal (#5293)

Browse source
This commit is contained in:
Jakob Rath 2021-05-21 22:50:01 +02:00 committed by GitHub
parent ce1a48486e
commit 089015b250
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/util/sat_literal.h
View file

@ -17,6 +17,7 @@ Author:
#pragma once
#include "util/lbool.h"
#include "util/approx_set.h"
#include "util/vector.h"
#include "util/uint_set.h"
@ -93,6 +94,8 @@ namespace sat {
inline bool operator==(literal const & l1, literal const & l2) { return l1.m_val == l2.m_val; }
inline bool operator!=(literal const & l1, literal const & l2) { return l1.m_val != l2.m_val; }
inline std::ostream & operator<<(std::ostream & out, sat::literal l) { if (l == sat::null_literal) out << "null"; else out << (l.sign() ? "-" : "") << l.var(); return out; }
typedef svector<literal> literal_vector;
typedef std::pair<literal, literal> literal_pair;
@ -160,7 +163,7 @@ namespace sat {
struct dimacs_lit {
literal m_lit;
dimacs_lit(literal l):m_lit(l) {}
explicit dimacs_lit(literal l):m_lit(l) {}
};
inline std::ostream & operator<<(std::ostream & out, dimacs_lit const & dl) {
@ -189,6 +192,3 @@ namespace sat {
}
};
inline std::ostream & operator<<(std::ostream & out, sat::literal l) { if (l == sat::null_literal) out << "null"; else out << (l.sign() ? "-" : "") << l.var(); return out; }