mirror of
https://github.com/Z3Prover/z3
synced 2025-04-30 04:15:51 +00:00
consolidate literals
This commit is contained in:
Nikolaj Bjorner
parent
c959e28d4a
commit
03d2c5f3d0
9 changed files with 299 additions and 323 deletions
|
|
@ -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> 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<unsigned>(_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<literal> {};
|
||||
|
||||
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> literal_vector;
|
||||
typedef std::pair<literal, literal> 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, literal2unsigned, unsigned> literal_approx_set;
|
||||
|
||||
|
|
@ -141,7 +64,6 @@ namespace sat {
|
|||
|
||||
typedef svector<lbool> 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() {}
|
||||
|
|
|
|||
|
|
@ -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 << ")";
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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";);
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
||||
|
|
|
|||
|
|
@ -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";
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
|
|||
|
|
@ -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<int>(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> literal_vector;
|
||||
typedef sbuffer<literal> 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<typename T>
|
||||
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, literal2unsigned> literal_approx_set;
|
||||
|
||||
bool backward_subsumption(unsigned num_lits1, literal const * lits1, unsigned num_lits2, literal const * lits2);
|
||||
};
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
|
|
|||
194
src/util/sat_literal.h
Normal file
194
src/util/sat_literal.h
Normal file
|
|
@ -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> 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<unsigned>(_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<literal> {};
|
||||
|
||||
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> literal_vector;
|
||||
typedef std::pair<literal, literal> literal_pair;
|
||||
|
||||
struct literal2unsigned { unsigned operator()(literal l) const { return l.to_uint(); } };
|
||||
|
||||
typedef approx_set_tpl<literal, literal2unsigned, unsigned> literal_approx_set;
|
||||
|
||||
typedef approx_set_tpl<bool_var, u2u, unsigned> 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; }
|
||||
|
||||
Loading…
Add table
Add a link
Reference in a new issue