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

Browse source 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
This commit is contained in:
Miguel Angelo Da Terra Neves 2017-12-15 09:51:17 -08:00
commit 2bb2ea59e9
29 changed files with 148 additions and 123 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_asymm_branch.cpp
View file

@ -72,7 +72,7 @@ namespace sat {
unsigned elim = m_elim_literals;
if (big) big->init_big(s, true);
process(big, s.m_clauses);
process(big, s.m_learned);
if (big) process(big, s.m_learned);
s.propagate(false);
if (s.m_inconsistent)
break;

1
src/sat/sat_asymm_branch.h
View file

@ -42,7 +42,6 @@ namespace sat {
unsigned m_asymm_branch_rounds;
unsigned m_asymm_branch_delay;
bool m_asymm_branch_sampled;
bool m_asymm_branch_propagate;
bool m_asymm_branch_all;
int64 m_asymm_branch_limit;

1
src/sat/sat_config.cpp
View file

@ -136,6 +136,7 @@ namespace sat {
m_gc_increment = p.gc_increment();
m_gc_small_lbd = p.gc_small_lbd();
m_gc_k = std::min(255u, p.gc_k());
m_gc_burst = p.gc_burst();
m_minimize_lemmas = p.minimize_lemmas();
m_core_minimize = p.core_minimize();

6
src/sat/sat_elim_eqs.cpp
View file

@ -181,9 +181,9 @@ namespace sat {
for (bool_var v : to_elim) {
literal l(v, false);
literal r = roots[v];
SASSERT(v != r.var());
if (m_solver.is_external(v)) {
m_solver.set_root(l, r);
SASSERT(v != r.var());
bool root_ok = !m_solver.is_external(v) || m_solver.set_root(l, r);
if (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok)) {
// cannot really eliminate v, since we have to notify extension of future assignments
m_solver.mk_bin_clause(~l, r, false);
m_solver.mk_bin_clause(l, ~r, false);

12
src/sat/sat_elim_vars.cpp
View file

@ -122,17 +122,17 @@ namespace sat{
bdd b = m.mk_exists(m_var2index[v], b0);
TRACE("elim_vars",
tout << "eliminate " << v << "\n";
/*for (watched const& w : simp.get_wlist(~pos_l)) {
if (w.is_binary_unblocked_clause()) {
for (watched const& w : simp.get_wlist(~pos_l)) {
if (w.is_binary_non_learned_clause()) {
tout << pos_l << " " << w.get_literal() << "\n";
}
}*/
}
m.display(tout, b1);
/*for (watched const& w : simp.get_wlist(~neg_l)) {
if (w.is_binary_unblocked_clause()) {
for (watched const& w : simp.get_wlist(~neg_l)) {
if (w.is_binary_non_learned_clause()) {
tout << neg_l << " " << w.get_literal() << "\n";
}
}*/
}
m.display(tout, b2);
clause_use_list::iterator itp = pos_occs.mk_iterator();
while (!itp.at_end()) {

50
src/sat/sat_lookahead.cpp
View file

@ -338,7 +338,7 @@ namespace sat {
}
TRACE("sat", display_candidates(tout << "sum: " << sum << "\n"););
if (skip_candidates > 0) {
IF_VERBOSE(0, verbose_stream() << "candidates: " << m_candidates.size() << " skip: " << skip_candidates << "\n";);
IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :candidates " << m_candidates.size() << " :skipped " << skip_candidates << ")\n";);
}
return sum;
}
@ -2050,15 +2050,15 @@ namespace sat {
return h;
}
lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) {
lbool lookahead::cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level) {
scoped_ext _scoped_ext(*this);
lits.reset();
m_select_lookahead_vars.reset();
for (auto v : vars) {
m_select_lookahead_vars.insert(v);
}
bool is_first = m_cube_state.m_first;
if (is_first) {
m_select_lookahead_vars.reset();
for (auto v : vars) {
m_select_lookahead_vars.insert(v);
}
init_search();
m_model.reset();
m_cube_state.m_first = false;
@ -2111,6 +2111,8 @@ namespace sat {
#else
lits.append(m_cube_state.m_cube);
#endif
vars.reset();
for (auto v : m_freevars) if (in_reduced_clause(v)) vars.push_back(v);
backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision);
return l_undef;
}
@ -2126,6 +2128,8 @@ namespace sat {
continue;
}
if (lit == null_literal) {
vars.reset();
for (auto v : m_freevars) if (in_reduced_clause(v)) vars.push_back(v);
return l_true;
}
TRACE("sat", tout << "choose: " << lit << " cube: " << m_cube_state.m_cube << "\n";);
@ -2248,40 +2252,6 @@ namespace sat {
return l;
}
literal lookahead::select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars) {
IF_VERBOSE(1, verbose_stream() << "(sat-select " << vars.size() << ")\n";);
scoped_ext _sext(*this);
m_search_mode = lookahead_mode::searching;
scoped_level _sl(*this, c_fixed_truth);
init();
if (inconsistent()) return null_literal;
inc_istamp();
for (auto v : vars) {
m_select_lookahead_vars.insert(v);
}
scoped_assumptions _sa(*this, assumptions);
literal l = choose();
m_select_lookahead_vars.reset();
if (inconsistent()) l = null_literal;
#if 0
// assign unit literals that were found during search for lookahead.
if (assumptions.empty()) {
unsigned num_assigned = 0;
for (literal lit : m_trail) {
if (!m_s.was_eliminated(lit.var()) && m_s.value(lit) != l_true) {
m_s.assign(lit, justification());
++num_assigned;
}
}
IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_assigned << ")\n";);
}
#endif
return l;
}
/**
\brief simplify set of clauses by extracting units from a lookahead at base level.
*/

5
src/sat/sat_lookahead.h
View file

@ -587,15 +587,14 @@ namespace sat {
/**
\brief create cubes to std-out in DIMACS form.
The cubes are controlled using cut-depth and cut-fraction parameters.
If cut-depth != 0, then it is used to control the depth of cuts.
If cut-depth != 0, then it is used to control thedepth of cuts.
Otherwise, cut-fraction gives an adaptive threshold for creating cuts.
*/
lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level);
lbool cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level);
void update_cube_statistics(statistics& st);
literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
/**
\brief simplify set of clauses by extracting units from a lookahead at base level.
*/

8
src/sat/sat_solver.cpp
View file

@ -60,6 +60,7 @@ namespace sat {
m_next_simplify = 0;
m_num_checkpoints = 0;
m_simplifications = 0;
m_ext = 0;
m_cuber = nullptr;
m_mc.set_solver(this);
}
@ -861,12 +862,7 @@ namespace sat {
return r;
}
literal solver::select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars) {
lookahead lh(*this);
return lh.select_lookahead(assumptions, vars);
}
lbool solver::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) {
lbool solver::cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level) {
if (!m_cuber) {
m_cuber = alloc(lookahead, *this);
}

4
src/sat/sat_solver.h
View file

@ -355,10 +355,10 @@ namespace sat {
bool check_clauses(model const& m) const;
bool is_assumption(bool_var v) const;
literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level);
lbool cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level);
protected:
unsigned m_conflicts_since_init;
unsigned m_restarts;
unsigned m_conflicts_since_restart;

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

@ -67,12 +67,12 @@ class inc_sat_solver : public solver {
std::string m_unknown;
// access formulas after they have been pre-processed and handled by the sat solver.
// this allows to access the internal state of the SAT solver and carry on partial results.
bool m_internalized; // are formulas internalized?
bool m_internalized_converted; // have internalized formulas been converted back
expr_ref_vector m_internalized_fmls; // formulas in internalized format
typedef obj_map<expr, sat::literal> dep2asm_t;
bool is_internalized() const { return m_fmls_head == m_fmls.size(); }
public:
inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_mode):
m(m),
@ -84,7 +84,6 @@ public:
m_map(m),
m_num_scopes(0),
m_unknown("no reason given"),
m_internalized(false),
m_internalized_converted(false),
m_internalized_fmls(m) {
updt_params(p);
@ -94,7 +93,6 @@ public:
bool override_incremental() const {
sat_simplifier_params p(m_params);
//std::cout << "override: " << p.override_incremental() << "\n";
return p.override_incremental();
}
@ -124,7 +122,6 @@ public:
if (m_mc0) result->m_mc0 = m_mc0->translate(tr);
//if (m_sat_mc) result->m_sat_mc = m_sat_mc->translate(tr); MN: commenting this line removes bloat
// copy m_bb_rewriter?
result->m_internalized = m_internalized;
result->m_internalized_converted = m_internalized_converted;
return result;
}
@ -188,8 +185,6 @@ public:
if (r != l_true) return r;
r = internalize_assumptions(sz, _assumptions.c_ptr(), dep2asm);
if (r != l_true) return r;
m_internalized = true;
m_internalized_converted = false;
init_reason_unknown();
try {
@ -226,11 +221,8 @@ public:
m_fmls_head_lim.push_back(m_fmls_head);
if (m_bb_rewriter) m_bb_rewriter->push();
m_map.push();
m_internalized = true;
m_internalized_converted = false;
}
virtual void pop(unsigned n) {
m_internalized = false;
if (n > m_num_scopes) { // allow inc_sat_solver to
n = m_num_scopes; // take over for another solver.
}
@ -264,7 +256,6 @@ public:
virtual ast_manager& get_manager() const { return m; }
virtual void assert_expr_core(expr * t) {
m_internalized = false;
TRACE("goal2sat", tout << mk_pp(t, m) << "\n";);
m_fmls.push_back(t);
}
@ -305,18 +296,19 @@ public:
return 0;
}
virtual expr_ref_vector cube(unsigned backtrack_level) {
if (!m_internalized) {
dep2asm_t dep2asm;
virtual expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) {
if (!is_internalized()) {
m_model = 0;
lbool r = internalize_formulas();
if (r != l_true) return expr_ref_vector(m);
m_internalized = true;
}
convert_internalized();
obj_hashtable<expr> _vs;
for (expr* v : vs) _vs.insert(v);
sat::bool_var_vector vars;
for (auto& kv : m_map) {
vars.push_back(kv.m_value);
if (_vs.empty() || _vs.contains(kv.m_key))
vars.push_back(kv.m_value);
}
sat::literal_vector lits;
lbool result = m_solver.cube(vars, lits, backtrack_level);
@ -327,7 +319,7 @@ public:
}
if (result == l_true) {
return expr_ref_vector(m);
}
}
expr_ref_vector fmls(m);
expr_ref_vector lit2expr(m);
lit2expr.resize(m_solver.num_vars() * 2);
@ -335,6 +327,13 @@ public:
for (sat::literal l : lits) {
fmls.push_back(lit2expr[l.index()].get());
}
vs.reset();
for (sat::bool_var v : vars) {
expr* x = lit2expr[sat::literal(v, false).index()].get();
if (x) {
vs.push_back(x);
}
}
return fmls;
}
@ -419,7 +418,7 @@ public:
}
virtual unsigned get_num_assertions() const {
const_cast<inc_sat_solver*>(this)->convert_internalized();
if (m_internalized && m_internalized_converted) {
if (is_internalized() && m_internalized_converted) {
return m_internalized_fmls.size();
}
else {
@ -427,7 +426,7 @@ public:
}
}
virtual expr * get_assertion(unsigned idx) const {
if (m_internalized && m_internalized_converted) {
if (is_internalized() && m_internalized_converted) {
return m_internalized_fmls[idx];
}
return m_fmls[idx];
@ -443,7 +442,7 @@ public:
const_cast<inc_sat_solver*>(this)->convert_internalized();
if (m_cached_mc)
return m_cached_mc;
if (m_internalized && m_internalized_converted) {
if (is_internalized() && m_internalized_converted) {
m_cached_mc = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits()));
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());
@ -455,7 +454,10 @@ public:
}
void convert_internalized() {
if (!m_internalized || m_internalized_converted) return;
if (!is_internalized() && m_fmls_head > 0) {
internalize_formulas();
}
if (!is_internalized() || m_internalized_converted) return;
sat2goal s2g;
m_cached_mc = nullptr;
goal g(m, false, true, false);
@ -679,6 +681,7 @@ private:
if (res != l_undef) {
m_fmls_head = m_fmls.size();
}
m_internalized_converted = false;
return res;
}