mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 12:58:44 +00:00
Code Activity

import more from csp

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-11 13:09:28 -08:00
parent 02c85dd6de
commit 22783a4bcb
5 changed files with 21 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/sat/sat_drat.cpp
View file

@ -213,8 +213,8 @@ namespace sat {
m_status.push_back(st);
m_proof.push_back(&c);
if (st == status::deleted) {
del_watch(c, c[0]);
del_watch(c, c[1]);
if (n > 0) del_watch(c, c[0]);
if (n > 1) del_watch(c, c[1]);
return;
}
unsigned num_watch = 0;
@ -338,8 +338,9 @@ namespace sat {
for (unsigned i = num_units; i < m_units.size(); ++i) {
m_assignment[m_units[i].var()] = l_undef;
}
m_units.resize(num_units);
m_units.shrink(num_units);
bool ok = m_inconsistent;
IF_VERBOSE(9, verbose_stream() << "is-drup " << m_inconsistent << "\n");
m_inconsistent = false;
return ok;
@ -583,6 +584,7 @@ namespace sat {
}
}
void drat::add(literal l, bool learned) {
TRACE("sat", tout << "add: " << l << " " << (learned?"l":"t") << "\n";);
declare(l);
status st = get_status(learned);
if (m_out) dump(1, &l, st);
@ -590,6 +592,7 @@ namespace sat {
if (m_check) append(l, st);
}
void drat::add(literal l1, literal l2, bool learned) {
TRACE("sat", tout << "add: " << l1 << " " << l2 << " " << (learned?"l":"t") << "\n";);
declare(l1);
declare(l2);
literal ls[2] = {l1, l2};

6
src/sat/sat_parallel.cpp
View file

@ -113,7 +113,7 @@ namespace sat {
s.m_params.set_sym("phase", symbol("random"));
}
m_solvers[i] = alloc(sat::solver, s.m_params, m_limits[i]);
m_solvers[i]->copy(s);
m_solvers[i]->copy(s, true);
m_solvers[i]->set_par(this, i);
push_child(m_solvers[i]->rlimit());
}
@ -235,7 +235,7 @@ namespace sat {
// there could be multiple local search engines running at the same time.
IF_VERBOSE(1, verbose_stream() << "(sat-parallel refresh :from " << m_num_clauses << " :to " << s.m_clauses.size() << ")\n";);
m_solver_copy = alloc(solver, s.m_params, s.rlimit());
m_solver_copy->copy(s);
m_solver_copy->copy(s, true);
m_num_clauses = s.m_clauses.size();
}
}
@ -292,7 +292,7 @@ namespace sat {
{
m_consumer_ready = true;
if (m_solver_copy && s.m_clauses.size() > m_solver_copy->m_clauses.size()) {
s.copy(*m_solver_copy);
s.copy(*m_solver_copy, true);
copied = true;
m_num_clauses = s.m_clauses.size();
}

4
src/sat/sat_solver.cpp
View file

@ -95,7 +95,7 @@ namespace sat {
if (ext) ext->set_solver(this);
}
void solver::copy(solver const & src) {
void solver::copy(solver const & src, bool copy_learned) {
pop_to_base_level();
del_clauses(m_clauses);
del_clauses(m_learned);
@ -192,7 +192,7 @@ namespace sat {
// copy high quality lemmas
unsigned num_learned = 0;
for (clause* c : src.m_learned) {
if (c->glue() <= 2 || (c->size() <= 40 && c->glue() <= 8)) {
if (copy_learned || c->glue() <= 2 || (c->size() <= 40 && c->glue() <= 8)) {
buffer.reset();
for (literal l : *c) buffer.push_back(l);
clause* c1 = mk_clause_core(buffer.size(), buffer.c_ptr(), true);

2
src/sat/sat_solver.h
View file

@ -210,7 +210,7 @@ namespace sat {
\pre the model converter of src and this must be empty
*/
void copy(solver const & src);
void copy(solver const & src, bool copy_learned = false);
// -----------------------
//

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

@ -60,7 +60,7 @@ struct goal2sat::imp {
sat::solver_core & m_solver;
atom2bool_var & m_map;
dep2asm_map & m_dep2asm;
sat::bool_var m_true;
sat::literal m_true;
bool m_ite_extra;
unsigned long long m_max_memory;
expr_ref_vector m_trail;
@ -81,13 +81,14 @@ struct goal2sat::imp {
m_default_external(default_external),
m_is_lemma(false) {
updt_params(p);
m_true = sat::null_bool_var;
m_true = sat::null_literal;
}
void updt_params(params_ref const & p) {
m_ite_extra = p.get_bool("ite_extra", true);
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_xor_solver = p.get_bool("xor_solver", false);
if (m_xor_solver) ensure_extension();
}
void throw_op_not_handled(std::string const& s) {
@ -117,11 +118,11 @@ struct goal2sat::imp {
m_solver.add_clause(num, lits, m_is_lemma);
}
sat::bool_var mk_true() {
if (m_true == sat::null_bool_var) {
sat::literal mk_true() {
if (m_true == sat::null_literal) {
// create fake variable to represent true;
m_true = m_solver.add_var(false);
mk_clause(sat::literal(m_true, false)); // v is true
m_true = sat::literal(m_solver.add_var(false), false);
mk_clause(m_true); // v is true
}
return m_true;
}
@ -132,10 +133,10 @@ struct goal2sat::imp {
sat::bool_var v = m_map.to_bool_var(t);
if (v == sat::null_bool_var) {
if (m.is_true(t)) {
l = sat::literal(mk_true(), sign);
l = sign ? ~mk_true() : mk_true();
}
else if (m.is_false(t)) {
l = sat::literal(mk_true(), !sign);
l = sign ? mk_true() : ~mk_true();
}
else {
bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);