mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

updated sat_smt

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-29 19:21:39 -07:00
parent e9a4e486ae
commit 86310a1a27
15 changed files with 389 additions and 437 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_extension.h
View file

@ -75,7 +75,6 @@ namespace sat {
virtual std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const = 0;
virtual void collect_statistics(statistics& st) const = 0;
virtual extension* copy(solver* s) = 0;
virtual extension* copy(lookahead* s, bool learned) = 0;
virtual void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) = 0;
virtual void gc() = 0;
virtual void pop_reinit() = 0;

4
src/sat/sat_lookahead.cpp
View file

@ -22,7 +22,6 @@ Notes:
#include <cmath>
#include "sat/sat_solver.h"
#include "sat/sat_extension.h"
#include "sat/sat_lookahead.h"
#include "sat/sat_scc.h"
#include "util/union_find.h"
@ -1037,9 +1036,6 @@ namespace sat {
}
}
if (m_s.m_ext) {
// m_ext = m_s.m_ext->copy(this, learned);
}
propagate();
m_qhead = m_trail.size();
m_init_freevars = m_freevars.size();

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

@ -126,7 +126,7 @@ public:
auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
if (ext) {
auto& si = result->m_goal2sat.si(dst_m, m_params, result->m_solver, result->m_map, result->m_dep2asm, is_incremental());
euf::solver::scoped_set_translate st(*ext, tr, result->m_map, si);
euf::solver::scoped_set_translate st(*ext, dst_m, result->m_map, si);
result->m_solver.copy(m_solver);
}
else {

133
src/sat/smt/ba_internalize.cpp
View file

@ -3,7 +3,7 @@ Copyright (c) 2020 Microsoft Corporation
Module Name:
ba_internalize.h
ba_core.h
Abstract:
@ -16,12 +16,13 @@ Author:
--*/
#include "sat/smt/ba_internalize.h"
#include "sat/smt/ba_solver.h"
#include "ast/pb_decl_plugin.h"
namespace sat {
literal ba_internalize::internalize(expr* e, bool sign, bool root) {
if (pb.is_pb(e))
literal ba_solver::internalize(expr* e, bool sign, bool root) {
if (m_pb.is_pb(e))
return internalize_pb(e, sign, root);
if (m.is_xor(e))
return internalize_xor(e, sign, root);
@ -29,13 +30,13 @@ namespace sat {
return null_literal;
}
literal ba_internalize::internalize_xor(expr* e, bool sign, bool root) {
literal ba_solver::internalize_xor(expr* e, bool sign, bool root) {
sat::literal_vector lits;
sat::bool_var v = m_solver.add_var(true);
sat::bool_var v = s().add_var(true);
lits.push_back(literal(v, true));
auto add_expr = [&](expr* a) {
literal lit = si.internalize(a);
m_solver.set_external(lit.var());
s().set_external(lit.var());
lits.push_back(lit);
};
expr* e1 = nullptr;
@ -46,34 +47,34 @@ namespace sat {
for (unsigned i = 1; i + 1 < lits.size(); ++i) {
lits[i].neg();
}
ba.add_xr(lits);
auto* aig = m_solver.get_cut_simplifier();
add_xr(lits);
auto* aig = s().get_cut_simplifier();
if (aig) aig->add_xor(~lits.back(), lits.size() - 1, lits.c_ptr() + 1);
sat::literal lit(v, sign);
return literal(v, sign);
}
literal ba_internalize::internalize_pb(expr* e, bool sign, bool root) {
SASSERT(pb.is_pb(e));
literal ba_solver::internalize_pb(expr* e, bool sign, bool root) {
SASSERT(m_pb.is_pb(e));
app* t = to_app(e);
rational k = pb.get_k(t);
rational k = m_pb.get_k(t);
switch (t->get_decl_kind()) {
case OP_AT_MOST_K:
return convert_at_most_k(t, k, root, sign);
case OP_AT_LEAST_K:
return convert_at_least_k(t, k, root, sign);
case OP_PB_LE:
if (pb.has_unit_coefficients(t))
if (m_pb.has_unit_coefficients(t))
return convert_at_most_k(t, k, root, sign);
else
return convert_pb_le(t, root, sign);
case OP_PB_GE:
if (pb.has_unit_coefficients(t))
if (m_pb.has_unit_coefficients(t))
return convert_at_least_k(t, k, root, sign);
else
return convert_pb_ge(t, root, sign);
case OP_PB_EQ:
if (pb.has_unit_coefficients(t))
if (m_pb.has_unit_coefficients(t))
return convert_eq_k(t, k, root, sign);
else
return convert_pb_eq(t, root, sign);
@ -83,35 +84,35 @@ namespace sat {
return null_literal;
}
void ba_internalize::check_unsigned(rational const& c) {
void ba_solver::check_unsigned(rational const& c) {
if (!c.is_unsigned()) {
throw default_exception("unsigned coefficient expected");
}
}
void ba_internalize::convert_to_wlits(app* t, sat::literal_vector const& lits, svector<wliteral>& wlits) {
void ba_solver::convert_to_wlits(app* t, sat::literal_vector const& lits, svector<wliteral>& wlits) {
for (unsigned i = 0; i < lits.size(); ++i) {
rational c = pb.get_coeff(t, i);
rational c = m_pb.get_coeff(t, i);
check_unsigned(c);
wlits.push_back(std::make_pair(c.get_unsigned(), lits[i]));
}
}
void ba_internalize::convert_pb_args(app* t, literal_vector& lits) {
void ba_solver::convert_pb_args(app* t, literal_vector& lits) {
for (expr* arg : *t) {
lits.push_back(si.internalize(arg));
m_solver.set_external(lits.back().var());
s().set_external(lits.back().var());
}
}
void ba_internalize::convert_pb_args(app* t, svector<wliteral>& wlits) {
void ba_solver::convert_pb_args(app* t, svector<wliteral>& wlits) {
sat::literal_vector lits;
convert_pb_args(t, lits);
convert_to_wlits(t, lits, wlits);
}
literal ba_internalize::convert_pb_le(app* t, bool root, bool sign) {
rational k = pb.get_k(t);
literal ba_solver::convert_pb_le(app* t, bool root, bool sign) {
rational k = m_pb.get_k(t);
k.neg();
svector<wliteral> wlits;
convert_pb_args(t, wlits);
@ -120,7 +121,7 @@ namespace sat {
k += rational(wl.first);
}
check_unsigned(k);
if (root && m_solver.num_user_scopes() == 0) {
if (root && s().num_user_scopes() == 0) {
unsigned k1 = k.get_unsigned();
if (sign) {
k1 = 1 - k1;
@ -129,25 +130,25 @@ namespace sat {
k1 += wl.first;
}
}
ba.add_pb_ge(null_bool_var, wlits, k1);
add_pb_ge(null_bool_var, wlits, k1);
return null_literal;
}
else {
bool_var v = m_solver.add_var(true);
bool_var v = s().add_var(true);
literal lit(v, sign);
ba.add_pb_ge(v, wlits, k.get_unsigned());
add_pb_ge(v, wlits, k.get_unsigned());
TRACE("ba", tout << "root: " << root << " lit: " << lit << "\n";);
return lit;
}
}
literal ba_internalize::convert_pb_ge(app* t, bool root, bool sign) {
rational k = pb.get_k(t);
literal ba_solver::convert_pb_ge(app* t, bool root, bool sign) {
rational k = m_pb.get_k(t);
check_unsigned(k);
svector<wliteral> wlits;
convert_pb_args(t, wlits);
if (root && m_solver.num_user_scopes() == 0) {
if (root && s().num_user_scopes() == 0) {
unsigned k1 = k.get_unsigned();
if (sign) {
k1 = 1 - k1;
@ -156,40 +157,40 @@ namespace sat {
k1 += wl.first;
}
}
ba.add_pb_ge(sat::null_bool_var, wlits, k1);
add_pb_ge(sat::null_bool_var, wlits, k1);
return null_literal;
}
else {
sat::bool_var v = m_solver.add_var(true);
sat::bool_var v = s().add_var(true);
sat::literal lit(v, sign);
ba.add_pb_ge(v, wlits, k.get_unsigned());
add_pb_ge(v, wlits, k.get_unsigned());
TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
return lit;
}
}
literal ba_internalize::convert_pb_eq(app* t, bool root, bool sign) {
rational k = pb.get_k(t);
literal ba_solver::convert_pb_eq(app* t, bool root, bool sign) {
rational k = m_pb.get_k(t);
SASSERT(k.is_unsigned());
svector<wliteral> wlits;
convert_pb_args(t, wlits);
bool base_assert = (root && !sign && m_solver.num_user_scopes() == 0);
bool_var v1 = base_assert ? null_bool_var : m_solver.add_var(true);
bool_var v2 = base_assert ? null_bool_var : m_solver.add_var(true);
ba.add_pb_ge(v1, wlits, k.get_unsigned());
bool base_assert = (root && !sign && s().num_user_scopes() == 0);
bool_var v1 = base_assert ? null_bool_var : s().add_var(true);
bool_var v2 = base_assert ? null_bool_var : s().add_var(true);
add_pb_ge(v1, wlits, k.get_unsigned());
k.neg();
for (wliteral& wl : wlits) {
wl.second.neg();
k += rational(wl.first);
}
check_unsigned(k);
ba.add_pb_ge(v2, wlits, k.get_unsigned());
add_pb_ge(v2, wlits, k.get_unsigned());
if (base_assert) {
return null_literal;
}
else {
literal l1(v1, false), l2(v2, false);
bool_var v = m_solver.add_var(false);
bool_var v = s().add_var(false);
literal l(v, false);
si.mk_clause(~l, l1);
si.mk_clause(~l, l2);
@ -200,23 +201,23 @@ namespace sat {
}
}
literal ba_internalize::convert_at_least_k(app* t, rational const& k, bool root, bool sign) {
literal ba_solver::convert_at_least_k(app* t, rational const& k, bool root, bool sign) {
SASSERT(k.is_unsigned());
literal_vector lits;
convert_pb_args(t, lits);
unsigned k2 = k.get_unsigned();
if (root && m_solver.num_user_scopes() == 0) {
if (root && s().num_user_scopes() == 0) {
if (sign) {
for (literal& l : lits) l.neg();
k2 = lits.size() + 1 - k2;
}
ba.add_at_least(null_bool_var, lits, k2);
add_at_least(null_bool_var, lits, k2);
return null_literal;
}
else {
bool_var v = m_solver.add_var(true);
bool_var v = s().add_var(true);
literal lit(v, false);
ba.add_at_least(v, lits, k.get_unsigned());
add_at_least(v, lits, k.get_unsigned());
si.cache(t, lit);
if (sign) lit.neg();
TRACE("ba", tout << "root: " << root << " lit: " << lit << "\n";);
@ -224,7 +225,7 @@ namespace sat {
}
}
literal ba_internalize::convert_at_most_k(app* t, rational const& k, bool root, bool sign) {
literal ba_solver::convert_at_most_k(app* t, rational const& k, bool root, bool sign) {
SASSERT(k.is_unsigned());
literal_vector lits;
convert_pb_args(t, lits);
@ -232,39 +233,39 @@ namespace sat {
l.neg();
}
unsigned k2 = lits.size() - k.get_unsigned();
if (root && m_solver.num_user_scopes() == 0) {
if (root && s().num_user_scopes() == 0) {
if (sign) {
for (literal& l : lits) l.neg();
k2 = lits.size() + 1 - k2;
}
ba.add_at_least(null_bool_var, lits, k2);
add_at_least(null_bool_var, lits, k2);
return null_literal;
}
else {
bool_var v = m_solver.add_var(true);
bool_var v = s().add_var(true);
literal lit(v, false);
ba.add_at_least(v, lits, k2);
add_at_least(v, lits, k2);
si.cache(t, lit);
if (sign) lit.neg();
return lit;
}
}
literal ba_internalize::convert_eq_k(app* t, rational const& k, bool root, bool sign) {
literal ba_solver::convert_eq_k(app* t, rational const& k, bool root, bool sign) {
SASSERT(k.is_unsigned());
literal_vector lits;
convert_pb_args(t, lits);
bool_var v1 = (root && !sign) ? null_bool_var : m_solver.add_var(true);
bool_var v2 = (root && !sign) ? null_bool_var : m_solver.add_var(true);
ba.add_at_least(v1, lits, k.get_unsigned());
bool_var v1 = (root && !sign) ? null_bool_var : s().add_var(true);
bool_var v2 = (root && !sign) ? null_bool_var : s().add_var(true);
add_at_least(v1, lits, k.get_unsigned());
for (literal& l : lits) {
l.neg();
}
ba.add_at_least(v2, lits, lits.size() - k.get_unsigned());
add_at_least(v2, lits, lits.size() - k.get_unsigned());
if (!root || sign) {
literal l1(v1, false), l2(v2, false);
bool_var v = m_solver.add_var(false);
bool_var v = s().add_var(false);
literal l(v, false);
si.mk_clause(~l, l1);
si.mk_clause(~l, l2);
@ -278,12 +279,12 @@ namespace sat {
}
}
expr_ref ba_decompile::get_card(std::function<expr_ref(sat::literal)>& lit2expr, ba_solver::card const& c) {
expr_ref ba_solver::get_card(std::function<expr_ref(sat::literal)>& lit2expr, ba_solver::card const& c) {
ptr_buffer<expr> lits;
for (sat::literal l : c) {
lits.push_back(lit2expr(l));
}
expr_ref fml(pb.mk_at_least_k(c.size(), lits.c_ptr(), c.k()), m);
expr_ref fml(m_pb.mk_at_least_k(c.size(), lits.c_ptr(), c.k()), m);
if (c.lit() != sat::null_literal) {
fml = m.mk_eq(lit2expr(c.lit()), fml);
@ -291,7 +292,7 @@ namespace sat {
return fml;
}
expr_ref ba_decompile::get_pb(std::function<expr_ref(sat::literal)>& lit2expr, ba_solver::pb const& p) {
expr_ref ba_solver::get_pb(std::function<expr_ref(sat::literal)>& lit2expr, ba_solver::pb const& p) {
ptr_buffer<expr> lits;
vector<rational> coeffs;
for (auto const& wl : p) {
@ -299,7 +300,7 @@ namespace sat {
coeffs.push_back(rational(wl.first));
}
rational k(p.k());
expr_ref fml(pb.mk_ge(p.size(), coeffs.c_ptr(), lits.c_ptr(), k), m);
expr_ref fml(m_pb.mk_ge(p.size(), coeffs.c_ptr(), lits.c_ptr(), k), m);
if (p.lit() != sat::null_literal) {
fml = m.mk_eq(lit2expr(p.lit()), fml);
@ -307,7 +308,7 @@ namespace sat {
return fml;
}
expr_ref ba_decompile::get_xor(std::function<expr_ref(sat::literal)>& lit2expr, ba_solver::xr const& x) {
expr_ref ba_solver::get_xor(std::function<expr_ref(sat::literal)>& lit2expr, ba_solver::xr const& x) {
ptr_buffer<expr> lits;
for (sat::literal l : x) {
lits.push_back(lit2expr(l));
@ -320,16 +321,16 @@ namespace sat {
return fml;
}
bool ba_decompile::to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) {
for (auto* c : ba.constraints()) {
bool ba_solver::to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) {
for (auto* c : constraints()) {
switch (c->tag()) {
case ba_solver::card_t:
fmls.push_back(get_card(l2e, c->to_card()));
break;
case sat::ba_solver::pb_t:
case ba_solver::pb_t:
fmls.push_back(get_pb(l2e, c->to_pb()));
break;
case sat::ba_solver::xr_t:
case ba_solver::xr_t:
fmls.push_back(get_xor(l2e, c->to_xr()));
break;
}

73
src/sat/smt/ba_internalize.h
View file

@ -1,73 +0,0 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
ba_internalize.h
Abstract:
INternalize methods for Boolean algebra operators.
Author:
Nikolaj Bjorner (nbjorner) 2020-08-25
--*/
#pragma once
#include "sat/smt/sat_th.h"
#include "sat/smt/ba_solver.h"
#include "ast/pb_decl_plugin.h"
namespace sat {
class ba_internalize : public th_internalizer {
typedef std::pair<unsigned, literal> wliteral;
ast_manager& m;
pb_util pb;
ba_solver& ba;
solver_core& m_solver;
sat_internalizer& si;
literal convert_eq_k(app* t, rational const& k, bool root, bool sign);
literal convert_at_most_k(app* t, rational const& k, bool root, bool sign);
literal convert_at_least_k(app* t, rational const& k, bool root, bool sign);
literal convert_pb_eq(app* t, bool root, bool sign);
literal convert_pb_le(app* t, bool root, bool sign);
literal convert_pb_ge(app* t, bool root, bool sign);
void check_unsigned(rational const& c);
void convert_to_wlits(app* t, sat::literal_vector const& lits, svector<wliteral>& wlits);
void convert_pb_args(app* t, svector<wliteral>& wlits);
void convert_pb_args(app* t, literal_vector& lits);
literal internalize_pb(expr* e, bool sign, bool root);
literal internalize_xor(expr* e, bool sign, bool root);
public:
ba_internalize(ba_solver& ba, solver_core& s, sat_internalizer& si, ast_manager& m) :
m(m), pb(m), ba(ba), m_solver(s), si(si) {}
~ba_internalize() override {}
literal internalize(expr* e, bool sign, bool root) override;
};
class ba_decompile : public sat::th_decompile {
ast_manager& m;
ba_solver& ba;
solver_core& m_solver;
pb_util pb;
expr_ref get_card(std::function<expr_ref(sat::literal)>& l2e, ba_solver::card const& c);
expr_ref get_pb(std::function<expr_ref(sat::literal)>& l2e, ba_solver::pb const& p);
expr_ref get_xor(std::function<expr_ref(sat::literal)>& l2e, ba_solver::xr const& x);
public:
ba_decompile(ba_solver& ba, solver_core& s, ast_manager& m) :
m(m), ba(ba), m_solver(s), pb(m) {}
~ba_decompile() override {}
bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override;
};
}

68
src/sat/smt/ba_solver.cpp
View file

@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation
Module Name:
ba_solver.cpp
ba_core.cpp
Abstract:
@ -119,8 +119,8 @@ namespace sat {
// ----------------------
// card
ba_solver::card::card(extension* e, unsigned id, literal lit, literal_vector const& lits, unsigned k):
pb_base(e, card_t, id, lit, lits.size(), get_obj_size(lits.size()), k) {
ba_solver::card::card(unsigned id, literal lit, literal_vector const& lits, unsigned k):
pb_base(card_t, id, lit, lits.size(), get_obj_size(lits.size()), k) {
for (unsigned i = 0; i < size(); ++i) {
m_lits[i] = lits[i];
}
@ -146,8 +146,8 @@ namespace sat {
// -----------------------------------
// pb
ba_solver::pb::pb(extension* e, unsigned id, literal lit, svector<ba_solver::wliteral> const& wlits, unsigned k):
pb_base(e, pb_t, id, lit, wlits.size(), get_obj_size(wlits.size()), k),
ba_solver::pb::pb(unsigned id, literal lit, svector<ba_solver::wliteral> const& wlits, unsigned k):
pb_base(pb_t, id, lit, wlits.size(), get_obj_size(wlits.size()), k),
m_slack(0),
m_num_watch(0),
m_max_sum(0) {
@ -302,7 +302,7 @@ namespace sat {
SASSERT(validate_conflict(c));
if (c.is_xr() && value(lit) == l_true) lit.neg();
SASSERT(value(lit) == l_false);
set_conflict(justification::mk_ext_justification(s().scope_lvl(), c.index()), ~lit);
set_conflict(justification::mk_ext_justification(s().scope_lvl(), c.cindex()), ~lit);
SASSERT(inconsistent());
}
@ -327,7 +327,7 @@ namespace sat {
ps.push_back(drat::premise(drat::s_ext(), c.lit())); // null_literal case.
drat_add(lits, ps);
}
assign(lit, justification::mk_ext_justification(s().scope_lvl(), c.index()));
assign(lit, justification::mk_ext_justification(s().scope_lvl(), c.cindex()));
break;
}
}
@ -1730,21 +1730,21 @@ namespace sat {
return p;
}
ba_solver::ba_solver()
: m_solver(nullptr), m_lookahead(nullptr),
ba_solver::ba_solver(ast_manager& m, sat_internalizer& si)
: m(m), si(si), m_pb(m),
m_solver(nullptr), m_lookahead(nullptr),
m_constraint_id(0), m_ba(*this), m_sort(m_ba) {
TRACE("ba", tout << this << "\n";);
std::cout << "mk " << this << "\n";
m_num_propagations_since_pop = 0;
}
ba_solver::~ba_solver() {
m_stats.reset();
for (constraint* c : m_constraints) {
m_allocator.deallocate(c->obj_size(), c);
c->deallocate(m_allocator);
}
for (constraint* c : m_learned) {
m_allocator.deallocate(c->obj_size(), c);
c->deallocate(m_allocator);
}
}
@ -1763,7 +1763,8 @@ namespace sat {
return nullptr;
}
void * mem = m_allocator.allocate(card::get_obj_size(lits.size()));
card* c = new (mem) card(this, next_id(), lit, lits, k);
constraint_base::initialize(mem, this);
card* c = new (constraint_base::ptr2mem(mem)) card(next_id(), lit, lits, k);
c->set_learned(learned);
add_constraint(c);
return c;
@ -1832,7 +1833,8 @@ namespace sat {
return add_at_least(lit, lits, k, learned);
}
void * mem = m_allocator.allocate(pb::get_obj_size(wlits.size()));
pb* p = new (mem) pb(this, next_id(), lit, wlits, k);
constraint_base::initialize(mem, this);
pb* p = new (constraint_base::ptr2mem(mem)) pb(next_id(), lit, wlits, k);
p->set_learned(learned);
add_constraint(p);
return p;
@ -2108,11 +2110,11 @@ namespace sat {
}
bool ba_solver::is_watched(literal lit, constraint const& c) const {
return get_wlist(~lit).contains(watched(c.index()));
return get_wlist(~lit).contains(watched(c.cindex()));
}
void ba_solver::unwatch_literal(literal lit, constraint& c) {
watched w(c.index());
watched w(c.cindex());
get_wlist(~lit).erase(w);
SASSERT(!is_watched(lit, c));
}
@ -2120,7 +2122,7 @@ namespace sat {
void ba_solver::watch_literal(literal lit, constraint& c) {
if (c.is_pure() && lit == ~c.lit()) return;
SASSERT(!is_watched(lit, c));
watched w(c.index());
watched w(c.cindex());
get_wlist(~lit).push_back(w);
}
@ -2425,7 +2427,7 @@ namespace sat {
constraint* c = m_learned[i];
if (!m_constraint_to_reinit.contains(c)) {
remove_constraint(*c, "gc");
m_allocator.deallocate(c->obj_size(), c);
c->deallocate(m_allocator);
++removed;
}
else {
@ -2639,7 +2641,7 @@ namespace sat {
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
get_wlist(~lit).erase(watched(cp->cindex())); // just ignore assignments to false
}
}
}
@ -3403,7 +3405,7 @@ namespace sat {
if (c.was_removed()) {
clear_watch(c);
nullify_tracking_literal(c);
m_allocator.deallocate(c.obj_size(), &c);
c.deallocate(m_allocator);
}
else if (learned && !c.learned()) {
m_constraints.push_back(&c);
@ -3537,10 +3539,10 @@ namespace sat {
}
card& c2 = c->to_card();
SASSERT(c1.index() != c2.index());
SASSERT(&c1 != &c2);
if (subsumes(c1, c2, slit)) {
if (slit.empty()) {
TRACE("ba", tout << "subsume cardinality\n" << c1 << "\n" << c2.index() << ":" << c2 << "\n";);
TRACE("ba", tout << "subsume cardinality\n" << c1 << "\n" << c2 << "\n";);
remove_constraint(c2, "subsumed");
++m_stats.m_num_pb_subsumes;
set_non_learned(c1);
@ -3713,22 +3715,14 @@ namespace sat {
}
extension* ba_solver::copy(solver* s) {
ba_solver* result = alloc(ba_solver);
return fresh(s, m, si);
}
th_solver* ba_solver::fresh(solver* s, ast_manager& m, sat_internalizer& si) {
ba_solver* result = alloc(ba_solver, m, si);
result->set_solver(s);
copy_core(result, false);
return result;
}
extension* ba_solver::copy(lookahead* s, bool learned) {
ba_solver* result = alloc(ba_solver);
result->set_lookahead(s);
copy_core(result, learned);
return result;
}
void ba_solver::copy_core(ba_solver* result, bool learned) {
copy_constraints(result, m_constraints);
if (learned) copy_constraints(result, m_learned);
return result;
}
void ba_solver::copy_constraints(ba_solver* result, ptr_vector<constraint> const& constraints) {
@ -3768,7 +3762,7 @@ namespace sat {
void ba_solver::init_use_list(ext_use_list& ul) {
ul.init(s().num_vars());
for (constraint const* cp : m_constraints) {
ext_constraint_idx idx = cp->index();
ext_constraint_idx idx = cp->cindex();
if (cp->lit() != null_literal) {
ul.insert(cp->lit(), idx);
ul.insert(~cp->lit(), idx);

68
src/sat/smt/ba_solver.h
View file

@ -25,15 +25,17 @@ Revision History:
#include "sat/sat_lookahead.h"
#include "sat/sat_big.h"
#include "sat/smt/sat_smt.h"
#include "sat/smt/sat_th.h"
#include "util/small_object_allocator.h"
#include "util/scoped_ptr_vector.h"
#include "util/sorting_network.h"
#include "ast/pb_decl_plugin.h"
namespace sat {
class xor_finder;
class ba_solver : public extension {
class ba_solver : public th_solver {
friend class local_search;
@ -65,7 +67,7 @@ namespace sat {
class xr;
class pb_base;
class constraint : public index_base {
class constraint {
protected:
tag_t m_tag;
bool m_removed;
@ -79,19 +81,11 @@ namespace sat {
unsigned m_id;
bool m_pure; // is the constraint pure (only positive occurrences)
public:
constraint(extension* e, tag_t t, unsigned id, literal l, unsigned sz, size_t osz):
index_base(e),
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_pure(false) {
std::cout << "constraint ext: " << t << " " << e << "\n";
size_t idx = reinterpret_cast<ext_constraint_idx>(this);
std::cout << "index " << idx << "\n";
std::cout << this << " " << index_base::from_index(idx) << "\n";
std::cout << e << " " << index_base::to_extension(idx) << "\n";
std::cout.flush();
}
ext_constraint_idx index() const {
return reinterpret_cast<ext_constraint_idx>(this);
}
ext_constraint_idx cindex() const { return constraint_base::mem2base(this); }
void deallocate(small_object_allocator& a) { a.deallocate(obj_size(), constraint_base::mem2base_ptr(this)); }
unsigned id() const { return m_id; }
tag_t tag() const { return m_tag; }
literal lit() const { return m_lit; }
@ -143,8 +137,8 @@ namespace sat {
protected:
unsigned m_k;
public:
pb_base(extension* e, tag_t t, unsigned id, literal l, unsigned sz, size_t osz, unsigned k):
constraint(e, t, id, l, sz, osz), m_k(k) { VERIFY(k < 4000000000); }
pb_base(tag_t t, unsigned id, literal l, unsigned sz, size_t osz, unsigned k):
constraint(t, id, l, sz, osz), m_k(k) { VERIFY(k < 4000000000); }
virtual void set_k(unsigned k) { VERIFY(k < 4000000000); m_k = k; }
virtual unsigned get_coeff(unsigned i) const { UNREACHABLE(); return 0; }
unsigned k() const { return m_k; }
@ -154,8 +148,8 @@ namespace sat {
class card : public pb_base {
literal m_lits[0];
public:
static size_t get_obj_size(unsigned num_lits) { return sizeof(card) + num_lits * sizeof(literal); }
card(extension* e, unsigned id, literal lit, literal_vector const& lits, unsigned k);
static size_t get_obj_size(unsigned num_lits) { return constraint_base::obj_size(sizeof(card) + num_lits * sizeof(literal)); }
card(unsigned id, literal lit, literal_vector const& lits, unsigned k);
literal operator[](unsigned i) const { return m_lits[i]; }
literal& operator[](unsigned i) { return m_lits[i]; }
literal const* begin() const { return m_lits; }
@ -178,8 +172,8 @@ namespace sat {
unsigned m_max_sum;
wliteral m_wlits[0];
public:
static size_t get_obj_size(unsigned num_lits) { return sizeof(pb) + num_lits * sizeof(wliteral); }
pb(extension* e, unsigned id, literal lit, svector<wliteral> const& wlits, unsigned k);
static size_t get_obj_size(unsigned num_lits) { return constraint_base::obj_size(sizeof(pb) + num_lits * sizeof(wliteral)); }
pb(unsigned id, literal lit, svector<wliteral> const& wlits, unsigned k);
literal lit() const { return m_lit; }
wliteral operator[](unsigned i) const { return m_wlits[i]; }
wliteral& operator[](unsigned i) { return m_wlits[i]; }
@ -206,8 +200,8 @@ namespace sat {
class xr : public constraint {
literal m_lits[0];
public:
static size_t get_obj_size(unsigned num_lits) { return sizeof(xr) + num_lits * sizeof(literal); }
xr(extension* e, unsigned id, literal_vector const& lits);
static size_t get_obj_size(unsigned num_lits) { return constraint_base::obj_size(sizeof(xr) + num_lits * sizeof(literal)); }
xr(unsigned id, literal_vector const& lits);
literal operator[](unsigned i) const { return m_lits[i]; }
literal const* begin() const { return m_lits; }
literal const* end() const { return begin() + m_size; }
@ -238,6 +232,10 @@ namespace sat {
bool contains(literal l) const { for (auto wl : m_wlits) if (wl.second == l) return true; return false; }
};
ast_manager& m;
sat_internalizer& si;
pb_util m_pb;
solver* m_solver;
lookahead* m_lookahead;
stats m_stats;
@ -343,7 +341,7 @@ namespace sat {
void remove_constraint(constraint& c, char const* reason);
// constraints
constraint& index2constraint(size_t idx) const { return *reinterpret_cast<constraint*>(idx); }
constraint& index2constraint(size_t idx) const { return *reinterpret_cast<constraint*>(constraint_base::from_index(idx)->mem()); }
void pop_constraint();
void unwatch_literal(literal w, constraint& c);
void watch_literal(literal w, constraint& c);
@ -545,8 +543,27 @@ namespace sat {
void copy_core(ba_solver* result, bool learned);
void copy_constraints(ba_solver* result, ptr_vector<constraint> const& constraints);
// Internalize
literal convert_eq_k(app* t, rational const& k, bool root, bool sign);
literal convert_at_most_k(app* t, rational const& k, bool root, bool sign);
literal convert_at_least_k(app* t, rational const& k, bool root, bool sign);
literal convert_pb_eq(app* t, bool root, bool sign);
literal convert_pb_le(app* t, bool root, bool sign);
literal convert_pb_ge(app* t, bool root, bool sign);
void check_unsigned(rational const& c);
void convert_to_wlits(app* t, sat::literal_vector const& lits, svector<wliteral>& wlits);
void convert_pb_args(app* t, svector<wliteral>& wlits);
void convert_pb_args(app* t, literal_vector& lits);
literal internalize_pb(expr* e, bool sign, bool root);
literal internalize_xor(expr* e, bool sign, bool root);
// Decompile
expr_ref get_card(std::function<expr_ref(sat::literal)>& l2e, ba_solver::card const& c);
expr_ref get_pb(std::function<expr_ref(sat::literal)>& l2e, ba_solver::pb const& p);
expr_ref get_xor(std::function<expr_ref(sat::literal)>& l2e, ba_solver::xr const& x);
public:
ba_solver();
ba_solver(ast_manager& m, sat_internalizer& si);
~ba_solver() override;
void set_solver(solver* s) override { m_solver = s; }
void set_lookahead(lookahead* l) override { m_lookahead = l; }
@ -572,7 +589,6 @@ namespace sat {
std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const override;
void collect_statistics(statistics& st) const override;
extension* copy(solver* s) override;
extension* copy(lookahead* s, bool learned) override;
void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override;
void pop_reinit() override;
void gc() override;
@ -583,6 +599,10 @@ namespace sat {
bool is_blocked(literal l, ext_constraint_idx idx) override;
bool check_model(model const& m) const override;
literal internalize(expr* e, bool sign, bool root) override;
bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override;
th_solver* fresh(solver* s, ast_manager& m, sat_internalizer& si) override;
ptr_vector<constraint> const & constraints() const { return m_constraints; }
std::ostream& display(std::ostream& out, constraint const& c, bool values) const;

18
src/sat/smt/euf_model.cpp
View file

@ -30,20 +30,10 @@ namespace euf {
values2model(deps, values, mdl);
}
sat::th_model_builder* solver::get_model_builder(expr* e) const {
if (is_app(e))
return get_model_builder(to_app(e)->get_decl());
return nullptr;
}
sat::th_model_builder* solver::get_model_builder(func_decl* f) const {
return m_id2model_builder.get(f->get_family_id(), nullptr);
}
bool solver::include_func_interp(func_decl* f) const {
bool solver::include_func_interp(func_decl* f) {
if (f->get_family_id() == null_family_id)
return true;
sat::th_model_builder* mb = get_model_builder(f);
sat::th_model_builder* mb = get_solver(f);
return mb && mb->include_func_interp(f);
}
@ -53,7 +43,7 @@ namespace euf {
deps.insert(n, nullptr);
continue;
}
auto* mb = get_model_builder(n->get_owner());
auto* mb = get_solver(n->get_owner());
if (mb)
mb->add_dep(n, deps);
else
@ -87,7 +77,7 @@ namespace euf {
}
continue;
}
auto* mb = get_model_builder(e);
auto* mb = get_solver(e);
if (mb)
mb->add_value(n, values);
else if (m.is_uninterp(m.get_sort(e))) {

194
src/sat/smt/euf_solver.cpp
View file

@ -20,7 +20,6 @@ Author:
#include "sat/sat_solver.h"
#include "sat/smt/sat_smt.h"
#include "sat/smt/ba_solver.h"
#include "sat/smt/ba_internalize.h"
#include "sat/smt/euf_solver.h"
namespace euf {
@ -32,54 +31,52 @@ namespace euf {
/**
* retrieve extension that is associated with Boolean variable.
*/
sat::extension* solver::get_extension(sat::bool_var v) {
sat::th_solver* solver::get_solver(sat::bool_var v) {
if (v >= m_var2node.size())
return nullptr;
euf::enode* n = m_var2node[v].first;
if (!n)
return nullptr;
return get_extension(n->get_owner());
return get_solver(n->get_owner());
}
void solver::add_extension(family_id fid, sat::extension* e) {
m_extensions.push_back(e);
m_id2extension.setx(fid, e, nullptr);
}
sat::extension* solver::get_extension(expr* e) {
if (is_app(e)) {
auto fid = to_app(e)->get_family_id();
if (fid == null_family_id)
return nullptr;
auto* ext = m_id2extension.get(fid, nullptr);
if (ext)
return ext;
pb_util pb(m);
if (pb.is_pb(e)) {
auto* ba = alloc(sat::ba_solver);
ba->set_solver(m_solver);
add_extension(pb.get_family_id(), ba);
auto* bai = alloc(sat::ba_internalize, *ba, s(), si, m);
m_id2internalize.setx(pb.get_family_id(), bai, nullptr);
m_internalizers.push_back(bai);
m_decompilers.push_back(alloc(sat::ba_decompile, *ba, s(), m));
ba->push_scopes(s().num_scopes());
std::cout << "extension ba " << ba << "\n";
return ba;
}
}
sat::th_solver* solver::get_solver(expr* e) {
if (is_app(e))
return fid2solver(to_app(e)->get_family_id());
return nullptr;
}
sat::th_solver* solver::fid2solver(family_id fid) {
if (fid == null_family_id)
return nullptr;
auto* ext = m_id2solver.get(fid, nullptr);
if (ext)
return ext;
pb_util pb(m);
if (pb.get_family_id() == fid) {
sat::ba_solver* ba = alloc(sat::ba_solver, m, si);
ba->set_solver(m_solver);
add_solver(pb.get_family_id(), ba);
ba->push_scopes(s().num_scopes());
return ba;
}
return nullptr;
}
void solver::add_solver(family_id fid, sat::th_solver* th) {
m_solvers.push_back(th);
m_id2solver.setx(fid, th, nullptr);
}
bool solver::propagate(literal l, ext_constraint_idx idx) {
auto* ext = sat::index_base::to_extension(idx);
std::cout << "extension " << ext << " " << idx << "\n";
auto* ext = sat::constraint_base::to_extension(idx);
SASSERT(ext != this);
return ext->propagate(l, idx);
}
void solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector& r) {
auto* ext = sat::index_base::to_extension(idx);
auto* ext = sat::constraint_base::to_extension(idx);
if (ext == this)
get_antecedents(l, *constraint::from_idx(idx), r);
else
@ -110,7 +107,7 @@ namespace euf {
break;
case 2:
SASSERT(m.is_bool(n->get_owner()));
m_egraph.explain_eq<unsigned>(m_explain, n, (sign ? m_false : m_true), false);
m_egraph.explain_eq<unsigned>(m_explain, n, (sign ? mk_false() : mk_true()), false);
break;
default:
UNREACHABLE();
@ -120,7 +117,7 @@ namespace euf {
}
void solver::asserted(literal l) {
auto* ext = get_extension(l.var());
auto* ext = get_solver(l.var());
if (ext) {
ext->asserted(l);
return;
@ -138,7 +135,7 @@ namespace euf {
m_egraph.merge(na, nb, base_ptr() + l.index());
}
else {
euf::enode* nb = sign ? m_false : m_true;
euf::enode* nb = sign ? mk_false() : mk_true();
m_egraph.merge(n, nb, base_ptr() + l.index());
}
// TBD: delay propagation?
@ -148,7 +145,7 @@ namespace euf {
void solver::propagate() {
m_egraph.propagate();
if (m_egraph.inconsistent()) {
s().set_conflict(sat::justification::mk_ext_justification(s().scope_lvl(), m_conflict_idx.to_index()));
s().set_conflict(sat::justification::mk_ext_justification(s().scope_lvl(), conflict_constraint().to_index()));
return;
}
for (euf::enode* eq : m_egraph.new_eqs()) {
@ -156,7 +153,7 @@ namespace euf {
expr* a = nullptr, *b = nullptr;
if (s().value(v) == l_false && m_ackerman && m.is_eq(eq->get_owner(), a, b))
m_ackerman->cg_conflict_eh(a, b);
s().assign(literal(v, false), sat::justification::mk_ext_justification(s().scope_lvl(), m_eq_idx.to_index()));
s().assign(literal(v, false), sat::justification::mk_ext_justification(s().scope_lvl(), eq_constraint().to_index()));
}
for (euf::enode* p : m_egraph.new_lits()) {
expr* e = p->get_owner();
@ -167,14 +164,31 @@ namespace euf {
literal lit(v, sign);
if (s().value(lit) == l_false && m_ackerman)
m_ackerman->cg_conflict_eh(p->get_owner(), p->get_root()->get_owner());
s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), m_lit_idx.to_index()));
s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), lit_constraint().to_index()));
}
}
constraint& solver::mk_constraint(constraint*& c, unsigned id) {
if (!c) {
void* mem = memory::allocate(sat::constraint_base::obj_size(sizeof(constraint)));
c = new (sat::constraint_base::ptr2mem(mem)) constraint(id);
sat::constraint_base::initialize(mem, this);
}
return *c;
}
enode* solver::mk_true() {
return visit(m.mk_true());
}
enode* solver::mk_false() {
return visit(m.mk_false());
}
sat::check_result solver::check() {
bool give_up = false;
bool cont = false;
for (auto* e : m_extensions)
for (auto* e : m_solvers)
switch (e->check()) {
case sat::CR_CONTINUE: cont = true; break;
case sat::CR_GIVEUP: give_up = true; break;
@ -188,7 +202,7 @@ namespace euf {
}
void solver::push() {
for (auto* e : m_extensions)
for (auto* e : m_solvers)
e->push();
m_egraph.push();
++m_num_scopes;
@ -196,7 +210,7 @@ namespace euf {
void solver::pop(unsigned n) {
m_egraph.pop(n);
for (auto* e : m_extensions)
for (auto* e : m_solvers)
e->pop(n);
if (n <= m_num_scopes) {
m_num_scopes -= n;
@ -212,24 +226,24 @@ namespace euf {
}
void solver::pre_simplify() {
for (auto* e : m_extensions)
for (auto* e : m_solvers)
e->pre_simplify();
}
void solver::simplify() {
for (auto* e : m_extensions)
for (auto* e : m_solvers)
e->simplify();
if (m_ackerman)
m_ackerman->propagate();
}
void solver::clauses_modifed() {
for (auto* e : m_extensions)
for (auto* e : m_solvers)
e->clauses_modifed();
}
lbool solver::get_phase(bool_var v) {
auto* ext = get_extension(v);
auto* ext = get_solver(v);
if (ext)
return ext->get_phase(v);
return l_undef;
@ -237,20 +251,20 @@ namespace euf {
std::ostream& solver::display(std::ostream& out) const {
m_egraph.display(out);
for (auto* e : m_extensions)
for (auto* e : m_solvers)
e->display(out);
return out;
}
std::ostream& solver::display_justification(std::ostream& out, ext_justification_idx idx) const {
auto* ext = sat::index_base::to_extension(idx);
auto* ext = sat::constraint_base::to_extension(idx);
if (ext != this)
return ext->display_justification(out, idx);
return out;
}
std::ostream& solver::display_constraint(std::ostream& out, ext_constraint_idx idx) const {
auto* ext = sat::index_base::to_extension(idx);
auto* ext = sat::constraint_base::to_extension(idx);
if (ext != this)
return ext->display_constraint(out, idx);
return out;
@ -258,89 +272,68 @@ namespace euf {
void solver::collect_statistics(statistics& st) const {
m_egraph.collect_statistics(st);
for (auto* e : m_extensions)
for (auto* e : m_solvers)
e->collect_statistics(st);
st.update("euf dynack", m_stats.m_num_dynack);
}
solver* solver::copy_core() {
ast_manager& to = m_translate ? m_translate->to() : m;
atom2bool_var& a2b = m_translate_expr2var ? *m_translate_expr2var : m_expr2var;
sat::sat_internalizer& to_si = m_translate_si ? *m_translate_si : si;
auto* r = alloc(solver, to, a2b, to_si);
r->m_config = m_config;
std::function<void*(void*)> copy_justification = [&](void* x) { return (void*)(r->base_ptr() + ((unsigned*)x - base_ptr())); };
r->m_egraph.copy_from(m_egraph, copy_justification);
return r;
}
sat::extension* solver::copy(sat::solver* s) {
auto* r = copy_core();
r->set_solver(s);
for (unsigned i = 0; i < m_id2extension.size(); ++i) {
auto* e = m_id2extension[i];
if (e)
r->add_extension(i, e->copy(s));
}
return r;
}
sat::extension* solver::copy(sat::lookahead* s, bool learned) {
(void) learned;
auto* r = copy_core();
r->set_lookahead(s);
for (unsigned i = 0; i < m_id2extension.size(); ++i) {
auto* e = m_id2extension[i];
if (e)
r->add_extension(i, e->copy(s, learned));
}
auto* r = alloc(solver, *m_to_m, *m_to_expr2var, *m_to_si);
r->m_config = m_config;
std::function<void* (void*)> copy_justification = [&](void* x) { return (void*)(r->base_ptr() + ((unsigned*)x - base_ptr())); };
r->m_egraph.copy_from(m_egraph, copy_justification);
r->set_solver(s);
for (unsigned i = 0; i < m_id2solver.size(); ++i) {
auto* e = m_id2solver[i];
if (e)
r->add_solver(i, e->fresh(s, *m_to_m, *m_to_si));
}
return r;
}
void solver::find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) {
for (auto* e : m_extensions)
for (auto* e : m_solvers)
e->find_mutexes(lits, mutexes);
}
void solver::gc() {
for (auto* e : m_extensions)
for (auto* e : m_solvers)
e->gc();
}
void solver::pop_reinit() {
for (auto* e : m_extensions)
for (auto* e : m_solvers)
e->pop_reinit();
}
bool solver::validate() {
for (auto* e : m_extensions)
for (auto* e : m_solvers)
if (!e->validate())
return false;
return true;
}
void solver::init_use_list(sat::ext_use_list& ul) {
for (auto* e : m_extensions)
for (auto* e : m_solvers)
e->init_use_list(ul);
}
bool solver::is_blocked(literal l, ext_constraint_idx idx) {
auto* ext = sat::index_base::to_extension(idx);
auto* ext = sat::constraint_base::to_extension(idx);
if (ext != this)
return is_blocked(l, idx);
return false;
}
bool solver::check_model(sat::model const& m) const {
for (auto* e : m_extensions)
for (auto* e : m_solvers)
if (!e->check_model(m))
return false;
return true;
}
unsigned solver::max_var(unsigned w) const {
for (auto* e : m_extensions)
for (auto* e : m_solvers)
w = e->max_var(w);
for (unsigned sz = m_var2node.size(); sz-- > 0; ) {
euf::enode* n = m_var2node[sz].first;
@ -368,25 +361,10 @@ namespace euf {
m_egraph.set_used_cc(used_cc);
}
sat::th_internalizer* solver::get_internalizer(expr* e) {
if (is_app(e))
return m_id2internalize.get(to_app(e)->get_family_id(), nullptr);
if (m.is_iff(e)) {
pb_util pb(m);
return m_id2internalize.get(pb.get_family_id(), nullptr);
}
return nullptr;
}
sat::literal solver::internalize(expr* e, bool sign, bool root) {
auto* ext = get_internalizer(e);
auto* ext = get_solver(e);
if (ext)
return ext->internalize(e, sign, root);
if (!m_true) {
m_true = visit(m.mk_true());
m_false = visit(m.mk_false());
}
std::cout << mk_pp(e, m) << "\n";
SASSERT(!si.is_bool_op(e));
sat::scoped_stack _sc(m_stack);
@ -466,7 +444,7 @@ namespace euf {
}
bool solver::to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) {
for (auto* th : m_decompilers) {
for (auto* th : m_solvers) {
if (!th->to_formulas(l2e, fmls))
return false;
}
@ -479,9 +457,7 @@ namespace euf {
bool solver::extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) {
if (m_true)
return false;
for (auto* e : m_extensions)
for (auto* e : m_solvers)
if (!e->extract_pb(card, pb))
return false;
return true;

79
src/sat/smt/euf_solver.h
View file

@ -33,14 +33,15 @@ namespace euf {
typedef sat::literal_vector literal_vector;
typedef sat::bool_var bool_var;
class constraint : public sat::index_base {
class constraint {
unsigned m_id;
public:
constraint(sat::extension* e, unsigned id) :
index_base(e), m_id(id)
constraint(unsigned id) :
m_id(id)
{}
unsigned id() const { return m_id; }
static constraint* from_idx(size_t z) { return reinterpret_cast<constraint*>(z); }
size_t to_index() const { return sat::constraint_base::mem2base(this); }
};
class solver : public sat::extension, public sat::th_internalizer, public sat::th_decompile {
@ -60,13 +61,11 @@ namespace euf {
stats m_stats;
sat::solver* m_solver { nullptr };
sat::lookahead* m_lookahead { nullptr };
ast_translation* m_translate { nullptr };
atom2bool_var* m_translate_expr2var { nullptr };
sat::sat_internalizer* m_translate_si{ nullptr };
scoped_ptr<ackerman> m_ackerman;
ast_manager* m_to_m { nullptr };
atom2bool_var* m_to_expr2var { nullptr };
sat::sat_internalizer* m_to_si{ nullptr };
scoped_ptr<ackerman> m_ackerman;
euf::enode* m_true { nullptr };
euf::enode* m_false { nullptr };
svector<euf::enode_bool_pair> m_var2node;
ptr_vector<unsigned> m_explain;
euf::enode_vector m_args;
@ -74,35 +73,33 @@ namespace euf {
unsigned m_num_scopes { 0 };
unsigned_vector m_bool_var_trail;
unsigned_vector m_bool_var_lim;
scoped_ptr_vector<sat::extension> m_extensions;
ptr_vector<sat::extension> m_id2extension;
ptr_vector<sat::th_internalizer> m_id2internalize;
scoped_ptr_vector<sat::th_internalizer> m_internalizers;
scoped_ptr_vector<sat::th_model_builder> m_model_builders;
ptr_vector<sat::th_model_builder> m_id2model_builder;
scoped_ptr_vector<sat::th_decompile> m_decompilers;
constraint m_conflict_idx, m_eq_idx, m_lit_idx;
scoped_ptr_vector<sat::th_solver> m_solvers;
ptr_vector<sat::th_solver> m_id2solver;
constraint* m_conflict { nullptr };
constraint* m_eq { nullptr };
constraint* m_lit { nullptr };
sat::solver& s() { return *m_solver; }
unsigned * base_ptr() { return reinterpret_cast<unsigned*>(this); }
// internalization
sat::th_internalizer* get_internalizer(expr* e);
euf::enode* visit(expr* e);
void attach_bool_var(euf::enode* n);
void attach_bool_var(sat::bool_var v, bool sign, euf::enode* n);
solver* copy_core();
euf::enode* mk_true();
euf::enode* mk_false();
// extensions
sat::extension* get_extension(sat::bool_var v);
sat::extension* get_extension(expr* e);
void add_extension(family_id fid, sat::extension* e);
sat::th_solver* get_solver(func_decl* f) { return fid2solver(f->get_family_id()); }
sat::th_solver* get_solver(expr* e);
sat::th_solver* get_solver(sat::bool_var v);
sat::th_solver* fid2solver(family_id fid);
void add_solver(family_id fid, sat::th_solver* th);
void init_ackerman();
// model building
bool include_func_interp(func_decl* f) const;
sat::th_model_builder* get_model_builder(expr* e) const;
sat::th_model_builder* get_model_builder(func_decl* f) const;
bool include_func_interp(func_decl* f);
void register_macros(model& mdl);
void dependencies2values(deps_t& deps, expr_ref_vector& values, model_ref const& mdl);
void collect_dependencies(deps_t& deps);
@ -112,6 +109,11 @@ namespace euf {
void propagate();
void get_antecedents(literal l, constraint& j, literal_vector& r);
constraint& mk_constraint(constraint*& c, unsigned id);
constraint& conflict_constraint() { return mk_constraint(m_conflict, 0); }
constraint& eq_constraint() { return mk_constraint(m_eq, 1); }
constraint& lit_constraint() { return mk_constraint(m_lit, 2); }
public:
solver(ast_manager& m, atom2bool_var& expr2var, sat::sat_internalizer& si, params_ref const& p = params_ref()):
m(m),
@ -120,31 +122,31 @@ namespace euf {
m_egraph(m),
m_solver(nullptr),
m_lookahead(nullptr),
m_translate(nullptr),
m_translate_expr2var(nullptr),
m_true(nullptr),
m_false(nullptr),
m_conflict_idx(this, 0),
m_eq_idx(this, 1),
m_lit_idx(this, 2)
m_to_m(&m),
m_to_expr2var(&expr2var),
m_to_si(&si)
{
updt_params(p);
}
~solver() override {}
~solver() override {
if (m_conflict) dealloc(sat::constraint_base::mem2base_ptr(m_conflict));
if (m_eq) dealloc(sat::constraint_base::mem2base_ptr(m_eq));
if (m_lit) dealloc(sat::constraint_base::mem2base_ptr(m_lit));
}
void updt_params(params_ref const& p);
void set_solver(sat::solver* s) override { m_solver = s; }
void set_lookahead(sat::lookahead* s) override { m_lookahead = s; }
struct scoped_set_translate {
solver& s;
scoped_set_translate(solver& s, ast_translation& t, atom2bool_var& a2b, sat::sat_internalizer& si) :
scoped_set_translate(solver& s, ast_manager& m, atom2bool_var& a2b, sat::sat_internalizer& si) :
s(s) {
s.m_translate = &t;
s.m_translate_expr2var = &a2b;
s.m_translate_si = &si;
s.m_to_m = &m;
s.m_to_expr2var = &a2b;
s.m_to_si = &si;
}
~scoped_set_translate() { s.m_translate = nullptr; s.m_translate_expr2var = nullptr; s.m_translate_si = nullptr; }
~scoped_set_translate() { s.m_to_m = &s.m; s.m_to_expr2var = &s.m_expr2var; s.m_to_si = &s.si; }
};
double get_reward(literal l, ext_constraint_idx idx, sat::literal_occs_fun& occs) const override { return 0; }
bool is_extended_binary(ext_justification_idx idx, literal_vector & r) override { return false; }
@ -165,7 +167,6 @@ namespace euf {
std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const override;
void collect_statistics(statistics& st) const override;
extension* copy(sat::solver* s) override;
extension* copy(sat::lookahead* s, bool learned) override;
void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override;
void gc() override;
void pop_reinit() override;

59
src/sat/smt/sat_smt.h
View file

@ -14,9 +14,6 @@ Author:
Nikolaj Bjorner (nbjorner) 2020-08-25
--*/
#pragma once
#pragma once
#include "ast/ast.h"
#include "ast/ast_pp.h"
@ -41,19 +38,59 @@ namespace sat {
public:
virtual ~sat_internalizer() {}
virtual bool is_bool_op(expr* e) const = 0;
virtual sat::literal internalize(expr* e) = 0;
virtual sat::bool_var add_bool_var(expr* e) = 0;
virtual literal internalize(expr* e) = 0;
virtual bool_var add_bool_var(expr* e) = 0;
virtual void mk_clause(literal a, literal b) = 0;
virtual void mk_clause(literal l1, literal l2, literal l3, bool is_lemma = false) = 0;
virtual void cache(app* t, literal l) = 0;
};
class index_base {
extension* ex;
class constraint_base {
extension* m_ex;
unsigned m_mem[0];
static size_t ext_size() {
return sizeof(((constraint_base*)nullptr)->m_ex);
}
public:
index_base(extension* e) : ex(e) { to_index(); }
static extension* to_extension(size_t s) { std::cout << "to_extension: " << from_index(s) << " " << from_index(s)->ex << " " << s << "\n"; return from_index(s)->ex; }
static index_base* from_index(size_t s) { return reinterpret_cast<index_base*>(s); }
size_t to_index() const { std::cout << "to_index " << this << " " << ex << " " << reinterpret_cast<size_t>(this) << "\n"; return reinterpret_cast<size_t>(this); }
constraint_base(): m_ex(nullptr) {}
void* mem() { return m_mem; }
static size_t obj_size(size_t sz) {
return ext_size() + sz;
}
static extension* to_extension(size_t s) {
return from_index(s)->m_ex;
}
static constraint_base* from_index(size_t s) {
return reinterpret_cast<constraint_base*>(s);
}
size_t to_index() const {
return reinterpret_cast<size_t>(this);
}
static constraint_base const* mem2base_ptr(void const* mem) {
return reinterpret_cast<constraint_base const*>((unsigned char const*)(mem) - ext_size());
}
static constraint_base* mem2base_ptr(void* mem) {
return reinterpret_cast<constraint_base*>((unsigned char*)(mem) - ext_size());
}
static size_t mem2base(void const* mem) {
return reinterpret_cast<size_t>(mem2base_ptr(mem));
}
static void initialize(void* ptr, extension* ext) {
reinterpret_cast<constraint_base*>(ptr)->m_ex = ext;
}
static void* ptr2mem(void* ptr) {
return reinterpret_cast<void*>(((unsigned char*) ptr) + ext_size());
}
};
}

22
src/sat/smt/sat_th.h
View file

@ -47,12 +47,12 @@ namespace sat {
\brief compute the value for enode \c n and store the value in \c values
for the root of the class of \c n.
*/
virtual void add_value(euf::enode* n, expr_ref_vector& values) = 0;
virtual void add_value(euf::enode* n, expr_ref_vector& values) {}
/**
\brief compute dependencies for node n
*/
virtual void add_dep(euf::enode* n, top_sort<euf::enode>& dep) = 0;
virtual void add_dep(euf::enode* n, top_sort<euf::enode>& dep) {}
/**
\brief should function be included in model.
@ -61,24 +61,10 @@ namespace sat {
};
class th_solver : public extension, public th_model_builder, public th_decompile, public th_internalizer {
public:
virtual ~th_solver() {}
/**
\brief compute the value for enode \c n and store the value in \c values
for the root of the class of \c n.
*/
virtual void add_value(euf::enode* n, expr_ref_vector& values) = 0;
/**
\brief compute dependencies for node n
*/
virtual void add_dep(euf::enode* n, top_sort<euf::enode>& dep) = 0;
/**
\brief should function be included in model.
*/
virtual bool include_func_interp(func_decl* f) const { return false; }
virtual th_solver* fresh(solver* s, ast_manager& m, sat_internalizer& si) = 0;
};

7
src/sat/smt/xor_solver.cpp
View file

@ -33,8 +33,8 @@ namespace sat {
return static_cast<xr const&>(*this);
}
ba_solver::xr::xr(extension* e, unsigned id, literal_vector const& lits):
constraint(e, xr_t, id, null_literal, lits.size(), get_obj_size(lits.size())) {
ba_solver::xr::xr(unsigned id, literal_vector const& lits):
constraint(xr_t, id, null_literal, lits.size(), get_obj_size(lits.size())) {
for (unsigned i = 0; i < size(); ++i) {
m_lits[i] = lits[i];
}
@ -264,7 +264,8 @@ namespace sat {
break;
}
void * mem = m_allocator.allocate(xr::get_obj_size(lits.size()));
xr* x = new (mem) xr(this, next_id(), lits);
constraint_base::initialize(mem, this);
xr* x = new (constraint_base::ptr2mem(mem)) xr(next_id(), lits);
x->set_learned(learned);
add_constraint(x);
return x;

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

@ -35,7 +35,6 @@ Notes:
#include "ast/for_each_expr.h"
#include "sat/tactic/goal2sat.h"
#include "sat/sat_cut_simplifier.h"
#include "sat/smt/ba_internalize.h"
#include "sat/smt/ba_solver.h"
#include "sat/smt/euf_solver.h"
#include "model/model_evaluator.h"
@ -95,7 +94,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_xor_solver = p.get_bool("xor_solver", false);
m_euf = false;
m_euf = true;
}
void throw_op_not_handled(std::string const& s) {
@ -220,6 +218,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
bool visit(expr * t, bool root, bool sign) {
SASSERT(m.is_bool(t));
if (!is_app(t)) {
convert_atom(t, root, sign);
return true;
@ -232,10 +231,12 @@ struct goal2sat::imp : public sat::sat_internalizer {
case OP_NOT:
case OP_OR:
case OP_AND:
case OP_ITE:
case OP_XOR:
case OP_IMPLIES:
m_frame_stack.push_back(frame(to_app(t), root, sign, 0));
return false;
case OP_ITE:
case OP_EQ:
case OP_EQ:
if (m.is_bool(to_app(t)->get_arg(1))) {
m_frame_stack.push_back(frame(to_app(t), root, sign, 0));
return false;
@ -244,8 +245,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
convert_atom(t, root, sign);
return true;
}
case OP_XOR:
case OP_IMPLIES:
case OP_DISTINCT: {
TRACE("goal2sat_not_handled", tout << mk_ismt2_pp(t, m) << "\n";);
std::ostringstream strm;
@ -397,7 +396,40 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
}
void convert_implies(app* t, bool root, bool sign) {
SASSERT(t->get_num_args() == 2);
unsigned sz = m_result_stack.size();
SASSERT(sz >= 2);
sat::literal l1 = m_result_stack[sz - 1];
sat::literal l2 = m_result_stack[sz - 2];
if (root) {
SASSERT(sz == 2);
if (sign) {
mk_clause(l1);
mk_clause(~l2);
}
else {
mk_clause(~l1, l2);
}
m_result_stack.reset();
}
else {
sat::bool_var k = m_solver.add_var(false);
sat::literal l(k, false);
m_cache.insert(t, l);
// l <=> (l1 => l2)
mk_clause(~l, ~l1, l2);
mk_clause(l1, l);
mk_clause(~l2, l);
if (sign)
l.neg();
m_result_stack.shrink(sz - 2);
m_result_stack.push_back(l);
}
}
void convert_iff2(app * t, bool root, bool sign) {
SASSERT(t->get_num_args() == 2);
TRACE("goal2sat", tout << "convert_iff " << root << " " << sign << "\n" << mk_bounded_pp(t, m, 2) << "\n";);
unsigned sz = m_result_stack.size();
SASSERT(sz >= 2);
@ -467,11 +499,10 @@ struct goal2sat::imp : public sat::sat_internalizer {
void convert_ba(app* t, bool root, bool sign) {
SASSERT(!m_euf);
std::cout << "convert ba\n";
sat::extension* ext = m_solver.get_extension();
sat::ba_solver* ba = nullptr;
if (!ext) {
ba = alloc(sat::ba_solver);
ba = alloc(sat::ba_solver, m, *this);
m_solver.set_extension(ba);
ba->push_scopes(m_solver.num_scopes());
}
@ -480,8 +511,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
if (!ba)
throw default_exception("cannot convert to pb");
sat::ba_internalize internalize(*ba, m_solver, *this, m);
sat::literal lit = internalize.internalize(t, sign, root);
sat::literal lit = ba->internalize(t, sign, root);
if (root)
m_result_stack.reset();
else
@ -509,6 +539,12 @@ struct goal2sat::imp : public sat::sat_internalizer {
case OP_EQ:
convert_iff(t, root, sign);
break;
case OP_XOR:
convert_iff(t, root, !sign);
break;
case OP_IMPLIES:
convert_implies(t, root, sign);
break;
default:
UNREACHABLE();
}
@ -614,6 +650,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
case OP_TRUE:
case OP_FALSE:
case OP_NOT:
case OP_IMPLIES:
case OP_XOR:
return true;
case OP_ITE:
case OP_EQ:
@ -657,6 +695,15 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
void operator()(goal const & g) {
struct scoped_reset {
imp& i;
scoped_reset(imp& i) :i(i) {}
~scoped_reset() {
i.m_interface_vars.reset();
i.m_cache.reset();
}
};
scoped_reset _reset(*this);
collect_boolean_interface(g, m_interface_vars);
unsigned size = g.size();
expr_ref f(m), d_new(m);
@ -696,16 +743,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
}
#if 0
void operator()(unsigned sz, expr * const * fs) {
m_interface_vars.reset();
collect_boolean_interface(m, sz, fs, m_interface_vars);
for (unsigned i = 0; i < sz; i++)
process(fs[i]);
}
#endif
};
struct unsupported_bool_proc {
@ -717,8 +754,6 @@ struct unsupported_bool_proc {
void operator()(app * n) {
if (n->get_family_id() == m.get_basic_family_id()) {
switch (n->get_decl_kind()) {
case OP_XOR:
case OP_IMPLIES:
case OP_DISTINCT:
throw found();
default:
@ -758,19 +793,8 @@ void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core
if (!m_imp)
m_imp = alloc(imp, g.m(), p, t, m, dep2asm, default_external);
struct scoped_reset {
goal2sat& g;
scoped_reset(goal2sat& g):g(g) {}
~scoped_reset() {
g.m_imp->m_interface_vars.reset();
g.m_imp->m_cache.reset();
}
};
{
scoped_reset _reset(*this);
(*m_imp)(g);
}
(*m_imp)(g);
m_interpreted_atoms = alloc(expr_ref_vector, g.m());
m_interpreted_atoms->append(m_imp->m_interpreted_atoms);
if (!t.get_extension()) {
@ -1021,8 +1045,7 @@ struct sat2goal::imp {
expr_ref_vector fmls(m);
sat::ba_solver* ba = dynamic_cast<sat::ba_solver*>(ext);
if (ba) {
sat::ba_decompile decompile(*ba, s, m);
decompile.to_formulas(l2e, fmls);
ba->to_formulas(l2e, fmls);
}
else
dynamic_cast<euf::solver*>(ext)->to_formulas(l2e, fmls);

1
src/smt/seq_regex.cpp
View file

@ -490,6 +490,7 @@ namespace smt {
expr_ref is_nullable = is_nullable_wrapper(r);
if (m.is_true(is_nullable))
return;
literal null_lit = th.mk_literal(is_nullable);
expr_ref hd = mk_first(r, n);
expr_ref d(m);