mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-01-19 13:57:25 -08:00
commit 67de30ca4a
24 changed files with 250 additions and 140 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/sat/ba_solver.cpp
View file

@ -111,7 +111,7 @@ namespace sat {
// card
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) {
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];
}
@ -420,17 +420,18 @@ namespace sat {
sz = j;
// _bad_id = p.id();
BADLOG(display(verbose_stream() << "simplify ", p, true));
p.set_size(sz);
p.set_k(p.k() - true_val);
if (p.k() == 1 && p.lit() == null_literal) {
unsigned k = p.k() - true_val;
if (k == 1 && p.lit() == null_literal) {
literal_vector lits(sz, p.literals().c_ptr());
s().mk_clause(sz, lits.c_ptr(), p.learned());
remove_constraint(p, "is clause");
return;
}
else if (p.lit() == null_literal || value(p.lit()) == l_true) {
p.set_size(sz);
p.set_k(k);
if (p.lit() == null_literal || value(p.lit()) == l_true) {
init_watch(p);
}
else {
@ -1139,8 +1140,7 @@ namespace sat {
if (m_overflow || offset > (1 << 12)) {
IF_VERBOSE(20, verbose_stream() << "offset: " << offset << "\n";
active2pb(m_A);
display(verbose_stream(), m_A););
DEBUG_CODE(active2pb(m_A); display(verbose_stream(), m_A);););
goto bail_out;
}
@ -1148,7 +1148,7 @@ namespace sat {
goto process_next_resolvent;
}
TRACE("sat_verbose", display(tout, m_A););
DEBUG_CODE(TRACE("sat_verbose", display(tout, m_A);););
TRACE("ba", tout << "process consequent: " << consequent << " : "; s().display_justification(tout, js) << "\n";);
SASSERT(offset > 0);
@ -1248,9 +1248,8 @@ namespace sat {
DEBUG_CODE(
active2pb(m_C);
VERIFY(validate_resolvent());
m_A = m_C;);
TRACE("ba", display(tout << "conflict: ", m_A););
m_A = m_C;
TRACE("ba", display(tout << "conflict: ", m_A);););
cut();
@ -1528,6 +1527,7 @@ namespace sat {
ba_solver::ba_solver(): m_solver(0), m_lookahead(0), m_unit_walk(0), m_constraint_id(0), m_ba(*this), m_sort(m_ba) {
TRACE("ba", tout << this << "\n";);
m_num_propagations_since_pop = 0;
}
ba_solver::~ba_solver() {
@ -2622,6 +2622,7 @@ namespace sat {
return;
}
VERIFY(c.size() - c.k() >= sz - k);
c.set_size(sz);
c.set_k(k);

1
src/sat/ba_solver.h
View file

@ -198,6 +198,7 @@ namespace sat {
literal_vector m_lits;
svector<uint64> m_coeffs;
uint64 m_k;
ineq(): m_k(0) {}
void reset(uint64 k) { m_lits.reset(); m_coeffs.reset(); m_k = k; }
void push(literal l, uint64 c) { m_lits.push_back(l); m_coeffs.push_back(c); }
};

1
src/sat/sat_model_converter.cpp
View file

@ -325,6 +325,7 @@ namespace sat {
}
void model_converter::flush(model_converter & src) {
VERIFY(this != &src);
m_entries.append(src.m_entries);
src.m_entries.reset();
}

2
src/sat/sat_scc.cpp
View file

@ -275,7 +275,7 @@ namespace sat {
}
void scc::collect_statistics(statistics & st) const {
st.update("elim bool vars", m_num_elim);
st.update("elim bool vars scc", m_num_elim);
st.update("elim binary", m_num_elim_bin);
}

13
src/sat/sat_simplifier.cpp
View file

@ -260,7 +260,6 @@ namespace sat {
break;
}
while (!m_sub_todo.empty());
bool vars_eliminated = m_num_elim_vars > m_old_num_elim_vars;
if (m_need_cleanup || vars_eliminated) {
@ -981,17 +980,21 @@ namespace sat {
void operator()() {
integrity_checker si(s.s);
si.check_watches();
if (s.bce_enabled())
if (s.bce_enabled()) {
block_clauses();
}
si.check_watches();
if (s.abce_enabled())
if (s.abce_enabled()) {
cce<false>();
}
si.check_watches();
if (s.cce_enabled())
if (s.cce_enabled()) {
cce<true>();
}
si.check_watches();
if (s.bca_enabled())
if (s.bca_enabled()) {
bca();
}
si.check_watches();
}

13
src/sat/sat_solver.cpp
View file

@ -1566,6 +1566,17 @@ namespace sat {
#endif
}
unsigned solver::get_hash() const {
unsigned result = 0;
for (clause* cp : m_clauses) {
result = combine_hash(cp->size(), combine_hash(result, cp->id()));
}
for (clause* cp : m_learned) {
result = combine_hash(cp->size(), combine_hash(result, cp->id()));
}
return result;
}
bool solver::set_root(literal l, literal r) {
return !m_ext || m_ext->set_root(l, r);
}
@ -4032,7 +4043,7 @@ namespace sat {
st.update("dyn subsumption resolution", m_dyn_sub_res);
st.update("blocked correction sets", m_blocked_corr_sets);
st.update("units", m_units);
st.update("elim bool vars", m_elim_var_res);
st.update("elim bool vars res", m_elim_var_res);
st.update("elim bool vars bdd", m_elim_var_bdd);
}

2
src/sat/sat_solver.h
View file

@ -538,6 +538,8 @@ namespace sat {
private:
unsigned get_hash() const;
typedef hashtable<unsigned, u_hash, u_eq> index_set;
u_map<index_set> m_antecedents;

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

@ -18,30 +18,32 @@ Notes:
--*/
#include "ast/ast_pp.h"
#include "ast/ast_translation.h"
#include "ast/ast_util.h"
#include "solver/solver.h"
#include "tactic/tactical.h"
#include "sat/sat_solver.h"
#include "solver/tactic2solver.h"
#include "tactic/tactical.h"
#include "tactic/aig/aig_tactic.h"
#include "tactic/core/propagate_values_tactic.h"
#include "tactic/bv/max_bv_sharing_tactic.h"
#include "tactic/arith/card2bv_tactic.h"
#include "tactic/bv/bit_blaster_tactic.h"
#include "tactic/core/simplify_tactic.h"
#include "sat/tactic/goal2sat.h"
#include "ast/ast_pp.h"
#include "model/model_smt2_pp.h"
#include "model/model_v2_pp.h"
#include "model/model_evaluator.h"
#include "tactic/bv/bit_blaster_model_converter.h"
#include "ast/ast_translation.h"
#include "ast/ast_util.h"
#include "tactic/core/propagate_values_tactic.h"
#include "sat/sat_solver.h"
#include "sat/sat_params.hpp"
#include "sat/tactic/goal2sat.h"
#include "sat/sat_simplifier_params.hpp"
// incremental SAT solver.
class inc_sat_solver : public solver {
ast_manager& m;
sat::solver m_solver;
mutable sat::solver m_solver;
goal2sat m_goal2sat;
params_ref m_params;
expr_ref_vector m_fmls;
@ -62,7 +64,7 @@ class inc_sat_solver : public solver {
model_converter_ref m_mc;
mutable model_converter_ref m_mc0;
mutable obj_hashtable<func_decl> m_inserted_const2bits;
ref<sat2goal::mc> m_sat_mc;
mutable ref<sat2goal::mc> m_sat_mc;
mutable model_converter_ref m_cached_mc;
svector<double> m_weights;
std::string m_unknown;
@ -382,7 +384,7 @@ public:
return r;
}
virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override {
sat::literal_vector ls;
u_map<expr*> lit2var;
for (unsigned i = 0; i < vars.size(); ++i) {
@ -410,15 +412,19 @@ public:
void init_reason_unknown() {
m_unknown = "no reason given";
}
virtual std::string reason_unknown() const {
std::string reason_unknown() const override {
return m_unknown;
}
virtual void set_reason_unknown(char const* msg) {
void set_reason_unknown(char const* msg) override {
m_unknown = msg;
}
virtual void get_labels(svector<symbol> & r) {
void get_labels(svector<symbol> & r) override {
}
virtual unsigned get_num_assertions() const {
unsigned get_num_assertions() const override {
const_cast<inc_sat_solver*>(this)->convert_internalized();
if (is_internalized() && m_internalized_converted) {
return m_internalized_fmls.size();
@ -427,28 +433,33 @@ public:
return m_fmls.size();
}
}
virtual expr * get_assertion(unsigned idx) const {
expr * get_assertion(unsigned idx) const override {
if (is_internalized() && m_internalized_converted) {
return m_internalized_fmls[idx];
}
return m_fmls[idx];
}
virtual unsigned get_num_assumptions() const {
unsigned get_num_assumptions() const override {
return m_asmsf.size();
}
virtual expr * get_assumption(unsigned idx) const {
expr * get_assumption(unsigned idx) const override {
return m_asmsf[idx];
}
virtual model_converter_ref get_model_converter() const {
model_converter_ref get_model_converter() const override {
const_cast<inc_sat_solver*>(this)->convert_internalized();
if (m_cached_mc)
return m_cached_mc;
if (is_internalized() && m_internalized_converted) {
insert_const2bits();
m_sat_mc->flush_smc(m_solver, m_map);
m_cached_mc = m_mc0.get();
m_cached_mc = concat(solver::get_model_converter().get(), m_cached_mc.get());
m_cached_mc = concat(m_cached_mc.get(), m_sat_mc.get());
// IF_VERBOSE(0, m_cached_mc->display(verbose_stream() << "get-model-converter\n"););
return m_cached_mc;
}
else {
@ -804,30 +815,37 @@ private:
}
}
m_model = md;
//IF_VERBOSE(0, model_v2_pp(verbose_stream(), *m_model, true););
if (m_sat_mc) {
// IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "satmc\n"););
(*m_sat_mc)(m_model);
}
insert_const2bits();
if (m_mc0) {
// IF_VERBOSE(0, m_mc0->display(verbose_stream() << "mc0\n"););
(*m_mc0)(m_model);
}
TRACE("sat", model_smt2_pp(tout, m, *m_model, 0););
// IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "after\n"););
#if 0
IF_VERBOSE(0, verbose_stream() << "Verifying solution\n";);
model_evaluator eval(*m_model);
for (expr * f : m_fmls) {
expr_ref tmp(m);
if (m_model->eval(f, tmp, true)) {
CTRACE("sat", !m.is_true(tmp),
tout << "Evaluation failed: " << mk_pp(f, m) << " to " << mk_pp(f, m) << "\n";
model_smt2_pp(tout, m, *(m_model.get()), 0););
if (!m.is_true(tmp)) {
IF_VERBOSE(0, verbose_stream() << "failed to verify: " << tmp << "\n";);
IF_VERBOSE(0, verbose_stream() << m_params << "\n";);
}
VERIFY(m.is_true(tmp));
eval(f, tmp);
CTRACE("sat", !m.is_true(tmp),
tout << "Evaluation failed: " << mk_pp(f, m) << " to " << mk_pp(f, m) << "\n";
model_smt2_pp(tout, m, *(m_model.get()), 0););
if (!m.is_true(tmp)) {
IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(f, m) << "\n";);
IF_VERBOSE(0, verbose_stream() << m_params << "\n";);
}
VERIFY(m.is_true(tmp));
}
#endif
}
};

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

@ -519,7 +519,7 @@ struct goal2sat::imp {
}
}
void convert_at_least_k(app* t, rational k, bool root, bool sign) {
void convert_at_least_k(app* t, rational const& k, bool root, bool sign) {
SASSERT(k.is_unsigned());
sat::literal_vector lits;
unsigned sz = m_result_stack.size();
@ -538,7 +538,7 @@ struct goal2sat::imp {
}
}
void convert_at_most_k(app* t, rational k, bool root, bool sign) {
void convert_at_most_k(app* t, rational const& k, bool root, bool sign) {
SASSERT(k.is_unsigned());
sat::literal_vector lits;
unsigned sz = m_result_stack.size();
@ -559,7 +559,7 @@ struct goal2sat::imp {
}
}
void convert_eq_k(app* t, rational k, bool root, bool sign) {
void convert_eq_k(app* t, rational const& k, bool root, bool sign) {
SASSERT(k.is_unsigned());
sat::literal_vector lits;
convert_pb_args(t->get_num_args(), lits);
@ -621,16 +621,20 @@ struct goal2sat::imp {
}
else if (t->get_family_id() == pb.get_family_id()) {
ensure_extension();
rational k;
switch (t->get_decl_kind()) {
case OP_AT_MOST_K:
convert_at_most_k(t, pb.get_k(t), root, sign);
k = pb.get_k(t);
convert_at_most_k(t, k, root, sign);
break;
case OP_AT_LEAST_K:
convert_at_least_k(t, pb.get_k(t), root, sign);
k = pb.get_k(t);
convert_at_least_k(t, k, root, sign);
break;
case OP_PB_LE:
if (pb.has_unit_coefficients(t)) {
convert_at_most_k(t, pb.get_k(t), root, sign);
k = pb.get_k(t);
convert_at_most_k(t, k, root, sign);
}
else {
convert_pb_le(t, root, sign);
@ -638,7 +642,8 @@ struct goal2sat::imp {
break;
case OP_PB_GE:
if (pb.has_unit_coefficients(t)) {
convert_at_least_k(t, pb.get_k(t), root, sign);
k = pb.get_k(t);
convert_at_least_k(t, k, root, sign);
}
else {
convert_pb_ge(t, root, sign);
@ -646,7 +651,8 @@ struct goal2sat::imp {
break;
case OP_PB_EQ:
if (pb.has_unit_coefficients(t)) {
convert_eq_k(t, pb.get_k(t), root, sign);
k = pb.get_k(t);
convert_eq_k(t, k, root, sign);
}
else {
convert_pb_eq(t, root, sign);
@ -891,14 +897,15 @@ void sat2goal::mc::flush_smc(sat::solver& s, atom2bool_var const& map) {
void sat2goal::mc::flush_gmc() {
sat::literal_vector updates;
m_smc.expand(updates);
m_smc.expand(updates);
m_smc.reset();
if (!m_gmc) m_gmc = alloc(generic_model_converter, m);
// now gmc owns the model converter
sat::literal_vector clause;
expr_ref_vector tail(m);
expr_ref def(m);
for (sat::literal l : updates) {
for (unsigned i = 0; i < updates.size(); ++i) {
sat::literal l = updates[i];
if (l == sat::null_literal) {
sat::literal lit0 = clause[0];
for (unsigned i = 1; i < clause.size(); ++i) {
@ -913,6 +920,21 @@ void sat2goal::mc::flush_gmc() {
clause.reset();
tail.reset();
}
// short circuit for equivalences:
else if (clause.empty() && tail.empty() &&
i + 5 < updates.size() &&
updates[i] == ~updates[i + 3] &&
updates[i + 1] == ~updates[i + 4] &&
updates[i + 2] == sat::null_literal &&
updates[i + 5] == sat::null_literal) {
sat::literal r = ~updates[i+1];
if (l.sign()) {
l.neg();
r.neg();
}
m_gmc->add(lit2expr(l), lit2expr(r));
i += 5;
}
else {
clause.push_back(l);
}