mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

bug fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-19 21:49:03 -08:00
parent bb4888ce31
commit 4c1379e8c9
22 changed files with 238 additions and 580 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
View file

@ -181,6 +181,17 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
}
}
unsigned m_keypos;
void start_rewrite() {
m_keypos = m_keys.size();
}
void end_rewrite(obj_map<func_decl, expr*>& const2bits) {
for (unsigned i = m_keypos; i < m_keys.size(); ++i) {
const2bits.insert(m_keys[i].get(), m_values[i].get());
}
}
template<typename V>
app * mk_mkbv(V const & bits) {
return m().mk_app(butil().get_family_id(), OP_MKBV, bits.size(), bits.c_ptr());
@ -635,6 +646,8 @@ struct bit_blaster_rewriter::imp : public rewriter_tpl<blaster_rewriter_cfg> {
}
void push() { m_cfg.push(); }
void pop(unsigned s) { m_cfg.pop(s); }
void start_rewrite() { m_cfg.start_rewrite(); }
void end_rewrite(obj_map<func_decl, expr*>& const2bits) { m_cfg.end_rewrite(const2bits); }
unsigned get_num_scopes() const { return m_cfg.get_num_scopes(); }
};
@ -683,3 +696,10 @@ unsigned bit_blaster_rewriter::get_num_scopes() const {
return m_imp->get_num_scopes();
}
void bit_blaster_rewriter::start_rewrite() {
m_imp->start_rewrite();
}
void bit_blaster_rewriter::end_rewrite(obj_map<func_decl, expr*>& const2bits) {
m_imp->end_rewrite(const2bits);
}

4
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h
View file

@ -33,7 +33,9 @@ public:
ast_manager & m() const;
unsigned get_num_steps() const;
void cleanup();
obj_map<func_decl, expr*> const& const2bits() const;
obj_map<func_decl, expr*> const& const2bits() const;
void start_rewrite();
void end_rewrite(obj_map<func_decl, expr*>& const2bits);
void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
void push();
void pop(unsigned num_scopes);

34
src/opt/opt_parse.cpp
View file

@ -670,6 +670,14 @@ private:
return peek(pos) == "<=" || peek(pos) == "=<";
}
bool peek_minus_infty(unsigned pos) {
return peek(pos) == "-" && (peek(pos+1) == "inf" || peek(pos+1) == "infinity");
}
bool peek_plus_infty(unsigned pos) {
return peek(pos) == "+" && (peek(pos+1) == "inf" || peek(pos+1) == "infinity");
}
void parse_indicator(symbol& var, rational& val) {
if (peek(1) == "=" && tok.peek_num(2) && peek(3) == "->") {
var = peek(0);
@ -703,11 +711,15 @@ private:
v = peek(2);
update_lower(lhs, v);
tok.next(3);
if (peek_le(0) && tok.peek_num(1)) {
rational rhs = tok.get_num(1);
update_upper(v, rhs);
tok.next(2);
}
parse_upper(v);
}
else if (peek_minus_infty(0) && peek_le(2)) {
v = peek(3);
tok.next(4);
parse_upper(v);
}
else if (peek_plus_infty(2) && peek_le(1)) {
tok.next(4);
}
else if (peek_le(1) && tok.peek_num(2)) {
v = peek(0);
@ -721,6 +733,18 @@ private:
}
}
void parse_upper(symbol const& v) {
if (peek_le(0) && tok.peek_num(1)) {
rational rhs = tok.get_num(1);
update_upper(v, rhs);
tok.next(2);
}
else if (peek_le(0) && peek_plus_infty(1)) {
tok.next(3);
}
}
void update_lower(rational const& r, symbol const& v) {
bound b;
m_bounds.find(v, b);

460
src/sat/ba_solver.cpp
View file

@ -47,16 +47,6 @@ namespace sat {
return static_cast<pb const&>(*this);
}
ba_solver::eq& ba_solver::constraint::to_eq() {
SASSERT(is_eq());
return static_cast<eq&>(*this);
}
ba_solver::eq const& ba_solver::constraint::to_eq() const{
SASSERT(is_eq());
return static_cast<eq const&>(*this);
}
ba_solver::xr& ba_solver::constraint::to_xr() {
SASSERT(is_xr());
return static_cast<xr&>(*this);
@ -95,15 +85,6 @@ namespace sat {
}
break;
}
case ba_solver::eq_t: {
ba_solver::eq const& e = cnstr.to_eq();
for (ba_solver::eliteral wl : e) {
if (wl.weight != 1) out << wl.weight << " * ";
out << wl.lit << " ";
}
out << " = " << e.k();
break;
}
default:
UNREACHABLE();
}
@ -205,33 +186,6 @@ namespace sat {
}
// -----------------------------------
// eq
ba_solver::eq::eq(unsigned id, literal lit, svector<ba_solver::wliteral> const& wlits, unsigned k):
constraint(eq_t, id, lit, wlits.size(), eq::get_obj_size(wlits.size())),
m_lo(0),
m_hi(0),
m_max(0),
m_k(k)
{
unsigned i = 0;
for (wliteral const& w : wlits) {
m_wlits[i++] = eliteral(w.first, w.second);
m_max += w.first;
}
m_hi = m_max;
m_trail_sz = 0;
}
unsigned ba_solver::eq::index(literal l) const {
for (unsigned i = 0; i < size(); ++i) {
if (l.var() == m_wlits[i].lit.var()) return i;
}
UNREACHABLE();
return UINT_MAX;
}
// -----------------------------------
// xr
@ -271,7 +225,7 @@ namespace sat {
}
if (root != null_literal) {
if (!is_watched(root, c)) watch_literal(root, c);
if (!is_watched(~root, c)) watch_literal(~root, c);
if (!c.is_pure() && !is_watched(~root, c)) watch_literal(~root, c);
}
TRACE("ba", display(tout << "init watch: ", c, true););
SASSERT(root == null_literal || value(root) == l_true);
@ -925,251 +879,6 @@ namespace sat {
out << ">= " << p.k() << "\n";
}
// --------------------
// eq:
ba_solver::constraint* ba_solver::add_eq(literal lit, svector<wliteral> const& wlits, unsigned k, bool learned) {
void * mem = m_allocator.allocate(eq::get_obj_size(wlits.size()));
eq* e = new (mem) eq(next_id(), lit, wlits, k);
e->set_learned(learned);
add_constraint(e);
for (eliteral const& wl : *e) {
watch_literal(wl.lit, *e);
watch_literal(~(wl.lit), *e);
}
return e;
}
void ba_solver::display(std::ostream& out, eq const& e, bool values) const {
display_lit(out, e.lit(), e.size(), values);
if (values) {
if (e.trail_sz() > 0) {
out << "trail: ";
for (unsigned i = 0; i < e.trail_sz(); ++i) {
out << e[i].tweight << " * " << e[i].tlit << " ";
}
}
out << "[" << e.lo() << ":" << e.hi() << "] ";
}
for (eliteral wl : e) {
literal l = wl.lit;
unsigned w = wl.weight;
if (w > 1) out << w << " * ";
out << l;
if (values) {
out << "@(" << value(l);
if (value(l) != l_undef) {
out << ":" << lvl(l);
}
out << ") ";
}
else {
out << " ";
}
}
out << "= " << e.k() << "\n";
}
bool ba_solver::init_watch(eq& e) {
return true;
}
void ba_solver::clear_watch(eq& e) {
for (eliteral const& wl : e) {
unwatch_literal(wl.lit, e);
unwatch_literal(~(wl.lit), e);
}
if (e.lit() != null_literal) {
unwatch_literal(e.lit(), e);
unwatch_literal(~e.lit(), e);
}
}
/*
* \update the bounds for [lo,hi] based on what is unassigned on the trail.
*/
void ba_solver::pop_eq(eq& e) {
unsigned idx = e.trail_sz() - 1;
literal tlit = e[idx].tlit;
if (tlit.sign()) {
e.inc_hi(e[idx].tweight);
}
else {
e.dec_lo(e[idx].tweight);
}
e.set_trail_sz(idx);
}
lbool ba_solver::add_assign(eq& e, literal nl) {
//IF_VERBOSE(0, verbose_stream() << nl << "@" << lvl(nl) << ": " << e << "\n");
SASSERT(value(nl) == l_false);
if (nl.var() == e.lit().var()) {
// no-op
}
else {
unsigned i = e.index(nl);
eliteral wl = e[i];
if (wl.lit == nl) {
e.dec_hi(wl);
}
else {
SASSERT(wl.lit == ~nl);
e.inc_lo(wl);
}
m_eq_to_pop.push_back(&e);
}
if (e.lo() > e.k() || e.hi() < e.k()) {
if (e.lit() == null_literal || value(e.lit()) == l_true) {
set_conflict(e, nl);
return l_false;
}
if (e.lit() != null_literal && value(e.lit()) == l_undef) {
assign(e, ~e.lit());
}
}
else if (e.lo() == e.hi()) {
SASSERT(e.lo() == e.k());
if (e.lit() != null_literal && value(e.lit()) == l_false) {
set_conflict(e, nl);
return l_false;
}
if (e.lit() != null_literal && value(e.lit()) == l_undef) {
assign(e, e.lit());
}
}
else if ((e.lit() == null_literal || value(e.lit()) == l_true)) {
if (e.lo() == e.k()) {
for (eliteral el : e) {
if (value(el.lit) == l_undef) {
//IF_VERBOSE(0, display(verbose_stream() << "proapgate " << ~el.lit << " ", e, true));
assign(e, ~el.lit);
}
}
}
else if (e.hi() == e.k()) {
for (eliteral el : e) {
if (value(el.lit) == l_undef) {
//IF_VERBOSE(0, display(verbose_stream() << "proapgate " << el.lit << " ", e, true));
assign(e, el.lit);
}
}
}
}
return l_true;
}
void ba_solver::simplify(eq& e) {
// no-op for now
}
void ba_solver::recompile(eq& e) {
for (eliteral const& el : e) {
m_weights[el.lit.index()] += el.weight;
}
unsigned k = e.k(), sz = e.size();
unsigned j = 0;
bool is_false = false;
for (unsigned i = 0; i < sz; ++i) {
eliteral el = e[i];
unsigned w1 = m_weights[el.lit.index()];
unsigned w2 = m_weights[(~el.lit).index()];
if (w1 == 0 || w1 < w2) continue;
if (k < w2) {
is_false = true;
break;
}
k -= w2;
w1 -= w2;
if (w1 == 0) continue;
e[j++] = eliteral(w1, el.lit);
}
sz = j;
for (eliteral const& el : e) {
m_weights[el.lit.index()] = 0;
m_weights[(~el.lit).index()] = 0;
}
if (is_false) {
if (e.lit() == null_literal) {
s().mk_clause(0, 0, true);
}
else {
literal lit = ~e.lit();
s().mk_clause(1, &lit, true);
}
remove_constraint(e, "recompiled to false");
return;
}
// update trail
e.set_size(sz);
e.set_k(k);
for (unsigned i = 0; i < sz; ++i) {
e[i].tlit = null_literal;
}
e.set_trail_sz(0);
e.reset_lo();
e.reset_hi();
for (eliteral const& el : e) {
switch (value(el.lit)) {
case l_true: e.inc_lo(el); break;
case l_false: e.dec_hi(el); break;
default: break;
}
}
}
void ba_solver::split_root(eq& e) {
NOT_IMPLEMENTED_YET();
}
void ba_solver::get_antecedents(literal l, eq const& e, literal_vector& r) {
for (eliteral wl : e) {
if (wl.lit.var() == l.var()) continue;
switch (value(wl.lit)) {
case l_true: r.push_back(wl.lit); break;
case l_false: r.push_back(~wl.lit); break;
default: break;
}
}
if (e.lit() != null_literal && l.var() != e.lit().var()) {
switch (value(e.lit())) {
case l_true: r.push_back(e.lit()); break;
case l_false: r.push_back(~e.lit()); break;
default: break;
}
}
}
lbool ba_solver::eval(eq const& e) const {
unsigned trues = 0, undefs = 0;
for (eliteral wl : e) {
switch (value(wl.lit)) {
case l_true: trues += wl.weight; break;
case l_undef: undefs += wl.weight; break;
default: break;
}
}
if (trues + undefs < e.k()) return l_false;
if (trues > e.k()) return l_false;
if (trues == e.k() && undefs == 0) return l_true;
return l_undef;
}
lbool ba_solver::eval(model const& m, eq const& e) const {
unsigned trues = 0, undefs = 0;
for (eliteral wl : e) {
switch (value(m, wl.lit)) {
case l_true: trues += wl.weight; break;
case l_undef: undefs += wl.weight; break;
default: break;
}
}
if (trues + undefs < e.k()) return l_false;
if (trues > e.k()) return l_false;
if (trues == e.k() && undefs == 0) return l_true;
return l_undef;
}
// --------------------
// xr:
@ -1512,17 +1221,6 @@ namespace sat {
for (literal l : m_lemma) process_antecedent(~l, offset);
break;
}
case eq_t: {
eq& e = cnstr.to_eq();
m_lemma.reset();
inc_bound(offset);
inc_coeff(consequent, offset);
get_antecedents(consequent, e, m_lemma);
TRACE("ba", display(tout, e, true); tout << m_lemma << "\n";);
for (literal l : m_lemma) process_antecedent(~l, offset);
break;
}
default:
UNREACHABLE();
break;
@ -1888,7 +1586,6 @@ namespace sat {
case card_t: return init_watch(c.to_card());
case pb_t: return init_watch(c.to_pb());
case xr_t: return init_watch(c.to_xr());
case eq_t: return init_watch(c.to_eq());
}
UNREACHABLE();
return false;
@ -1899,7 +1596,6 @@ namespace sat {
case card_t: return add_assign(c.to_card(), l);
case pb_t: return add_assign(c.to_pb(), l);
case xr_t: return add_assign(c.to_xr(), l);
case eq_t: return add_assign(c.to_eq(), l);
}
UNREACHABLE();
return l_undef;
@ -1950,7 +1646,7 @@ namespace sat {
init_watch(c);
return true;
}
else if (c.lit() != null_literal && value(c.lit()) != l_true && c.tag() != eq_t) {
else if (c.lit() != null_literal && value(c.lit()) != l_true) {
return true;
}
else {
@ -2005,7 +1701,6 @@ namespace sat {
case card_t: return get_reward(c.to_card(), occs);
case pb_t: return get_reward(c.to_pb(), occs);
case xr_t: return 0;
case eq_t: return 1;
default: UNREACHABLE(); return 0;
}
}
@ -2310,6 +2005,7 @@ namespace sat {
}
void ba_solver::watch_literal(literal lit, constraint& c) {
if (c.is_pure() && lit == ~c.lit()) return;
get_wlist(~lit).push_back(watched(c.index()));
}
@ -2318,7 +2014,6 @@ namespace sat {
case card_t: get_antecedents(l, c.to_card(), r); break;
case pb_t: get_antecedents(l, c.to_pb(), r); break;
case xr_t: get_antecedents(l, c.to_xr(), r); break;
case eq_t: get_antecedents(l, c.to_eq(), r); break;
default: UNREACHABLE(); break;
}
}
@ -2342,9 +2037,6 @@ namespace sat {
case xr_t:
clear_watch(c.to_xr());
break;
case eq_t:
clear_watch(c.to_eq());
break;
default:
UNREACHABLE();
}
@ -2367,7 +2059,6 @@ namespace sat {
case card_t: return validate_unit_propagation(c.to_card(), l);
case pb_t: return validate_unit_propagation(c.to_pb(), l);
case xr_t: return true;
case eq_t: return validate_unit_propagation(c.to_eq(), l);
default: UNREACHABLE(); break;
}
return false;
@ -2383,7 +2074,6 @@ namespace sat {
case card_t: return eval(v1, eval(c.to_card()));
case pb_t: return eval(v1, eval(c.to_pb()));
case xr_t: return eval(v1, eval(c.to_xr()));
case eq_t: return eval(v1, eval(c.to_eq()));
default: UNREACHABLE(); break;
}
return l_undef;
@ -2395,7 +2085,6 @@ namespace sat {
case card_t: return eval(v1, eval(m, c.to_card()));
case pb_t: return eval(v1, eval(m, c.to_pb()));
case xr_t: return eval(v1, eval(m, c.to_xr()));
case eq_t: return eval(v1, eval(m, c.to_eq()));
default: UNREACHABLE(); break;
}
return l_undef;
@ -2730,7 +2419,6 @@ namespace sat {
void ba_solver::push() {
m_constraint_to_reinit_lim.push_back(m_constraint_to_reinit.size());
m_eq_to_pop_lim.push_back(m_eq_to_pop.size());
}
void ba_solver::pop(unsigned n) {
@ -2739,13 +2427,6 @@ namespace sat {
m_constraint_to_reinit_last_sz = m_constraint_to_reinit_lim[new_lim];
m_constraint_to_reinit_lim.shrink(new_lim);
m_num_propagations_since_pop = 0;
new_lim = m_eq_to_pop_lim.size() - n;
for (unsigned i = m_eq_to_pop_lim[new_lim]; i < m_eq_to_pop.size(); ++i) {
pop_eq(*m_eq_to_pop[i]);
}
m_eq_to_pop.shrink(m_eq_to_pop_lim[new_lim]);
m_eq_to_pop_lim.shrink(new_lim);
}
void ba_solver::pop_reinit() {
@ -2772,9 +2453,6 @@ namespace sat {
case xr_t:
simplify(c.to_xr());
break;
case eq_t:
simplify(c.to_eq());
break;
default:
UNREACHABLE();
}
@ -2798,6 +2476,7 @@ namespace sat {
for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]);
cleanup_clauses();
cleanup_constraints();
update_pure();
}
while (m_simplify_change || trail_sz < s().init_trail_size());
@ -2814,7 +2493,41 @@ namespace sat {
// IF_VERBOSE(0, s().display(verbose_stream()));
// mutex_reduction();
// if (s().m_clauses.size() < 80000) lp_lookahead_reduction();
}
/*
* ~lit does not occur in clauses
* ~lit is only in one constraint use list
* lit == C
* -> ignore assignemnts to ~lit for C
*
* ~lit does not occur in clauses
* lit is only in one constraint use list
* lit == C
* -> negate: ~lit == ~C
*/
void ba_solver::update_pure() {
// return;
for (constraint* cp : m_constraints) {
literal lit = cp->lit();
if (lit != null_literal &&
!cp->is_pure() &&
value(lit) == l_undef &&
get_wlist(~lit).size() == 1 &&
m_clause_use_list.get(lit).empty()) {
clear_watch(*cp);
cp->negate();
lit.neg();
}
if (lit != null_literal &&
!cp->is_pure() &&
m_cnstr_use_list[(~lit).index()].size() == 1 &&
get_wlist(lit).size() == 1 &&
m_clause_use_list.get(~lit).empty()) {
cp->set_pure();
get_wlist(~lit).erase(watched(cp->index())); // just ignore assignments to false
}
}
}
void ba_solver::mutex_reduction() {
@ -2930,9 +2643,6 @@ namespace sat {
case pb_t:
recompile(c.to_pb());
break;
case eq_t:
recompile(c.to_eq());
break;
case xr_t:
NOT_IMPLEMENTED_YET();
break;
@ -3144,7 +2854,6 @@ namespace sat {
case card_t: split_root(c.to_card()); break;
case pb_t: split_root(c.to_pb()); break;
case xr_t: NOT_IMPLEMENTED_YET(); break;
case eq_t: split_root(c.to_eq()); break;
}
}
@ -3265,15 +2974,6 @@ namespace sat {
}
break;
}
case eq_t: {
eq& e = cp->to_eq();
for (eliteral wl : e) {
literal l = wl.lit;
m_cnstr_use_list[l.index()].push_back(&e);
m_cnstr_use_list[(~l).index()].push_back(&e);
}
break;
}
}
}
}
@ -3296,8 +2996,6 @@ namespace sat {
}
break;
}
case eq_t:
break;
default:
break;
}
@ -3372,8 +3070,6 @@ namespace sat {
if (p.k() > 1) subsumption(p);
break;
}
case eq_t:
break;
default:
break;
}
@ -3464,30 +3160,32 @@ namespace sat {
return c1_exclusive + c2.k() + comp.size() <= c1.k();
}
bool ba_solver::subsumes(card& c1, clause& c2, literal_vector & comp) {
unsigned c2_exclusive = 0;
unsigned common = 0;
comp.reset();
/*
\brief L + A >= k subsumes L + C if |A| < k
A + L + B >= k self-subsumes A + ~L + C >= 1
if k + 1 - |B| - |C| - |L| > 0
*/
bool ba_solver::subsumes(card& c1, clause& c2, bool& self) {
unsigned common = 0, complement = 0, c2_exclusive = 0;
self = false;
for (literal l : c2) {
if (is_marked(l)) {
++common;
}
else if (is_marked(~l)) {
comp.push_back(l);
++complement;
}
else {
++c2_exclusive;
}
}
unsigned c1_exclusive = c1.size() - common - comp.size();
bool result = c1_exclusive + 1 <= c1.k();
if (!comp.empty() && result) {
IF_VERBOSE(10, verbose_stream() << "self-subsume clause " << c2 << " is TBD\n";);
return false;
unsigned c1_exclusive = c1.size() - common - complement;
if (complement > 0 && c1.k() + 1 > c1_exclusive + c2_exclusive + common) {
self = true;
return true;
}
return result;
return c1.size() - common < c1.k();
}
/*
@ -3517,8 +3215,6 @@ namespace sat {
case pb_t:
s = subsumes(p1, c->to_pb());
break;
case eq_t:
break;
default:
break;
}
@ -3582,23 +3278,22 @@ namespace sat {
void ba_solver::clause_subsumption(card& c1, literal lit, clause_vector& removed_clauses) {
SASSERT(!c1.was_removed());
literal_vector slit;
clause_use_list::iterator it = m_clause_use_list.get(lit).mk_iterator();
clause_use_list& occurs = m_clause_use_list.get(lit);
clause_use_list::iterator it = occurs.mk_iterator();
while (!it.at_end()) {
clause& c2 = it.curr();
if (!c2.was_removed() && subsumes(c1, c2, slit)) {
if (slit.empty()) {
bool self;
if (!c2.was_removed() && subsumes(c1, c2, self)) {
if (self) {
// self-subsumption is TBD
}
else {
TRACE("ba", tout << "remove\n" << c1 << "\n" << c2 << "\n";);
removed_clauses.push_back(&c2);
++m_stats.m_num_clause_subsumes;
c1.set_learned(false);
}
else {
IF_VERBOSE(11, verbose_stream() << "self-subsume clause is TBD\n";);
// remove literal slit from c2.
TRACE("ba", tout << "TBD remove literals " << slit << " from " << c2 << "\n";);
}
}
}
}
it.next();
}
}
@ -3615,7 +3310,7 @@ namespace sat {
watched w = *it;
if (w.is_binary_clause() && is_marked(w.get_literal())) {
++m_stats.m_num_bin_subsumes;
// IF_VERBOSE(10, verbose_stream() << c1 << " subsumes (" << lit << " " << w.get_literal() << ")\n";);
IF_VERBOSE(10, verbose_stream() << c1 << " subsumes (" << lit << " " << w.get_literal() << ")\n";);
if (!w.is_learned()) {
c1.set_learned(false);
}
@ -3745,15 +3440,6 @@ namespace sat {
result->add_xr(lits, x.learned());
break;
}
case eq_t: {
eq const& e = cp->to_eq();
wlits.reset();
for (eliteral w : e) {
wlits.push_back(wliteral(w.weight, w.lit));
}
result->add_eq(e.lit(), wlits, e.k(), e.learned());
break;
}
default:
UNREACHABLE();
}
@ -3791,14 +3477,6 @@ namespace sat {
}
break;
}
case eq_t: {
eq const& e = cp->to_eq();
for (eliteral w : e) {
ul.insert(w.lit, idx);
ul.insert(~(w.lit), idx);
}
break;
}
default:
UNREACHABLE();
}
@ -3840,8 +3518,6 @@ namespace sat {
}
return weight >= p.k();
}
case eq_t:
break;
default:
break;
}
@ -3963,7 +3639,6 @@ namespace sat {
case card_t: display(out, c.to_card(), values); break;
case pb_t: display(out, c.to_pb(), values); break;
case xr_t: display(out, c.to_xr(), values); break;
case eq_t: display(out, c.to_eq(), values); break;
default: UNREACHABLE(); break;
}
}
@ -4280,13 +3955,6 @@ namespace sat {
if (lxr != null_literal) ineq.push(~lxr, offset);
break;
}
case eq_t: {
eq& e = cnstr.to_eq();
ineq.reset(e.k());
for (eliteral wl : e) ineq.push(wl.lit, wl.weight);
if (e.lit() != null_literal) ineq.push(~e.lit(), e.k());
break;
}
default:
UNREACHABLE();
break;

87
src/sat/ba_solver.h
View file

@ -51,14 +51,12 @@ namespace sat {
enum tag_t {
card_t,
pb_t,
xr_t,
eq_t
xr_t
};
class card;
class pb;
class xr;
class eq;
class constraint {
protected:
@ -72,9 +70,10 @@ namespace sat {
size_t m_obj_size;
bool m_learned;
unsigned m_id;
bool m_pure; // is the constraint pure (only positive occurrences)
public:
constraint(tag_t t, unsigned id, literal l, unsigned sz, size_t osz):
m_tag(t), m_removed(false), m_lit(l), m_watch(null_literal), m_glue(0), m_psm(0), m_size(sz), m_obj_size(osz), m_learned(false), m_id(id) {}
m_tag(t), m_removed(false), m_lit(l), m_watch(null_literal), m_glue(0), m_psm(0), m_size(sz), m_obj_size(osz), m_learned(false), m_id(id), m_pure(false) {}
ext_constraint_idx index() const { return reinterpret_cast<ext_constraint_idx>(this); }
unsigned id() const { return m_id; }
tag_t tag() const { return m_tag; }
@ -95,20 +94,19 @@ namespace sat {
void set_watch() { m_watch = m_lit; }
void clear_watch() { m_watch = null_literal; }
bool is_clear() const { return m_watch == null_literal && m_lit != null_literal; }
bool is_pure() const { return m_pure; }
void set_pure() { m_pure = true; }
size_t obj_size() const { return m_obj_size; }
card& to_card();
pb& to_pb();
xr& to_xr();
eq& to_eq();
card const& to_card() const;
pb const& to_pb() const;
xr const& to_xr() const;
eq const& to_eq() const;
bool is_card() const { return m_tag == card_t; }
bool is_pb() const { return m_tag == pb_t; }
bool is_xr() const { return m_tag == xr_t; }
bool is_eq() const { return m_tag == eq_t; }
virtual bool is_watching(literal l) const { UNREACHABLE(); return false; };
virtual literal_vector literals() const { UNREACHABLE(); return literal_vector(); }
@ -185,60 +183,6 @@ namespace sat {
virtual unsigned get_coeff(unsigned i) const { return m_wlits[i].first; }
};
struct eliteral {
unsigned weight;
literal lit;
unsigned tweight;
literal tlit;
eliteral(unsigned w, literal lit):
weight(w), lit(lit), tweight(0), tlit(null_literal)
{}
eliteral(): weight(0), lit(null_literal), tweight(0), tlit(null_literal) {}
};
class eq : public constraint {
unsigned m_lo, m_hi, m_max, m_k, m_trail_sz;
eliteral m_wlits[0];
public:
static size_t get_obj_size(unsigned num_lits) { return sizeof(eq) + num_lits * sizeof(eliteral); }
eq(unsigned id, literal lit, svector<wliteral> const& wlits, unsigned k);
literal lit() const { return m_lit; }
eliteral operator[](unsigned i) const { return m_wlits[i]; }
eliteral& operator[](unsigned i) { return m_wlits[i]; }
eliteral const* begin() const { return m_wlits; }
eliteral const* end() const { return begin() + m_size; }
unsigned index(literal l) const;
unsigned k() const { return m_k; }
void reset_lo() { m_lo = 0; }
void reset_hi() { m_hi = m_max; }
unsigned lo() const { return m_lo; }
unsigned hi() const { return m_hi; }
void inc_hi(unsigned d) { m_hi += d; }
void dec_lo(unsigned d) { SASSERT(d <= m_lo); m_lo -= d; }
// increment/decrement lo/hi save delta and variable in a trail.
void inc_lo(eliteral const& e) {
m_lo += e.weight;
m_wlits[m_trail_sz].tlit = literal(e.lit.var(), false);
m_wlits[m_trail_sz++].tweight = e.weight;
}
void dec_hi(eliteral const& e) {
m_hi -= e.weight;
m_wlits[m_trail_sz].tlit = literal(e.lit.var(), true);
m_wlits[m_trail_sz++].tweight = e.weight;
}
unsigned trail_sz() const { return m_trail_sz; }
void set_trail_sz(unsigned sz) { m_trail_sz = sz; }
virtual void negate() { SASSERT(lit() != null_literal); m_lit.neg(); }
virtual void set_k(unsigned k) { m_k = k; }
virtual void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); }
virtual literal_vector literals() const { literal_vector lits; for (auto wl : *this) lits.push_back(wl.lit); return lits; }
virtual bool is_watching(literal l) const { return true; }
virtual literal get_lit(unsigned i) const { return m_wlits[i].lit; }
virtual void set_lit(unsigned i, literal l) { m_wlits[i].lit = l; }
virtual unsigned get_coeff(unsigned i) const { return m_wlits[i].weight; }
};
class xr : public constraint {
literal m_lits[0];
public:
@ -281,8 +225,6 @@ namespace sat {
unsigned_vector m_constraint_to_reinit_lim;
unsigned m_constraint_to_reinit_last_sz;
unsigned m_constraint_id;
ptr_vector<eq> m_eq_to_pop;
unsigned_vector m_eq_to_pop_lim;
// conflict resolution
unsigned m_num_marks;
@ -340,7 +282,7 @@ namespace sat {
unsigned_vector m_weights;
svector<wliteral> m_wlits;
bool subsumes(card& c1, card& c2, literal_vector& comp);
bool subsumes(card& c1, clause& c2, literal_vector& comp);
bool subsumes(card& c1, clause& c2, bool& self);
bool subsumed(card& c1, literal l1, literal l2);
bool subsumes(pb const& p1, pb_base const& p2);
void subsumes(pb& p1, literal lit);
@ -363,6 +305,7 @@ namespace sat {
void gc_half(char const* _method);
void update_psm(constraint& c) const;
void mutex_reduction();
void update_pure();
unsigned use_count(literal lit) const { return m_cnstr_use_list[lit.index()].size() + m_clause_use_list.get(lit).size(); }
@ -451,19 +394,6 @@ namespace sat {
lbool eval(model const& m, pb const& p) const;
double get_reward(pb const& p, literal_occs_fun& occs) const;
// eq functionality
void pop_eq(eq& e);
bool init_watch(eq& e);
void clear_watch(eq& e);
lbool add_assign(eq& e, literal alit);
void get_antecedents(literal l, eq const& e, literal_vector& r);
void simplify(eq& e);
void recompile(eq& e);
void split_root(eq& e);
void calibrate(eq& e);
lbool eval(eq const& e) const;
lbool eval(model const& m, eq const& e) const;
// access solver
inline lbool value(bool_var v) const { return value(literal(v, false)); }
inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); }
@ -541,13 +471,11 @@ namespace sat {
void display(std::ostream& out, card const& c, bool values) const;
void display(std::ostream& out, pb const& p, bool values) const;
void display(std::ostream& out, xr const& c, bool values) const;
void display(std::ostream& out, eq const& e, bool values) const;
void display_lit(std::ostream& out, literal l, unsigned sz, bool values) const;
constraint* add_at_least(literal l, literal_vector const& lits, unsigned k, bool learned);
constraint* add_pb_ge(literal l, svector<wliteral> const& wlits, unsigned k, bool learned);
constraint* add_xr(literal_vector const& lits, bool learned);
constraint* add_eq(literal l, svector<wliteral> const& wlits, unsigned k, bool learned);
void copy_core(ba_solver* result, bool learned);
void copy_constraints(ba_solver* result, ptr_vector<constraint> const& constraints);
@ -561,7 +489,6 @@ namespace sat {
void add_at_least(bool_var v, literal_vector const& lits, unsigned k);
void add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k);
void add_xr(literal_vector const& lits);
void add_eq(literal l, svector<wliteral> const& wlits, unsigned k) { add_eq(l, wlits, k, false); }
virtual bool propagate(literal l, ext_constraint_idx idx);
virtual lbool resolve_conflict();

2
src/sat/sat_asymm_branch.cpp
View file

@ -87,8 +87,6 @@ namespace sat {
IF_VERBOSE(1, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";);
if (num_elim == 0)
break;
if (false && num_elim > 1000)
i = 0;
}
IF_VERBOSE(1, if (m_elim_learned_literals > eliml0)
verbose_stream() << "(sat-asymm-branch :elim " << m_elim_learned_literals - eliml0 << ")\n";);

2
src/sat/sat_asymm_branch_params.pyg
View file

@ -2,7 +2,7 @@ def_module_params(module_name='sat',
class_name='sat_asymm_branch_params',
export=True,
params=(('asymm_branch', BOOL, True, 'asymmetric branching'),
('asymm_branch.rounds', UINT, 10, 'maximal number of rounds to run asymmetric branch simplifications if progress is made'),
('asymm_branch.rounds', UINT, 2, 'maximal number of rounds to run asymmetric branch simplifications if progress is made'),
('asymm_branch.delay', UINT, 1, 'number of simplification rounds to wait until invoking asymmetric branch simplification'),
('asymm_branch.sampled', BOOL, True, 'use sampling based asymmetric branching based on binary implication graph'),
('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching'),

6
src/sat/sat_big.cpp
View file

@ -169,6 +169,7 @@ namespace sat {
unsigned idx = 0;
unsigned elim = 0;
for (watch_list & wlist : s.m_watches) {
if (s.inconsistent()) break;
literal u = to_literal(idx++);
watch_list::iterator it = wlist.begin();
watch_list::iterator itprev = it;
@ -179,6 +180,10 @@ namespace sat {
literal v = w.get_literal();
if (reaches(u, v) && u != get_parent(v)) {
++elim;
if (find_binary_watch(wlist, ~v)) {
IF_VERBOSE(10, verbose_stream() << "binary: " << ~u << "\n");
s.assign(~u, justification());
}
// could turn non-learned non-binary tautology into learned binary.
s.get_wlist(~v).erase(watched(~u, w.is_learned()));
continue;
@ -189,6 +194,7 @@ namespace sat {
}
wlist.set_end(itprev);
}
s.propagate(false);
return elim;
}

4
src/sat/sat_config.cpp
View file

@ -72,6 +72,10 @@ namespace sat {
m_num_threads = p.threads();
m_local_search = p.local_search();
m_local_search_threads = p.local_search_threads();
if (p.local_search_mode() == symbol("gsat"))
m_local_search_mode = local_search_mode::gsat;
else
m_local_search_mode = local_search_mode::wsat;
m_unit_walk = p.unit_walk();
m_unit_walk_threads = p.unit_walk_threads();
m_lookahead_simplify = p.lookahead_simplify();

6
src/sat/sat_config.h
View file

@ -73,6 +73,11 @@ namespace sat {
adaptive_psat_cutoff
};
enum local_search_mode {
gsat,
wsat
};
struct config {
unsigned long long m_max_memory;
phase_selection m_phase;
@ -90,6 +95,7 @@ namespace sat {
unsigned m_num_threads;
unsigned m_local_search_threads;
bool m_local_search;
local_search_mode m_local_search_mode;
unsigned m_unit_walk_threads;
bool m_unit_walk;
bool m_lookahead_simplify;

2
src/sat/sat_elim_eqs.cpp
View file

@ -223,6 +223,7 @@ namespace sat {
}
void elim_eqs::operator()(literal_vector const & roots, bool_var_vector const & to_elim) {
TRACE("elim_eqs", tout << "before bin cleanup\n"; m_solver.display(tout););
cleanup_bin_watches(roots);
TRACE("elim_eqs", tout << "after bin cleanup\n"; m_solver.display(tout););
cleanup_clauses(roots, m_solver.m_clauses);
@ -232,5 +233,6 @@ namespace sat {
save_elim(roots, to_elim);
m_solver.propagate(false);
SASSERT(check_clauses(roots));
TRACE("elim_eqs", tout << "after full cleanup\n"; m_solver.display(tout););
}
};

35
src/sat/sat_local_search.cpp
View file

@ -72,9 +72,12 @@ namespace sat {
void local_search::init_cur_solution() {
for (unsigned v = 0; v < num_vars(); ++v) {
// use bias with a small probability
if (m_rand() % 100 < 2) {
if (m_rand() % 10 < 5) {
m_vars[v].m_value = ((unsigned)(m_rand() % 100) < m_vars[v].m_bias);
}
else {
m_vars[v].m_value = (m_rand() % 2) == 0;
}
}
}
@ -449,7 +452,6 @@ namespace sat {
m_best_unsat_rate = 1;
m_last_best_unsat_rate = 1;
reinit();
timer timer;
timer.start();
@ -457,20 +459,23 @@ namespace sat {
PROGRESS(tries, total_flips);
for (tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) {
if (m_unsat_stack.size() < m_best_unsat) {
m_best_unsat = m_unsat_stack.size();
m_last_best_unsat_rate = m_best_unsat_rate;
m_best_unsat_rate = (double)m_unsat_stack.size() / num_constraints();
}
for (step = 0; step < m_max_steps && !m_unsat_stack.empty(); ++step) {
pick_flip_walksat();
if (m_unsat_stack.size() < m_best_unsat) {
m_best_unsat = m_unsat_stack.size();
m_last_best_unsat_rate = m_best_unsat_rate;
m_best_unsat_rate = (double)m_unsat_stack.size() / num_constraints();
}
}
total_flips += step;
PROGRESS(tries, total_flips);
if (m_par && tries % 1 == 0) {
m_par->get_phase(*this);
if (m_par && m_par->get_phase(*this)) {
reinit();
}
if (tries % 10 == 0 && !m_unsat_stack.empty()) {
reinit();
}
}
}
@ -490,7 +495,10 @@ namespace sat {
if (m_best_objective_value >= m_best_known_value) {
break;
}
}
}
if (m_unsat_stack.size() < m_best_unsat) {
m_best_unsat = m_unsat_stack.size();
}
flipvar = pick_var_gsat();
flip_gsat(flipvar);
m_vars[flipvar].m_time_stamp = step++;
@ -563,6 +571,9 @@ namespace sat {
unsigned num_unsat = m_unsat_stack.size();
constraint const& c = m_constraints[m_unsat_stack[m_rand() % m_unsat_stack.size()]];
SASSERT(c.m_k < constraint_value(c));
unsigned reflipped = 0;
bool is_core = m_unsat_stack.size() <= 10;
reflip:
// TBD: dynamic noise strategy
//if (m_rand() % 100 < 98) {
if (m_rand() % 10000 <= m_noise) {
@ -635,6 +646,10 @@ namespace sat {
}
}
flip_walksat(best_var);
if (false && is_core && c.m_k < constraint_value(c)) {
++reflipped;
goto reflip;
}
}
void local_search::flip_walksat(bool_var flipvar) {

6
src/sat/sat_local_search.h
View file

@ -21,17 +21,13 @@
#include "util/vector.h"
#include "sat/sat_types.h"
#include "sat/sat_config.h"
#include "util/rlimit.h"
namespace sat {
class parallel;
enum local_search_mode {
gsat,
wsat
};
class local_search_config {
unsigned m_seed;
unsigned m_strategy_id;

7
src/sat/sat_parallel.cpp
View file

@ -229,7 +229,6 @@ namespace sat {
break;
}
}
IF_VERBOSE(1, verbose_stream() << "set phase: " << m_num_clauses << " " << s.m_clauses.size() << " " << m_solver_copy << "\n";);
}
if (m_consumer_ready && (m_num_clauses == 0 || (m_num_clauses > s.m_clauses.size()))) {
// time to update local search with new clauses.
@ -268,10 +267,13 @@ namespace sat {
}
}
void parallel::get_phase(local_search& s) {
bool parallel::get_phase(local_search& s) {
bool copied = false;
#pragma omp critical (par_solver)
{
m_consumer_ready = true;
if (m_solver_copy && s.num_non_binary_clauses() > m_solver_copy->m_clauses.size()) {
copied = true;
s.import(*m_solver_copy.get(), true);
}
for (unsigned i = 0; i < m_phase.size(); ++i) {
@ -280,6 +282,7 @@ namespace sat {
}
m_phase.reserve(s.num_vars(), l_undef);
}
return copied;
}
void parallel::set_phase(local_search& s) {

2
src/sat/sat_parallel.h
View file

@ -106,7 +106,7 @@ namespace sat {
void set_phase(local_search& s);
void get_phase(local_search& s);
bool get_phase(local_search& s);
bool copy_solver(solver& s);
};

1
src/sat/sat_params.pyg
View file

@ -38,6 +38,7 @@ def_module_params('sat',
('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'),
('local_search', BOOL, False, 'use local search instead of CDCL'),
('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
('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'),

1
src/sat/sat_scc.cpp
View file

@ -232,6 +232,7 @@ namespace sat {
if (m_scc_tr) {
reduce_tr();
}
TRACE("scc_detail", m_solver.display(tout););
return to_elim.size();
}

4
src/sat/sat_simplifier.cpp
View file

@ -198,7 +198,7 @@ namespace sat {
initialize();
CASSERT("sat_solver", s.check_invariant());
TRACE("before_simplifier", s.display(tout););
TRACE("sat_simplifier", s.display(tout););
s.m_cleaner(true);
TRACE("after_cleanup", s.display(tout););
@ -254,7 +254,7 @@ namespace sat {
}
CASSERT("sat_solver", s.check_invariant());
TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
TRACE("sat_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
finalize();

19
src/sat/sat_solver.cpp
View file

@ -332,6 +332,14 @@ namespace sat {
}
void solver::mk_bin_clause(literal l1, literal l2, bool learned) {
if (find_binary_watch(get_wlist(~l1), ~l2)) {
assign(l1, justification());
return;
}
if (find_binary_watch(get_wlist(~l2), ~l1)) {
assign(l2, justification());
return;
}
watched* w0 = find_binary_watch(get_wlist(~l1), l2);
if (w0) {
if (w0->is_learned() && !learned) {
@ -355,7 +363,7 @@ namespace sat {
}
m_stats.m_mk_bin_clause++;
get_wlist(~l1).push_back(watched(l2, learned));
get_wlist(~l2).push_back(watched(l1, learned));
get_wlist(~l2).push_back(watched(l1, learned));
}
bool solver::propagate_bin_clause(literal l1, literal l2) {
@ -1023,6 +1031,7 @@ namespace sat {
scoped_limits scoped_rl(rlimit());
local_search srch;
srch.config().set_seed(m_config.m_random_seed);
srch.config().set_mode(m_config.m_local_search_mode);
srch.import(*this, false);
scoped_rl.push_child(&srch.rlimit());
lbool r = srch.check(num_lits, lits, 0);
@ -1047,6 +1056,7 @@ namespace sat {
for (int i = 0; i < num_local_search; ++i) {
local_search* l = alloc(local_search);
l->config().set_seed(m_config.m_random_seed + i);
l->config().set_mode(m_config.m_local_search_mode);
l->import(*this, false);
ls.push_back(l);
}
@ -1095,7 +1105,7 @@ namespace sat {
r = par.get_solver(i).check(num_lits, lits);
}
else if (IS_LOCAL_SEARCH(i)) {
r = ls[i-local_search_offset]->check(num_lits, lits);
r = ls[i-local_search_offset]->check(num_lits, lits, &par);
}
else if (IS_UNIT_WALK(i)) {
r = uw[i-unit_walk_offset]->check(num_lits, lits);
@ -1519,9 +1529,9 @@ namespace sat {
m_scc();
CASSERT("sat_simplify_bug", check_invariant());
m_simplifier(false);
CASSERT("sat_simplify_bug", check_invariant());
CASSERT("sat_missed_prop", check_missed_propagation());
if (!m_learned.empty()) {
@ -1536,6 +1546,7 @@ namespace sat {
CASSERT("sat_missed_prop", check_missed_propagation());
CASSERT("sat_simplify_bug", check_invariant());
m_asymm_branch(false);
CASSERT("sat_missed_prop", check_missed_propagation());
CASSERT("sat_simplify_bug", check_invariant());
if (m_ext) {

81
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -60,7 +60,8 @@ class inc_sat_solver : public solver {
sat::literal_vector m_asms;
goal_ref_buffer m_subgoals;
proof_converter_ref m_pc;
mutable model_converter_ref m_mc0;
sref_vector<model_converter> m_mcs;
mutable model_converter_ref m_mc0; // TBD: should be saved/retained under push/pop
mutable obj_hashtable<func_decl> m_inserted_const2bits;
mutable ref<sat2goal::mc> m_sat_mc;
mutable model_converter_ref m_cached_mc;
@ -88,6 +89,7 @@ public:
m_internalized_converted(false),
m_internalized_fmls(m) {
updt_params(p);
m_mcs.push_back(nullptr);
init_preprocess();
m_solver.set_incremental(incremental_mode && !override_incremental());
}
@ -119,7 +121,7 @@ public:
for (unsigned a : m_asms_lim) result->m_asms_lim.push_back(a);
for (unsigned h : m_fmls_head_lim) result->m_fmls_head_lim.push_back(h);
for (expr* f : m_internalized_fmls) result->m_internalized_fmls.push_back(tr(f));
if (m_mc0) result->m_mc0 = m_mc0->translate(tr);
if (m_mcs.back()) result->m_mcs.push_back(m_mcs.back()->translate(tr));
if (m_sat_mc) result->m_sat_mc = dynamic_cast<sat2goal::mc*>(m_sat_mc->translate(tr));
// copy m_bb_rewriter?
result->m_internalized_converted = m_internalized_converted;
@ -186,6 +188,7 @@ public:
if (r != l_true) return r;
init_reason_unknown();
m_internalized_converted = false;
try {
// IF_VERBOSE(0, m_solver.display(verbose_stream()));
r = m_solver.check(m_asms.size(), m_asms.c_ptr());
@ -217,6 +220,7 @@ public:
internalize_formulas();
m_solver.user_push();
++m_num_scopes;
m_mcs.push_back(m_mcs.back());
m_fmls_lim.push_back(m_fmls.size());
m_asms_lim.push_back(m_asmsf.size());
m_fmls_head_lim.push_back(m_fmls_head);
@ -234,7 +238,9 @@ public:
SASSERT(n <= m_num_scopes);
m_solver.user_pop(n);
m_num_scopes -= n;
// ? m_internalized_converted = false;
while (n > 0) {
m_mcs.pop_back();
m_fmls_head = m_fmls_head_lim.back();
m_fmls.resize(m_fmls_lim.back());
m_fmls_lim.pop_back();
@ -448,12 +454,10 @@ public:
if (m_cached_mc)
return m_cached_mc;
if (is_internalized() && m_internalized_converted) {
insert_const2bits();
m_sat_mc->flush_smc(m_solver, m_map);
m_cached_mc = m_mc0.get();
m_cached_mc = m_mcs.back();
m_cached_mc = concat(solver::get_model_converter().get(), m_cached_mc.get());
m_cached_mc = concat(m_cached_mc.get(), m_sat_mc.get());
// IF_VERBOSE(0, m_cached_mc->display(verbose_stream() << "get-model-converter\n"););
return m_cached_mc;
}
else {
@ -493,12 +497,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),
and_then(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()),
//mk_aig_tactic(),
//mk_propagate_values_tactic(m, simp2_p),
mk_bit_blaster_tactic(m, m_bb_rewriter.get()), // updates model converter
using_params(mk_simplify_tactic(m), simp2_p));
while (m_bb_rewriter->get_num_scopes() < m_num_scopes) {
m_bb_rewriter->push();
@ -508,22 +510,6 @@ public:
private:
void insert_const2bits() const {
if (!m_bb_rewriter) return;
obj_map<func_decl, expr*> to_insert;
obj_map<func_decl, expr*> const& const2bits = m_bb_rewriter->const2bits();
for (auto const& kv : const2bits) {
if (!m_inserted_const2bits.contains(kv.m_key)) {
m_inserted_const2bits.insert(kv.m_key);
to_insert.insert(kv.m_key, kv.m_value);
}
}
if (!to_insert.empty()) {
m_mc0 = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, to_insert));
}
}
lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm, bool is_lemma) {
m_pc.reset();
m_subgoals.reset();
@ -543,15 +529,15 @@ private:
m_preprocess = 0;
m_bb_rewriter = 0;
return l_undef;
}
}
if (m_subgoals.size() != 1) {
IF_VERBOSE(0, verbose_stream() << "size of subgoals is not 1, it is: " << m_subgoals.size() << "\n";);
IF_VERBOSE(0, verbose_stream() << "size of subgoals is not 1, it is: " << m_subgoals.size() << "\n");
return l_undef;
}
g = m_subgoals[0];
expr_ref_vector atoms(m);
m_pc = g->pc();
m_mc0 = concat(m_mc0.get(), g->mc());
m_mcs.set(m_mcs.size()-1, concat(m_mcs.back(), g->mc()));
TRACE("sat", g->display_with_dependencies(tout););
// ensure that if goal is already internalized, then import mc from m_solver.
@ -591,8 +577,8 @@ private:
}
lbool internalize_vars(expr_ref_vector const& vars, sat::bool_var_vector& bvars) {
for (unsigned i = 0; i < vars.size(); ++i) {
internalize_var(vars[i], bvars);
for (expr* v : vars) {
internalize_var(v, bvars);
}
return l_true;
}
@ -604,7 +590,6 @@ private:
bool internalized = false;
if (is_uninterp_const(v) && m.is_bool(v)) {
sat::bool_var b = m_map.to_bool_var(v);
if (b != sat::null_bool_var) {
bvars.push_back(b);
internalized = true;
@ -614,10 +599,9 @@ private:
SASSERT(bvutil.is_bv(bv));
app* abv = to_app(bv);
internalized = true;
unsigned sz = abv->get_num_args();
for (unsigned j = 0; j < sz; ++j) {
SASSERT(is_uninterp_const(abv->get_arg(j)));
sat::bool_var b = m_map.to_bool_var(abv->get_arg(j));
for (expr* arg : *abv) {
SASSERT(is_uninterp_const(arg));
sat::bool_var b = m_map.to_bool_var(arg);
if (b == sat::null_bool_var) {
internalized = false;
}
@ -625,7 +609,7 @@ private:
bvars.push_back(b);
}
}
CTRACE("sat", internalized, tout << "var: "; for (unsigned j = 0; j < sz; ++j) tout << bvars[bvars.size()-sz+j] << " "; tout << "\n";);
CTRACE("sat", internalized, tout << "var: " << bvars << "\n";);
}
else if (is_uninterp_const(v) && bvutil.is_bv(v)) {
// variable does not occur in assertions, so is unconstrained.
@ -813,18 +797,18 @@ private:
//IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "satmc\n"););
(*m_sat_mc)(mdl);
}
insert_const2bits();
if (m_mc0) {
if (m_mcs.back()) {
//IF_VERBOSE(0, m_mc0->display(verbose_stream() << "mc0\n"););
(*m_mc0)(mdl);
(*m_mcs.back())(mdl);
}
TRACE("sat", model_smt2_pp(tout, m, *mdl, 0););
// IF_VERBOSE(0, model_smt2_pp(verbose_stream() << "after\n", m, *mdl, 0););
#if 0
IF_VERBOSE(0, verbose_stream() << "Verifying solution\n";);
IF_VERBOSE(0, verbose_streamm() << "Verifying solution\n";);
model_evaluator eval(*mdl);
bool all_true = true;
for (expr * f : m_fmls) {
expr_ref tmp(m);
eval(f, tmp);
@ -833,13 +817,20 @@ private:
model_smt2_pp(tout, m, *(mdl.get()), 0););
if (!m.is_true(tmp)) {
IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(f, m) << "\n";);
IF_VERBOSE(0, verbose_stream() << m_params << "\n";);
IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "sat mc\n"););
IF_VERBOSE(0, if (m_mc0) m_mc0->display(verbose_stream() << "mc0\n"););
break;
all_true = false;
}
else {
VERIFY(m.is_true(tmp));
}
VERIFY(m.is_true(tmp));
}
if (!all_true) {
IF_VERBOSE(0, verbose_stream() << m_params << "\n";);
IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "sat mc\n"););
IF_VERBOSE(0, if (m_mcs.back()) m_mcs.back()->display(verbose_stream() << "mc0\n"););
//IF_VERBOSE(0, m_solver.display(verbose_stream()));
IF_VERBOSE(0, for (auto const& kv : m_map) verbose_stream() << mk_pp(kv.m_key, m) << " |-> " << kv.m_value << "\n";);
}
#endif
}
};

23
src/sat/tactic/goal2sat.cpp
View file

@ -573,28 +573,6 @@ struct goal2sat::imp {
void convert_eq_k(app* t, rational const& k, bool root, bool sign) {
SASSERT(k.is_unsigned());
#if 0
IF_VERBOSE(0, verbose_stream() << t->get_id() << ": " << mk_pp(t, m) << "\n";);
svector<wliteral> wlits;
convert_pb_args(t, wlits);
if (root && !sign) {
m_ext->add_eq(sat::null_literal, wlits, k.get_unsigned());
m_result_stack.reset();
}
else {
sat::bool_var v = m_solver.mk_var();
sat::literal l(v, false);
m_ext->add_eq(l, wlits, k.get_unsigned());
m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
m_cache.insert(t, l);
if (sign) l.neg();
m_result_stack.push_back(l);
if (root) {
mk_clause(l);
m_result_stack.reset();
}
}
#else
sat::literal_vector lits;
convert_pb_args(t->get_num_args(), lits);
sat::bool_var v1 = (root && !sign) ? sat::null_bool_var : m_solver.mk_var(true);
@ -625,7 +603,6 @@ struct goal2sat::imp {
m_result_stack.reset();
}
}
#endif
}
void ensure_extension() {

12
src/tactic/bv/bit_blaster_tactic.cpp
View file

@ -62,6 +62,7 @@ class bit_blaster_tactic : public tactic {
TRACE("before_bit_blaster", g->display(tout););
m_num_steps = 0;
m_rewriter->start_rewrite();
expr_ref new_curr(m());
proof_ref new_pr(m());
unsigned size = g->size();
@ -78,13 +79,16 @@ class bit_blaster_tactic : public tactic {
}
if (curr != new_curr) {
change = true;
TRACE("bit_blaster", tout << mk_pp(curr, m()) << " -> " << mk_pp(new_curr, m()) << "\n";);
TRACE("bit_blaster", tout << mk_pp(curr, m()) << " -> " << new_curr << "\n";);
g->update(idx, new_curr, new_pr, g->dep(idx));
}
}
if (change && g->models_enabled())
g->add(mk_bit_blaster_model_converter(m(), m_rewriter->const2bits()));
if (change && g->models_enabled()) {
obj_map<func_decl, expr*> const2bits;
m_rewriter->end_rewrite(const2bits);
g->add(mk_bit_blaster_model_converter(m(), const2bits));
}
g->inc_depth();
result.push_back(g.get());
TRACE("after_bit_blaster", g->display(tout); if (g->mc()) g->mc()->display(tout); tout << "\n";);
@ -148,6 +152,7 @@ public:
return m_imp->get_num_steps();
}
};
@ -158,3 +163,4 @@ tactic * mk_bit_blaster_tactic(ast_manager & m, params_ref const & p) {
tactic * mk_bit_blaster_tactic(ast_manager & m, bit_blaster_rewriter* rw, params_ref const & p) {
return clean(alloc(bit_blaster_tactic, m, rw, p));
}