mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
merge with opt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
commit
859c68c2ac
58 changed files with 1329 additions and 526 deletions
|
|
@ -71,6 +71,11 @@ public:
|
|||
|
||||
template<typename T>
|
||||
T * operator()(T const * n) {
|
||||
return translate(n);
|
||||
}
|
||||
|
||||
template<typename T>
|
||||
T * translate(T const * n) {
|
||||
if (&from() == &to()) return const_cast<T*>(n);
|
||||
SASSERT(!n || from().contains(const_cast<T*>(n)));
|
||||
ast * r = process(n);
|
||||
|
|
@ -78,9 +83,17 @@ public:
|
|||
return static_cast<T*>(r);
|
||||
}
|
||||
|
||||
|
||||
ast_manager & from() const { return m_from_manager; }
|
||||
ast_manager & to() const { return m_to_manager; }
|
||||
|
||||
template<typename T>
|
||||
ref_vector<T, ast_manager> operator()(ref_vector<T, ast_manager> const& src) {
|
||||
ref_vector<T, ast_manager> dst(to());
|
||||
for (expr* v : src) dst.push_back(translate(v));
|
||||
return dst;
|
||||
}
|
||||
|
||||
void reset_cache();
|
||||
void cleanup();
|
||||
|
||||
|
|
@ -100,6 +113,7 @@ inline expr * translate(expr const * e, ast_manager & from, ast_manager & to) {
|
|||
return ast_translation(from, to)(e);
|
||||
}
|
||||
|
||||
|
||||
class expr_dependency_translation {
|
||||
ast_translation & m_translation;
|
||||
ptr_vector<expr> m_buffer;
|
||||
|
|
|
|||
|
|
@ -56,9 +56,7 @@ struct pb2bv_rewriter::imp {
|
|||
rational m_k;
|
||||
vector<rational> m_coeffs;
|
||||
bool m_keep_cardinality_constraints;
|
||||
bool m_keep_pb_constraints;
|
||||
bool m_pb_num_system;
|
||||
bool m_pb_totalizer;
|
||||
symbol m_pb_solver;
|
||||
unsigned m_min_arity;
|
||||
|
||||
template<lbool is_le>
|
||||
|
|
@ -85,7 +83,7 @@ struct pb2bv_rewriter::imp {
|
|||
|
||||
struct compare_coeffs {
|
||||
bool operator()(ca const& x, ca const& y) const {
|
||||
return x.first < y.first;
|
||||
return x.first > y.first;
|
||||
}
|
||||
};
|
||||
|
||||
|
|
@ -126,11 +124,12 @@ struct pb2bv_rewriter::imp {
|
|||
if (i + 1 < sz && !m_coeffs[i+1].is_neg()) tout << "+ ";
|
||||
}
|
||||
switch (is_le) {
|
||||
case l_true: tout << "<= "; break;
|
||||
case l_true: tout << "<= "; break;
|
||||
case l_undef: tout << "= "; break;
|
||||
case l_false: tout << ">= "; break;
|
||||
}
|
||||
tout << k << "\n";);
|
||||
|
||||
if (k.is_zero()) {
|
||||
if (is_le != l_false) {
|
||||
return expr_ref(m.mk_not(::mk_or(m_args)), m);
|
||||
|
|
@ -143,7 +142,7 @@ struct pb2bv_rewriter::imp {
|
|||
return expr_ref((is_le == l_false)?m.mk_true():m.mk_false(), m);
|
||||
}
|
||||
|
||||
if (m_pb_totalizer) {
|
||||
if (m_pb_solver == "totalizer") {
|
||||
expr_ref result(m);
|
||||
switch (is_le) {
|
||||
case l_true: if (mk_le_tot(sz, args, k, result)) return result; else break;
|
||||
|
|
@ -152,7 +151,7 @@ struct pb2bv_rewriter::imp {
|
|||
}
|
||||
}
|
||||
|
||||
if (m_pb_num_system) {
|
||||
if (m_pb_solver == "sorting") {
|
||||
expr_ref result(m);
|
||||
switch (is_le) {
|
||||
case l_true: if (mk_le(sz, args, k, result)) return result; else break;
|
||||
|
|
@ -161,6 +160,15 @@ struct pb2bv_rewriter::imp {
|
|||
}
|
||||
}
|
||||
|
||||
if (m_pb_solver == "segmented") {
|
||||
expr_ref result(m);
|
||||
switch (is_le) {
|
||||
case l_true: return mk_seg_le(k);
|
||||
case l_false: return mk_seg_ge(k);
|
||||
case l_undef: break;
|
||||
}
|
||||
}
|
||||
|
||||
// fall back to divide and conquer encoding.
|
||||
SASSERT(k.is_pos());
|
||||
expr_ref zero(m), bound(m);
|
||||
|
|
@ -486,14 +494,82 @@ struct pb2bv_rewriter::imp {
|
|||
return true;
|
||||
}
|
||||
|
||||
expr_ref mk_and(expr_ref& a, expr_ref& b) {
|
||||
/**
|
||||
\brief Segment based encoding.
|
||||
The PB terms are partitoned into segments, such that each segment contains arguments with the same cofficient.
|
||||
The segments are sorted, such that the segment with highest coefficient is first.
|
||||
Then for each segment create circuits based on sorting networks the arguments of the segment.
|
||||
*/
|
||||
|
||||
expr_ref mk_seg_ge(rational const& k) {
|
||||
rational bound(-k);
|
||||
for (unsigned i = 0; i < m_args.size(); ++i) {
|
||||
m_args[i] = mk_not(m_args[i].get());
|
||||
bound += m_coeffs[i];
|
||||
}
|
||||
return mk_seg_le(bound);
|
||||
}
|
||||
|
||||
expr_ref mk_seg_le(rational const& k) {
|
||||
sort_args();
|
||||
unsigned sz = m_args.size();
|
||||
expr* const* args = m_args.c_ptr();
|
||||
|
||||
// Create sorted entries.
|
||||
vector<ptr_vector<expr>> outs;
|
||||
vector<rational> coeffs;
|
||||
for (unsigned i = 0, seg_size = 0; i < sz; i += seg_size) {
|
||||
seg_size = segment_size(i);
|
||||
ptr_vector<expr> out;
|
||||
m_sort.sorting(seg_size, args + i, out);
|
||||
out.push_back(m.mk_false());
|
||||
outs.push_back(out);
|
||||
coeffs.push_back(m_coeffs[i]);
|
||||
}
|
||||
return mk_seg_le_rec(outs, coeffs, 0, k);
|
||||
}
|
||||
|
||||
expr_ref mk_seg_le_rec(vector<ptr_vector<expr>> const& outs, vector<rational> const& coeffs, unsigned i, rational const& k) {
|
||||
rational const& c = coeffs[i];
|
||||
ptr_vector<expr> const& out = outs[i];
|
||||
if (k.is_neg()) {
|
||||
return expr_ref(m.mk_false(), m);
|
||||
}
|
||||
if (i == outs.size()) {
|
||||
return expr_ref(m.mk_true(), m);
|
||||
}
|
||||
if (i + 1 == outs.size() && k >= rational(out.size()-1)*c) {
|
||||
return expr_ref(m.mk_true(), m);
|
||||
}
|
||||
expr_ref_vector fmls(m);
|
||||
fmls.push_back(m.mk_implies(m.mk_not(out[0]), mk_seg_le_rec(outs, coeffs, i + 1, k)));
|
||||
rational k1;
|
||||
for (unsigned j = 0; j + 1 < out.size(); ++j) {
|
||||
k1 = k - rational(j+1)*c;
|
||||
if (k1.is_neg()) {
|
||||
fmls.push_back(m.mk_not(out[j]));
|
||||
break;
|
||||
}
|
||||
fmls.push_back(m.mk_implies(m.mk_and(out[j], m.mk_not(out[j+1])), mk_seg_le_rec(outs, coeffs, i + 1, k1)));
|
||||
}
|
||||
return ::mk_and(fmls);
|
||||
}
|
||||
|
||||
// The number of arguments with the same coefficient.
|
||||
unsigned segment_size(unsigned start) const {
|
||||
unsigned i = start;
|
||||
while (i < m_args.size() && m_coeffs[i] == m_coeffs[start]) ++i;
|
||||
return i - start;
|
||||
}
|
||||
|
||||
expr_ref mk_and(expr_ref& a, expr_ref& b) {
|
||||
if (m.is_true(a)) return b;
|
||||
if (m.is_true(b)) return a;
|
||||
if (m.is_false(a)) return a;
|
||||
if (m.is_false(b)) return b;
|
||||
return expr_ref(m.mk_and(a, b), m);
|
||||
}
|
||||
|
||||
|
||||
expr_ref mk_or(expr_ref& a, expr_ref& b) {
|
||||
if (m.is_true(a)) return a;
|
||||
if (m.is_true(b)) return b;
|
||||
|
|
@ -607,12 +683,12 @@ struct pb2bv_rewriter::imp {
|
|||
m_trail(m),
|
||||
m_args(m),
|
||||
m_keep_cardinality_constraints(false),
|
||||
m_keep_pb_constraints(false),
|
||||
m_pb_num_system(false),
|
||||
m_pb_totalizer(false),
|
||||
m_pb_solver(symbol("solver")),
|
||||
m_min_arity(9)
|
||||
{}
|
||||
|
||||
void set_pb_solver(symbol const& s) { m_pb_solver = s; }
|
||||
|
||||
bool mk_app(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
|
||||
if (f->get_family_id() == pb.get_family_id() && mk_pb(full, f, sz, args, result)) {
|
||||
// skip
|
||||
|
|
@ -756,13 +832,13 @@ struct pb2bv_rewriter::imp {
|
|||
result = m_sort.ge(full, pb.get_k(f).get_unsigned(), sz, args);
|
||||
++m_imp.m_compile_card;
|
||||
}
|
||||
else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_keep_pb_constraints) {
|
||||
else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_pb_solver == "solver") {
|
||||
return false;
|
||||
}
|
||||
else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_keep_pb_constraints) {
|
||||
else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_pb_solver == "solver") {
|
||||
return false;
|
||||
}
|
||||
else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_keep_pb_constraints) {
|
||||
else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_pb_solver == "solver") {
|
||||
return false;
|
||||
}
|
||||
else {
|
||||
|
|
@ -811,17 +887,6 @@ struct pb2bv_rewriter::imp {
|
|||
m_keep_cardinality_constraints = f;
|
||||
}
|
||||
|
||||
void keep_pb_constraints(bool f) {
|
||||
m_keep_pb_constraints = f;
|
||||
}
|
||||
|
||||
void pb_num_system(bool f) {
|
||||
m_pb_num_system = f;
|
||||
}
|
||||
|
||||
void pb_totalizer(bool f) {
|
||||
m_pb_totalizer = f;
|
||||
}
|
||||
void set_at_most1(sorting_network_encoding enc) { m_sort.cfg().m_encoding = enc; }
|
||||
|
||||
};
|
||||
|
|
@ -836,9 +901,7 @@ struct pb2bv_rewriter::imp {
|
|||
}
|
||||
card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {}
|
||||
void keep_cardinality_constraints(bool f) { m_r.keep_cardinality_constraints(f); }
|
||||
void keep_pb_constraints(bool f) { m_r.keep_pb_constraints(f); }
|
||||
void pb_num_system(bool f) { m_r.pb_num_system(f); }
|
||||
void pb_totalizer(bool f) { m_r.pb_totalizer(f); }
|
||||
void set_pb_solver(symbol const& s) { m_r.set_pb_solver(s); }
|
||||
void set_at_most1(sorting_network_encoding enc) { m_r.set_at_most1(enc); }
|
||||
|
||||
};
|
||||
|
|
@ -850,9 +913,7 @@ struct pb2bv_rewriter::imp {
|
|||
rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg),
|
||||
m_cfg(i, m) {}
|
||||
void keep_cardinality_constraints(bool f) { m_cfg.keep_cardinality_constraints(f); }
|
||||
void keep_pb_constraints(bool f) { m_cfg.keep_pb_constraints(f); }
|
||||
void pb_num_system(bool f) { m_cfg.pb_num_system(f); }
|
||||
void pb_totalizer(bool f) { m_cfg.pb_totalizer(f); }
|
||||
void set_pb_solver(symbol const& s) { m_cfg.set_pb_solver(s); }
|
||||
void set_at_most1(sorting_network_encoding e) { m_cfg.set_at_most1(e); }
|
||||
void rewrite(expr* e, expr_ref& r, proof_ref& p) {
|
||||
expr_ref ee(e, m());
|
||||
|
|
@ -875,26 +936,15 @@ struct pb2bv_rewriter::imp {
|
|||
gparams::get_module("sat").get_bool("cardinality.solver", false);
|
||||
}
|
||||
|
||||
bool keep_pb() const {
|
||||
symbol pb_solver() const {
|
||||
params_ref const& p = m_params;
|
||||
return
|
||||
p.get_bool("keep_pb_constraints", false) ||
|
||||
p.get_bool("sat.pb.solver", false) ||
|
||||
p.get_bool("pb.solver", false) ||
|
||||
gparams::get_module("sat").get_sym("pb.solver", symbol()) == symbol("solver") ;
|
||||
symbol s = p.get_sym("sat.pb.solver", symbol());
|
||||
if (s != symbol()) return s;
|
||||
s = p.get_sym("pb.solver", symbol());
|
||||
if (s != symbol()) return s;
|
||||
return gparams::get_module("sat").get_sym("pb.solver", symbol("solver"));
|
||||
}
|
||||
|
||||
bool pb_num_system() const {
|
||||
return m_params.get_bool("pb_num_system", false) ||
|
||||
gparams::get_module("sat").get_sym("pb.solver", symbol()) == symbol("sorting");
|
||||
}
|
||||
|
||||
bool pb_totalizer() const {
|
||||
return m_params.get_bool("pb_totalizer", false) ||
|
||||
gparams::get_module("sat").get_sym("pb.solver", symbol()) == symbol("totalizer");
|
||||
}
|
||||
|
||||
|
||||
sorting_network_encoding atmost1_encoding() const {
|
||||
symbol enc = m_params.get_sym("atmost1_encoding", symbol());
|
||||
if (enc == symbol()) {
|
||||
|
|
@ -920,16 +970,12 @@ struct pb2bv_rewriter::imp {
|
|||
void updt_params(params_ref const & p) {
|
||||
m_params.append(p);
|
||||
m_rw.keep_cardinality_constraints(keep_cardinality());
|
||||
m_rw.keep_pb_constraints(keep_pb());
|
||||
m_rw.pb_num_system(pb_num_system());
|
||||
m_rw.pb_totalizer(pb_totalizer());
|
||||
m_rw.set_pb_solver(pb_solver());
|
||||
m_rw.set_at_most1(atmost1_encoding());
|
||||
}
|
||||
void collect_param_descrs(param_descrs& r) const {
|
||||
r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints (don't bit-blast them) and use built-in cardinality solver");
|
||||
r.insert("keep_pb_constraints", CPK_BOOL, "(default: true) retain pb constraints (don't bit-blast them) and use built-in pb solver");
|
||||
r.insert("pb_num_system", CPK_BOOL, "(default: false) use pb number system encoding");
|
||||
r.insert("pb_totalizer", CPK_BOOL, "(default: false) use pb totalizer encoding");
|
||||
r.insert("pb.solver", CPK_SYMBOL, "(default: solver) retain pb constraints (don't bit-blast them) and use built-in pb solver");
|
||||
}
|
||||
|
||||
unsigned get_num_steps() const { return m_rw.get_num_steps(); }
|
||||
|
|
|
|||
|
|
@ -253,6 +253,7 @@ bool zstring::contains(zstring const& other) const {
|
|||
|
||||
int zstring::indexof(zstring const& other, int offset) const {
|
||||
SASSERT(offset >= 0);
|
||||
if (static_cast<unsigned>(offset) <= length() && other.length() == 0) return offset;
|
||||
if (static_cast<unsigned>(offset) == length()) return -1;
|
||||
if (other.length() + offset > length()) return -1;
|
||||
unsigned last = length() - other.length();
|
||||
|
|
|
|||
|
|
@ -2245,8 +2245,8 @@ namespace sat {
|
|||
IF_VERBOSE(0,
|
||||
verbose_stream() << "Discrepancy of watched literal: " << l << " id: " << c.id()
|
||||
<< " clause: " << c << (found?" is watched, but shouldn't be":" not watched, but should be") << "\n";
|
||||
display_watch_list(verbose_stream() << l << ": ", s().m_cls_allocator, get_wlist(l)) << "\n";
|
||||
display_watch_list(verbose_stream() << ~l << ": ", s().m_cls_allocator, get_wlist(~l)) << "\n";
|
||||
s().display_watch_list(verbose_stream() << l << ": ", get_wlist(l)) << "\n";
|
||||
s().display_watch_list(verbose_stream() << ~l << ": ", get_wlist(~l)) << "\n";
|
||||
verbose_stream() << "value: " << value(l) << " level: " << lvl(l) << "\n";
|
||||
display(verbose_stream(), c, true);
|
||||
if (c.lit() != null_literal) verbose_stream() << value(c.lit()) << "\n";);
|
||||
|
|
|
|||
101
src/sat/sat_allocator.h
Normal file
101
src/sat/sat_allocator.h
Normal file
|
|
@ -0,0 +1,101 @@
|
|||
/*++
|
||||
Copyright (c) 2018 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
sat_allocator.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Small object allocator suitable for clauses
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj bjorner (nbjorner) 2018-04-26.
|
||||
|
||||
Revision History:
|
||||
--*/
|
||||
|
||||
#ifndef SAT_ALLOCATOR_H_
|
||||
#define SAT_ALLOCATOR_H_
|
||||
|
||||
#include "util/vector.h"
|
||||
#include "util/machine.h"
|
||||
|
||||
class sat_allocator {
|
||||
static const unsigned CHUNK_SIZE = (1 << 16);
|
||||
static const unsigned SMALL_OBJ_SIZE = 512;
|
||||
static const unsigned MASK = ((1 << PTR_ALIGNMENT) - 1);
|
||||
static const unsigned NUM_FREE = 1 + (SMALL_OBJ_SIZE >> PTR_ALIGNMENT);
|
||||
struct chunk {
|
||||
char * m_curr;
|
||||
char m_data[CHUNK_SIZE];
|
||||
chunk():m_curr(m_data) {}
|
||||
};
|
||||
ptr_vector<chunk> m_chunks;
|
||||
void * m_chunk_ptr;
|
||||
ptr_vector<void> m_free[NUM_FREE];
|
||||
size_t m_alloc_size;
|
||||
char const * m_id;
|
||||
|
||||
unsigned align_size(size_t sz) const {
|
||||
return free_slot_id(sz) << PTR_ALIGNMENT;
|
||||
}
|
||||
unsigned free_slot_id(size_t size) const {
|
||||
return (static_cast<unsigned>(size >> PTR_ALIGNMENT) + ((0 != (size & MASK)) ? 1u : 0u));
|
||||
}
|
||||
public:
|
||||
sat_allocator(char const * id = "unknown"): m_id(id), m_alloc_size(0), m_chunk_ptr(nullptr) {}
|
||||
~sat_allocator() { reset(); }
|
||||
void reset() {
|
||||
for (chunk * ch : m_chunks) dealloc(ch);
|
||||
m_chunks.reset();
|
||||
for (unsigned i = 0; i < NUM_FREE; ++i) m_free[i].reset();
|
||||
m_alloc_size = 0;
|
||||
m_chunk_ptr = nullptr;
|
||||
}
|
||||
void * allocate(size_t size) {
|
||||
m_alloc_size += size;
|
||||
if (size >= SMALL_OBJ_SIZE) {
|
||||
return memory::allocate(size);
|
||||
}
|
||||
unsigned slot_id = free_slot_id(size);
|
||||
if (!m_free[slot_id].empty()) {
|
||||
void* result = m_free[slot_id].back();
|
||||
m_free[slot_id].pop_back();
|
||||
return result;
|
||||
}
|
||||
if (m_chunks.empty()) {
|
||||
m_chunks.push_back(alloc(chunk));
|
||||
m_chunk_ptr = m_chunks.back();
|
||||
}
|
||||
|
||||
unsigned sz = align_size(size);
|
||||
if ((char*)m_chunk_ptr + sz > (char*)m_chunks.back() + CHUNK_SIZE) {
|
||||
m_chunks.push_back(alloc(chunk));
|
||||
m_chunk_ptr = m_chunks.back();
|
||||
}
|
||||
void * result = m_chunk_ptr;
|
||||
m_chunk_ptr = (char*)m_chunk_ptr + sz;
|
||||
return result;
|
||||
}
|
||||
|
||||
void deallocate(size_t size, void * p) {
|
||||
m_alloc_size -= size;
|
||||
if (size >= SMALL_OBJ_SIZE) {
|
||||
memory::deallocate(p);
|
||||
}
|
||||
else {
|
||||
m_free[free_slot_id(size)].push_back(p);
|
||||
}
|
||||
}
|
||||
size_t get_allocation_size() const { return m_alloc_size; }
|
||||
};
|
||||
|
||||
inline void * operator new(size_t s, sat_allocator & r) { return r.allocate(s); }
|
||||
inline void * operator new[](size_t s, sat_allocator & r) { return r.allocate(s); }
|
||||
inline void operator delete(void * p, sat_allocator & r) { UNREACHABLE(); }
|
||||
inline void operator delete[](void * p, sat_allocator & r) { UNREACHABLE(); }
|
||||
|
||||
#endif /* SAT_ALLOCATOR_H_ */
|
||||
|
||||
|
|
@ -108,7 +108,6 @@ namespace sat {
|
|||
int64 limit = -m_asymm_branch_limit;
|
||||
std::stable_sort(clauses.begin(), clauses.end(), clause_size_lt());
|
||||
m_counter -= clauses.size();
|
||||
SASSERT(s.m_qhead == s.m_trail.size());
|
||||
clause_vector::iterator it = clauses.begin();
|
||||
clause_vector::iterator it2 = it;
|
||||
clause_vector::iterator end = clauses.end();
|
||||
|
|
@ -120,7 +119,6 @@ namespace sat {
|
|||
}
|
||||
break;
|
||||
}
|
||||
SASSERT(s.m_qhead == s.m_trail.size());
|
||||
clause & c = *(*it);
|
||||
if (m_counter < limit || s.inconsistent() || c.was_removed()) {
|
||||
*it2 = *it;
|
||||
|
|
@ -335,13 +333,18 @@ namespace sat {
|
|||
if (!m_to_delete.empty()) {
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < c.size(); ++i) {
|
||||
if (!m_to_delete.contains(c[i])) {
|
||||
c[j] = c[i];
|
||||
++j;
|
||||
}
|
||||
else {
|
||||
m_pos.erase(c[i]);
|
||||
m_neg.erase(~c[i]);
|
||||
literal lit = c[i];
|
||||
switch (s.value(lit)) {
|
||||
case l_true:
|
||||
scoped_d.del_clause();
|
||||
return false;
|
||||
case l_false:
|
||||
break;
|
||||
default:
|
||||
if (!m_to_delete.contains(lit)) {
|
||||
c[j++] = lit;
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
return re_attach(scoped_d, c, j);
|
||||
|
|
@ -361,6 +364,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
bool asymm_branch::flip_literal_at(clause const& c, unsigned flip_index, unsigned& new_sz) {
|
||||
VERIFY(s.m_trail.size() == s.m_qhead);
|
||||
bool found_conflict = false;
|
||||
unsigned i = 0, sz = c.size();
|
||||
s.push();
|
||||
|
|
@ -401,10 +405,12 @@ namespace sat {
|
|||
}
|
||||
|
||||
bool asymm_branch::re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz) {
|
||||
VERIFY(s.m_trail.size() == s.m_qhead);
|
||||
m_elim_literals += c.size() - new_sz;
|
||||
if (c.is_learned()) {
|
||||
m_elim_learned_literals += c.size() - new_sz;
|
||||
}
|
||||
|
||||
switch(new_sz) {
|
||||
case 0:
|
||||
s.set_conflict(justification());
|
||||
|
|
@ -414,19 +420,18 @@ namespace sat {
|
|||
s.assign(c[0], justification());
|
||||
s.propagate_core(false);
|
||||
scoped_d.del_clause();
|
||||
SASSERT(s.inconsistent() || s.m_qhead == s.m_trail.size());
|
||||
return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state.
|
||||
case 2:
|
||||
SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
|
||||
VERIFY(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
|
||||
s.mk_bin_clause(c[0], c[1], c.is_learned());
|
||||
if (s.m_trail.size() > s.m_qhead) s.propagate_core(false);
|
||||
scoped_d.del_clause();
|
||||
SASSERT(s.m_qhead == s.m_trail.size());
|
||||
return false;
|
||||
default:
|
||||
c.shrink(new_sz);
|
||||
if (s.m_config.m_drat) s.m_drat.add(c, true);
|
||||
// if (s.m_config.m_drat) s.m_drat.del(c0); // TBD
|
||||
SASSERT(s.m_qhead == s.m_trail.size());
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
@ -445,12 +450,8 @@ namespace sat {
|
|||
bool asymm_branch::process(clause & c) {
|
||||
TRACE("asymm_branch_detail", tout << "processing: " << c << "\n";);
|
||||
SASSERT(s.scope_lvl() == 0);
|
||||
SASSERT(s.m_qhead == s.m_trail.size());
|
||||
SASSERT(!s.inconsistent());
|
||||
|
||||
#ifdef Z3DEBUG
|
||||
unsigned trail_sz = s.m_trail.size();
|
||||
#endif
|
||||
unsigned sz = c.size();
|
||||
SASSERT(sz > 0);
|
||||
unsigned i;
|
||||
|
|
@ -474,8 +475,6 @@ namespace sat {
|
|||
bool found_conflict = flip_literal_at(c, flip_position, new_sz);
|
||||
SASSERT(!s.inconsistent());
|
||||
SASSERT(s.scope_lvl() == 0);
|
||||
SASSERT(trail_sz == s.m_trail.size());
|
||||
SASSERT(s.m_qhead == s.m_trail.size());
|
||||
if (!found_conflict) {
|
||||
// clause size can't be reduced.
|
||||
return true;
|
||||
|
|
|
|||
|
|
@ -194,7 +194,9 @@ namespace sat {
|
|||
if (u != get_parent(v) && safe_reach(u, v)) {
|
||||
++elim;
|
||||
add_del(~u, v);
|
||||
// IF_VERBOSE(1, verbose_stream() << "remove " << u << " -> " << v << "\n");
|
||||
if (s.get_config().m_drat) s.m_drat.del(~u, v);
|
||||
s.m_mc.stackv().reset(); // TBD: brittle code
|
||||
s.add_ate(~u, v);
|
||||
if (find_binary_watch(wlist, ~v)) {
|
||||
IF_VERBOSE(10, verbose_stream() << "binary: " << ~u << "\n");
|
||||
s.assign(~u, justification());
|
||||
|
|
|
|||
|
|
@ -95,7 +95,6 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
bool clause::satisfied_by(model const & m) const {
|
||||
for (literal l : *this) {
|
||||
if (l.sign()) {
|
||||
|
|
@ -110,6 +109,23 @@ namespace sat {
|
|||
return false;
|
||||
}
|
||||
|
||||
clause_offset clause::get_new_offset() const {
|
||||
unsigned o1 = m_lits[0].index();
|
||||
if (sizeof(clause_offset) == 8) {
|
||||
unsigned o2 = m_lits[1].index();
|
||||
return (clause_offset)o1 + (((clause_offset)o2) << 32);
|
||||
}
|
||||
return (clause_offset)o1;
|
||||
}
|
||||
|
||||
void clause::set_new_offset(clause_offset offset) {
|
||||
m_lits[0] = to_literal(static_cast<unsigned>(offset));
|
||||
if (sizeof(offset) == 8) {
|
||||
m_lits[1] = to_literal(static_cast<unsigned>(offset >> 32));
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void tmp_clause::set(unsigned num_lits, literal const * lits, bool learned) {
|
||||
if (m_clause && m_clause->m_capacity < num_lits) {
|
||||
dealloc_svect(m_clause);
|
||||
|
|
@ -135,12 +151,15 @@ namespace sat {
|
|||
m_allocator("clause-allocator") {
|
||||
}
|
||||
|
||||
void clause_allocator::finalize() {
|
||||
m_allocator.reset();
|
||||
}
|
||||
|
||||
clause * clause_allocator::get_clause(clause_offset cls_off) const {
|
||||
SASSERT(cls_off == reinterpret_cast<clause_offset>(reinterpret_cast<clause*>(cls_off)));
|
||||
return reinterpret_cast<clause *>(cls_off);
|
||||
}
|
||||
|
||||
|
||||
clause_offset clause_allocator::get_offset(clause const * cls) const {
|
||||
SASSERT(cls == reinterpret_cast<clause *>(reinterpret_cast<size_t>(cls)));
|
||||
return reinterpret_cast<size_t>(cls);
|
||||
|
|
@ -155,6 +174,18 @@ namespace sat {
|
|||
return cls;
|
||||
}
|
||||
|
||||
clause * clause_allocator::copy_clause(clause const& other) {
|
||||
size_t size = clause::get_obj_size(other.size());
|
||||
void * mem = m_allocator.allocate(size);
|
||||
clause * cls = new (mem) clause(m_id_gen.mk(), other.size(), other.m_lits, other.is_learned());
|
||||
cls->m_reinit_stack = other.on_reinit_stack();
|
||||
cls->m_glue = other.glue();
|
||||
cls->m_psm = other.psm();
|
||||
cls->m_frozen = other.frozen();
|
||||
cls->m_approx = other.approx();
|
||||
return cls;
|
||||
}
|
||||
|
||||
void clause_allocator::del_clause(clause * cls) {
|
||||
TRACE("sat_clause", tout << "delete: " << cls->id() << " " << *cls << "\n";);
|
||||
m_id_gen.recycle(cls->id());
|
||||
|
|
|
|||
|
|
@ -19,10 +19,11 @@ Revision History:
|
|||
#ifndef SAT_CLAUSE_H_
|
||||
#define SAT_CLAUSE_H_
|
||||
|
||||
#include "sat/sat_types.h"
|
||||
#include "util/small_object_allocator.h"
|
||||
#include "util/id_gen.h"
|
||||
#include "util/map.h"
|
||||
#include "sat/sat_types.h"
|
||||
#include "sat/sat_allocator.h"
|
||||
|
||||
#ifdef _MSC_VER
|
||||
#pragma warning(disable : 4200)
|
||||
|
|
@ -97,6 +98,8 @@ namespace sat {
|
|||
unsigned glue() const { return m_glue; }
|
||||
void set_psm(unsigned psm) { m_psm = psm > 255 ? 255 : psm; }
|
||||
unsigned psm() const { return m_psm; }
|
||||
clause_offset get_new_offset() const;
|
||||
void set_new_offset(clause_offset off);
|
||||
|
||||
bool on_reinit_stack() const { return m_reinit_stack; }
|
||||
void set_reinit_stack(bool f) { m_reinit_stack = f; }
|
||||
|
|
@ -133,13 +136,16 @@ namespace sat {
|
|||
\brief Simple clause allocator that allows uint (32bit integers) to be used to reference clauses (even in 64bit machines).
|
||||
*/
|
||||
class clause_allocator {
|
||||
small_object_allocator m_allocator;
|
||||
id_gen m_id_gen;
|
||||
small_object_allocator m_allocator;
|
||||
id_gen m_id_gen;
|
||||
public:
|
||||
clause_allocator();
|
||||
void finalize();
|
||||
size_t get_allocation_size() const { return m_allocator.get_allocation_size(); }
|
||||
clause * get_clause(clause_offset cls_off) const;
|
||||
clause_offset get_offset(clause const * ptr) const;
|
||||
clause * mk_clause(unsigned num_lits, literal const * lits, bool learned);
|
||||
clause * copy_clause(clause const& other);
|
||||
void del_clause(clause * cls);
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -124,6 +124,15 @@ namespace sat {
|
|||
};
|
||||
|
||||
iterator mk_iterator() const { return iterator(const_cast<clause_use_list*>(this)->m_clauses); }
|
||||
|
||||
std::ostream& display(std::ostream& out) const {
|
||||
iterator it = mk_iterator();
|
||||
while (!it.at_end()) {
|
||||
out << it.curr() << "\n";
|
||||
it.next();
|
||||
}
|
||||
return out;
|
||||
}
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -41,6 +41,7 @@ namespace sat {
|
|||
else
|
||||
throw sat_param_exception("invalid restart strategy");
|
||||
|
||||
m_restart_fast = p.restart_fast();
|
||||
s = p.phase();
|
||||
if (s == symbol("always_false"))
|
||||
m_phase = PS_ALWAYS_FALSE;
|
||||
|
|
@ -60,6 +61,7 @@ namespace sat {
|
|||
m_restart_initial = p.restart_initial();
|
||||
m_restart_factor = p.restart_factor();
|
||||
m_restart_max = p.restart_max();
|
||||
m_propagate_prefetch = p.propagate_prefetch();
|
||||
m_inprocess_max = p.inprocess_max();
|
||||
|
||||
m_random_freq = p.random_freq();
|
||||
|
|
@ -113,12 +115,15 @@ namespace sat {
|
|||
m_lookahead_cube_psat_clause_base = p.lookahead_cube_psat_clause_base();
|
||||
m_lookahead_cube_psat_trigger = p.lookahead_cube_psat_trigger();
|
||||
m_lookahead_global_autarky = p.lookahead_global_autarky();
|
||||
m_lookahead_use_learned = p.lookahead_use_learned();
|
||||
|
||||
|
||||
// These parameters are not exposed
|
||||
m_simplify_mult1 = _p.get_uint("simplify_mult1", 300);
|
||||
m_next_simplify1 = _p.get_uint("next_simplify", 30000);
|
||||
m_simplify_mult2 = _p.get_double("simplify_mult2", 1.5);
|
||||
m_simplify_max = _p.get_uint("simplify_max", 500000);
|
||||
// --------------------------------
|
||||
m_simplify_delay = p.simplify_delay();
|
||||
|
||||
s = p.gc();
|
||||
if (s == symbol("dyn_psm"))
|
||||
|
|
@ -138,6 +143,7 @@ namespace sat {
|
|||
m_gc_small_lbd = p.gc_small_lbd();
|
||||
m_gc_k = std::min(255u, p.gc_k());
|
||||
m_gc_burst = p.gc_burst();
|
||||
m_gc_defrag = p.gc_defrag();
|
||||
|
||||
m_minimize_lemmas = p.minimize_lemmas();
|
||||
m_core_minimize = p.core_minimize();
|
||||
|
|
@ -178,8 +184,10 @@ namespace sat {
|
|||
m_pb_solver = PB_TOTALIZER;
|
||||
else if (s == symbol("solver"))
|
||||
m_pb_solver = PB_SOLVER;
|
||||
else if (s == symbol("segmented"))
|
||||
m_pb_solver = PB_SEGMENTED;
|
||||
else
|
||||
throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting");
|
||||
throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting, segmented");
|
||||
|
||||
m_card_solver = p.cardinality_solver();
|
||||
|
||||
|
|
|
|||
|
|
@ -54,7 +54,8 @@ namespace sat {
|
|||
PB_SOLVER,
|
||||
PB_CIRCUIT,
|
||||
PB_SORTING,
|
||||
PB_TOTALIZER
|
||||
PB_TOTALIZER,
|
||||
PB_SEGMENTED
|
||||
};
|
||||
|
||||
enum reward_t {
|
||||
|
|
@ -84,7 +85,9 @@ namespace sat {
|
|||
unsigned m_phase_caching_on;
|
||||
unsigned m_phase_caching_off;
|
||||
bool m_phase_sticky;
|
||||
bool m_propagate_prefetch;
|
||||
restart_strategy m_restart;
|
||||
bool m_restart_fast;
|
||||
unsigned m_restart_initial;
|
||||
double m_restart_factor; // for geometric case
|
||||
unsigned m_restart_max;
|
||||
|
|
@ -110,11 +113,13 @@ namespace sat {
|
|||
double m_lookahead_cube_psat_trigger;
|
||||
reward_t m_lookahead_reward;
|
||||
bool m_lookahead_global_autarky;
|
||||
bool m_lookahead_use_learned;
|
||||
|
||||
bool m_incremental;
|
||||
unsigned m_simplify_mult1;
|
||||
unsigned m_next_simplify1;
|
||||
double m_simplify_mult2;
|
||||
unsigned m_simplify_max;
|
||||
unsigned m_simplify_delay;
|
||||
|
||||
unsigned m_variable_decay;
|
||||
|
||||
|
|
@ -124,6 +129,8 @@ namespace sat {
|
|||
unsigned m_gc_small_lbd;
|
||||
unsigned m_gc_k;
|
||||
bool m_gc_burst;
|
||||
bool m_gc_defrag;
|
||||
|
||||
|
||||
bool m_minimize_lemmas;
|
||||
bool m_dyn_sub_res;
|
||||
|
|
|
|||
|
|
@ -42,7 +42,7 @@ namespace sat {
|
|||
for (unsigned i = 0; i < m_proof.size(); ++i) {
|
||||
clause* c = m_proof[i];
|
||||
if (c && (c->size() == 2 || m_status[i] == status::deleted || m_status[i] == status::external)) {
|
||||
s.m_cls_allocator.del_clause(c);
|
||||
s.dealloc_clause(c);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -118,7 +118,7 @@ namespace sat {
|
|||
if (st == status::learned) {
|
||||
verify(2, lits);
|
||||
}
|
||||
clause* c = s.m_cls_allocator.mk_clause(2, lits, st == status::learned);
|
||||
clause* c = s.alloc_clause(2, lits, st == status::learned);
|
||||
m_proof.push_back(c);
|
||||
m_status.push_back(st);
|
||||
unsigned idx = m_watched_clauses.size();
|
||||
|
|
@ -452,7 +452,7 @@ namespace sat {
|
|||
case 0: add(); break;
|
||||
case 1: append(lits[0], status::external); break;
|
||||
default: {
|
||||
clause* c = s.m_cls_allocator.mk_clause(lits.size(), lits.c_ptr(), true);
|
||||
clause* c = s.alloc_clause(lits.size(), lits.c_ptr(), true);
|
||||
append(*c, status::external);
|
||||
break;
|
||||
}
|
||||
|
|
@ -468,7 +468,7 @@ namespace sat {
|
|||
case 1: append(c[0], status::learned); break;
|
||||
default: {
|
||||
verify(c.size(), c.begin());
|
||||
clause* cl = s.m_cls_allocator.mk_clause(c.size(), c.c_ptr(), true);
|
||||
clause* cl = s.alloc_clause(c.size(), c.c_ptr(), true);
|
||||
append(*cl, status::external);
|
||||
break;
|
||||
}
|
||||
|
|
@ -490,7 +490,7 @@ namespace sat {
|
|||
TRACE("sat", tout << "del: " << c << "\n";);
|
||||
if (m_out) dump(c.size(), c.begin(), status::deleted);
|
||||
if (m_check) {
|
||||
clause* c1 = s.m_cls_allocator.mk_clause(c.size(), c.begin(), c.is_learned());
|
||||
clause* c1 = s.alloc_clause(c.size(), c.begin(), c.is_learned());
|
||||
append(*c1, status::deleted);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -199,7 +199,7 @@ namespace sat {
|
|||
literal r = roots[v];
|
||||
SASSERT(v != r.var());
|
||||
bool root_ok = !m_solver.is_external(v) || m_solver.set_root(l, r);
|
||||
if (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok)) {
|
||||
if (m_solver.is_assumption(v) || (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok))) {
|
||||
// cannot really eliminate v, since we have to notify extension of future assignments
|
||||
m_solver.mk_bin_clause(~l, r, false);
|
||||
m_solver.mk_bin_clause(l, ~r, false);
|
||||
|
|
|
|||
|
|
@ -101,7 +101,7 @@ namespace sat{
|
|||
pos_occs.reset();
|
||||
neg_occs.reset();
|
||||
literal_vector lits;
|
||||
add_clauses(b, lits);
|
||||
add_clauses(v, b, lits);
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
@ -157,7 +157,7 @@ namespace sat{
|
|||
return b;
|
||||
}
|
||||
|
||||
void elim_vars::add_clauses(bdd const& b, literal_vector& lits) {
|
||||
void elim_vars::add_clauses(bool_var v0, bdd const& b, literal_vector& lits) {
|
||||
if (b.is_true()) {
|
||||
// no-op
|
||||
}
|
||||
|
|
@ -167,6 +167,7 @@ namespace sat{
|
|||
if (simp.cleanup_clause(c))
|
||||
return;
|
||||
|
||||
if (v0 == 39063) IF_VERBOSE(0, verbose_stream() << "bdd: " << c << "\n");
|
||||
switch (c.size()) {
|
||||
case 0:
|
||||
s.set_conflict(justification());
|
||||
|
|
@ -184,7 +185,7 @@ namespace sat{
|
|||
s.m_stats.m_mk_ter_clause++;
|
||||
else
|
||||
s.m_stats.m_mk_clause++;
|
||||
clause* cp = s.m_cls_allocator.mk_clause(c.size(), c.c_ptr(), false);
|
||||
clause* cp = s.alloc_clause(c.size(), c.c_ptr(), false);
|
||||
s.m_clauses.push_back(cp);
|
||||
simp.m_use_list.insert(*cp);
|
||||
if (simp.m_sub_counter > 0)
|
||||
|
|
@ -198,10 +199,10 @@ namespace sat{
|
|||
else {
|
||||
unsigned v = m_vars[b.var()];
|
||||
lits.push_back(literal(v, false));
|
||||
add_clauses(b.lo(), lits);
|
||||
add_clauses(v0, b.lo(), lits);
|
||||
lits.pop_back();
|
||||
lits.push_back(literal(v, true));
|
||||
add_clauses(b.hi(), lits);
|
||||
add_clauses(v0, b.hi(), lits);
|
||||
lits.pop_back();
|
||||
}
|
||||
}
|
||||
|
|
@ -213,7 +214,7 @@ namespace sat{
|
|||
}
|
||||
if (b.is_false()) {
|
||||
if (lits.size() > 1) {
|
||||
clause* c = s.m_cls_allocator.mk_clause(lits.size(), lits.c_ptr(), false);
|
||||
clause* c = s.alloc_clause(lits.size(), lits.c_ptr(), false);
|
||||
clauses.push_back(c);
|
||||
}
|
||||
else {
|
||||
|
|
|
|||
|
|
@ -57,7 +57,7 @@ namespace sat {
|
|||
bdd make_clauses(literal lit);
|
||||
bdd mk_literal(literal l);
|
||||
void get_clauses(bdd const& b, literal_vector& lits, clause_vector& clauses, literal_vector& units);
|
||||
void add_clauses(bdd const& b, literal_vector& lits);
|
||||
void add_clauses(bool_var v, bdd const& b, literal_vector& lits);
|
||||
bool elim_var(bool_var v, bdd const& b);
|
||||
bdd elim_var(bool_var v);
|
||||
|
||||
|
|
|
|||
|
|
@ -136,9 +136,9 @@ namespace sat {
|
|||
TRACE("iff3_finder",
|
||||
tout << "visiting: " << x << "\n";
|
||||
tout << "pos:\n";
|
||||
display_watch_list(tout, s.m_cls_allocator, pos_wlist);
|
||||
s.display_watch_list(tout, pos_wlist);
|
||||
tout << "\nneg:\n";
|
||||
display_watch_list(tout, s.m_cls_allocator, neg_wlist);
|
||||
s.display_watch_list(tout, neg_wlist);
|
||||
tout << "\n--------------\n";);
|
||||
// traverse the ternary clauses x \/ l1 \/ l2
|
||||
bool_var curr_v1 = null_bool_var;
|
||||
|
|
|
|||
|
|
@ -66,7 +66,7 @@ namespace sat {
|
|||
if (c.size() == 3) {
|
||||
CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2]), tout << c << "\n";
|
||||
tout << "watch_list:\n";
|
||||
sat::display_watch_list(tout, s.m_cls_allocator, s.get_wlist(~c[0]));
|
||||
s.display_watch_list(tout, s.get_wlist(~c[0]));
|
||||
tout << "\n";);
|
||||
VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2]));
|
||||
VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2]));
|
||||
|
|
@ -164,9 +164,9 @@ namespace sat {
|
|||
tout << "was_eliminated1: " << s.was_eliminated(l.var());
|
||||
tout << " was_eliminated2: " << s.was_eliminated(w.get_literal().var());
|
||||
tout << " learned: " << w.is_learned() << "\n";
|
||||
sat::display_watch_list(tout, s.m_cls_allocator, wlist);
|
||||
s.display_watch_list(tout, wlist);
|
||||
tout << "\n";
|
||||
sat::display_watch_list(tout, s.m_cls_allocator, s.get_wlist(~(w.get_literal())));
|
||||
s.display_watch_list(tout, s.get_wlist(~(w.get_literal())));
|
||||
tout << "\n";);
|
||||
VERIFY(find_binary_watch(s.get_wlist(~(w.get_literal())), l));
|
||||
break;
|
||||
|
|
@ -176,7 +176,7 @@ namespace sat {
|
|||
VERIFY(w.get_literal1().index() < w.get_literal2().index());
|
||||
break;
|
||||
case watched::CLAUSE:
|
||||
VERIFY(!s.m_cls_allocator.get_clause(w.get_clause_offset())->was_removed());
|
||||
VERIFY(!s.get_clause(w.get_clause_offset()).was_removed());
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
|
|
|
|||
|
|
@ -79,11 +79,13 @@ namespace sat {
|
|||
void local_search::init_cur_solution() {
|
||||
for (var_info& vi : m_vars) {
|
||||
// use bias with a small probability
|
||||
if (m_rand() % 10 < 5 || m_config.phase_sticky()) {
|
||||
vi.m_value = ((unsigned)(m_rand() % 100) < vi.m_bias);
|
||||
}
|
||||
else {
|
||||
vi.m_value = (m_rand() % 2) == 0;
|
||||
if (!vi.m_unit) {
|
||||
if (m_rand() % 10 < 5 || m_config.phase_sticky()) {
|
||||
vi.m_value = ((unsigned)(m_rand() % 100) < vi.m_bias);
|
||||
}
|
||||
else {
|
||||
vi.m_value = (m_rand() % 2) == 0;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -149,7 +151,7 @@ namespace sat {
|
|||
|
||||
void local_search::reinit() {
|
||||
|
||||
IF_VERBOSE(0, verbose_stream() << "(sat-local-search reinit)\n";);
|
||||
IF_VERBOSE(1, verbose_stream() << "(sat-local-search reinit)\n";);
|
||||
if (true || !m_is_pb) {
|
||||
//
|
||||
// the following methods does NOT converge for pseudo-boolean
|
||||
|
|
@ -216,13 +218,15 @@ namespace sat {
|
|||
for (unsigned i = 0; i < m_prop_queue.size() && i < m_vars.size(); ++i) {
|
||||
literal lit2 = m_prop_queue[i];
|
||||
if (!is_true(lit2)) {
|
||||
if (is_unit(lit2)) return false;
|
||||
if (is_unit(lit2)) {
|
||||
return false;
|
||||
}
|
||||
flip_walksat(lit2.var());
|
||||
add_propagation(lit2);
|
||||
}
|
||||
}
|
||||
if (m_prop_queue.size() >= m_vars.size()) {
|
||||
IF_VERBOSE(0, verbose_stream() << "failed literal\n");
|
||||
IF_VERBOSE(0, verbose_stream() << "propagation loop\n");
|
||||
return false;
|
||||
}
|
||||
if (unit) {
|
||||
|
|
@ -328,6 +332,7 @@ namespace sat {
|
|||
return;
|
||||
}
|
||||
if (k == 1 && sz == 2) {
|
||||
// IF_VERBOSE(0, verbose_stream() << "bin: " << ~c[0] << " + " << ~c[1] << " <= 1\n");
|
||||
for (unsigned i = 0; i < 2; ++i) {
|
||||
literal t(c[i]), s(c[1-i]);
|
||||
m_vars.reserve(t.var() + 1);
|
||||
|
|
@ -750,11 +755,12 @@ namespace sat {
|
|||
IF_VERBOSE(1, verbose_stream() << "(sat.local_search :unsat)\n");
|
||||
return;
|
||||
}
|
||||
|
||||
if (is_unit(best_var)) {
|
||||
goto reflip;
|
||||
}
|
||||
flip_walksat(best_var);
|
||||
literal lit(best_var, !cur_solution(best_var));
|
||||
if (!propagate(lit)) {
|
||||
IF_VERBOSE(0, verbose_stream() << "failed literal " << lit << "\n");
|
||||
if (is_true(lit)) {
|
||||
flip_walksat(best_var);
|
||||
}
|
||||
|
|
@ -774,6 +780,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
void local_search::flip_walksat(bool_var flipvar) {
|
||||
VERIFY(!is_unit(flipvar));
|
||||
m_vars[flipvar].m_value = !cur_solution(flipvar);
|
||||
|
||||
bool flip_is_true = cur_solution(flipvar);
|
||||
|
|
|
|||
|
|
@ -1034,7 +1034,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
if (m_s.m_ext) {
|
||||
m_ext = m_s.m_ext->copy(this, learned);
|
||||
// m_ext = m_s.m_ext->copy(this, learned);
|
||||
}
|
||||
propagate();
|
||||
m_qhead = m_trail.size();
|
||||
|
|
@ -1832,7 +1832,7 @@ namespace sat {
|
|||
unsigned dl_truth = base + m_lookahead.size() * m_config.m_dl_max_iterations;
|
||||
scoped_level _sl(*this, dl_truth);
|
||||
//SASSERT(get_level(m_trail.back()) == dl_truth);
|
||||
IF_VERBOSE(2, verbose_stream() << "(sat-lookahead :double " << l << " :depth " << m_trail_lim.size() << ")\n";);
|
||||
IF_VERBOSE(3, verbose_stream() << "(sat-lookahead :double " << l << " :depth " << m_trail_lim.size() << ")\n";);
|
||||
lookahead_backtrack();
|
||||
assign(l);
|
||||
propagate();
|
||||
|
|
@ -2227,7 +2227,7 @@ namespace sat {
|
|||
void lookahead::init_search() {
|
||||
m_search_mode = lookahead_mode::searching;
|
||||
scoped_level _sl(*this, c_fixed_truth);
|
||||
init(true);
|
||||
init(m_s.m_config.m_lookahead_use_learned);
|
||||
}
|
||||
|
||||
void lookahead::checkpoint() {
|
||||
|
|
|
|||
|
|
@ -247,7 +247,7 @@ namespace sat {
|
|||
stats m_stats;
|
||||
model m_model;
|
||||
cube_state m_cube_state;
|
||||
scoped_ptr<extension> m_ext;
|
||||
//scoped_ptr<extension> m_ext;
|
||||
|
||||
// ---------------------------------------
|
||||
// truth values
|
||||
|
|
|
|||
|
|
@ -75,32 +75,42 @@ namespace sat {
|
|||
void model_converter::operator()(model & m) const {
|
||||
vector<entry>::const_iterator begin = m_entries.begin();
|
||||
vector<entry>::const_iterator it = m_entries.end();
|
||||
bool first = true;
|
||||
bool first = false; // true; // false; // // true;
|
||||
//SASSERT(!m_solver || m_solver->check_clauses(m));
|
||||
while (it != begin) {
|
||||
--it;
|
||||
SASSERT(it->get_kind() != ELIM_VAR || m[it->var()] == l_undef);
|
||||
// if it->get_kind() == BLOCK_LIT, then it might be the case that m[it->var()] != l_undef,
|
||||
bool_var v0 = it->var();
|
||||
SASSERT(it->get_kind() != ELIM_VAR || v0 == null_bool_var || m[v0] == l_undef);
|
||||
// if it->get_kind() == BCE, then it might be the case that m[v] != l_undef,
|
||||
// and the following procedure flips its value.
|
||||
bool sat = false;
|
||||
bool var_sign = false;
|
||||
unsigned index = 0;
|
||||
literal_vector clause;
|
||||
VERIFY(legal_to_flip(it->var()));
|
||||
VERIFY(v0 == null_bool_var || legal_to_flip(v0));
|
||||
for (literal l : it->m_clauses) {
|
||||
if (l == null_literal) {
|
||||
// end of clause
|
||||
elim_stack* st = it->m_elim_stack[index];
|
||||
if (!sat) {
|
||||
VERIFY(legal_to_flip(it->var()));
|
||||
m[it->var()] = var_sign ? l_false : l_true;
|
||||
if (!sat && it->get_kind() == ATE) {
|
||||
IF_VERBOSE(0, display(verbose_stream() << "violated ate\n", *it) << "\n");
|
||||
IF_VERBOSE(0, for (unsigned v = 0; v < m.size(); ++v) verbose_stream() << v << " := " << m[v] << "\n";);
|
||||
IF_VERBOSE(0, display(verbose_stream()));
|
||||
exit(0);
|
||||
first = false;
|
||||
}
|
||||
if (!sat && it->get_kind() != ATE && v0 != null_bool_var) {
|
||||
VERIFY(legal_to_flip(v0));
|
||||
m[v0] = var_sign ? l_false : l_true;
|
||||
//IF_VERBOSE(0, verbose_stream() << "assign " << v0 << " "<< m[v0] << "\n");
|
||||
}
|
||||
elim_stack* st = it->m_elim_stack[index];
|
||||
if (st) {
|
||||
process_stack(m, clause, st->stack());
|
||||
}
|
||||
sat = false;
|
||||
if (false && first && m_solver && !m_solver->check_clauses(m)) {
|
||||
display(std::cout, *it) << "\n";
|
||||
if (first && m_solver && !m_solver->check_clauses(m)) {
|
||||
IF_VERBOSE(0, display(verbose_stream() << "after processing stack\n", *it) << "\n");
|
||||
IF_VERBOSE(0, display(verbose_stream()));
|
||||
first = false;
|
||||
}
|
||||
++index;
|
||||
|
|
@ -115,18 +125,18 @@ namespace sat {
|
|||
bool_var v = l.var();
|
||||
if (v >= m.size()) std::cout << v << " model size: " << m.size() << "\n";
|
||||
VERIFY(v < m.size());
|
||||
if (v == it->var())
|
||||
if (v == v0)
|
||||
var_sign = sign;
|
||||
if (value_at(l, m) == l_true)
|
||||
sat = true;
|
||||
else if (!sat && v != it->var() && m[v] == l_undef) {
|
||||
else if (!sat && v != v0 && m[v] == l_undef) {
|
||||
VERIFY(legal_to_flip(v));
|
||||
// clause can be satisfied by assigning v.
|
||||
m[v] = sign ? l_false : l_true;
|
||||
// if (first) std::cout << "set: " << l << "\n";
|
||||
sat = true;
|
||||
if (false && first && m_solver && !m_solver->check_clauses(m)) {
|
||||
display(std::cout, *it) << "\n";;
|
||||
if (first && m_solver && !m_solver->check_clauses(m)) {
|
||||
IF_VERBOSE(0, display(verbose_stream() << "after flipping undef\n", *it) << "\n");
|
||||
first = false;
|
||||
}
|
||||
}
|
||||
|
|
@ -190,17 +200,43 @@ namespace sat {
|
|||
entry & e = m_entries.back();
|
||||
SASSERT(e.var() == v);
|
||||
SASSERT(e.get_kind() == k);
|
||||
VERIFY(legal_to_flip(v));
|
||||
VERIFY(v == null_bool_var || legal_to_flip(v));
|
||||
return e;
|
||||
}
|
||||
|
||||
void model_converter::add_ate(clause const& c) {
|
||||
if (stackv().empty()) return;
|
||||
insert(mk(ATE, null_bool_var), c);
|
||||
}
|
||||
|
||||
void model_converter::add_ate(literal_vector const& lits) {
|
||||
if (stackv().empty()) return;
|
||||
insert(mk(ATE, null_bool_var), lits);
|
||||
}
|
||||
|
||||
void model_converter::add_ate(literal l1, literal l2) {
|
||||
if (stackv().empty()) return;
|
||||
insert(mk(ATE, null_bool_var), l1, l2);
|
||||
}
|
||||
|
||||
void model_converter::add_elim_stack(entry & e) {
|
||||
e.m_elim_stack.push_back(stackv().empty() ? nullptr : alloc(elim_stack, stackv()));
|
||||
#if 0
|
||||
if (!stackv().empty() && e.get_kind() == ATE) {
|
||||
IF_VERBOSE(0, display(verbose_stream(), e) << "\n");
|
||||
}
|
||||
#endif
|
||||
for (auto const& s : stackv()) VERIFY(legal_to_flip(s.second.var()));
|
||||
stackv().reset();
|
||||
}
|
||||
|
||||
void model_converter::insert(entry & e, clause const & c) {
|
||||
SASSERT(c.contains(e.var()));
|
||||
SASSERT(m_entries.begin() <= &e);
|
||||
SASSERT(&e < m_entries.end());
|
||||
for (literal l : c) e.m_clauses.push_back(l);
|
||||
e.m_clauses.push_back(null_literal);
|
||||
e.m_elim_stack.push_back(nullptr);
|
||||
add_elim_stack(e);
|
||||
TRACE("sat_mc_bug", tout << "adding: " << c << "\n";);
|
||||
}
|
||||
|
||||
|
|
@ -211,7 +247,7 @@ namespace sat {
|
|||
e.m_clauses.push_back(l1);
|
||||
e.m_clauses.push_back(l2);
|
||||
e.m_clauses.push_back(null_literal);
|
||||
e.m_elim_stack.push_back(nullptr);
|
||||
add_elim_stack(e);
|
||||
TRACE("sat_mc_bug", tout << "adding (binary): " << l1 << " " << l2 << "\n";);
|
||||
}
|
||||
|
||||
|
|
@ -223,18 +259,17 @@ namespace sat {
|
|||
for (unsigned i = 0; i < sz; ++i)
|
||||
e.m_clauses.push_back(c[i]);
|
||||
e.m_clauses.push_back(null_literal);
|
||||
e.m_elim_stack.push_back(nullptr);
|
||||
add_elim_stack(e);
|
||||
// TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";);
|
||||
}
|
||||
|
||||
void model_converter::insert(entry & e, literal_vector const& c, elim_stackv const& elims) {
|
||||
void model_converter::insert(entry & e, literal_vector const& c) {
|
||||
SASSERT(c.contains(literal(e.var(), false)) || c.contains(literal(e.var(), true)));
|
||||
SASSERT(m_entries.begin() <= &e);
|
||||
SASSERT(&e < m_entries.end());
|
||||
for (literal l : c) e.m_clauses.push_back(l);
|
||||
e.m_clauses.push_back(null_literal);
|
||||
e.m_elim_stack.push_back(elims.empty() ? nullptr : alloc(elim_stack, elims));
|
||||
for (auto const& s : elims) VERIFY(legal_to_flip(s.second.var()));
|
||||
add_elim_stack(e);
|
||||
TRACE("sat_mc_bug", tout << "adding: " << c << "\n";);
|
||||
}
|
||||
|
||||
|
|
@ -245,7 +280,7 @@ namespace sat {
|
|||
vector<entry>::const_iterator it = m_entries.begin();
|
||||
vector<entry>::const_iterator end = m_entries.end();
|
||||
for (; it != end; ++it) {
|
||||
SASSERT(it->var() < num_vars);
|
||||
SASSERT(it->var() == null_bool_var || it->var() < num_vars);
|
||||
if (it->get_kind() == ELIM_VAR) {
|
||||
svector<entry>::const_iterator it2 = it;
|
||||
it2++;
|
||||
|
|
@ -275,7 +310,8 @@ namespace sat {
|
|||
}
|
||||
|
||||
std::ostream& model_converter::display(std::ostream& out, entry const& entry) const {
|
||||
out << " (" << entry.get_kind() << " " << entry.var();
|
||||
out << " (" << entry.get_kind() << " ";
|
||||
if (entry.var() != null_bool_var) out << entry.var();
|
||||
bool start = true;
|
||||
unsigned index = 0;
|
||||
for (literal l : entry.m_clauses) {
|
||||
|
|
@ -305,7 +341,7 @@ namespace sat {
|
|||
}
|
||||
out << ")";
|
||||
for (literal l : entry.m_clauses) {
|
||||
if (l != null_literal) {
|
||||
if (l != null_literal && l.var() != null_bool_var) {
|
||||
if (false && m_solver && m_solver->was_eliminated(l.var())) out << "\neliminated: " << l;
|
||||
}
|
||||
}
|
||||
|
|
@ -332,7 +368,7 @@ namespace sat {
|
|||
for (entry const& e : m_entries) {
|
||||
for (literal l : e.m_clauses) {
|
||||
if (l != null_literal) {
|
||||
if (l.var() > result)
|
||||
if (l.var() != null_bool_var && l.var() > result)
|
||||
result = l.var();
|
||||
}
|
||||
}
|
||||
|
|
@ -371,9 +407,11 @@ namespace sat {
|
|||
update_stack.push_back(null_literal);
|
||||
}
|
||||
}
|
||||
swap(e.var(), clause.size(), clause);
|
||||
update_stack.append(clause);
|
||||
update_stack.push_back(null_literal);
|
||||
if (e.var() != null_bool_var) {
|
||||
swap(e.var(), clause.size(), clause);
|
||||
update_stack.append(clause);
|
||||
update_stack.push_back(null_literal);
|
||||
}
|
||||
clause.reset();
|
||||
}
|
||||
else {
|
||||
|
|
|
|||
|
|
@ -66,11 +66,11 @@ namespace sat {
|
|||
unsigned ref_count() const { return m_refcount; }
|
||||
};
|
||||
|
||||
enum kind { ELIM_VAR = 0, BLOCK_LIT, CCE, ACCE };
|
||||
enum kind { ELIM_VAR = 0, BCE, CCE, ACCE, ABCE, ATE };
|
||||
class entry {
|
||||
friend class model_converter;
|
||||
unsigned m_var:30;
|
||||
unsigned m_kind:2;
|
||||
bool_var m_var;
|
||||
kind m_kind;
|
||||
literal_vector m_clauses; // the different clauses are separated by null_literal
|
||||
sref_vector<elim_stack> m_elim_stack;
|
||||
entry(kind k, bool_var v): m_var(v), m_kind(k) {}
|
||||
|
|
@ -82,11 +82,12 @@ namespace sat {
|
|||
m_elim_stack.append(src.m_elim_stack);
|
||||
}
|
||||
bool_var var() const { return m_var; }
|
||||
kind get_kind() const { return static_cast<kind>(m_kind); }
|
||||
kind get_kind() const { return m_kind; }
|
||||
};
|
||||
private:
|
||||
vector<entry> m_entries;
|
||||
solver const* m_solver;
|
||||
elim_stackv m_elim_stack;
|
||||
|
||||
void process_stack(model & m, literal_vector const& clause, elim_stackv const& stack) const;
|
||||
|
||||
|
|
@ -96,6 +97,8 @@ namespace sat {
|
|||
|
||||
void swap(bool_var v, unsigned sz, literal_vector& clause);
|
||||
|
||||
void add_elim_stack(entry & e);
|
||||
|
||||
public:
|
||||
model_converter();
|
||||
~model_converter();
|
||||
|
|
@ -103,11 +106,17 @@ namespace sat {
|
|||
void operator()(model & m) const;
|
||||
model_converter& operator=(model_converter const& other);
|
||||
|
||||
elim_stackv& stackv() { return m_elim_stack; }
|
||||
|
||||
entry & mk(kind k, bool_var v);
|
||||
void insert(entry & e, clause const & c);
|
||||
void insert(entry & e, literal l1, literal l2);
|
||||
void insert(entry & e, clause_wrapper const & c);
|
||||
void insert(entry & c, literal_vector const& covered_clause, elim_stackv const& elim_stack);
|
||||
void insert(entry & c, literal_vector const& covered_clause);
|
||||
|
||||
void add_ate(literal_vector const& lits);
|
||||
void add_ate(literal l1, literal l2);
|
||||
void add_ate(clause const& c);
|
||||
|
||||
bool empty() const { return m_entries.empty(); }
|
||||
|
||||
|
|
@ -137,9 +146,11 @@ namespace sat {
|
|||
inline std::ostream& operator<<(std::ostream& out, model_converter::kind k) {
|
||||
switch (k) {
|
||||
case model_converter::ELIM_VAR: out << "elim"; break;
|
||||
case model_converter::BLOCK_LIT: out << "blocked"; break;
|
||||
case model_converter::BCE: out << "bce"; break;
|
||||
case model_converter::CCE: out << "cce"; break;
|
||||
case model_converter::ACCE: out << "acce"; break;
|
||||
case model_converter::ABCE: out << "abce"; break;
|
||||
case model_converter::ATE: out << "ate"; break;
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -6,11 +6,13 @@ def_module_params('sat',
|
|||
('phase.caching.on', UINT, 400, 'phase caching on period (in number of conflicts)'),
|
||||
('phase.caching.off', UINT, 100, 'phase caching off period (in number of conflicts)'),
|
||||
('phase.sticky', BOOL, False, 'use sticky phase caching for local search'),
|
||||
('propagate.prefetch', BOOL, True, 'prefetch watch lists for assigned literals'),
|
||||
('restart', SYMBOL, 'luby', 'restart strategy: luby or geometric'),
|
||||
('restart.initial', UINT, 100, 'initial restart (number of conflicts)'),
|
||||
('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
|
||||
('restart.fast', BOOL, False, 'use fast restart strategy.'),
|
||||
('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
|
||||
('variable_decay', UINT, 120, 'multiplier (divided by 100) for the VSIDS activity increement'),
|
||||
('variable_decay', UINT, 110, 'multiplier (divided by 100) for the VSIDS activity increement'),
|
||||
('inprocess.max', UINT, UINT_MAX, 'maximal number of inprocessing passes'),
|
||||
('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'),
|
||||
('branching.anti_exploration', BOOL, False, 'apply anti-exploration heuristic for branch selection'),
|
||||
|
|
@ -24,6 +26,8 @@ def_module_params('sat',
|
|||
('gc.small_lbd', UINT, 3, 'learned clauses with small LBD are never deleted (only used in dyn_psm)'),
|
||||
('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'),
|
||||
('gc.burst', BOOL, True, 'perform eager garbage collection during initialization'),
|
||||
('gc.defrag', BOOL, True, 'defragment clauses when garbage collecting'),
|
||||
('simplify.delay', UINT, 0, 'set initial delay of simplification by a conflict count'),
|
||||
('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
|
||||
('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
|
||||
('core.minimize', BOOL, False, 'minimize computed core'),
|
||||
|
|
@ -42,9 +46,9 @@ def_module_params('sat',
|
|||
('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'),
|
||||
('unit_walk', BOOL, False, 'use unit-walk search instead of CDCL'),
|
||||
('unit_walk_threads', UINT, 0, 'number of unit-walk search threads to find satisfiable solution'),
|
||||
('lookahead.cube.cutoff', SYMBOL, 'adaptive_freevars', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'),
|
||||
('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'),
|
||||
('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat'),
|
||||
('lookahead.cube.depth', UINT, 10, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'),
|
||||
('lookahead.cube.depth', UINT, 1, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'),
|
||||
('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is freevars'),
|
||||
('lookahead.cube.psat.var_exp', DOUBLE, 1, 'free variable exponent for PSAT cutoff'),
|
||||
('lookahead.cube.psat.clause_base', DOUBLE, 2, 'clause base for PSAT cutoff'),
|
||||
|
|
@ -52,6 +56,7 @@ def_module_params('sat',
|
|||
('lookahead_search', BOOL, False, 'use lookahead solver'),
|
||||
('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
|
||||
('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
|
||||
('lookahead.use_learned', BOOL, False, 'use learned clauses when selecting lookahead literal'),
|
||||
('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'),
|
||||
('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'),
|
||||
('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu')))
|
||||
|
|
|
|||
|
|
@ -100,7 +100,7 @@ namespace sat {
|
|||
!m_learned_in_use_lists && m_num_calls >= m_bce_delay && single_threaded();
|
||||
}
|
||||
|
||||
bool simplifier::ate_enabled() const { return m_ate; }
|
||||
bool simplifier::ate_enabled() const { return m_num_calls >= m_bce_delay && m_ate; }
|
||||
bool simplifier::bce_enabled() const { return bce_enabled_base() && (m_bce || m_bce_at == m_num_calls || m_acce || m_abce || m_cce); }
|
||||
bool simplifier::acce_enabled() const { return bce_enabled_base() && m_acce; }
|
||||
bool simplifier::cce_enabled() const { return bce_enabled_base() && (m_cce || m_acce); }
|
||||
|
|
@ -939,6 +939,24 @@ namespace sat {
|
|||
bool operator==(clause_ante const& a) const {
|
||||
return a.m_lit1 == m_lit1 && a.m_lit2 == m_lit2 && a.m_clause == m_clause;
|
||||
}
|
||||
std::ostream& display(std::ostream& out, literal lit) const {
|
||||
if (cls()) {
|
||||
out << *cls() << " ";
|
||||
}
|
||||
else {
|
||||
out << "(" << ~lit;
|
||||
}
|
||||
if (lit1() != null_literal) {
|
||||
out << " " << lit1();
|
||||
}
|
||||
if (lit2() != null_literal) {
|
||||
out << " " << lit2();
|
||||
}
|
||||
if (!cls()) out << ")";
|
||||
if (from_ri()) out << "ri";
|
||||
out << "\n";
|
||||
return out;
|
||||
}
|
||||
};
|
||||
|
||||
class queue {
|
||||
|
|
@ -965,7 +983,7 @@ namespace sat {
|
|||
|
||||
simplifier & s;
|
||||
int m_counter;
|
||||
model_converter & mc;
|
||||
model_converter & m_mc;
|
||||
queue m_queue;
|
||||
|
||||
literal_vector m_covered_clause; // covered clause
|
||||
|
|
@ -974,7 +992,6 @@ namespace sat {
|
|||
literal_vector m_tautology; // literals that are used in blocking tautology
|
||||
literal_vector m_new_intersection;
|
||||
svector<bool> m_in_intersection;
|
||||
sat::model_converter::elim_stackv m_elim_stack;
|
||||
unsigned m_ala_qhead;
|
||||
clause_wrapper m_clause;
|
||||
|
||||
|
|
@ -982,7 +999,7 @@ namespace sat {
|
|||
vector<watch_list> & wlist):
|
||||
s(_s),
|
||||
m_counter(limit),
|
||||
mc(_mc),
|
||||
m_mc(_mc),
|
||||
m_queue(l, wlist),
|
||||
m_clause(null_literal, null_literal) {
|
||||
m_in_intersection.resize(s.s.num_vars() * 2, false);
|
||||
|
|
@ -994,7 +1011,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
bool process_var(bool_var v) {
|
||||
return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v);
|
||||
return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v) && s.value(v) == l_undef;
|
||||
}
|
||||
|
||||
enum elim_type {
|
||||
|
|
@ -1052,10 +1069,11 @@ namespace sat {
|
|||
// Find literals that are in the intersection of all resolvents with l.
|
||||
//
|
||||
bool resolution_intersection(literal l, bool adding) {
|
||||
unsigned tsz = m_tautology.size();
|
||||
reset_intersection();
|
||||
m_tautology.reset();
|
||||
if (!process_var(l.var())) return false;
|
||||
bool first = true;
|
||||
VERIFY(s.value(l) == l_undef);
|
||||
for (watched & w : s.get_wlist(l)) {
|
||||
// when adding a blocked clause, then all non-learned clauses have to be considered for the
|
||||
// resolution intersection.
|
||||
|
|
@ -1068,6 +1086,7 @@ namespace sat {
|
|||
}
|
||||
if (!first || s.is_marked(lit)) {
|
||||
reset_intersection();
|
||||
m_tautology.shrink(tsz);
|
||||
return false; // intersection is empty or does not add anything new.
|
||||
}
|
||||
first = false;
|
||||
|
|
@ -1104,22 +1123,31 @@ namespace sat {
|
|||
for (literal lit : m_new_intersection)
|
||||
add_intersection(lit);
|
||||
}
|
||||
if (m_intersection.empty())
|
||||
if (m_intersection.empty()) {
|
||||
m_tautology.shrink(tsz);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
// remove tautology literals if literal has no resolution intersection
|
||||
if (m_intersection.empty() && !first) {
|
||||
m_tautology.shrink(tsz);
|
||||
}
|
||||
// if (first) IF_VERBOSE(0, verbose_stream() << "taut: " << m_tautology << "\n";);
|
||||
return first;
|
||||
}
|
||||
|
||||
bool check_abce_tautology(literal l) {
|
||||
m_tautology.reset();
|
||||
unsigned tsz = m_tautology.size();
|
||||
if (!process_var(l.var())) return false;
|
||||
for (watched & w : s.get_wlist(l)) {
|
||||
if (w.is_binary_non_learned_clause()) {
|
||||
literal lit = w.get_literal();
|
||||
VERIFY(lit != ~l);
|
||||
if (!s.is_marked(~lit)) return false;
|
||||
if (!s.is_marked(~lit)) {
|
||||
m_tautology.shrink(tsz);
|
||||
return false;
|
||||
}
|
||||
m_tautology.push_back(~lit);
|
||||
}
|
||||
}
|
||||
|
|
@ -1135,7 +1163,10 @@ namespace sat {
|
|||
break;
|
||||
}
|
||||
}
|
||||
if (!tautology) return false;
|
||||
if (!tautology) {
|
||||
m_tautology.shrink(tsz);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
|
@ -1154,10 +1185,15 @@ namespace sat {
|
|||
\brief idx is the index of the blocked literal.
|
||||
m_tautology contains literals that were used to establish that the current members of m_covered_clause is blocked.
|
||||
This routine removes literals that were not relevant to establishing it was blocked.
|
||||
|
||||
It has a bug: literals that are used to prune tautologies during resolution intersection should be included
|
||||
in the dependencies. They may get used in some RI prunings and then they have to be included to avoid flipping
|
||||
RI literals.
|
||||
*/
|
||||
void minimize_covered_clause(unsigned idx) {
|
||||
// IF_VERBOSE(0, verbose_stream() << "minimize: " << m_covered_clause
|
||||
// << " @ " << idx << "\n" << "tautology: " << m_tautology << "\n";);
|
||||
literal _blocked = m_covered_clause[idx];
|
||||
for (literal l : m_tautology) VERIFY(s.is_marked(l));
|
||||
for (literal l : m_covered_clause) s.unmark_visited(l);
|
||||
for (literal l : m_tautology) s.mark_visited(l);
|
||||
|
|
@ -1167,8 +1203,18 @@ namespace sat {
|
|||
if (m_covered_antecedent[i] == clause_ante()) s.mark_visited(lit);
|
||||
if (s.is_marked(lit)) idx = i;
|
||||
}
|
||||
if (false && _blocked.var() == 8074) {
|
||||
IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n";
|
||||
verbose_stream() << "tautology: " << m_tautology << "\n";
|
||||
verbose_stream() << "index: " << idx << "\n";
|
||||
for (unsigned i = idx; i > 0; --i) {
|
||||
m_covered_antecedent[i].display(verbose_stream(), m_covered_clause[i]);
|
||||
});
|
||||
}
|
||||
for (unsigned i = idx; i > 0; --i) {
|
||||
literal lit = m_covered_clause[i];
|
||||
//s.mark_visited(lit);
|
||||
//continue;
|
||||
if (!s.is_marked(lit)) continue;
|
||||
clause_ante const& ante = m_covered_antecedent[i];
|
||||
if (ante.cls()) {
|
||||
|
|
@ -1195,16 +1241,22 @@ namespace sat {
|
|||
clause_ante const& ante = m_covered_antecedent[i];
|
||||
if (ante.from_ri() && blocked != ante.lit1()) {
|
||||
blocked = ante.lit1();
|
||||
m_elim_stack.push_back(std::make_pair(j, blocked));
|
||||
VERIFY(s.value(blocked) == l_undef);
|
||||
m_mc.stackv().push_back(std::make_pair(j, blocked));
|
||||
}
|
||||
m_covered_clause[j++] = lit;
|
||||
s.unmark_visited(lit);
|
||||
}
|
||||
}
|
||||
for (literal l : m_covered_clause) VERIFY(!s.is_marked(l));
|
||||
for (bool_var v = 0; v < s.s.num_vars(); ++v) VERIFY(!s.is_marked(literal(v, true)) && !s.is_marked(literal(v, false)));
|
||||
|
||||
// unsigned sz0 = m_covered_clause.size();
|
||||
m_covered_clause.resize(j);
|
||||
VERIFY(j >= m_clause.size());
|
||||
if (false && _blocked.var() == 16774) {
|
||||
IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n");
|
||||
}
|
||||
// IF_VERBOSE(0, verbose_stream() << "reduced from size " << sz0 << " to " << m_covered_clause << "\n" << m_clause << "\n";);
|
||||
}
|
||||
|
||||
|
|
@ -1233,6 +1285,7 @@ namespace sat {
|
|||
return true;
|
||||
}
|
||||
if (!s.is_marked(~lit)) {
|
||||
// if (m_covered_clause[0].var() == 10219) IF_VERBOSE(0, verbose_stream() << "ala: " << l << " " << lit << "\n");
|
||||
m_covered_clause.push_back(~lit);
|
||||
m_covered_antecedent.push_back(clause_ante(l, false));
|
||||
s.mark_visited(~lit);
|
||||
|
|
@ -1262,6 +1315,7 @@ namespace sat {
|
|||
if (lit1 == null_literal) {
|
||||
return true;
|
||||
}
|
||||
// if (m_covered_clause[0].var() == 10219) IF_VERBOSE(0, verbose_stream() << "ala: " << c << " " << lit1 << "\n");
|
||||
m_covered_clause.push_back(~lit1);
|
||||
m_covered_antecedent.push_back(clause_ante(c));
|
||||
s.mark_visited(~lit1);
|
||||
|
|
@ -1282,7 +1336,7 @@ namespace sat {
|
|||
for (unsigned i = 0; i < m_covered_clause.size(); ++i) {
|
||||
literal lit = m_covered_clause[i];
|
||||
if (resolution_intersection(lit, false)) {
|
||||
blocked = m_covered_clause[i];
|
||||
blocked = m_covered_clause[i];
|
||||
minimize_covered_clause(i);
|
||||
return true;
|
||||
}
|
||||
|
|
@ -1302,13 +1356,18 @@ namespace sat {
|
|||
return sz0 * 400 < m_covered_clause.size();
|
||||
}
|
||||
|
||||
void reset_mark() {
|
||||
for (literal l : m_covered_clause) s.unmark_visited(l);
|
||||
}
|
||||
|
||||
template<elim_type et>
|
||||
elim_type cce(literal& blocked, model_converter::kind& k) {
|
||||
bool is_tautology = false, first = true;
|
||||
bool first = true;
|
||||
unsigned sz = 0, sz0 = m_covered_clause.size();
|
||||
for (literal l : m_covered_clause) s.mark_visited(l);
|
||||
shuffle<literal>(m_covered_clause.size(), m_covered_clause.c_ptr(), s.s.m_rand);
|
||||
m_elim_stack.reset();
|
||||
m_tautology.reset();
|
||||
m_mc.stackv().reset();
|
||||
m_ala_qhead = 0;
|
||||
|
||||
switch (et) {
|
||||
|
|
@ -1319,7 +1378,7 @@ namespace sat {
|
|||
k = model_converter::ACCE;
|
||||
break;
|
||||
default:
|
||||
k = model_converter::BLOCK_LIT;
|
||||
k = model_converter::BCE;
|
||||
break;
|
||||
}
|
||||
|
||||
|
|
@ -1331,48 +1390,76 @@ namespace sat {
|
|||
* and then check if any of the first sz0 literals are blocked.
|
||||
*/
|
||||
|
||||
while (!is_tautology && m_covered_clause.size() > sz && !above_threshold(sz0)) {
|
||||
SASSERT(!is_tautology);
|
||||
if (et == ate_t) {
|
||||
bool ala = add_ala();
|
||||
reset_mark();
|
||||
m_covered_clause.shrink(sz0);
|
||||
return ala ? ate_t : no_t;
|
||||
}
|
||||
|
||||
if ((et == abce_t || et == acce_t || et == ate_t) && add_ala()) {
|
||||
for (literal l : m_covered_clause) s.unmark_visited(l);
|
||||
while (m_covered_clause.size() > sz && !above_threshold(sz0)) {
|
||||
|
||||
if ((et == abce_t || et == acce_t) && add_ala()) {
|
||||
reset_mark();
|
||||
if (first) {
|
||||
m_covered_clause.shrink(sz0);
|
||||
}
|
||||
else {
|
||||
/*
|
||||
* tautology depends on resolution intersection.
|
||||
* literals used for resolution intersection may have to be flipped.
|
||||
*/
|
||||
for (literal l : m_covered_clause) {
|
||||
m_tautology.push_back(l);
|
||||
s.mark_visited(l);
|
||||
}
|
||||
minimize_covered_clause(m_covered_clause.size()-1);
|
||||
}
|
||||
return ate_t;
|
||||
}
|
||||
|
||||
if (et == ate_t) {
|
||||
for (literal l : m_covered_clause) s.unmark_visited(l);
|
||||
return no_t;
|
||||
}
|
||||
|
||||
if (first) {
|
||||
for (unsigned i = 0; i < sz0; ++i) {
|
||||
if (check_abce_tautology(m_covered_clause[i])) {
|
||||
blocked = m_covered_clause[i];
|
||||
is_tautology = true;
|
||||
break;
|
||||
reset_mark();
|
||||
#if 0
|
||||
if (sz0 == 3 && blocked.var() == 10219) {
|
||||
IF_VERBOSE(0, verbose_stream() << "abce: " << m_covered_clause << "\n";
|
||||
for (literal l : m_covered_clause) verbose_stream() << s.value(l) << "\n";
|
||||
);
|
||||
literal l = blocked;
|
||||
clause_use_list & neg_occs = s.m_use_list.get(~l);
|
||||
for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) {
|
||||
clause & c = it.curr();
|
||||
IF_VERBOSE(0, verbose_stream() << c << "\n");
|
||||
}
|
||||
}
|
||||
#endif
|
||||
m_covered_clause.shrink(sz0);
|
||||
if (et == bce_t) return bce_t;
|
||||
k = model_converter::ABCE;
|
||||
return abce_t;
|
||||
}
|
||||
}
|
||||
first = false;
|
||||
}
|
||||
first = false;
|
||||
|
||||
if (is_tautology || et == abce_t || et == bce_t) {
|
||||
for (literal l : m_covered_clause) s.unmark_visited(l);
|
||||
m_covered_clause.shrink(sz0);
|
||||
if (!is_tautology) return no_t;
|
||||
if (et == bce_t) return bce_t;
|
||||
return abce_t;
|
||||
if (et == abce_t || et == bce_t) {
|
||||
break;
|
||||
}
|
||||
|
||||
/*
|
||||
* Add resolution intersection while checking if the clause becomes a tautology.
|
||||
*/
|
||||
sz = m_covered_clause.size();
|
||||
if (et == cce_t || et == acce_t) {
|
||||
is_tautology = add_cla(blocked);
|
||||
if ((et == cce_t || et == acce_t) && add_cla(blocked)) {
|
||||
reset_mark();
|
||||
return et;
|
||||
}
|
||||
}
|
||||
for (literal l : m_covered_clause) s.unmark_visited(l);
|
||||
return is_tautology ? et : no_t;
|
||||
reset_mark();
|
||||
return no_t;
|
||||
}
|
||||
|
||||
// perform covered clause elimination.
|
||||
|
|
@ -1433,13 +1520,14 @@ namespace sat {
|
|||
case ate_t:
|
||||
w.set_learned(true);
|
||||
s.s.set_learned1(l2, l, true);
|
||||
m_mc.add_ate(m_covered_clause);
|
||||
break;
|
||||
case no_t:
|
||||
break;
|
||||
default:
|
||||
block_covered_binary(w, l, blocked, k);
|
||||
w.set_learned(true);
|
||||
s.s.set_learned1(l2, l, true);
|
||||
block_covered_binary(w, l, blocked, k);
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
|
@ -1457,7 +1545,8 @@ namespace sat {
|
|||
inc_bc(r);
|
||||
switch (r) {
|
||||
case ate_t:
|
||||
s.set_learned(c);
|
||||
m_mc.add_ate(m_covered_clause);
|
||||
s.set_learned(c);
|
||||
break;
|
||||
case no_t:
|
||||
break;
|
||||
|
|
@ -1488,24 +1577,33 @@ namespace sat {
|
|||
}
|
||||
|
||||
void block_covered_clause(clause& c, literal l, model_converter::kind k) {
|
||||
if (false) {
|
||||
IF_VERBOSE(0, verbose_stream() << "blocked: " << l << " @ " << c << " :covered " << m_covered_clause << "\n";
|
||||
s.m_use_list.display(verbose_stream() << "use " << l << ":", l);
|
||||
s.m_use_list.display(verbose_stream() << "use " << ~l << ":", ~l);
|
||||
s.s.display_watch_list(verbose_stream() << ~l << ": ", s.get_wlist(l)) << "\n";
|
||||
s.s.display_watch_list(verbose_stream() << l << ": ", s.get_wlist(~l)) << "\n";
|
||||
);
|
||||
|
||||
}
|
||||
TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
|
||||
SASSERT(!s.is_external(l));
|
||||
model_converter::entry& new_entry = mc.mk(k, l.var());
|
||||
model_converter::entry& new_entry = m_mc.mk(k, l.var());
|
||||
for (literal lit : c) {
|
||||
if (lit != l && process_var(lit.var())) {
|
||||
m_queue.decreased(~lit);
|
||||
}
|
||||
}
|
||||
mc.insert(new_entry, m_covered_clause, m_elim_stack);
|
||||
m_mc.insert(new_entry, m_covered_clause);
|
||||
}
|
||||
|
||||
void block_covered_binary(watched const& w, literal l1, literal blocked, model_converter::kind k) {
|
||||
SASSERT(!s.is_external(blocked));
|
||||
model_converter::entry& new_entry = mc.mk(k, blocked.var());
|
||||
model_converter::entry& new_entry = m_mc.mk(k, blocked.var());
|
||||
literal l2 = w.get_literal();
|
||||
TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l1 << "\n";);
|
||||
s.set_learned(l1, l2);
|
||||
mc.insert(new_entry, m_covered_clause, m_elim_stack);
|
||||
m_mc.insert(new_entry, m_covered_clause);
|
||||
m_queue.decreased(~l2);
|
||||
}
|
||||
|
||||
|
|
@ -1526,18 +1624,15 @@ namespace sat {
|
|||
Then the following binary clause is blocked: l \/ ~l'
|
||||
*/
|
||||
void bca(literal l) {
|
||||
m_tautology.reset();
|
||||
if (resolution_intersection(l, true)) {
|
||||
// this literal is pure.
|
||||
return;
|
||||
}
|
||||
for (literal l2 : m_intersection) {
|
||||
l2.neg();
|
||||
watched* w = find_binary_watch(s.get_wlist(~l), l2);
|
||||
watched* w = find_binary_watch(s.get_wlist(~l), ~l2);
|
||||
if (!w) {
|
||||
IF_VERBOSE(100, verbose_stream() << "bca " << l << " " << l2 << "\n";);
|
||||
s.get_wlist(~l).push_back(watched(l2, true));
|
||||
VERIFY(!find_binary_watch(s.get_wlist(~l2), l));
|
||||
s.get_wlist(~l2).push_back(watched(l, true));
|
||||
s.s.mk_bin_clause(l, ~l2, true);
|
||||
++s.m_num_bca;
|
||||
}
|
||||
}
|
||||
|
|
@ -1743,13 +1838,19 @@ namespace sat {
|
|||
}
|
||||
|
||||
void simplifier::save_clauses(model_converter::entry & mc_entry, clause_wrapper_vector const & cs) {
|
||||
model_converter & mc = s.m_mc;
|
||||
for (auto & e : cs) {
|
||||
mc.insert(mc_entry, e);
|
||||
s.m_mc.insert(mc_entry, e);
|
||||
}
|
||||
}
|
||||
|
||||
void simplifier::add_non_learned_binary_clause(literal l1, literal l2) {
|
||||
#if 0
|
||||
if ((l1.var() == 2039 || l2.var() == 2039) &&
|
||||
(l1.var() == 27042 || l2.var() == 27042)) {
|
||||
IF_VERBOSE(1, verbose_stream() << "add_bin: " << l1 << " " << l2 << "\n");
|
||||
}
|
||||
#endif
|
||||
#if 0
|
||||
watched* w;
|
||||
watch_list & wlist1 = get_wlist(~l1);
|
||||
watch_list & wlist2 = get_wlist(~l2);
|
||||
|
|
@ -1770,6 +1871,9 @@ namespace sat {
|
|||
else {
|
||||
wlist2.push_back(watched(l1, false));
|
||||
}
|
||||
#else
|
||||
s.mk_bin_clause(l1, l2, false);
|
||||
#endif
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -1786,6 +1890,11 @@ namespace sat {
|
|||
watch_list::iterator end2 = wlist2.end();
|
||||
for (; it2 != end2; ++it2) {
|
||||
if (it2->is_binary_clause() && it2->get_literal() == l) {
|
||||
if ((l.var() == 2039 || l2.var() == 2039) &&
|
||||
(l.var() == 27042 || l2.var() == 27042)) {
|
||||
IF_VERBOSE(1, verbose_stream() << "remove_bin: " << l << " " << l2 << "\n");
|
||||
}
|
||||
|
||||
TRACE("bin_clause_bug", tout << "removing: " << l << " " << it2->get_literal() << "\n";);
|
||||
m_sub_bin_todo.erase(bin_clause(l2, l, it2->is_learned()));
|
||||
continue;
|
||||
|
|
@ -1886,6 +1995,13 @@ namespace sat {
|
|||
|
||||
m_elim_counter -= num_pos * num_neg + before_lits;
|
||||
|
||||
if (false) {
|
||||
literal l(v, false);
|
||||
IF_VERBOSE(0,
|
||||
verbose_stream() << "elim: " << l << "\n";
|
||||
s.display_watch_list(verbose_stream() << ~l << ": ", get_wlist(l)) << "\n";
|
||||
s.display_watch_list(verbose_stream() << l << ": ", get_wlist(~l)) << "\n";);
|
||||
}
|
||||
// eliminate variable
|
||||
++s.m_stats.m_elim_var_res;
|
||||
VERIFY(!is_external(v));
|
||||
|
|
@ -1907,6 +2023,7 @@ namespace sat {
|
|||
m_new_cls.reset();
|
||||
if (!resolve(c1, c2, pos_l, m_new_cls))
|
||||
continue;
|
||||
if (false && v == 27041) IF_VERBOSE(0, verbose_stream() << "elim: " << c1 << " + " << c2 << " -> " << m_new_cls << "\n");
|
||||
TRACE("resolution_new_cls", tout << c1 << "\n" << c2 << "\n-->\n" << m_new_cls << "\n";);
|
||||
if (cleanup_clause(m_new_cls))
|
||||
continue; // clause is already satisfied.
|
||||
|
|
@ -1927,7 +2044,7 @@ namespace sat {
|
|||
s.m_stats.m_mk_ter_clause++;
|
||||
else
|
||||
s.m_stats.m_mk_clause++;
|
||||
clause * new_c = s.m_cls_allocator.mk_clause(m_new_cls.size(), m_new_cls.c_ptr(), false);
|
||||
clause * new_c = s.alloc_clause(m_new_cls.size(), m_new_cls.c_ptr(), false);
|
||||
|
||||
if (s.m_config.m_drat) s.m_drat.add(*new_c, true);
|
||||
s.m_clauses.push_back(new_c);
|
||||
|
|
@ -1997,7 +2114,7 @@ namespace sat {
|
|||
sat_simplifier_params p(_p);
|
||||
m_cce = p.cce();
|
||||
m_acce = p.acce();
|
||||
m_bca = p.bca();
|
||||
m_bca = false && p.bca(); // disabled
|
||||
m_abce = p.abce();
|
||||
m_ate = p.ate();
|
||||
m_bce_delay = p.bce_delay();
|
||||
|
|
@ -2018,7 +2135,7 @@ namespace sat {
|
|||
m_subsumption = p.subsumption();
|
||||
m_subsumption_limit = p.subsumption_limit();
|
||||
m_elim_vars = p.elim_vars();
|
||||
m_elim_vars_bdd = p.elim_vars_bdd();
|
||||
m_elim_vars_bdd = false && p.elim_vars_bdd(); // buggy?
|
||||
m_elim_vars_bdd_delay = p.elim_vars_bdd_delay();
|
||||
m_incremental_mode = s.get_config().m_incremental && !p.override_incremental();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -47,6 +47,7 @@ namespace sat {
|
|||
clause_use_list & get(literal l) { return m_use_list[l.index()]; }
|
||||
clause_use_list const & get(literal l) const { return m_use_list[l.index()]; }
|
||||
void finalize() { m_use_list.finalize(); }
|
||||
std::ostream& display(std::ostream& out, literal l) const { return m_use_list[l.index()].display(out); }
|
||||
};
|
||||
|
||||
class simplifier {
|
||||
|
|
|
|||
|
|
@ -37,6 +37,7 @@ namespace sat {
|
|||
m_checkpoint_enabled(true),
|
||||
m_config(p),
|
||||
m_par(nullptr),
|
||||
m_cls_allocator_idx(false),
|
||||
m_par_syncing_clauses(false),
|
||||
m_par_id(0),
|
||||
m_cleaner(*this),
|
||||
|
|
@ -78,7 +79,7 @@ namespace sat {
|
|||
|
||||
void solver::del_clauses(clause_vector& clauses) {
|
||||
for (clause * cp : clauses)
|
||||
m_cls_allocator.del_clause(cp);
|
||||
dealloc_clause(cp);
|
||||
clauses.reset();
|
||||
++m_stats.m_non_learned_generation;
|
||||
}
|
||||
|
|
@ -298,7 +299,7 @@ namespace sat {
|
|||
if (m_config.m_drat && !m_drat.is_cleaned(c)) {
|
||||
m_drat.del(c);
|
||||
}
|
||||
m_cls_allocator.del_clause(&c);
|
||||
dealloc_clause(&c);
|
||||
m_stats.m_del_clause++;
|
||||
}
|
||||
|
||||
|
|
@ -333,6 +334,12 @@ namespace sat {
|
|||
}
|
||||
|
||||
void solver::mk_bin_clause(literal l1, literal l2, bool learned) {
|
||||
#if 0
|
||||
if ((l1.var() == 2039 || l2.var() == 2039) &&
|
||||
(l1.var() == 27042 || l2.var() == 27042)) {
|
||||
IF_VERBOSE(1, verbose_stream() << "mk_bin: " << l1 << " " << l2 << " " << learned << "\n");
|
||||
}
|
||||
#endif
|
||||
if (find_binary_watch(get_wlist(~l1), ~l2)) {
|
||||
assign(l1, justification());
|
||||
return;
|
||||
|
|
@ -345,13 +352,13 @@ namespace sat {
|
|||
if (w0) {
|
||||
if (w0->is_learned() && !learned) {
|
||||
w0->set_learned(false);
|
||||
}
|
||||
w0 = find_binary_watch(get_wlist(~l2), l1);
|
||||
}
|
||||
if (w0) {
|
||||
if (w0->is_learned() && !learned) {
|
||||
w0->set_learned(false);
|
||||
}
|
||||
}
|
||||
else {
|
||||
return;
|
||||
}
|
||||
w0 = find_binary_watch(get_wlist(~l2), l1);
|
||||
VERIFY(w0);
|
||||
w0->set_learned(false);
|
||||
return;
|
||||
}
|
||||
if (m_config.m_drat)
|
||||
|
|
@ -390,7 +397,7 @@ namespace sat {
|
|||
|
||||
clause * solver::mk_ter_clause(literal * lits, bool learned) {
|
||||
m_stats.m_mk_ter_clause++;
|
||||
clause * r = m_cls_allocator.mk_clause(3, lits, learned);
|
||||
clause * r = alloc_clause(3, lits, learned);
|
||||
bool reinit = attach_ter_clause(*r);
|
||||
if (reinit && !learned) push_reinit_stack(*r);
|
||||
if (m_config.m_drat) m_drat.add(*r, learned);
|
||||
|
|
@ -429,7 +436,7 @@ namespace sat {
|
|||
|
||||
clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, bool learned) {
|
||||
m_stats.m_mk_clause++;
|
||||
clause * r = m_cls_allocator.mk_clause(num_lits, lits, learned);
|
||||
clause * r = alloc_clause(num_lits, lits, learned);
|
||||
SASSERT(!learned || r->is_learned());
|
||||
bool reinit = attach_nary_clause(*r);
|
||||
if (reinit && !learned) push_reinit_stack(*r);
|
||||
|
|
@ -446,7 +453,7 @@ namespace sat {
|
|||
|
||||
bool solver::attach_nary_clause(clause & c) {
|
||||
bool reinit = false;
|
||||
clause_offset cls_off = m_cls_allocator.get_offset(&c);
|
||||
clause_offset cls_off = cls_allocator().get_offset(&c);
|
||||
if (!at_base_lvl()) {
|
||||
if (c.is_learned()) {
|
||||
unsigned w2_idx = select_learned_watch_lit(c);
|
||||
|
|
@ -480,6 +487,8 @@ namespace sat {
|
|||
return reinit;
|
||||
}
|
||||
|
||||
static unsigned s_count = 0;
|
||||
|
||||
void solver::attach_clause(clause & c, bool & reinit) {
|
||||
SASSERT(c.size() > 2);
|
||||
reinit = false;
|
||||
|
|
@ -503,6 +512,83 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
bool solver::memory_pressure() {
|
||||
return 3*cls_allocator().get_allocation_size()/2 + memory::get_allocation_size() > memory::get_max_memory_size();
|
||||
}
|
||||
|
||||
struct solver::cmp_activity {
|
||||
solver& s;
|
||||
cmp_activity(solver& s):s(s) {}
|
||||
bool operator()(bool_var v1, bool_var v2) const {
|
||||
return s.m_activity[v1] > s.m_activity[v2];
|
||||
}
|
||||
};
|
||||
|
||||
void solver::defrag_clauses() {
|
||||
if (memory_pressure()) return;
|
||||
IF_VERBOSE(1, verbose_stream() << "(sat-defrag)\n");
|
||||
clause_allocator& alloc = m_cls_allocator[!m_cls_allocator_idx];
|
||||
ptr_vector<clause> new_clauses, new_learned;
|
||||
for (clause* c : m_clauses) c->unmark_used();
|
||||
for (clause* c : m_learned) c->unmark_used();
|
||||
|
||||
svector<bool_var> vars;
|
||||
for (unsigned i = 0; i < num_vars(); ++i) vars.push_back(i);
|
||||
std::stable_sort(vars.begin(), vars.end(), cmp_activity(*this));
|
||||
literal_vector lits;
|
||||
for (bool_var v : vars) lits.push_back(literal(v, false)), lits.push_back(literal(v, true));
|
||||
// walk clauses, reallocate them in an order that defragments memory and creates locality.
|
||||
for (literal lit : lits) {
|
||||
watch_list& wlist = m_watches[lit.index()];
|
||||
// for (watch_list& wlist : m_watches) {
|
||||
for (watched& w : wlist) {
|
||||
if (w.is_clause()) {
|
||||
clause& c1 = get_clause(w);
|
||||
clause_offset offset;
|
||||
if (c1.was_used()) {
|
||||
offset = c1.get_new_offset();
|
||||
}
|
||||
else {
|
||||
clause* c2 = alloc.copy_clause(c1);
|
||||
c1.mark_used();
|
||||
if (c1.is_learned()) {
|
||||
new_learned.push_back(c2);
|
||||
}
|
||||
else {
|
||||
new_clauses.push_back(c2);
|
||||
}
|
||||
offset = get_offset(*c2);
|
||||
c1.set_new_offset(offset);
|
||||
}
|
||||
w = watched(w.get_blocked_literal(), offset);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// reallocate ternary clauses.
|
||||
for (clause* c : m_clauses) {
|
||||
if (!c->was_used()) {
|
||||
SASSERT(c->size() == 3);
|
||||
new_clauses.push_back(alloc.copy_clause(*c));
|
||||
}
|
||||
dealloc_clause(c);
|
||||
}
|
||||
|
||||
for (clause* c : m_learned) {
|
||||
if (!c->was_used()) {
|
||||
SASSERT(c->size() == 3);
|
||||
new_learned.push_back(alloc.copy_clause(*c));
|
||||
}
|
||||
dealloc_clause(c);
|
||||
}
|
||||
m_clauses.swap(new_clauses);
|
||||
m_learned.swap(new_learned);
|
||||
|
||||
cls_allocator().finalize();
|
||||
m_cls_allocator_idx = !m_cls_allocator_idx;
|
||||
}
|
||||
|
||||
|
||||
void solver::set_learned(literal l1, literal l2, bool learned) {
|
||||
set_learned1(l1, l2, learned);
|
||||
set_learned1(l2, l1, learned);
|
||||
|
|
@ -669,7 +755,6 @@ namespace sat {
|
|||
TRACE("sat_assign_core", tout << l << " " << j << " level: " << scope_lvl() << "\n";);
|
||||
if (at_base_lvl()) {
|
||||
if (m_config.m_drat) m_drat.add(l, !j.is_none());
|
||||
|
||||
j = justification(); // erase justification for level 0
|
||||
}
|
||||
m_assignment[l.index()] = l_true;
|
||||
|
|
@ -695,6 +780,7 @@ namespace sat {
|
|||
m_reasoned[v] = 0;
|
||||
break;
|
||||
}
|
||||
|
||||
if (m_config.m_anti_exploration) {
|
||||
uint64 age = m_stats.m_conflict - m_canceled[v];
|
||||
if (age > 0) {
|
||||
|
|
@ -705,7 +791,10 @@ namespace sat {
|
|||
m_case_split_queue.activity_changed_eh(v, false);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
if (m_config.m_propagate_prefetch) {
|
||||
_mm_prefetch((const char*)(m_watches[l.index()].c_ptr()), 1);
|
||||
}
|
||||
|
||||
SASSERT(!l.sign() || m_phase[v] == NEG_PHASE);
|
||||
SASSERT(l.sign() || m_phase[v] == POS_PHASE);
|
||||
|
|
@ -718,9 +807,8 @@ namespace sat {
|
|||
|
||||
lbool solver::status(clause const & c) const {
|
||||
bool found_undef = false;
|
||||
unsigned sz = c.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
switch (value(c[i])) {
|
||||
for (literal lit : c) {
|
||||
switch (value(lit)) {
|
||||
case l_true:
|
||||
return l_true;
|
||||
case l_undef:
|
||||
|
|
@ -999,7 +1087,7 @@ namespace sat {
|
|||
return l_undef;
|
||||
}
|
||||
|
||||
restart();
|
||||
restart(!m_config.m_restart_fast);
|
||||
simplify_problem();
|
||||
if (check_inconsistent()) return l_false;
|
||||
gc();
|
||||
|
|
@ -1213,7 +1301,7 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
if (num_in > 0 || num_out > 0) {
|
||||
IF_VERBOSE(1, verbose_stream() << "(sat-sync out: " << num_out << " in: " << num_in << ")\n";);
|
||||
IF_VERBOSE(2, verbose_stream() << "(sat-sync out: " << num_out << " in: " << num_in << ")\n";);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1412,7 +1500,6 @@ namespace sat {
|
|||
SASSERT(m_search_lvl == 1);
|
||||
}
|
||||
|
||||
|
||||
void solver::update_min_core() {
|
||||
if (!m_min_core_valid || m_core.size() < m_min_core.size()) {
|
||||
m_min_core.reset();
|
||||
|
|
@ -1443,8 +1530,7 @@ namespace sat {
|
|||
push();
|
||||
reset_assumptions();
|
||||
TRACE("sat", tout << "reassert: " << m_min_core << "\n";);
|
||||
for (unsigned i = 0; i < m_min_core.size(); ++i) {
|
||||
literal lit = m_min_core[i];
|
||||
for (literal lit : m_min_core) {
|
||||
SASSERT(is_external(lit.var()));
|
||||
add_assumption(lit);
|
||||
assign(lit, justification());
|
||||
|
|
@ -1464,12 +1550,12 @@ namespace sat {
|
|||
assign(m_assumptions[i], justification());
|
||||
}
|
||||
TRACE("sat",
|
||||
for (unsigned i = 0; i < m_assumptions.size(); ++i) {
|
||||
index_set s;
|
||||
if (m_antecedents.find(m_assumptions[i].var(), s)) {
|
||||
tout << m_assumptions[i] << ": "; display_index_set(tout, s) << "\n";
|
||||
}
|
||||
});
|
||||
for (literal a : m_assumptions) {
|
||||
index_set s;
|
||||
if (m_antecedents.find(a.var(), s)) {
|
||||
tout << a << ": "; display_index_set(tout, s) << "\n";
|
||||
}
|
||||
});
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1496,10 +1582,11 @@ namespace sat {
|
|||
m_restarts = 0;
|
||||
m_simplifications = 0;
|
||||
m_conflicts_since_init = 0;
|
||||
m_next_simplify = 0;
|
||||
m_next_simplify = m_config.m_simplify_delay;
|
||||
m_min_d_tk = 1.0;
|
||||
m_search_lvl = 0;
|
||||
m_conflicts_since_gc = 0;
|
||||
m_restart_next_out = 0;
|
||||
m_asymm_branch.init_search();
|
||||
m_stopwatch.reset();
|
||||
m_stopwatch.start();
|
||||
|
|
@ -1511,7 +1598,6 @@ namespace sat {
|
|||
|
||||
/**
|
||||
\brief Apply all simplifications.
|
||||
|
||||
*/
|
||||
void solver::simplify_problem() {
|
||||
if (m_conflicts_since_init < m_next_simplify) {
|
||||
|
|
@ -1566,7 +1652,7 @@ namespace sat {
|
|||
reinit_assumptions();
|
||||
|
||||
if (m_next_simplify == 0) {
|
||||
m_next_simplify = m_config.m_restart_initial * m_config.m_simplify_mult1;
|
||||
m_next_simplify = m_config.m_next_simplify1;
|
||||
}
|
||||
else {
|
||||
m_next_simplify = static_cast<unsigned>(m_conflicts_since_init * m_config.m_simplify_mult2);
|
||||
|
|
@ -1652,10 +1738,14 @@ namespace sat {
|
|||
|
||||
// m_mc.set_solver(nullptr);
|
||||
m_mc(m_model);
|
||||
|
||||
|
||||
if (!check_clauses(m_model)) {
|
||||
IF_VERBOSE(0, verbose_stream() << "failure checking clauses on transformed model\n";);
|
||||
IF_VERBOSE(10, m_mc.display(verbose_stream()));
|
||||
//IF_VERBOSE(0, display_units(verbose_stream()));
|
||||
//IF_VERBOSE(0, display(verbose_stream()));
|
||||
IF_VERBOSE(0, for (bool_var v = 0; v < num; v++) verbose_stream() << v << ": " << m_model[v] << "\n";);
|
||||
|
||||
throw solver_exception("check model failed");
|
||||
}
|
||||
|
||||
|
|
@ -1666,7 +1756,9 @@ namespace sat {
|
|||
if (!m_clone->check_model(m_model)) {
|
||||
//IF_VERBOSE(0, display(verbose_stream()));
|
||||
//IF_VERBOSE(0, display_watches(verbose_stream()));
|
||||
//IF_VERBOSE(0, m_mc.display(verbose_stream()));
|
||||
IF_VERBOSE(0, m_mc.display(verbose_stream()));
|
||||
IF_VERBOSE(0, display_units(verbose_stream()));
|
||||
//IF_VERBOSE(0, m_clone->display(verbose_stream() << "clone\n"));
|
||||
throw solver_exception("check model failed (for cloned solver)");
|
||||
}
|
||||
}
|
||||
|
|
@ -1739,15 +1831,42 @@ namespace sat {
|
|||
return ok;
|
||||
}
|
||||
|
||||
void solver::restart() {
|
||||
void solver::restart(bool to_base) {
|
||||
m_stats.m_restart++;
|
||||
m_restarts++;
|
||||
IF_VERBOSE(1,
|
||||
verbose_stream() << "(sat-restart :conflicts " << m_stats.m_conflict << " :decisions " << m_stats.m_decision
|
||||
<< " :restarts " << m_stats.m_restart << mk_stat(*this)
|
||||
<< " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";);
|
||||
if (m_conflicts_since_init > m_restart_next_out + 500) {
|
||||
m_restart_next_out = m_conflicts_since_init;
|
||||
IF_VERBOSE(1,
|
||||
verbose_stream() << "(sat-restart :conflicts " << m_stats.m_conflict << " :decisions " << m_stats.m_decision
|
||||
<< " :restarts " << m_stats.m_restart << mk_stat(*this)
|
||||
<< " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";);
|
||||
}
|
||||
IF_VERBOSE(30, display_status(verbose_stream()););
|
||||
pop_reinit(scope_lvl() - search_lvl());
|
||||
unsigned num_scopes = 0;
|
||||
if (to_base || scope_lvl() == search_lvl()) {
|
||||
num_scopes = scope_lvl() - search_lvl();
|
||||
}
|
||||
else {
|
||||
bool_var next = m_case_split_queue.min_var();
|
||||
|
||||
// Implementations of Marijn's idea of reusing the
|
||||
// trail when the next decision literal has lower precedence.
|
||||
#if 0
|
||||
// pop the trail from top
|
||||
do {
|
||||
bool_var prev = scope_literal(scope_lvl() - num_scopes - 1).var();
|
||||
if (m_case_split_queue.more_active(prev, next)) break;
|
||||
++num_scopes;
|
||||
}
|
||||
while (num_scopes < scope_lvl() - search_lvl());
|
||||
#else
|
||||
// pop the trail from bottom
|
||||
unsigned n = search_lvl();
|
||||
for (; n < scope_lvl() && m_case_split_queue.more_active(scope_literal(n).var(), next); ++n) ;
|
||||
num_scopes = n - search_lvl();
|
||||
#endif
|
||||
}
|
||||
pop_reinit(num_scopes);
|
||||
m_conflicts_since_restart = 0;
|
||||
switch (m_config.m_restart) {
|
||||
case RS_GEOMETRIC:
|
||||
|
|
@ -1775,6 +1894,7 @@ namespace sat {
|
|||
return;
|
||||
if (m_config.m_gc_strategy == GC_DYN_PSM && !at_base_lvl())
|
||||
return;
|
||||
unsigned gc = m_stats.m_gc_clause;
|
||||
IF_VERBOSE(10, verbose_stream() << "(sat.gc)\n";);
|
||||
CASSERT("sat_gc_bug", check_invariant());
|
||||
switch (m_config.m_gc_strategy) {
|
||||
|
|
@ -1800,6 +1920,11 @@ namespace sat {
|
|||
break;
|
||||
}
|
||||
if (m_ext) m_ext->gc();
|
||||
if (gc > 0 && m_config.m_gc_defrag && !memory_pressure()) {
|
||||
pop(scope_lvl());
|
||||
defrag_clauses();
|
||||
reinit_assumptions();
|
||||
}
|
||||
m_conflicts_since_gc = 0;
|
||||
m_gc_threshold += m_config.m_gc_increment;
|
||||
CASSERT("sat_gc_bug", check_invariant());
|
||||
|
|
@ -2307,8 +2432,7 @@ namespace sat {
|
|||
void solver::resolve_conflict_for_unsat_core() {
|
||||
TRACE("sat", display(tout);
|
||||
unsigned level = 0;
|
||||
for (unsigned i = 0; i < m_trail.size(); ++i) {
|
||||
literal l = m_trail[i];
|
||||
for (literal l : m_trail) {
|
||||
if (level != m_level[l.var()]) {
|
||||
level = m_level[l.var()];
|
||||
tout << level << ": ";
|
||||
|
|
@ -2328,8 +2452,8 @@ namespace sat {
|
|||
}
|
||||
SASSERT(m_unmark.empty());
|
||||
DEBUG_CODE({
|
||||
for (unsigned i = 0; i < m_trail.size(); ++i) {
|
||||
SASSERT(!is_marked(m_trail[i].var()));
|
||||
for (literal lit : m_trail) {
|
||||
SASSERT(!is_marked(lit.var()));
|
||||
}});
|
||||
|
||||
unsigned old_size = m_unmark.size();
|
||||
|
|
@ -2739,7 +2863,8 @@ namespace sat {
|
|||
\brief Reset the mark of the variables in the current lemma.
|
||||
*/
|
||||
void solver::reset_lemma_var_marks() {
|
||||
if (m_config.m_branching_heuristic == BH_LRB) {
|
||||
if (m_config.m_branching_heuristic == BH_LRB ||
|
||||
m_config.m_branching_heuristic == BH_VSIDS) {
|
||||
update_lrb_reasoned();
|
||||
}
|
||||
literal_vector::iterator it = m_lemma.begin();
|
||||
|
|
@ -2785,8 +2910,7 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
reset_mark(m_lemma[0].var());
|
||||
for (unsigned i = m_lemma.size(); i > sz; ) {
|
||||
--i;
|
||||
for (unsigned i = m_lemma.size(); i-- > sz; ) {
|
||||
reset_mark(m_lemma[i].var());
|
||||
}
|
||||
m_lemma.shrink(sz);
|
||||
|
|
@ -2797,6 +2921,7 @@ namespace sat {
|
|||
if (!is_marked(v)) {
|
||||
mark(v);
|
||||
m_reasoned[v]++;
|
||||
inc_activity(v);
|
||||
m_lemma.push_back(lit);
|
||||
}
|
||||
}
|
||||
|
|
@ -3426,7 +3551,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
void solver::display_watches(std::ostream & out, literal lit) const {
|
||||
sat::display_watch_list(out << lit << ": ", m_cls_allocator, get_wlist(lit)) << "\n";
|
||||
display_watch_list(out << lit << ": ", get_wlist(lit)) << "\n";
|
||||
}
|
||||
|
||||
void solver::display_watches(std::ostream & out) const {
|
||||
|
|
@ -3434,10 +3559,14 @@ namespace sat {
|
|||
for (watch_list const& wlist : m_watches) {
|
||||
literal l = to_literal(l_idx++);
|
||||
if (!wlist.empty())
|
||||
sat::display_watch_list(out << l << ": ", m_cls_allocator, wlist) << "\n";
|
||||
display_watch_list(out << l << ": ", wlist) << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
std::ostream& solver::display_watch_list(std::ostream& out, watch_list const& wl) const {
|
||||
return sat::display_watch_list(out, cls_allocator(), wl);
|
||||
}
|
||||
|
||||
void solver::display_assignment(std::ostream & out) const {
|
||||
out << m_trail << "\n";
|
||||
}
|
||||
|
|
@ -3769,7 +3898,7 @@ namespace sat {
|
|||
return l_undef;
|
||||
}
|
||||
|
||||
restart();
|
||||
restart(true);
|
||||
simplify_problem();
|
||||
if (check_inconsistent()) {
|
||||
fixup_consequence_core();
|
||||
|
|
@ -3862,7 +3991,7 @@ namespace sat {
|
|||
else {
|
||||
is_sat = bounded_search();
|
||||
if (is_sat == l_undef) {
|
||||
restart();
|
||||
restart(true);
|
||||
}
|
||||
extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -86,7 +86,8 @@ namespace sat {
|
|||
scoped_ptr<extension> m_ext;
|
||||
parallel* m_par;
|
||||
random_gen m_rand;
|
||||
clause_allocator m_cls_allocator;
|
||||
clause_allocator m_cls_allocator[2];
|
||||
bool m_cls_allocator_idx;
|
||||
cleaner m_cleaner;
|
||||
model m_model;
|
||||
model_converter m_mc;
|
||||
|
|
@ -217,9 +218,16 @@ namespace sat {
|
|||
void mk_clause(literal_vector const& lits, bool learned = false) { mk_clause(lits.size(), lits.c_ptr(), learned); }
|
||||
void mk_clause(unsigned num_lits, literal * lits, bool learned = false);
|
||||
void mk_clause(literal l1, literal l2, bool learned = false);
|
||||
void mk_clause(literal l1, literal l2, literal l3, bool learned = false);
|
||||
void mk_clause(literal l1, literal l2, literal l3, bool learned = false);
|
||||
|
||||
protected:
|
||||
inline clause_allocator& cls_allocator() { return m_cls_allocator[m_cls_allocator_idx]; }
|
||||
inline clause_allocator const& cls_allocator() const { return m_cls_allocator[m_cls_allocator_idx]; }
|
||||
inline clause * alloc_clause(unsigned num_lits, literal const * lits, bool learned) { return cls_allocator().mk_clause(num_lits, lits, learned); }
|
||||
inline void dealloc_clause(clause* c) { cls_allocator().del_clause(c); }
|
||||
struct cmp_activity;
|
||||
void defrag_clauses();
|
||||
bool memory_pressure();
|
||||
void del_clause(clause & c);
|
||||
clause * mk_clause_core(unsigned num_lits, literal * lits, bool learned);
|
||||
clause * mk_clause_core(literal_vector const& lits) { return mk_clause_core(lits.size(), lits.c_ptr()); }
|
||||
|
|
@ -236,6 +244,10 @@ namespace sat {
|
|||
void set_learned(clause& c, bool learned);
|
||||
void set_learned(literal l1, literal l2, bool learned);
|
||||
void set_learned1(literal l1, literal l2, bool learned);
|
||||
void add_ate(clause& c) { m_mc.add_ate(c); }
|
||||
void add_ate(literal l1, literal l2) { m_mc.add_ate(l1, l2); }
|
||||
void add_ate(literal_vector const& lits) { m_mc.add_ate(lits); }
|
||||
|
||||
class scoped_disable_checkpoint {
|
||||
solver& s;
|
||||
public:
|
||||
|
|
@ -285,6 +297,7 @@ namespace sat {
|
|||
unsigned lvl(literal l) const { return m_level[l.var()]; }
|
||||
unsigned init_trail_size() const { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; }
|
||||
literal trail_literal(unsigned i) const { return m_trail[i]; }
|
||||
literal scope_literal(unsigned n) const { return m_trail[m_scopes[n].m_trail_lim]; }
|
||||
void assign(literal l, justification j) {
|
||||
TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";);
|
||||
switch (value(l)) {
|
||||
|
|
@ -297,7 +310,7 @@ namespace sat {
|
|||
void set_conflict(justification c, literal not_l);
|
||||
void set_conflict(justification c) { set_conflict(c, null_literal); }
|
||||
lbool status(clause const & c) const;
|
||||
clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); }
|
||||
clause_offset get_offset(clause const & c) const { return cls_allocator().get_offset(&c); }
|
||||
void checkpoint() {
|
||||
if (!m_checkpoint_enabled) return;
|
||||
if (!m_rlimit.inc()) {
|
||||
|
|
@ -369,6 +382,7 @@ namespace sat {
|
|||
|
||||
unsigned m_conflicts_since_init;
|
||||
unsigned m_restarts;
|
||||
unsigned m_restart_next_out;
|
||||
unsigned m_conflicts_since_restart;
|
||||
unsigned m_simplifications;
|
||||
unsigned m_restart_threshold;
|
||||
|
|
@ -401,7 +415,7 @@ namespace sat {
|
|||
void simplify_problem();
|
||||
void mk_model();
|
||||
bool check_model(model const & m) const;
|
||||
void restart();
|
||||
void restart(bool to_base);
|
||||
void sort_watch_lits();
|
||||
void exchange_par();
|
||||
lbool check_par(unsigned num_lits, literal const* lits);
|
||||
|
|
@ -433,7 +447,7 @@ namespace sat {
|
|||
if (value(l0) != l_true)
|
||||
return true;
|
||||
justification const & jst = m_justification[l0.var()];
|
||||
return !jst.is_clause() || m_cls_allocator.get_clause(jst.get_clause_offset()) != &c;
|
||||
return !jst.is_clause() || cls_allocator().get_clause(jst.get_clause_offset()) != &c;
|
||||
}
|
||||
|
||||
clause& get_clause(watch_list::iterator it) const {
|
||||
|
|
@ -441,13 +455,18 @@ namespace sat {
|
|||
return get_clause(it->get_clause_offset());
|
||||
}
|
||||
|
||||
clause& get_clause(watched const& w) const {
|
||||
SASSERT(w.get_kind() == watched::CLAUSE);
|
||||
return get_clause(w.get_clause_offset());
|
||||
}
|
||||
|
||||
clause& get_clause(justification const& j) const {
|
||||
SASSERT(j.is_clause());
|
||||
return get_clause(j.get_clause_offset());
|
||||
}
|
||||
|
||||
clause& get_clause(clause_offset cls_off) const {
|
||||
return *(m_cls_allocator.get_clause(cls_off));
|
||||
return *(cls_allocator().get_clause(cls_off));
|
||||
}
|
||||
|
||||
// -----------------------
|
||||
|
|
@ -630,6 +649,7 @@ namespace sat {
|
|||
void display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const;
|
||||
void display_assignment(std::ostream & out) const;
|
||||
std::ostream& display_justification(std::ostream & out, justification const& j) const;
|
||||
std::ostream& display_watch_list(std::ostream& out, watch_list const& wl) const;
|
||||
|
||||
protected:
|
||||
void display_binary(std::ostream & out) const;
|
||||
|
|
|
|||
|
|
@ -24,6 +24,8 @@ Notes:
|
|||
#include "ast/ast_util.h"
|
||||
#include "solver/solver.h"
|
||||
#include "solver/tactic2solver.h"
|
||||
#include "solver/parallel_params.hpp"
|
||||
#include "solver/parallel_tactic.h"
|
||||
#include "tactic/tactical.h"
|
||||
#include "tactic/aig/aig_tactic.h"
|
||||
#include "tactic/core/propagate_values_tactic.h"
|
||||
|
|
@ -31,14 +33,15 @@ Notes:
|
|||
#include "tactic/arith/card2bv_tactic.h"
|
||||
#include "tactic/bv/bit_blaster_tactic.h"
|
||||
#include "tactic/core/simplify_tactic.h"
|
||||
#include "tactic/core/solve_eqs_tactic.h"
|
||||
#include "tactic/bv/bit_blaster_model_converter.h"
|
||||
#include "model/model_smt2_pp.h"
|
||||
#include "model/model_v2_pp.h"
|
||||
#include "model/model_evaluator.h"
|
||||
#include "tactic/bv/bit_blaster_model_converter.h"
|
||||
#include "tactic/core/propagate_values_tactic.h"
|
||||
#include "sat/sat_solver.h"
|
||||
#include "sat/sat_params.hpp"
|
||||
#include "sat/tactic/goal2sat.h"
|
||||
#include "sat/tactic/sat_tactic.h"
|
||||
#include "sat/sat_simplifier_params.hpp"
|
||||
|
||||
// incremental SAT solver.
|
||||
|
|
@ -281,9 +284,12 @@ public:
|
|||
m_params.append(p);
|
||||
sat_params p1(p);
|
||||
m_params.set_bool("keep_cardinality_constraints", p1.cardinality_solver());
|
||||
m_params.set_sym("pb.solver", p1.pb_solver());
|
||||
|
||||
m_params.set_bool("keep_pb_constraints", m_solver.get_config().m_pb_solver == sat::PB_SOLVER);
|
||||
m_params.set_bool("pb_num_system", m_solver.get_config().m_pb_solver == sat::PB_SORTING);
|
||||
m_params.set_bool("pb_totalizer", m_solver.get_config().m_pb_solver == sat::PB_TOTALIZER);
|
||||
|
||||
m_params.set_bool("xor_solver", p1.xor_solver());
|
||||
m_solver.updt_params(m_params);
|
||||
m_solver.set_incremental(is_incremental() && !override_incremental());
|
||||
|
|
@ -498,7 +504,10 @@ public:
|
|||
simp2_p.set_bool("elim_and", true);
|
||||
simp2_p.set_bool("blast_distinct", true);
|
||||
m_preprocess =
|
||||
and_then(mk_card2bv_tactic(m, m_params), // updates model converter
|
||||
and_then(mk_simplify_tactic(m),
|
||||
mk_propagate_values_tactic(m),
|
||||
//time consuming if done in inner loop: mk_solve_eqs_tactic(m, simp2_p),
|
||||
mk_card2bv_tactic(m, m_params), // updates model converter
|
||||
using_params(mk_simplify_tactic(m), simp2_p),
|
||||
mk_max_bv_sharing_tactic(m),
|
||||
mk_bit_blaster_tactic(m, m_bb_rewriter.get()), // updates model converter
|
||||
|
|
@ -859,3 +868,9 @@ void inc_sat_display(std::ostream& out, solver& _s, unsigned sz, expr*const* sof
|
|||
s.display_weighted(out, sz, soft, weights.c_ptr());
|
||||
}
|
||||
|
||||
|
||||
tactic * mk_psat_tactic(ast_manager& m, params_ref const& p) {
|
||||
parallel_params pp(p);
|
||||
bool use_parallel = pp.enable();
|
||||
return pp.enable() ? mk_parallel_tactic(mk_inc_sat_solver(m, p, false), p) : mk_sat_tactic(m);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -22,8 +22,12 @@ Notes:
|
|||
|
||||
#include "solver/solver.h"
|
||||
|
||||
class tactic;
|
||||
|
||||
solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_mode = true);
|
||||
|
||||
tactic* mk_psat_tactic(ast_manager& m, params_ref const& p);
|
||||
|
||||
|
||||
void inc_sat_display(std::ostream& out, solver& s, unsigned sz, expr*const* soft, rational const* _weights);
|
||||
|
||||
|
|
|
|||
|
|
@ -72,6 +72,8 @@ namespace sat {
|
|||
bool_var next_var() { SASSERT(!empty()); return m_queue.erase_min(); }
|
||||
|
||||
bool_var min_var() { SASSERT(!empty()); return m_queue.min_value(); }
|
||||
|
||||
bool more_active(bool_var v1, bool_var v2) const { return m_queue.less_than(v1, v2); }
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -20,6 +20,8 @@ Notes:
|
|||
#include "tactic/tactical.h"
|
||||
#include "sat/tactic/goal2sat.h"
|
||||
#include "sat/sat_solver.h"
|
||||
#include "solver/parallel_tactic.h"
|
||||
#include "solver/parallel_params.hpp"
|
||||
#include "model/model_v2_pp.h"
|
||||
|
||||
class sat_tactic : public tactic {
|
||||
|
|
@ -215,3 +217,4 @@ tactic * mk_sat_preprocessor_tactic(ast_manager & m, params_ref const & p) {
|
|||
return t;
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -39,6 +39,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
|
|||
m_timeout = p.timeout();
|
||||
m_rlimit = p.rlimit();
|
||||
m_max_conflicts = p.max_conflicts();
|
||||
m_restart_max = p.restart_max();
|
||||
m_core_validate = p.core_validate();
|
||||
m_logic = _p.get_sym("logic", m_logic);
|
||||
m_string_solver = p.string_solver();
|
||||
|
|
|
|||
|
|
@ -99,6 +99,7 @@ struct smt_params : public preprocessor_params,
|
|||
unsigned m_phase_caching_off;
|
||||
bool m_minimize_lemmas;
|
||||
unsigned m_max_conflicts;
|
||||
unsigned m_restart_max;
|
||||
bool m_simplify_clauses;
|
||||
unsigned m_tick;
|
||||
bool m_display_features;
|
||||
|
|
|
|||
|
|
@ -21,6 +21,7 @@ def_module_params(module_name='smt',
|
|||
('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
|
||||
('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
|
||||
('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'),
|
||||
('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
|
||||
('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
|
||||
('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
|
||||
('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'),
|
||||
|
|
|
|||
|
|
@ -1826,6 +1826,15 @@ namespace smt {
|
|||
m_bvar_inc *= INV_ACTIVITY_LIMIT;
|
||||
}
|
||||
|
||||
expr* context::next_decision() {
|
||||
bool_var var;
|
||||
lbool phase;
|
||||
m_case_split_queue->next_case_split(var, phase);
|
||||
if (var == null_bool_var) return m_manager.mk_true();
|
||||
m_case_split_queue->unassign_var_eh(var);
|
||||
return bool_var2expr(var);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Execute next clase split, return false if there are no
|
||||
more case splits to be performed.
|
||||
|
|
@ -3412,6 +3421,7 @@ namespace smt {
|
|||
m_num_conflicts = 0;
|
||||
m_num_conflicts_since_restart = 0;
|
||||
m_num_conflicts_since_lemma_gc = 0;
|
||||
m_num_restarts = 0;
|
||||
m_restart_threshold = m_fparams.m_restart_initial;
|
||||
m_restart_outer_threshold = m_fparams.m_restart_initial;
|
||||
m_agility = 0.0;
|
||||
|
|
@ -3543,7 +3553,7 @@ namespace smt {
|
|||
inc_limits();
|
||||
if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
|
||||
SASSERT(!inconsistent());
|
||||
IF_VERBOSE(2, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations
|
||||
IF_VERBOSE(2, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations
|
||||
<< " :decisions " << m_stats.m_num_decisions
|
||||
<< " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold;
|
||||
if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) {
|
||||
|
|
@ -3552,9 +3562,10 @@ namespace smt {
|
|||
if (m_fparams.m_restart_adaptive) {
|
||||
verbose_stream() << " :agility " << m_agility;
|
||||
}
|
||||
verbose_stream() << ")" << std::endl; verbose_stream().flush(););
|
||||
verbose_stream() << ")\n");
|
||||
// execute the restart
|
||||
m_stats.m_num_restarts++;
|
||||
m_num_restarts++;
|
||||
if (m_scope_lvl > curr_lvl) {
|
||||
pop_scope(m_scope_lvl - curr_lvl);
|
||||
SASSERT(at_search_level());
|
||||
|
|
@ -3571,6 +3582,11 @@ namespace smt {
|
|||
status = l_false;
|
||||
return false;
|
||||
}
|
||||
if (m_num_restarts >= m_fparams.m_restart_max) {
|
||||
status = l_undef;
|
||||
m_last_search_failure = NUM_CONFLICTS;
|
||||
return false;
|
||||
}
|
||||
}
|
||||
if (m_fparams.m_simplify_clauses)
|
||||
simplify_clauses();
|
||||
|
|
|
|||
|
|
@ -896,6 +896,8 @@ namespace smt {
|
|||
unsigned m_num_conflicts;
|
||||
unsigned m_num_conflicts_since_restart;
|
||||
unsigned m_num_conflicts_since_lemma_gc;
|
||||
unsigned m_num_restarts;
|
||||
unsigned m_num_simplifications;
|
||||
unsigned m_restart_threshold;
|
||||
unsigned m_restart_outer_threshold;
|
||||
unsigned m_luby_idx;
|
||||
|
|
@ -1037,6 +1039,8 @@ namespace smt {
|
|||
|
||||
enode * get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args);
|
||||
|
||||
expr* next_decision();
|
||||
|
||||
protected:
|
||||
bool decide();
|
||||
|
||||
|
|
|
|||
|
|
@ -174,11 +174,15 @@ namespace smt {
|
|||
void get_guessed_literals(expr_ref_vector & result) {
|
||||
m_kernel.get_guessed_literals(result);
|
||||
}
|
||||
|
||||
|
||||
expr* next_decision() {
|
||||
return m_kernel.next_decision();
|
||||
}
|
||||
|
||||
void collect_statistics(::statistics & st) const {
|
||||
m_kernel.collect_statistics(st);
|
||||
}
|
||||
|
||||
|
||||
void reset_statistics() {
|
||||
}
|
||||
|
||||
|
|
@ -343,6 +347,10 @@ namespace smt {
|
|||
m_imp->get_guessed_literals(result);
|
||||
}
|
||||
|
||||
expr* kernel::next_decision() {
|
||||
return m_imp->next_decision();
|
||||
}
|
||||
|
||||
void kernel::display(std::ostream & out) const {
|
||||
m_imp->display(out);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -212,6 +212,11 @@ namespace smt {
|
|||
*/
|
||||
void get_guessed_literals(expr_ref_vector & result);
|
||||
|
||||
/**
|
||||
\brief return the next case split literal.
|
||||
*/
|
||||
expr* next_decision();
|
||||
|
||||
/**
|
||||
\brief (For debubbing purposes) Prints the state of the kernel
|
||||
*/
|
||||
|
|
|
|||
|
|
@ -30,9 +30,35 @@ Notes:
|
|||
namespace smt {
|
||||
|
||||
class smt_solver : public solver_na2as {
|
||||
|
||||
struct cuber {
|
||||
smt_solver& m_solver;
|
||||
unsigned m_round;
|
||||
expr_ref m_result;
|
||||
cuber(smt_solver& s):
|
||||
m_solver(s),
|
||||
m_round(0),
|
||||
m_result(s.get_manager()) {}
|
||||
expr_ref cube() {
|
||||
switch (m_round) {
|
||||
case 0:
|
||||
m_result = m_solver.m_context.next_decision();
|
||||
break;
|
||||
case 1:
|
||||
m_result = m_solver.get_manager().mk_not(m_result);
|
||||
break;
|
||||
default:
|
||||
m_result = m_solver.get_manager().mk_false();
|
||||
break;
|
||||
}
|
||||
++m_round;
|
||||
return m_result;
|
||||
}
|
||||
};
|
||||
|
||||
smt_params m_smt_params;
|
||||
smt::kernel m_context;
|
||||
progress_callback * m_callback;
|
||||
cuber* m_cuber;
|
||||
symbol m_logic;
|
||||
bool m_minimizing_core;
|
||||
bool m_core_extend_patterns;
|
||||
|
|
@ -45,6 +71,7 @@ namespace smt {
|
|||
solver_na2as(m),
|
||||
m_smt_params(p),
|
||||
m_context(m, m_smt_params),
|
||||
m_cuber(nullptr),
|
||||
m_minimizing_core(false),
|
||||
m_core_extend_patterns(false),
|
||||
m_core_extend_patterns_max_distance(UINT_MAX),
|
||||
|
|
@ -72,6 +99,7 @@ namespace smt {
|
|||
|
||||
~smt_solver() override {
|
||||
dec_ref_values(get_manager(), m_name2assertion);
|
||||
dealloc(m_cuber);
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p) override {
|
||||
|
|
@ -204,7 +232,6 @@ namespace smt {
|
|||
ast_manager & get_manager() const override { return m_context.m(); }
|
||||
|
||||
void set_progress_callback(progress_callback * callback) override {
|
||||
m_callback = callback;
|
||||
m_context.set_progress_callback(callback);
|
||||
}
|
||||
|
||||
|
|
@ -217,13 +244,24 @@ namespace smt {
|
|||
return m_context.get_formula(idx);
|
||||
}
|
||||
|
||||
virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) {
|
||||
virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned cutoff) {
|
||||
ast_manager& m = get_manager();
|
||||
return expr_ref(m.mk_true(), m);
|
||||
}
|
||||
|
||||
virtual expr_ref_vector cube(expr_ref_vector&, unsigned) {
|
||||
return expr_ref_vector(get_manager());
|
||||
if (!m_cuber) {
|
||||
m_cuber = alloc(cuber, *this);
|
||||
}
|
||||
expr_ref result = m_cuber->cube();
|
||||
expr_ref_vector lits(m);
|
||||
if (m.is_false(result)) {
|
||||
dealloc(m_cuber);
|
||||
m_cuber = nullptr;
|
||||
}
|
||||
if (m.is_true(result)) {
|
||||
dealloc(m_cuber);
|
||||
m_cuber = nullptr;
|
||||
return lits;
|
||||
}
|
||||
lits.push_back(result);
|
||||
return lits;
|
||||
}
|
||||
|
||||
struct collect_fds_proc {
|
||||
|
|
|
|||
|
|
@ -16,19 +16,21 @@ Author:
|
|||
Notes:
|
||||
|
||||
--*/
|
||||
#include "tactic/tactic.h"
|
||||
#include "tactic/tactical.h"
|
||||
#include "util/lp/lp_params.hpp"
|
||||
#include "ast/rewriter/rewriter_types.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "smt/smt_kernel.h"
|
||||
#include "smt/params/smt_params.h"
|
||||
#include "smt/params/smt_params_helper.hpp"
|
||||
#include "util/lp/lp_params.hpp"
|
||||
#include "ast/rewriter/rewriter_types.h"
|
||||
#include "tactic/generic_model_converter.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "solver/solver2tactic.h"
|
||||
#include "smt/smt_solver.h"
|
||||
#include "tactic/tactic.h"
|
||||
#include "tactic/tactical.h"
|
||||
#include "tactic/generic_model_converter.h"
|
||||
#include "solver/solver2tactic.h"
|
||||
#include "solver/solver.h"
|
||||
#include "solver/mus.h"
|
||||
#include "solver/parallel_tactic.h"
|
||||
#include "solver/parallel_params.hpp"
|
||||
|
||||
typedef obj_map<expr, expr *> expr2expr_map;
|
||||
|
||||
|
|
@ -301,3 +303,20 @@ tactic * mk_smt_tactic_using(bool auto_config, params_ref const & _p) {
|
|||
return using_params(r, p);
|
||||
}
|
||||
|
||||
tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic) {
|
||||
parallel_params pp(p);
|
||||
bool use_parallel = pp.enable();
|
||||
return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p);
|
||||
}
|
||||
|
||||
tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& _p, symbol const& logic) {
|
||||
parallel_params pp(_p);
|
||||
bool use_parallel = pp.enable();
|
||||
params_ref p = _p;
|
||||
p.set_bool("auto_config", auto_config);
|
||||
return using_params(pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p), p);
|
||||
}
|
||||
|
||||
tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) {
|
||||
return mk_parallel_tactic(mk_smt_solver(m, p, symbol::null), p);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -31,8 +31,13 @@ tactic * mk_smt_tactic(params_ref const & p = params_ref());
|
|||
// syntax sugar for using_params(mk_smt_tactic(), p) where p = (:auto_config, auto_config)
|
||||
tactic * mk_smt_tactic_using(bool auto_config = true, params_ref const & p = params_ref());
|
||||
|
||||
tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic = symbol::null);
|
||||
tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& p, symbol const& logic = symbol::null);
|
||||
tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p);
|
||||
|
||||
|
||||
/*
|
||||
ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(p)")
|
||||
ADD_TACTIC("psmt", "builtin strategy for SMT tactic in parallel.", "mk_parallel_smt_tactic(m, p)")
|
||||
*/
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -3,6 +3,7 @@ z3_add_component(solver
|
|||
check_sat_result.cpp
|
||||
combined_solver.cpp
|
||||
mus.cpp
|
||||
parallel_tactic.cpp
|
||||
smt_logics.cpp
|
||||
solver.cpp
|
||||
solver_na2as.cpp
|
||||
|
|
@ -14,4 +15,6 @@ z3_add_component(solver
|
|||
tactic
|
||||
PYG_FILES
|
||||
combined_solver_params.pyg
|
||||
parallel_params.pyg
|
||||
|
||||
)
|
||||
|
|
|
|||
15
src/solver/parallel_params.pyg
Normal file
15
src/solver/parallel_params.pyg
Normal file
|
|
@ -0,0 +1,15 @@
|
|||
def_module_params('parallel',
|
||||
description='parameters for parallel solver',
|
||||
class_name='parallel_params',
|
||||
export=True,
|
||||
params=(
|
||||
('enable', BOOL, False, 'enable parallel solver by default on selected tactics (for QF_BV)'),
|
||||
('threads.max', UINT, 10000, 'caps maximal number of threads below the number of processors'),
|
||||
('conquer.batch_size', UINT, 100, 'number of cubes to batch together for fast conquer'),
|
||||
('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'),
|
||||
('conquer.delay', UINT, 10, 'delay of cubes until applying conquer'),
|
||||
('conquer.backtrack_frequency', UINT, 10, 'frequency to apply core minimization during conquer'),
|
||||
('simplify.exp', DOUBLE, 1, 'restart and inprocess max is multipled by simplify.exp ^ depth'),
|
||||
('simplify.restart.max', UINT, 5000, 'maximal number of restarts during simplification phase'),
|
||||
('simplify.inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'),
|
||||
))
|
||||
|
|
@ -16,20 +16,16 @@ Author:
|
|||
Miguel Neves
|
||||
|
||||
Notes:
|
||||
|
||||
|
||||
A task comprises of a non-empty sequence of cubes, a type and parameters
|
||||
|
||||
If in the cube state, the solver performs the following:
|
||||
|
||||
It invokes the following procedure:
|
||||
1. Clone the state with the remaining cubes if there is more than one cube. Re-enqueue the remaining cubes.
|
||||
2. Apply simplifications and pre-processing according to configuration.
|
||||
3. Cube using the parameter settings prescribed in m_params.
|
||||
4. Create a conquer state with the produced cubes.
|
||||
If in the conquer state, the solver performs the following
|
||||
1. Pass the cubes as assumptions and solve each sub-cube with a prescribed resource bound.
|
||||
2. Assemble cubes that could not be solved and create a cube state.
|
||||
4. Optionally pass the cubes as assumptions and solve each sub-cube with a prescribed resource bound.
|
||||
5. Assemble cubes that could not be solved and create a cube state.
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#include <thread>
|
||||
|
|
@ -41,13 +37,18 @@ Notes:
|
|||
#include "solver/solver.h"
|
||||
#include "solver/solver2tactic.h"
|
||||
#include "tactic/tactic.h"
|
||||
#include "tactic/tactical.h"
|
||||
#include "tactic/portfolio/fd_solver.h"
|
||||
#include "solver/parallel_tactic.h"
|
||||
#include "solver/parallel_params.hpp"
|
||||
#include "smt/tactic/smt_tactic.h"
|
||||
#include "smt/smt_solver.h"
|
||||
#include "sat/sat_solver/inc_sat_solver.h"
|
||||
#include "sat/tactic/sat_tactic.h"
|
||||
|
||||
class parallel_tactic : public tactic {
|
||||
|
||||
|
||||
enum task_type { cube_task, conquer_task };
|
||||
|
||||
class solver_state;
|
||||
|
||||
class task_queue {
|
||||
|
|
@ -98,6 +99,8 @@ class parallel_tactic : public tactic {
|
|||
}
|
||||
}
|
||||
|
||||
bool in_shutdown() const { return m_shutdown; }
|
||||
|
||||
void add_task(solver_state* task) {
|
||||
std::lock_guard<std::mutex> lock(m_mutex);
|
||||
m_tasks.push_back(task);
|
||||
|
|
@ -106,6 +109,11 @@ class parallel_tactic : public tactic {
|
|||
}
|
||||
}
|
||||
|
||||
bool is_idle() {
|
||||
std::lock_guard<std::mutex> lock(m_mutex);
|
||||
return m_tasks.empty() && m_num_waiters > 0;
|
||||
}
|
||||
|
||||
solver_state* get_task() {
|
||||
while (!m_shutdown) {
|
||||
inc_wait();
|
||||
|
|
@ -114,10 +122,10 @@ class parallel_tactic : public tactic {
|
|||
dec_wait();
|
||||
return st;
|
||||
}
|
||||
{
|
||||
std::unique_lock<std::mutex> lock(m_mutex);
|
||||
m_cond.wait(lock);
|
||||
}
|
||||
{
|
||||
std::unique_lock<std::mutex> lock(m_mutex);
|
||||
m_cond.wait(lock);
|
||||
}
|
||||
dec_wait();
|
||||
}
|
||||
return nullptr;
|
||||
|
|
@ -150,75 +158,68 @@ class parallel_tactic : public tactic {
|
|||
|
||||
};
|
||||
|
||||
class cube_var {
|
||||
expr_ref_vector m_vars;
|
||||
expr_ref_vector m_cube;
|
||||
public:
|
||||
cube_var(expr_ref_vector& c, expr_ref_vector& vs):
|
||||
m_vars(vs), m_cube(c) {}
|
||||
|
||||
cube_var operator()(ast_translation& tr) {
|
||||
return cube_var(tr(m_cube), tr(m_vars));
|
||||
}
|
||||
|
||||
expr_ref_vector const& cube() const { return m_cube; }
|
||||
expr_ref_vector const& vars() const { return m_vars; }
|
||||
};
|
||||
|
||||
class solver_state {
|
||||
task_type m_type; // current work role of the task
|
||||
scoped_ptr<ast_manager> m_manager; // ownership handle to ast_manager
|
||||
expr_ref_vector m_cubes; // set of cubes to process by task
|
||||
vector<cube_var> m_cubes; // set of cubes to process by task
|
||||
expr_ref_vector m_asserted_cubes; // set of cubes asserted on the current solver
|
||||
params_ref m_params; // configuration parameters
|
||||
ref<solver> m_solver; // solver state
|
||||
unsigned m_depth; // number of nested calls to cubing
|
||||
double m_width; // estimate of fraction of problem handled by state
|
||||
unsigned m_cube_cutoff; // saved configuration value
|
||||
double m_cube_fraction; // saved configuration value
|
||||
unsigned m_restart_max; // saved configuration value
|
||||
|
||||
expr_ref_vector cube_literals(expr* cube) {
|
||||
expr_ref_vector literals(m());
|
||||
if (m().is_and(cube)) {
|
||||
literals.append(to_app(cube)->get_num_args(), to_app(cube)->get_args());
|
||||
}
|
||||
else {
|
||||
literals.push_back(cube);
|
||||
}
|
||||
return literals;
|
||||
}
|
||||
|
||||
public:
|
||||
solver_state(ast_manager* m, solver* s, params_ref const& p, task_type t):
|
||||
m_type(t),
|
||||
solver_state(ast_manager* m, solver* s, params_ref const& p):
|
||||
m_manager(m),
|
||||
m_cubes(s->get_manager()),
|
||||
m_asserted_cubes(s->get_manager()),
|
||||
m_params(p),
|
||||
m_solver(s),
|
||||
m_depth(0),
|
||||
m_width(1.0)
|
||||
{
|
||||
m_cube_cutoff = p.get_uint("sat.lookahead.cube.cutoff", 8);
|
||||
m_cube_fraction = p.get_double("sat.lookahead.cube.fraction", 0.4);
|
||||
m_restart_max = p.get_uint("sat.restart.max", 10);
|
||||
}
|
||||
|
||||
ast_manager& m() { return m_solver->get_manager(); }
|
||||
|
||||
solver& get_solver() { return *m_solver; }
|
||||
|
||||
solver* copy_solver() { return m_solver->translate(m_solver->get_manager(), m_params); }
|
||||
|
||||
solver const& get_solver() const { return *m_solver; }
|
||||
|
||||
solver_state* clone() {
|
||||
SASSERT(!m_cubes.empty());
|
||||
ast_manager& m = m_solver->get_manager();
|
||||
ast_manager* new_m = alloc(ast_manager, m, !m.proof_mode());
|
||||
ast_manager* new_m = alloc(ast_manager, m, m.proof_mode());
|
||||
ast_translation tr(m, *new_m);
|
||||
solver* s = m_solver->translate(*new_m, m_params);
|
||||
solver_state* st = alloc(solver_state, new_m, s, m_params, m_type);
|
||||
for (expr* c : m_cubes) st->m_cubes.push_back(tr(c));
|
||||
solver* s = m_solver.get()->translate(*new_m, m_params);
|
||||
solver_state* st = alloc(solver_state, new_m, s, m_params);
|
||||
for (auto & c : m_cubes) st->m_cubes.push_back(c(tr));
|
||||
for (expr* c : m_asserted_cubes) st->m_asserted_cubes.push_back(tr(c));
|
||||
st->m_depth = m_depth;
|
||||
st->m_width = m_width;
|
||||
return st;
|
||||
}
|
||||
|
||||
task_type type() const { return m_type; }
|
||||
|
||||
void set_type(task_type t) { m_type = t; }
|
||||
|
||||
expr_ref_vector const& cubes() const { SASSERT(m_type == conquer_task); return m_cubes; }
|
||||
vector<cube_var> const& cubes() const { return m_cubes; }
|
||||
|
||||
// remove up to n cubes from list of cubes.
|
||||
expr_ref_vector split_cubes(unsigned n) {
|
||||
expr_ref_vector result(m());
|
||||
vector<cube_var> split_cubes(unsigned n) {
|
||||
vector<cube_var> result;
|
||||
while (n-- > 0 && !m_cubes.empty()) {
|
||||
result.push_back(m_cubes.back());
|
||||
m_cubes.pop_back();
|
||||
|
|
@ -226,14 +227,14 @@ class parallel_tactic : public tactic {
|
|||
return result;
|
||||
}
|
||||
|
||||
void set_cubes(expr_ref_vector const& c) {
|
||||
void set_cubes(vector<cube_var>& c) {
|
||||
m_cubes.reset();
|
||||
m_cubes.append(c);
|
||||
}
|
||||
|
||||
void inc_depth(unsigned inc) { m_depth += inc; }
|
||||
|
||||
void inc_width(unsigned w) { m_width *= w; }
|
||||
void inc_width(unsigned w) { m_width *= w; }
|
||||
|
||||
double get_width() const { return m_width; }
|
||||
|
||||
|
|
@ -241,71 +242,53 @@ class parallel_tactic : public tactic {
|
|||
|
||||
lbool simplify() {
|
||||
lbool r = l_undef;
|
||||
if (m_depth == 1) {
|
||||
IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-1)\n";);
|
||||
set_simplify_params(true, true); // retain PB, retain blocked
|
||||
r = get_solver().check_sat(0,0);
|
||||
if (r != l_undef) return r;
|
||||
|
||||
// copy over the resulting clauses with a configuration that blasts PB constraints
|
||||
set_simplify_params(false, true);
|
||||
expr_ref_vector fmls(m());
|
||||
get_solver().get_assertions(fmls);
|
||||
model_converter_ref mc = get_solver().get_model_converter();
|
||||
m_solver = mk_fd_solver(m(), m_params);
|
||||
m_solver->set_model_converter(mc.get());
|
||||
m_solver->assert_expr(fmls);
|
||||
}
|
||||
IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-2)\n";);
|
||||
set_simplify_params(false, true); // remove PB, retain blocked
|
||||
IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-1)\n";);
|
||||
set_simplify_params(true); // retain blocked
|
||||
r = get_solver().check_sat(0,0);
|
||||
if (r != l_undef) return r;
|
||||
IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-3)\n";);
|
||||
set_simplify_params(false, false); // remove any PB, remove blocked
|
||||
IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-2)\n";);
|
||||
set_simplify_params(false); // remove blocked
|
||||
r = get_solver().check_sat(0,0);
|
||||
return r;
|
||||
}
|
||||
|
||||
void assert_cube(expr* cube) {
|
||||
void assert_cube(expr_ref_vector const& cube) {
|
||||
get_solver().assert_expr(cube);
|
||||
m_asserted_cubes.append(cube_literals(cube));
|
||||
m_asserted_cubes.append(cube);
|
||||
}
|
||||
|
||||
lbool solve(expr* cube) {
|
||||
set_conquer_params();
|
||||
expr_ref_vector literals = cube_literals(cube);
|
||||
return get_solver().check_sat(literals);
|
||||
}
|
||||
|
||||
void set_cube_params() {
|
||||
unsigned cutoff = m_cube_cutoff;
|
||||
double fraction = m_cube_fraction;
|
||||
if (m_depth == 1 && cutoff > 0) {
|
||||
fraction = 0; // use fixed cubing at depth 1.
|
||||
}
|
||||
else {
|
||||
cutoff = 0; // use dynamic cubing beyond depth 1
|
||||
}
|
||||
m_params.set_uint ("lookahead.cube.cutoff", cutoff);
|
||||
m_params.set_double("lookahead.cube.fraction", fraction);
|
||||
get_solver().updt_params(m_params);
|
||||
void set_cube_params() {
|
||||
}
|
||||
|
||||
void set_conquer_params() {
|
||||
m_params.set_bool("lookahead_simplify", false);
|
||||
m_params.set_uint("restart.max", m_restart_max);
|
||||
get_solver().updt_params(m_params);
|
||||
set_conquer_params(get_solver());
|
||||
}
|
||||
|
||||
void set_simplify_params(bool pb_simp, bool retain_blocked) {
|
||||
m_params.set_bool("cardinality.solver", pb_simp);
|
||||
m_params.set_sym ("pb.solver", pb_simp ? symbol("solver") : symbol("circuit"));
|
||||
if (m_params.get_uint("inprocess.max", UINT_MAX) == UINT_MAX)
|
||||
m_params.set_uint("inprocess.max", 2);
|
||||
m_params.set_bool("lookahead_simplify", true);
|
||||
m_params.set_uint("restart.max", UINT_MAX);
|
||||
m_params.set_bool("retain_blocked_clauses", retain_blocked);
|
||||
get_solver().updt_params(m_params);
|
||||
void set_conquer_params(solver& s) {
|
||||
parallel_params pp(m_params);
|
||||
params_ref p;
|
||||
p.copy(m_params);
|
||||
p.set_bool("gc.burst", true); // apply eager gc
|
||||
p.set_uint("simplify.delay", 1000); // delay simplification by 1000 conflicts
|
||||
p.set_bool("lookahead_simplify", false);
|
||||
p.set_uint("restart.max", pp.conquer_restart_max());
|
||||
p.set_uint("inprocess.max", UINT_MAX); // base bounds on restart.max
|
||||
s.updt_params(p);
|
||||
}
|
||||
|
||||
void set_simplify_params(bool retain_blocked) {
|
||||
parallel_params pp(m_params);
|
||||
params_ref p;
|
||||
p.copy(m_params);
|
||||
double exp = pp.simplify_exp();
|
||||
exp = std::max(exp, 1.0);
|
||||
unsigned mult = static_cast<unsigned>(pow(exp, m_depth - 1));
|
||||
p.set_uint("inprocess.max", pp.simplify_inprocess_max() * mult);
|
||||
p.set_uint("restart.max", pp.simplify_restart_max() * mult);
|
||||
p.set_bool("lookahead_simplify", true);
|
||||
p.set_bool("retain_blocked_clauses", retain_blocked);
|
||||
if (m_depth > 1) p.set_uint("bce_delay", 0);
|
||||
get_solver().updt_params(p);
|
||||
}
|
||||
|
||||
bool canceled() {
|
||||
|
|
@ -321,40 +304,67 @@ class parallel_tactic : public tactic {
|
|||
|
||||
private:
|
||||
|
||||
ast_manager& m_manager;
|
||||
params_ref m_params;
|
||||
solver_ref m_solver;
|
||||
ast_manager& m_manager;
|
||||
params_ref m_params;
|
||||
sref_vector<model> m_models;
|
||||
unsigned m_num_threads;
|
||||
statistics m_stats;
|
||||
task_queue m_queue;
|
||||
std::mutex m_mutex;
|
||||
double m_progress;
|
||||
bool m_has_undef;
|
||||
bool m_allsat;
|
||||
unsigned m_num_unsat;
|
||||
int m_exn_code;
|
||||
std::string m_exn_msg;
|
||||
unsigned m_num_threads;
|
||||
statistics m_stats;
|
||||
task_queue m_queue;
|
||||
std::mutex m_mutex;
|
||||
double m_progress;
|
||||
unsigned m_branches;
|
||||
unsigned m_backtrack_frequency;
|
||||
unsigned m_conquer_delay;
|
||||
volatile bool m_has_undef;
|
||||
bool m_allsat;
|
||||
unsigned m_num_unsat;
|
||||
int m_exn_code;
|
||||
std::string m_exn_msg;
|
||||
|
||||
void init() {
|
||||
m_num_threads = omp_get_num_procs(); // TBD adjust by possible threads used inside each solver.
|
||||
parallel_params pp(m_params);
|
||||
m_num_threads = std::min((unsigned)omp_get_num_procs(), pp.threads_max());
|
||||
m_progress = 0;
|
||||
m_has_undef = false;
|
||||
m_allsat = false;
|
||||
m_num_unsat = 0;
|
||||
m_branches = 0;
|
||||
m_num_unsat = 0;
|
||||
m_backtrack_frequency = pp.conquer_backtrack_frequency();
|
||||
m_conquer_delay = pp.conquer_delay();
|
||||
m_exn_code = 0;
|
||||
m_params.set_bool("override_incremental", true);
|
||||
}
|
||||
|
||||
void log_branches(lbool status) {
|
||||
IF_VERBOSE(0, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% ";
|
||||
if (status == l_true) verbose_stream() << ":status sat ";
|
||||
if (status == l_undef) verbose_stream() << ":status unknown ";
|
||||
verbose_stream() << ":closed " << m_num_unsat << " :open " << m_branches << ")\n";);
|
||||
}
|
||||
|
||||
void add_branches(unsigned b) {
|
||||
if (b == 0) return;
|
||||
{
|
||||
std::lock_guard<std::mutex> lock(m_mutex);
|
||||
m_branches += b;
|
||||
}
|
||||
log_branches(l_false);
|
||||
}
|
||||
|
||||
void dec_branch() {
|
||||
std::lock_guard<std::mutex> lock(m_mutex);
|
||||
--m_branches;
|
||||
}
|
||||
|
||||
void close_branch(solver_state& s, lbool status) {
|
||||
double f = 100.0 / s.get_width();
|
||||
{
|
||||
std::lock_guard<std::mutex> lock(m_mutex);
|
||||
m_progress += f;
|
||||
--m_branches;
|
||||
}
|
||||
IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% ";
|
||||
if (status == l_true) verbose_stream() << ":status sat ";
|
||||
if (status == l_undef) verbose_stream() << ":status unknown ";
|
||||
verbose_stream() << ":unsat " << m_num_unsat << ")\n";);
|
||||
log_branches(status);
|
||||
}
|
||||
|
||||
void report_sat(solver_state& s) {
|
||||
|
|
@ -374,11 +384,15 @@ private:
|
|||
}
|
||||
}
|
||||
|
||||
void report_unsat(solver_state& s) {
|
||||
close_branch(s, l_false);
|
||||
void inc_unsat() {
|
||||
std::lock_guard<std::mutex> lock(m_mutex);
|
||||
++m_num_unsat;
|
||||
}
|
||||
|
||||
void report_unsat(solver_state& s) {
|
||||
inc_unsat();
|
||||
close_branch(s, l_false);
|
||||
}
|
||||
|
||||
void report_undef(solver_state& s) {
|
||||
m_has_undef = true;
|
||||
|
|
@ -387,26 +401,26 @@ private:
|
|||
|
||||
void cube_and_conquer(solver_state& s) {
|
||||
ast_manager& m = s.m();
|
||||
expr_ref_vector cubes(m), cube(m), hard_cubes(m);
|
||||
|
||||
switch (s.type()) {
|
||||
case cube_task: goto cube;
|
||||
case conquer_task: goto conquer;
|
||||
}
|
||||
|
||||
cube:
|
||||
SASSERT(s.type() == cube_task);
|
||||
vector<cube_var> cube, hard_cubes, cubes;
|
||||
expr_ref_vector vars(m);
|
||||
|
||||
cube_again:
|
||||
// extract up to one cube and add it.
|
||||
cube.reset();
|
||||
cube.append(s.split_cubes(1));
|
||||
SASSERT(cube.size() <= 1);
|
||||
IF_VERBOSE(2, verbose_stream() << "(sat.parallel :split-cube " << cube.size() << ")\n";);
|
||||
IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :split-cube " << cube.size() << ")\n";);
|
||||
if (!s.cubes().empty()) m_queue.add_task(s.clone());
|
||||
if (!cube.empty()) s.assert_cube(cube.get(0));
|
||||
s.inc_depth(1);
|
||||
if (!cube.empty()) {
|
||||
s.assert_cube(cube.get(0).cube());
|
||||
vars.reset();
|
||||
vars.append(cube.get(0).vars());
|
||||
}
|
||||
|
||||
simplify_again:
|
||||
s.inc_depth(1);
|
||||
// simplify
|
||||
if (canceled(s)) return;
|
||||
switch (s.simplify()) {
|
||||
case l_undef: break;
|
||||
case l_true: report_sat(s); return;
|
||||
|
|
@ -414,60 +428,127 @@ private:
|
|||
}
|
||||
if (canceled(s)) return;
|
||||
|
||||
if (memory_pressure()) {
|
||||
goto simplify_again;
|
||||
}
|
||||
// extract cubes.
|
||||
cubes.reset();
|
||||
s.set_cube_params();
|
||||
while (true) {
|
||||
expr_ref_vector vars(m);
|
||||
expr_ref_vector c = s.get_solver().cube(vars, UINT_MAX); // TBD tune this
|
||||
solver_ref conquer;
|
||||
|
||||
unsigned cutoff = UINT_MAX;
|
||||
bool first = true;
|
||||
unsigned num_backtracks = 0, width = 0;
|
||||
while (cutoff > 0 && !canceled(s)) {
|
||||
expr_ref_vector c = s.get_solver().cube(vars, cutoff);
|
||||
if (c.empty()) {
|
||||
report_undef(s);
|
||||
return;
|
||||
goto simplify_again;
|
||||
}
|
||||
if (m.is_false(c.back())) {
|
||||
break;
|
||||
}
|
||||
cubes.push_back(mk_and(c));
|
||||
lbool is_sat = l_undef;
|
||||
if (width >= m_conquer_delay && !conquer) {
|
||||
conquer = s.copy_solver();
|
||||
s.set_conquer_params(*conquer.get());
|
||||
}
|
||||
if (conquer) {
|
||||
is_sat = conquer->check_sat(c);
|
||||
}
|
||||
switch (is_sat) {
|
||||
case l_false:
|
||||
cutoff = c.size();
|
||||
backtrack(*conquer.get(), c, (num_backtracks++) % m_backtrack_frequency == 0);
|
||||
if (cutoff != c.size()) {
|
||||
IF_VERBOSE(0, verbose_stream() << "(tactic.parallel :backtrack " << cutoff << " -> " << c.size() << ")\n");
|
||||
cutoff = c.size();
|
||||
}
|
||||
inc_unsat();
|
||||
log_branches(l_false);
|
||||
break;
|
||||
|
||||
case l_true:
|
||||
report_sat(s);
|
||||
if (conquer) {
|
||||
collect_statistics(*conquer.get());
|
||||
}
|
||||
return;
|
||||
|
||||
case l_undef:
|
||||
++width;
|
||||
IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :cube " << c.size() << " :vars " << vars.size() << ")\n");
|
||||
cubes.push_back(cube_var(c, vars));
|
||||
cutoff = UINT_MAX;
|
||||
break;
|
||||
|
||||
}
|
||||
if (cubes.size() >= conquer_batch_size()) {
|
||||
spawn_cubes(s, 10*width, cubes);
|
||||
first = false;
|
||||
cubes.reset();
|
||||
}
|
||||
}
|
||||
|
||||
IF_VERBOSE(1, verbose_stream() << "(parallel_tactic :cubes " << cubes.size() << ")\n";);
|
||||
IF_VERBOSE(10, verbose_stream() << "(parallel_tactic :cubes " << cubes << ")\n";);
|
||||
if (conquer) {
|
||||
collect_statistics(*conquer.get());
|
||||
}
|
||||
|
||||
if (cubes.empty()) {
|
||||
if (cubes.empty() && first) {
|
||||
report_unsat(s);
|
||||
return;
|
||||
}
|
||||
else if (cubes.empty()) {
|
||||
dec_branch();
|
||||
}
|
||||
else {
|
||||
s.inc_width(cubes.size());
|
||||
s.inc_width(width);
|
||||
add_branches(cubes.size()-1);
|
||||
s.set_cubes(cubes);
|
||||
s.set_type(conquer_task);
|
||||
goto conquer;
|
||||
}
|
||||
goto cube_again;
|
||||
}
|
||||
}
|
||||
|
||||
conquer:
|
||||
SASSERT(s.type() == conquer_task);
|
||||
void spawn_cubes(solver_state& s, unsigned width, vector<cube_var>& cubes) {
|
||||
if (cubes.empty()) return;
|
||||
add_branches(cubes.size());
|
||||
s.set_cubes(cubes);
|
||||
solver_state* s1 = s.clone();
|
||||
s1->inc_width(width);
|
||||
m_queue.add_task(s1);
|
||||
}
|
||||
|
||||
// extract a batch of cubes
|
||||
cubes.reset();
|
||||
cubes.append(s.split_cubes(conquer_batch_size()));
|
||||
if (!s.cubes().empty()) m_queue.add_task(s.clone());
|
||||
/*
|
||||
* \brief backtrack from unsatisfiable core
|
||||
*/
|
||||
void backtrack(solver& s, expr_ref_vector& asms, bool full) {
|
||||
ast_manager& m = s.get_manager();
|
||||
expr_ref_vector core(m);
|
||||
obj_hashtable<expr> hcore;
|
||||
s.get_unsat_core(core);
|
||||
while (!asms.empty() && !core.contains(asms.back())) asms.pop_back();
|
||||
if (!full) return;
|
||||
|
||||
s.set_conquer_params();
|
||||
hard_cubes.reset();
|
||||
for (expr * c : cubes) {
|
||||
switch (s.solve(c)) {
|
||||
case l_undef: hard_cubes.push_back(c); break;
|
||||
case l_true: report_sat(s); break;
|
||||
case l_false: report_unsat(s); break;
|
||||
//s.assert_expr(m.mk_not(mk_and(core)));
|
||||
if (!asms.empty()) {
|
||||
expr* last = asms.back();
|
||||
expr_ref not_last(mk_not(m, last), m);
|
||||
asms.pop_back();
|
||||
asms.push_back(not_last);
|
||||
lbool r = s.check_sat(asms);
|
||||
asms.pop_back();
|
||||
if (r != l_false) {
|
||||
asms.push_back(last);
|
||||
return;
|
||||
}
|
||||
if (canceled(s)) return;
|
||||
}
|
||||
IF_VERBOSE(1, verbose_stream() << "(parallel_tactic :cubes " << cubes.size() << " :hard-cubes " << hard_cubes.size() << ")\n";);
|
||||
if (hard_cubes.empty()) return;
|
||||
|
||||
s.set_cubes(hard_cubes);
|
||||
s.set_type(cube_task);
|
||||
goto cube;
|
||||
core.reset();
|
||||
s.get_unsat_core(core);
|
||||
if (core.contains(not_last)) {
|
||||
//s.assert_expr(m.mk_not(mk_and(core)));
|
||||
r = s.check_sat(asms);
|
||||
}
|
||||
if (r == l_false) {
|
||||
backtrack(s, asms, full);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool canceled(solver_state& s) {
|
||||
|
|
@ -480,6 +561,10 @@ private:
|
|||
}
|
||||
}
|
||||
|
||||
bool memory_pressure() {
|
||||
return memory::above_high_watermark();
|
||||
}
|
||||
|
||||
void run_solver() {
|
||||
try {
|
||||
while (solver_state* st = m_queue.get_task()) {
|
||||
|
|
@ -493,6 +578,7 @@ private:
|
|||
}
|
||||
catch (z3_exception& ex) {
|
||||
IF_VERBOSE(1, verbose_stream() << ex.msg() << "\n";);
|
||||
if (m_queue.in_shutdown()) return;
|
||||
m_queue.shutdown();
|
||||
std::lock_guard<std::mutex> lock(m_mutex);
|
||||
if (ex.has_error_code()) {
|
||||
|
|
@ -506,11 +592,16 @@ private:
|
|||
}
|
||||
|
||||
void collect_statistics(solver_state& s) {
|
||||
collect_statistics(s.get_solver());
|
||||
}
|
||||
|
||||
void collect_statistics(solver& s) {
|
||||
std::lock_guard<std::mutex> lock(m_mutex);
|
||||
s.get_solver().collect_statistics(m_stats);
|
||||
s.collect_statistics(m_stats);
|
||||
}
|
||||
|
||||
lbool solve(model_ref& mdl) {
|
||||
add_branches(1);
|
||||
vector<std::thread> threads;
|
||||
for (unsigned i = 0; i < m_num_threads; ++i)
|
||||
threads.push_back(std::thread([this]() { run_solver(); }));
|
||||
|
|
@ -531,25 +622,33 @@ private:
|
|||
}
|
||||
|
||||
std::ostream& display(std::ostream& out) {
|
||||
unsigned n_models, n_unsat;
|
||||
double n_progress;
|
||||
{
|
||||
std::lock_guard<std::mutex> lock(m_mutex);
|
||||
n_models = m_models.size();
|
||||
n_unsat = m_num_unsat;
|
||||
n_progress = m_progress;
|
||||
}
|
||||
m_stats.display(out);
|
||||
m_queue.display(out);
|
||||
std::lock_guard<std::mutex> lock(m_mutex);
|
||||
out << "(parallel_tactic :unsat " << m_num_unsat << " :progress " << m_progress << "% :models " << m_models.size() << ")\n";
|
||||
out << "(tactic.parallel :unsat " << n_unsat << " :progress " << n_progress << "% :models " << n_models << ")\n";
|
||||
return out;
|
||||
}
|
||||
|
||||
public:
|
||||
|
||||
parallel_tactic(ast_manager& m, params_ref const& p) :
|
||||
m_manager(m),
|
||||
parallel_tactic(solver* s, params_ref const& p) :
|
||||
m_solver(s),
|
||||
m_manager(s->get_manager()),
|
||||
m_params(p) {
|
||||
init();
|
||||
init();
|
||||
}
|
||||
|
||||
void operator ()(const goal_ref & g,goal_ref_buffer & result) {
|
||||
ast_manager& m = g->m();
|
||||
solver* s = mk_fd_solver(m, m_params);
|
||||
solver_state* st = alloc(solver_state, 0, s, m_params, cube_task);
|
||||
solver* s = m_solver->translate(m, m_params);
|
||||
solver_state* st = alloc(solver_state, 0, s, m_params);
|
||||
m_queue.add_task(st);
|
||||
expr_ref_vector clauses(m);
|
||||
ptr_vector<expr> assumptions;
|
||||
|
|
@ -583,25 +682,24 @@ public:
|
|||
result.push_back(g.get());
|
||||
}
|
||||
|
||||
unsigned conquer_batch_size() const {
|
||||
parallel_params pp(m_params);
|
||||
return pp.conquer_batch_size();
|
||||
}
|
||||
|
||||
void cleanup() {
|
||||
m_queue.reset();
|
||||
init();
|
||||
}
|
||||
|
||||
tactic* translate(ast_manager& m) {
|
||||
return alloc(parallel_tactic, m, m_params);
|
||||
solver* s = m_solver->translate(m, m_params);
|
||||
return alloc(parallel_tactic, s, m_params);
|
||||
}
|
||||
|
||||
virtual void updt_params(params_ref const & p) {
|
||||
m_params.copy(p);
|
||||
}
|
||||
|
||||
virtual void collect_param_descrs(param_descrs & r) {
|
||||
r.insert("conquer_batch_size", CPK_UINT, "(default: 1000) batch size of cubes to conquer");
|
||||
}
|
||||
|
||||
unsigned conquer_batch_size() const {
|
||||
return m_params.get_uint("conquer_batch_size", 1000);
|
||||
parallel_params pp(p);
|
||||
m_conquer_delay = pp.conquer_delay();
|
||||
}
|
||||
|
||||
virtual void collect_statistics(statistics & st) const {
|
||||
|
|
@ -610,15 +708,14 @@ public:
|
|||
st.update("par models", m_models.size());
|
||||
st.update("par progress", m_progress);
|
||||
}
|
||||
|
||||
virtual void reset_statistics() {
|
||||
m_stats.reset();
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
||||
|
||||
tactic * mk_parallel_tactic(ast_manager& m, params_ref const& p) {
|
||||
return alloc(parallel_tactic, m, p);
|
||||
tactic * mk_parallel_tactic(solver* s, params_ref const& p) {
|
||||
return alloc(parallel_tactic, s, p);
|
||||
}
|
||||
|
||||
|
|
@ -19,13 +19,9 @@ Notes:
|
|||
#ifndef PARALLEL_TACTIC_H_
|
||||
#define PARALLEL_TACTIC_H_
|
||||
|
||||
class solver;
|
||||
class tactic;
|
||||
class solver;
|
||||
|
||||
tactic * mk_parallel_tactic(ast_manager& m, params_ref const& p);
|
||||
|
||||
/*
|
||||
ADD_TACTIC("qffdp", "builtin strategy for solving QF_FD problems in parallel.", "mk_parallel_tactic(m, p)")
|
||||
*/
|
||||
tactic * mk_parallel_tactic(solver* s, params_ref const& p);
|
||||
|
||||
#endif
|
||||
|
|
@ -144,9 +144,6 @@ struct bit_blaster_model_converter : public model_converter {
|
|||
}
|
||||
new_val = util.mk_numeral(val, bv_sz);
|
||||
new_model->register_decl(m_vars.get(i), new_val);
|
||||
continue;
|
||||
bail:
|
||||
new_model->register_decl(m_vars.get(i), mk_bv(bs, *old_model));
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -804,19 +804,17 @@ class elim_uncnstr_tactic : public tactic {
|
|||
ast_manager & m() { return m_manager; }
|
||||
|
||||
void init_mc(bool produce_models) {
|
||||
if (!produce_models) {
|
||||
m_mc = nullptr;
|
||||
return;
|
||||
m_mc = nullptr;
|
||||
if (produce_models) {
|
||||
m_mc = alloc(mc, m(), "elim_uncstr");
|
||||
}
|
||||
m_mc = alloc(mc, m(), "elim_uncstr");
|
||||
}
|
||||
|
||||
void init_rw(bool produce_proofs) {
|
||||
m_rw = alloc(rw, m(), produce_proofs, m_vars, m_mc.get(), m_max_memory, m_max_steps);
|
||||
}
|
||||
|
||||
void operator()(goal_ref const & g, goal_ref_buffer& result) {
|
||||
bool produce_models = g->models_enabled();
|
||||
|
||||
void operator()(goal_ref const & g, goal_ref_buffer & result) {
|
||||
bool produce_proofs = g->proofs_enabled();
|
||||
|
||||
TRACE("elim_uncnstr_bug", g->display(tout););
|
||||
|
|
@ -831,11 +829,9 @@ class elim_uncnstr_tactic : public tactic {
|
|||
}
|
||||
bool modified = true;
|
||||
TRACE("elim_uncnstr", tout << "unconstrained variables...\n";
|
||||
for (expr * v : m_vars) {
|
||||
tout << mk_ismt2_pp(v, m()) << " ";
|
||||
}
|
||||
for (expr * v : m_vars) tout << mk_ismt2_pp(v, m()) << " ";
|
||||
tout << "\n";);
|
||||
init_mc(produce_models);
|
||||
init_mc(g->models_enabled());
|
||||
init_rw(produce_proofs);
|
||||
|
||||
expr_ref new_f(m());
|
||||
|
|
@ -862,14 +858,9 @@ class elim_uncnstr_tactic : public tactic {
|
|||
else {
|
||||
app_ref_vector & fresh_vars = m_rw->cfg().m_fresh_vars;
|
||||
m_num_elim_apps = fresh_vars.size();
|
||||
if (produce_models && !fresh_vars.empty()) {
|
||||
generic_model_converter * fmc = alloc(generic_model_converter, m(), "elim_uncnstr");
|
||||
for (app * f : fresh_vars)
|
||||
fmc->hide(f);
|
||||
g->add(concat(fmc, m_mc.get()));
|
||||
}
|
||||
else {
|
||||
g->set((model_converter*)nullptr);
|
||||
if (m_mc.get()) {
|
||||
for (app * f : fresh_vars) m_mc->hide(f);
|
||||
g->add(m_mc.get());
|
||||
}
|
||||
}
|
||||
m_mc = nullptr;
|
||||
|
|
|
|||
|
|
@ -85,7 +85,9 @@ goal::goal(goal const & src, bool):
|
|||
m_core_enabled(src.unsat_core_enabled()),
|
||||
m_inconsistent(false),
|
||||
m_precision(src.m_precision) {
|
||||
add(src.mc());
|
||||
m_mc = src.m_mc.get();
|
||||
m_pc = src.m_pc.get();
|
||||
m_dc = src.m_dc.get();
|
||||
}
|
||||
|
||||
goal::~goal() {
|
||||
|
|
|
|||
|
|
@ -4,7 +4,6 @@ z3_add_component(portfolio
|
|||
default_tactic.cpp
|
||||
enum2bv_solver.cpp
|
||||
fd_solver.cpp
|
||||
parallel_tactic.cpp
|
||||
pb2bv_solver.cpp
|
||||
smt_strategic_solver.cpp
|
||||
solver2lookahead.cpp
|
||||
|
|
@ -21,5 +20,4 @@ z3_add_component(portfolio
|
|||
TACTIC_HEADERS
|
||||
default_tactic.h
|
||||
fd_solver.h
|
||||
parallel_tactic.h
|
||||
)
|
||||
|
|
|
|||
|
|
@ -24,6 +24,8 @@ Notes:
|
|||
#include "tactic/portfolio/pb2bv_solver.h"
|
||||
#include "tactic/portfolio/bounded_int2bv_solver.h"
|
||||
#include "solver/solver2tactic.h"
|
||||
#include "solver/parallel_tactic.h"
|
||||
#include "solver/parallel_params.hpp"
|
||||
|
||||
solver * mk_fd_solver(ast_manager & m, params_ref const & p, bool incremental_mode) {
|
||||
solver* s = mk_inc_sat_solver(m, p, incremental_mode);
|
||||
|
|
@ -36,3 +38,8 @@ solver * mk_fd_solver(ast_manager & m, params_ref const & p, bool incremental_mo
|
|||
tactic * mk_fd_tactic(ast_manager & m, params_ref const& p) {
|
||||
return mk_solver2tactic(mk_fd_solver(m, p, false));
|
||||
}
|
||||
|
||||
tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p) {
|
||||
solver* s = mk_fd_solver(m, p);
|
||||
return mk_parallel_tactic(s, p);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -27,9 +27,11 @@ class tactic;
|
|||
|
||||
solver * mk_fd_solver(ast_manager & m, params_ref const & p, bool incremental_mode = true);
|
||||
tactic * mk_fd_tactic(ast_manager & m, params_ref const & p);
|
||||
tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p);
|
||||
|
||||
/*
|
||||
ADD_TACTIC("qffd", "builtin strategy for solving QF_FD problems.", "mk_fd_tactic(m, p)")
|
||||
ADD_TACTIC("pqffd", "builtin strategy for solving QF_FD problems in parallel.", "mk_parallel_qffd_tactic(m, p)")
|
||||
*/
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -19,13 +19,13 @@ Notes:
|
|||
#include "tactic/tactical.h"
|
||||
#include "tactic/core/simplify_tactic.h"
|
||||
#include "tactic/core/propagate_values_tactic.h"
|
||||
#include "smt/tactic/smt_tactic.h"
|
||||
#include "tactic/core/nnf_tactic.h"
|
||||
#include "tactic/arith/probe_arith.h"
|
||||
#include "smt/tactic/smt_tactic.h"
|
||||
#include "qe/qe_tactic.h"
|
||||
#include "qe/nlqsat.h"
|
||||
#include "nlsat/tactic/qfnra_nlsat_tactic.h"
|
||||
#include "qe/qe_lite.h"
|
||||
#include "tactic/arith/probe_arith.h"
|
||||
#include "nlsat/tactic/qfnra_nlsat_tactic.h"
|
||||
|
||||
tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) {
|
||||
params_ref p1 = p;
|
||||
|
|
|
|||
|
|
@ -28,6 +28,7 @@ Notes:
|
|||
#include "tactic/bv/bv_size_reduction_tactic.h"
|
||||
#include "tactic/aig/aig_tactic.h"
|
||||
#include "sat/tactic/sat_tactic.h"
|
||||
#include "sat/sat_solver/inc_sat_solver.h"
|
||||
#include "ackermannization/ackermannize_bv_tactic.h"
|
||||
|
||||
#define MEMLIMIT 300
|
||||
|
|
@ -127,11 +128,10 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
|
|||
|
||||
|
||||
tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
|
||||
|
||||
tactic * new_sat = cond(mk_produce_proofs_probe(),
|
||||
and_then(mk_simplify_tactic(m), mk_smt_tactic()),
|
||||
mk_sat_tactic(m));
|
||||
mk_psat_tactic(m, p));
|
||||
|
||||
return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic());
|
||||
return mk_qfbv_tactic(m, p, new_sat, mk_psmt_tactic(m, p));
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -89,7 +89,7 @@ static tactic * mk_bv2sat_tactic(ast_manager & m) {
|
|||
mk_max_bv_sharing_tactic(m),
|
||||
mk_bit_blaster_tactic(m),
|
||||
mk_aig_tactic(),
|
||||
mk_sat_tactic(m)),
|
||||
mk_sat_tactic(m, solver_p)),
|
||||
solver_p);
|
||||
}
|
||||
|
||||
|
|
@ -220,7 +220,7 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
|
|||
using_params(mk_lia2sat_tactic(m), quasi_pb_p),
|
||||
mk_fail_if_undecided_tactic()),
|
||||
mk_bounded_tactic(m),
|
||||
mk_smt_tactic())),
|
||||
mk_psmt_tactic(m, p))),
|
||||
main_p);
|
||||
|
||||
st->updt_params(p);
|
||||
|
|
|
|||
|
|
@ -40,6 +40,7 @@ Notes:
|
|||
#include "tactic/smtlogics/qfbv_tactic.h"
|
||||
#include "solver/tactic2solver.h"
|
||||
#include "tactic/bv/bv_bound_chk_tactic.h"
|
||||
#include "ackermannization/ackermannize_bv_tactic.h"
|
||||
///////////////
|
||||
|
||||
class qfufbv_ackr_tactic : public tactic {
|
||||
|
|
@ -157,13 +158,14 @@ static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) {
|
|||
|
||||
static tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) {
|
||||
return and_then(mk_simplify_tactic(m),
|
||||
mk_propagate_values_tactic(m),
|
||||
mk_solve_eqs_tactic(m),
|
||||
mk_elim_uncnstr_tactic(m),
|
||||
if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))),
|
||||
if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
|
||||
mk_max_bv_sharing_tactic(m)
|
||||
);
|
||||
mk_propagate_values_tactic(m),
|
||||
mk_solve_eqs_tactic(m),
|
||||
mk_elim_uncnstr_tactic(m),
|
||||
if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))),
|
||||
if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
|
||||
mk_max_bv_sharing_tactic(m),
|
||||
if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m,p)))
|
||||
);
|
||||
}
|
||||
|
||||
tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) {
|
||||
|
|
|
|||
|
|
@ -27,10 +27,6 @@ class heap : private LT {
|
|||
int_vector m_values;
|
||||
int_vector m_value2indices;
|
||||
|
||||
bool less_than(int v1, int v2) const {
|
||||
return LT::operator()(v1, v2);
|
||||
}
|
||||
|
||||
static int left(int i) {
|
||||
return i << 1;
|
||||
}
|
||||
|
|
@ -126,6 +122,10 @@ public:
|
|||
CASSERT("heap", check_invariant());
|
||||
}
|
||||
|
||||
bool less_than(int v1, int v2) const {
|
||||
return LT::operator()(v1, v2);
|
||||
}
|
||||
|
||||
bool empty() const {
|
||||
return m_values.size() == 1;
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue