From 904f87feaca2db704ce603b9cf464b45fedfd6ce Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Jan 2017 21:36:52 -0800 Subject: [PATCH] working on card Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 3 +++ src/smt/theory_pb.cpp | 45 +++++++++++++++++++++++++++++++++-------- src/smt/theory_pb.h | 16 +++++---------- 3 files changed, 45 insertions(+), 19 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 3bb4996c7..5853f8fd1 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3719,6 +3719,9 @@ namespace smt { svector expr_signs; for (unsigned i = 0; i < num_lits; i++) { literal l = lits[i]; + if (get_assignment(l) != l_false) { + std::cout << l << " " << get_assignment(l) << "\n"; + } SASSERT(get_assignment(l) == l_false); expr_lits.push_back(bool_var2expr(l.var())); expr_signs.push_back(l.sign()); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index c0eb379d9..22c7ddc24 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -236,6 +236,7 @@ namespace smt { m_args[i].neg(); } m_bound = sz - m_bound + 1; + SASSERT(m_bound > 0); } lbool theory_pb::card::assign(theory_pb& th, literal lit) { @@ -259,6 +260,10 @@ namespace smt { break; } } + if (index == m_bound + 1) { + // literal is no longer watched. + return l_undef; + } SASSERT(index <= m_bound); SASSERT(m_args[index] == lit); @@ -401,7 +406,9 @@ namespace smt { } else if (j == m_bound) { literal_vector lits(size() - m_bound, m_args.c_ptr() + m_bound); - for (i = 0; i < j; ++i) { + th.negate(lits); + lits.push_back(lit()); + for (i = 0; i < m_bound; ++i) { if (ctx.get_assignment(lit(i)) == l_undef) { th.add_assign(*this, lits, lit(i)); } @@ -473,9 +480,9 @@ namespace smt { m_stats.m_num_predicates++; if (m_util.is_aux_bool(atom)) { - std::cout << "aux bool\n"; bool_var abv = ctx.mk_bool_var(atom); ctx.set_var_theory(abv, get_id()); + // std::cout << "aux bool " << ctx.get_scope_level() << " " << mk_pp(atom, get_manager()) << " " << literal(abv) << "\n"; return true; } @@ -909,6 +916,7 @@ namespace smt { m_stats.m_num_propagations++; context& ctx = get_context(); TRACE("pb", tout << "#prop: " << c.num_propagations() << " - " << lits << " " << c.lit() << " => " << l << "\n";); + SASSERT(validate_antecedents(lits)); ctx.assign(l, ctx.mk_justification( card_justification( c, get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), l))); @@ -1528,9 +1536,6 @@ namespace smt { } m_card_lim.resize(new_lim); - - add_cardinality_lemma(); - } void theory_pb::clear_watch(ineq& c) { @@ -1619,6 +1624,7 @@ namespace smt { tout << " => " << l << "\n"; display(tout, c, true);); + SASSERT(validate_antecedents(lits)); ctx.assign(l, ctx.mk_justification( pb_justification( c, get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), l))); @@ -1672,7 +1678,7 @@ namespace smt { void theory_pb::process_card(card& c, int offset) { context& ctx = get_context(); - process_antecedent(c.lit(0), offset); + inc_coeff(c.lit(0), offset); for (unsigned i = c.k() + 1; i < c.size(); ++i) { process_antecedent(c.lit(i), offset); } @@ -1893,7 +1899,10 @@ namespace smt { } } - void theory_pb::add_cardinality_lemma() { + bool theory_pb::can_propagate() { return m_card_reinit; } + + + void theory_pb::propagate() { context& ctx = get_context(); ast_manager& m = get_manager(); if (ctx.inconsistent() || !m_card_reinit) { @@ -1901,11 +1910,15 @@ namespace smt { } m_card_reinit = false; + if (!validate_antecedents(m_antecedents)) { + return; + } pb_util pb(m); expr_ref pred(pb.mk_fresh_bool(), m); bool_var abv = ctx.mk_bool_var(pred); ctx.set_var_theory(abv, get_id()); literal lit(abv); + // std::cout << "fresh " << pred << " " << lit << "\n"; card* c = alloc(card, lit, m_bound); for (unsigned i = 0; i < m_active_coeffs.size(); ++i) { @@ -1967,7 +1980,6 @@ namespace smt { b_justification js; literal conseq = ~confl[2]; - while (m_num_marks > 0) { v = conseq.var(); @@ -2112,6 +2124,7 @@ namespace smt { --slack; } } + SASSERT(validate_antecedents(m_antecedents)); ctx.assign(prop_lit, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), m_antecedents.size(), m_antecedents.c_ptr(), prop_lit, 0, 0))); } @@ -2220,6 +2233,22 @@ namespace smt { SASSERT(!c.is_eq() || (sum == c.k()) == (ctx.get_assignment(c.lit()) == l_true)); } + bool theory_pb::validate_antecedents(literal_vector const& lits) { + context& ctx = get_context(); + for (unsigned i = 0; i < lits.size(); ++i) { + if (ctx.get_assignment(lits[i]) != l_true) { + return false; + } + } + return true; + } + + void theory_pb::negate(literal_vector & lits) { + for (unsigned i = 0; i < lits.size(); ++i) { + lits[i].neg(); + } + } + // display methods void theory_pb::display_resolved_lemma(std::ostream& out) const { diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 5046d7ab3..ab83160ce 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -201,6 +201,7 @@ namespace smt { m_compilation_threshold(0), m_compiled(l_false) { + SASSERT(bound > 0); } literal lit() const { return m_lit; } @@ -270,16 +271,6 @@ namespace smt { } }; - struct card_reinit { - literal_vector m_lits; - card* m_card; - - card_reinit(literal_vector const& lits, card* c): - m_lits(lits), - m_card(c) - {} - }; - theory_pb_params m_params; svector m_var_infos; @@ -393,7 +384,6 @@ namespace smt { void reset_coeffs(); literal cardinality_reduction(literal propagation_lit); - void add_cardinality_lemma(); bool resolve_conflict(card& c, literal_vector const& conflict_clause); void process_antecedent(literal l, int offset); @@ -409,6 +399,8 @@ namespace smt { void validate_final_check(ineq& c); void validate_assign(ineq const& c, literal_vector const& lits, literal l) const; void validate_watch(ineq const& c) const; + bool validate_antecedents(literal_vector const& lits); + void negate(literal_vector & lits); bool proofs_enabled() const { return get_manager().proofs_enabled(); } justification* justify(literal l1, literal l2); @@ -437,6 +429,8 @@ namespace smt { virtual model_value_proc * mk_value(enode * n, model_generator & mg); virtual void init_model(model_generator & m); virtual bool include_func_interp(func_decl* f) { return false; } + virtual bool can_propagate(); + virtual void propagate(); static literal assert_ge(context& ctx, unsigned k, unsigned n, literal const* xs); };