diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index c96328bf8..d8227a152 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -24,6 +24,7 @@ Revision History: #include"bv_decl_plugin.h" #include"datatype_decl_plugin.h" #include"array_decl_plugin.h" +#include"card_decl_plugin.h" #include"ast_translation.h" #include"ast_pp.h" #include"ast_ll_pp.h" @@ -1122,6 +1123,14 @@ extern "C" { } } + if (mk_c(c)->get_pb_fid() == _d->get_family_id()) { + switch(_d->get_decl_kind()) { + case OP_PB_LE: return Z3_OP_PB_LE; + case OP_AT_MOST_K: return Z3_OP_PB_AT_MOST; + default: UNREACHABLE(); + } + } + return Z3_OP_UNINTERPRETED; Z3_CATCH_RETURN(Z3_OP_UNINTERPRETED); } diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 05e1ca675..49fa1ab99 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -109,6 +109,7 @@ namespace api { m_basic_fid = m().get_basic_family_id(); m_arith_fid = m().mk_family_id("arith"); m_bv_fid = m().mk_family_id("bv"); + m_pb_fid = m().mk_family_id("card"); m_array_fid = m().mk_family_id("array"); m_dt_fid = m().mk_family_id("datatype"); m_datalog_fid = m().mk_family_id("datalog_relation"); diff --git a/src/api/api_context.h b/src/api/api_context.h index e0c95b07b..8b4418c9a 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -75,6 +75,7 @@ namespace api { family_id m_bv_fid; family_id m_dt_fid; family_id m_datalog_fid; + family_id m_pb_fid; datatype_decl_plugin * m_dt_plugin; std::string m_string_buffer; // temporary buffer used to cache strings sent to the "external" world. @@ -121,6 +122,7 @@ namespace api { family_id get_bv_fid() const { return m_bv_fid; } family_id get_dt_fid() const { return m_dt_fid; } family_id get_datalog_fid() const { return m_datalog_fid; } + family_id get_pb_fid() const { return m_pb_fid; } datatype_decl_plugin * get_dt_plugin() const { return m_dt_plugin; } Z3_error_code get_error_code() const { return m_error_code; } diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 2edb28504..14233300a 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -34,7 +34,7 @@ namespace opt { if (m_soft_constraints.empty()) { m_msolver = 0; is_sat = s.check_sat(0, 0); - m_answer.append(m_soft_constraints); + m_answer.reset(); } else if (is_maxsat_problem(m_weights)) { if (m_maxsat_engine == symbol("core_maxsat")) { @@ -64,7 +64,7 @@ namespace opt { IF_VERBOSE(0, verbose_stream() << "validating assignment\n";); m_s->push(); commit_assignment(); - VERIFY(is_sat == m_s->check_sat(0,0)); + VERIFY(l_true == m_s->check_sat(0,0)); m_s->pop(1); // TBD: check that all extensions are unsat too @@ -94,7 +94,7 @@ namespace opt { if (m_msolver) { return inf_eps(m_msolver->get_upper()); } - return inf_eps(); + return inf_eps(rational(m_soft_constraints.size())); } void maxsmt::commit_assignment() { diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index fcd4f6309..7bc430244 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -996,8 +996,9 @@ public: svector neighbours; get_neighbours_undirected(current, neighbours); for (unsigned i = 0; i < neighbours.size(); ++i) { + DEBUG_CODE( edge_id id; - SASSERT(prev == -1 || get_edge_id(prev, current, id) || get_edge_id(current, prev, id)); + SASSERT(prev == -1 || get_edge_id(prev, current, id) || get_edge_id(current, prev, id));); if (!visited.contains(neighbours[i])) { nodes.push_back(neighbours[i]); } @@ -1023,8 +1024,9 @@ public: get_neighbours_undirected(current, neighbours); for (unsigned i = 0; i < neighbours.size(); ++i) { dl_var & next = neighbours[i]; + DEBUG_CODE( edge_id id; - SASSERT(get_edge_id(current, next, id) || get_edge_id(next, current, id)); + SASSERT(get_edge_id(current, next, id) || get_edge_id(next, current, id));); if (!visited.contains(next)) { parents[next] = current; depths[next] = depths[current] + 1; diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 2b42e39f9..a52d4b93b 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -429,6 +429,45 @@ namespace smt { void theory_pb::new_eq_eh(theory_var v1, theory_var v2) { IF_VERBOSE(0, verbose_stream() << v1 << " = " << v2 << "\n";); } + + final_check_status theory_pb::final_check_eh() { + TRACE("card", display(tout);); + DEBUG_CODE(validate_final_check();); + return FC_DONE; + } + + void theory_pb::validate_final_check() { + u_map::iterator itc = m_ineqs.begin(), endc = m_ineqs.end(); + for (; itc != endc; ++itc) { + validate_final_check(*itc->m_value); + } + } + + void theory_pb::validate_final_check(ineq& c) { + context& ctx = get_context(); + + if (ctx.get_assignment(c.lit()) == l_undef) { + return; + } + numeral sum = 0, maxsum = 0; + for (unsigned i = 0; i < c.size(); ++i) { + switch(ctx.get_assignment(c.lit(i))) { + case l_true: + sum += c.coeff(i); + case l_undef: + maxsum += c.coeff(i); + break; + } + } + TRACE("card", display(tout << "validate: ", c); + tout << "sum: " << sum << " " << maxsum << " " << ctx.get_assignment(c.lit()) << "\n"; + ); + + SASSERT(sum <= maxsum); + SASSERT((sum >= c.k()) == (ctx.get_assignment(c.lit()) == l_true)); + SASSERT((maxsum < c.k()) == (ctx.get_assignment(c.lit()) == l_false)); + } + void theory_pb::assign_eh(bool_var v, bool is_true) { context& ctx = get_context(); @@ -447,7 +486,6 @@ namespace smt { if (m_ineqs.find(v, c)) { assign_ineq(*c, is_true); } - TRACE("card", display(tout);); } literal_vector& theory_pb::get_helpful_literals(ineq& c, bool negate) { @@ -505,21 +543,21 @@ namespace smt { display(tout, c); ); if (maxsum < c.k()) { - literal_vector& lits = get_unhelpful_literals(c, true); + literal_vector& lits = get_unhelpful_literals(c, false); lits.push_back(~c.lit()); add_clause(c, c.lit(), lits); - return; } - - c.m_max_sum = 0; - c.m_watch_sz = 0; - for (unsigned i = 0; c.max_sum() < c.k() + c.max_coeff() && i < c.size(); ++i) { - if (ctx.get_assignment(c.lit(i)) != l_false) { - add_watch(c, i); - } + else { + c.m_max_sum = 0; + c.m_watch_sz = 0; + for (unsigned i = 0; c.max_sum() < c.k() + c.max_coeff() && i < c.size(); ++i) { + if (ctx.get_assignment(c.lit(i)) != l_false) { + add_watch(c, i); + } + } + SASSERT(c.max_sum() >= c.k()); + m_assign_ineqs_trail.push_back(&c); } - SASSERT(c.max_sum() >= c.k()); - m_assign_ineqs_trail.push_back(&c); } /** @@ -544,16 +582,16 @@ namespace smt { // numeral k = c.k(); - del_watch(watch, watch_index, c, w); - removed = true; + numeral coeff = c.coeff(w); - for (unsigned i = c.watch_size(); c.max_sum() < k + c.max_coeff() && i < c.size(); ++i) { + for (unsigned i = c.watch_size(); c.max_sum() - coeff < k + c.max_coeff() && i < c.size(); ++i) { if (ctx.get_assignment(c.lit(i)) != l_false) { add_watch(c, i); } } - - if (c.max_sum() < k) { + + + if (c.max_sum() - coeff < k) { // // L: 3*x1 + 2*x2 + x4 >= 3, but x1 <- 0, x2 <- 0 // create clause x1 or x2 or ~L @@ -562,32 +600,37 @@ namespace smt { lits.push_back(~c.lit()); add_clause(c, literal(v, !is_true), lits); } - else if (c.max_sum() < k + c.max_coeff()) { - // - // opportunities for unit propagation for unassigned - // literals whose coefficients satisfy - // c.max_sum() - coeff < k - // - // L: 3*x1 + 2*x2 + x4 >= 3, but x1 <- 0 - // Create clauses x1 or ~L or x2 - // x1 or ~L or x4 - // + else { + del_watch(watch, watch_index, c, w); + removed = true; + if (c.max_sum() - coeff < k + c.max_coeff()) { - literal_vector& lits = get_unhelpful_literals(c, true); - lits.push_back(c.lit()); - for (unsigned i = 0; i < c.size(); ++i) { - if (c.max_sum() - c.coeff(i) < k && ctx.get_assignment(c.lit(i)) == l_undef) { - add_assign(c, lits, c.lit(i)); + // + // opportunities for unit propagation for unassigned + // literals whose coefficients satisfy + // c.max_sum() - coeff < k + // + // L: 3*x1 + 2*x2 + x4 >= 3, but x1 <- 0 + // Create clauses x1 or ~L or x2 + // x1 or ~L or x4 + // + + literal_vector& lits = get_unhelpful_literals(c, true); + lits.push_back(c.lit()); + for (unsigned i = 0; i < c.size(); ++i) { + if (c.max_sum() - c.coeff(i) < k && ctx.get_assignment(c.lit(i)) == l_undef) { + add_assign(c, lits, c.lit(i)); + } } } + // + // else: c.max_sum() >= k + c.max_coeff() + // we might miss opportunities for unit propagation if + // max_coeff is not the maximal coefficient + // of the current unassigned literal, but we can + // rely on eventually learning this from propagations. + // } - // - // else: c.max_sum() >= k + c.max_coeff() - // we might miss opportunities for unit propagation if - // max_coeff is not the maximal coefficient - // of the current unassigned literal, but we can - // rely on eventually learning this from propagations. - // } // @@ -736,10 +779,12 @@ namespace smt { void theory_pb::inc_propagations(ineq& c) { ++c.m_num_propagations; +#if 1 if (c.m_compiled == l_false && c.m_num_propagations > c.m_compilation_threshold) { c.m_compiled = l_undef; m_to_compile.push_back(&c); } +#endif } void theory_pb::restart_eh() { @@ -850,14 +895,12 @@ namespace smt { std::ostream& theory_pb::display(std::ostream& out, ineq& c) const { ast_manager& m = get_manager(); context& ctx = get_context(); + out << c.lit() << " "; if (c.lit() != null_literal) { expr_ref tmp(m); ctx.literal2expr(c.lit(), tmp); out << tmp << "\n"; } - else { - out << "null\n"; - } for (unsigned i = 0; i < c.size(); ++i) { out << c.coeff(i) << "*" << c.lit(i); if (i + 1 < c.size()) { @@ -960,7 +1003,7 @@ namespace smt { // assigned below current index 'idx'. context& ctx = get_context(); for (unsigned i = 0; i < c.size(); ++i) { - if (ctx.get_assignment(c.lit(i)) != l_undef) { + if (ctx.get_assignment(c.lit(i)) == l_false) { process_antecedent(c.lit(i), c.coeff(i)); } } @@ -981,7 +1024,8 @@ namespace smt { for (unsigned i = 0; i < c.size(); ++i) { v = c.lit(i).var(); if (ctx.get_assignment(v) != l_undef) { - IF_VERBOSE(0, verbose_stream() << c.lit(i) << " " << ctx.get_assign_level(v) << "\n";); + IF_VERBOSE(0, verbose_stream() << c.lit(i) << " " + << ctx.get_assign_level(v) << "\n";); lvl = std::max(lvl, ctx.get_assign_level(v)); } } @@ -991,8 +1035,9 @@ namespace smt { } b_justification js(ctx.mk_justification( - pb_justification(c, get_id(), ctx.get_region(), - 0, 0, c.lit()))); + pb_justification( + c, get_id(), ctx.get_region(), + 0, 0, c.lit()))); m_lemma.reset(); m_num_marks = 0; diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index e50be1538..2d23b97d6 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -144,6 +144,9 @@ namespace smt { void resolve_conflict(literal conseq, ineq& c); void process_antecedent(literal l, numeral coeff); void process_ineq(ineq& c); + + void validate_final_check(); + void validate_final_check(ineq& c); public: theory_pb(ast_manager& m); @@ -156,7 +159,7 @@ namespace smt { virtual void new_diseq_eh(theory_var v1, theory_var v2) { } virtual bool use_diseqs() const { return false; } virtual bool build_models() const { return false; } - virtual final_check_status final_check_eh() { return FC_DONE; } + virtual final_check_status final_check_eh(); virtual void reset_eh(); virtual void assign_eh(bool_var v, bool is_true);