mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

fix build errors

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-01 09:15:53 -07:00
parent a91d7a7189
commit bfac44f7ed
3 changed files with 7 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/sat/ba_solver.cpp
View file

@ -1125,8 +1125,6 @@ namespace sat {
unsigned offset = 1; unsigned offset = 1;
DEBUG_CODE(active2pb(m_A);); DEBUG_CODE(active2pb(m_A););
unsigned init_marks = m_num_marks;
do { do {
if (m_overflow || offset > (1 << 12)) { if (m_overflow || offset > (1 << 12)) {
@ -1361,10 +1359,9 @@ namespace sat {
int64_t coeff = get_coeff(v); int64_t coeff = get_coeff(v);
lbool val = value(v); lbool val = value(v);
bool is_true = val == l_true; bool is_true = val == l_true;
bool append = coeff != 0 && val != l_undef && (coeff < 0 == is_true); bool append = coeff != 0 && val != l_undef && ((coeff < 0) == is_true);
if (append) { if (append) {
literal lit(v, !is_true); literal lit(v, !is_true);
unsigned acoeff = get_abs_coeff(v);
if (lvl(lit) == m_conflict_lvl) { if (lvl(lit) == m_conflict_lvl) {
if (m_lemma[0] == null_literal) { if (m_lemma[0] == null_literal) {
asserting_coeff = std::abs(coeff); asserting_coeff = std::abs(coeff);
@ -1699,7 +1696,6 @@ namespace sat {
double ba_solver::get_reward(literal l, ext_justification_idx idx, literal_occs_fun& occs) const { double ba_solver::get_reward(literal l, ext_justification_idx idx, literal_occs_fun& occs) const {
constraint const& c = index2constraint(idx); constraint const& c = index2constraint(idx);
unsigned sz = c.size();
switch (c.tag()) { switch (c.tag()) {
case card_t: return get_reward(c.to_card(), occs); case card_t: return get_reward(c.to_card(), occs);
case pb_t: return get_reward(c.to_pb(), occs); case pb_t: return get_reward(c.to_pb(), occs);
@ -2264,7 +2260,7 @@ namespace sat {
bool ba_solver::validate_watch(pb const& p, literal alit) const { bool ba_solver::validate_watch(pb const& p, literal alit) const {
for (unsigned i = 0; i < p.size(); ++i) { for (unsigned i = 0; i < p.size(); ++i) {
literal l = p[i].second; literal l = p[i].second;
if (l != alit && lvl(l) != 0 && is_watched(l, p) != i < p.num_watch()) { if (l != alit && lvl(l) != 0 && is_watched(l, p) != (i < p.num_watch())) {
IF_VERBOSE(0, display(verbose_stream(), p, true); IF_VERBOSE(0, display(verbose_stream(), p, true);
verbose_stream() << "literal " << l << " at position " << i << " " << is_watched(l, p) << "\n";); verbose_stream() << "literal " << l << " at position " << i << " " << is_watched(l, p) << "\n";);
UNREACHABLE(); UNREACHABLE();

6
src/sat/ba_solver.h
View file

@ -243,11 +243,13 @@ namespace sat {
struct ba_sort { struct ba_sort {
ba_solver& s; ba_solver& s;
typedef typename sat::literal literal;
typedef typename sat::literal_vector literal_vector;
literal m_true; literal m_true;
literal_vector m_lits; literal_vector m_lits;
typedef sat::literal literal;
typedef sat::literal_vector literal_vector;
ba_sort(ba_solver& s): s(s), m_true(null_literal) {} ba_sort(ba_solver& s): s(s), m_true(null_literal) {}
literal mk_false(); literal mk_false();
literal mk_true(); literal mk_true();

2
src/sat/sat_lookahead.h
View file

@ -90,7 +90,7 @@ namespace sat {
double m_cube_psat_trigger; double m_cube_psat_trigger;
config() { config() {
memset(this, sizeof(*this), 0); memset(this, 0, sizeof(*this));
m_dl_success = 0.8; m_dl_success = 0.8;
m_alpha = 3.5; m_alpha = 3.5;
m_max_score = 20.0; m_max_score = 20.0;