From 12198d13ac75459d870d9caf5a793896765abd2d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 Dec 2020 12:24:35 -0800 Subject: [PATCH] fix #4794 --- src/sat/sat_drat.cpp | 5 ----- src/sat/sat_solver.cpp | 5 +++-- src/sat/sat_solver.h | 1 + src/sat/smt/arith_internalize.cpp | 1 + src/sat/smt/bv_solver.cpp | 9 ++++----- src/sat/smt/euf_proof.cpp | 3 ++- src/sat/smt/euf_solver.cpp | 7 +++++++ src/sat/tactic/goal2sat.cpp | 2 +- src/shell/drat_frontend.cpp | 22 ++++++++++++++-------- src/smt/seq_regex.cpp | 15 +++++++++------ 10 files changed, 42 insertions(+), 28 deletions(-) diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 6f3ccd809..20d7c8f1e 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -142,11 +142,6 @@ namespace sat { buffer[len++] = '\n'; m_out->write(buffer, len); - if (n == 3 && c[0] == literal(9357, true) && c[1] == literal(25, true) && c[2] == literal(8691, false)) { - m_out->flush(); - SASSERT(false); - UNREACHABLE(); - } } void drat::dump_activity() { diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 1a33a1ab7..0af1a3548 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3486,7 +3486,6 @@ namespace sat { return value(v) != l_undef && lvl(v) <= new_lvl; }; - for (unsigned i = old_num_vars; i < sz; ++i) { bool_var v = m_active_vars[i]; if (is_visited(v) || is_active(v)) { @@ -3496,7 +3495,9 @@ namespace sat { } else { set_eliminated(v, true); - m_free_vars.push_back(v); + if (!is_external(v) || true) { + m_free_vars.push_back(v); + } } } m_active_vars.shrink(j); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index f22fdcefe..5ada5ef88 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -669,6 +669,7 @@ namespace sat { void set_should_simplify() { m_next_simplify = m_conflicts_since_init; } bool_var_vector const& get_vars_to_reinit() const { return m_vars_to_reinit; } bool is_probing() const { return m_is_probing; } + bool is_free(bool_var v) const { return m_free_vars.contains(v); } public: void user_push() override; diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index a6668d367..b9370b1fe 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -436,6 +436,7 @@ namespace arith { if (_has_var) return v; theory_var w = mk_evar(n); + internalize_term(n); svector vars; for (unsigned i = 0; i < p; ++i) vars.push_back(register_theory_var_in_lar_solver(w)); diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index 50beead8c..f8d24147a 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -360,11 +360,12 @@ namespace bv { case bv_justification::kind_t::eq2bit: ++s_count; // std::cout << "eq2bit " << s_count << "\n"; -#if 1 +#if 0 if (s_count == 1899) { std::cout << "eq2bit " << mk_bounded_pp(var2expr(c.m_v1), m) << " == " << mk_bounded_pp(var2expr(c.m_v2), m) << "\n"; - std::cout << mk_bounded_pp(literal2expr(~c.m_antecedent), m, 2) << "\n"; - std::cout << mk_bounded_pp(literal2expr(c.m_consequent), m, 2) << "\n"; + std::cout << mk_bounded_pp(literal2expr(~c.m_antecedent), m, 4) << "\n"; + std::cout << mk_bounded_pp(literal2expr(c.m_consequent), m, 4) << "\n"; + std::cout << literal2expr(c.m_consequent) << "\n"; #if 0 solver_ref slv = mk_smt2_solver(m, ctx.s().params()); slv->assert_expr(eq); @@ -779,8 +780,6 @@ namespace bv { } sat::justification solver::mk_eq2bit_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a) { - if (v1 == 3202 && v2 == 3404) std::cout << a << " -> " << c << "\n"; - SASSERT(!(v1 == 3202 && v2 == 3404 && c.var() == 8691)); void* mem = get_region().allocate(bv_justification::get_obj_size()); sat::constraint_base::initialize(mem, this); auto* constraint = new (sat::constraint_base::ptr2mem(mem)) bv_justification(v1, v2, c, a); diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index 281906eae..4295ca2c8 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -76,7 +76,8 @@ namespace euf { if (!use_drat()) return; literal_vector lits; - for (literal lit : r) lits.push_back(~lit); + for (literal lit : r) + lits.push_back(~lit); if (l != sat::null_literal) lits.push_back(l); get_drat().add(lits, sat::status::th(true, get_id())); diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 28ced2898..206e8889f 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -692,6 +692,13 @@ namespace euf { finish_reinit(); for (auto* e : m_solvers) e->pop_reinit(); + +#if 0 + for (enode* n : m_egraph.nodes()) { + if (n->bool_var() != sat::null_bool_var && s().is_free(n->bool_var())) + std::cout << "has free " << n->bool_var() << "\n"; + } +#endif } bool solver::validate() { diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index e3d86c59b..e6d0cedd8 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -213,7 +213,7 @@ struct goal2sat::imp : public sat::sat_internalizer { sat::bool_var to_bool_var(expr* e) override { sat::literal l; sat::bool_var v = m_map.to_bool_var(e); - if (v != sat::null_bool_var) + if (v != sat::null_bool_var) return v; if (is_app(e) && m_cache.find(to_app(e), l) && !l.sign()) return l.var(); diff --git a/src/shell/drat_frontend.cpp b/src/shell/drat_frontend.cpp index 31646009b..3271a31e1 100644 --- a/src/shell/drat_frontend.cpp +++ b/src/shell/drat_frontend.cpp @@ -71,10 +71,12 @@ class smt_checker { void add_units() { auto const& units = m_drat.units(); +#if 0 for (unsigned i = m_units.size(); i < units.size(); ++i) { sat::literal lit = units[i]; m_lemma_solver->assert_expr(lit2expr(lit)); } +#endif m_units.append(units.size() - m_units.size(), units.c_ptr() + m_units.size()); } @@ -113,20 +115,22 @@ class smt_checker { std::cout << "drup\n"; return; } - m_lemma_solver->push(); - for (auto lit : drup_units) - m_lemma_solver->assert_expr(lit2expr(lit)); - lbool is_sat = m_lemma_solver->check_sat(); + m_input_solver->push(); +// for (auto lit : drup_units) +// m_input_solver->assert_expr(lit2expr(lit)); + for (auto lit : lits) + m_input_solver->assert_expr(lit2expr(~lit)); + lbool is_sat = m_input_solver->check_sat(); if (is_sat != l_false) { std::cout << "did not verify: " << lits << "\n"; for (sat::literal lit : lits) { std::cout << lit2expr(lit) << "\n"; } std::cout << "\n"; - m_lemma_solver->display(std::cout); + m_input_solver->display(std::cout); exit(0); } - m_lemma_solver->pop(1); + m_input_solver->pop(1); std::cout << "smt\n"; // check_assertion_redundant(lits); } @@ -280,8 +284,10 @@ static void verify_smt(char const* drat_file, char const* smt_file) { switch (r.m_tag) { case dimacs::drat_record::tag_t::is_clause: checker.add(r.m_lits, r.m_status); - if (drat_checker.inconsistent()) - std::cout << "inconsistent\n"; + if (drat_checker.inconsistent()) { + std::cout << "inconsistent\n"; + return; + } break; case dimacs::drat_record::tag_t::is_node: { expr_ref e(m); diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 41d0a10f5..3effad182 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -278,12 +278,15 @@ namespace smt { return; } - update_state_graph(r); - - if (m_state_graph.is_dead(get_state_id(r))) { - STRACE("seq_regex_brief", tout << "(dead) ";); - th.add_axiom(~lit); - return; + auto info = re().get_info(r); + if (info.interpreted) { + update_state_graph(r); + + if (m_state_graph.is_dead(get_state_id(r))) { + STRACE("seq_regex_brief", tout << "(dead) ";); + th.add_axiom(~lit); + return; + } } if (block_unfolding(lit, idx)) {