mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 05:11:21 +00:00
Code Activity

updates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-09 09:55:37 -08:00
parent 0a9946578b
commit 700f413e26
3 changed files with 7 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/sat/ba_solver.cpp
View file

@ -349,7 +349,7 @@ namespace sat {
} }
bool nullify = p.lit() != null_literal && value(p.lit()) == l_true; bool nullify = p.lit() != null_literal && value(p.lit()) == l_true;
if (nullify) { if (nullify) {
IF_VERBOSE(10, display(verbose_stream() << "nullify tracking literal\n", p, true);); IF_VERBOSE(100, display(verbose_stream() << "nullify tracking literal\n", p, true););
SASSERT(lvl(p.lit()) == 0); SASSERT(lvl(p.lit()) == 0);
nullify_tracking_literal(p); nullify_tracking_literal(p);
init_watch(p, true); init_watch(p, true);
@ -374,7 +374,7 @@ namespace sat {
if (p.k() == 1 && p.lit() == null_literal) { if (p.k() == 1 && p.lit() == null_literal) {
literal_vector lits(p.literals()); literal_vector lits(p.literals());
s().mk_clause(lits.size(), lits.c_ptr(), p.learned()); s().mk_clause(lits.size(), lits.c_ptr(), p.learned());
IF_VERBOSE(10, display(verbose_stream() << "add clause: " << lits << "\n", p, true);); IF_VERBOSE(100, display(verbose_stream() << "add clause: " << lits << "\n", p, true););
remove_constraint(p, "implies clause"); remove_constraint(p, "implies clause");
} }
else if (true_val == 0 && num_false == 0) { else if (true_val == 0 && num_false == 0) {
@ -384,14 +384,14 @@ namespace sat {
} }
else if (true_val >= p.k()) { else if (true_val >= p.k()) {
if (p.lit() != null_literal) { if (p.lit() != null_literal) {
IF_VERBOSE(10, display(verbose_stream() << "assign true literal ", p, true);); IF_VERBOSE(100, display(verbose_stream() << "assign true literal ", p, true););
s().assign(p.lit(), justification()); s().assign(p.lit(), justification());
} }
remove_constraint(p, "is true"); remove_constraint(p, "is true");
} }
else if (slack + true_val < p.k()) { else if (slack + true_val < p.k()) {
if (p.lit() != null_literal) { if (p.lit() != null_literal) {
IF_VERBOSE(10, display(verbose_stream() << "assign false literal ", p, true);); IF_VERBOSE(100, display(verbose_stream() << "assign false literal ", p, true););
s().assign(~p.lit(), justification()); s().assign(~p.lit(), justification());
} }
else { else {
@ -2877,7 +2877,7 @@ namespace sat {
bool ba_solver::elim_pure(literal lit) { bool ba_solver::elim_pure(literal lit) {
if (value(lit) == l_undef && !m_cnstr_use_list[lit.index()].empty() && if (value(lit) == l_undef && !m_cnstr_use_list[lit.index()].empty() &&
use_count(~lit) == 0 && get_num_unblocked_bin(~lit) == 0) { use_count(~lit) == 0 && get_num_unblocked_bin(~lit) == 0) {
IF_VERBOSE(10, verbose_stream() << "pure literal: " << lit << "\n";); IF_VERBOSE(100, verbose_stream() << "pure literal: " << lit << "\n";);
s().assign(lit, justification()); s().assign(lit, justification());
return true; return true;
} }

2
src/solver/solver.h
View file

@ -61,7 +61,7 @@ public:
/** /**
\brief Retrieve set of parameters set on solver. \brief Retrieve set of parameters set on solver.
*/ */
virtual params_ref const& get_params() { return m_params; } virtual params_ref const& get_params() const { return m_params; }
/** /**
\brief Store in \c r a description of the configuration \brief Store in \c r a description of the configuration

1
src/tactic/portfolio/pb2bv_solver.cpp
View file

@ -134,6 +134,7 @@ public:
private: private:
void flush_assertions() const { void flush_assertions() const {
m_rewriter.updt_params(get_params());
proof_ref proof(m); proof_ref proof(m);
expr_ref fml1(m), fml(m); expr_ref fml1(m), fml(m);
expr_ref_vector fmls(m); expr_ref_vector fmls(m);