From 03d2c5f3d0868526088cde0a163c542e5dae0eda Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 May 2021 12:58:27 -0700 Subject: [PATCH] consolidate literals --- src/sat/sat_types.h | 162 +------------------------------ src/smt/smt_clause.cpp | 4 +- src/smt/smt_context.cpp | 4 +- src/smt/smt_context.h | 2 +- src/smt/smt_context_pp.cpp | 4 +- src/smt/smt_literal.cpp | 55 ++++++----- src/smt/smt_literal.h | 87 +++-------------- src/test/finder.cpp | 110 ++++++++++----------- src/util/sat_literal.h | 194 +++++++++++++++++++++++++++++++++++++ 9 files changed, 299 insertions(+), 323 deletions(-) create mode 100644 src/util/sat_literal.h diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 54e2b0e5e..57300a705 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -27,6 +27,7 @@ Revision History: #include "util/uint_set.h" #include "util/stopwatch.h" #include "util/symbol.h" +#include "util/sat_literal.h" class params_ref; class reslimit; @@ -35,89 +36,11 @@ class statistics; namespace sat { #define SAT_VB_LVL 10 - // TODO: there is some duplication in the sat and smt namespaces. - // The sat namespace should be the base. - // I should cleanup the smt namespace later. - - /** - \brief A boolean variable is just an integer. - */ - typedef unsigned bool_var; - - typedef svector bool_var_vector; - - const bool_var null_bool_var = UINT_MAX >> 1; - - /** - \brief The literal b is represented by the value 2*b, and - the literal (not b) by the value 2*b + 1 - */ - class literal { - unsigned m_val; - explicit literal(unsigned v):m_val(v) {} - public: - literal():m_val(null_bool_var << 1) { - SASSERT(var() == null_bool_var && !sign()); - } - - literal(bool_var v, bool _sign): - m_val((v << 1) + static_cast(_sign)) { - SASSERT(var() == v); - SASSERT(sign() == _sign); - } - - bool_var var() const { - return m_val >> 1; - } - - bool sign() const { - return m_val & 1; - } - - literal unsign() const { - return literal(m_val & ~1); - } - - unsigned index() const { - return m_val; - } - - void neg() { - m_val = m_val ^ 1; - } - - friend literal operator~(literal l) { - return literal(l.m_val ^ 1); - } - - unsigned to_uint() const { return m_val; } - - unsigned hash() const { return to_uint(); } - - friend literal to_literal(unsigned x); - friend bool operator<(literal const & l1, literal const & l2); - friend bool operator==(literal const & l1, literal const & l2); - friend bool operator!=(literal const & l1, literal const & l2); - }; - - const literal null_literal; - struct literal_hash : obj_hash {}; - - inline literal to_literal(unsigned x) { return literal(x); } - 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 bool operator!=(literal const & l1, literal const & l2) { return l1.m_val != l2.m_val; } - - inline std::ostream & operator<<(std::ostream & out, literal l) { if (l == null_literal) out << "null"; else out << (l.sign() ? "-" : "") << l.var(); return out; } - - typedef svector literal_vector; - typedef std::pair literal_pair; typedef size_t clause_offset; typedef size_t ext_constraint_idx; typedef size_t ext_justification_idx; - struct literal2unsigned { unsigned operator()(literal l) const { return l.to_uint(); } }; typedef approx_set_tpl literal_approx_set; @@ -141,7 +64,6 @@ namespace sat { typedef svector model; - inline void negate(literal_vector& ls) { for (unsigned i = 0; i < ls.size(); ++i) ls[i].neg(); } inline lbool value_at(bool_var v, model const & m) { return m[v]; } inline lbool value_at(literal l, model const & m) { lbool r = value_at(l.var(), m); return l.sign() ? ~r : r; } @@ -155,88 +77,6 @@ namespace sat { return out; } - typedef tracked_uint_set uint_set; - - typedef uint_set bool_var_set; - - class literal_set { - uint_set m_set; - public: - literal_set(literal_vector const& v) { - for (unsigned i = 0; i < v.size(); ++i) insert(v[i]); - } - literal_set() {} - literal_vector to_vector() const { - literal_vector result; - for (literal lit : *this) result.push_back(lit); - return result; - } - literal_set& operator=(literal_vector const& v) { - reset(); - for (unsigned i = 0; i < v.size(); ++i) insert(v[i]); - return *this; - } - - void insert(literal l) { m_set.insert(l.index()); } - void remove(literal l) { m_set.remove(l.index()); } - literal pop() { return to_literal(m_set.erase()); } - bool contains(literal l) const { return m_set.contains(l.index()); } - bool empty() const { return m_set.empty(); } - unsigned size() const { return m_set.size(); } - void reset() { m_set.reset(); } - void finalize() { m_set.finalize(); } - class iterator { - uint_set::iterator m_it; - public: - iterator(uint_set::iterator it):m_it(it) {} - literal operator*() const { return to_literal(*m_it); } - iterator& operator++() { ++m_it; return *this; } - iterator operator++(int) { iterator tmp = *this; ++m_it; return tmp; } - bool operator==(iterator const& it) const { return m_it == it.m_it; } - bool operator!=(iterator const& it) const { return m_it != it.m_it; } - }; - iterator begin() const { return iterator(m_set.begin()); } - iterator end() const { return iterator(m_set.end()); } - literal_set& operator&=(literal_set const& other) { - m_set &= other.m_set; - return *this; - } - literal_set& operator|=(literal_set const& other) { - m_set |= other.m_set; - return *this; - } - }; - - struct dimacs_lit { - literal m_lit; - dimacs_lit(literal l):m_lit(l) {} - }; - - inline std::ostream & operator<<(std::ostream & out, dimacs_lit const & dl) { - literal l = dl.m_lit; - if (l.sign()) out << "-" << (l.var() + 1); - else out << (l.var() + 1); - return out; - } - - struct mk_lits_pp { - unsigned m_num; - literal const * m_lits; - mk_lits_pp(unsigned num, literal const * ls):m_num(num), m_lits(ls) {} - }; - - inline std::ostream & operator<<(std::ostream & out, mk_lits_pp const & ls) { - for (unsigned i = 0; i < ls.m_num; i++) { - if (i > 0) out << " "; - out << ls.m_lits[i]; - } - return out; - } - - inline std::ostream & operator<<(std::ostream & out, literal_vector const & ls) { - return out << mk_lits_pp(ls.size(), ls.data()); - } - class i_local_search { public: virtual ~i_local_search() {} diff --git a/src/smt/smt_clause.cpp b/src/smt/smt_clause.cpp index 291adbecf..654ed161f 100644 --- a/src/smt/smt_clause.cpp +++ b/src/smt/smt_clause.cpp @@ -101,7 +101,7 @@ namespace smt { out << "(clause"; for (unsigned i = 0; i < m_num_literals; i++) { out << " "; - m_lits[i].display(out, m, bool_var2expr_map); + smt::display(out, m_lits[i], m, bool_var2expr_map); } return out << ")"; } @@ -110,7 +110,7 @@ namespace smt { out << "(clause"; for (unsigned i = 0; i < m_num_literals; i++) { out << " "; - m_lits[i].display_compact(out, bool_var2expr_map); + smt::display_compact(out, m_lits[i], bool_var2expr_map); } return out << ")"; } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 9c45df153..d16e3a051 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3081,7 +3081,7 @@ namespace smt { literal l2 = *set_it; if (l2 != l) { b_justification js(l); - TRACE("theory_case_split", tout << "case split literal "; l2.display(tout, m, m_bool_var2expr.data()); tout << std::endl;); + TRACE("theory_case_split", tout << "case split literal "; smt::display(tout, l2, m, m_bool_var2expr.data()); tout << std::endl;); if (l2 == true_literal || l2 == false_literal || l2 == null_literal) continue; assign(~l2, js); if (inconsistent()) { @@ -4188,7 +4188,7 @@ namespace smt { for (unsigned i = 0; i < num_lits; i++) { display_literal(tout, v[i]); tout << "\n"; - v[i].display(tout, m, m_bool_var2expr.data()); + smt::display(tout, v[i], m, m_bool_var2expr.data()); tout << "\n\n"; } tout << "\n";); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 163d205f8..20d177955 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1357,7 +1357,7 @@ namespace smt { std::ostream& display_literal(std::ostream & out, literal l) const; - std::ostream& display_detailed_literal(std::ostream & out, literal l) const { l.display(out, m, m_bool_var2expr.data()); return out; } + std::ostream& display_detailed_literal(std::ostream & out, literal l) const { return smt::display(out, l, m, m_bool_var2expr.data()); } void display_literal_info(std::ostream & out, literal l) const; diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 4c3fb18e0..ed1dae13b 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -89,7 +89,7 @@ namespace smt { } std::ostream& context::display_literal(std::ostream & out, literal l) const { - l.display_compact(out, m_bool_var2expr.data()); return out; + smt::display_compact(out, l, m_bool_var2expr.data()); return out; } std::ostream& context::display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const { @@ -120,7 +120,7 @@ namespace smt { } void context::display_literal_info(std::ostream & out, literal l) const { - l.display_compact(out, m_bool_var2expr.data()); + smt::display_compact(out, l, m_bool_var2expr.data()); display_literal_smt2(out, l); out << "relevant: " << is_relevant(bool_var2expr(l.var())) << ", val: " << get_assignment(l) << "\n"; } diff --git a/src/smt/smt_literal.cpp b/src/smt/smt_literal.cpp index 55592d9ab..f654f684d 100644 --- a/src/smt/smt_literal.cpp +++ b/src/smt/smt_literal.cpp @@ -22,41 +22,44 @@ Revision History: namespace smt { - void literal::display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const { - if (*this == true_literal) + std::ostream& display(std::ostream & out, literal lit, ast_manager & m, expr * const * bool_var2expr_map) { + if (lit == true_literal) out << "true"; - else if (*this == false_literal) + else if (lit == false_literal) out << "false"; - else if (*this == null_literal) + else if (lit == null_literal) out << "null"; - else if (sign()) - out << "(not " << mk_bounded_pp(bool_var2expr_map[var()], m, 3) << ")"; + else if (lit.sign()) + out << "(not " << mk_bounded_pp(bool_var2expr_map[lit.var()], m, 3) << ")"; else - out << mk_bounded_pp(bool_var2expr_map[var()], m, 3); + out << mk_bounded_pp(bool_var2expr_map[lit.var()], m, 3); + return out; } - void literal::display_smt2(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const { - if (*this == true_literal) + std::ostream& display_smt2(std::ostream & out, literal lit, ast_manager & m, expr * const * bool_var2expr_map) { + if (lit == true_literal) out << "true"; - else if (*this == false_literal) + else if (lit == false_literal) out << "false"; - else if (*this == null_literal) + else if (lit == null_literal) out << "null"; - else if (sign()) - out << "(not " << mk_pp(bool_var2expr_map[var()], m, 3) << ")"; + else if (lit.sign()) + out << "(not " << mk_pp(bool_var2expr_map[lit.var()], m, 3) << ")"; else - out << mk_pp(bool_var2expr_map[var()], m, 3); + out << mk_pp(bool_var2expr_map[lit.var()], m, 3); + return out; } - void literal::display_compact(std::ostream & out, expr * const * bool_var2expr_map) const { - if (*this == true_literal) + std::ostream& display_compact(std::ostream & out, literal lit, expr * const * bool_var2expr_map) { + if (lit == true_literal) out << "true"; - else if (*this == false_literal) + else if (lit == false_literal) out << "false"; - else if (sign()) - out << "(not #" << bool_var2expr_map[var()]->get_id() << ")"; + else if (lit.sign()) + out << "(not #" << bool_var2expr_map[lit.var()]->get_id() << ")"; else - out << "#" << bool_var2expr_map[var()]->get_id(); + out << "#" << bool_var2expr_map[lit.var()]->get_id(); + return out; } std::ostream & operator<<(std::ostream & out, literal l) { @@ -72,24 +75,26 @@ namespace smt { } std::ostream & operator<<(std::ostream & out, const literal_vector & v) { - display(out, v.begin(), v.end()); + ::display(out, v.begin(), v.end()); return out; } - void display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map) { + std::ostream& display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map) { for (unsigned i = 0; i < num_lits; i++) { if (i > 0) out << " "; - lits[i].display_compact(out, bool_var2expr_map); + display_compact(out, lits[i], bool_var2expr_map); } + return out; } - void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep) { + std::ostream& display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep) { for (unsigned i = 0; i < num_lits; i++) { if (i > 0) out << sep; - lits[i].display(out, m, bool_var2expr_map); + display(out, lits[i], m, bool_var2expr_map); } + return out; } /** diff --git a/src/smt/smt_literal.h b/src/smt/smt_literal.h index 863f4f13c..17ed9c6c4 100644 --- a/src/smt/smt_literal.h +++ b/src/smt/smt_literal.h @@ -21,90 +21,30 @@ Revision History: #include "ast/ast.h" #include "smt/smt_types.h" #include "util/approx_set.h" +#include "util/sat_literal.h" namespace smt { - /** - \brief The literal b is represented by the value 2*b, and - the literal (not b) by the value 2*b + 1 - - */ - class literal { - int m_val; - - public: - literal():m_val(-2) { - SASSERT(var() == null_bool_var && !sign()); - } - - explicit literal(bool_var v, bool sign = false): - m_val((v << 1) + static_cast(sign)) { - } - - bool_var var() const { - return m_val >> 1; - } - - bool sign() const { - return m_val & 1; - } - - int index() const { - return m_val; - } - - void neg() { - m_val = m_val ^ 1; - } - - friend literal operator~(literal l); - - friend literal to_literal(int x); - void display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const; + typedef sat::literal literal; + + inline literal to_literal(int x) { return sat::to_literal(x); } - void display_smt2(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const; - - void display_compact(std::ostream & out, expr * const * bool_var2expr_map) const; - - unsigned hash() const { return m_val; } - }; - - inline bool operator==(literal l1, literal l2) { - return l1.index() == l2.index(); - } - - inline bool operator!=(literal l1, literal l2) { - return l1.index() != l2.index(); - } - - inline bool operator<(literal l1, literal l2) { - return l1.index() < l2.index(); - } - - inline literal operator~(literal l) { - literal r; - r.m_val = l.m_val ^ 1; - return r; - } - - inline literal to_literal(int x) { - literal l; - l.m_val = x; - return l; - } - const literal null_literal; const literal true_literal(true_bool_var, false); const literal false_literal(true_bool_var, true); typedef svector literal_vector; typedef sbuffer literal_buffer; - std::ostream & operator<<(std::ostream & out, literal l); - std::ostream & operator<<(std::ostream & out, const literal_vector & v); - void display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map); + std::ostream& display(std::ostream & out, literal lit, ast_manager & m, expr * const * bool_var2expr_map); + + std::ostream& display_smt2(std::ostream & out, literal lit, ast_manager & m, expr * const * bool_var2expr_map); + + std::ostream& display_compact(std::ostream & out, literal lit, expr * const * bool_var2expr_map); - void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep = "\n"); + std::ostream& display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map); + + std::ostream& display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep = "\n"); template void neg_literals(unsigned num_lits, literal const * lits, T & result) { @@ -112,9 +52,6 @@ namespace smt { result.push_back(~lits[i]); } - struct literal2unsigned { unsigned operator()(literal l) const { return l.index(); } }; - - typedef approx_set_tpl literal_approx_set; bool backward_subsumption(unsigned num_lits1, literal const * lits1, unsigned num_lits2, literal const * lits2); }; diff --git a/src/test/finder.cpp b/src/test/finder.cpp index 488384fa3..c34a16d40 100644 --- a/src/test/finder.cpp +++ b/src/test/finder.cpp @@ -13,7 +13,7 @@ static void _init_solver(sat::solver& s) s.mk_var(); } -static void _mk_clause4(sat::solver& s, sat::literal w, sat::literal x, sat::literal y, sat::literal z) +static void _mk_clause4(sat::solver& s, sat::literal const & w, sat::literal const& x, sat::literal const& y, sat::literal const& z) { sat::literal lits[] = {w, x, y, z}; s.mk_clause(4, lits); @@ -41,10 +41,10 @@ static void tst_single_mux() { sat::solver s({}, r); _init_solver(s); - s.mk_clause({ 0, true }, { 1, true }, { 3, false }); - s.mk_clause({ 0, true }, { 1, false }, { 3, true }); - s.mk_clause({ 0, false }, { 2, true }, { 3, false }); - s.mk_clause({ 0, false }, { 2, false }, { 3, true }); + s.mk_clause(sat::literal(0, true), sat::literal(1, true), sat::literal(3, false)); + s.mk_clause(sat::literal(0, true), sat::literal(1, false), sat::literal(3, true)); + s.mk_clause(sat::literal(0, false), sat::literal(2, true), sat::literal(3, false)); + s.mk_clause(sat::literal(0, false), sat::literal(2, false), sat::literal(3, true)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_mux), "mux", 7, 0, 3, 5); } @@ -54,12 +54,12 @@ static void tst_single_maj() { sat::solver s({}, r); _init_solver(s); - s.mk_clause({ 0, false }, { 1, false }, { 3, true }); - s.mk_clause({ 0, false }, { 2, false }, { 3, true }); - s.mk_clause({ 1, false }, { 2, false }, { 3, true }); - s.mk_clause({ 0, true }, { 1, true }, { 3, false }); - s.mk_clause({ 0, true }, { 2, true }, { 3, false }); - s.mk_clause({ 1, true }, { 2, true }, { 3, false }); + s.mk_clause(sat::literal(0, false), sat::literal(1, false), sat::literal(3, true)); + s.mk_clause(sat::literal(0, false), sat::literal(2, false), sat::literal(3, true)); + s.mk_clause(sat::literal(1, false), sat::literal(2, false), sat::literal(3, true)); + s.mk_clause(sat::literal(0, true), sat::literal(1, true), sat::literal(3, false)); + s.mk_clause(sat::literal(0, true), sat::literal(2, true), sat::literal(3, false)); + s.mk_clause(sat::literal(1, true), sat::literal(2, true), sat::literal(3, false)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_maj), "maj", 6, 0, 2, 4); } @@ -69,10 +69,10 @@ static void tst_single_orand() { sat::solver s({}, r); _init_solver(s); - s.mk_clause({0, false}, {3, true}); - s.mk_clause({1, false}, {2, false}, {3, true}); - s.mk_clause({0, true}, {1, true}, {3, false}); - s.mk_clause({0, true}, {2, true}, {3, false}); + s.mk_clause(sat::literal(0, false), sat::literal(3, true)); + s.mk_clause(sat::literal(1, false), sat::literal(2, false), sat::literal(3, true)); + s.mk_clause(sat::literal(0, true), sat::literal(1, true), sat::literal(3, false)); + s.mk_clause(sat::literal(0, true), sat::literal(2, true), sat::literal(3, false)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_orand), "orand", 6, 0, 2, 4); } @@ -82,11 +82,11 @@ static void tst_single_and() { sat::solver s({}, r); _init_solver(s); - sat::literal ls1[] = {{0, true}, {1, true}, {2, true}, {3, false}}; + sat::literal ls1[] = {sat::literal(0, true), sat::literal(1, true), sat::literal(2, true), sat::literal(3, false)}; s.mk_clause(4, ls1); - s.mk_clause({0, false}, {3, true}); - s.mk_clause({1, false}, {3, true}); - s.mk_clause({2, false}, {3, true}); + s.mk_clause(sat::literal(0, false), sat::literal(3, true)); + s.mk_clause(sat::literal(1, false), sat::literal(3, true)); + s.mk_clause(sat::literal(2, false), sat::literal(3, true)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_and), "and", 6, 0, 2, 4); } @@ -96,14 +96,14 @@ static void tst_single_xor() { sat::solver s({}, r); _init_solver(s); - _mk_clause4(s, {0, true}, {1, false}, {2, false}, {3, false}); - _mk_clause4(s, {0, false}, {1, true}, {2, false}, {3, false}); - _mk_clause4(s, {0, false}, {1, false}, {2, true}, {3, false}); - _mk_clause4(s, {0, false}, {1, false}, {2, false}, {3, true}); - _mk_clause4(s, {0, false}, {1, true}, {2, true}, {3, true}); - _mk_clause4(s, {0, true}, {1, false}, {2, true}, {3, true}); - _mk_clause4(s, {0, true}, {1, true}, {2, false}, {3, true}); - _mk_clause4(s, {0, true}, {1, true}, {2, true}, {3, false}); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, false), sat::literal(2, false), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, true), sat::literal(2, false), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, false), sat::literal(2, true), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, false), sat::literal(2, false), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, true), sat::literal(2, true), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, false), sat::literal(2, true), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, true), sat::literal(2, false), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, true), sat::literal(2, true), sat::literal(3, false)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_xor), "xor", 1, 3, 4, 6); } @@ -113,12 +113,12 @@ static void tst_single_andxor() { sat::solver s({}, r); _init_solver(s); - s.mk_clause({0, true}, {1, false}, {3, true}); - s.mk_clause({0, true}, {2, false}, {3, true}); - _mk_clause4(s, {0, true}, {1, true}, {2, true}, {3, false}); - s.mk_clause({0, false}, {1, false}, {3, false}); - s.mk_clause({0, false}, {2, false}, {3, false}); - _mk_clause4(s, {0, false}, {1, true}, {2, true}, {3, true}); + s.mk_clause(sat::literal(0, true), sat::literal(1, false), sat::literal(3, true)); + s.mk_clause(sat::literal(0, true), sat::literal(2, false), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, true), sat::literal(2, true), sat::literal(3, false)); + s.mk_clause(sat::literal(0, false), sat::literal(1, false), sat::literal(3, false)); + s.mk_clause(sat::literal(0, false), sat::literal(2, false), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, true), sat::literal(2, true), sat::literal(3, true)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_andxor), "andxor", 0, 6, 2, 4); } @@ -128,11 +128,11 @@ static void tst_single_xorand() { sat::solver s({}, r); _init_solver(s); - s.mk_clause({0, false}, {3, true}); - s.mk_clause({1, false}, {2, false}, {3, true}); - s.mk_clause({1, true}, {2, true}, {3, true}); - _mk_clause4(s, {0, true}, {1, true}, {2, false}, {3, false}); - _mk_clause4(s, {0, true}, {1, false}, {2, true}, {3, false}); + s.mk_clause(sat::literal(0, false), sat::literal(3, true)); + s.mk_clause(sat::literal(1, false), sat::literal(2, false), sat::literal(3, true)); + s.mk_clause(sat::literal(1, true), sat::literal(2, true), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, true), sat::literal(2, false), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, false), sat::literal(2, true), sat::literal(3, false)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_xorand), "xorand", 6, 0, 3, 5); } @@ -142,11 +142,11 @@ static void tst_single_gamble() { sat::solver s({}, r); _init_solver(s); - s.mk_clause({0, true}, {1, false}, {3, true}); - s.mk_clause({1, true}, {2, false}, {3, true}); - s.mk_clause({0, false}, {2, true}, {3, true}); - _mk_clause4(s, {0, false}, {1, false}, {2, false}, {3, false}); - _mk_clause4(s, {0, true}, {1, true}, {2, true}, {3, false}); + s.mk_clause(sat::literal(0, true), sat::literal(1, false), sat::literal(3, true)); + s.mk_clause(sat::literal(1, true), sat::literal(2, false), sat::literal(3, true)); + s.mk_clause(sat::literal(0, false), sat::literal(2, true), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, false), sat::literal(2, false), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, true), sat::literal(2, true), sat::literal(3, false)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_gamble), "gamble", 6, 0, 2, 4); } @@ -156,13 +156,13 @@ static void tst_single_onehot() { sat::solver s({}, r); _init_solver(s); - s.mk_clause({0, true}, {1, true}, {3, true}); - s.mk_clause({0, true}, {2, true}, {3, true}); - s.mk_clause({1, true}, {2, true}, {3, true}); - _mk_clause4(s, {0, false}, {1, false}, {2, false}, {3, true}); - _mk_clause4(s, {0, true}, {1, false}, {2, false}, {3, false}); - _mk_clause4(s, {0, false}, {1, true}, {2, false}, {3, false}); - _mk_clause4(s, {0, false}, {1, false}, {2, true}, {3, false}); + s.mk_clause(sat::literal(0, true), sat::literal(1, true), sat::literal(3, true)); + s.mk_clause(sat::literal(0, true), sat::literal(2, true), sat::literal(3, true)); + s.mk_clause(sat::literal(1, true), sat::literal(2, true), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, false), sat::literal(2, false), sat::literal(3, true)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, false), sat::literal(2, false), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, true), sat::literal(2, false), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, false), sat::literal(1, false), sat::literal(2, true), sat::literal(3, false)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_onehot), "onehot", 6, 0, 2, 4); } @@ -172,11 +172,11 @@ static void tst_single_dot() { sat::solver s({}, r); _init_solver(s); - s.mk_clause({0, false}, {2, false}, {3, true}); - s.mk_clause({0, true}, {1, true}, {3, true}); - s.mk_clause({0, true}, {2, true}, {3, true}); - s.mk_clause({0, false}, {2, true}, {3, false}); - _mk_clause4(s, {0, true}, {1, false}, {2, false}, {3, false}); + s.mk_clause(sat::literal(0, false), sat::literal(2, false), sat::literal(3, true)); + s.mk_clause(sat::literal(0, true), sat::literal(1, true), sat::literal(3, true)); + s.mk_clause(sat::literal(0, true), sat::literal(2, true), sat::literal(3, true)); + s.mk_clause(sat::literal(0, false), sat::literal(2, true), sat::literal(3, false)); + _mk_clause4(s, sat::literal(0, true), sat::literal(1, false), sat::literal(2, false), sat::literal(3, false)); _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_dot), "dot", 6, 0, 2, 4); } diff --git a/src/util/sat_literal.h b/src/util/sat_literal.h new file mode 100644 index 000000000..f8be2eb3f --- /dev/null +++ b/src/util/sat_literal.h @@ -0,0 +1,194 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + sat_literal.h + +Abstract: + + Literal datatype + +Author: + + Leonardo de Moura (leonardo) 2011-05-21. + +--*/ +#pragma once + +#include "util/lbool.h" +#include "util/vector.h" +#include "util/uint_set.h" + +namespace sat { + + /** + \brief A boolean variable is just an integer. + */ + typedef unsigned bool_var; + + typedef svector bool_var_vector; + + const bool_var null_bool_var = UINT_MAX >> 1; + + /** + \brief The literal b is represented by the value 2*b, and + the literal (not b) by the value 2*b + 1 + */ + class literal { + unsigned m_val; + public: + literal():m_val(null_bool_var << 1) { + SASSERT(var() == null_bool_var && !sign()); + } + + explicit literal(bool_var v, bool _sign = false): + m_val((v << 1) + static_cast(_sign)) { + SASSERT(var() == v); + SASSERT(sign() == _sign); + } + + bool_var var() const { + return m_val >> 1; + } + + bool sign() const { + return m_val & 1ul; + } + + literal unsign() const { + literal l; + l.m_val = m_val & ~1; + return l; + } + + unsigned index() const { + return m_val; + } + + void neg() { + m_val = m_val ^ 1; + } + + friend literal operator~(literal l) { + l.m_val = l.m_val ^1; + return l; + } + + unsigned to_uint() const { return m_val; } + + unsigned hash() const { return to_uint(); } + + friend literal to_literal(unsigned x); + friend bool operator<(literal const & l1, literal const & l2); + friend bool operator==(literal const & l1, literal const & l2); + friend bool operator!=(literal const & l1, literal const & l2); + }; + + const literal null_literal; + struct literal_hash : obj_hash {}; + + inline literal to_literal(unsigned x) { literal l; l.m_val = x; return l; } + 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 bool operator!=(literal const & l1, literal const & l2) { return l1.m_val != l2.m_val; } + + + typedef svector literal_vector; + typedef std::pair literal_pair; + + struct literal2unsigned { unsigned operator()(literal l) const { return l.to_uint(); } }; + + typedef approx_set_tpl literal_approx_set; + + typedef approx_set_tpl var_approx_set; + + + inline void negate(literal_vector& ls) { for (unsigned i = 0; i < ls.size(); ++i) ls[i].neg(); } + + typedef tracked_uint_set uint_set; + + typedef uint_set bool_var_set; + + class literal_set { + uint_set m_set; + public: + literal_set(literal_vector const& v) { + for (unsigned i = 0; i < v.size(); ++i) insert(v[i]); + } + literal_set() {} + literal_vector to_vector() const { + literal_vector result; + for (literal lit : *this) result.push_back(lit); + return result; + } + literal_set& operator=(literal_vector const& v) { + reset(); + for (unsigned i = 0; i < v.size(); ++i) insert(v[i]); + return *this; + } + + void insert(literal l) { m_set.insert(l.index()); } + void remove(literal l) { m_set.remove(l.index()); } + literal pop() { return to_literal(m_set.erase()); } + bool contains(literal l) const { return m_set.contains(l.index()); } + bool empty() const { return m_set.empty(); } + unsigned size() const { return m_set.size(); } + void reset() { m_set.reset(); } + void finalize() { m_set.finalize(); } + class iterator { + uint_set::iterator m_it; + public: + iterator(uint_set::iterator it):m_it(it) {} + literal operator*() const { return to_literal(*m_it); } + iterator& operator++() { ++m_it; return *this; } + iterator operator++(int) { iterator tmp = *this; ++m_it; return tmp; } + bool operator==(iterator const& it) const { return m_it == it.m_it; } + bool operator!=(iterator const& it) const { return m_it != it.m_it; } + }; + iterator begin() const { return iterator(m_set.begin()); } + iterator end() const { return iterator(m_set.end()); } + literal_set& operator&=(literal_set const& other) { + m_set &= other.m_set; + return *this; + } + literal_set& operator|=(literal_set const& other) { + m_set |= other.m_set; + return *this; + } + }; + + struct dimacs_lit { + literal m_lit; + dimacs_lit(literal l):m_lit(l) {} + }; + + inline std::ostream & operator<<(std::ostream & out, dimacs_lit const & dl) { + literal l = dl.m_lit; + if (l.sign()) out << "-" << (l.var() + 1); + else out << (l.var() + 1); + return out; + } + + struct mk_lits_pp { + unsigned m_num; + literal const * m_lits; + mk_lits_pp(unsigned num, literal const * ls):m_num(num), m_lits(ls) {} + }; + + inline std::ostream & operator<<(std::ostream & out, mk_lits_pp const & ls) { + for (unsigned i = 0; i < ls.m_num; i++) { + if (i > 0) out << " "; + out << ls.m_lits[i]; + } + return out; + } + + inline std::ostream & operator<<(std::ostream & out, literal_vector const & ls) { + return out << mk_lits_pp(ls.size(), ls.data()); + } + +}; + +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; } +