mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-27 13:39:49 +00:00
Code Activity

adding ack/model

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-28 12:55:31 -07:00
parent 7f0b5bc129
commit 4244ce4aad
31 changed files with 831 additions and 914 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/sat/smt/CMakeLists.txt
View file

@ -1,7 +1,12 @@
z3_add_component(sat_smt
SOURCES
atom2bool_var.cpp
sat_th.cpp
ba_solver.cpp
xor_solver.cpp
ba_internalize.cpp
euf_ackerman.cpp
euf_solver.cpp
euf_model.cpp
COMPONENT_DEPENDENCIES
sat
ast

339
src/sat/smt/ba_internalize.cpp Normal file
View file

@ -0,0 +1,339 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
ba_internalize.h
Abstract:
Internalize methods for Boolean algebra operators.
Author:
Nikolaj Bjorner (nbjorner) 2020-08-25
--*/
#include "sat/smt/ba_internalize.h"
namespace sat {
literal ba_internalize::internalize(expr* e, bool sign, bool root) {
if (pb.is_pb(e))
return internalize_pb(e, sign, root);
if (m.is_xor(e))
return internalize_xor(e, sign, root);
UNREACHABLE();
return null_literal;
}
literal ba_internalize::internalize_xor(expr* e, bool sign, bool root) {
sat::literal_vector lits;
sat::bool_var v = m_solver.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());
lits.push_back(lit);
};
expr* e1 = nullptr;
while (m.is_iff(e, e1, e))
add_expr(e1);
add_expr(e);
// ensure that = is converted to xor
for (unsigned i = 1; i + 1 < lits.size(); ++i) {
lits[i].neg();
}
ba.add_xr(lits);
auto* aig = m_solver.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));
app* t = to_app(e);
rational k = 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))
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))
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))
return convert_eq_k(t, k, root, sign);
else
return convert_pb_eq(t, root, sign);
default:
UNREACHABLE();
}
return null_literal;
}
void ba_internalize::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) {
for (unsigned i = 0; i < lits.size(); ++i) {
rational c = 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) {
for (expr* arg : *t) {
lits.push_back(si.internalize(arg));
m_solver.set_external(lits.back().var());
}
}
void ba_internalize::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);
k.neg();
svector<wliteral> wlits;
convert_pb_args(t, wlits);
for (wliteral& wl : wlits) {
wl.second.neg();
k += rational(wl.first);
}
check_unsigned(k);
if (root && m_solver.num_user_scopes() == 0) {
unsigned k1 = k.get_unsigned();
if (sign) {
k1 = 1 - k1;
for (wliteral& wl : wlits) {
wl.second.neg();
k1 += wl.first;
}
}
ba.add_pb_ge(null_bool_var, wlits, k1);
return null_literal;
}
else {
bool_var v = m_solver.add_var(true);
literal lit(v, sign);
ba.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);
check_unsigned(k);
svector<wliteral> wlits;
convert_pb_args(t, wlits);
if (root && m_solver.num_user_scopes() == 0) {
unsigned k1 = k.get_unsigned();
if (sign) {
k1 = 1 - k1;
for (wliteral& wl : wlits) {
wl.second.neg();
k1 += wl.first;
}
}
ba.add_pb_ge(sat::null_bool_var, wlits, k1);
return null_literal;
}
else {
sat::bool_var v = m_solver.add_var(true);
sat::literal lit(v, sign);
ba.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);
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());
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());
if (base_assert) {
return null_literal;
}
else {
literal l1(v1, false), l2(v2, false);
bool_var v = m_solver.add_var(false);
literal l(v, false);
si.mk_clause(~l, l1);
si.mk_clause(~l, l2);
si.mk_clause(~l1, ~l2, l);
si.cache(t, l);
if (sign) l.neg();
return l;
}
}
literal ba_internalize::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 (sign) {
for (literal& l : lits) l.neg();
k2 = lits.size() + 1 - k2;
}
ba.add_at_least(null_bool_var, lits, k2);
return null_literal;
}
else {
bool_var v = m_solver.add_var(true);
literal lit(v, false);
ba.add_at_least(v, lits, k.get_unsigned());
si.cache(t, lit);
if (sign) lit.neg();
TRACE("ba", tout << "root: " << root << " lit: " << lit << "\n";);
return lit;
}
}
literal ba_internalize::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);
for (literal& l : lits) {
l.neg();
}
unsigned k2 = lits.size() - k.get_unsigned();
if (root && m_solver.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);
return null_literal;
}
else {
bool_var v = m_solver.add_var(true);
literal lit(v, false);
ba.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) {
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());
for (literal& l : lits) {
l.neg();
}
ba.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);
literal l(v, false);
si.mk_clause(~l, l1);
si.mk_clause(~l, l2);
si.mk_clause(~l1, ~l2, l);
si.cache(t, l);
if (sign) l.neg();
return l;
}
else {
return null_literal;
}
}
expr_ref ba_decompile::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);
if (c.lit() != sat::null_literal) {
fml = m.mk_eq(lit2expr(c.lit()), fml);
}
return fml;
}
expr_ref ba_decompile::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) {
lits.push_back(lit2expr(wl.second));
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);
if (p.lit() != sat::null_literal) {
fml = m.mk_eq(lit2expr(p.lit()), fml);
}
return fml;
}
expr_ref ba_decompile::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));
}
expr_ref fml(m.mk_xor(x.size(), lits.c_ptr()), m);
if (x.lit() != sat::null_literal) {
fml = m.mk_eq(lit2expr(x.lit()), fml);
}
return fml;
}
bool ba_decompile::to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) {
for (auto* c : ba.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:
fmls.push_back(get_pb(l2e, c->to_pb()));
break;
case sat::ba_solver::xr_t:
fmls.push_back(get_xor(l2e, c->to_xr()));
break;
}
}
return true;
}
}

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

@ -0,0 +1,73 @@
/*++
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;
};
}

4622
src/sat/smt/ba_solver.cpp Normal file
View file

File diff suppressed because it is too large Load diff

589
src/sat/smt/ba_solver.h Normal file
View file

@ -0,0 +1,589 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
ba_solver.h
Abstract:
Cardinality extensions,
Pseudo Booleans,
Xors
Author:
Nikolaj Bjorner (nbjorner) 2017-01-30
Revision History:
--*/
#pragma once
#include "sat/sat_extension.h"
#include "sat/sat_solver.h"
#include "sat/sat_lookahead.h"
#include "sat/sat_big.h"
#include "sat/smt/sat_smt.h"
#include "util/small_object_allocator.h"
#include "util/scoped_ptr_vector.h"
#include "util/sorting_network.h"
namespace sat {
class xor_finder;
class ba_solver : public extension {
friend class local_search;
struct stats {
unsigned m_num_propagations;
unsigned m_num_conflicts;
unsigned m_num_resolves;
unsigned m_num_bin_subsumes;
unsigned m_num_clause_subsumes;
unsigned m_num_pb_subsumes;
unsigned m_num_big_strengthenings;
unsigned m_num_cut;
unsigned m_num_gc;
unsigned m_num_overflow;
unsigned m_num_lemmas;
stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
};
public:
enum tag_t {
card_t,
pb_t,
xr_t
};
class card;
class pb;
class xr;
class pb_base;
class constraint : public index_base {
protected:
tag_t m_tag;
bool m_removed;
literal m_lit;
literal m_watch;
unsigned m_glue;
unsigned m_psm;
unsigned m_size;
size_t m_obj_size;
bool m_learned;
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),
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; }
literal lit() const { return m_lit; }
unsigned size() const { return m_size; }
void set_size(unsigned sz) { SASSERT(sz <= m_size); m_size = sz; }
void update_literal(literal l) { m_lit = l; }
bool was_removed() const { return m_removed; }
void set_removed() { m_removed = true; }
void nullify_literal() { m_lit = null_literal; }
unsigned glue() const { return m_glue; }
void set_glue(unsigned g) { m_glue = g; }
unsigned psm() const { return m_psm; }
void set_psm(unsigned p) { m_psm = p; }
void set_learned(bool f) { m_learned = f; }
bool learned() const { return m_learned; }
bool is_watched() const { return m_watch == m_lit && m_lit != null_literal; }
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; }
unsigned fold_max_var(unsigned w) const;
size_t obj_size() const { return m_obj_size; }
card& to_card();
pb& to_pb();
xr& to_xr();
card const& to_card() const;
pb const& to_pb() const;
xr const& to_xr() const;
pb_base const& to_pb_base() 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; }
virtual bool is_watching(literal l) const { UNREACHABLE(); return false; };
virtual literal_vector literals() const { UNREACHABLE(); return literal_vector(); }
virtual void swap(unsigned i, unsigned j) { UNREACHABLE(); }
virtual literal get_lit(unsigned i) const { UNREACHABLE(); return null_literal; }
virtual void set_lit(unsigned i, literal l) { UNREACHABLE(); }
virtual bool well_formed() const { return true; }
virtual void negate() { UNREACHABLE(); }
};
friend std::ostream& operator<<(std::ostream& out, constraint const& c);
// base class for pb and cardinality constraints
class pb_base : public constraint {
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); }
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; }
bool well_formed() const override;
};
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);
literal operator[](unsigned i) const { return m_lits[i]; }
literal& operator[](unsigned i) { return m_lits[i]; }
literal const* begin() const { return m_lits; }
literal const* end() const { return static_cast<literal const*>(m_lits) + m_size; }
void negate() override;
void swap(unsigned i, unsigned j) override { std::swap(m_lits[i], m_lits[j]); }
literal_vector literals() const override { return literal_vector(m_size, m_lits); }
bool is_watching(literal l) const override;
literal get_lit(unsigned i) const override { return m_lits[i]; }
void set_lit(unsigned i, literal l) override { m_lits[i] = l; }
unsigned get_coeff(unsigned i) const override { return 1; }
};
typedef std::pair<unsigned, literal> wliteral;
class pb : public pb_base {
unsigned m_slack;
unsigned m_num_watch;
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);
literal lit() const { return m_lit; }
wliteral operator[](unsigned i) const { return m_wlits[i]; }
wliteral& operator[](unsigned i) { return m_wlits[i]; }
wliteral const* begin() const { return m_wlits; }
wliteral const* end() const { return begin() + m_size; }
unsigned slack() const { return m_slack; }
void set_slack(unsigned s) { m_slack = s; }
unsigned num_watch() const { return m_num_watch; }
unsigned max_sum() const { return m_max_sum; }
void update_max_sum();
void set_num_watch(unsigned s) { m_num_watch = s; }
bool is_cardinality() const;
void negate() override;
void set_k(unsigned k) override { m_k = k; VERIFY(k < 4000000000); update_max_sum(); }
void swap(unsigned i, unsigned j) override { std::swap(m_wlits[i], m_wlits[j]); }
literal_vector literals() const override { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; }
bool is_watching(literal l) const override;
literal get_lit(unsigned i) const override { return m_wlits[i].second; }
void set_lit(unsigned i, literal l) override { m_wlits[i].second = l; }
unsigned get_coeff(unsigned i) const override { return m_wlits[i].first; }
};
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);
literal operator[](unsigned i) const { return m_lits[i]; }
literal const* begin() const { return m_lits; }
literal const* end() const { return begin() + m_size; }
void negate() override { m_lits[0].neg(); }
void swap(unsigned i, unsigned j) override { std::swap(m_lits[i], m_lits[j]); }
bool is_watching(literal l) const override;
literal_vector literals() const override { return literal_vector(size(), begin()); }
literal get_lit(unsigned i) const override { return m_lits[i]; }
void set_lit(unsigned i, literal l) override { m_lits[i] = l; }
bool well_formed() const override;
};
protected:
struct ineq {
svector<wliteral> m_wlits;
uint64_t m_k;
ineq(): m_k(0) {}
unsigned size() const { return m_wlits.size(); }
literal lit(unsigned i) const { return m_wlits[i].second; }
unsigned coeff(unsigned i) const { return m_wlits[i].first; }
void reset(uint64_t k) { m_wlits.reset(); m_k = k; }
void push(literal l, unsigned c) { m_wlits.push_back(wliteral(c,l)); }
unsigned bv_coeff(bool_var v) const;
void divide(unsigned c);
void weaken(unsigned i);
bool contains(literal l) const { for (auto wl : m_wlits) if (wl.second == l) return true; return false; }
};
solver* m_solver;
lookahead* m_lookahead;
stats m_stats;
small_object_allocator m_allocator;
ptr_vector<constraint> m_constraints;
ptr_vector<constraint> m_learned;
ptr_vector<constraint> m_constraint_to_reinit;
unsigned_vector m_constraint_to_reinit_lim;
unsigned m_constraint_to_reinit_last_sz;
unsigned m_constraint_id;
// conflict resolution
unsigned m_num_marks;
unsigned m_conflict_lvl;
svector<int64_t> m_coeffs;
svector<bool_var> m_active_vars;
unsigned m_bound;
tracked_uint_set m_active_var_set;
literal_vector m_lemma;
literal_vector m_skipped;
unsigned m_num_propagations_since_pop;
unsigned_vector m_parity_marks;
literal_vector m_parity_trail;
unsigned_vector m_pb_undef;
struct ba_sort {
typedef sat::literal pliteral;
typedef sat::literal_vector pliteral_vector;
ba_solver& s;
pliteral m_true;
pliteral_vector m_lits;
ba_sort(ba_solver& s): s(s), m_true(null_literal) {}
pliteral mk_false();
pliteral mk_true();
pliteral mk_not(pliteral l);
pliteral fresh(char const*);
pliteral mk_min(unsigned, pliteral const* lits);
pliteral mk_max(unsigned, pliteral const* lits);
void mk_clause(unsigned n, literal const* lits);
std::ostream& pp(std::ostream& out, pliteral l) const;
};
ba_sort m_ba;
psort_nw<ba_sort> m_sort;
void ensure_parity_size(bool_var v);
unsigned get_parity(bool_var v);
void inc_parity(bool_var v);
void reset_parity(bool_var v);
solver& s() const { return *m_solver; }
// simplification routines
vector<svector<constraint*>> m_cnstr_use_list;
use_list m_clause_use_list;
bool m_simplify_change;
bool m_clause_removed;
bool m_constraint_removed;
literal_vector m_roots;
bool_vector m_root_vars;
unsigned_vector m_weights;
svector<wliteral> m_wlits;
bool subsumes(card& c1, card& 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);
void subsumption(pb& p1);
void binary_subsumption(card& c1, literal lit);
void clause_subsumption(card& c1, literal lit, clause_vector& removed_clauses);
void card_subsumption(card& c1, literal lit);
unsigned get_num_unblocked_bin(literal l);
literal get_min_occurrence_literal(card const& c);
void init_use_lists();
void remove_unused_defs();
unsigned set_non_external();
unsigned elim_pure();
bool elim_pure(literal lit);
void unit_strengthen();
void unit_strengthen(big& big, constraint& cs);
void unit_strengthen(big& big, pb_base& p);
void subsumption(constraint& c1);
void subsumption(card& c1);
void gc_half(char const* _method);
void update_psm(constraint& c) const;
void mutex_reduction();
void update_pure();
void reserve_roots();
unsigned use_count(literal lit) const { return m_cnstr_use_list[lit.index()].size() + m_clause_use_list.get(lit).size(); }
void cleanup_clauses();
void cleanup_clauses(clause_vector& clauses);
void cleanup_constraints();
void cleanup_constraints(ptr_vector<constraint>& cs, bool learned);
void remove_constraint(constraint& c, char const* reason);
// constraints
constraint& index2constraint(size_t idx) const { return *reinterpret_cast<constraint*>(idx); }
void pop_constraint();
void unwatch_literal(literal w, constraint& c);
void watch_literal(literal w, constraint& c);
void watch_literal(wliteral w, pb& p);
bool is_watched(literal l, constraint const& c) const;
void add_constraint(constraint* c);
bool init_watch(constraint& c);
void init_watch(bool_var v);
void clear_watch(constraint& c);
lbool add_assign(constraint& c, literal l);
bool incremental_mode() const;
void simplify(constraint& c);
void pre_simplify(xor_finder& xu, constraint& c);
void nullify_tracking_literal(constraint& c);
void set_conflict(constraint& c, literal lit);
void assign(constraint& c, literal lit);
bool assigned_above(literal above, literal below);
void get_antecedents(literal l, constraint const& c, literal_vector & r);
bool validate_conflict(constraint const& c) const;
bool validate_unit_propagation(constraint const& c, literal alit) const;
void validate_eliminated();
void validate_eliminated(ptr_vector<constraint> const& cs);
void attach_constraint(constraint const& c);
void detach_constraint(constraint const& c);
lbool eval(constraint const& c) const;
lbool eval(model const& m, constraint const& c) const;
lbool eval(lbool a, lbool b) const;
void assert_unconstrained(literal lit, literal_vector const& lits);
void flush_roots(constraint& c);
void recompile(constraint& c);
void split_root(constraint& c);
unsigned next_id() { return m_constraint_id++; }
void set_non_learned(constraint& c);
// cardinality
bool init_watch(card& c);
lbool add_assign(card& c, literal lit);
void clear_watch(card& c);
void reset_coeffs();
void reset_marked_literals();
void get_antecedents(literal l, card const& c, literal_vector & r);
void flush_roots(card& c);
void recompile(card& c);
bool clausify(card& c);
bool clausify(literal lit, unsigned n, literal const* lits, unsigned k);
lbool eval(card const& c) const;
lbool eval(model const& m, card const& c) const;
double get_reward(card const& c, literal_occs_fun& occs) const;
// xr specific functionality
void clear_watch(xr& x);
bool init_watch(xr& x);
bool parity(xr const& x, unsigned offset) const;
lbool add_assign(xr& x, literal alit);
void get_xr_antecedents(literal l, unsigned index, justification js, literal_vector& r);
void get_antecedents(literal l, xr const& x, literal_vector & r);
void simplify(xr& x);
void extract_xor();
void merge_xor();
bool clausify(xr& x);
void flush_roots(xr& x);
lbool eval(xr const& x) const;
lbool eval(model const& m, xr const& x) const;
// pb functionality
unsigned m_a_max;
bool init_watch(pb& p);
lbool add_assign(pb& p, literal alit);
void add_index(pb& p, unsigned index, literal lit);
void clear_watch(pb& p);
void get_antecedents(literal l, pb const& p, literal_vector & r);
void split_root(pb_base& p);
void simplify(pb_base& p);
void simplify2(pb& p);
bool is_cardinality(pb const& p);
void flush_roots(pb& p);
void recompile(pb& p);
bool clausify(pb& p);
bool is_cardinality(pb const& p, literal_vector& lits);
lbool eval(pb const& p) const;
lbool eval(model const& m, pb const& p) const;
double get_reward(pb const& p, literal_occs_fun& occs) const;
// RoundingPb conflict resolution
lbool resolve_conflict_rs();
void round_to_one(ineq& ineq, bool_var v);
void round_to_one(bool_var v);
void divide(unsigned c);
void resolve_on(literal lit);
void resolve_with(ineq const& ineq);
void reset_marks(unsigned idx);
void mark_variables(ineq const& ineq);
void bail_resolve_conflict(unsigned idx);
void init_visited();
void mark_visited(literal l);
void mark_visited(bool_var v);
bool is_visited(bool_var v) const;
bool is_visited(literal l) 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); }
inline lbool value(model const& m, literal l) const { return l.sign() ? ~m[l.var()] : m[l.var()]; }
inline bool is_false(literal lit) const { return l_false == value(lit); }
inline unsigned lvl(literal lit) const { return m_lookahead ? 0 : m_solver->lvl(lit); }
inline unsigned lvl(bool_var v) const { return m_lookahead ? 0 : m_solver->lvl(v); }
inline bool inconsistent() const {
if (m_lookahead) return m_lookahead->inconsistent();
return m_solver->inconsistent();
}
inline watch_list& get_wlist(literal l) { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); }
inline watch_list const& get_wlist(literal l) const { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); }
inline void assign(literal l, justification j) {
if (m_lookahead) m_lookahead->assign(l);
else m_solver->assign(l, j);
}
inline void set_conflict(justification j, literal l) {
if (m_lookahead) m_lookahead->set_conflict();
else m_solver->set_conflict(j, l);
}
inline config const& get_config() const { return m_lookahead ? m_lookahead->get_config() : m_solver->get_config(); }
inline void drat_add(literal_vector const& c, svector<drat::premise> const& premises) { if (m_solver) m_solver->m_drat.add(c, premises); }
mutable bool m_overflow;
void reset_active_var_set();
bool test_and_set_active(bool_var v);
void inc_coeff(literal l, unsigned offset);
int64_t get_coeff(bool_var v) const;
uint64_t get_coeff(literal lit) const;
wliteral get_wliteral(bool_var v);
unsigned get_abs_coeff(bool_var v) const;
int get_int_coeff(bool_var v) const;
unsigned get_bound() const;
void inc_bound(int64_t i);
literal get_asserting_literal(literal conseq);
void process_antecedent(literal l, unsigned offset);
void process_antecedent(literal l) { process_antecedent(l, 1); }
void process_card(card& c, unsigned offset);
void cut();
bool create_asserting_lemma();
// validation utilities
bool validate_conflict(card const& c) const;
bool validate_conflict(xr const& x) const;
bool validate_conflict(pb const& p) const;
bool validate_assign(literal_vector const& lits, literal lit);
bool validate_lemma();
bool validate_ineq(ineq const& ineq) const;
bool validate_unit_propagation(card const& c, literal alit) const;
bool validate_unit_propagation(pb const& p, literal alit) const;
bool validate_unit_propagation(pb const& p, literal_vector const& r, literal alit) const;
bool validate_unit_propagation(xr const& x, literal alit) const;
bool validate_conflict(literal_vector const& lits, ineq& p);
bool validate_watch_literals() const;
bool validate_watch_literal(literal lit) const;
bool validate_watched_constraint(constraint const& c) const;
bool validate_watch(pb const& p, literal alit) const;
bool is_watching(literal lit, constraint const& c) const;
literal translate_to_sat(solver& s, u_map<bool_var>& translation, ineq const& pb);
literal translate_to_sat(solver& s, u_map<bool_var>& translation, ineq& a, ineq& b);
literal translate_to_sat(solver& s, u_map<bool_var>& translation, literal lit);
ineq negate(ineq const& a) const;
void push_lit(literal_vector& lits, literal lit);
ineq m_A, m_B, m_C;
void active2pb(ineq& p);
constraint* active2lemma();
constraint* active2constraint();
constraint* active2card();
void active2wlits();
void active2wlits(svector<wliteral>& wlits);
void justification2pb(justification const& j, literal lit, unsigned offset, ineq& p);
void constraint2pb(constraint& cnstr, literal lit, unsigned offset, ineq& p);
bool validate_resolvent();
unsigned get_coeff(ineq const& pb, literal lit);
void display(std::ostream& out, ineq const& p, bool values = false) const;
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_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);
literal add_xor_def(literal_vector& lits, bool learned = false);
bool all_distinct(literal_vector const& lits);
bool all_distinct(clause const& c);
bool all_distinct(xr const& x);
void copy_core(ba_solver* result, bool learned);
void copy_constraints(ba_solver* result, ptr_vector<constraint> const& constraints);
public:
ba_solver();
~ba_solver() override;
void set_solver(solver* s) override { m_solver = s; }
void set_lookahead(lookahead* l) override { m_lookahead = l; }
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);
bool propagate(literal l, ext_constraint_idx idx) override;
lbool resolve_conflict() override;
void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) override;
void asserted(literal l) override;
check_result check() override;
void push() override;
void pop(unsigned n) override;
void pre_simplify() override;
void simplify() override;
void clauses_modifed() override;
lbool get_phase(bool_var v) override;
bool set_root(literal l, literal r) override;
void flush_roots() override;
std::ostream& display(std::ostream& out) const override;
std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const override;
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;
unsigned max_var(unsigned w) const override;
double get_reward(literal l, ext_justification_idx idx, literal_occs_fun& occs) const override;
bool is_extended_binary(ext_justification_idx idx, literal_vector & r) override;
void init_use_list(ext_use_list& ul) override;
bool is_blocked(literal l, ext_constraint_idx idx) override;
bool check_model(model const& m) const override;
ptr_vector<constraint> const & constraints() const { return m_constraints; }
std::ostream& display(std::ostream& out, constraint const& c, bool values) const;
bool validate() override;
bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& add_cardinlaity,
std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& add_pb) override;
};
};

211
src/sat/smt/euf_ackerman.cpp Normal file
View file

@ -0,0 +1,211 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
euf_ackerman.cpp
Abstract:
Ackerman reduction plugin for EUF
Author:
Nikolaj Bjorner (nbjorner) 2020-08-28
--*/
#pragma once
#include "sat/smt/euf_solver.h"
#include "sat/smt/euf_ackerman.h"
namespace euf {
ackerman::ackerman(solver& s, ast_manager& m): s(s), m(m) {
new_tmp();
}
ackerman::~ackerman() {
reset();
dealloc(m_tmp_inference);
}
void ackerman::reset() {
for (inference* inf : m_table) {
m.dec_ref(inf->a);
m.dec_ref(inf->b);
m.dec_ref(inf->c);
}
m_table.reset();
m_queue = nullptr;
}
void ackerman::insert(expr* a, expr* b, expr* lca) {
if (a->get_id() > b->get_id())
std::swap(a, b);
inference& inf = *m_tmp_inference;
inf.a = a;
inf.b = b;
inf.c = lca;
inf.is_cc = false;
insert();
}
void ackerman::insert(app* a, app* b) {
if (a->get_id() > b->get_id())
std::swap(a, b);
inference& inf = *m_tmp_inference;
inf.a = a;
inf.b = b;
inf.c = nullptr;
inf.is_cc = true;
insert();
}
void ackerman::remove_from_queue(inference* inf) {
if (m_queue->m_next == m_queue) {
SASSERT(inf == m_queue);
m_queue = nullptr;
return;
}
if (m_queue == inf)
m_queue = inf->m_next;
auto* next = inf->m_next;
auto* prev = inf->m_prev;
prev->m_next = next;
next->m_prev = prev;
}
void ackerman::push_to_front(inference* inf) {
if (!m_queue) {
m_queue = inf;
}
else if (m_queue != inf) {
auto* next = inf->m_next;
auto* prev = inf->m_prev;
prev->m_next = next;
next->m_prev = prev;
inf->m_prev = m_queue->m_prev;
inf->m_next = m_queue;
m_queue->m_prev = inf;
}
}
void ackerman::insert() {
inference* inf = m_tmp_inference;
inference* other = m_table.insert_if_not_there(inf);
if (other == inf) {
m.inc_ref(inf->a);
m.inc_ref(inf->b);
m.inc_ref(inf->c);
}
else
new_tmp();
other->m_count++;
push_to_front(other);
}
void ackerman::remove(inference* inf) {
remove_from_queue(inf);
m_table.erase(inf);
m.dec_ref(inf->a);
m.dec_ref(inf->b);
m.dec_ref(inf->c);
dealloc(inf);
}
void ackerman::new_tmp() {
m_tmp_inference = alloc(inference);
m_tmp_inference->m_next = m_tmp_inference->m_prev = m_tmp_inference;
m_tmp_inference->m_count = 0;
}
void ackerman::cg_conflict_eh(expr * n1, expr * n2) {
if (s.m_config.m_dack != DACK_ROOT)
return;
if (!is_app(n1) || !is_app(n2))
return;
app* a = to_app(n1);
app* b = to_app(n2);
if (a->get_decl() != b->get_decl() || a->get_num_args() != b->get_num_args())
return;
insert(a, b);
gc();
}
void ackerman::used_eq_eh(expr* a, expr* b, expr* c) {
if (!s.m_config.m_dack_eq)
return;
if (a == b || a == c || b == c)
return;
insert(a, b, c);
gc();
}
void ackerman::used_cc_eh(app* a, app* b) {
if (s.m_config.m_dack != DACK_CR)
return;
SASSERT(a->get_decl() == b->get_decl());
SASSERT(a->get_num_args() == b->get_num_args());
insert(a, b);
gc();
}
void ackerman::gc() {
m_num_propagations_since_last_gc++;
if (m_num_propagations_since_last_gc <= s.m_config.m_dack_gc)
return;
m_num_propagations_since_last_gc = 0;
while (m_table.size() > m_gc_threshold)
remove(m_queue->m_prev);
m_gc_threshold *= 110;
m_gc_threshold /= 100;
m_gc_threshold++;
}
void ackerman::propagate() {
SASSERT(s.s().at_base_lvl());
auto* n = m_queue;
inference* k = nullptr;
unsigned num_prop = static_cast<unsigned>(s.s().stats().m_conflict * s.m_config.m_dack_factor);
num_prop = std::min(num_prop, m_table.size());
for (unsigned i = 0; i < num_prop; ++i, n = k) {
k = n->m_next;
if (n->m_count < s.m_config.m_dack_threshold)
continue;
if (n->is_cc)
add_cc(n->a, n->b);
else
add_eq(n->a, n->b, n->c);
remove(n);
}
}
void ackerman::add_cc(expr* _a, expr* _b) {
app* a = to_app(_a);
app* b = to_app(_b);
sat::literal_vector lits;
unsigned sz = a->get_num_args();
for (unsigned i = 0; i < sz; ++i) {
expr_ref eq(m.mk_eq(a->get_arg(i), b->get_arg(i)), m);
sat::literal lit = s.internalize(eq, true, false);
lits.push_back(~lit);
}
expr_ref eq(m.mk_eq(a, b), m);
lits.push_back(s.internalize(eq, false, false));
s.s().mk_clause(lits, true);
}
void ackerman::add_eq(expr* a, expr* b, expr* c) {
sat::literal lits[3];
expr_ref eq1(m.mk_eq(a, c), m);
expr_ref eq2(m.mk_eq(b, c), m);
expr_ref eq3(m.mk_eq(a, b), m);
lits[0] = s.internalize(eq1, true, false);
lits[1] = s.internalize(eq2, true, false);
lits[2] = s.internalize(eq3, false, false);
s.s().mk_clause(3, lits, true);
}
}

89
src/sat/smt/euf_ackerman.h Normal file
View file

@ -0,0 +1,89 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
euf_ackerman.h
Abstract:
Ackerman reduction plugin for EUF
Author:
Nikolaj Bjorner (nbjorner) 2020-08-25
--*/
#pragma once
#include "ast/euf/euf_egraph.h"
#include "sat/smt/atom2bool_var.h"
#include "sat/smt/sat_th.h"
namespace euf {
class solver;
class ackerman {
struct inference {
bool is_cc;
expr* a, *b, *c;
inference* m_next{ nullptr };
inference* m_prev{ nullptr };
unsigned m_count{ 0 };
inference():is_cc(false), a(nullptr), b(nullptr), c(nullptr) {}
inference(app* a, app* b):is_cc(true), a(a), b(b), c(nullptr) {}
inference(expr* a, expr* b, expr* c):is_cc(false), a(a), b(b), c(c) {}
};
struct inference_eq {
bool operator()(inference const* a, inference const* b) const {
return a->is_cc == b->is_cc && a->a == b->a && a->b == b->b && a->c == b->c;
}
};
struct inference_hash {
unsigned operator()(inference const* a) const {
SASSERT(a->a && a->b);
return mk_mix(a->a->get_id(), a->b->get_id(), a->c ? a->c->get_id() : 0);
}
};
typedef hashtable<inference*, inference_hash, inference_eq> table_t;
solver& s;
ast_manager& m;
table_t m_table;
inference* m_queue { nullptr };
inference* m_tmp_inference { nullptr };
unsigned m_gc_threshold { 1 };
unsigned m_propagate_threshold { 0 };
unsigned m_num_propagations_since_last_gc { 0 };
void reset();
void new_tmp();
void insert(expr* a, expr* b, expr* lca);
void insert(app* a, app* b);
void insert();
void remove(inference* inf);
void add_cc(expr* a, expr* b);
void add_eq(expr* a, expr* b, expr* c);
void gc();
void push_to_front(inference* inf);
void remove_from_queue(inference* inf);
public:
ackerman(solver& s, ast_manager& m);
~ackerman();
void cg_conflict_eh(expr * n1, expr * n2);
void used_eq_eh(expr* a, expr* b, expr* lca);
void used_cc_eh(app* a, app* b);
void propagate();
};
};

138
src/sat/smt/euf_model.cpp Normal file
View file

@ -0,0 +1,138 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
euf_model.cpp
Abstract:
Model building for EUF solver plugin.
Author:
Nikolaj Bjorner (nbjorner) 2020-08-25
--*/
#include "ast/ast_pp.h"
#include "sat/smt/euf_solver.h"
#include "model/value_factory.h"
namespace euf {
void solver::update_model(model_ref& mdl) {
deps_t deps;
expr_ref_vector values(m);
collect_dependencies(deps);
deps.topological_sort();
dependencies2values(deps, values, mdl);
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 {
if (f->get_family_id() == null_family_id)
return true;
sat::th_model_builder* mb = get_model_builder(f);
return mb && mb->include_func_interp(f);
}
void solver::collect_dependencies(deps_t& deps) {
for (enode* n : m_egraph.nodes()) {
if (n->num_args() == 0) {
deps.insert(n, nullptr);
continue;
}
auto* mb = get_model_builder(n->get_owner());
if (mb)
mb->add_dep(n, deps);
else
deps.insert(n, nullptr);
}
}
void solver::dependencies2values(deps_t& deps, expr_ref_vector& values, model_ref const& mdl) {
user_sort_factory user_sort(m);
for (enode* n : deps.top_sorted()) {
unsigned id = n->get_root_id();
if (values.get(id, nullptr))
continue;
expr* e = n->get_owner();
values.reserve(id + 1);
if (m.is_bool(e) && is_uninterp_const(e) && mdl->get_const_interp(to_app(e)->get_decl())) {
values.set(id, mdl->get_const_interp(to_app(e)->get_decl()));
continue;
}
// model of s() must have been fixed.
if (m.is_bool(e)) {
switch (s().value(m_expr2var.to_bool_var(e))) {
case l_true:
values.set(id, m.mk_true());
break;
case l_false:
values.set(id, m.mk_false());
break;
default:
break;
}
continue;
}
auto* mb = get_model_builder(e);
if (mb)
mb->add_value(n, values);
else if (m.is_uninterp(m.get_sort(e))) {
expr* v = user_sort.get_fresh_value(m.get_sort(e));
values.set(id, v);
}
else {
IF_VERBOSE(1, verbose_stream() << "no model values created for " << mk_pp(e, m) << "\n");
}
}
}
void solver::values2model(deps_t const& deps, expr_ref_vector const& values, model_ref& mdl) {
ptr_vector<expr> args;
for (enode* n : deps.top_sorted()) {
expr* e = n->get_owner();
if (!is_app(e))
continue;
app* a = to_app(e);
func_decl* f = a->get_decl();
if (!include_func_interp(f))
continue;
if (m.is_bool(e) && is_uninterp_const(e) && mdl->get_const_interp(f))
continue;
expr* v = values.get(n->get_root_id());
unsigned arity = f->get_arity();
if (arity == 0)
mdl->register_decl(f, v);
else {
auto* fi = mdl->get_func_interp(f);
if (!fi) {
fi = alloc(func_interp, m, arity);
mdl->register_decl(f, fi);
}
args.reset();
for (enode* arg : enode_args(n))
args.push_back(values.get(arg->get_root_id()));
if (!fi->get_entry(args.c_ptr()))
fi->insert_new_entry(args.c_ptr(), v);
}
}
}
void solver::register_macros(model& mdl) {
// TODO
}
}

472
src/sat/smt/euf_solver.cpp Normal file
View file

@ -0,0 +1,472 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
euf_solver.cpp
Abstract:
Solver plugin for EUF
Author:
Nikolaj Bjorner (nbjorner) 2020-08-25
--*/
#include "ast/pb_decl_plugin.h"
#include "tactic/tactic_exception.h"
#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 {
void solver::updt_params(params_ref const& p) {
m_config.updt_params(p);
}
/**
* retrieve extension that is associated with Boolean variable.
*/
sat::extension* solver::get_extension(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());
}
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());
return ba;
}
}
return nullptr;
}
bool solver::propagate(literal l, ext_constraint_idx idx) {
auto* ext = sat::index_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);
if (ext == this)
get_antecedents(l, *constraint::from_idx(idx), r);
else
ext->get_antecedents(l, idx, r);
}
void solver::get_antecedents(literal l, constraint& j, literal_vector& r) {
m_explain.reset();
euf::enode* n = nullptr;
bool sign = false;
if (j.id() != 0) {
auto p = m_var2node[l.var()];
n = p.first;
SASSERT(n);
sign = l.sign() != p.second;
}
// init_ackerman();
switch (j.id()) {
case 0:
SASSERT(m_egraph.inconsistent());
m_egraph.explain<unsigned>(m_explain);
break;
case 1:
SASSERT(m_egraph.is_equality(n));
m_egraph.explain_eq<unsigned>(m_explain, n->get_arg(0), n->get_arg(1), n->commutative());
break;
case 2:
SASSERT(m.is_bool(n->get_owner()));
m_egraph.explain_eq<unsigned>(m_explain, n, (sign ? m_false : m_true), false);
break;
default:
UNREACHABLE();
}
for (unsigned* idx : m_explain)
r.push_back(sat::to_literal((unsigned)(idx - base_ptr())));
}
void solver::asserted(literal l) {
auto* ext = get_extension(l.var());
if (ext) {
ext->asserted(l);
return;
}
auto p = m_var2node.get(l.var(), enode_bool_pair(nullptr, false));
if (!p.first)
return;
bool sign = p.second != l.sign();
euf::enode* n = p.first;
expr* e = n->get_owner();
if (m.is_eq(e) && !sign) {
euf::enode* na = n->get_arg(0);
euf::enode* nb = n->get_arg(1);
m_egraph.merge(na, nb, base_ptr() + l.index());
}
else {
euf::enode* nb = sign ? m_false : m_true;
m_egraph.merge(n, nb, base_ptr() + l.index());
}
// TBD: delay propagation?
propagate();
}
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()));
return;
}
for (euf::enode* eq : m_egraph.new_eqs()) {
bool_var v = m_expr2var.to_bool_var(eq->get_owner());
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()));
}
for (euf::enode* p : m_egraph.new_lits()) {
expr* e = p->get_owner();
bool sign = m.is_false(p->get_root()->get_owner());
SASSERT(m.is_bool(e));
SASSERT(m.is_true(p->get_root()->get_owner()) || sign);
bool_var v = m_expr2var.to_bool_var(e);
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()));
}
}
sat::check_result solver::check() {
bool give_up = false;
bool cont = false;
for (auto* e : m_extensions)
switch (e->check()) {
case sat::CR_CONTINUE: cont = true; break;
case sat::CR_GIVEUP: give_up = true; break;
default: break;
}
if (cont)
return sat::CR_CONTINUE;
if (give_up)
return sat::CR_GIVEUP;
return sat::CR_DONE;
}
void solver::push() {
for (auto* e : m_extensions)
e->push();
m_egraph.push();
++m_num_scopes;
}
void solver::pop(unsigned n) {
m_egraph.pop(n);
for (auto* e : m_extensions)
e->pop(n);
if (n <= m_num_scopes) {
m_num_scopes -= n;
return;
}
n -= m_num_scopes;
unsigned old_lim = m_bool_var_lim.size() - n;
unsigned old_sz = m_bool_var_lim[old_lim];
for (unsigned i = m_bool_var_trail.size(); i-- > old_sz; )
m_var2node[m_bool_var_trail[i]] = enode_bool_pair(nullptr, false);
m_bool_var_trail.shrink(old_sz);
m_bool_var_lim.shrink(old_lim);
}
void solver::pre_simplify() {
for (auto* e : m_extensions)
e->pre_simplify();
}
void solver::simplify() {
for (auto* e : m_extensions)
e->simplify();
if (m_ackerman)
m_ackerman->propagate();
}
void solver::clauses_modifed() {
for (auto* e : m_extensions)
e->clauses_modifed();
}
lbool solver::get_phase(bool_var v) {
auto* ext = get_extension(v);
if (ext)
return ext->get_phase(v);
return l_undef;
}
std::ostream& solver::display(std::ostream& out) const {
m_egraph.display(out);
for (auto* e : m_extensions)
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);
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);
if (ext != this)
return ext->display_constraint(out, idx);
return out;
}
void solver::collect_statistics(statistics& st) const {
m_egraph.collect_statistics(st);
for (auto* e : m_extensions)
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;
auto* r = alloc(solver, to, a2b, 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 (auto* e : m_extensions)
r->m_extensions.push_back(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 (auto* e : m_extensions)
r->m_extensions.push_back(e->copy(s, learned));
return r;
}
void solver::find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) {
for (auto* e : m_extensions)
e->find_mutexes(lits, mutexes);
}
void solver::gc() {
for (auto* e : m_extensions)
e->gc();
}
void solver::pop_reinit() {
for (auto* e : m_extensions)
e->pop_reinit();
}
bool solver::validate() {
for (auto* e : m_extensions)
if (!e->validate())
return false;
return true;
}
void solver::init_use_list(sat::ext_use_list& ul) {
for (auto* e : m_extensions)
e->init_use_list(ul);
}
bool solver::is_blocked(literal l, ext_constraint_idx idx) {
auto* ext = sat::index_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)
if (!e->check_model(m))
return false;
return true;
}
unsigned solver::max_var(unsigned w) const {
for (auto* e : m_extensions)
w = e->max_var(w);
for (unsigned sz = m_var2node.size(); sz-- > 0; ) {
euf::enode* n = m_var2node[sz].first;
if (n && m.is_bool(n->get_owner())) {
w = std::max(w, sz);
break;
}
}
return w;
}
void solver::init_ackerman() {
if (m_ackerman)
return;
if (m_config.m_dack == DACK_DISABLED)
return;
m_ackerman = alloc(ackerman, *this, m);
std::function<void(expr*,expr*,expr*)> used_eq = [&](expr* a, expr* b, expr* lca) {
m_ackerman->used_eq_eh(a, b, lca);
};
std::function<void(app*,app*)> used_cc = [&](app* a, app* b) {
m_ackerman->used_cc_eh(a, b);
};
m_egraph.set_used_eq(used_eq);
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);
if (ext)
return ext->internalize(e, sign, root);
if (!m_true) {
m_true = visit(m.mk_true());
m_false = visit(m.mk_false());
}
SASSERT(!si.is_bool_op(e));
sat::scoped_stack _sc(m_stack);
unsigned sz = m_stack.size();
euf::enode* n = visit(e);
while (m_stack.size() > sz) {
loop:
if (!m.inc())
throw tactic_exception(m.limit().get_cancel_msg());
sat::frame & fr = m_stack.back();
expr* e = fr.m_e;
if (m_egraph.find(e)) {
m_stack.pop_back();
continue;
}
unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0;
while (fr.m_idx < num) {
expr* arg = to_app(e)->get_arg(fr.m_idx);
fr.m_idx++;
n = visit(arg);
if (!n)
goto loop;
}
m_args.reset();
for (unsigned i = 0; i < num; ++i)
m_args.push_back(m_egraph.find(to_app(e)->get_arg(i)));
n = m_egraph.mk(e, num, m_args.c_ptr());
attach_bool_var(n);
}
SASSERT(m_egraph.find(e));
return literal(m_expr2var.to_bool_var(e), sign);
}
euf::enode* solver::visit(expr* e) {
euf::enode* n = m_egraph.find(e);
if (n)
return n;
if (si.is_bool_op(e)) {
sat::literal lit = si.internalize(e);
n = m_egraph.mk(e, 0, nullptr);
attach_bool_var(lit.var(), lit.sign(), n);
if (!m.is_true(e) && !m.is_false(e))
s().set_external(lit.var());
return n;
}
if (is_app(e) && to_app(e)->get_num_args() > 0) {
m_stack.push_back(sat::frame(e));
return nullptr;
}
n = m_egraph.mk(e, 0, nullptr);
attach_bool_var(n);
return n;
}
void solver::attach_bool_var(euf::enode* n) {
expr* e = n->get_owner();
if (m.is_bool(e)) {
sat::bool_var v = si.add_bool_var(e);
attach_bool_var(v, false, n);
}
}
void solver::attach_bool_var(sat::bool_var v, bool sign, euf::enode* n) {
m_var2node.reserve(v + 1, enode_bool_pair(nullptr, false));
for (; m_num_scopes > 0; --m_num_scopes)
m_bool_var_lim.push_back(m_bool_var_trail.size());
SASSERT(m_var2node[v].first == nullptr);
m_var2node[v] = euf::enode_bool_pair(n, sign);
m_bool_var_trail.push_back(v);
}
bool solver::to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) {
for (auto* th : m_decompilers) {
if (!th->to_formulas(l2e, fmls))
return false;
}
for (euf::enode* n : m_egraph.nodes()) {
if (!n->is_root())
fmls.push_back(m.mk_eq(n->get_owner(), n->get_root()->get_owner()));
}
return true;
}
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)
if (!e->extract_pb(card, pb))
return false;
return true;
}
}

180
src/sat/smt/euf_solver.h Normal file
View file

@ -0,0 +1,180 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
euf_solver.h
Abstract:
Solver plugin for EUF
Author:
Nikolaj Bjorner (nbjorner) 2020-08-25
--*/
#pragma once
#include "util/scoped_ptr_vector.h"
#include "ast/ast_translation.h"
#include "ast/euf/euf_egraph.h"
#include "smt/params/smt_params.h"
#include "tactic/model_converter.h"
#include "sat/sat_extension.h"
#include "sat/smt/atom2bool_var.h"
#include "sat/smt/sat_th.h"
#include "sat/smt/euf_ackerman.h"
namespace euf {
typedef sat::literal literal;
typedef sat::ext_constraint_idx ext_constraint_idx;
typedef sat::ext_justification_idx ext_justification_idx;
typedef sat::literal_vector literal_vector;
typedef sat::bool_var bool_var;
class constraint : public sat::index_base {
unsigned m_id;
public:
constraint(sat::extension* e, unsigned id) :
index_base(e), m_id(id)
{}
unsigned id() const { return m_id; }
static constraint* from_idx(size_t z) { return reinterpret_cast<constraint*>(z); }
};
class solver : public sat::extension, public sat::th_internalizer, public sat::th_decompile {
typedef top_sort<euf::enode> deps_t;
friend class ackerman;
struct stats {
unsigned m_num_dynack;
stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
};
ast_manager& m;
atom2bool_var& m_expr2var;
sat::sat_internalizer& si;
smt_params m_config;
euf::egraph m_egraph;
stats m_stats;
sat::solver* m_solver { nullptr };
sat::lookahead* m_lookahead { nullptr };
ast_translation* m_translate { nullptr };
atom2bool_var* m_translate_expr2var { 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;
svector<sat::frame> m_stack;
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;
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();
// extensions
sat::extension* get_extension(sat::bool_var v);
sat::extension* get_extension(expr* e);
void add_extension(family_id fid, sat::extension* e);
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;
void register_macros(model& mdl);
void dependencies2values(deps_t& deps, expr_ref_vector& values, model_ref const& mdl);
void collect_dependencies(deps_t& deps);
void values2model(deps_t const& deps, expr_ref_vector const& values, model_ref& mdl);
// solving
void propagate();
void get_antecedents(literal l, constraint& j, literal_vector& r);
public:
solver(ast_manager& m, atom2bool_var& expr2var, sat::sat_internalizer& si, params_ref const& p = params_ref()):
m(m),
m_expr2var(expr2var),
si(si),
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)
{
updt_params(p);
}
~solver() override {}
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):s(s) { s.m_translate = &t; s.m_translate_expr2var = &a2b; }
~scoped_set_translate() { s.m_translate = nullptr; s. m_translate_expr2var = nullptr; }
};
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; }
bool propagate(literal l, ext_constraint_idx idx) override;
void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) override;
void asserted(literal l) override;
sat::check_result check() override;
void push() override;
void pop(unsigned n) override;
void pre_simplify() override;
void simplify() override;
// have a way to replace l by r in all constraints
void clauses_modifed() override;
lbool get_phase(bool_var v) override;
std::ostream& display(std::ostream& out) const override;
std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const override;
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;
bool validate() override;
void init_use_list(sat::ext_use_list& ul) override;
bool is_blocked(literal l, ext_constraint_idx) override;
bool check_model(sat::model const& m) const override;
unsigned max_var(unsigned w) const override;
bool 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) override;
bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls);
sat::literal internalize(expr* e, bool sign, bool root) override;
void update_model(model_ref& mdl);
};
};

37
src/sat/smt/sat_th.cpp
View file

@ -1,37 +0,0 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
sat_th.cpp
Abstract:
Theory plugins
Author:
Nikolaj Bjorner (nbjorner) 2020-08-25
--*/
#include "sat/smt/sat_th.h"
#include "util/top_sort.h"
namespace sat {
/*
* \brief add dependency: dst depends on src.
*/
void th_dependencies::add(euf::enode* src, euf::enode* dst) {
}
/*
* \brief sort dependencies.
*/
void th_dependencies::sort() {
top_sort<euf::enode> top;
}
}

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

@ -16,33 +16,26 @@ Author:
--*/
#pragma once
#include "util/top_sort.h"
#include "sat/smt/sat_smt.h"
#include "ast/euf/euf_egraph.h"
namespace sat {
class th_dependencies {
public:
th_dependencies() {}
euf::enode * const* begin() const { return nullptr; }
euf::enode * const* end() const { return nullptr; }
/*
* \brief add dependency: dst depends on src.
*/
void add(euf::enode* src, euf::enode* dst);
/*
* \brief sort dependencies.
*/
void sort();
};
class th_internalizer {
public:
virtual literal internalize(sat_internalizer& si, expr* e, bool sign, bool root) = 0;
virtual ~th_internalizer() {}
virtual literal internalize(expr* e, bool sign, bool root) = 0;
};
class th_decompile {
public:
virtual ~th_decompile() {}
virtual bool to_formulas(std::function<expr_ref(sat::literal)>& lit2expr, expr_ref_vector& fmls) = 0;
};
class th_model_builder {
@ -59,7 +52,12 @@ namespace sat {
/**
\brief compute dependencies for node n
*/
virtual void add_dep(euf::enode* n, th_dependencies& dep) = 0;
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; }
};